equal
deleted
inserted
replaced
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
214 |
214 |
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 |
|
219 ML {* val defs = |
|
220 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
|
221 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
|
222 *} |
|
223 |
218 |
224 ML {* |
219 ML {* |
225 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
220 val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} |
226 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
221 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} |
227 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
222 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} |
262 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
257 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
258 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
264 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 |
265 apply - |
260 apply - |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
|
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
|
263 prefer 2 |
|
264 apply(tactic {* clean_tac @{context} quot 1 *}) |
267 (* |
265 (* |
268 Profiling: |
266 Profiling: |
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
267 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)) *} |
268 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)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
|
270 ML_prf {* PolyML.profiling 1 *} |
|
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
272 *) |
272 *) |
273 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
273 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
274 prefer 2 |
|
275 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
|
276 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) |
|
277 done |
274 done |
278 |
275 |
279 (* Does not work: |
276 (* Does not work: |
280 lemma |
277 lemma |
281 assumes a0: "P1 TYP" |
278 assumes a0: "P1 TYP" |
301 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
298 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
302 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
299 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
303 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
300 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
304 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
301 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
305 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
306 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
303 apply(tactic {* clean_tac @{context} quot 1 *}) |
307 done |
304 done |
308 |
305 |
309 print_quotients |
306 print_quotients |
310 |
307 |
311 end |
308 end |