15 lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P; Suc x < 5\<rbrakk> \<Longrightarrow> R" |
15 lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P; Suc x < 5\<rbrakk> \<Longrightarrow> R" |
16 by (drule mp, (assumption|arith))+ |
16 by (drule mp, (assumption|arith))+ |
17 |
17 |
18 text{*exercise: what's going on here?*} |
18 text{*exercise: what's going on here?*} |
19 lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R" |
19 lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R" |
20 by (drule mp, intro?, assumption+)+ |
20 by (drule mp, (intro conjI)?, assumption+)+ |
21 |
21 |
22 text{*defer and prefer*} |
22 text{*defer and prefer*} |
23 |
23 |
24 lemma "hard \<and> (P \<or> ~P) \<and> (Q\<longrightarrow>Q)" |
24 lemma "hard \<and> (P \<or> ~P) \<and> (Q\<longrightarrow>Q)" |
25 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
25 apply (intro conjI) --{* @{subgoals[display,indent=0,margin=65]} *} |
26 defer 1 --{* @{subgoals[display,indent=0,margin=65]} *} |
26 defer 1 --{* @{subgoals[display,indent=0,margin=65]} *} |
27 apply blast+ --{* @{subgoals[display,indent=0,margin=65]} *} |
27 apply blast+ --{* @{subgoals[display,indent=0,margin=65]} *} |
28 oops |
28 oops |
29 |
29 |
30 lemma "ok1 \<and> ok2 \<and> doubtful" |
30 lemma "ok1 \<and> ok2 \<and> doubtful" |
31 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
31 apply (intro conjI) --{* @{subgoals[display,indent=0,margin=65]} *} |
32 prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *} |
32 prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *} |
33 oops |
33 oops |
34 |
34 |
35 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6" |
35 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6" |
36 apply intro --{* @{subgoals[display,indent=0,margin=65]} *} |
36 apply (intro conjI) --{* @{subgoals[display,indent=0,margin=65]} *} |
37 txt{* @{subgoals[display,indent=0,margin=65]} |
37 txt{* @{subgoals[display,indent=0,margin=65]} |
38 A total of 6 subgoals... |
38 A total of 6 subgoals... |
39 *} |
39 *} |
40 oops |
40 oops |
41 |
41 |
42 |
42 |
43 |
43 |
44 (*needed??*) |
44 (*needed??*) |
45 |
45 |
46 lemma "(P\<or>Q) \<and> (R\<or>S) \<Longrightarrow> PP" |
46 lemma "(P\<or>Q) \<and> (R\<or>S) \<Longrightarrow> PP" |
47 apply elim |
47 apply (elim conjE disjE) |
48 oops |
48 oops |
49 |
49 |
50 lemma "((P\<or>Q) \<and> R) \<and> (Q \<and> (P\<or>S)) \<Longrightarrow> PP" |
50 lemma "((P\<or>Q) \<and> R) \<and> (Q \<and> (P\<or>S)) \<Longrightarrow> PP" |
51 apply (elim conjE) |
51 apply (elim conjE) |
52 oops |
52 oops |