10 definition "if" :: "[o,o,o]=>o" where |
10 definition "if" :: "[o,o,o]=>o" where |
11 "if(P,Q,R) == P&Q | ~P&R" |
11 "if(P,Q,R) == P&Q | ~P&R" |
12 |
12 |
13 lemma ifI: |
13 lemma ifI: |
14 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
14 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
15 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
15 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
16 apply (simp add: if_def) |
16 apply (simp add: if_def) |
17 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
17 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
18 apply blast |
18 apply blast |
19 done |
19 done |
20 |
20 |
21 lemma ifE: |
21 lemma ifE: |
22 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S" |
22 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S" |
23 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
23 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
24 apply (simp add: if_def) |
24 apply (simp add: if_def) |
25 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
25 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
26 apply blast |
26 apply blast |
27 done |
27 done |
28 |
28 |
29 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
29 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
30 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
30 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
31 apply (rule iffI) |
31 apply (rule iffI) |
32 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
32 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
33 apply (erule ifE) |
33 apply (erule ifE) |
34 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
34 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
35 apply (erule ifE) |
35 apply (erule ifE) |
36 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
36 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
37 apply (rule ifI) |
37 apply (rule ifI) |
38 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
38 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
39 apply (rule ifI) |
39 apply (rule ifI) |
40 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
40 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
41 oops |
41 oops |
42 |
42 |
43 text\<open>Trying again from the beginning in order to use @{text blast}\<close> |
43 text\<open>Trying again from the beginning in order to use @{text blast}\<close> |
44 declare ifI [intro!] |
44 declare ifI [intro!] |
45 declare ifE [elim!] |
45 declare ifE [elim!] |
47 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
47 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
48 by blast |
48 by blast |
49 |
49 |
50 |
50 |
51 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
51 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
52 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
52 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
53 by blast |
53 by blast |
54 |
54 |
55 text\<open>Trying again from the beginning in order to prove from the definitions\<close> |
55 text\<open>Trying again from the beginning in order to prove from the definitions\<close> |
56 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
56 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
57 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
57 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
58 apply (simp add: if_def) |
58 apply (simp add: if_def) |
59 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
59 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
60 apply blast |
60 apply blast |
61 done |
61 done |
62 |
62 |
63 |
63 |
64 text\<open>An invalid formula. High-level rules permit a simpler diagnosis\<close> |
64 text\<open>An invalid formula. High-level rules permit a simpler diagnosis\<close> |
65 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
65 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
66 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
66 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
67 apply auto |
67 apply auto |
68 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
68 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
69 (*The next step will fail unless subgoals remain*) |
69 (*The next step will fail unless subgoals remain*) |
70 apply (tactic all_tac) |
70 apply (tactic all_tac) |
71 oops |
71 oops |
72 |
72 |
73 text\<open>Trying again from the beginning in order to prove from the definitions\<close> |
73 text\<open>Trying again from the beginning in order to prove from the definitions\<close> |
74 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
74 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
75 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
75 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
76 apply (simp add: if_def) |
76 apply (simp add: if_def) |
77 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
77 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
78 apply (auto) |
78 apply (auto) |
79 \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close> |
79 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
80 (*The next step will fail unless subgoals remain*) |
80 (*The next step will fail unless subgoals remain*) |
81 apply (tactic all_tac) |
81 apply (tactic all_tac) |
82 oops |
82 oops |
83 |
83 |
84 |
84 |