285 and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" |
285 and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" |
286 shows "P1 mkind \<and> P2 mty \<and> P3 mtrm" |
286 shows "P1 mkind \<and> P2 mty \<and> P3 mtrm" |
287 using a0 a1 a2 a3 a4 a5 a6 a7 a8 |
287 using a0 a1 a2 a3 a4 a5 a6 a7 a8 |
288 *) |
288 *) |
289 |
289 |
290 lemma "\<lbrakk>P1 TYP; |
290 lemma "\<lbrakk>P TYP; |
291 \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind); |
291 \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind); |
292 \<And>id. P2 (TCONST id); |
292 \<And>id. Q (TCONST id); |
293 \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm); |
293 \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm); |
294 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
294 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
295 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
295 \<And>id. R (CONS id); \<And>name. R (VAR name); |
296 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
296 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (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>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
298 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
298 \<Longrightarrow> P mkind \<and> Q mty \<and> R 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} @{thms alpha_equivps} 1 *}) |
300 done |
300 done |
301 |
301 |
302 print_quotients |
302 print_quotients |
303 |
303 |