| changeset 62020 | 5d208fd2507d |
| parent 61489 | b8d375aee0df |
| child 69590 | e65314985426 |
| 62019:9de1eb745aeb | 62020:5d208fd2507d |
|---|---|
24 apply (erule ifE) |
24 apply (erule ifE) |
25 apply (rule ifI) |
25 apply (rule ifI) |
26 apply (rule ifI) |
26 apply (rule ifI) |
27 oops |
27 oops |
28 |
28 |
29 text\<open>Trying again from the beginning in order to use @{text blast}\<close> |
29 text\<open>Trying again from the beginning in order to use \<open>blast\<close>\<close> |
30 declare ifI [intro!] |
30 declare ifI [intro!] |
31 declare ifE [elim!] |
31 declare ifE [elim!] |
32 |
32 |
33 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))" |
33 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))" |
34 by blast |
34 by blast |
43 |
43 |
44 |
44 |
45 text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close> |
45 text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close> |
46 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))" |
46 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))" |
47 apply auto |
47 apply auto |
48 -- \<open>The next step will fail unless subgoals remain\<close> |
48 \<comment> \<open>The next step will fail unless subgoals remain\<close> |
49 apply (tactic all_tac) |
49 apply (tactic all_tac) |
50 oops |
50 oops |
51 |
51 |
52 text \<open>Trying again from the beginning in order to prove from the definitions.\<close> |
52 text \<open>Trying again from the beginning in order to prove from the definitions.\<close> |
53 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))" |
53 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))" |
54 unfolding if_def |
54 unfolding if_def |
55 apply auto |
55 apply auto |
56 -- \<open>The next step will fail unless subgoals remain\<close> |
56 \<comment> \<open>The next step will fail unless subgoals remain\<close> |
57 apply (tactic all_tac) |
57 apply (tactic all_tac) |
58 oops |
58 oops |
59 |
59 |
60 end |
60 end |