65 and "M \<approx>tr M" |
65 and "M \<approx>tr M" |
66 apply(induct K and A and M rule: kind_ty_trm.inducts) |
66 apply(induct K and A and M rule: kind_ty_trm.inducts) |
67 apply(auto intro: akind_aty_atrm.intros) |
67 apply(auto intro: akind_aty_atrm.intros) |
68 done |
68 done |
69 |
69 |
70 lemma alpha_EQUIVs: |
70 lemma alpha_equivps: |
71 shows "EQUIV akind" |
71 shows "equivp akind" |
72 and "EQUIV aty" |
72 and "equivp aty" |
73 and "EQUIV atrm" |
73 and "equivp atrm" |
74 sorry |
74 sorry |
75 |
75 |
76 quotient KIND = kind / akind |
76 quotient KIND = kind / akind |
77 by (rule alpha_EQUIVs) |
77 by (rule alpha_equivps) |
78 |
78 |
79 quotient TY = ty / aty |
79 quotient TY = ty / aty |
80 and TRM = trm / atrm |
80 and TRM = trm / atrm |
81 by (auto intro: alpha_EQUIVs) |
81 by (auto intro: alpha_equivps) |
82 |
82 |
83 print_quotients |
83 print_quotients |
84 |
84 |
85 quotient_def |
85 quotient_def |
86 TYP :: "KIND" |
86 TYP :: "KIND" |
215 |
215 |
216 thm akind_aty_atrm.induct |
216 thm akind_aty_atrm.induct |
217 thm kind_ty_trm.induct |
217 thm kind_ty_trm.induct |
218 |
218 |
219 ML {* |
219 ML {* |
220 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
220 val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} |
221 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
221 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} |
222 (*val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}*) |
222 (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*) |
223 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
223 val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quot |
224 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
224 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
225 *} |
225 *} |
226 |
226 |
227 lemma |
227 lemma |
228 assumes a0: |
228 assumes a0: |
256 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
256 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
257 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
257 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
258 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
258 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
260 apply - |
260 apply - |
261 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *}) |
261 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *}) |
262 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
262 (*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) |
263 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
263 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
265 *) |
265 *) |
266 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) |
266 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) |
267 (* |
267 (* |
268 Profiling: |
268 Profiling: |
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
270 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
270 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
271 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
271 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
272 ML_prf {* PolyML.profiling 1 *} |
272 ML_prf {* PolyML.profiling 1 *} |
273 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
273 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
274 *) |
274 *) |
275 done |
275 done |
276 |
276 |
296 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
296 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
297 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
297 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
298 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
298 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
299 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
299 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
300 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
300 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
301 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *}) |
301 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *}) |
302 done |
302 done |
303 |
303 |
304 print_quotients |
304 print_quotients |
305 |
305 |
306 end |
306 end |