115 |
115 |
116 To see better where we are, let us explicitly name the assumptions |
116 To see better where we are, let us explicitly name the assumptions |
117 by starting a subproof. |
117 by starting a subproof. |
118 \<close> |
118 \<close> |
119 |
119 |
|
120 subgoal premises for P |
120 proof - |
121 proof - |
121 case (goal1 P) |
|
122 have p1: "R x y" by fact |
122 have p1: "R x y" by fact |
123 have p2: "\<forall>P. (\<forall>x. P x x) |
123 have p2: "\<forall>P. (\<forall>x. P x x) |
124 \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact |
124 \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact |
125 have r1: "\<forall>x. P x x" by fact |
125 have r1: "\<forall>x. P x x" by fact |
126 have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
126 have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
153 |
153 |
154 apply(rule p1) |
154 apply(rule p1) |
155 apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2]) |
155 apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2]) |
156 done |
156 done |
157 qed |
157 qed |
|
158 done |
158 |
159 |
159 text \<open> |
160 text \<open> |
160 Now we are done. It might be surprising that we are not using the automatic |
161 Now we are done. It might be surprising that we are not using the automatic |
161 tactics available in Isabelle/HOL for proving this lemmas. After all \<open>blast\<close> would easily dispense of it. |
162 tactics available in Isabelle/HOL for proving this lemmas. After all \<open>blast\<close> would easily dispense of it. |
162 \<close> |
163 \<close> |
229 |
230 |
230 lemma %linenos evenS: |
231 lemma %linenos evenS: |
231 shows "odd m \<Longrightarrow> even (Suc m)" |
232 shows "odd m \<Longrightarrow> even (Suc m)" |
232 apply (unfold odd_def even_def) |
233 apply (unfold odd_def even_def) |
233 apply (rule allI impI)+ |
234 apply (rule allI impI)+ |
|
235 subgoal premises for P Q |
234 proof - |
236 proof - |
235 case (goal1 P Q) |
|
236 have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
237 have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
237 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact |
238 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact |
238 have r1: "P 0" by fact |
239 have r1: "P 0" by fact |
239 have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact |
240 have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact |
240 have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact |
241 have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact |
242 apply(rule r2[rule_format]) |
243 apply(rule r2[rule_format]) |
243 apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q], |
244 apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q], |
244 THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3]) |
245 THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3]) |
245 done |
246 done |
246 qed |
247 qed |
|
248 done |
247 |
249 |
248 text \<open> |
250 text \<open> |
249 The interesting lines are 7 to 15. Again, the assumptions fall into two categories: |
251 The interesting lines are 7 to 15. Again, the assumptions fall into two categories: |
250 \<open>p1\<close> corresponds to the premise of the introduction rule; \<open>r1\<close> |
252 \<open>p1\<close> corresponds to the premise of the introduction rule; \<open>r1\<close> |
251 to \<open>r3\<close> come from the definition of \<open>even\<close>. |
253 to \<open>r3\<close> come from the definition of \<open>even\<close>. |
278 |
280 |
279 lemma %linenos accpartI: |
281 lemma %linenos accpartI: |
280 shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
282 shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
281 apply (unfold accpart_def) |
283 apply (unfold accpart_def) |
282 apply (rule allI impI)+ |
284 apply (rule allI impI)+ |
|
285 subgoal premises for P |
283 proof - |
286 proof - |
284 case (goal1 P) |
|
285 have p1: "\<And>y. R y x \<Longrightarrow> |
287 have p1: "\<And>y. R y x \<Longrightarrow> |
286 (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact |
288 (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact |
287 have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact |
289 have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact |
288 show "P x" |
290 show "P x" |
289 apply(rule r1[rule_format]) |
291 apply(rule r1[rule_format]) |
|
292 subgoal premises for y |
290 proof - |
293 proof - |
291 case (goal1 y) |
|
292 have r1_prem: "R y x" by fact |
294 have r1_prem: "R y x" by fact |
293 show "P y" |
295 show "P y" |
294 apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1]) |
296 apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1]) |
295 done |
297 done |
296 qed |
298 qed |
|
299 done |
297 qed |
300 qed |
|
301 done |
298 |
302 |
299 text \<open> |
303 text \<open> |
300 As you can see, there are now two subproofs. The assumptions fall as usual into |
304 As you can see, there are now two subproofs. The assumptions fall as usual into |
301 two categories (Lines 7 to 9). In Line 11, applying the assumption \<open>r1\<close> generates a goal state with the new local assumption @{term "R y x"}, |
305 two categories (Lines 7 to 9). In Line 11, applying the assumption \<open>r1\<close> generates a goal state with the new local assumption @{term "R y x"}, |
302 named \<open>r1_prem\<close> in the second subproof (Line 14). This local assumption is |
306 named \<open>r1_prem\<close> in the second subproof (Line 14). This local assumption is |