13250
|
1 |
(*<*)theory Rules = Main:(*>*)
|
11235
|
2 |
|
13238
|
3 |
section{*The Rules of the Game*}
|
11235
|
4 |
|
|
5 |
|
|
6 |
subsection{*Introduction Rules*}
|
|
7 |
|
13238
|
8 |
text{* Introduction rules for propositional logic:
|
|
9 |
\begin{center}
|
|
10 |
\begin{tabular}{ll}
|
|
11 |
@{thm[source]impI} & @{thm impI[no_vars]} \\
|
|
12 |
@{thm[source]conjI} & @{thm conjI[no_vars]} \\
|
|
13 |
@{thm[source]disjI1} & @{thm disjI1[no_vars]} \\
|
|
14 |
@{thm[source]disjI2} & @{thm disjI2[no_vars]} \\
|
|
15 |
@{thm[source]iffI} & @{thm iffI[no_vars]}
|
|
16 |
\end{tabular}
|
|
17 |
\end{center}
|
|
18 |
*}
|
|
19 |
|
13250
|
20 |
(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)
|
11235
|
21 |
|
|
22 |
lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
|
|
23 |
apply(rule impI)
|
|
24 |
apply(rule conjI)
|
|
25 |
apply assumption
|
|
26 |
apply(rule conjI)
|
|
27 |
apply assumption
|
|
28 |
apply assumption
|
|
29 |
done
|
|
30 |
|
|
31 |
|
|
32 |
subsection{*Elimination Rules*}
|
|
33 |
|
13238
|
34 |
text{* Elimination rules for propositional logic:
|
|
35 |
\begin{center}
|
|
36 |
\begin{tabular}{ll}
|
|
37 |
@{thm[source]impE} & @{thm impE[no_vars]} \\
|
|
38 |
@{thm[source]mp} & @{thm mp[no_vars]} \\
|
|
39 |
@{thm[source]conjE} & @{thm conjE[no_vars]} \\
|
|
40 |
@{thm[source]disjE} & @{thm disjE[no_vars]}
|
|
41 |
\end{tabular}
|
|
42 |
\end{center}
|
|
43 |
*}
|
|
44 |
(*<*)
|
11235
|
45 |
thm impE mp
|
|
46 |
thm conjE
|
|
47 |
thm disjE
|
13238
|
48 |
(*>*)
|
|
49 |
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
|
11235
|
50 |
apply (erule disjE)
|
|
51 |
apply (rule disjI2)
|
|
52 |
apply assumption
|
|
53 |
apply (rule disjI1)
|
|
54 |
apply assumption
|
|
55 |
done
|
|
56 |
|
|
57 |
|
|
58 |
subsection{*Destruction Rules*}
|
|
59 |
|
13238
|
60 |
text{* Destruction rules for propositional logic:
|
|
61 |
\begin{center}
|
|
62 |
\begin{tabular}{ll}
|
|
63 |
@{thm[source]conjunct1} & @{thm conjunct1[no_vars]} \\
|
|
64 |
@{thm[source]conjunct2} & @{thm conjunct2[no_vars]} \\
|
|
65 |
@{thm[source]iffD1} & @{thm iffD1[no_vars]} \\
|
|
66 |
@{thm[source]iffD2} & @{thm iffD2[no_vars]}
|
|
67 |
\end{tabular}
|
|
68 |
\end{center}
|
|
69 |
*}
|
|
70 |
|
13250
|
71 |
(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)
|
13238
|
72 |
|
11235
|
73 |
lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
|
|
74 |
apply (rule conjI)
|
|
75 |
apply (drule conjunct2)
|
|
76 |
apply assumption
|
|
77 |
apply (drule conjunct1)
|
|
78 |
apply assumption
|
|
79 |
done
|
|
80 |
|
|
81 |
|
|
82 |
subsection{*Quantifiers*}
|
|
83 |
|
13238
|
84 |
text{* Quantifier rules:
|
|
85 |
\begin{center}
|
|
86 |
\begin{tabular}{ll}
|
|
87 |
@{thm[source]allI} & @{thm allI[no_vars]} \\
|
|
88 |
@{thm[source]exI} & @{thm exI[no_vars]} \\
|
|
89 |
@{thm[source]allE} & @{thm allE[no_vars]} \\
|
|
90 |
@{thm[source]exE} & @{thm exE[no_vars]} \\
|
|
91 |
@{thm[source]spec} & @{thm spec[no_vars]}
|
|
92 |
\end{tabular}
|
|
93 |
\end{center}
|
|
94 |
*}
|
|
95 |
(*<*)
|
11235
|
96 |
thm allI exI
|
|
97 |
thm allE exE
|
|
98 |
thm spec
|
13238
|
99 |
(*>*)
|
11235
|
100 |
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
|
13238
|
101 |
(*<*)oops(*>*)
|
11235
|
102 |
|
|
103 |
subsection{*Instantiation*}
|
|
104 |
|
|
105 |
lemma "\<exists>xs. xs @ xs = xs"
|
|
106 |
apply(rule_tac x = "[]" in exI)
|
|
107 |
by simp
|
|
108 |
|
|
109 |
lemma "\<forall>xs. f(xs @ xs) = xs \<Longrightarrow> f [] = []"
|
|
110 |
apply(erule_tac x = "[]" in allE)
|
|
111 |
by simp
|
|
112 |
|
|
113 |
|
|
114 |
subsection{*Automation*}
|
|
115 |
|
|
116 |
lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
|
|
117 |
\<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
|
|
118 |
(\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
|
|
119 |
(\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
|
|
120 |
(\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
|
|
121 |
\<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
|
|
122 |
by blast
|
|
123 |
|
|
124 |
lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
|
|
125 |
(\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
|
|
126 |
by fast
|
|
127 |
|
|
128 |
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
|
|
129 |
apply(clarify)
|
|
130 |
by blast
|
|
131 |
|
|
132 |
|
|
133 |
subsection{*Forward Proof*}
|
|
134 |
|
13238
|
135 |
text{*
|
|
136 |
Instantiation of unknowns (in left-to-right order):
|
|
137 |
\begin{center}
|
|
138 |
\begin{tabular}{@ {}ll@ {}}
|
|
139 |
@{thm[source]append_self_conv} & @{thm append_self_conv} \\
|
|
140 |
@{thm[source]append_self_conv[of _ "[]"]} & @{thm append_self_conv[of _ "[]"]}
|
|
141 |
\end{tabular}
|
|
142 |
\end{center}
|
|
143 |
Applying one theorem to another
|
|
144 |
by unifying the premise of one theorem with the conclusion of another:
|
|
145 |
\begin{center}
|
|
146 |
\begin{tabular}{@ {}ll@ {}}
|
|
147 |
@{thm[source]sym} & @{thm sym} \\
|
|
148 |
@{thm[source]sym[OF append_self_conv]} & @{thm sym[OF append_self_conv]}\\
|
|
149 |
@{thm[source]append_self_conv[THEN sym]} & @{thm append_self_conv[THEN sym]}
|
|
150 |
\end{tabular}
|
|
151 |
\end{center}
|
|
152 |
*}
|
|
153 |
(*<*)
|
|
154 |
thm append_self_conv
|
|
155 |
thm append_self_conv[of _ "[]"]
|
11235
|
156 |
thm sym
|
13238
|
157 |
thm sym[OF append_self_conv]
|
|
158 |
thm append_self_conv[THEN sym]
|
|
159 |
(*>*)
|
11235
|
160 |
subsection{*Further Useful Methods*}
|
|
161 |
|
|
162 |
lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
|
|
163 |
apply(subgoal_tac "n=1")
|
|
164 |
apply simp
|
|
165 |
apply arith
|
|
166 |
done
|
|
167 |
|
13238
|
168 |
text{* And a cute example: *}
|
11235
|
169 |
lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
|
|
170 |
\<forall>x y z. sqrt x * sqrt x = x \<and>
|
|
171 |
x ^ 2 = x * x \<and>
|
|
172 |
(x ^ y) ^ z = x ^ (y*z)
|
|
173 |
\<rbrakk> \<Longrightarrow> \<exists>a b. a \<notin> Q \<and> b \<notin> Q \<and> a ^ b \<in> Q"
|
|
174 |
(*
|
|
175 |
apply(case_tac "")
|
|
176 |
apply blast
|
|
177 |
apply(rule_tac x = "" in exI)
|
|
178 |
apply(rule_tac x = "" in exI)
|
|
179 |
apply simp
|
|
180 |
done
|
|
181 |
*)
|
13250
|
182 |
(*<*)oops
|
|
183 |
|
|
184 |
end(*>*)
|