1 theory Isar0 = Main: |
|
2 |
|
3 (* |
|
4 proof ::= "proof" [method] statement* "qed" |
|
5 | "by" method |
|
6 statement ::= "fix" variables |
|
7 | "assume" proposition* |
|
8 | ["then"] ("show" | "have") proposition proof |
|
9 proposition ::= [label":"] string |
|
10 |
|
11 Typical skelton: |
|
12 |
|
13 proof |
|
14 assume <assumptions> |
|
15 have <formula1> -- intermediate result |
|
16 : |
|
17 have <formulan> -- intermediate result |
|
18 show ?thesis -- the conclusion |
|
19 end |
|
20 *) |
|
21 |
|
22 lemma "A \<longrightarrow> A" |
|
23 proof (rule impI) |
|
24 assume A: "A" |
|
25 show "A" by(rule A) |
|
26 qed |
|
27 |
|
28 (* Operational reading: assume A - show A proves "A \<Longrightarrow> A", which rule impI |
|
29 turns into the desired "A \<longrightarrow> A". Too much (operational) text *) |
|
30 |
|
31 (* 1st Principle: let "proof" select the rule automatically; based on the |
|
32 goal and a predefined list of (introduction) rules. Here: impI is found |
|
33 automatically: *) |
|
34 |
|
35 lemma "A \<longrightarrow> A" |
|
36 proof |
|
37 assume A: "A" |
|
38 show "A" by(rule A) |
|
39 qed |
|
40 |
|
41 (* Proof by assumption should be trivial. Method "." does just that (and a |
|
42 bit more - see later). Thus naming of assumptions is often superfluous. *) |
|
43 |
|
44 lemma "A \<longrightarrow> A" |
|
45 proof |
|
46 assume "A" |
|
47 have "A" . |
|
48 qed |
|
49 |
|
50 (* To hide proofs by assumption, by(method) first applies method and then |
|
51 tries to solve all remaining subgoals by assumption. *) |
|
52 |
|
53 lemma "A \<longrightarrow> A & A" |
|
54 proof |
|
55 assume A |
|
56 show "A & A" by(rule conjI) |
|
57 qed |
|
58 |
|
59 (* Proofs of the form by(rule <rule>) can be abbreviated to ".." if <rule> is |
|
60 one of the predefined introduction rules (for user supplied rules see below). |
|
61 Thus |
|
62 *) |
|
63 |
|
64 lemma "A \<longrightarrow> A & A" |
|
65 proof |
|
66 assume A |
|
67 show "A & A" .. |
|
68 qed |
|
69 |
|
70 (* What happens: applies "conj" (first "."), then solves the two subgoals by |
|
71 assumptions (second ".") *) |
|
72 |
|
73 (* Now: elimination *) |
|
74 |
|
75 lemma "A & B \<longrightarrow> B & A" |
|
76 proof |
|
77 assume AB: "A & B" |
|
78 show "B & A" |
|
79 proof (rule conjE[OF AB]) |
|
80 assume A and B |
|
81 show ?thesis .. --"thesis = statement in previous show" |
|
82 qed |
|
83 qed |
|
84 |
|
85 (* Again: too much text. |
|
86 |
|
87 Elimination rules are used to conclude new stuff from old. In Isar they are |
|
88 triggered by propositions being fed INTO a proof block. Syntax: |
|
89 from <previously proved propositions> show \<dots> |
|
90 applies an elimination rule whose first premise matches one of the <previously proved propositions>. Thus: |
|
91 *) |
|
92 |
|
93 lemma "A & B \<longrightarrow> B & A" |
|
94 proof |
|
95 assume AB: "A & B" |
|
96 from AB show "B & A" |
|
97 proof |
|
98 assume A and B |
|
99 show ?thesis .. |
|
100 qed |
|
101 qed |
|
102 |
|
103 (* |
|
104 2nd principle: try to arrange sequence of propositions in a UNIX like |
|
105 pipe, such that the proof of the next proposition uses the previous |
|
106 one. The previous proposition can be referred to via "this". |
|
107 This greatly reduces the need for explicit naming of propositions. |
|
108 *) |
|
109 lemma "A & B \<longrightarrow> B & A" |
|
110 proof |
|
111 assume "A & B" |
|
112 from this show "B & A" |
|
113 proof |
|
114 assume A and B |
|
115 show ?thesis .. |
|
116 qed |
|
117 qed |
|
118 |
|
119 (* Final simplification: "from this" = "thus". |
|
120 |
|
121 Alternative: pure forward reasoning: *) |
|
122 |
|
123 lemma "A & B --> B & A" |
|
124 proof |
|
125 assume ab: "A & B" |
|
126 from ab have a: A .. |
|
127 from ab have b: B .. |
|
128 from b a show "B & A" .. |
|
129 qed |
|
130 |
|
131 (* New: itermediate haves *) |
|
132 |
|
133 (* The predefined introduction and elimination rules include all the usual |
|
134 natural deduction rules for propositional logic. Here is a longer example: *) |
|
135 |
|
136 lemma "~(A & B) \<longrightarrow> ~A | ~B" |
|
137 proof |
|
138 assume n: "~(A & B)" |
|
139 show "~A | ~B" |
|
140 proof (rule ccontr) |
|
141 assume nn: "~(~ A | ~B)" |
|
142 from n show False |
|
143 proof |
|
144 show "A & B" |
|
145 proof |
|
146 show A |
|
147 proof (rule ccontr) |
|
148 assume "~A" |
|
149 have "\<not> A \<or> \<not> B" .. |
|
150 from nn this show False .. |
|
151 qed |
|
152 next |
|
153 show B |
|
154 proof (rule ccontr) |
|
155 assume "~B" |
|
156 have "\<not> A \<or> \<not> B" .. |
|
157 from nn this show False .. |
|
158 qed |
|
159 qed |
|
160 qed |
|
161 qed |
|
162 qed; |
|
163 |
|
164 (* New: |
|
165 |
|
166 1. Multiple subgoals. When showing "A & B" we need to show both A and B. |
|
167 Each subgoal is proved separately, in ANY order. The individual proofs are |
|
168 separated by "next". |
|
169 |
|
170 2. "have" for proving an intermediate fact |
|
171 *) |
|
172 |
|
173 subsection{*Becoming more concise*} |
|
174 |
|
175 (* Normally want to prove rules expressed with \<Longrightarrow>, not \<longrightarrow> *) |
|
176 |
|
177 lemma "\<lbrakk> A \<Longrightarrow> False \<rbrakk> \<Longrightarrow> \<not> A" |
|
178 proof |
|
179 assume "A \<Longrightarrow> False" A |
|
180 thus False . |
|
181 qed |
|
182 |
|
183 (* In this case the "proof" works on the "~A", thus selecting notI |
|
184 |
|
185 Now: avoid repeating formulae (which may be large). *) |
|
186 |
|
187 lemma "(large_formula \<Longrightarrow> False) \<Longrightarrow> ~ large_formula" |
|
188 (is "(?P \<Longrightarrow> _) \<Longrightarrow> _") |
|
189 proof |
|
190 assume "?P \<Longrightarrow> False" ?P |
|
191 thus False . |
|
192 qed |
|
193 |
|
194 (* Even better: can state assumptions directly *) |
|
195 |
|
196 lemma assumes A: "large_formula \<Longrightarrow> False" |
|
197 shows "~ large_formula" (is "~ ?P") |
|
198 proof |
|
199 assume ?P |
|
200 from A show False . |
|
201 qed; |
|
202 |
|
203 |
|
204 (* Predicate calculus. Keyword fix introduces new local variables into a |
|
205 proof. Corresponds to !! just like assume-show corresponds to \<Longrightarrow> *) |
|
206 |
|
207 lemma assumes P: "!x. P x" shows "!x. P(f x)" |
|
208 proof --"allI" |
|
209 fix x |
|
210 from P show "P(f x)" .. --"allE" |
|
211 qed |
|
212 |
|
213 lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" |
|
214 proof - |
|
215 from Pf show ?thesis |
|
216 proof --"exE" |
|
217 fix a |
|
218 assume "P(f a)" |
|
219 show ?thesis .. --"exI" |
|
220 qed |
|
221 qed |
|
222 |
|
223 text {* |
|
224 Explicit $\exists$-elimination as seen above can become quite |
|
225 cumbersome in practice. The derived Isar language element |
|
226 ``\isakeyword{obtain}'' provides a more handsome way to do |
|
227 generalized existence reasoning. |
|
228 *} |
|
229 |
|
230 lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" |
|
231 proof - |
|
232 from Pf obtain a where "P (f a)" .. --"exE" |
|
233 thus "EX y. P y" .. --"exI" |
|
234 qed |
|
235 |
|
236 text {* |
|
237 Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and |
|
238 \isakeyword{assume} together with a soundness proof of the |
|
239 elimination involved. Thus it behaves similar to any other forward |
|
240 proof element. Also note that due to the nature of general existence |
|
241 reasoning involved here, any result exported from the context of an |
|
242 \isakeyword{obtain} statement may \emph{not} refer to the parameters |
|
243 introduced there. |
|
244 *} |
|
245 |
|
246 lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" |
|
247 proof --"allI" |
|
248 fix y |
|
249 from ex obtain x where "ALL y. P x y" .. --"exE" |
|
250 from this have "P x y" .. --"allE" |
|
251 thus "EX x. P x y" .. --"exI" |
|
252 qed |
|
253 |
|
254 (* some example with blast, if . and .. fail *) |
|
255 |
|
256 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
|
257 proof |
|
258 let ?S = "{x. x ~: f x}" |
|
259 show "?S ~: range f" |
|
260 proof |
|
261 assume "?S : range f" |
|
262 then obtain y where fy: "?S = f y" .. |
|
263 show False |
|
264 proof (cases) |
|
265 assume "y : ?S" |
|
266 with fy show False by blast |
|
267 next |
|
268 assume "y ~: ?S" |
|
269 with fy show False by blast |
|
270 qed |
|
271 qed |
|
272 qed |
|
273 |
|
274 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
|
275 proof |
|
276 let ?S = "{x. x ~: f x}" |
|
277 show "?S ~: range f" |
|
278 proof |
|
279 assume "?S : range f" |
|
280 then obtain y where eq: "?S = f y" .. |
|
281 show False |
|
282 proof (cases) |
|
283 assume A: "y : ?S" |
|
284 hence isin: "y : f y" by(simp add:eq) |
|
285 from A have "y ~: f y" by simp |
|
286 with isin show False by contradiction |
|
287 next |
|
288 assume A: "y ~: ?S" |
|
289 hence notin: "y ~: f y" by(simp add:eq) |
|
290 from A have "y : f y" by simp |
|
291 with notin show False by contradiction |
|
292 qed |
|
293 qed |
|
294 qed |
|
295 |
|
296 text {* |
|
297 How much creativity is required? As it happens, Isabelle can prove |
|
298 this theorem automatically using best-first search. Depth-first |
|
299 search would diverge, but best-first search successfully navigates |
|
300 through the large search space. The context of Isabelle's classical |
|
301 prover contains rules for the relevant constructs of HOL's set |
|
302 theory. |
|
303 *} |
|
304 |
|
305 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
|
306 by best |
|
307 |
|
308 (* Finally, whole scripts may appear in the leaves of the proof tree, |
|
309 although this is best avoided. Here is a contrived example. *) |
|
310 |
|
311 lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B" |
|
312 proof |
|
313 assume A: A |
|
314 show "(A \<longrightarrow>B) \<longrightarrow> B" |
|
315 apply(rule impI) |
|
316 apply(erule impE) |
|
317 apply(rule A) |
|
318 apply assumption |
|
319 done |
|
320 qed |
|
321 |
|
322 |
|
323 (* You may need to resort to this technique if an automatic step fails to |
|
324 prove the desired proposition. *) |
|
325 |
|
326 end |
|