1 (*<*)theory Rules = Main:(*>*) |
|
2 |
|
3 section{*The Rules of the Game*} |
|
4 |
|
5 |
|
6 subsection{*Introduction Rules*} |
|
7 |
|
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 |
|
20 (*<*)thm impI conjI disjI1 disjI2 iffI(*>*) |
|
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 |
|
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 (*<*) |
|
45 thm impE mp |
|
46 thm conjE |
|
47 thm disjE |
|
48 (*>*) |
|
49 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P" |
|
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 |
|
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 |
|
71 (*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*) |
|
72 |
|
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 |
|
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 (*<*) |
|
96 thm allI exI |
|
97 thm allE exE |
|
98 thm spec |
|
99 (*>*) |
|
100 lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y" |
|
101 (*<*)oops(*>*) |
|
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 |
|
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 _ "[]"] |
|
156 thm sym |
|
157 thm sym[OF append_self_conv] |
|
158 thm append_self_conv[THEN sym] |
|
159 (*>*) |
|
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 |
|
168 text{* And a cute example: *} |
|
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 *) |
|
182 (*<*)oops |
|
183 |
|
184 end(*>*) |
|