summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Basic_Logic.thy

changeset 33026 | 8f35633c4922 |

parent 31758 | 3edd5f813f01 |

child 37671 | fa53d267dab3 |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Isar_Examples/Basic_Logic.thy Tue Oct 20 19:37:09 2009 +0200 1.3 @@ -0,0 +1,448 @@ 1.4 +(* Title: HOL/Isar_Examples/Basic_Logic.thy 1.5 + Author: Markus Wenzel, TU Muenchen 1.6 + 1.7 +Basic propositional and quantifier reasoning. 1.8 +*) 1.9 + 1.10 +header {* Basic logical reasoning *} 1.11 + 1.12 +theory Basic_Logic 1.13 +imports Main 1.14 +begin 1.15 + 1.16 + 1.17 +subsection {* Pure backward reasoning *} 1.18 + 1.19 +text {* 1.20 + In order to get a first idea of how Isabelle/Isar proof documents 1.21 + may look like, we consider the propositions @{text I}, @{text K}, 1.22 + and @{text S}. The following (rather explicit) proofs should 1.23 + require little extra explanations. 1.24 +*} 1.25 + 1.26 +lemma I: "A --> A" 1.27 +proof 1.28 + assume A 1.29 + show A by fact 1.30 +qed 1.31 + 1.32 +lemma K: "A --> B --> A" 1.33 +proof 1.34 + assume A 1.35 + show "B --> A" 1.36 + proof 1.37 + show A by fact 1.38 + qed 1.39 +qed 1.40 + 1.41 +lemma S: "(A --> B --> C) --> (A --> B) --> A --> C" 1.42 +proof 1.43 + assume "A --> B --> C" 1.44 + show "(A --> B) --> A --> C" 1.45 + proof 1.46 + assume "A --> B" 1.47 + show "A --> C" 1.48 + proof 1.49 + assume A 1.50 + show C 1.51 + proof (rule mp) 1.52 + show "B --> C" by (rule mp) fact+ 1.53 + show B by (rule mp) fact+ 1.54 + qed 1.55 + qed 1.56 + qed 1.57 +qed 1.58 + 1.59 +text {* 1.60 + Isar provides several ways to fine-tune the reasoning, avoiding 1.61 + excessive detail. Several abbreviated language elements are 1.62 + available, enabling the writer to express proofs in a more concise 1.63 + way, even without referring to any automated proof tools yet. 1.64 + 1.65 + First of all, proof by assumption may be abbreviated as a single 1.66 + dot. 1.67 +*} 1.68 + 1.69 +lemma "A --> A" 1.70 +proof 1.71 + assume A 1.72 + show A by fact+ 1.73 +qed 1.74 + 1.75 +text {* 1.76 + In fact, concluding any (sub-)proof already involves solving any 1.77 + remaining goals by assumption\footnote{This is not a completely 1.78 + trivial operation, as proof by assumption may involve full 1.79 + higher-order unification.}. Thus we may skip the rather vacuous 1.80 + body of the above proof as well. 1.81 +*} 1.82 + 1.83 +lemma "A --> A" 1.84 +proof 1.85 +qed 1.86 + 1.87 +text {* 1.88 + Note that the \isacommand{proof} command refers to the @{text rule} 1.89 + method (without arguments) by default. Thus it implicitly applies a 1.90 + single rule, as determined from the syntactic form of the statements 1.91 + involved. The \isacommand{by} command abbreviates any proof with 1.92 + empty body, so the proof may be further pruned. 1.93 +*} 1.94 + 1.95 +lemma "A --> A" 1.96 + by rule 1.97 + 1.98 +text {* 1.99 + Proof by a single rule may be abbreviated as double-dot. 1.100 +*} 1.101 + 1.102 +lemma "A --> A" .. 1.103 + 1.104 +text {* 1.105 + Thus we have arrived at an adequate representation of the proof of a 1.106 + tautology that holds by a single standard rule.\footnote{Apparently, 1.107 + the rule here is implication introduction.} 1.108 +*} 1.109 + 1.110 +text {* 1.111 + Let us also reconsider @{text K}. Its statement is composed of 1.112 + iterated connectives. Basic decomposition is by a single rule at a 1.113 + time, which is why our first version above was by nesting two 1.114 + proofs. 1.115 + 1.116 + The @{text intro} proof method repeatedly decomposes a goal's 1.117 + conclusion.\footnote{The dual method is @{text elim}, acting on a 1.118 + goal's premises.} 1.119 +*} 1.120 + 1.121 +lemma "A --> B --> A" 1.122 +proof (intro impI) 1.123 + assume A 1.124 + show A by fact 1.125 +qed 1.126 + 1.127 +text {* 1.128 + Again, the body may be collapsed. 1.129 +*} 1.130 + 1.131 +lemma "A --> B --> A" 1.132 + by (intro impI) 1.133 + 1.134 +text {* 1.135 + Just like @{text rule}, the @{text intro} and @{text elim} proof 1.136 + methods pick standard structural rules, in case no explicit 1.137 + arguments are given. While implicit rules are usually just fine for 1.138 + single rule application, this may go too far with iteration. Thus 1.139 + in practice, @{text intro} and @{text elim} would be typically 1.140 + restricted to certain structures by giving a few rules only, e.g.\ 1.141 + \isacommand{proof}~@{text "(intro impI allI)"} to strip implications 1.142 + and universal quantifiers. 1.143 + 1.144 + Such well-tuned iterated decomposition of certain structures is the 1.145 + prime application of @{text intro} and @{text elim}. In contrast, 1.146 + terminal steps that solve a goal completely are usually performed by 1.147 + actual automated proof methods (such as \isacommand{by}~@{text 1.148 + blast}. 1.149 +*} 1.150 + 1.151 + 1.152 +subsection {* Variations of backward vs.\ forward reasoning *} 1.153 + 1.154 +text {* 1.155 + Certainly, any proof may be performed in backward-style only. On 1.156 + the other hand, small steps of reasoning are often more naturally 1.157 + expressed in forward-style. Isar supports both backward and forward 1.158 + reasoning as a first-class concept. In order to demonstrate the 1.159 + difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}. 1.160 + 1.161 + The first version is purely backward. 1.162 +*} 1.163 + 1.164 +lemma "A & B --> B & A" 1.165 +proof 1.166 + assume "A & B" 1.167 + show "B & A" 1.168 + proof 1.169 + show B by (rule conjunct2) fact 1.170 + show A by (rule conjunct1) fact 1.171 + qed 1.172 +qed 1.173 + 1.174 +text {* 1.175 + Above, the @{text "conjunct_1/2"} projection rules had to be named 1.176 + explicitly, since the goals @{text B} and @{text A} did not provide 1.177 + any structural clue. This may be avoided using \isacommand{from} to 1.178 + focus on the @{text "A \<and> B"} assumption as the current facts, 1.179 + enabling the use of double-dot proofs. Note that \isacommand{from} 1.180 + already does forward-chaining, involving the \name{conjE} rule here. 1.181 +*} 1.182 + 1.183 +lemma "A & B --> B & A" 1.184 +proof 1.185 + assume "A & B" 1.186 + show "B & A" 1.187 + proof 1.188 + from `A & B` show B .. 1.189 + from `A & B` show A .. 1.190 + qed 1.191 +qed 1.192 + 1.193 +text {* 1.194 + In the next version, we move the forward step one level upwards. 1.195 + Forward-chaining from the most recent facts is indicated by the 1.196 + \isacommand{then} command. Thus the proof of @{text "B \<and> A"} from 1.197 + @{text "A \<and> B"} actually becomes an elimination, rather than an 1.198 + introduction. The resulting proof structure directly corresponds to 1.199 + that of the @{text conjE} rule, including the repeated goal 1.200 + proposition that is abbreviated as @{text ?thesis} below. 1.201 +*} 1.202 + 1.203 +lemma "A & B --> B & A" 1.204 +proof 1.205 + assume "A & B" 1.206 + then show "B & A" 1.207 + proof -- {* rule @{text conjE} of @{text "A \<and> B"} *} 1.208 + assume B A 1.209 + then show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *} 1.210 + qed 1.211 +qed 1.212 + 1.213 +text {* 1.214 + In the subsequent version we flatten the structure of the main body 1.215 + by doing forward reasoning all the time. Only the outermost 1.216 + decomposition step is left as backward. 1.217 +*} 1.218 + 1.219 +lemma "A & B --> B & A" 1.220 +proof 1.221 + assume "A & B" 1.222 + from `A & B` have A .. 1.223 + from `A & B` have B .. 1.224 + from `B` `A` show "B & A" .. 1.225 +qed 1.226 + 1.227 +text {* 1.228 + We can still push forward-reasoning a bit further, even at the risk 1.229 + of getting ridiculous. Note that we force the initial proof step to 1.230 + do nothing here, by referring to the ``-'' proof method. 1.231 +*} 1.232 + 1.233 +lemma "A & B --> B & A" 1.234 +proof - 1.235 + { 1.236 + assume "A & B" 1.237 + from `A & B` have A .. 1.238 + from `A & B` have B .. 1.239 + from `B` `A` have "B & A" .. 1.240 + } 1.241 + then show ?thesis .. -- {* rule \name{impI} *} 1.242 +qed 1.243 + 1.244 +text {* 1.245 + \medskip With these examples we have shifted through a whole range 1.246 + from purely backward to purely forward reasoning. Apparently, in 1.247 + the extreme ends we get slightly ill-structured proofs, which also 1.248 + require much explicit naming of either rules (backward) or local 1.249 + facts (forward). 1.250 + 1.251 + The general lesson learned here is that good proof style would 1.252 + achieve just the \emph{right} balance of top-down backward 1.253 + decomposition, and bottom-up forward composition. In general, there 1.254 + is no single best way to arrange some pieces of formal reasoning, of 1.255 + course. Depending on the actual applications, the intended audience 1.256 + etc., rules (and methods) on the one hand vs.\ facts on the other 1.257 + hand have to be emphasized in an appropriate way. This requires the 1.258 + proof writer to develop good taste, and some practice, of course. 1.259 +*} 1.260 + 1.261 +text {* 1.262 + For our example the most appropriate way of reasoning is probably 1.263 + the middle one, with conjunction introduction done after 1.264 + elimination. 1.265 +*} 1.266 + 1.267 +lemma "A & B --> B & A" 1.268 +proof 1.269 + assume "A & B" 1.270 + then show "B & A" 1.271 + proof 1.272 + assume B A 1.273 + then show ?thesis .. 1.274 + qed 1.275 +qed 1.276 + 1.277 + 1.278 + 1.279 +subsection {* A few examples from ``Introduction to Isabelle'' *} 1.280 + 1.281 +text {* 1.282 + We rephrase some of the basic reasoning examples of 1.283 + \cite{isabelle-intro}, using HOL rather than FOL. 1.284 +*} 1.285 + 1.286 +subsubsection {* A propositional proof *} 1.287 + 1.288 +text {* 1.289 + We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof below 1.290 + involves forward-chaining from @{text "P \<or> P"}, followed by an 1.291 + explicit case-analysis on the two \emph{identical} cases. 1.292 +*} 1.293 + 1.294 +lemma "P | P --> P" 1.295 +proof 1.296 + assume "P | P" 1.297 + then show P 1.298 + proof -- {* 1.299 + rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} 1.300 + *} 1.301 + assume P show P by fact 1.302 + next 1.303 + assume P show P by fact 1.304 + qed 1.305 +qed 1.306 + 1.307 +text {* 1.308 + Case splits are \emph{not} hardwired into the Isar language as a 1.309 + special feature. The \isacommand{next} command used to separate the 1.310 + cases above is just a short form of managing block structure. 1.311 + 1.312 + \medskip In general, applying proof methods may split up a goal into 1.313 + separate ``cases'', i.e.\ new subgoals with individual local 1.314 + assumptions. The corresponding proof text typically mimics this by 1.315 + establishing results in appropriate contexts, separated by blocks. 1.316 + 1.317 + In order to avoid too much explicit parentheses, the Isar system 1.318 + implicitly opens an additional block for any new goal, the 1.319 + \isacommand{next} statement then closes one block level, opening a 1.320 + new one. The resulting behavior is what one would expect from 1.321 + separating cases, only that it is more flexible. E.g.\ an induction 1.322 + base case (which does not introduce local assumptions) would 1.323 + \emph{not} require \isacommand{next} to separate the subsequent step 1.324 + case. 1.325 + 1.326 + \medskip In our example the situation is even simpler, since the two 1.327 + cases actually coincide. Consequently the proof may be rephrased as 1.328 + follows. 1.329 +*} 1.330 + 1.331 +lemma "P | P --> P" 1.332 +proof 1.333 + assume "P | P" 1.334 + then show P 1.335 + proof 1.336 + assume P 1.337 + show P by fact 1.338 + show P by fact 1.339 + qed 1.340 +qed 1.341 + 1.342 +text {* 1.343 + Again, the rather vacuous body of the proof may be collapsed. Thus 1.344 + the case analysis degenerates into two assumption steps, which are 1.345 + implicitly performed when concluding the single rule step of the 1.346 + double-dot proof as follows. 1.347 +*} 1.348 + 1.349 +lemma "P | P --> P" 1.350 +proof 1.351 + assume "P | P" 1.352 + then show P .. 1.353 +qed 1.354 + 1.355 + 1.356 +subsubsection {* A quantifier proof *} 1.357 + 1.358 +text {* 1.359 + To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f 1.360 + x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any @{text a} 1.361 + with @{text "P (f a)"} may be taken as a witness for the second 1.362 + existential statement. 1.363 + 1.364 + The first proof is rather verbose, exhibiting quite a lot of 1.365 + (redundant) detail. It gives explicit rules, even with some 1.366 + instantiation. Furthermore, we encounter two new language elements: 1.367 + the \isacommand{fix} command augments the context by some new 1.368 + ``arbitrary, but fixed'' element; the \isacommand{is} annotation 1.369 + binds term abbreviations by higher-order pattern matching. 1.370 +*} 1.371 + 1.372 +lemma "(EX x. P (f x)) --> (EX y. P y)" 1.373 +proof 1.374 + assume "EX x. P (f x)" 1.375 + then show "EX y. P y" 1.376 + proof (rule exE) -- {* 1.377 + rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$} 1.378 + *} 1.379 + fix a 1.380 + assume "P (f a)" (is "P ?witness") 1.381 + then show ?thesis by (rule exI [of P ?witness]) 1.382 + qed 1.383 +qed 1.384 + 1.385 +text {* 1.386 + While explicit rule instantiation may occasionally improve 1.387 + readability of certain aspects of reasoning, it is usually quite 1.388 + redundant. Above, the basic proof outline gives already enough 1.389 + structural clues for the system to infer both the rules and their 1.390 + instances (by higher-order unification). Thus we may as well prune 1.391 + the text as follows. 1.392 +*} 1.393 + 1.394 +lemma "(EX x. P (f x)) --> (EX y. P y)" 1.395 +proof 1.396 + assume "EX x. P (f x)" 1.397 + then show "EX y. P y" 1.398 + proof 1.399 + fix a 1.400 + assume "P (f a)" 1.401 + then show ?thesis .. 1.402 + qed 1.403 +qed 1.404 + 1.405 +text {* 1.406 + Explicit @{text \<exists>}-elimination as seen above can become quite 1.407 + cumbersome in practice. The derived Isar language element 1.408 + ``\isakeyword{obtain}'' provides a more handsome way to do 1.409 + generalized existence reasoning. 1.410 +*} 1.411 + 1.412 +lemma "(EX x. P (f x)) --> (EX y. P y)" 1.413 +proof 1.414 + assume "EX x. P (f x)" 1.415 + then obtain a where "P (f a)" .. 1.416 + then show "EX y. P y" .. 1.417 +qed 1.418 + 1.419 +text {* 1.420 + Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and 1.421 + \isakeyword{assume} together with a soundness proof of the 1.422 + elimination involved. Thus it behaves similar to any other forward 1.423 + proof element. Also note that due to the nature of general 1.424 + existence reasoning involved here, any result exported from the 1.425 + context of an \isakeyword{obtain} statement may \emph{not} refer to 1.426 + the parameters introduced there. 1.427 +*} 1.428 + 1.429 + 1.430 + 1.431 +subsubsection {* Deriving rules in Isabelle *} 1.432 + 1.433 +text {* 1.434 + We derive the conjunction elimination rule from the corresponding 1.435 + projections. The proof is quite straight-forward, since 1.436 + Isabelle/Isar supports non-atomic goals and assumptions fully 1.437 + transparently. 1.438 +*} 1.439 + 1.440 +theorem conjE: "A & B ==> (A ==> B ==> C) ==> C" 1.441 +proof - 1.442 + assume "A & B" 1.443 + assume r: "A ==> B ==> C" 1.444 + show C 1.445 + proof (rule r) 1.446 + show A by (rule conjunct1) fact 1.447 + show B by (rule conjunct2) fact 1.448 + qed 1.449 +qed 1.450 + 1.451 +end