equal
deleted
inserted
replaced
71 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
71 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
72 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
72 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
73 and a9: "\<And>c. P3 c (BNil)" |
73 and a9: "\<And>c. P3 c (BNil)" |
74 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
74 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
75 shows "P1 c t" "P2 c as" "P3 c as'" |
75 shows "P1 c t" "P2 c as" "P3 c as'" |
76 using assms |
76 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) |
77 apply(induction_schema) |
|
78 apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1)) |
77 apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1)) |
79 apply(simp_all)[7] |
78 apply(simp_all)[7] |
80 apply(rule_tac ya="as"in foo.strong_exhaust(2)) |
79 apply(rule_tac ya="as"in foo.strong_exhaust(2)) |
81 apply(simp_all)[1] |
80 apply(simp_all)[1] |
82 apply(rule_tac yb="as'" in foo.strong_exhaust(3)) |
81 apply(rule_tac yb="as'" in foo.strong_exhaust(3)) |