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