equal
deleted
inserted
replaced
158 closure example: |
158 closure example: |
159 *} |
159 *} |
160 |
160 |
161 lemma even_induct: |
161 lemma even_induct: |
162 assumes even: "even n" |
162 assumes even: "even n" |
163 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
163 shows "P 0 \<Longrightarrow> |
|
164 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
164 apply (atomize (full)) |
165 apply (atomize (full)) |
165 apply (cut_tac even) |
166 apply (cut_tac even) |
166 apply (unfold even_def) |
167 apply (unfold even_def) |
167 apply (drule spec [where x=P]) |
168 apply (drule spec [where x=P]) |
168 apply (drule spec [where x=Q]) |
169 apply (drule spec [where x=Q]) |