257 |
257 |
258 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
258 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
259 ML {* val consts = lookup_quot_consts defs *} |
259 ML {* val consts = lookup_quot_consts defs *} |
260 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
260 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
261 |
261 |
262 ML {* val t_a = atomize_thm @{thm alpha.induct} *} |
262 ML {* val t_a = atomize_thm @{thm alpha.cases} *} |
263 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
263 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
264 ML_prf {* fun tac ctxt = |
264 ML_prf {* fun tac ctxt = |
265 (FIRST' [ |
265 (FIRST' [ |
266 rtac rel_refl, |
266 rtac rel_refl, |
267 atac, |
267 atac, |
276 ]); |
276 ]); |
277 *} |
277 *} |
278 apply (tactic {* tac @{context} 1 *}) *) |
278 apply (tactic {* tac @{context} 1 *}) *) |
279 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
279 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
280 |
280 |
281 (*ML {* |
281 ML {* |
282 val rt = build_repabs_term @{context} t_r consts rty qty |
282 val rt = build_repabs_term @{context} t_r consts rty qty |
283 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
283 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
284 *} |
284 *} |
285 prove rg |
285 prove rg |
286 apply(atomize(full)) |
286 apply(atomize(full)) |
287 ML_prf {* |
287 (*ML_prf {* |
288 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
288 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
289 (FIRST' [ |
289 (FIRST' [ |
290 rtac trans_thm, |
290 rtac trans_thm, |
291 LAMBDA_RES_TAC ctxt, |
291 LAMBDA_RES_TAC ctxt, |
292 res_forall_rsp_tac ctxt, |
292 res_forall_rsp_tac ctxt, |
306 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
306 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
307 THEN_ALL_NEW (fn _ => no_tac) |
307 THEN_ALL_NEW (fn _ => no_tac) |
308 ), |
308 ), |
309 WEAK_LAMBDA_RES_TAC ctxt |
309 WEAK_LAMBDA_RES_TAC ctxt |
310 ]); |
310 ]); |
|
311 *}*) |
|
312 ML_prf {* |
311 fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms |
313 fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms |
312 *} |
314 *} |
|
315 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
316 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
317 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
318 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
319 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
320 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
321 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
322 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
323 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
324 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
325 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
326 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
327 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
328 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
329 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
330 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
331 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
332 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
333 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
334 |
|
335 |
|
336 |
|
337 |
|
338 |
|
339 |
313 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
340 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
314 *) |
341 |
315 |
342 |
316 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
343 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
317 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
344 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
318 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
345 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
319 ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} |
346 ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} |