# HG changeset patch
# User wenzelm
# Date 1245707304 -7200
# Node ID 3edd5f813f01c8a82f86f16847e5d7ecfdff1799
# Parent  c1262feb61c7600a713641844812068ad2277b34
observe standard theory naming conventions;
modernized headers;

diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/IsaMakefile	Mon Jun 22 23:48:24 2009 +0200
@@ -886,13 +886,13 @@
 
 HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
 
-$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy	\
+$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/Basic_Logic.thy	\
   Isar_examples/Cantor.thy Isar_examples/Drinker.thy			\
-  Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy		\
+  Isar_examples/Expr_Compiler.thy Isar_examples/Fibonacci.thy		\
   Isar_examples/Group.thy Isar_examples/Hoare.thy			\
-  Isar_examples/HoareEx.thy Isar_examples/KnasterTarski.thy		\
-  Isar_examples/MutilatedCheckerboard.thy				\
-  Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy		\
+  Isar_examples/Hoare_Ex.thy Isar_examples/Knaster_Tarski.thy		\
+  Isar_examples/Mutilated_Checkerboard.thy				\
+  Isar_examples/Nested_Datatype.thy Isar_examples/Peirce.thy		\
   Isar_examples/Puzzle.thy Isar_examples/Summation.thy			\
   Isar_examples/ROOT.ML Isar_examples/document/proof.sty		\
   Isar_examples/document/root.bib Isar_examples/document/root.tex	\
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,447 +0,0 @@
-(*  Title:      HOL/Isar_examples/BasicLogic.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Basic propositional and quantifier reasoning.
-*)
-
-header {* Basic logical reasoning *}
-
-theory BasicLogic imports Main begin
-
-
-subsection {* Pure backward reasoning *}
-
-text {*
-  In order to get a first idea of how Isabelle/Isar proof documents
-  may look like, we consider the propositions @{text I}, @{text K},
-  and @{text S}.  The following (rather explicit) proofs should
-  require little extra explanations.
-*}
-
-lemma I: "A --> A"
-proof
-  assume A
-  show A by fact
-qed
-
-lemma K: "A --> B --> A"
-proof
-  assume A
-  show "B --> A"
-  proof
-    show A by fact
-  qed
-qed
-
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
-proof
-  assume "A --> B --> C"
-  show "(A --> B) --> A --> C"
-  proof
-    assume "A --> B"
-    show "A --> C"
-    proof
-      assume A
-      show C
-      proof (rule mp)
-        show "B --> C" by (rule mp) fact+
-        show B by (rule mp) fact+
-      qed
-    qed
-  qed
-qed
-
-text {*
-  Isar provides several ways to fine-tune the reasoning, avoiding
-  excessive detail.  Several abbreviated language elements are
-  available, enabling the writer to express proofs in a more concise
-  way, even without referring to any automated proof tools yet.
-
-  First of all, proof by assumption may be abbreviated as a single
-  dot.
-*}
-
-lemma "A --> A"
-proof
-  assume A
-  show A by fact+
-qed
-
-text {*
-  In fact, concluding any (sub-)proof already involves solving any
-  remaining goals by assumption\footnote{This is not a completely
-  trivial operation, as proof by assumption may involve full
-  higher-order unification.}.  Thus we may skip the rather vacuous
-  body of the above proof as well.
-*}
-
-lemma "A --> A"
-proof
-qed
-
-text {*
-  Note that the \isacommand{proof} command refers to the @{text rule}
-  method (without arguments) by default.  Thus it implicitly applies a
-  single rule, as determined from the syntactic form of the statements
-  involved.  The \isacommand{by} command abbreviates any proof with
-  empty body, so the proof may be further pruned.
-*}
-
-lemma "A --> A"
-  by rule
-
-text {*
-  Proof by a single rule may be abbreviated as double-dot.
-*}
-
-lemma "A --> A" ..
-
-text {*
-  Thus we have arrived at an adequate representation of the proof of a
-  tautology that holds by a single standard rule.\footnote{Apparently,
-  the rule here is implication introduction.}
-*}
-
-text {*
-  Let us also reconsider @{text K}.  Its statement is composed of
-  iterated connectives.  Basic decomposition is by a single rule at a
-  time, which is why our first version above was by nesting two
-  proofs.
-
-  The @{text intro} proof method repeatedly decomposes a goal's
-  conclusion.\footnote{The dual method is @{text elim}, acting on a
-  goal's premises.}
-*}
-
-lemma "A --> B --> A"
-proof (intro impI)
-  assume A
-  show A by fact
-qed
-
-text {*
-  Again, the body may be collapsed.
-*}
-
-lemma "A --> B --> A"
-  by (intro impI)
-
-text {*
-  Just like @{text rule}, the @{text intro} and @{text elim} proof
-  methods pick standard structural rules, in case no explicit
-  arguments are given.  While implicit rules are usually just fine for
-  single rule application, this may go too far with iteration.  Thus
-  in practice, @{text intro} and @{text elim} would be typically
-  restricted to certain structures by giving a few rules only, e.g.\
-  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
-  and universal quantifiers.
-
-  Such well-tuned iterated decomposition of certain structures is the
-  prime application of @{text intro} and @{text elim}.  In contrast,
-  terminal steps that solve a goal completely are usually performed by
-  actual automated proof methods (such as \isacommand{by}~@{text
-  blast}.
-*}
-
-
-subsection {* Variations of backward vs.\ forward reasoning *}
-
-text {*
-  Certainly, any proof may be performed in backward-style only.  On
-  the other hand, small steps of reasoning are often more naturally
-  expressed in forward-style.  Isar supports both backward and forward
-  reasoning as a first-class concept.  In order to demonstrate the
-  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
-
-  The first version is purely backward.
-*}
-
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  show "B & A"
-  proof
-    show B by (rule conjunct2) fact
-    show A by (rule conjunct1) fact
-  qed
-qed
-
-text {*
-  Above, the @{text "conjunct_1/2"} projection rules had to be named
-  explicitly, since the goals @{text B} and @{text A} did not provide
-  any structural clue.  This may be avoided using \isacommand{from} to
-  focus on the @{text "A \<and> B"} assumption as the current facts,
-  enabling the use of double-dot proofs.  Note that \isacommand{from}
-  already does forward-chaining, involving the \name{conjE} rule here.
-*}
-
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  show "B & A"
-  proof
-    from `A & B` show B ..
-    from `A & B` show A ..
-  qed
-qed
-
-text {*
-  In the next version, we move the forward step one level upwards.
-  Forward-chaining from the most recent facts is indicated by the
-  \isacommand{then} command.  Thus the proof of @{text "B \<and> A"} from
-  @{text "A \<and> B"} actually becomes an elimination, rather than an
-  introduction.  The resulting proof structure directly corresponds to
-  that of the @{text conjE} rule, including the repeated goal
-  proposition that is abbreviated as @{text ?thesis} below.
-*}
-
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  then show "B & A"
-  proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
-    assume B A
-    then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
-  qed
-qed
-
-text {*
-  In the subsequent version we flatten the structure of the main body
-  by doing forward reasoning all the time.  Only the outermost
-  decomposition step is left as backward.
-*}
-
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  from `A & B` have A ..
-  from `A & B` have B ..
-  from `B` `A` show "B & A" ..
-qed
-
-text {*
-  We can still push forward-reasoning a bit further, even at the risk
-  of getting ridiculous.  Note that we force the initial proof step to
-  do nothing here, by referring to the ``-'' proof method.
-*}
-
-lemma "A & B --> B & A"
-proof -
-  {
-    assume "A & B"
-    from `A & B` have A ..
-    from `A & B` have B ..
-    from `B` `A` have "B & A" ..
-  }
-  then show ?thesis ..         -- {* rule \name{impI} *}
-qed
-
-text {*
-  \medskip With these examples we have shifted through a whole range
-  from purely backward to purely forward reasoning.  Apparently, in
-  the extreme ends we get slightly ill-structured proofs, which also
-  require much explicit naming of either rules (backward) or local
-  facts (forward).
-
-  The general lesson learned here is that good proof style would
-  achieve just the \emph{right} balance of top-down backward
-  decomposition, and bottom-up forward composition.  In general, there
-  is no single best way to arrange some pieces of formal reasoning, of
-  course.  Depending on the actual applications, the intended audience
-  etc., rules (and methods) on the one hand vs.\ facts on the other
-  hand have to be emphasized in an appropriate way.  This requires the
-  proof writer to develop good taste, and some practice, of course.
-*}
-
-text {*
-  For our example the most appropriate way of reasoning is probably
-  the middle one, with conjunction introduction done after
-  elimination.
-*}
-
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  then show "B & A"
-  proof
-    assume B A
-    then show ?thesis ..
-  qed
-qed
-
-
-
-subsection {* A few examples from ``Introduction to Isabelle'' *}
-
-text {*
-  We rephrase some of the basic reasoning examples of
-  \cite{isabelle-intro}, using HOL rather than FOL.
-*}
-
-subsubsection {* A propositional proof *}
-
-text {*
-  We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof below
-  involves forward-chaining from @{text "P \<or> P"}, followed by an
-  explicit case-analysis on the two \emph{identical} cases.
-*}
-
-lemma "P | P --> P"
-proof
-  assume "P | P"
-  then show P
-  proof                    -- {*
-    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
-  *}
-    assume P show P by fact
-  next
-    assume P show P by fact
-  qed
-qed
-
-text {*
-  Case splits are \emph{not} hardwired into the Isar language as a
-  special feature.  The \isacommand{next} command used to separate the
-  cases above is just a short form of managing block structure.
-
-  \medskip In general, applying proof methods may split up a goal into
-  separate ``cases'', i.e.\ new subgoals with individual local
-  assumptions.  The corresponding proof text typically mimics this by
-  establishing results in appropriate contexts, separated by blocks.
-
-  In order to avoid too much explicit parentheses, the Isar system
-  implicitly opens an additional block for any new goal, the
-  \isacommand{next} statement then closes one block level, opening a
-  new one.  The resulting behavior is what one would expect from
-  separating cases, only that it is more flexible.  E.g.\ an induction
-  base case (which does not introduce local assumptions) would
-  \emph{not} require \isacommand{next} to separate the subsequent step
-  case.
-
-  \medskip In our example the situation is even simpler, since the two
-  cases actually coincide.  Consequently the proof may be rephrased as
-  follows.
-*}
-
-lemma "P | P --> P"
-proof
-  assume "P | P"
-  then show P
-  proof
-    assume P
-    show P by fact
-    show P by fact
-  qed
-qed
-
-text {*
-  Again, the rather vacuous body of the proof may be collapsed.  Thus
-  the case analysis degenerates into two assumption steps, which are
-  implicitly performed when concluding the single rule step of the
-  double-dot proof as follows.
-*}
-
-lemma "P | P --> P"
-proof
-  assume "P | P"
-  then show P ..
-qed
-
-
-subsubsection {* A quantifier proof *}
-
-text {*
-  To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
-  x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any @{text a}
-  with @{text "P (f a)"} may be taken as a witness for the second
-  existential statement.
-
-  The first proof is rather verbose, exhibiting quite a lot of
-  (redundant) detail.  It gives explicit rules, even with some
-  instantiation.  Furthermore, we encounter two new language elements:
-  the \isacommand{fix} command augments the context by some new
-  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
-  binds term abbreviations by higher-order pattern matching.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
-  proof (rule exE)             -- {*
-    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
-  *}
-    fix a
-    assume "P (f a)" (is "P ?witness")
-    then show ?thesis by (rule exI [of P ?witness])
-  qed
-qed
-
-text {*
-  While explicit rule instantiation may occasionally improve
-  readability of certain aspects of reasoning, it is usually quite
-  redundant.  Above, the basic proof outline gives already enough
-  structural clues for the system to infer both the rules and their
-  instances (by higher-order unification).  Thus we may as well prune
-  the text as follows.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
-  proof
-    fix a
-    assume "P (f a)"
-    then show ?thesis ..
-  qed
-qed
-
-text {*
-  Explicit @{text \<exists>}-elimination as seen above can become quite
-  cumbersome in practice.  The derived Isar language element
-  ``\isakeyword{obtain}'' provides a more handsome way to do
-  generalized existence reasoning.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
-  then obtain a where "P (f a)" ..
-  then show "EX y. P y" ..
-qed
-
-text {*
-  Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
-  \isakeyword{assume} together with a soundness proof of the
-  elimination involved.  Thus it behaves similar to any other forward
-  proof element.  Also note that due to the nature of general
-  existence reasoning involved here, any result exported from the
-  context of an \isakeyword{obtain} statement may \emph{not} refer to
-  the parameters introduced there.
-*}
-
-
-
-subsubsection {* Deriving rules in Isabelle *}
-
-text {*
-  We derive the conjunction elimination rule from the corresponding
-  projections.  The proof is quite straight-forward, since
-  Isabelle/Isar supports non-atomic goals and assumptions fully
-  transparently.
-*}
-
-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
-proof -
-  assume "A & B"
-  assume r: "A ==> B ==> C"
-  show C
-  proof (rule r)
-    show A by (rule conjunct1) fact
-    show B by (rule conjunct2) fact
-  qed
-qed
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Basic_Logic.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Basic_Logic.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,448 @@
+(*  Title:      HOL/Isar_examples/Basic_Logic.thy
+    Author:     Markus Wenzel, TU Muenchen
+
+Basic propositional and quantifier reasoning.
+*)
+
+header {* Basic logical reasoning *}
+
+theory Basic_Logic
+imports Main
+begin
+
+
+subsection {* Pure backward reasoning *}
+
+text {*
+  In order to get a first idea of how Isabelle/Isar proof documents
+  may look like, we consider the propositions @{text I}, @{text K},
+  and @{text S}.  The following (rather explicit) proofs should
+  require little extra explanations.
+*}
+
+lemma I: "A --> A"
+proof
+  assume A
+  show A by fact
+qed
+
+lemma K: "A --> B --> A"
+proof
+  assume A
+  show "B --> A"
+  proof
+    show A by fact
+  qed
+qed
+
+lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
+proof
+  assume "A --> B --> C"
+  show "(A --> B) --> A --> C"
+  proof
+    assume "A --> B"
+    show "A --> C"
+    proof
+      assume A
+      show C
+      proof (rule mp)
+        show "B --> C" by (rule mp) fact+
+        show B by (rule mp) fact+
+      qed
+    qed
+  qed
+qed
+
+text {*
+  Isar provides several ways to fine-tune the reasoning, avoiding
+  excessive detail.  Several abbreviated language elements are
+  available, enabling the writer to express proofs in a more concise
+  way, even without referring to any automated proof tools yet.
+
+  First of all, proof by assumption may be abbreviated as a single
+  dot.
+*}
+
+lemma "A --> A"
+proof
+  assume A
+  show A by fact+
+qed
+
+text {*
+  In fact, concluding any (sub-)proof already involves solving any
+  remaining goals by assumption\footnote{This is not a completely
+  trivial operation, as proof by assumption may involve full
+  higher-order unification.}.  Thus we may skip the rather vacuous
+  body of the above proof as well.
+*}
+
+lemma "A --> A"
+proof
+qed
+
+text {*
+  Note that the \isacommand{proof} command refers to the @{text rule}
+  method (without arguments) by default.  Thus it implicitly applies a
+  single rule, as determined from the syntactic form of the statements
+  involved.  The \isacommand{by} command abbreviates any proof with
+  empty body, so the proof may be further pruned.
+*}
+
+lemma "A --> A"
+  by rule
+
+text {*
+  Proof by a single rule may be abbreviated as double-dot.
+*}
+
+lemma "A --> A" ..
+
+text {*
+  Thus we have arrived at an adequate representation of the proof of a
+  tautology that holds by a single standard rule.\footnote{Apparently,
+  the rule here is implication introduction.}
+*}
+
+text {*
+  Let us also reconsider @{text K}.  Its statement is composed of
+  iterated connectives.  Basic decomposition is by a single rule at a
+  time, which is why our first version above was by nesting two
+  proofs.
+
+  The @{text intro} proof method repeatedly decomposes a goal's
+  conclusion.\footnote{The dual method is @{text elim}, acting on a
+  goal's premises.}
+*}
+
+lemma "A --> B --> A"
+proof (intro impI)
+  assume A
+  show A by fact
+qed
+
+text {*
+  Again, the body may be collapsed.
+*}
+
+lemma "A --> B --> A"
+  by (intro impI)
+
+text {*
+  Just like @{text rule}, the @{text intro} and @{text elim} proof
+  methods pick standard structural rules, in case no explicit
+  arguments are given.  While implicit rules are usually just fine for
+  single rule application, this may go too far with iteration.  Thus
+  in practice, @{text intro} and @{text elim} would be typically
+  restricted to certain structures by giving a few rules only, e.g.\
+  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
+  and universal quantifiers.
+
+  Such well-tuned iterated decomposition of certain structures is the
+  prime application of @{text intro} and @{text elim}.  In contrast,
+  terminal steps that solve a goal completely are usually performed by
+  actual automated proof methods (such as \isacommand{by}~@{text
+  blast}.
+*}
+
+
+subsection {* Variations of backward vs.\ forward reasoning *}
+
+text {*
+  Certainly, any proof may be performed in backward-style only.  On
+  the other hand, small steps of reasoning are often more naturally
+  expressed in forward-style.  Isar supports both backward and forward
+  reasoning as a first-class concept.  In order to demonstrate the
+  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
+
+  The first version is purely backward.
+*}
+
+lemma "A & B --> B & A"
+proof
+  assume "A & B"
+  show "B & A"
+  proof
+    show B by (rule conjunct2) fact
+    show A by (rule conjunct1) fact
+  qed
+qed
+
+text {*
+  Above, the @{text "conjunct_1/2"} projection rules had to be named
+  explicitly, since the goals @{text B} and @{text A} did not provide
+  any structural clue.  This may be avoided using \isacommand{from} to
+  focus on the @{text "A \<and> B"} assumption as the current facts,
+  enabling the use of double-dot proofs.  Note that \isacommand{from}
+  already does forward-chaining, involving the \name{conjE} rule here.
+*}
+
+lemma "A & B --> B & A"
+proof
+  assume "A & B"
+  show "B & A"
+  proof
+    from `A & B` show B ..
+    from `A & B` show A ..
+  qed
+qed
+
+text {*
+  In the next version, we move the forward step one level upwards.
+  Forward-chaining from the most recent facts is indicated by the
+  \isacommand{then} command.  Thus the proof of @{text "B \<and> A"} from
+  @{text "A \<and> B"} actually becomes an elimination, rather than an
+  introduction.  The resulting proof structure directly corresponds to
+  that of the @{text conjE} rule, including the repeated goal
+  proposition that is abbreviated as @{text ?thesis} below.
+*}
+
+lemma "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
+    assume B A
+    then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
+  qed
+qed
+
+text {*
+  In the subsequent version we flatten the structure of the main body
+  by doing forward reasoning all the time.  Only the outermost
+  decomposition step is left as backward.
+*}
+
+lemma "A & B --> B & A"
+proof
+  assume "A & B"
+  from `A & B` have A ..
+  from `A & B` have B ..
+  from `B` `A` show "B & A" ..
+qed
+
+text {*
+  We can still push forward-reasoning a bit further, even at the risk
+  of getting ridiculous.  Note that we force the initial proof step to
+  do nothing here, by referring to the ``-'' proof method.
+*}
+
+lemma "A & B --> B & A"
+proof -
+  {
+    assume "A & B"
+    from `A & B` have A ..
+    from `A & B` have B ..
+    from `B` `A` have "B & A" ..
+  }
+  then show ?thesis ..         -- {* rule \name{impI} *}
+qed
+
+text {*
+  \medskip With these examples we have shifted through a whole range
+  from purely backward to purely forward reasoning.  Apparently, in
+  the extreme ends we get slightly ill-structured proofs, which also
+  require much explicit naming of either rules (backward) or local
+  facts (forward).
+
+  The general lesson learned here is that good proof style would
+  achieve just the \emph{right} balance of top-down backward
+  decomposition, and bottom-up forward composition.  In general, there
+  is no single best way to arrange some pieces of formal reasoning, of
+  course.  Depending on the actual applications, the intended audience
+  etc., rules (and methods) on the one hand vs.\ facts on the other
+  hand have to be emphasized in an appropriate way.  This requires the
+  proof writer to develop good taste, and some practice, of course.
+*}
+
+text {*
+  For our example the most appropriate way of reasoning is probably
+  the middle one, with conjunction introduction done after
+  elimination.
+*}
+
+lemma "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B A
+    then show ?thesis ..
+  qed
+qed
+
+
+
+subsection {* A few examples from ``Introduction to Isabelle'' *}
+
+text {*
+  We rephrase some of the basic reasoning examples of
+  \cite{isabelle-intro}, using HOL rather than FOL.
+*}
+
+subsubsection {* A propositional proof *}
+
+text {*
+  We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof below
+  involves forward-chaining from @{text "P \<or> P"}, followed by an
+  explicit case-analysis on the two \emph{identical} cases.
+*}
+
+lemma "P | P --> P"
+proof
+  assume "P | P"
+  then show P
+  proof                    -- {*
+    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
+  *}
+    assume P show P by fact
+  next
+    assume P show P by fact
+  qed
+qed
+
+text {*
+  Case splits are \emph{not} hardwired into the Isar language as a
+  special feature.  The \isacommand{next} command used to separate the
+  cases above is just a short form of managing block structure.
+
+  \medskip In general, applying proof methods may split up a goal into
+  separate ``cases'', i.e.\ new subgoals with individual local
+  assumptions.  The corresponding proof text typically mimics this by
+  establishing results in appropriate contexts, separated by blocks.
+
+  In order to avoid too much explicit parentheses, the Isar system
+  implicitly opens an additional block for any new goal, the
+  \isacommand{next} statement then closes one block level, opening a
+  new one.  The resulting behavior is what one would expect from
+  separating cases, only that it is more flexible.  E.g.\ an induction
+  base case (which does not introduce local assumptions) would
+  \emph{not} require \isacommand{next} to separate the subsequent step
+  case.
+
+  \medskip In our example the situation is even simpler, since the two
+  cases actually coincide.  Consequently the proof may be rephrased as
+  follows.
+*}
+
+lemma "P | P --> P"
+proof
+  assume "P | P"
+  then show P
+  proof
+    assume P
+    show P by fact
+    show P by fact
+  qed
+qed
+
+text {*
+  Again, the rather vacuous body of the proof may be collapsed.  Thus
+  the case analysis degenerates into two assumption steps, which are
+  implicitly performed when concluding the single rule step of the
+  double-dot proof as follows.
+*}
+
+lemma "P | P --> P"
+proof
+  assume "P | P"
+  then show P ..
+qed
+
+
+subsubsection {* A quantifier proof *}
+
+text {*
+  To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
+  x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any @{text a}
+  with @{text "P (f a)"} may be taken as a witness for the second
+  existential statement.
+
+  The first proof is rather verbose, exhibiting quite a lot of
+  (redundant) detail.  It gives explicit rules, even with some
+  instantiation.  Furthermore, we encounter two new language elements:
+  the \isacommand{fix} command augments the context by some new
+  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
+  binds term abbreviations by higher-order pattern matching.
+*}
+
+lemma "(EX x. P (f x)) --> (EX y. P y)"
+proof
+  assume "EX x. P (f x)"
+  then show "EX y. P y"
+  proof (rule exE)             -- {*
+    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
+  *}
+    fix a
+    assume "P (f a)" (is "P ?witness")
+    then show ?thesis by (rule exI [of P ?witness])
+  qed
+qed
+
+text {*
+  While explicit rule instantiation may occasionally improve
+  readability of certain aspects of reasoning, it is usually quite
+  redundant.  Above, the basic proof outline gives already enough
+  structural clues for the system to infer both the rules and their
+  instances (by higher-order unification).  Thus we may as well prune
+  the text as follows.
+*}
+
+lemma "(EX x. P (f x)) --> (EX y. P y)"
+proof
+  assume "EX x. P (f x)"
+  then show "EX y. P y"
+  proof
+    fix a
+    assume "P (f a)"
+    then show ?thesis ..
+  qed
+qed
+
+text {*
+  Explicit @{text \<exists>}-elimination as seen above can become quite
+  cumbersome in practice.  The derived Isar language element
+  ``\isakeyword{obtain}'' provides a more handsome way to do
+  generalized existence reasoning.
+*}
+
+lemma "(EX x. P (f x)) --> (EX y. P y)"
+proof
+  assume "EX x. P (f x)"
+  then obtain a where "P (f a)" ..
+  then show "EX y. P y" ..
+qed
+
+text {*
+  Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
+  \isakeyword{assume} together with a soundness proof of the
+  elimination involved.  Thus it behaves similar to any other forward
+  proof element.  Also note that due to the nature of general
+  existence reasoning involved here, any result exported from the
+  context of an \isakeyword{obtain} statement may \emph{not} refer to
+  the parameters introduced there.
+*}
+
+
+
+subsubsection {* Deriving rules in Isabelle *}
+
+text {*
+  We derive the conjunction elimination rule from the corresponding
+  projections.  The proof is quite straight-forward, since
+  Isabelle/Isar supports non-atomic goals and assumptions fully
+  transparently.
+*}
+
+theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
+proof -
+  assume "A & B"
+  assume r: "A ==> B ==> C"
+  show C
+  proof (rule r)
+    show A by (rule conjunct1) fact
+    show B by (rule conjunct2) fact
+  qed
+qed
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Isar_examples/Cantor.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Cantor's Theorem *}
 
-theory Cantor imports Main begin
+theory Cantor
+imports Main
+begin
 
 text_raw {*
   \footnote{This is an Isar version of the final example of the
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Drinker.thy
--- a/src/HOL/Isar_examples/Drinker.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Drinker.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Isar_examples/Drinker.thy
-    ID:         $Id$
     Author:     Makarius
 *)
 
 header {* The Drinker's Principle *}
 
-theory Drinker imports Main begin
+theory Drinker
+imports Main
+begin
 
 text {*
   Here is another example of classical reasoning: the Drinker's
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(*  Title:      HOL/Isar_examples/ExprCompiler.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Correctness of a simple expression/stack-machine compiler.
-*)
-
-header {* Correctness of a simple expression compiler *}
-
-theory ExprCompiler imports Main begin
-
-text {*
- This is a (rather trivial) example of program verification.  We model
- a compiler for translating expressions to stack machine instructions,
- and prove its correctness wrt.\ some evaluation semantics.
-*}
-
-
-subsection {* Binary operations *}
-
-text {*
- Binary operations are just functions over some type of values.  This
- is both for abstract syntax and semantics, i.e.\ we use a ``shallow
- embedding'' here.
-*}
-
-types
-  'val binop = "'val => 'val => 'val"
-
-
-subsection {* Expressions *}
-
-text {*
- The language of expressions is defined as an inductive type,
- consisting of variables, constants, and binary operations on
- expressions.
-*}
-
-datatype ('adr, 'val) expr =
-  Variable 'adr |
-  Constant 'val |
-  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
-
-text {*
- Evaluation (wrt.\ some environment of variable assignments) is
- defined by primitive recursion over the structure of expressions.
-*}
-
-consts
-  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
-
-primrec
-  "eval (Variable x) env = env x"
-  "eval (Constant c) env = c"
-  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
-
-
-subsection {* Machine *}
-
-text {*
- Next we model a simple stack machine, with three instructions.
-*}
-
-datatype ('adr, 'val) instr =
-  Const 'val |
-  Load 'adr |
-  Apply "'val binop"
-
-text {*
- Execution of a list of stack machine instructions is easily defined
- as follows.
-*}
-
-consts
-  exec :: "(('adr, 'val) instr) list
-    => 'val list => ('adr => 'val) => 'val list"
-
-primrec
-  "exec [] stack env = stack"
-  "exec (instr # instrs) stack env =
-    (case instr of
-      Const c => exec instrs (c # stack) env
-    | Load x => exec instrs (env x # stack) env
-    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
-                   # (tl (tl stack))) env)"
-
-constdefs
-  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
-  "execute instrs env == hd (exec instrs [] env)"
-
-
-subsection {* Compiler *}
-
-text {*
- We are ready to define the compilation function of expressions to
- lists of stack machine instructions.
-*}
-
-consts
-  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
-
-primrec
-  "compile (Variable x) = [Load x]"
-  "compile (Constant c) = [Const c]"
-  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
-
-
-text {*
- The main result of this development is the correctness theorem for
- $\idt{compile}$.  We first establish a lemma about $\idt{exec}$ and
- list append.
-*}
-
-lemma exec_append:
-  "exec (xs @ ys) stack env =
-    exec ys (exec xs stack env) env"
-proof (induct xs arbitrary: stack)
-  case Nil
-  show ?case by simp
-next
-  case (Cons x xs)
-  show ?case
-  proof (induct x)
-    case Const
-    from Cons show ?case by simp
-  next
-    case Load
-    from Cons show ?case by simp
-  next
-    case Apply
-    from Cons show ?case by simp
-  qed
-qed
-
-theorem correctness: "execute (compile e) env = eval e env"
-proof -
-  have "\<And>stack. exec (compile e) stack env = eval e env # stack"
-  proof (induct e)
-    case Variable show ?case by simp
-  next
-    case Constant show ?case by simp
-  next
-    case Binop then show ?case by (simp add: exec_append)
-  qed
-  then show ?thesis by (simp add: execute_def)
-qed
-
-
-text {*
- \bigskip In the proofs above, the \name{simp} method does quite a lot
- of work behind the scenes (mostly ``functional program execution'').
- Subsequently, the same reasoning is elaborated in detail --- at most
- one recursive function definition is used at a time.  Thus we get a
- better idea of what is actually going on.
-*}
-
-lemma exec_append':
-  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
-proof (induct xs arbitrary: stack)
-  case (Nil s)
-  have "exec ([] @ ys) s env = exec ys s env" by simp
-  also have "... = exec ys (exec [] s env) env" by simp
-  finally show ?case .
-next
-  case (Cons x xs s)
-  show ?case
-  proof (induct x)
-    case (Const val)
-    have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
-      by simp
-    also have "... = exec (xs @ ys) (val # s) env" by simp
-    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
-    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
-    finally show ?case .
-  next
-    case (Load adr)
-    from Cons show ?case by simp -- {* same as above *}
-  next
-    case (Apply fn)
-    have "exec ((Apply fn # xs) @ ys) s env =
-        exec (Apply fn # xs @ ys) s env" by simp
-    also have "... =
-        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
-    also from Cons have "... =
-        exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
-    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
-    finally show ?case .
-  qed
-qed
-
-theorem correctness': "execute (compile e) env = eval e env"
-proof -
-  have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
-  proof (induct e)
-    case (Variable adr s)
-    have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
-      by simp
-    also have "... = env adr # s" by simp
-    also have "env adr = eval (Variable adr) env" by simp
-    finally show ?case .
-  next
-    case (Constant val s)
-    show ?case by simp -- {* same as above *}
-  next
-    case (Binop fn e1 e2 s)
-    have "exec (compile (Binop fn e1 e2)) s env =
-        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
-    also have "... = exec [Apply fn]
-        (exec (compile e1) (exec (compile e2) s env) env) env"
-      by (simp only: exec_append)
-    also have "exec (compile e2) s env = eval e2 env # s" by fact
-    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
-    also have "exec [Apply fn] ... env =
-        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
-    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
-    also have "fn (eval e1 env) (eval e2 env) =
-        eval (Binop fn e1 e2) env"
-      by simp
-    finally show ?case .
-  qed
-
-  have "execute (compile e) env = hd (exec (compile e) [] env)"
-    by (simp add: execute_def)
-  also from exec_compile
-    have "exec (compile e) [] env = [eval e env]" .
-  also have "hd ... = eval e env" by simp
-  finally show ?thesis .
-qed
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Expr_Compiler.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Expr_Compiler.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,231 @@
+(*  Title:      HOL/Isar_examples/Expr_Compiler.thy
+    Author:     Markus Wenzel, TU Muenchen
+
+Correctness of a simple expression/stack-machine compiler.
+*)
+
+header {* Correctness of a simple expression compiler *}
+
+theory Expr_Compiler
+imports Main
+begin
+
+text {*
+ This is a (rather trivial) example of program verification.  We model
+ a compiler for translating expressions to stack machine instructions,
+ and prove its correctness wrt.\ some evaluation semantics.
+*}
+
+
+subsection {* Binary operations *}
+
+text {*
+ Binary operations are just functions over some type of values.  This
+ is both for abstract syntax and semantics, i.e.\ we use a ``shallow
+ embedding'' here.
+*}
+
+types
+  'val binop = "'val => 'val => 'val"
+
+
+subsection {* Expressions *}
+
+text {*
+ The language of expressions is defined as an inductive type,
+ consisting of variables, constants, and binary operations on
+ expressions.
+*}
+
+datatype ('adr, 'val) expr =
+  Variable 'adr |
+  Constant 'val |
+  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
+
+text {*
+ Evaluation (wrt.\ some environment of variable assignments) is
+ defined by primitive recursion over the structure of expressions.
+*}
+
+consts
+  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
+
+primrec
+  "eval (Variable x) env = env x"
+  "eval (Constant c) env = c"
+  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+
+
+subsection {* Machine *}
+
+text {*
+ Next we model a simple stack machine, with three instructions.
+*}
+
+datatype ('adr, 'val) instr =
+  Const 'val |
+  Load 'adr |
+  Apply "'val binop"
+
+text {*
+ Execution of a list of stack machine instructions is easily defined
+ as follows.
+*}
+
+consts
+  exec :: "(('adr, 'val) instr) list
+    => 'val list => ('adr => 'val) => 'val list"
+
+primrec
+  "exec [] stack env = stack"
+  "exec (instr # instrs) stack env =
+    (case instr of
+      Const c => exec instrs (c # stack) env
+    | Load x => exec instrs (env x # stack) env
+    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
+                   # (tl (tl stack))) env)"
+
+constdefs
+  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+  "execute instrs env == hd (exec instrs [] env)"
+
+
+subsection {* Compiler *}
+
+text {*
+ We are ready to define the compilation function of expressions to
+ lists of stack machine instructions.
+*}
+
+consts
+  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+
+primrec
+  "compile (Variable x) = [Load x]"
+  "compile (Constant c) = [Const c]"
+  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+
+
+text {*
+ The main result of this development is the correctness theorem for
+ $\idt{compile}$.  We first establish a lemma about $\idt{exec}$ and
+ list append.
+*}
+
+lemma exec_append:
+  "exec (xs @ ys) stack env =
+    exec ys (exec xs stack env) env"
+proof (induct xs arbitrary: stack)
+  case Nil
+  show ?case by simp
+next
+  case (Cons x xs)
+  show ?case
+  proof (induct x)
+    case Const
+    from Cons show ?case by simp
+  next
+    case Load
+    from Cons show ?case by simp
+  next
+    case Apply
+    from Cons show ?case by simp
+  qed
+qed
+
+theorem correctness: "execute (compile e) env = eval e env"
+proof -
+  have "\<And>stack. exec (compile e) stack env = eval e env # stack"
+  proof (induct e)
+    case Variable show ?case by simp
+  next
+    case Constant show ?case by simp
+  next
+    case Binop then show ?case by (simp add: exec_append)
+  qed
+  then show ?thesis by (simp add: execute_def)
+qed
+
+
+text {*
+ \bigskip In the proofs above, the \name{simp} method does quite a lot
+ of work behind the scenes (mostly ``functional program execution'').
+ Subsequently, the same reasoning is elaborated in detail --- at most
+ one recursive function definition is used at a time.  Thus we get a
+ better idea of what is actually going on.
+*}
+
+lemma exec_append':
+  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
+proof (induct xs arbitrary: stack)
+  case (Nil s)
+  have "exec ([] @ ys) s env = exec ys s env" by simp
+  also have "... = exec ys (exec [] s env) env" by simp
+  finally show ?case .
+next
+  case (Cons x xs s)
+  show ?case
+  proof (induct x)
+    case (Const val)
+    have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
+      by simp
+    also have "... = exec (xs @ ys) (val # s) env" by simp
+    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
+    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
+    finally show ?case .
+  next
+    case (Load adr)
+    from Cons show ?case by simp -- {* same as above *}
+  next
+    case (Apply fn)
+    have "exec ((Apply fn # xs) @ ys) s env =
+        exec (Apply fn # xs @ ys) s env" by simp
+    also have "... =
+        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
+    also from Cons have "... =
+        exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
+    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
+    finally show ?case .
+  qed
+qed
+
+theorem correctness': "execute (compile e) env = eval e env"
+proof -
+  have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
+  proof (induct e)
+    case (Variable adr s)
+    have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
+      by simp
+    also have "... = env adr # s" by simp
+    also have "env adr = eval (Variable adr) env" by simp
+    finally show ?case .
+  next
+    case (Constant val s)
+    show ?case by simp -- {* same as above *}
+  next
+    case (Binop fn e1 e2 s)
+    have "exec (compile (Binop fn e1 e2)) s env =
+        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
+    also have "... = exec [Apply fn]
+        (exec (compile e1) (exec (compile e2) s env) env) env"
+      by (simp only: exec_append)
+    also have "exec (compile e2) s env = eval e2 env # s" by fact
+    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
+    also have "exec [Apply fn] ... env =
+        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
+    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
+    also have "fn (eval e1 env) (eval e2 env) =
+        eval (Binop fn e1 e2) env"
+      by simp
+    finally show ?case .
+  qed
+
+  have "execute (compile e) env = hd (exec (compile e) [] env)"
+    by (simp add: execute_def)
+  also from exec_compile
+    have "exec (compile e) [] env = [eval e env]" .
+  also have "hd ... = eval e env" by simp
+  finally show ?thesis .
+qed
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Isar_examples/Fibonacci.thy
-    ID:         $Id$
     Author:     Gertrud Bauer
     Copyright   1999 Technische Universitaet Muenchen
 
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Group.thy
--- a/src/HOL/Isar_examples/Group.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Isar_examples/Group.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Basic group theory *}
 
-theory Group imports Main begin
+theory Group
+imports Main
+begin
 
 subsection {* Groups and calculational reasoning *} 
 
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Isar_examples/Hoare.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 A formulation of Hoare logic suitable for Isar.
@@ -7,8 +6,10 @@
 
 header {* Hoare Logic *}
 
-theory Hoare imports Main
-uses ("~~/src/HOL/Hoare/hoare_tac.ML") begin
+theory Hoare
+imports Main
+uses ("~~/src/HOL/Hoare/hoare_tac.ML")
+begin
 
 subsection {* Abstract syntax and semantics *}
 
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,328 +0,0 @@
-
-header {* Using Hoare Logic *}
-
-theory HoareEx imports Hoare begin
-
-subsection {* State spaces *}
-
-text {*
- First of all we provide a store of program variables that
- occur in any of the programs considered later.  Slightly unexpected
- things may happen when attempting to work with undeclared variables.
-*}
-
-record vars =
-  I :: nat
-  M :: nat
-  N :: nat
-  S :: nat
-
-text {*
- While all of our variables happen to have the same type, nothing
- would prevent us from working with many-sorted programs as well, or
- even polymorphic ones.  Also note that Isabelle/HOL's extensible
- record types even provides simple means to extend the state space
- later.
-*}
-
-
-subsection {* Basic examples *}
-
-text {*
- We look at few trivialities involving assignment and sequential
- composition, in order to get an idea of how to work with our
- formulation of Hoare Logic.
-*}
-
-text {*
- Using the basic \name{assign} rule directly is a bit cumbersome.
-*}
-
-lemma
-  "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
-  by (rule assign)
-
-text {*
- Certainly we want the state modification already done, e.g.\ by
- simplification.  The \name{hoare} method performs the basic state
- update for us; we may apply the Simplifier afterwards to achieve
- ``obvious'' consequences as well.
-*}
-
-lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
-  by hoare
-
-lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
-  by hoare
-
-lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
-  by hoare simp
-
-lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
-  by hoare
-
-lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
-  by hoare simp
-
-lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
-  by hoare
-
-lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
-  by hoare simp
-
-lemma
-"|- .{\<acute>M = a & \<acute>N = b}.
-    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
-    .{\<acute>M = b & \<acute>N = a}."
-  by hoare simp
-
-text {*
- It is important to note that statements like the following one can
- only be proven for each individual program variable.  Due to the
- extra-logical nature of record fields, we cannot formulate a theorem
- relating record selectors and updates schematically.
-*}
-
-lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
-  by hoare
-
-lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
-  oops
-
-lemma
-  "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
-  -- {* same statement without concrete syntax *}
-  oops
-
-
-text {*
- In the following assignments we make use of the consequence rule in
- order to achieve the intended precondition.  Certainly, the
- \name{hoare} method is able to handle this case, too.
-*}
-
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
-proof -
-  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
-    by auto
-  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
-    by hoare
-  finally show ?thesis .
-qed
-
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
-proof -
-  have "!!m n::nat. m = n --> m + 1 ~= n"
-      -- {* inclusion of assertions expressed in ``pure'' logic, *}
-      -- {* without mentioning the state space *}
-    by simp
-  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
-    by hoare
-  finally show ?thesis .
-qed
-
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
-  by hoare simp
-
-
-subsection {* Multiplication by addition *}
-
-text {*
- We now do some basic examples of actual \texttt{WHILE} programs.
- This one is a loop for calculating the product of two natural
- numbers, by iterated addition.  We first give detailed structured
- proof based on single-step Hoare rules.
-*}
-
-lemma
-  "|- .{\<acute>M = 0 & \<acute>S = 0}.
-      WHILE \<acute>M ~= a
-      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
-      .{\<acute>S = a * b}."
-proof -
-  let "|- _ ?while _" = ?thesis
-  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
-
-  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
-  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
-  proof
-    let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
-    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
-      by auto
-    also have "|- ... ?c .{\<acute>?inv}." by hoare
-    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
-  qed
-  also have "... <= .{\<acute>S = a * b}." by auto
-  finally show ?thesis .
-qed
-
-text {*
- The subsequent version of the proof applies the \name{hoare} method
- to reduce the Hoare statement to a purely logical problem that can be
- solved fully automatically.  Note that we have to specify the
- \texttt{WHILE} loop invariant in the original statement.
-*}
-
-lemma
-  "|- .{\<acute>M = 0 & \<acute>S = 0}.
-      WHILE \<acute>M ~= a
-      INV .{\<acute>S = \<acute>M * b}.
-      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
-      .{\<acute>S = a * b}."
-  by hoare auto
-
-
-subsection {* Summing natural numbers *}
-
-text {*
- We verify an imperative program to sum natural numbers up to a given
- limit.  First some functional definition for proper specification of
- the problem.
-*}
-
-text {*
- The following proof is quite explicit in the individual steps taken,
- with the \name{hoare} method only applied locally to take care of
- assignment and sequential composition.  Note that we express
- intermediate proof obligation in pure logic, without referring to the
- state space.
-*}
-
-declare atLeast0LessThan[symmetric,simp]
-
-theorem
-  "|- .{True}.
-      \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
-      DO
-        \<acute>S := \<acute>S + \<acute>I;
-        \<acute>I := \<acute>I + 1
-      OD
-      .{\<acute>S = (SUM j<n. j)}."
-  (is "|- _ (_; ?while) _")
-proof -
-  let ?sum = "\<lambda>k::nat. SUM j<k. j"
-  let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
-  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
-  proof -
-    have "True --> 0 = ?sum 1"
-      by simp
-    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
-      by hoare
-    finally show ?thesis .
-  qed
-  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
-  proof
-    let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
-    have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
-      by simp
-    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
-      by hoare
-    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
-  qed
-  also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
-    by simp
-  finally show ?thesis .
-qed
-
-text {*
- The next version uses the \name{hoare} method, while still explaining
- the resulting proof obligations in an abstract, structured manner.
-*}
-
-theorem
-  "|- .{True}.
-      \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
-      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
-      DO
-        \<acute>S := \<acute>S + \<acute>I;
-        \<acute>I := \<acute>I + 1
-      OD
-      .{\<acute>S = (SUM j<n. j)}."
-proof -
-  let ?sum = "\<lambda>k::nat. SUM j<k. j"
-  let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
-  show ?thesis
-  proof hoare
-    show "?inv 0 1" by simp
-  next
-    fix s i assume "?inv s i & i ~= n"
-    thus "?inv (s + i) (i + 1)" by simp
-  next
-    fix s i assume "?inv s i & ~ i ~= n"
-    thus "s = ?sum n" by simp
-  qed
-qed
-
-text {*
- Certainly, this proof may be done fully automatic as well, provided
- that the invariant is given beforehand.
-*}
-
-theorem
-  "|- .{True}.
-      \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
-      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
-      DO
-        \<acute>S := \<acute>S + \<acute>I;
-        \<acute>I := \<acute>I + 1
-      OD
-      .{\<acute>S = (SUM j<n. j)}."
-  by hoare auto
-
-
-subsection{* Time *}
-
-text{*
-  A simple embedding of time in Hoare logic: function @{text timeit}
-  inserts an extra variable to keep track of the elapsed time.
-*}
-
-record tstate = time :: nat
-
-types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
-
-consts timeit :: "'a time com \<Rightarrow> 'a time com"
-primrec
-  "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
-  "timeit (c1; c2) = (timeit c1; timeit c2)"
-  "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-  "timeit (While b iv c) = While b iv (timeit c)"
-
-record tvars = tstate +
-  I :: nat
-  J :: nat
-
-lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"
-  by (induct n) simp_all
-
-lemma "|- .{i = \<acute>I & \<acute>time = 0}.
- timeit(
- WHILE \<acute>I \<noteq> 0
- INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.
- DO
-   \<acute>J := \<acute>I;
-   WHILE \<acute>J \<noteq> 0
-   INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.
-   DO \<acute>J := \<acute>J - 1 OD;
-   \<acute>I := \<acute>I - 1
- OD
- ) .{2*\<acute>time = i*i + 5*i}."
-  apply simp
-  apply hoare
-      apply simp
-     apply clarsimp
-    apply clarsimp
-   apply arith
-   prefer 2
-   apply clarsimp
-  apply (clarsimp simp: nat_distrib)
-  apply (frule lem)
-  apply arith
-  done
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Hoare_Ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Hoare_Ex.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,329 @@
+header {* Using Hoare Logic *}
+
+theory Hoare_Ex
+imports Hoare
+begin
+
+subsection {* State spaces *}
+
+text {*
+ First of all we provide a store of program variables that
+ occur in any of the programs considered later.  Slightly unexpected
+ things may happen when attempting to work with undeclared variables.
+*}
+
+record vars =
+  I :: nat
+  M :: nat
+  N :: nat
+  S :: nat
+
+text {*
+ While all of our variables happen to have the same type, nothing
+ would prevent us from working with many-sorted programs as well, or
+ even polymorphic ones.  Also note that Isabelle/HOL's extensible
+ record types even provides simple means to extend the state space
+ later.
+*}
+
+
+subsection {* Basic examples *}
+
+text {*
+ We look at few trivialities involving assignment and sequential
+ composition, in order to get an idea of how to work with our
+ formulation of Hoare Logic.
+*}
+
+text {*
+ Using the basic \name{assign} rule directly is a bit cumbersome.
+*}
+
+lemma
+  "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+  by (rule assign)
+
+text {*
+ Certainly we want the state modification already done, e.g.\ by
+ simplification.  The \name{hoare} method performs the basic state
+ update for us; we may apply the Simplifier afterwards to achieve
+ ``obvious'' consequences as well.
+*}
+
+lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
+  by hoare
+
+lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+  by hoare
+
+lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+  by hoare simp
+
+lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
+  by hoare
+
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
+  by hoare simp
+
+lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
+  by hoare
+
+lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
+  by hoare simp
+
+lemma
+"|- .{\<acute>M = a & \<acute>N = b}.
+    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
+    .{\<acute>M = b & \<acute>N = a}."
+  by hoare simp
+
+text {*
+ It is important to note that statements like the following one can
+ only be proven for each individual program variable.  Due to the
+ extra-logical nature of record fields, we cannot formulate a theorem
+ relating record selectors and updates schematically.
+*}
+
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
+  by hoare
+
+lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
+  oops
+
+lemma
+  "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
+  -- {* same statement without concrete syntax *}
+  oops
+
+
+text {*
+ In the following assignments we make use of the consequence rule in
+ order to achieve the intended precondition.  Certainly, the
+ \name{hoare} method is able to handle this case, too.
+*}
+
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+proof -
+  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
+    by auto
+  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+    by hoare
+  finally show ?thesis .
+qed
+
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+proof -
+  have "!!m n::nat. m = n --> m + 1 ~= n"
+      -- {* inclusion of assertions expressed in ``pure'' logic, *}
+      -- {* without mentioning the state space *}
+    by simp
+  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+    by hoare
+  finally show ?thesis .
+qed
+
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+  by hoare simp
+
+
+subsection {* Multiplication by addition *}
+
+text {*
+ We now do some basic examples of actual \texttt{WHILE} programs.
+ This one is a loop for calculating the product of two natural
+ numbers, by iterated addition.  We first give detailed structured
+ proof based on single-step Hoare rules.
+*}
+
+lemma
+  "|- .{\<acute>M = 0 & \<acute>S = 0}.
+      WHILE \<acute>M ~= a
+      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+      .{\<acute>S = a * b}."
+proof -
+  let "|- _ ?while _" = ?thesis
+  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
+
+  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
+  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
+  proof
+    let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
+    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
+      by auto
+    also have "|- ... ?c .{\<acute>?inv}." by hoare
+    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
+  qed
+  also have "... <= .{\<acute>S = a * b}." by auto
+  finally show ?thesis .
+qed
+
+text {*
+ The subsequent version of the proof applies the \name{hoare} method
+ to reduce the Hoare statement to a purely logical problem that can be
+ solved fully automatically.  Note that we have to specify the
+ \texttt{WHILE} loop invariant in the original statement.
+*}
+
+lemma
+  "|- .{\<acute>M = 0 & \<acute>S = 0}.
+      WHILE \<acute>M ~= a
+      INV .{\<acute>S = \<acute>M * b}.
+      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+      .{\<acute>S = a * b}."
+  by hoare auto
+
+
+subsection {* Summing natural numbers *}
+
+text {*
+ We verify an imperative program to sum natural numbers up to a given
+ limit.  First some functional definition for proper specification of
+ the problem.
+*}
+
+text {*
+ The following proof is quite explicit in the individual steps taken,
+ with the \name{hoare} method only applied locally to take care of
+ assignment and sequential composition.  Note that we express
+ intermediate proof obligation in pure logic, without referring to the
+ state space.
+*}
+
+declare atLeast0LessThan[symmetric,simp]
+
+theorem
+  "|- .{True}.
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
+      DO
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
+      OD
+      .{\<acute>S = (SUM j<n. j)}."
+  (is "|- _ (_; ?while) _")
+proof -
+  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?inv = "\<lambda>s i::nat. s = ?sum i"
+
+  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
+  proof -
+    have "True --> 0 = ?sum 1"
+      by simp
+    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
+      by hoare
+    finally show ?thesis .
+  qed
+  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
+  proof
+    let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
+    have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
+      by simp
+    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
+      by hoare
+    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
+  qed
+  also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
+    by simp
+  finally show ?thesis .
+qed
+
+text {*
+ The next version uses the \name{hoare} method, while still explaining
+ the resulting proof obligations in an abstract, structured manner.
+*}
+
+theorem
+  "|- .{True}.
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
+      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
+      DO
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
+      OD
+      .{\<acute>S = (SUM j<n. j)}."
+proof -
+  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?inv = "\<lambda>s i::nat. s = ?sum i"
+
+  show ?thesis
+  proof hoare
+    show "?inv 0 1" by simp
+  next
+    fix s i assume "?inv s i & i ~= n"
+    thus "?inv (s + i) (i + 1)" by simp
+  next
+    fix s i assume "?inv s i & ~ i ~= n"
+    thus "s = ?sum n" by simp
+  qed
+qed
+
+text {*
+ Certainly, this proof may be done fully automatic as well, provided
+ that the invariant is given beforehand.
+*}
+
+theorem
+  "|- .{True}.
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
+      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
+      DO
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
+      OD
+      .{\<acute>S = (SUM j<n. j)}."
+  by hoare auto
+
+
+subsection{* Time *}
+
+text{*
+  A simple embedding of time in Hoare logic: function @{text timeit}
+  inserts an extra variable to keep track of the elapsed time.
+*}
+
+record tstate = time :: nat
+
+types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
+
+consts timeit :: "'a time com \<Rightarrow> 'a time com"
+primrec
+  "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
+  "timeit (c1; c2) = (timeit c1; timeit c2)"
+  "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+  "timeit (While b iv c) = While b iv (timeit c)"
+
+record tvars = tstate +
+  I :: nat
+  J :: nat
+
+lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"
+  by (induct n) simp_all
+
+lemma "|- .{i = \<acute>I & \<acute>time = 0}.
+ timeit(
+ WHILE \<acute>I \<noteq> 0
+ INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.
+ DO
+   \<acute>J := \<acute>I;
+   WHILE \<acute>J \<noteq> 0
+   INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.
+   DO \<acute>J := \<acute>J - 1 OD;
+   \<acute>I := \<acute>I - 1
+ OD
+ ) .{2*\<acute>time = i*i + 5*i}."
+  apply simp
+  apply hoare
+      apply simp
+     apply clarsimp
+    apply clarsimp
+   apply arith
+   prefer 2
+   apply clarsimp
+  apply (clarsimp simp: nat_distrib)
+  apply (frule lem)
+  apply arith
+  done
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(*  Title:      HOL/Isar_examples/KnasterTarski.thy
-    Author:     Markus Wenzel, TU Muenchen
-
-Typical textbook proof example.
-*)
-
-header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
-
-theory KnasterTarski
-imports Main Lattice_Syntax
-begin
-
-
-subsection {* Prose version *}
-
-text {*
-  According to the textbook \cite[pages 93--94]{davey-priestley}, the
-  Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
-  dualized the argument, and tuned the notation a little bit.}
-
-  \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
-  complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
-  Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
-
-  \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
-  \<Sqinter>H"}.  For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
-  "f(a) \<le> f(x) \<le> x"}.  Thus @{text "f(a)"} is a lower bound of @{text
-  H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
-  the reverse one (!) and thereby complete the proof that @{text a} is
-  a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
-  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
-*}
-
-
-subsection {* Formal versions *}
-
-text {*
-  The Isar proof below closely follows the original presentation.
-  Virtually all of the prose narration has been rephrased in terms of
-  formal Isar language elements.  Just as many textbook-style proofs,
-  there is a strong bias towards forward proof, and several bends in
-  the course of reasoning.
-*}
-
-theorem Knaster_Tarski:
-  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
-  assumes "mono f"
-  shows "\<exists>a. f a = a"
-proof
-  let ?H = "{u. f u \<le> u}"
-  let ?a = "\<Sqinter>?H"
-  show "f ?a = ?a"
-  proof -
-    {
-      fix x
-      assume "x \<in> ?H"
-      then have "?a \<le> x" by (rule Inf_lower)
-      with `mono f` have "f ?a \<le> f x" ..
-      also from `x \<in> ?H` have "\<dots> \<le> x" ..
-      finally have "f ?a \<le> x" .
-    }
-    then have "f ?a \<le> ?a" by (rule Inf_greatest)
-    {
-      also presume "\<dots> \<le> f ?a"
-      finally (order_antisym) show ?thesis .
-    }
-    from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
-    then have "f ?a \<in> ?H" ..
-    then show "?a \<le> f ?a" by (rule Inf_lower)
-  qed
-qed
-
-text {*
-  Above we have used several advanced Isar language elements, such as
-  explicit block structure and weak assumptions.  Thus we have
-  mimicked the particular way of reasoning of the original text.
-
-  In the subsequent version the order of reasoning is changed to
-  achieve structured top-down decomposition of the problem at the
-  outer level, while only the inner steps of reasoning are done in a
-  forward manner.  We are certainly more at ease here, requiring only
-  the most basic features of the Isar language.
-*}
-
-theorem Knaster_Tarski':
-  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
-  assumes "mono f"
-  shows "\<exists>a. f a = a"
-proof
-  let ?H = "{u. f u \<le> u}"
-  let ?a = "\<Sqinter>?H"
-  show "f ?a = ?a"
-  proof (rule order_antisym)
-    show "f ?a \<le> ?a"
-    proof (rule Inf_greatest)
-      fix x
-      assume "x \<in> ?H"
-      then have "?a \<le> x" by (rule Inf_lower)
-      with `mono f` have "f ?a \<le> f x" ..
-      also from `x \<in> ?H` have "\<dots> \<le> x" ..
-      finally show "f ?a \<le> x" .
-    qed
-    show "?a \<le> f ?a"
-    proof (rule Inf_lower)
-      from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
-      then show "f ?a \<in> ?H" ..
-    qed
-  qed
-qed
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Knaster_Tarski.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Knaster_Tarski.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,111 @@
+(*  Title:      HOL/Isar_examples/Knaster_Tarski.thy
+    Author:     Markus Wenzel, TU Muenchen
+
+Typical textbook proof example.
+*)
+
+header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
+
+theory Knaster_Tarski
+imports Main Lattice_Syntax
+begin
+
+
+subsection {* Prose version *}
+
+text {*
+  According to the textbook \cite[pages 93--94]{davey-priestley}, the
+  Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
+  dualized the argument, and tuned the notation a little bit.}
+
+  \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
+  complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
+  Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
+
+  \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
+  \<Sqinter>H"}.  For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
+  "f(a) \<le> f(x) \<le> x"}.  Thus @{text "f(a)"} is a lower bound of @{text
+  H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
+  the reverse one (!) and thereby complete the proof that @{text a} is
+  a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
+  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
+*}
+
+
+subsection {* Formal versions *}
+
+text {*
+  The Isar proof below closely follows the original presentation.
+  Virtually all of the prose narration has been rephrased in terms of
+  formal Isar language elements.  Just as many textbook-style proofs,
+  there is a strong bias towards forward proof, and several bends in
+  the course of reasoning.
+*}
+
+theorem Knaster_Tarski:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f"
+  shows "\<exists>a. f a = a"
+proof
+  let ?H = "{u. f u \<le> u}"
+  let ?a = "\<Sqinter>?H"
+  show "f ?a = ?a"
+  proof -
+    {
+      fix x
+      assume "x \<in> ?H"
+      then have "?a \<le> x" by (rule Inf_lower)
+      with `mono f` have "f ?a \<le> f x" ..
+      also from `x \<in> ?H` have "\<dots> \<le> x" ..
+      finally have "f ?a \<le> x" .
+    }
+    then have "f ?a \<le> ?a" by (rule Inf_greatest)
+    {
+      also presume "\<dots> \<le> f ?a"
+      finally (order_antisym) show ?thesis .
+    }
+    from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+    then have "f ?a \<in> ?H" ..
+    then show "?a \<le> f ?a" by (rule Inf_lower)
+  qed
+qed
+
+text {*
+  Above we have used several advanced Isar language elements, such as
+  explicit block structure and weak assumptions.  Thus we have
+  mimicked the particular way of reasoning of the original text.
+
+  In the subsequent version the order of reasoning is changed to
+  achieve structured top-down decomposition of the problem at the
+  outer level, while only the inner steps of reasoning are done in a
+  forward manner.  We are certainly more at ease here, requiring only
+  the most basic features of the Isar language.
+*}
+
+theorem Knaster_Tarski':
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f"
+  shows "\<exists>a. f a = a"
+proof
+  let ?H = "{u. f u \<le> u}"
+  let ?a = "\<Sqinter>?H"
+  show "f ?a = ?a"
+  proof (rule order_antisym)
+    show "f ?a \<le> ?a"
+    proof (rule Inf_greatest)
+      fix x
+      assume "x \<in> ?H"
+      then have "?a \<le> x" by (rule Inf_lower)
+      with `mono f` have "f ?a \<le> f x" ..
+      also from `x \<in> ?H` have "\<dots> \<le> x" ..
+      finally show "f ?a \<le> x" .
+    qed
+    show "?a \<le> f ?a"
+    proof (rule Inf_lower)
+      from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+      then show "f ?a \<in> ?H" ..
+    qed
+  qed
+qed
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,299 +0,0 @@
-(*  Title:      HOL/Isar_examples/MutilatedCheckerboard.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen (Isar document)
-                Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
-*)
-
-header {* The Mutilated Checker Board Problem *}
-
-theory MutilatedCheckerboard imports Main begin
-
-text {*
- The Mutilated Checker Board Problem, formalized inductively.  See
- \cite{paulson-mutilated-board} and
- \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the
- original tactic script version.
-*}
-
-subsection {* Tilings *}
-
-inductive_set
-  tiling :: "'a set set => 'a set set"
-  for A :: "'a set set"
-  where
-    empty: "{} : tiling A"
-  | Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
-
-
-text "The union of two disjoint tilings is a tiling."
-
-lemma tiling_Un:
-  assumes "t : tiling A" and "u : tiling A" and "t Int u = {}"
-  shows "t Un u : tiling A"
-proof -
-  let ?T = "tiling A"
-  from `t : ?T` and `t Int u = {}`
-  show "t Un u : ?T"
-  proof (induct t)
-    case empty
-    with `u : ?T` show "{} Un u : ?T" by simp
-  next
-    case (Un a t)
-    show "(a Un t) Un u : ?T"
-    proof -
-      have "a Un (t Un u) : ?T"
-	using `a : A`
-      proof (rule tiling.Un)
-        from `(a Un t) Int u = {}` have "t Int u = {}" by blast
-        then show "t Un u: ?T" by (rule Un)
-        from `a <= - t` and `(a Un t) Int u = {}`
-	show "a <= - (t Un u)" by blast
-      qed
-      also have "a Un (t Un u) = (a Un t) Un u"
-        by (simp only: Un_assoc)
-      finally show ?thesis .
-    qed
-  qed
-qed
-
-
-subsection {* Basic properties of ``below'' *}
-
-constdefs
-  below :: "nat => nat set"
-  "below n == {i. i < n}"
-
-lemma below_less_iff [iff]: "(i: below k) = (i < k)"
-  by (simp add: below_def)
-
-lemma below_0: "below 0 = {}"
-  by (simp add: below_def)
-
-lemma Sigma_Suc1:
-    "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"
-  by (simp add: below_def less_Suc_eq) blast
-
-lemma Sigma_Suc2:
-    "m = n + 2 ==> A <*> below m =
-      (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
-  by (auto simp add: below_def)
-
-lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
-
-
-subsection {* Basic properties of ``evnodd'' *}
-
-constdefs
-  evnodd :: "(nat * nat) set => nat => (nat * nat) set"
-  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
-
-lemma evnodd_iff:
-    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
-  by (simp add: evnodd_def)
-
-lemma evnodd_subset: "evnodd A b <= A"
-  by (unfold evnodd_def, rule Int_lower1)
-
-lemma evnoddD: "x : evnodd A b ==> x : A"
-  by (rule subsetD, rule evnodd_subset)
-
-lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
-  by (rule finite_subset, rule evnodd_subset)
-
-lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"
-  by (unfold evnodd_def) blast
-
-lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
-  by (unfold evnodd_def) blast
-
-lemma evnodd_empty: "evnodd {} b = {}"
-  by (simp add: evnodd_def)
-
-lemma evnodd_insert: "evnodd (insert (i, j) C) b =
-    (if (i + j) mod 2 = b
-      then insert (i, j) (evnodd C b) else evnodd C b)"
-  by (simp add: evnodd_def) blast
-
-
-subsection {* Dominoes *}
-
-inductive_set
-  domino :: "(nat * nat) set set"
-  where
-    horiz: "{(i, j), (i, j + 1)} : domino"
-  | vertl: "{(i, j), (i + 1, j)} : domino"
-
-lemma dominoes_tile_row:
-  "{i} <*> below (2 * n) : tiling domino"
-  (is "?B n : ?T")
-proof (induct n)
-  case 0
-  show ?case by (simp add: below_0 tiling.empty)
-next
-  case (Suc n)
-  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
-  have "?B (Suc n) = ?a Un ?B n"
-    by (auto simp add: Sigma_Suc Un_assoc)
-  moreover have "... : ?T"
-  proof (rule tiling.Un)
-    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
-      by (rule domino.horiz)
-    also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
-    finally show "... : domino" .
-    show "?B n : ?T" by (rule Suc)
-    show "?a <= - ?B n" by blast
-  qed
-  ultimately show ?case by simp
-qed
-
-lemma dominoes_tile_matrix:
-  "below m <*> below (2 * n) : tiling domino"
-  (is "?B m : ?T")
-proof (induct m)
-  case 0
-  show ?case by (simp add: below_0 tiling.empty)
-next
-  case (Suc m)
-  let ?t = "{m} <*> below (2 * n)"
-  have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
-  moreover have "... : ?T"
-  proof (rule tiling_Un)
-    show "?t : ?T" by (rule dominoes_tile_row)
-    show "?B m : ?T" by (rule Suc)
-    show "?t Int ?B m = {}" by blast
-  qed
-  ultimately show ?case by simp
-qed
-
-lemma domino_singleton:
-  assumes d: "d : domino" and "b < 2"
-  shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
-  using d
-proof induct
-  from `b < 2` have b_cases: "b = 0 | b = 1" by arith
-  fix i j
-  note [simp] = evnodd_empty evnodd_insert mod_Suc
-  from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
-  from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
-qed
-
-lemma domino_finite:
-  assumes d: "d: domino"
-  shows "finite d"
-  using d
-proof induct
-  fix i j :: nat
-  show "finite {(i, j), (i, j + 1)}" by (intro finite.intros)
-  show "finite {(i, j), (i + 1, j)}" by (intro finite.intros)
-qed
-
-
-subsection {* Tilings of dominoes *}
-
-lemma tiling_domino_finite:
-  assumes t: "t : tiling domino"  (is "t : ?T")
-  shows "finite t"  (is "?F t")
-  using t
-proof induct
-  show "?F {}" by (rule finite.emptyI)
-  fix a t assume "?F t"
-  assume "a : domino" then have "?F a" by (rule domino_finite)
-  from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
-qed
-
-lemma tiling_domino_01:
-  assumes t: "t : tiling domino"  (is "t : ?T")
-  shows "card (evnodd t 0) = card (evnodd t 1)"
-  using t
-proof induct
-  case empty
-  show ?case by (simp add: evnodd_def)
-next
-  case (Un a t)
-  let ?e = evnodd
-  note hyp = `card (?e t 0) = card (?e t 1)`
-    and at = `a <= - t`
-  have card_suc:
-    "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
-  proof -
-    fix b :: nat assume "b < 2"
-    have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
-    also obtain i j where e: "?e a b = {(i, j)}"
-    proof -
-      from `a \<in> domino` and `b < 2`
-      have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
-      then show ?thesis by (blast intro: that)
-    qed
-    moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
-    moreover have "card ... = Suc (card (?e t b))"
-    proof (rule card_insert_disjoint)
-      from `t \<in> tiling domino` have "finite t"
-	by (rule tiling_domino_finite)
-      then show "finite (?e t b)"
-        by (rule evnodd_finite)
-      from e have "(i, j) : ?e a b" by simp
-      with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
-    qed
-    ultimately show "?thesis b" by simp
-  qed
-  then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
-  also from hyp have "card (?e t 0) = card (?e t 1)" .
-  also from card_suc have "Suc ... = card (?e (a Un t) 1)"
-    by simp
-  finally show ?case .
-qed
-
-
-subsection {* Main theorem *}
-
-constdefs
-  mutilated_board :: "nat => nat => (nat * nat) set"
-  "mutilated_board m n ==
-    below (2 * (m + 1)) <*> below (2 * (n + 1))
-      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
-
-theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
-proof (unfold mutilated_board_def)
-  let ?T = "tiling domino"
-  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
-  let ?t' = "?t - {(0, 0)}"
-  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
-
-  show "?t'' ~: ?T"
-  proof
-    have t: "?t : ?T" by (rule dominoes_tile_matrix)
-    assume t'': "?t'' : ?T"
-
-    let ?e = evnodd
-    have fin: "finite (?e ?t 0)"
-      by (rule evnodd_finite, rule tiling_domino_finite, rule t)
-
-    note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
-    have "card (?e ?t'' 0) < card (?e ?t' 0)"
-    proof -
-      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
-        < card (?e ?t' 0)"
-      proof (rule card_Diff1_less)
-        from _ fin show "finite (?e ?t' 0)"
-          by (rule finite_subset) auto
-        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
-      qed
-      then show ?thesis by simp
-    qed
-    also have "... < card (?e ?t 0)"
-    proof -
-      have "(0, 0) : ?e ?t 0" by simp
-      with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
-        by (rule card_Diff1_less)
-      then show ?thesis by simp
-    qed
-    also from t have "... = card (?e ?t 1)"
-      by (rule tiling_domino_01)
-    also have "?e ?t 1 = ?e ?t'' 1" by simp
-    also from t'' have "card ... = card (?e ?t'' 0)"
-      by (rule tiling_domino_01 [symmetric])
-    finally have "... < ..." . then show False ..
-  qed
-qed
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Mutilated_Checkerboard.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Mutilated_Checkerboard.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,300 @@
+(*  Title:      HOL/Isar_examples/Mutilated_Checkerboard.thy
+    Author:     Markus Wenzel, TU Muenchen (Isar document)
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
+*)
+
+header {* The Mutilated Checker Board Problem *}
+
+theory Mutilated_Checkerboard
+imports Main
+begin
+
+text {*
+ The Mutilated Checker Board Problem, formalized inductively.  See
+ \cite{paulson-mutilated-board} and
+ \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the
+ original tactic script version.
+*}
+
+subsection {* Tilings *}
+
+inductive_set
+  tiling :: "'a set set => 'a set set"
+  for A :: "'a set set"
+  where
+    empty: "{} : tiling A"
+  | Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
+
+
+text "The union of two disjoint tilings is a tiling."
+
+lemma tiling_Un:
+  assumes "t : tiling A" and "u : tiling A" and "t Int u = {}"
+  shows "t Un u : tiling A"
+proof -
+  let ?T = "tiling A"
+  from `t : ?T` and `t Int u = {}`
+  show "t Un u : ?T"
+  proof (induct t)
+    case empty
+    with `u : ?T` show "{} Un u : ?T" by simp
+  next
+    case (Un a t)
+    show "(a Un t) Un u : ?T"
+    proof -
+      have "a Un (t Un u) : ?T"
+	using `a : A`
+      proof (rule tiling.Un)
+        from `(a Un t) Int u = {}` have "t Int u = {}" by blast
+        then show "t Un u: ?T" by (rule Un)
+        from `a <= - t` and `(a Un t) Int u = {}`
+	show "a <= - (t Un u)" by blast
+      qed
+      also have "a Un (t Un u) = (a Un t) Un u"
+        by (simp only: Un_assoc)
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+
+subsection {* Basic properties of ``below'' *}
+
+constdefs
+  below :: "nat => nat set"
+  "below n == {i. i < n}"
+
+lemma below_less_iff [iff]: "(i: below k) = (i < k)"
+  by (simp add: below_def)
+
+lemma below_0: "below 0 = {}"
+  by (simp add: below_def)
+
+lemma Sigma_Suc1:
+    "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"
+  by (simp add: below_def less_Suc_eq) blast
+
+lemma Sigma_Suc2:
+    "m = n + 2 ==> A <*> below m =
+      (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
+  by (auto simp add: below_def)
+
+lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
+
+
+subsection {* Basic properties of ``evnodd'' *}
+
+constdefs
+  evnodd :: "(nat * nat) set => nat => (nat * nat) set"
+  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
+
+lemma evnodd_iff:
+    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
+  by (simp add: evnodd_def)
+
+lemma evnodd_subset: "evnodd A b <= A"
+  by (unfold evnodd_def, rule Int_lower1)
+
+lemma evnoddD: "x : evnodd A b ==> x : A"
+  by (rule subsetD, rule evnodd_subset)
+
+lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
+  by (rule finite_subset, rule evnodd_subset)
+
+lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"
+  by (unfold evnodd_def) blast
+
+lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
+  by (unfold evnodd_def) blast
+
+lemma evnodd_empty: "evnodd {} b = {}"
+  by (simp add: evnodd_def)
+
+lemma evnodd_insert: "evnodd (insert (i, j) C) b =
+    (if (i + j) mod 2 = b
+      then insert (i, j) (evnodd C b) else evnodd C b)"
+  by (simp add: evnodd_def) blast
+
+
+subsection {* Dominoes *}
+
+inductive_set
+  domino :: "(nat * nat) set set"
+  where
+    horiz: "{(i, j), (i, j + 1)} : domino"
+  | vertl: "{(i, j), (i + 1, j)} : domino"
+
+lemma dominoes_tile_row:
+  "{i} <*> below (2 * n) : tiling domino"
+  (is "?B n : ?T")
+proof (induct n)
+  case 0
+  show ?case by (simp add: below_0 tiling.empty)
+next
+  case (Suc n)
+  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
+  have "?B (Suc n) = ?a Un ?B n"
+    by (auto simp add: Sigma_Suc Un_assoc)
+  moreover have "... : ?T"
+  proof (rule tiling.Un)
+    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
+      by (rule domino.horiz)
+    also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
+    finally show "... : domino" .
+    show "?B n : ?T" by (rule Suc)
+    show "?a <= - ?B n" by blast
+  qed
+  ultimately show ?case by simp
+qed
+
+lemma dominoes_tile_matrix:
+  "below m <*> below (2 * n) : tiling domino"
+  (is "?B m : ?T")
+proof (induct m)
+  case 0
+  show ?case by (simp add: below_0 tiling.empty)
+next
+  case (Suc m)
+  let ?t = "{m} <*> below (2 * n)"
+  have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
+  moreover have "... : ?T"
+  proof (rule tiling_Un)
+    show "?t : ?T" by (rule dominoes_tile_row)
+    show "?B m : ?T" by (rule Suc)
+    show "?t Int ?B m = {}" by blast
+  qed
+  ultimately show ?case by simp
+qed
+
+lemma domino_singleton:
+  assumes d: "d : domino" and "b < 2"
+  shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
+  using d
+proof induct
+  from `b < 2` have b_cases: "b = 0 | b = 1" by arith
+  fix i j
+  note [simp] = evnodd_empty evnodd_insert mod_Suc
+  from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
+  from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
+qed
+
+lemma domino_finite:
+  assumes d: "d: domino"
+  shows "finite d"
+  using d
+proof induct
+  fix i j :: nat
+  show "finite {(i, j), (i, j + 1)}" by (intro finite.intros)
+  show "finite {(i, j), (i + 1, j)}" by (intro finite.intros)
+qed
+
+
+subsection {* Tilings of dominoes *}
+
+lemma tiling_domino_finite:
+  assumes t: "t : tiling domino"  (is "t : ?T")
+  shows "finite t"  (is "?F t")
+  using t
+proof induct
+  show "?F {}" by (rule finite.emptyI)
+  fix a t assume "?F t"
+  assume "a : domino" then have "?F a" by (rule domino_finite)
+  from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
+qed
+
+lemma tiling_domino_01:
+  assumes t: "t : tiling domino"  (is "t : ?T")
+  shows "card (evnodd t 0) = card (evnodd t 1)"
+  using t
+proof induct
+  case empty
+  show ?case by (simp add: evnodd_def)
+next
+  case (Un a t)
+  let ?e = evnodd
+  note hyp = `card (?e t 0) = card (?e t 1)`
+    and at = `a <= - t`
+  have card_suc:
+    "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+  proof -
+    fix b :: nat assume "b < 2"
+    have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
+    also obtain i j where e: "?e a b = {(i, j)}"
+    proof -
+      from `a \<in> domino` and `b < 2`
+      have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
+      then show ?thesis by (blast intro: that)
+    qed
+    moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+    moreover have "card ... = Suc (card (?e t b))"
+    proof (rule card_insert_disjoint)
+      from `t \<in> tiling domino` have "finite t"
+	by (rule tiling_domino_finite)
+      then show "finite (?e t b)"
+        by (rule evnodd_finite)
+      from e have "(i, j) : ?e a b" by simp
+      with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
+    qed
+    ultimately show "?thesis b" by simp
+  qed
+  then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
+  also from hyp have "card (?e t 0) = card (?e t 1)" .
+  also from card_suc have "Suc ... = card (?e (a Un t) 1)"
+    by simp
+  finally show ?case .
+qed
+
+
+subsection {* Main theorem *}
+
+constdefs
+  mutilated_board :: "nat => nat => (nat * nat) set"
+  "mutilated_board m n ==
+    below (2 * (m + 1)) <*> below (2 * (n + 1))
+      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+
+theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
+proof (unfold mutilated_board_def)
+  let ?T = "tiling domino"
+  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
+  let ?t' = "?t - {(0, 0)}"
+  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
+
+  show "?t'' ~: ?T"
+  proof
+    have t: "?t : ?T" by (rule dominoes_tile_matrix)
+    assume t'': "?t'' : ?T"
+
+    let ?e = evnodd
+    have fin: "finite (?e ?t 0)"
+      by (rule evnodd_finite, rule tiling_domino_finite, rule t)
+
+    note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
+    have "card (?e ?t'' 0) < card (?e ?t' 0)"
+    proof -
+      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
+        < card (?e ?t' 0)"
+      proof (rule card_Diff1_less)
+        from _ fin show "finite (?e ?t' 0)"
+          by (rule finite_subset) auto
+        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
+      qed
+      then show ?thesis by simp
+    qed
+    also have "... < card (?e ?t 0)"
+    proof -
+      have "(0, 0) : ?e ?t 0" by simp
+      with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
+        by (rule card_Diff1_less)
+      then show ?thesis by simp
+    qed
+    also from t have "... = card (?e ?t 1)"
+      by (rule tiling_domino_01)
+    also have "?e ?t 1 = ?e ?t'' 1" by simp
+    also from t'' have "card ... = card (?e ?t'' 0)"
+      by (rule tiling_domino_01 [symmetric])
+    finally have "... < ..." . then show False ..
+  qed
+qed
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/NestedDatatype.thy
--- a/src/HOL/Isar_examples/NestedDatatype.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-
-(* $Id$ *)
-
-header {* Nested datatypes *}
-
-theory NestedDatatype imports Main begin
-
-subsection {* Terms and substitution *}
-
-datatype ('a, 'b) "term" =
-    Var 'a
-  | App 'b "('a, 'b) term list"
-
-consts
-  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
-  subst_term_list ::
-    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
-
-primrec (subst)
-  "subst_term f (Var a) = f a"
-  "subst_term f (App b ts) = App b (subst_term_list f ts)"
-  "subst_term_list f [] = []"
-  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-
-
-text {*
- \medskip A simple lemma about composition of substitutions.
-*}
-
-lemma "subst_term (subst_term f1 o f2) t =
-      subst_term f1 (subst_term f2 t)"
-  and "subst_term_list (subst_term f1 o f2) ts =
-      subst_term_list f1 (subst_term_list f2 ts)"
-  by (induct t and ts) simp_all
-
-lemma "subst_term (subst_term f1 o f2) t =
-  subst_term f1 (subst_term f2 t)"
-proof -
-  let "?P t" = ?thesis
-  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
-    subst_term_list f1 (subst_term_list f2 ts)"
-  show ?thesis
-  proof (induct t)
-    fix a show "?P (Var a)" by simp
-  next
-    fix b ts assume "?Q ts"
-    then show "?P (App b ts)"
-      by (simp only: subst.simps)
-  next
-    show "?Q []" by simp
-  next
-    fix t ts
-    assume "?P t" "?Q ts" then show "?Q (t # ts)"
-      by (simp only: subst.simps)
-  qed
-qed
-
-
-subsection {* Alternative induction *}
-
-theorem term_induct' [case_names Var App]:
-  assumes var: "!!a. P (Var a)"
-    and app: "!!b ts. list_all P ts ==> P (App b ts)"
-  shows "P t"
-proof (induct t)
-  fix a show "P (Var a)" by (rule var)
-next
-  fix b t ts assume "list_all P ts"
-  then show "P (App b ts)" by (rule app)
-next
-  show "list_all P []" by simp
-next
-  fix t ts assume "P t" "list_all P ts"
-  then show "list_all P (t # ts)" by simp
-qed
-
-lemma
-  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
-proof (induct t rule: term_induct')
-  case (Var a)
-  show ?case by (simp add: o_def)
-next
-  case (App b ts)
-  then show ?case by (induct ts) simp_all
-qed
-
-end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Nested_Datatype.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Nested_Datatype.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,86 @@
+header {* Nested datatypes *}
+
+theory Nested_Datatype
+imports Main
+begin
+
+subsection {* Terms and substitution *}
+
+datatype ('a, 'b) "term" =
+    Var 'a
+  | App 'b "('a, 'b) term list"
+
+consts
+  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
+  subst_term_list ::
+    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+
+primrec (subst)
+  "subst_term f (Var a) = f a"
+  "subst_term f (App b ts) = App b (subst_term_list f ts)"
+  "subst_term_list f [] = []"
+  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
+
+
+text {*
+ \medskip A simple lemma about composition of substitutions.
+*}
+
+lemma "subst_term (subst_term f1 o f2) t =
+      subst_term f1 (subst_term f2 t)"
+  and "subst_term_list (subst_term f1 o f2) ts =
+      subst_term_list f1 (subst_term_list f2 ts)"
+  by (induct t and ts) simp_all
+
+lemma "subst_term (subst_term f1 o f2) t =
+  subst_term f1 (subst_term f2 t)"
+proof -
+  let "?P t" = ?thesis
+  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
+    subst_term_list f1 (subst_term_list f2 ts)"
+  show ?thesis
+  proof (induct t)
+    fix a show "?P (Var a)" by simp
+  next
+    fix b ts assume "?Q ts"
+    then show "?P (App b ts)"
+      by (simp only: subst.simps)
+  next
+    show "?Q []" by simp
+  next
+    fix t ts
+    assume "?P t" "?Q ts" then show "?Q (t # ts)"
+      by (simp only: subst.simps)
+  qed
+qed
+
+
+subsection {* Alternative induction *}
+
+theorem term_induct' [case_names Var App]:
+  assumes var: "!!a. P (Var a)"
+    and app: "!!b ts. list_all P ts ==> P (App b ts)"
+  shows "P t"
+proof (induct t)
+  fix a show "P (Var a)" by (rule var)
+next
+  fix b t ts assume "list_all P ts"
+  then show "P (App b ts)" by (rule app)
+next
+  show "list_all P []" by simp
+next
+  fix t ts assume "P t" "list_all P ts"
+  then show "list_all P (t # ts)" by simp
+qed
+
+lemma
+  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
+proof (induct t rule: term_induct')
+  case (Var a)
+  show ?case by (simp add: o_def)
+next
+  case (App b ts)
+  then show ?case by (induct ts) simp_all
+qed
+
+end
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Isar_examples/Peirce.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Peirce's Law *}
 
-theory Peirce imports Main begin
+theory Peirce
+imports Main
+begin
 
 text {*
  We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,7 +1,8 @@
-
 header {* An old chestnut *}
 
-theory Puzzle imports Main begin
+theory Puzzle
+imports Main
+begin
 
 text_raw {*
   \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Mon Jun 22 23:48:24 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Isar_examples/ROOT.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
@@ -8,16 +7,16 @@
 no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"];
 
 use_thys [
-  "BasicLogic",
+  "Basic_Logic",
   "Cantor",
   "Peirce",
   "Drinker",
-  "ExprCompiler",
+  "Expr_Compiler",
   "Group",
   "Summation",
-  "KnasterTarski",
-  "MutilatedCheckerboard",
+  "Knaster_Tarski",
+  "Mutilated_Checkerboard",
   "Puzzle",
-  "NestedDatatype",
-  "HoareEx"
+  "Nested_Datatype",
+  "Hoare_Ex"
 ];
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Mon Jun 22 23:48:24 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Isar_examples/Summation.thy
-    ID:         $Id$
     Author:     Markus Wenzel
 *)
 
diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/document/root.tex	Mon Jun 22 23:48:24 2009 +0200
@@ -1,6 +1,3 @@
-
-% $Id$
-
 \input{style}
 
 \hyphenation{Isabelle}