equal
deleted
inserted
replaced
216 |
216 |
217 |
217 |
218 thm akind_aty_atrm.induct |
218 thm akind_aty_atrm.induct |
219 thm kind_ty_trm.induct |
219 thm kind_ty_trm.induct |
220 |
220 |
221 ML {* |
|
222 val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} |
|
223 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} |
|
224 val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot |
|
225 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot |
|
226 *} |
|
227 |
221 |
228 lemma |
222 lemma |
229 assumes a0: |
223 assumes a0: |
230 "P1 TYP TYP" |
224 "P1 TYP TYP" |
231 and a1: |
225 and a1: |
259 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
253 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
260 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
254 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
261 apply - |
255 apply - |
262 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
256 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
263 apply(tactic {* regularize_tac @{context} 1 *}) |
257 apply(tactic {* regularize_tac @{context} 1 *}) |
264 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
258 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
265 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
259 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
266 apply(tactic {* clean_tac @{context} 1 *}) |
260 apply(tactic {* clean_tac @{context} 1 *}) |
267 (* |
261 (* |
268 Profiling: |
262 Profiling: |
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
263 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |