equal
deleted
inserted
replaced
310 apply (induct x rule: inducts(9)) |
310 apply (induct x rule: inducts(9)) |
311 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
311 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
312 apply (simp) |
312 apply (simp) |
313 oops |
313 oops |
314 |
314 |
315 lemma |
315 lemma strong_inudction_principle: |
316 assumes a01: "\<And>b. P1 b KStar" |
316 assumes a01: "\<And>b. P1 b KStar" |
317 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
317 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
318 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
318 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
319 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
319 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
320 and a05: "\<And>char b. P3 b (TC char)" |
320 and a05: "\<And>char b. P3 b (TC char)" |