384 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
384 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
385 ]; *} |
385 ]; *} |
386 apply (atomize(full)) |
386 apply (atomize(full)) |
387 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
387 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
388 done*) |
388 done*) |
389 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *} |
389 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
390 ML {* |
390 ML {* |
391 val rt = build_repabs_term @{context} t_r consts rty qty |
391 val rt = build_repabs_term @{context} t_r consts rty qty |
392 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
392 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
393 *} |
393 *} |
394 prove {* Syntax.check_term @{context} rg *} |
394 prove {* Syntax.check_term @{context} rg *} |
395 apply(atomize(full)) |
395 apply(atomize(full)) |
396 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
396 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
397 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
397 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
398 |
398 |
399 done |
399 done |
400 ML {* val t_t = |
400 ML {* |
401 Toplevel.program (fn () => |
401 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
402 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
|
403 ) |
|
404 *} |
402 *} |
405 |
403 |
406 ML {* val abs = findabs rty (prop_of (t_a)) *} |
404 ML {* val abs = findabs rty (prop_of (t_a)) *} |
407 ML {* val aps = findaps rty (prop_of (t_a)) *} |
405 ML {* val aps = findaps rty (prop_of (t_a)) *} |
408 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
406 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |