294 \<And>A A' M x x' M' B'. |
294 \<And>A A' M x x' M' B'. |
295 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
295 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
296 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
296 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
297 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
297 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
298 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
298 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
|
299 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
|
300 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
301 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
299 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
302 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
300 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
303 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
301 prefer 2 |
304 prefer 2 |
302 thm QUOTIENT_TY |
305 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
303 apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *}) |
306 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
304 |
307 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
305 |
308 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
|
309 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
|
310 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) |
|
311 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
312 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
313 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
|
314 apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *}) |
|
315 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
316 |
|
317 |
|
318 apply (tactic {* clean_tac @{context} defs aps 1 *}) |
|
319 ML_prf {* *} |
306 print_quotients |
320 print_quotients |
307 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*}) |
321 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*}) |
308 |
322 |
309 |
323 |
310 ML {* val consts = lookup_quot_consts defs *} |
324 ML {* val consts = lookup_quot_consts defs *} |