equal
deleted
inserted
replaced
256 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
256 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
257 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
257 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
259 apply - |
259 apply - |
260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) |
261 apply(tactic {* regularize_tac @{context} 1 *}) |
262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
263 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
263 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
265 (* |
265 (* |
266 Profiling: |
266 Profiling: |
294 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
294 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
295 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
295 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
296 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
296 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
297 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
297 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
298 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
298 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *}) |
299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
300 done |
300 done |
301 |
301 |
302 print_quotients |
302 print_quotients |
303 |
303 |
304 end |
304 end |