174 ML {* val qty = @{typ "lam"} *} |
174 ML {* val qty = @{typ "lam"} *} |
175 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
175 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
176 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
176 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
177 @{thms ho_all_prs ho_ex_prs} *} |
177 @{thms ho_all_prs ho_ex_prs} *} |
178 |
178 |
179 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
|
180 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
181 ML {* val consts = lookup_quot_consts defs *} |
180 ML {* val consts = lookup_quot_consts defs *} |
182 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
183 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
184 |
183 |
266 |
265 |
267 |
266 |
268 |
267 |
269 (* Construction Site code *) |
268 (* Construction Site code *) |
270 |
269 |
271 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
272 ML {* val consts = lookup_quot_consts defs *} |
|
273 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
|
274 |
|
275 ML {* val t_a = atomize_thm @{thm alpha.cases} *} |
|
276 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
|
277 ML_prf {* fun tac ctxt = |
|
278 (FIRST' [ |
|
279 rtac rel_refl, |
|
280 atac, |
|
281 rtac @{thm universal_twice}, |
|
282 (rtac @{thm impI} THEN' atac), |
|
283 rtac @{thm implication_twice}, |
|
284 EqSubst.eqsubst_tac ctxt [0] |
|
285 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
286 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
287 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
|
288 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
289 ]); |
|
290 *} |
|
291 apply (tactic {* tac @{context} 1 *}) *) |
|
292 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
293 |
|
294 ML {* |
|
295 val rt = build_repabs_term @{context} t_r consts rty qty |
|
296 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
|
297 *} |
|
298 prove rg |
|
299 apply(atomize(full)) |
|
300 (*ML_prf {* |
|
301 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
302 (FIRST' [ |
|
303 rtac trans_thm, |
|
304 LAMBDA_RES_TAC ctxt, |
|
305 res_forall_rsp_tac ctxt, |
|
306 res_exists_rsp_tac ctxt, |
|
307 ( |
|
308 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
|
309 THEN_ALL_NEW (fn _ => no_tac) |
|
310 ), |
|
311 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
312 rtac refl, |
|
313 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
314 Cong_Tac.cong_tac @{thm cong}, |
|
315 rtac @{thm ext}, |
|
316 rtac reflex_thm, |
|
317 atac, |
|
318 ( |
|
319 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
320 THEN_ALL_NEW (fn _ => no_tac) |
|
321 ), |
|
322 WEAK_LAMBDA_RES_TAC ctxt |
|
323 ]); |
|
324 *}*) |
|
325 ML_prf {* |
|
326 fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms |
|
327 *} |
|
328 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
329 |
|
330 |
|
331 |
|
332 |
|
333 |
|
334 |
|
335 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
336 |
|
337 |
|
338 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
339 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
340 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
341 ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
342 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *} |
|
343 ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *} |
|
344 ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *} |
|
345 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
|
346 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
|
347 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *} |
|
348 ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *} |
|
349 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
|
350 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} |
|
351 ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *} |
|
352 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} |
|
353 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
354 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} |
|
355 ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} |
|
356 ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} |
|
357 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} |
|
358 |
|
359 (*local_setup {* |
|
360 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
|
361 *}*) |
|
362 |
|
363 thm alpha_induct |
|
364 thm alpha.induct |
|
365 |
|
366 |
270 |
367 |
271 |
368 |
272 |
369 |
273 |
370 |
274 |