|
41777
|
1 |
(* Title: FOL/ex/If.thy
|
|
14151
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
3 |
Copyright 1991 University of Cambridge
|
|
14957
|
4 |
*)
|
|
14151
|
5 |
|
|
60770
|
6 |
section \<open>First-Order Logic: the 'if' example\<close>
|
|
14151
|
7 |
|
|
61489
|
8 |
theory If
|
|
|
9 |
imports FOL
|
|
|
10 |
begin
|
|
14151
|
11 |
|
|
69590
|
12 |
definition "if" :: \<open>[o,o,o]=>o\<close>
|
|
|
13 |
where \<open>if(P,Q,R) \<equiv> P \<and> Q \<or> \<not> P \<and> R\<close>
|
|
61489
|
14 |
|
|
69590
|
15 |
lemma ifI: \<open>\<lbrakk>P \<Longrightarrow> Q; \<not> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> if(P,Q,R)\<close>
|
|
61489
|
16 |
unfolding if_def by blast
|
|
14151
|
17 |
|
|
69590
|
18 |
lemma ifE: \<open>\<lbrakk>if(P,Q,R); \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> S; \<lbrakk>\<not> P; R\<rbrakk> \<Longrightarrow> S\<rbrakk> \<Longrightarrow> S\<close>
|
|
61489
|
19 |
unfolding if_def by blast
|
|
14151
|
20 |
|
|
69590
|
21 |
lemma if_commute: \<open>if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))\<close>
|
|
61489
|
22 |
apply (rule iffI)
|
|
|
23 |
apply (erule ifE)
|
|
|
24 |
apply (erule ifE)
|
|
|
25 |
apply (rule ifI)
|
|
|
26 |
apply (rule ifI)
|
|
|
27 |
oops
|
|
14151
|
28 |
|
|
62020
|
29 |
text\<open>Trying again from the beginning in order to use \<open>blast\<close>\<close>
|
|
14151
|
30 |
declare ifI [intro!]
|
|
|
31 |
declare ifE [elim!]
|
|
|
32 |
|
|
69590
|
33 |
lemma if_commute: \<open>if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))\<close>
|
|
61489
|
34 |
by blast
|
|
14151
|
35 |
|
|
|
36 |
|
|
69590
|
37 |
lemma \<open>if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))\<close>
|
|
61489
|
38 |
by blast
|
|
14151
|
39 |
|
|
60770
|
40 |
text\<open>Trying again from the beginning in order to prove from the definitions\<close>
|
|
69590
|
41 |
lemma \<open>if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))\<close>
|
|
61489
|
42 |
unfolding if_def by blast
|
|
14151
|
43 |
|
|
|
44 |
|
|
61489
|
45 |
text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close>
|
|
69590
|
46 |
lemma \<open>if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))\<close>
|
|
61489
|
47 |
apply auto
|
|
62020
|
48 |
\<comment> \<open>The next step will fail unless subgoals remain\<close>
|
|
61489
|
49 |
apply (tactic all_tac)
|
|
|
50 |
oops
|
|
14151
|
51 |
|
|
61489
|
52 |
text \<open>Trying again from the beginning in order to prove from the definitions.\<close>
|
|
69590
|
53 |
lemma \<open>if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))\<close>
|
|
61489
|
54 |
unfolding if_def
|
|
|
55 |
apply auto
|
|
62020
|
56 |
\<comment> \<open>The next step will fail unless subgoals remain\<close>
|
|
61489
|
57 |
apply (tactic all_tac)
|
|
|
58 |
oops
|
|
14151
|
59 |
|
|
0
|
60 |
end
|