author wenzelm Thu Jul 01 18:31:46 2010 +0200 (2010-07-01) changeset 37671 fa53d267dab3 parent 37670 0ce594837524 child 37672 645eb9fec794
misc tuning and modernization;
 src/HOL/Isar_Examples/Basic_Logic.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Cantor.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Drinker.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Expr_Compiler.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Fibonacci.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Group.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare_Ex.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Knaster_Tarski.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Mutilated_Checkerboard.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Nested_Datatype.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Peirce.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Puzzle.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Summation.thy file | annotate | diff | revisions
     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 -

     2.1 --- a/src/HOL/Isar_Examples/Cantor.thy	Thu Jul 01 14:32:57 2010 +0200
2.2 +++ b/src/HOL/Isar_Examples/Cantor.thy	Thu Jul 01 18:31:46 2010 +0200
2.3 @@ -8,14 +8,11 @@
2.4  imports Main
2.5  begin
2.6
2.7 -text_raw {*
2.8 -  \footnote{This is an Isar version of the final example of the
2.9 -  Isabelle/HOL manual \cite{isabelle-HOL}.}
2.10 -*}
2.11 +text_raw {* \footnote{This is an Isar version of the final example of
2.12 +  the Isabelle/HOL manual \cite{isabelle-HOL}.}  *}
2.13
2.14 -text {*
2.15 -  Cantor's Theorem states that every set has more subsets than it has
2.16 -  elements.  It has become a favorite basic example in pure
2.17 +text {* Cantor's Theorem states that every set has more subsets than
2.18 +  it has elements.  It has become a favorite basic example in pure
2.19    higher-order logic since it is so easily expressed: $\all{f::\alpha 2.20 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} 2.21 \all{x::\alpha} f \ap x \not= S$
2.22 @@ -25,8 +22,7 @@
2.23    every function from $\alpha$ to its powerset, some subset is outside
2.24    its range.  The Isabelle/Isar proofs below uses HOL's set theory,
2.25    with the type $\alpha \ap \idt{set}$ and the operator
2.26 -  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
2.27 -*}
2.28 +  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
2.29
2.30  theorem "EX S. S ~: range (f :: 'a => 'a set)"
2.31  proof
2.32 @@ -48,24 +44,20 @@
2.33    qed
2.34  qed
2.35
2.36 -text {*
2.37 -  How much creativity is required?  As it happens, Isabelle can prove
2.38 -  this theorem automatically using best-first search.  Depth-first
2.39 -  search would diverge, but best-first search successfully navigates
2.40 -  through the large search space.  The context of Isabelle's classical
2.41 -  prover contains rules for the relevant constructs of HOL's set
2.42 -  theory.
2.43 -*}
2.44 +text {* How much creativity is required?  As it happens, Isabelle can
2.45 +  prove this theorem automatically using best-first search.
2.46 +  Depth-first search would diverge, but best-first search successfully
2.47 +  navigates through the large search space.  The context of Isabelle's
2.48 +  classical prover contains rules for the relevant constructs of HOL's
2.49 +  set theory.  *}
2.50
2.51  theorem "EX S. S ~: range (f :: 'a => 'a set)"
2.52    by best
2.53
2.54 -text {*
2.55 -  While this establishes the same theorem internally, we do not get
2.56 -  any idea of how the proof actually works.  There is currently no way
2.57 -  to transform internal system-level representations of Isabelle
2.58 +text {* While this establishes the same theorem internally, we do not
2.59 +  get any idea of how the proof actually works.  There is currently no
2.60 +  way to transform internal system-level representations of Isabelle
2.61    proofs back into Isar text.  Writing intelligible proof documents
2.62 -  really is a creative process, after all.
2.63 -*}
2.64 +  really is a creative process, after all. *}
2.65
2.66  end

     3.1 --- a/src/HOL/Isar_Examples/Drinker.thy	Thu Jul 01 14:32:57 2010 +0200
3.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Thu Jul 01 18:31:46 2010 +0200
3.3 @@ -8,24 +8,21 @@
3.4  imports Main
3.5  begin
3.6
3.7 -text {*
3.8 -  Here is another example of classical reasoning: the Drinker's
3.9 +text {* Here is another example of classical reasoning: the Drinker's
3.10    Principle says that for some person, if he is drunk, everybody else
3.11    is drunk!
3.12
3.13 -  We first prove a classical part of de-Morgan's law.
3.14 -*}
3.15 +  We first prove a classical part of de-Morgan's law. *}
3.16
3.17 -lemma deMorgan:
3.18 +lemma de_Morgan:
3.19    assumes "\<not> (\<forall>x. P x)"
3.20    shows "\<exists>x. \<not> P x"
3.21 -  using prems
3.22 +  using assms
3.23  proof (rule contrapos_np)
3.24    assume a: "\<not> (\<exists>x. \<not> P x)"
3.25    show "\<forall>x. P x"
3.26    proof
3.27 -    fix x
3.28 -    show "P x"
3.29 +    fix x show "P x"
3.30      proof (rule classical)
3.31        assume "\<not> P x"
3.32        then have "\<exists>x. \<not> P x" ..
3.33 @@ -41,12 +38,12 @@
3.34    then show ?thesis ..
3.35  next
3.36    assume "\<not> (\<forall>x. drunk x)"
3.37 -  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
3.38 +  then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
3.39    then obtain a where a: "\<not> drunk a" ..
3.40    have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
3.41    proof
3.42      assume "drunk a"
3.43 -    with a show "\<forall>x. drunk x" by (contradiction)
3.44 +    with a show "\<forall>x. drunk x" by contradiction
3.45    qed
3.46    then show ?thesis ..
3.47  qed

     4.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Jul 01 14:32:57 2010 +0200
4.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Jul 01 18:31:46 2010 +0200
4.3 @@ -10,20 +10,17 @@
4.4  imports Main
4.5  begin
4.6
4.7 -text {*
4.8 - This is a (rather trivial) example of program verification.  We model
4.9 - a compiler for translating expressions to stack machine instructions,
4.10 - and prove its correctness wrt.\ some evaluation semantics.
4.11 -*}
4.12 +text {* This is a (rather trivial) example of program verification.
4.13 +  We model a compiler for translating expressions to stack machine
4.14 +  instructions, and prove its correctness wrt.\ some evaluation
4.15 +  semantics. *}
4.16
4.17
4.18  subsection {* Binary operations *}
4.19
4.20 -text {*
4.21 - Binary operations are just functions over some type of values.  This
4.22 - is both for abstract syntax and semantics, i.e.\ we use a shallow
4.23 - embedding'' here.
4.24 -*}
4.25 +text {* Binary operations are just functions over some type of values.
4.26 +  This is both for abstract syntax and semantics, i.e.\ we use a
4.27 +  shallow embedding'' here. *}
4.28
4.29  types
4.30    'val binop = "'val => 'val => 'val"
4.31 @@ -31,85 +28,71 @@
4.32
4.33  subsection {* Expressions *}
4.34
4.35 -text {*
4.36 - The language of expressions is defined as an inductive type,
4.37 - consisting of variables, constants, and binary operations on
4.38 - expressions.
4.39 -*}
4.40 +text {* The language of expressions is defined as an inductive type,
4.41 +  consisting of variables, constants, and binary operations on
4.42 +  expressions. *}
4.43
4.44  datatype ('adr, 'val) expr =
4.46 -  Constant 'val |
4.49 +  | Constant 'val
4.50 +  | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
4.51
4.52 -text {*
4.53 - Evaluation (wrt.\ some environment of variable assignments) is
4.54 - defined by primitive recursion over the structure of expressions.
4.55 -*}
4.56 +text {* Evaluation (wrt.\ some environment of variable assignments) is
4.57 +  defined by primitive recursion over the structure of expressions. *}
4.58
4.59 -consts
4.60 -  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
4.61 -
4.62 -primrec
4.63 +primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
4.64 +where
4.65    "eval (Variable x) env = env x"
4.66 -  "eval (Constant c) env = c"
4.67 -  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
4.68 +| "eval (Constant c) env = c"
4.69 +| "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
4.70
4.71
4.72  subsection {* Machine *}
4.73
4.74 -text {*
4.75 - Next we model a simple stack machine, with three instructions.
4.76 -*}
4.77 +text {* Next we model a simple stack machine, with three
4.78 +  instructions. *}
4.79
4.80  datatype ('adr, 'val) instr =
4.81 -  Const 'val |
4.83 -  Apply "'val binop"
4.84 +    Const 'val
4.86 +  | Apply "'val binop"
4.87
4.88 -text {*
4.89 - Execution of a list of stack machine instructions is easily defined
4.90 - as follows.
4.91 -*}
4.92 +text {* Execution of a list of stack machine instructions is easily
4.93 +  defined as follows. *}
4.94
4.95 -consts
4.96 +primrec
4.97    exec :: "(('adr, 'val) instr) list
4.98      => 'val list => ('adr => 'val) => 'val list"
4.99 -
4.100 -primrec
4.101 +where
4.102    "exec [] stack env = stack"
4.103 -  "exec (instr # instrs) stack env =
4.104 +| "exec (instr # instrs) stack env =
4.105      (case instr of
4.106        Const c => exec instrs (c # stack) env
4.107      | Load x => exec instrs (env x # stack) env
4.108      | Apply f => exec instrs (f (hd stack) (hd (tl stack))
4.109                     # (tl (tl stack))) env)"
4.110
4.111 -definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" where
4.112 -  "execute instrs env == hd (exec instrs [] env)"
4.113 +definition
4.114 +  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
4.115 +  where "execute instrs env = hd (exec instrs [] env)"
4.116
4.117
4.118  subsection {* Compiler *}
4.119
4.120 -text {*
4.121 - We are ready to define the compilation function of expressions to
4.122 - lists of stack machine instructions.
4.123 -*}
4.124 -
4.125 -consts
4.126 -  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
4.127 +text {* We are ready to define the compilation function of expressions
4.128 +  to lists of stack machine instructions. *}
4.129
4.130  primrec
4.131 +  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
4.132 +where
4.133    "compile (Variable x) = [Load x]"
4.134 -  "compile (Constant c) = [Const c]"
4.135 -  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
4.136 +| "compile (Constant c) = [Const c]"
4.137 +| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
4.138
4.139
4.140 -text {*
4.141 - The main result of this development is the correctness theorem for
4.142 - $\idt{compile}$.  We first establish a lemma about $\idt{exec}$ and
4.143 - list append.
4.144 -*}
4.145 +text {* The main result of this development is the correctness theorem
4.146 +  for @{text compile}.  We first establish a lemma about @{text exec}
4.147 +  and list append. *}
4.148
4.149  lemma exec_append:
4.150    "exec (xs @ ys) stack env =
4.151 @@ -146,13 +129,11 @@
4.152  qed
4.153
4.154
4.155 -text {*
4.156 - \bigskip In the proofs above, the \name{simp} method does quite a lot
4.157 - of work behind the scenes (mostly functional program execution'').
4.158 - Subsequently, the same reasoning is elaborated in detail --- at most
4.159 - one recursive function definition is used at a time.  Thus we get a
4.160 - better idea of what is actually going on.
4.161 -*}
4.162 +text {* \bigskip In the proofs above, the @{text simp} method does
4.163 +  quite a lot of work behind the scenes (mostly functional program
4.164 +  execution'').  Subsequently, the same reasoning is elaborated in
4.165 +  detail --- at most one recursive function definition is used at a
4.166 +  time.  Thus we get a better idea of what is actually going on. *}
4.167
4.168  lemma exec_append':
4.169    "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
4.170 @@ -221,8 +202,7 @@
4.171
4.172    have "execute (compile e) env = hd (exec (compile e) [] env)"
4.174 -  also from exec_compile
4.175 -    have "exec (compile e) [] env = [eval e env]" .
4.176 +  also from exec_compile have "exec (compile e) [] env = [eval e env]" .
4.177    also have "hd ... = eval e env" by simp
4.178    finally show ?thesis .
4.179  qed

     5.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy	Thu Jul 01 14:32:57 2010 +0200
5.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy	Thu Jul 01 18:31:46 2010 +0200
5.3 @@ -15,22 +15,20 @@
5.4  header {* Fib and Gcd commute *}
5.5
5.6  theory Fibonacci
5.7 -imports Primes
5.8 +imports "../Old_Number_Theory/Primes"
5.9  begin
5.10
5.11 -text_raw {*
5.12 - \footnote{Isar version by Gertrud Bauer.  Original tactic script by
5.13 - Larry Paulson.  A few proofs of laws taken from
5.14 - \cite{Concrete-Math}.}
5.15 -*}
5.16 +text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
5.17 +  script by Larry Paulson.  A few proofs of laws taken from
5.18 +  \cite{Concrete-Math}.} *}
5.19
5.20
5.21  subsection {* Fibonacci numbers *}
5.22
5.23  fun fib :: "nat \<Rightarrow> nat" where
5.24    "fib 0 = 0"
5.25 -  | "fib (Suc 0) = 1"
5.26 -  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
5.27 +| "fib (Suc 0) = 1"
5.28 +| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
5.29
5.30  lemma [simp]: "0 < fib (Suc n)"
5.31    by (induct n rule: fib.induct) simp_all
5.32 @@ -102,7 +100,7 @@
5.33    then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
5.35    also have "fib (n + k + 1)
5.36 -    = fib (k + 1) * fib (n + 1) + fib k * fib n"
5.37 +      = fib (k + 1) * fib (n + 1) + fib k * fib n"
5.39    also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
5.41 @@ -139,18 +137,17 @@
5.42        case False then have "m <= n" by simp
5.43        from 0 < m and False have "n - m < n" by simp
5.44        with hyp have "gcd (fib m) (fib ((n - m) mod m))
5.45 -        = gcd (fib m) (fib (n - m))" by simp
5.46 +          = gcd (fib m) (fib (n - m))" by simp
5.47        also have "... = gcd (fib m) (fib n)"
5.48          using m <= n by (rule gcd_fib_diff)
5.49        finally have "gcd (fib m) (fib ((n - m) mod m)) =
5.50 -        gcd (fib m) (fib n)" .
5.51 +          gcd (fib m) (fib n)" .
5.52        with False show ?thesis by simp
5.53      qed
5.54      finally show ?thesis .
5.55    qed
5.56  qed
5.57
5.58 -
5.59  theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
5.60  proof (induct m n rule: gcd_induct)
5.61    fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp

     6.1 --- a/src/HOL/Isar_Examples/Group.thy	Thu Jul 01 14:32:57 2010 +0200
6.2 +++ b/src/HOL/Isar_Examples/Group.thy	Thu Jul 01 18:31:46 2010 +0200
6.3 @@ -10,92 +10,83 @@
6.4
6.5  subsection {* Groups and calculational reasoning *}
6.6
6.7 -text {*
6.8 - Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, 6.9 - \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
6.10 - as an axiomatic type class as follows.  Note that the parent class
6.11 - $\idt{times}$ is provided by the basic HOL theory.
6.12 -*}
6.13 -
6.14 -notation Groups.one ("one")
6.15 +text {* Groups over signature $({\times} :: \alpha \To \alpha \To 6.16 + \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$
6.17 +  are defined as an axiomatic type class as follows.  Note that the
6.18 +  parent class $\idt{times}$ is provided by the basic HOL theory. *}
6.19
6.20  class group = times + one + inverse +
6.21 -  assumes group_assoc:         "(x * y) * z = x * (y * z)"
6.22 -  assumes group_left_one:      "one * x = x"
6.23 -  assumes group_left_inverse:  "inverse x * x = one"
6.24 +  assumes group_assoc: "(x * y) * z = x * (y * z)"
6.25 +    and group_left_one: "1 * x = x"
6.26 +    and group_left_inverse: "inverse x * x = 1"
6.27
6.28 -text {*
6.29 - The group axioms only state the properties of left one and inverse,
6.30 - the right versions may be derived as follows.
6.31 -*}
6.32 +text {* The group axioms only state the properties of left one and
6.33 +  inverse, the right versions may be derived as follows. *}
6.34
6.35 -theorem group_right_inverse: "x * inverse x = (one::'a::group)"
6.36 +theorem (in group) group_right_inverse: "x * inverse x = 1"
6.37  proof -
6.38 -  have "x * inverse x = one * (x * inverse x)"
6.39 +  have "x * inverse x = 1 * (x * inverse x)"
6.40      by (simp only: group_left_one)
6.41 -  also have "... = one * x * inverse x"
6.42 +  also have "... = 1 * x * inverse x"
6.43      by (simp only: group_assoc)
6.44    also have "... = inverse (inverse x) * inverse x * x * inverse x"
6.45      by (simp only: group_left_inverse)
6.46    also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
6.47      by (simp only: group_assoc)
6.48 -  also have "... = inverse (inverse x) * one * inverse x"
6.49 +  also have "... = inverse (inverse x) * 1 * inverse x"
6.50      by (simp only: group_left_inverse)
6.51 -  also have "... = inverse (inverse x) * (one * inverse x)"
6.52 +  also have "... = inverse (inverse x) * (1 * inverse x)"
6.53      by (simp only: group_assoc)
6.54    also have "... = inverse (inverse x) * inverse x"
6.55      by (simp only: group_left_one)
6.56 -  also have "... = one"
6.57 +  also have "... = 1"
6.58      by (simp only: group_left_inverse)
6.59    finally show ?thesis .
6.60  qed
6.61
6.62 -text {*
6.63 - With \name{group-right-inverse} already available,
6.64 - \name{group-right-one}\label{thm:group-right-one} is now established
6.65 - much easier.
6.66 -*}
6.67 +text {* With \name{group-right-inverse} already available,
6.68 +  \name{group-right-one}\label{thm:group-right-one} is now established
6.69 +  much easier. *}
6.70
6.71 -theorem group_right_one: "x * one = (x::'a::group)"
6.72 +theorem (in group) group_right_one: "x * 1 = x"
6.73  proof -
6.74 -  have "x * one = x * (inverse x * x)"
6.75 +  have "x * 1 = x * (inverse x * x)"
6.76      by (simp only: group_left_inverse)
6.77    also have "... = x * inverse x * x"
6.78      by (simp only: group_assoc)
6.79 -  also have "... = one * x"
6.80 +  also have "... = 1 * x"
6.81      by (simp only: group_right_inverse)
6.82    also have "... = x"
6.83      by (simp only: group_left_one)
6.84    finally show ?thesis .
6.85  qed
6.86
6.87 -text {*
6.88 - \medskip The calculational proof style above follows typical
6.89 - presentations given in any introductory course on algebra.  The basic
6.90 - technique is to form a transitive chain of equations, which in turn
6.91 - are established by simplifying with appropriate rules.  The low-level
6.92 - logical details of equational reasoning are left implicit.
6.93 +text {* \medskip The calculational proof style above follows typical
6.94 +  presentations given in any introductory course on algebra.  The
6.95 +  basic technique is to form a transitive chain of equations, which in
6.96 +  turn are established by simplifying with appropriate rules.  The
6.97 +  low-level logical details of equational reasoning are left implicit.
6.98
6.99 - Note that $\dots$'' is just a special term variable that is bound
6.100 - automatically to the argument\footnote{The argument of a curried
6.101 - infix expression happens to be its right-hand side.} of the last fact
6.102 - achieved by any local assumption or proven statement.  In contrast to
6.103 - $\var{thesis}$, the $\dots$'' variable is bound \emph{after} the
6.104 - proof is finished, though.
6.105 +  Note that $\dots$'' is just a special term variable that is bound
6.106 +  automatically to the argument\footnote{The argument of a curried
6.107 +  infix expression happens to be its right-hand side.} of the last
6.108 +  fact achieved by any local assumption or proven statement.  In
6.109 +  contrast to $\var{thesis}$, the $\dots$'' variable is bound
6.110 +  \emph{after} the proof is finished, though.
6.111
6.112 - There are only two separate Isar language elements for calculational
6.113 - proofs: \isakeyword{also}'' for initial or intermediate
6.114 - calculational steps, and \isakeyword{finally}'' for exhibiting the
6.115 - result of a calculation.  These constructs are not hardwired into
6.116 - Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
6.117 - Expanding the \isakeyword{also} and \isakeyword{finally} derived
6.118 - language elements, calculations may be simulated by hand as
6.119 - demonstrated below.
6.120 +  There are only two separate Isar language elements for calculational
6.121 +  proofs: \isakeyword{also}'' for initial or intermediate
6.122 +  calculational steps, and \isakeyword{finally}'' for exhibiting the
6.123 +  result of a calculation.  These constructs are not hardwired into
6.124 +  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
6.125 +  Expanding the \isakeyword{also} and \isakeyword{finally} derived
6.126 +  language elements, calculations may be simulated by hand as
6.127 +  demonstrated below.
6.128  *}
6.129
6.130 -theorem "x * one = (x::'a::group)"
6.131 +theorem (in group) "x * 1 = x"
6.132  proof -
6.133 -  have "x * one = x * (inverse x * x)"
6.134 +  have "x * 1 = x * (inverse x * x)"
6.135      by (simp only: group_left_inverse)
6.136
6.137    note calculation = this
6.138 @@ -107,7 +98,7 @@
6.139    note calculation = trans [OF calculation this]
6.140      -- {* general calculational step: compose with transitivity rule *}
6.141
6.142 -  have "... = one * x"
6.143 +  have "... = 1 * x"
6.144      by (simp only: group_right_inverse)
6.145
6.146    note calculation = trans [OF calculation this]
6.147 @@ -124,129 +115,119 @@
6.148    show ?thesis .
6.149  qed
6.150
6.151 -text {*
6.152 - Note that this scheme of calculations is not restricted to plain
6.153 - transitivity.  Rules like anti-symmetry, or even forward and backward
6.154 - substitution work as well.  For the actual implementation of
6.155 - \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
6.156 - separate context information of transitivity'' rules.  Rule
6.157 - selection takes place automatically by higher-order unification.
6.158 -*}
6.159 +text {* Note that this scheme of calculations is not restricted to
6.160 +  plain transitivity.  Rules like anti-symmetry, or even forward and
6.161 +  backward substitution work as well.  For the actual implementation
6.162 +  of \isacommand{also} and \isacommand{finally}, Isabelle/Isar
6.163 +  maintains separate context information of transitivity'' rules.
6.164 +  Rule selection takes place automatically by higher-order
6.165 +  unification. *}
6.166
6.167
6.168  subsection {* Groups as monoids *}
6.169
6.170 -text {*
6.171 - Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, 6.172 - \idt{one} :: \alpha)$ are defined like this.
6.173 +text {* Monoids over signature $({\times} :: \alpha \To \alpha \To 6.174 + \alpha, \idt{one} :: \alpha)$ are defined like this.
6.175  *}
6.176
6.177  class monoid = times + one +
6.178 -  assumes monoid_assoc:       "(x * y) * z = x * (y * z)"
6.179 -  assumes monoid_left_one:   "one * x = x"
6.180 -  assumes monoid_right_one:  "x * one = x"
6.181 +  assumes monoid_assoc: "(x * y) * z = x * (y * z)"
6.182 +    and monoid_left_one: "1 * x = x"
6.183 +    and monoid_right_one: "x * 1 = x"
6.184
6.185 -text {*
6.186 - Groups are \emph{not} yet monoids directly from the definition.  For
6.187 - monoids, \name{right-one} had to be included as an axiom, but for
6.188 - groups both \name{right-one} and \name{right-inverse} are derivable
6.189 - from the other axioms.  With \name{group-right-one} derived as a
6.190 - theorem of group theory (see page~\pageref{thm:group-right-one}), we
6.191 - may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
6.192 - as follows.
6.193 -*}
6.194 +text {* Groups are \emph{not} yet monoids directly from the
6.195 +  definition.  For monoids, \name{right-one} had to be included as an
6.196 +  axiom, but for groups both \name{right-one} and \name{right-inverse}
6.197 +  are derivable from the other axioms.  With \name{group-right-one}
6.198 +  derived as a theorem of group theory (see
6.199 +  page~\pageref{thm:group-right-one}), we may still instantiate
6.200 +  $\idt{group} \subseteq \idt{monoid}$ properly as follows. *}
6.201
6.202  instance group < monoid
6.203 -  by (intro_classes,
6.204 -       rule group_assoc,
6.205 -       rule group_left_one,
6.206 -       rule group_right_one)
6.207 +  by intro_classes
6.208 +    (rule group_assoc,
6.209 +      rule group_left_one,
6.210 +      rule group_right_one)
6.211
6.212 -text {*
6.213 - The \isacommand{instance} command actually is a version of
6.214 - \isacommand{theorem}, setting up a goal that reflects the intended
6.215 - class relation (or type constructor arity).  Thus any Isar proof
6.216 - language element may be involved to establish this statement.  When
6.217 - concluding the proof, the result is transformed into the intended
6.218 - type signature extension behind the scenes.
6.219 -*}
6.220 +text {* The \isacommand{instance} command actually is a version of
6.221 +  \isacommand{theorem}, setting up a goal that reflects the intended
6.222 +  class relation (or type constructor arity).  Thus any Isar proof
6.223 +  language element may be involved to establish this statement.  When
6.224 +  concluding the proof, the result is transformed into the intended
6.225 +  type signature extension behind the scenes. *}
6.226 +
6.227
6.228  subsection {* More theorems of group theory *}
6.229
6.230 -text {*
6.231 - The one element is already uniquely determined by preserving an
6.232 - \emph{arbitrary} group element.
6.233 -*}
6.234 +text {* The one element is already uniquely determined by preserving
6.235 +  an \emph{arbitrary} group element. *}
6.236
6.237 -theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
6.238 +theorem (in group) group_one_equality:
6.239 +  assumes eq: "e * x = x"
6.240 +  shows "1 = e"
6.241  proof -
6.242 -  assume eq: "e * x = x"
6.243 -  have "one = x * inverse x"
6.244 +  have "1 = x * inverse x"
6.245      by (simp only: group_right_inverse)
6.246    also have "... = (e * x) * inverse x"
6.247      by (simp only: eq)
6.248    also have "... = e * (x * inverse x)"
6.249      by (simp only: group_assoc)
6.250 -  also have "... = e * one"
6.251 +  also have "... = e * 1"
6.252      by (simp only: group_right_inverse)
6.253    also have "... = e"
6.254      by (simp only: group_right_one)
6.255    finally show ?thesis .
6.256  qed
6.257
6.258 -text {*
6.259 - Likewise, the inverse is already determined by the cancel property.
6.260 -*}
6.261 +text {* Likewise, the inverse is already determined by the cancel property. *}
6.262
6.263 -theorem group_inverse_equality:
6.264 -  "x' * x = one ==> inverse x = (x'::'a::group)"
6.265 +theorem (in group) group_inverse_equality:
6.266 +  assumes eq: "x' * x = 1"
6.267 +  shows "inverse x = x'"
6.268  proof -
6.269 -  assume eq: "x' * x = one"
6.270 -  have "inverse x = one * inverse x"
6.271 +  have "inverse x = 1 * inverse x"
6.272      by (simp only: group_left_one)
6.273    also have "... = (x' * x) * inverse x"
6.274      by (simp only: eq)
6.275    also have "... = x' * (x * inverse x)"
6.276      by (simp only: group_assoc)
6.277 -  also have "... = x' * one"
6.278 +  also have "... = x' * 1"
6.279      by (simp only: group_right_inverse)
6.280    also have "... = x'"
6.281      by (simp only: group_right_one)
6.282    finally show ?thesis .
6.283  qed
6.284
6.285 -text {*
6.286 - The inverse operation has some further characteristic properties.
6.287 -*}
6.288 +text {* The inverse operation has some further characteristic properties. *}
6.289
6.290 -theorem group_inverse_times:
6.291 -  "inverse (x * y) = inverse y * inverse (x::'a::group)"
6.292 +theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
6.293  proof (rule group_inverse_equality)
6.294 -  show "(inverse y * inverse x) * (x * y) = one"
6.295 +  show "(inverse y * inverse x) * (x * y) = 1"
6.296    proof -
6.297      have "(inverse y * inverse x) * (x * y) =
6.298          (inverse y * (inverse x * x)) * y"
6.299        by (simp only: group_assoc)
6.300 -    also have "... = (inverse y * one) * y"
6.301 +    also have "... = (inverse y * 1) * y"
6.302        by (simp only: group_left_inverse)
6.303      also have "... = inverse y * y"
6.304        by (simp only: group_right_one)
6.305 -    also have "... = one"
6.306 +    also have "... = 1"
6.307        by (simp only: group_left_inverse)
6.308      finally show ?thesis .
6.309    qed
6.310  qed
6.311
6.312 -theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
6.313 +theorem (in group) inverse_inverse: "inverse (inverse x) = x"
6.314  proof (rule group_inverse_equality)
6.315    show "x * inverse x = one"
6.316      by (simp only: group_right_inverse)
6.317  qed
6.318
6.319 -theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
6.320 +theorem (in group) inverse_inject:
6.321 +  assumes eq: "inverse x = inverse y"
6.322 +  shows "x = y"
6.323  proof -
6.324 -  assume eq: "inverse x = inverse y"
6.325 -  have "x = x * one"
6.326 +  have "x = x * 1"
6.327      by (simp only: group_right_one)
6.328    also have "... = x * (inverse y * y)"
6.329      by (simp only: group_left_inverse)
6.330 @@ -254,7 +235,7 @@
6.331      by (simp only: eq)
6.332    also have "... = (x * inverse x) * y"
6.333      by (simp only: group_assoc)
6.334 -  also have "... = one * y"
6.335 +  also have "... = 1 * y"
6.336      by (simp only: group_right_inverse)
6.337    also have "... = y"
6.338      by (simp only: group_left_one)

     7.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Thu Jul 01 14:32:57 2010 +0200
7.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Jul 01 18:31:46 2010 +0200
7.3 @@ -13,14 +13,12 @@
7.4
7.5  subsection {* Abstract syntax and semantics *}
7.6
7.7 -text {*
7.8 - The following abstract syntax and semantics of Hoare Logic over
7.9 - \texttt{WHILE} programs closely follows the existing tradition in
7.10 - Isabelle/HOL of formalizing the presentation given in
7.12 - \url{http://isabelle.in.tum.de/library/Hoare/} and
7.13 - \cite{Nipkow:1998:Winskel}.
7.14 -*}
7.15 +text {* The following abstract syntax and semantics of Hoare Logic
7.16 +  over \texttt{WHILE} programs closely follows the existing tradition
7.17 +  in Isabelle/HOL of formalizing the presentation given in
7.19 +  \url{http://isabelle.in.tum.de/library/Hoare/} and
7.20 +  \cite{Nipkow:1998:Winskel}. *}
7.21
7.22  types
7.23    'a bexp = "'a set"
7.24 @@ -32,33 +30,31 @@
7.25    | Cond "'a bexp" "'a com" "'a com"
7.26    | While "'a bexp" "'a assn" "'a com"
7.27
7.28 -abbreviation
7.29 -  Skip  ("SKIP") where
7.30 -  "SKIP == Basic id"
7.31 +abbreviation Skip  ("SKIP")
7.32 +  where "SKIP == Basic id"
7.33
7.34  types
7.35    'a sem = "'a => 'a => bool"
7.36
7.37 -consts
7.38 -  iter :: "nat => 'a bexp => 'a sem => 'a sem"
7.39 -primrec
7.40 +primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
7.41 +where
7.42    "iter 0 b S s s' = (s ~: b & s = s')"
7.43 -  "iter (Suc n) b S s s' =
7.44 -    (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
7.45 +| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
7.46
7.47 -consts
7.48 -  Sem :: "'a com => 'a sem"
7.49 -primrec
7.50 +primrec Sem :: "'a com => 'a sem"
7.51 +where
7.52    "Sem (Basic f) s s' = (s' = f s)"
7.53 -  "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
7.54 -  "Sem (Cond b c1 c2) s s' =
7.55 +| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
7.56 +| "Sem (Cond b c1 c2) s s' =
7.57      (if s : b then Sem c1 s s' else Sem c2 s s')"
7.58 -  "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
7.59 +| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
7.60
7.61 -definition Valid :: "'a bexp => 'a com => 'a bexp => bool" ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) where
7.62 -  "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
7.63 +definition
7.64 +  Valid :: "'a bexp => 'a com => 'a bexp => bool"
7.65 +    ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
7.66 +  where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
7.67
7.68 -notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
7.69 +notation (xsymbols) Valid  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
7.70
7.71  lemma ValidI [intro?]:
7.72      "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
7.73 @@ -71,22 +67,20 @@
7.74
7.75  subsection {* Primitive Hoare rules *}
7.76
7.77 -text {*
7.78 - From the semantics defined above, we derive the standard set of
7.79 - primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.  Usually,
7.80 - variant forms of these rules are applied in actual proof, see also
7.81 - \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
7.82 +text {* From the semantics defined above, we derive the standard set
7.83 +  of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.
7.84 +  Usually, variant forms of these rules are applied in actual proof,
7.86
7.87 - \medskip The \name{basic} rule represents any kind of atomic access
7.88 - to the state space.  This subsumes the common rules of \name{skip}
7.89 - and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.
7.90 -*}
7.91 +  \medskip The \name{basic} rule represents any kind of atomic access
7.92 +  to the state space.  This subsumes the common rules of \name{skip}
7.93 +  and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
7.94
7.95  theorem basic: "|- {s. f s : P} (Basic f) P"
7.96  proof
7.97    fix s s' assume s: "s : {s. f s : P}"
7.98    assume "Sem (Basic f) s s'"
7.99 -  hence "s' = f s" by simp
7.100 +  then have "s' = f s" by simp
7.101    with s show "s' : P" by simp
7.102  qed
7.103
7.104 @@ -117,11 +111,9 @@
7.105    with QQ' show "s' : Q'" ..
7.106  qed
7.107
7.108 -text {*
7.109 - The rule for conditional commands is directly reflected by the
7.110 - corresponding semantics; in the proof we just have to look closely
7.111 - which cases apply.
7.112 -*}
7.113 +text {* The rule for conditional commands is directly reflected by the
7.114 +  corresponding semantics; in the proof we just have to look closely
7.115 +  which cases apply. *}
7.116
7.117  theorem cond:
7.118    "|- (P Int b) c1 Q ==> |- (P Int -b) c2 Q ==> |- P (Cond b c1 c2) Q"
7.119 @@ -147,14 +139,12 @@
7.120    qed
7.121  qed
7.122
7.123 -text {*
7.124 - The \name{while} rule is slightly less trivial --- it is the only one
7.125 - based on recursion, which is expressed in the semantics by a
7.126 - Kleene-style least fixed-point construction.  The auxiliary statement
7.127 - below, which is by induction on the number of iterations is the main
7.128 - point to be proven; the rest is by routine application of the
7.129 - semantics of \texttt{WHILE}.
7.130 -*}
7.131 +text {* The @{text while} rule is slightly less trivial --- it is the
7.132 +  only one based on recursion, which is expressed in the semantics by
7.133 +  a Kleene-style least fixed-point construction.  The auxiliary
7.134 +  statement below, which is by induction on the number of iterations
7.135 +  is the main point to be proven; the rest is by routine application
7.136 +  of the semantics of \texttt{WHILE}. *}
7.137
7.138  theorem while:
7.139    assumes body: "|- (P Int b) c P"
7.140 @@ -166,12 +156,11 @@
7.141    from this and s show "s' : P Int -b"
7.142    proof (induct n arbitrary: s)
7.143      case 0
7.144 -    thus ?case by auto
7.145 +    then show ?case by auto
7.146    next
7.147      case (Suc n)
7.148      then obtain s'' where b: "s : b" and sem: "Sem c s s''"
7.149 -      and iter: "iter n b (Sem c) s'' s'"
7.150 -      by auto
7.151 +      and iter: "iter n b (Sem c) s'' s'" by auto
7.152      from Suc and b have "s : P Int b" by simp
7.153      with body sem have "s'' : P" ..
7.154      with iter show ?case by (rule Suc)
7.155 @@ -181,30 +170,26 @@
7.156
7.157  subsection {* Concrete syntax for assertions *}
7.158
7.159 -text {*
7.160 - We now introduce concrete syntax for describing commands (with
7.161 - embedded expressions) and assertions. The basic technique is that of
7.162 - semantic quote-antiquote''.  A \emph{quotation} is a syntactic
7.163 - entity delimited by an implicit abstraction, say over the state
7.164 - space.  An \emph{antiquotation} is a marked expression within a
7.165 - quotation that refers the implicit argument; a typical antiquotation
7.166 - would select (or even update) components from the state.
7.167 +text {* We now introduce concrete syntax for describing commands (with
7.168 +  embedded expressions) and assertions. The basic technique is that of
7.169 +  semantic quote-antiquote''.  A \emph{quotation} is a syntactic
7.170 +  entity delimited by an implicit abstraction, say over the state
7.171 +  space.  An \emph{antiquotation} is a marked expression within a
7.172 +  quotation that refers the implicit argument; a typical antiquotation
7.173 +  would select (or even update) components from the state.
7.174
7.175 - We will see some examples later in the concrete rules and
7.176 - applications.
7.177 -*}
7.178 +  We will see some examples later in the concrete rules and
7.179 +  applications. *}
7.180
7.181 -text {*
7.182 - The following specification of syntax and translations is for
7.183 - Isabelle experts only; feel free to ignore it.
7.184 +text {* The following specification of syntax and translations is for
7.185 +  Isabelle experts only; feel free to ignore it.
7.186
7.187 - While the first part is still a somewhat intelligible specification
7.188 - of the concrete syntactic representation of our Hoare language, the
7.189 - actual ML drivers'' is quite involved.  Just note that the we
7.190 - re-use the basic quote/antiquote translations as already defined in
7.191 - Isabelle/Pure (see \verb,Syntax.quote_tr, and
7.192 - \verb,Syntax.quote_tr',).
7.193 -*}
7.194 +  While the first part is still a somewhat intelligible specification
7.195 +  of the concrete syntactic representation of our Hoare language, the
7.196 +  actual ML drivers'' is quite involved.  Just note that the we
7.197 +  re-use the basic quote/antiquote translations as already defined in
7.198 +  Isabelle/Pure (see \verb,Syntax.quote_tr, and
7.199 +  \verb,Syntax.quote_tr',). *}
7.200
7.201  syntax
7.202    "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
7.203 @@ -238,11 +223,10 @@
7.204    in [(@{syntax_const "_quote"}, quote_tr)] end
7.205  *}
7.206
7.207 -text {*
7.208 - As usual in Isabelle syntax translations, the part for printing is
7.209 - more complicated --- we cannot express parts as macro rules as above.
7.210 - Don't look here, unless you have to do similar things for yourself.
7.211 -*}
7.212 +text {* As usual in Isabelle syntax translations, the part for
7.213 +  printing is more complicated --- we cannot express parts as macro
7.214 +  rules as above.  Don't look here, unless you have to do similar
7.215 +  things for yourself. *}
7.216
7.217  print_translation {*
7.218    let
7.219 @@ -277,15 +261,13 @@
7.220
7.221  subsection {* Rules for single-step proof \label{sec:hoare-isar} *}
7.222
7.223 -text {*
7.224 - We are now ready to introduce a set of Hoare rules to be used in
7.225 - single-step structured proofs in Isabelle/Isar.  We refer to the
7.226 - concrete syntax introduce above.
7.227 +text {* We are now ready to introduce a set of Hoare rules to be used
7.228 +  in single-step structured proofs in Isabelle/Isar.  We refer to the
7.229 +  concrete syntax introduce above.
7.230
7.231 - \medskip Assertions of Hoare Logic may be manipulated in
7.232 - calculational proofs, with the inclusion expressed in terms of sets
7.233 - or predicates.  Reversed order is supported as well.
7.234 -*}
7.235 +  \medskip Assertions of Hoare Logic may be manipulated in
7.236 +  calculational proofs, with the inclusion expressed in terms of sets
7.237 +  or predicates.  Reversed order is supported as well. *}
7.238
7.239  lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
7.240    by (unfold Valid_def) blast
7.241 @@ -312,49 +294,41 @@
7.243
7.244
7.245 -text {*
7.246 - Identity and basic assignments.\footnote{The $\idt{hoare}$ method
7.247 - introduced in \S\ref{sec:hoare-vcg} is able to provide proper
7.248 - instances for any number of basic assignments, without producing
7.250 -*}
7.251 +text {* Identity and basic assignments.\footnote{The $\idt{hoare}$
7.252 +  method introduced in \S\ref{sec:hoare-vcg} is able to provide proper
7.253 +  instances for any number of basic assignments, without producing
7.254 +  additional verification conditions.} *}
7.255
7.256  lemma skip [intro?]: "|- P SKIP P"
7.257  proof -
7.258    have "|- {s. id s : P} SKIP P" by (rule basic)
7.259 -  thus ?thesis by simp
7.260 +  then show ?thesis by simp
7.261  qed
7.262
7.263  lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
7.264    by (rule basic)
7.265
7.266 -text {*
7.267 - Note that above formulation of assignment corresponds to our
7.268 - preferred way to model state spaces, using (extensible) record types
7.269 - in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field
7.270 - $x$, Isabelle/HOL provides a functions $x$ (selector) and
7.271 - $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
7.272 - appearing for the latter kind of function: due to concrete syntax
7.273 - \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
7.274 - to the external nature of HOL record fields, we could not even state
7.275 - a general theorem relating selector and update functions (if this
7.276 - were required here); this would only work for any particular instance
7.277 - of record fields introduced so far.}
7.278 -*}
7.279 +text {* Note that above formulation of assignment corresponds to our
7.280 +  preferred way to model state spaces, using (extensible) record types
7.281 +  in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field
7.282 +  $x$, Isabelle/HOL provides a functions $x$ (selector) and
7.283 +  $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
7.284 +  appearing for the latter kind of function: due to concrete syntax
7.285 +  \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that
7.286 +  due to the external nature of HOL record fields, we could not even
7.287 +  state a general theorem relating selector and update functions (if
7.288 +  this were required here); this would only work for any particular
7.289 +  instance of record fields introduced so far.} *}
7.290
7.291 -text {*
7.292 - Sequential composition --- normalizing with associativity achieves
7.293 - proper of chunks of code verified separately.
7.294 -*}
7.295 +text {* Sequential composition --- normalizing with associativity
7.296 +  achieves proper of chunks of code verified separately. *}
7.297
7.298  lemmas [trans, intro?] = seq
7.299
7.300  lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
7.301    by (auto simp add: Valid_def)
7.302
7.303 -text {*
7.304 - Conditional statements.
7.305 -*}
7.306 +text {* Conditional statements. *}
7.307
7.308  lemmas [trans, intro?] = cond
7.309
7.310 @@ -364,9 +338,7 @@
7.311        ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
7.312      by (rule cond) (simp_all add: Valid_def)
7.313
7.314 -text {*
7.315 - While statements --- with optional invariant.
7.316 -*}
7.317 +text {* While statements --- with optional invariant. *}
7.318
7.319  lemma [intro?]:
7.320      "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
7.321 @@ -390,18 +362,16 @@
7.322
7.323  subsection {* Verification conditions \label{sec:hoare-vcg} *}
7.324
7.325 -text {*
7.326 - We now load the \emph{original} ML file for proof scripts and tactic
7.327 - definition for the Hoare Verification Condition Generator (see
7.328 - \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we are
7.329 - concerned here, the result is a proof method \name{hoare}, which may
7.330 - be applied to a Hoare Logic assertion to extract purely logical
7.331 - verification conditions.  It is important to note that the method
7.332 - requires \texttt{WHILE} loops to be fully annotated with invariants
7.333 - beforehand.  Furthermore, only \emph{concrete} pieces of code are
7.334 - handled --- the underlying tactic fails ungracefully if supplied with
7.335 - meta-variables or parameters, for example.
7.336 -*}
7.337 +text {* We now load the \emph{original} ML file for proof scripts and
7.338 +  tactic definition for the Hoare Verification Condition Generator
7.339 +  (see \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we
7.340 +  are concerned here, the result is a proof method \name{hoare}, which
7.341 +  may be applied to a Hoare Logic assertion to extract purely logical
7.342 +  verification conditions.  It is important to note that the method
7.343 +  requires \texttt{WHILE} loops to be fully annotated with invariants
7.344 +  beforehand.  Furthermore, only \emph{concrete} pieces of code are
7.345 +  handled --- the underlying tactic fails ungracefully if supplied
7.346 +  with meta-variables or parameters, for example. *}
7.347
7.348  lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
7.349    by (auto simp add: Valid_def)

     8.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Jul 01 14:32:57 2010 +0200
8.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Jul 01 18:31:46 2010 +0200
8.3 @@ -6,11 +6,9 @@
8.4
8.5  subsection {* State spaces *}
8.6
8.7 -text {*
8.8 - First of all we provide a store of program variables that
8.9 - occur in any of the programs considered later.  Slightly unexpected
8.10 - things may happen when attempting to work with undeclared variables.
8.11 -*}
8.12 +text {* First of all we provide a store of program variables that
8.13 +  occur in any of the programs considered later.  Slightly unexpected
8.14 +  things may happen when attempting to work with undeclared variables. *}
8.15
8.16  record vars =
8.17    I :: nat
8.18 @@ -18,37 +16,29 @@
8.19    N :: nat
8.20    S :: nat
8.21
8.22 -text {*
8.23 - While all of our variables happen to have the same type, nothing
8.24 - would prevent us from working with many-sorted programs as well, or
8.25 - even polymorphic ones.  Also note that Isabelle/HOL's extensible
8.26 - record types even provides simple means to extend the state space
8.27 - later.
8.28 -*}
8.29 +text {* While all of our variables happen to have the same type,
8.30 +  nothing would prevent us from working with many-sorted programs as
8.31 +  well, or even polymorphic ones.  Also note that Isabelle/HOL's
8.32 +  extensible record types even provides simple means to extend the
8.33 +  state space later. *}
8.34
8.35
8.36  subsection {* Basic examples *}
8.37
8.38 -text {*
8.39 - We look at few trivialities involving assignment and sequential
8.40 - composition, in order to get an idea of how to work with our
8.41 - formulation of Hoare Logic.
8.42 -*}
8.43 +text {* We look at few trivialities involving assignment and
8.44 +  sequential composition, in order to get an idea of how to work with
8.45 +  our formulation of Hoare Logic. *}
8.46
8.47 -text {*
8.48 - Using the basic \name{assign} rule directly is a bit cumbersome.
8.49 -*}
8.50 +text {* Using the basic @{text assign} rule directly is a bit
8.51 +  cumbersome. *}
8.52
8.53 -lemma
8.54 -  "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
8.55 +lemma "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
8.56    by (rule assign)
8.57
8.58 -text {*
8.59 - Certainly we want the state modification already done, e.g.\ by
8.60 - simplification.  The \name{hoare} method performs the basic state
8.61 - update for us; we may apply the Simplifier afterwards to achieve
8.62 - obvious'' consequences as well.
8.63 -*}
8.64 +text {* Certainly we want the state modification already done, e.g.\
8.65 +  by simplification.  The \name{hoare} method performs the basic state
8.66 +  update for us; we may apply the Simplifier afterwards to achieve
8.67 +  obvious'' consequences as well. *}
8.68
8.69  lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
8.70    by hoare
8.71 @@ -77,12 +67,10 @@
8.72      .{\<acute>M = b & \<acute>N = a}."
8.73    by hoare simp
8.74
8.75 -text {*
8.76 - It is important to note that statements like the following one can
8.77 - only be proven for each individual program variable.  Due to the
8.78 - extra-logical nature of record fields, we cannot formulate a theorem
8.79 - relating record selectors and updates schematically.
8.80 -*}
8.81 +text {* It is important to note that statements like the following one
8.82 +  can only be proven for each individual program variable.  Due to the
8.83 +  extra-logical nature of record fields, we cannot formulate a theorem
8.84 +  relating record selectors and updates schematically. *}
8.85
8.86  lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
8.87    by hoare
8.88 @@ -96,11 +84,9 @@
8.89    oops
8.90
8.91
8.92 -text {*
8.93 - In the following assignments we make use of the consequence rule in
8.94 - order to achieve the intended precondition.  Certainly, the
8.95 - \name{hoare} method is able to handle this case, too.
8.96 -*}
8.97 +text {* In the following assignments we make use of the consequence
8.98 +  rule in order to achieve the intended precondition.  Certainly, the
8.99 +  \name{hoare} method is able to handle this case, too. *}
8.100
8.101  lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
8.102  proof -
8.103 @@ -128,12 +114,10 @@
8.104
8.105  subsection {* Multiplication by addition *}
8.106
8.107 -text {*
8.108 - We now do some basic examples of actual \texttt{WHILE} programs.
8.109 - This one is a loop for calculating the product of two natural
8.110 - numbers, by iterated addition.  We first give detailed structured
8.111 - proof based on single-step Hoare rules.
8.112 -*}
8.113 +text {* We now do some basic examples of actual \texttt{WHILE}
8.114 +  programs.  This one is a loop for calculating the product of two
8.115 +  natural numbers, by iterated addition.  We first give detailed
8.116 +  structured proof based on single-step Hoare rules. *}
8.117
8.118  lemma
8.119    "|- .{\<acute>M = 0 & \<acute>S = 0}.
8.120 @@ -157,12 +141,10 @@
8.121    finally show ?thesis .
8.122  qed
8.123
8.124 -text {*
8.125 - The subsequent version of the proof applies the \name{hoare} method
8.126 - to reduce the Hoare statement to a purely logical problem that can be
8.127 - solved fully automatically.  Note that we have to specify the
8.128 - \texttt{WHILE} loop invariant in the original statement.
8.129 -*}
8.130 +text {* The subsequent version of the proof applies the @{text hoare}
8.131 +  method to reduce the Hoare statement to a purely logical problem
8.132 +  that can be solved fully automatically.  Note that we have to
8.133 +  specify the \texttt{WHILE} loop invariant in the original statement. *}
8.134
8.135  lemma
8.136    "|- .{\<acute>M = 0 & \<acute>S = 0}.
8.137 @@ -175,21 +157,15 @@
8.138
8.139  subsection {* Summing natural numbers *}
8.140
8.141 -text {*
8.142 - We verify an imperative program to sum natural numbers up to a given
8.143 - limit.  First some functional definition for proper specification of
8.144 - the problem.
8.145 -*}
8.146 +text {* We verify an imperative program to sum natural numbers up to a
8.147 +  given limit.  First some functional definition for proper
8.148 +  specification of the problem. *}
8.149
8.150 -text {*
8.151 - The following proof is quite explicit in the individual steps taken,
8.152 - with the \name{hoare} method only applied locally to take care of
8.153 - assignment and sequential composition.  Note that we express
8.154 - intermediate proof obligation in pure logic, without referring to the
8.155 - state space.
8.156 -*}
8.157 -
8.158 -declare atLeast0LessThan[symmetric,simp]
8.159 +text {* The following proof is quite explicit in the individual steps
8.160 +  taken, with the \name{hoare} method only applied locally to take
8.161 +  care of assignment and sequential composition.  Note that we express
8.162 +  intermediate proof obligation in pure logic, without referring to
8.163 +  the state space. *}
8.164
8.165  theorem
8.166    "|- .{True}.
8.167 @@ -227,10 +203,9 @@
8.168    finally show ?thesis .
8.169  qed
8.170
8.171 -text {*
8.172 - The next version uses the \name{hoare} method, while still explaining
8.173 - the resulting proof obligations in an abstract, structured manner.
8.174 -*}
8.175 +text {* The next version uses the @{text hoare} method, while still
8.176 +  explaining the resulting proof obligations in an abstract,
8.177 +  structured manner. *}
8.178
8.179  theorem
8.180    "|- .{True}.
8.181 @@ -251,17 +226,15 @@
8.182      show "?inv 0 1" by simp
8.183    next
8.184      fix s i assume "?inv s i & i ~= n"
8.185 -    thus "?inv (s + i) (i + 1)" by simp
8.186 +    then show "?inv (s + i) (i + 1)" by simp
8.187    next
8.188      fix s i assume "?inv s i & ~ i ~= n"
8.189 -    thus "s = ?sum n" by simp
8.190 +    then show "s = ?sum n" by simp
8.191    qed
8.192  qed
8.193
8.194 -text {*
8.195 - Certainly, this proof may be done fully automatic as well, provided
8.196 - that the invariant is given beforehand.
8.197 -*}
8.198 +text {* Certainly, this proof may be done fully automatic as well,
8.199 +  provided that the invariant is given beforehand. *}
8.200
8.201  theorem
8.202    "|- .{True}.
8.203 @@ -278,21 +251,19 @@
8.204
8.205  subsection{* Time *}
8.206
8.207 -text{*
8.208 -  A simple embedding of time in Hoare logic: function @{text timeit}
8.209 -  inserts an extra variable to keep track of the elapsed time.
8.210 -*}
8.211 +text{* A simple embedding of time in Hoare logic: function @{text
8.212 +  timeit} inserts an extra variable to keep track of the elapsed time. *}
8.213
8.214  record tstate = time :: nat
8.215
8.216  types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
8.217
8.218 -consts timeit :: "'a time com \<Rightarrow> 'a time com"
8.219 -primrec
8.220 +primrec timeit :: "'a time com \<Rightarrow> 'a time com"
8.221 +where
8.222    "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
8.223 -  "timeit (c1; c2) = (timeit c1; timeit c2)"
8.224 -  "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
8.225 -  "timeit (While b iv c) = While b iv (timeit c)"
8.226 +| "timeit (c1; c2) = (timeit c1; timeit c2)"
8.227 +| "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
8.228 +| "timeit (While b iv c) = While b iv (timeit c)"
8.229
8.230  record tvars = tstate +
8.231    I :: nat

     9.1 --- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Thu Jul 01 14:32:57 2010 +0200
9.2 +++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Thu Jul 01 18:31:46 2010 +0200
9.3 @@ -13,10 +13,10 @@
9.4
9.5  subsection {* Prose version *}
9.6
9.7 -text {*
9.8 -  According to the textbook \cite[pages 93--94]{davey-priestley}, the
9.9 -  Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
9.10 -  dualized the argument, and tuned the notation a little bit.}
9.11 +text {* According to the textbook \cite[pages
9.12 +  93--94]{davey-priestley}, the Knaster-Tarski fixpoint theorem is as
9.13 +  follows.\footnote{We have dualized the argument, and tuned the
9.14 +  notation a little bit.}
9.15
9.16    \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
9.17    complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
9.18 @@ -28,19 +28,16 @@
9.19    H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
9.20    the reverse one (!) and thereby complete the proof that @{text a} is
9.21    a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
9.22 -  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
9.23 -*}
9.24 +  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}. *}
9.25
9.26
9.27  subsection {* Formal versions *}
9.28
9.29 -text {*
9.30 -  The Isar proof below closely follows the original presentation.
9.31 -  Virtually all of the prose narration has been rephrased in terms of
9.32 -  formal Isar language elements.  Just as many textbook-style proofs,
9.33 -  there is a strong bias towards forward proof, and several bends in
9.34 -  the course of reasoning.
9.35 -*}
9.36 +text {* The Isar proof below closely follows the original
9.37 +  presentation.  Virtually all of the prose narration has been
9.38 +  rephrased in terms of formal Isar language elements.  Just as many
9.39 +  textbook-style proofs, there is a strong bias towards forward proof,
9.40 +  and several bends in the course of reasoning. *}
9.41
9.42  theorem Knaster_Tarski:
9.43    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
9.44 @@ -70,17 +67,15 @@
9.45    qed
9.46  qed
9.47
9.48 -text {*
9.49 -  Above we have used several advanced Isar language elements, such as
9.50 -  explicit block structure and weak assumptions.  Thus we have
9.51 +text {* Above we have used several advanced Isar language elements,
9.52 +  such as explicit block structure and weak assumptions.  Thus we have
9.53    mimicked the particular way of reasoning of the original text.
9.54
9.55    In the subsequent version the order of reasoning is changed to
9.56    achieve structured top-down decomposition of the problem at the
9.57    outer level, while only the inner steps of reasoning are done in a
9.58    forward manner.  We are certainly more at ease here, requiring only
9.59 -  the most basic features of the Isar language.
9.60 -*}
9.61 +  the most basic features of the Isar language. *}
9.62
9.63  theorem Knaster_Tarski':
9.64    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"

    10.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Jul 01 14:32:57 2010 +0200
10.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Jul 01 18:31:46 2010 +0200
10.3 @@ -9,27 +9,26 @@
10.4  imports Main
10.5  begin
10.6
10.7 -text {*
10.8 - The Mutilated Checker Board Problem, formalized inductively.  See
10.9 - \cite{paulson-mutilated-board} and
10.10 - \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the
10.11 - original tactic script version.
10.12 -*}
10.13 +text {* The Mutilated Checker Board Problem, formalized inductively.
10.14 +  See \cite{paulson-mutilated-board} and
10.15 +  \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for
10.16 +  the original tactic script version. *}
10.17
10.18  subsection {* Tilings *}
10.19
10.20 -inductive_set
10.21 -  tiling :: "'a set set => 'a set set"
10.22 +inductive_set tiling :: "'a set set => 'a set set"
10.23    for A :: "'a set set"
10.24 -  where
10.25 -    empty: "{} : tiling A"
10.26 -  | Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
10.27 +where
10.28 +  empty: "{} : tiling A"
10.29 +| Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
10.30
10.31
10.32  text "The union of two disjoint tilings is a tiling."
10.33
10.34  lemma tiling_Un:
10.35 -  assumes "t : tiling A" and "u : tiling A" and "t Int u = {}"
10.36 +  assumes "t : tiling A"
10.37 +    and "u : tiling A"
10.38 +    and "t Int u = {}"
10.39    shows "t Un u : tiling A"
10.40  proof -
10.41    let ?T = "tiling A"
10.42 @@ -60,8 +59,8 @@
10.43
10.44  subsection {* Basic properties of below'' *}
10.45
10.46 -definition below :: "nat => nat set" where
10.47 -  "below n == {i. i < n}"
10.48 +definition below :: "nat => nat set"
10.49 +  where "below n = {i. i < n}"
10.50
10.51  lemma below_less_iff [iff]: "(i: below k) = (i < k)"
10.53 @@ -74,8 +73,8 @@
10.54    by (simp add: below_def less_Suc_eq) blast
10.55
10.56  lemma Sigma_Suc2:
10.57 -    "m = n + 2 ==> A <*> below m =
10.58 -      (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
10.59 +  "m = n + 2 ==> A <*> below m =
10.60 +    (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
10.61    by (auto simp add: below_def)
10.62
10.63  lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
10.64 @@ -83,27 +82,26 @@
10.65
10.66  subsection {* Basic properties of evnodd'' *}
10.67
10.68 -definition evnodd :: "(nat * nat) set => nat => (nat * nat) set" where
10.69 -  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
10.70 +definition evnodd :: "(nat * nat) set => nat => (nat * nat) set"
10.71 +  where "evnodd A b = A Int {(i, j). (i + j) mod 2 = b}"
10.72
10.73 -lemma evnodd_iff:
10.74 -    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
10.75 +lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
10.77
10.78  lemma evnodd_subset: "evnodd A b <= A"
10.79 -  by (unfold evnodd_def, rule Int_lower1)
10.80 +  unfolding evnodd_def by (rule Int_lower1)
10.81
10.82  lemma evnoddD: "x : evnodd A b ==> x : A"
10.83 -  by (rule subsetD, rule evnodd_subset)
10.84 +  by (rule subsetD) (rule evnodd_subset)
10.85
10.86  lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
10.87 -  by (rule finite_subset, rule evnodd_subset)
10.88 +  by (rule finite_subset) (rule evnodd_subset)
10.89
10.90  lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"
10.91 -  by (unfold evnodd_def) blast
10.92 +  unfolding evnodd_def by blast
10.93
10.94  lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
10.95 -  by (unfold evnodd_def) blast
10.96 +  unfolding evnodd_def by blast
10.97
10.98  lemma evnodd_empty: "evnodd {} b = {}"
10.100 @@ -116,11 +114,10 @@
10.101
10.102  subsection {* Dominoes *}
10.103
10.104 -inductive_set
10.105 -  domino :: "(nat * nat) set set"
10.106 -  where
10.107 -    horiz: "{(i, j), (i, j + 1)} : domino"
10.108 -  | vertl: "{(i, j), (i + 1, j)} : domino"
10.109 +inductive_set domino :: "(nat * nat) set set"
10.110 +where
10.111 +  horiz: "{(i, j), (i, j + 1)} : domino"
10.112 +| vertl: "{(i, j), (i + 1, j)} : domino"
10.113
10.114  lemma dominoes_tile_row:
10.115    "{i} <*> below (2 * n) : tiling domino"
10.116 @@ -165,9 +162,10 @@
10.117  qed
10.118
10.119  lemma domino_singleton:
10.120 -  assumes d: "d : domino" and "b < 2"
10.121 +  assumes "d : domino"
10.122 +    and "b < 2"
10.123    shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
10.124 -  using d
10.125 +  using assms
10.126  proof induct
10.127    from b < 2 have b_cases: "b = 0 | b = 1" by arith
10.128    fix i j
10.129 @@ -177,9 +175,9 @@
10.130  qed
10.131
10.132  lemma domino_finite:
10.133 -  assumes d: "d: domino"
10.134 +  assumes "d: domino"
10.135    shows "finite d"
10.136 -  using d
10.137 +  using assms
10.138  proof induct
10.139    fix i j :: nat
10.140    show "finite {(i, j), (i, j + 1)}" by (intro finite.intros)
10.141 @@ -245,8 +243,9 @@
10.142
10.143  subsection {* Main theorem *}
10.144
10.145 -definition mutilated_board :: "nat => nat => (nat * nat) set" where
10.146 -  "mutilated_board m n ==
10.147 +definition mutilated_board :: "nat => nat => (nat * nat) set"
10.148 +where
10.149 +  "mutilated_board m n =
10.150      below (2 * (m + 1)) <*> below (2 * (n + 1))
10.151        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
10.152
10.153 @@ -256,7 +255,7 @@
10.154    let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
10.155    let ?t' = "?t - {(0, 0)}"
10.156    let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
10.157 -
10.158 +
10.159    show "?t'' ~: ?T"
10.160    proof
10.161      have t: "?t : ?T" by (rule dominoes_tile_matrix)

    11.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Thu Jul 01 14:32:57 2010 +0200
11.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Thu Jul 01 18:31:46 2010 +0200
11.3 @@ -10,8 +10,10 @@
11.4      Var 'a
11.5    | App 'b "('a, 'b) term list"
11.6
11.7 -primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
11.8 -  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
11.9 +primrec
11.10 +  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
11.11 +  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
11.12 +where
11.13    "subst_term f (Var a) = f a"
11.14  | "subst_term f (App b ts) = App b (subst_term_list f ts)"
11.15  | "subst_term_list f [] = []"
11.16 @@ -19,18 +21,18 @@
11.17
11.18  lemmas subst_simps = subst_term_subst_term_list.simps
11.19
11.20 -text {*
11.21 - \medskip A simple lemma about composition of substitutions.
11.22 -*}
11.23 +text {* \medskip A simple lemma about composition of substitutions. *}
11.24
11.25 -lemma "subst_term (subst_term f1 o f2) t =
11.26 -      subst_term f1 (subst_term f2 t)"
11.27 -  and "subst_term_list (subst_term f1 o f2) ts =
11.28 -      subst_term_list f1 (subst_term_list f2 ts)"
11.29 +lemma
11.30 +  "subst_term (subst_term f1 o f2) t =
11.31 +    subst_term f1 (subst_term f2 t)"
11.32 +  and
11.33 +  "subst_term_list (subst_term f1 o f2) ts =
11.34 +    subst_term_list f1 (subst_term_list f2 ts)"
11.35    by (induct t and ts) simp_all
11.36
11.37  lemma "subst_term (subst_term f1 o f2) t =
11.38 -  subst_term f1 (subst_term f2 t)"
11.39 +    subst_term f1 (subst_term f2 t)"
11.40  proof -
11.41    let "?P t" = ?thesis
11.42    let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =

    12.1 --- a/src/HOL/Isar_Examples/Peirce.thy	Thu Jul 01 14:32:57 2010 +0200
12.2 +++ b/src/HOL/Isar_Examples/Peirce.thy	Thu Jul 01 18:31:46 2010 +0200
12.3 @@ -8,17 +8,16 @@
12.4  imports Main
12.5  begin
12.6
12.7 -text {*
12.8 - We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
12.9 - an inherently non-intuitionistic statement, so its proof will
12.10 - certainly involve some form of classical contradiction.
12.11 +text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
12.12 +  This is an inherently non-intuitionistic statement, so its proof
12.13 +  will certainly involve some form of classical contradiction.
12.14
12.15 - The first proof is again a well-balanced combination of plain
12.16 - backward and forward reasoning.  The actual classical step is where
12.17 - the negated goal may be introduced as additional assumption.  This
12.19 - is negation elimination; it holds in intuitionistic logic as well.}
12.20 -*}
12.21 +  The first proof is again a well-balanced combination of plain
12.22 +  backward and forward reasoning.  The actual classical step is where
12.23 +  the negated goal may be introduced as additional assumption.  This
12.25 +  there is negation elimination; it holds in intuitionistic logic as
12.26 +  well.} *}
12.27
12.28  theorem "((A --> B) --> A) --> A"
12.29  proof
12.30 @@ -35,21 +34,19 @@
12.31    qed
12.32  qed
12.33
12.34 -text {*
12.35 - In the subsequent version the reasoning is rearranged by means of
12.36 - weak assumptions'' (as introduced by \isacommand{presume}).  Before
12.37 - assuming the negated goal $\neg A$, its intended consequence $A \impl 12.38 - B$ is put into place in order to solve the main problem.
12.39 - Nevertheless, we do not get anything for free, but have to establish
12.40 - $A \impl B$ later on.  The overall effect is that of a logical
12.41 - \emph{cut}.
12.42 +text {* In the subsequent version the reasoning is rearranged by means
12.43 +  of weak assumptions'' (as introduced by \isacommand{presume}).
12.44 +  Before assuming the negated goal $\neg A$, its intended consequence
12.45 +  $A \impl B$ is put into place in order to solve the main problem.
12.46 +  Nevertheless, we do not get anything for free, but have to establish
12.47 +  $A \impl B$ later on.  The overall effect is that of a logical
12.48 +  \emph{cut}.
12.49
12.50 - Technically speaking, whenever some goal is solved by
12.51 - \isacommand{show} in the context of weak assumptions then the latter
12.52 - give rise to new subgoals, which may be established separately.  In
12.53 - contrast, strong assumptions (as introduced by \isacommand{assume})
12.54 - are solved immediately.
12.55 -*}
12.56 +  Technically speaking, whenever some goal is solved by
12.57 +  \isacommand{show} in the context of weak assumptions then the latter
12.58 +  give rise to new subgoals, which may be established separately.  In
12.59 +  contrast, strong assumptions (as introduced by \isacommand{assume})
12.60 +  are solved immediately. *}
12.61
12.62  theorem "((A --> B) --> A) --> A"
12.63  proof
12.64 @@ -68,23 +65,21 @@
12.65    qed
12.66  qed
12.67
12.68 -text {*
12.69 - Note that the goals stemming from weak assumptions may be even left
12.70 - until qed time, where they get eventually solved by assumption'' as
12.71 - well.  In that case there is really no fundamental difference between
12.72 - the two kinds of assumptions, apart from the order of reducing the
12.73 - individual parts of the proof configuration.
12.74 +text {* Note that the goals stemming from weak assumptions may be even
12.75 +  left until qed time, where they get eventually solved by
12.76 +  assumption'' as well.  In that case there is really no fundamental
12.77 +  difference between the two kinds of assumptions, apart from the
12.78 +  order of reducing the individual parts of the proof configuration.
12.79
12.80 - Nevertheless, the strong'' mode of plain assumptions is quite
12.81 - important in practice to achieve robustness of proof text
12.82 - interpretation.  By forcing both the conclusion \emph{and} the
12.83 - assumptions to unify with the pending goal to be solved, goal
12.84 - selection becomes quite deterministic.  For example, decomposition
12.85 - with rules of the case-analysis'' type usually gives rise to
12.86 - several goals that only differ in there local contexts.  With strong
12.87 - assumptions these may be still solved in any order in a predictable
12.88 - way, while weak ones would quickly lead to great confusion,
12.89 - eventually demanding even some backtracking.
12.90 -*}
12.91 +  Nevertheless, the strong'' mode of plain assumptions is quite
12.92 +  important in practice to achieve robustness of proof text
12.93 +  interpretation.  By forcing both the conclusion \emph{and} the
12.94 +  assumptions to unify with the pending goal to be solved, goal
12.95 +  selection becomes quite deterministic.  For example, decomposition
12.96 +  with rules of the case-analysis'' type usually gives rise to
12.97 +  several goals that only differ in there local contexts.  With strong
12.98 +  assumptions these may be still solved in any order in a predictable
12.99 +  way, while weak ones would quickly lead to great confusion,
12.100 +  eventually demanding even some backtracking. *}
12.101
12.102  end

    13.1 --- a/src/HOL/Isar_Examples/Puzzle.thy	Thu Jul 01 14:32:57 2010 +0200
13.2 +++ b/src/HOL/Isar_Examples/Puzzle.thy	Thu Jul 01 18:31:46 2010 +0200
13.3 @@ -4,17 +4,13 @@
13.4  imports Main
13.5  begin
13.6
13.7 -text_raw {*
13.8 -  \footnote{A question from Bundeswettbewerb Mathematik''.  Original
13.9 -  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
13.10 -  Tobias Nipkow.}
13.11 -*}
13.12 +text_raw {* \footnote{A question from Bundeswettbewerb Mathematik''.
13.13 +  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
13.14 +  script by Tobias Nipkow.} *}
13.15
13.16 -text {*
13.17 -  \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
13.18 -  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
13.19 -  Demonstrate that $f$ is the identity.
13.20 -*}
13.21 +text {* \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$
13.22 +  such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
13.23 +  Demonstrate that $f$ is the identity. *}
13.24
13.25  theorem
13.26    assumes f_ax: "\<And>n. f (f n) < f (Suc n)"

    14.1 --- a/src/HOL/Isar_Examples/Summation.thy	Thu Jul 01 14:32:57 2010 +0200
14.2 +++ b/src/HOL/Isar_Examples/Summation.thy	Thu Jul 01 18:31:46 2010 +0200
14.3 @@ -8,28 +8,22 @@
14.4  imports Main
14.5  begin
14.6
14.7 -text_raw {*
14.8 - \footnote{This example is somewhat reminiscent of the
14.9 - \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
14.10 - discussed in \cite{isabelle-ref} in the context of permutative
14.11 - rewrite rules and ordered rewriting.}
14.12 -*}
14.13 +text_raw {* \footnote{This example is somewhat reminiscent of the
14.14 +  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
14.15 +  discussed in \cite{isabelle-ref} in the context of permutative
14.16 +  rewrite rules and ordered rewriting.} *}
14.17
14.18 -text {*
14.19 - Subsequently, we prove some summation laws of natural numbers
14.20 - (including odds, squares, and cubes).  These examples demonstrate how
14.21 - plain natural deduction (including induction) may be combined with
14.22 - calculational proof.
14.23 -*}
14.24 +text {* Subsequently, we prove some summation laws of natural numbers
14.25 +  (including odds, squares, and cubes).  These examples demonstrate
14.26 +  how plain natural deduction (including induction) may be combined
14.27 +  with calculational proof. *}
14.28
14.29
14.30  subsection {* Summation laws *}
14.31
14.32 -text {*
14.33 - The sum of natural numbers $0 + \cdots + n$ equals $n \times (n + 14.34 - 1)/2$.  Avoiding formal reasoning about division we prove this
14.35 - equation multiplied by $2$.
14.36 -*}
14.37 +text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times 14.38 + (n + 1)/2$.  Avoiding formal reasoning about division we prove this
14.39 +  equation multiplied by $2$. *}
14.40
14.41  theorem sum_of_naturals:
14.42    "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
14.43 @@ -43,48 +37,47 @@
14.44    finally show "?P (Suc n)" by simp
14.45  qed
14.46
14.47 -text {*
14.48 - The above proof is a typical instance of mathematical induction.  The
14.49 - main statement is viewed as some $\var{P} \ap n$ that is split by the
14.50 - induction method into base case $\var{P} \ap 0$, and step case
14.51 - $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
14.52 +text {* The above proof is a typical instance of mathematical
14.53 +  induction.  The main statement is viewed as some $\var{P} \ap n$
14.54 +  that is split by the induction method into base case $\var{P} \ap 14.55 + 0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap 14.56 + n)$ for arbitrary $n$.
14.57
14.58 - The step case is established by a short calculation in forward
14.59 - manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
14.60 - the thesis, the final result is achieved by transformations involving
14.61 - basic arithmetic reasoning (using the Simplifier).  The main point is
14.62 - where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
14.63 - introduced in order to replace a certain subterm.  So the
14.64 - transitivity'' rule involved here is actual \emph{substitution}.
14.65 - Also note how the occurrence of \dots'' in the subsequent step
14.66 - documents the position where the right-hand side of the hypothesis
14.67 - got filled in.
14.68 +  The step case is established by a short calculation in forward
14.69 +  manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
14.70 +  the thesis, the final result is achieved by transformations
14.71 +  involving basic arithmetic reasoning (using the Simplifier).  The
14.72 +  main point is where the induction hypothesis $\var{S} \ap n = n 14.73 + \times (n + 1)$ is introduced in order to replace a certain subterm.
14.74 +  So the transitivity'' rule involved here is actual
14.75 +  \emph{substitution}.  Also note how the occurrence of \dots'' in
14.76 +  the subsequent step documents the position where the right-hand side
14.77 +  of the hypothesis got filled in.
14.78
14.79 - \medskip A further notable point here is integration of calculations
14.80 - with plain natural deduction.  This works so well in Isar for two
14.81 - reasons.
14.82 - \begin{enumerate}
14.83 +  \medskip A further notable point here is integration of calculations
14.84 +  with plain natural deduction.  This works so well in Isar for two
14.85 +  reasons.
14.86 +  \begin{enumerate}
14.87 +
14.88 +  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
14.89 +  calculational chains may be just anything.  There is nothing special
14.90 +  about \isakeyword{have}, so the natural deduction element
14.91 +  \isakeyword{assume} works just as well.
14.92
14.93 - \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
14.94 - calculational chains may be just anything.  There is nothing special
14.95 - about \isakeyword{have}, so the natural deduction element
14.96 - \isakeyword{assume} works just as well.
14.97 +  \item There are two \emph{separate} primitives for building natural
14.98 +  deduction contexts: \isakeyword{fix}~$x$ and
14.99 +  \isakeyword{assume}~$A$.  Thus it is possible to start reasoning
14.100 +  with some new arbitrary, but fixed'' elements before bringing in
14.101 +  the actual assumption.  In contrast, natural deduction is
14.102 +  occasionally formalized with basic context elements of the form
14.103 +  $x:A$ instead.
14.104
14.105 - \item There are two \emph{separate} primitives for building natural
14.106 - deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
14.107 - Thus it is possible to start reasoning with some new arbitrary, but
14.108 - fixed'' elements before bringing in the actual assumption.  In
14.109 - contrast, natural deduction is occasionally formalized with basic
14.110 - context elements of the form $x:A$ instead.
14.111 -
14.112 - \end{enumerate}
14.113 +  \end{enumerate}
14.114  *}
14.115
14.116 -text {*
14.117 - \medskip We derive further summation laws for odds, squares, and
14.118 - cubes as follows.  The basic technique of induction plus calculation
14.119 - is the same as before.
14.120 -*}
14.121 +text {* \medskip We derive further summation laws for odds, squares,
14.122 +  and cubes as follows.  The basic technique of induction plus
14.123 +  calculation is the same as before. *}
14.124
14.125  theorem sum_of_odds:
14.126    "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
14.127 @@ -98,11 +91,9 @@
14.128    finally show "?P (Suc n)" by simp
14.129  qed
14.130
14.131 -text {*
14.132 - Subsequently we require some additional tweaking of Isabelle built-in
14.133 - arithmetic simplifications, such as bringing in distributivity by
14.134 - hand.
14.135 -*}
14.136 +text {* Subsequently we require some additional tweaking of Isabelle
14.137 +  built-in arithmetic simplifications, such as bringing in
14.138 +  distributivity by hand. *}
14.139
14.141
14.142 @@ -116,7 +107,7 @@
14.144    also assume "?S n = n * (n + 1) * (2 * n + 1)"
14.145    also have "... + 6 * (n + 1)^Suc (Suc 0) =
14.146 -    (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
14.147 +      (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
14.148    finally show "?P (Suc n)" by simp
14.149  qed
14.150
14.151 @@ -134,25 +125,23 @@
14.152    finally show "?P (Suc n)" by simp
14.153  qed
14.154
14.155 -text {*
14.156 - Comparing these examples with the tactic script version
14.157 - \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
14.158 - an important difference of how induction vs.\ simplification is
14.159 - applied.  While \cite[\S10]{isabelle-ref} advises for these examples
14.160 - that induction should not be applied until the goal is in the
14.161 - simplest form'' this would be a very bad idea in our setting.
14.162 +text {* Comparing these examples with the tactic script version
14.163 +  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
14.164 +  an important difference of how induction vs.\ simplification is
14.165 +  applied.  While \cite[\S10]{isabelle-ref} advises for these examples
14.166 +  that induction should not be applied until the goal is in the
14.167 +  simplest form'' this would be a very bad idea in our setting.
14.168
14.169 - Simplification normalizes all arithmetic expressions involved,
14.170 - producing huge intermediate goals.  With applying induction
14.171 - afterwards, the Isar proof text would have to reflect the emerging
14.172 - configuration by appropriate sub-proofs.  This would result in badly
14.173 - structured, low-level technical reasoning, without any good idea of
14.174 - the actual point.
14.175 +  Simplification normalizes all arithmetic expressions involved,
14.176 +  producing huge intermediate goals.  With applying induction
14.177 +  afterwards, the Isar proof text would have to reflect the emerging
14.178 +  configuration by appropriate sub-proofs.  This would result in badly
14.179 +  structured, low-level technical reasoning, without any good idea of
14.180 +  the actual point.
14.181
14.182 - \medskip As a general rule of good proof style, automatic methods
14.183 - such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
14.184 - initial proof methods, but only as terminal ones, solving certain
14.185 - goals completely.
14.186 -*}
14.187 +  \medskip As a general rule of good proof style, automatic methods
14.188 +  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used
14.189 +  as initial proof methods, but only as terminal ones, solving certain
14.190 +  goals completely.  *}
14.191
14.192  end