# 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 \ B \ B \ 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 \ 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 \ A"} from - @{text "A \ 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 \ B"} *} - assume B A - then show ?thesis .. -- {* rule @{text conjI} of @{text "B \ 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 \ P \ P"}. The proof below - involves forward-chaining from @{text "P \ 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 "(\x. P (f - x)) \ (\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 \}-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 \ B \ B \ 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 \ 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 \ A"} from + @{text "A \ 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 \ B"} *} + assume B A + then show ?thesis .. -- {* rule @{text conjI} of @{text "B \ 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 \ P \ P"}. The proof below + involves forward-chaining from @{text "P \ 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 "(\x. P (f + x)) \ (\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 \}-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 "\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: "\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 "\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: "\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 - "|- .{\(N_update (\_. (2 * \N))) : .{\N = 10}.}. \N := 2 * \N .{\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}. \N := 10 .{\N = 10}." - by hoare - -lemma "|- .{2 * \N = 10}. \N := 2 * \N .{\N = 10}." - by hoare - -lemma "|- .{\N = 5}. \N := 2 * \N .{\N = 10}." - by hoare simp - -lemma "|- .{\N + 1 = a + 1}. \N := \N + 1 .{\N = a + 1}." - by hoare - -lemma "|- .{\N = a}. \N := \N + 1 .{\N = a + 1}." - by hoare simp - -lemma "|- .{a = a & b = b}. \M := a; \N := b .{\M = a & \N = b}." - by hoare - -lemma "|- .{True}. \M := a; \N := b .{\M = a & \N = b}." - by hoare simp - -lemma -"|- .{\M = a & \N = b}. - \I := \M; \M := \N; \N := \I - .{\M = b & \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 "|- .{\N = a}. \N := \N .{\N = a}." - by hoare - -lemma "|- .{\x = a}. \x := \x .{\x = a}." - oops - -lemma - "Valid {s. x s = a} (Basic (\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 "|- .{\M = \N}. \M := \M + 1 .{\M ~= \N}." -proof - - have ".{\M = \N}. <= .{\M + 1 ~= \N}." - by auto - also have "|- ... \M := \M + 1 .{\M ~= \N}." - by hoare - finally show ?thesis . -qed - -lemma "|- .{\M = \N}. \M := \M + 1 .{\M ~= \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 "|- .{\M + 1 ~= \N}. \M := \M + 1 .{\M ~= \N}." - by hoare - finally show ?thesis . -qed - -lemma "|- .{\M = \N}. \M := \M + 1 .{\M ~= \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 - "|- .{\M = 0 & \S = 0}. - WHILE \M ~= a - DO \S := \S + b; \M := \M + 1 OD - .{\S = a * b}." -proof - - let "|- _ ?while _" = ?thesis - let ".{\?inv}." = ".{\S = \M * b}." - - have ".{\M = 0 & \S = 0}. <= .{\?inv}." by auto - also have "|- ... ?while .{\?inv & ~ (\M ~= a)}." - proof - let ?c = "\S := \S + b; \M := \M + 1" - have ".{\?inv & \M ~= a}. <= .{\S + b = (\M + 1) * b}." - by auto - also have "|- ... ?c .{\?inv}." by hoare - finally show "|- .{\?inv & \M ~= a}. ?c .{\?inv}." . - qed - also have "... <= .{\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 - "|- .{\M = 0 & \S = 0}. - WHILE \M ~= a - INV .{\S = \M * b}. - DO \S := \S + b; \M := \M + 1 OD - .{\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}. - \S := 0; \I := 1; - WHILE \I ~= n - DO - \S := \S + \I; - \I := \I + 1 - OD - .{\S = (SUM jS := 0; \I := 1 .{?inv \S \I}." - proof - - have "True --> 0 = ?sum 1" - by simp - also have "|- .{...}. \S := 0; \I := 1 .{?inv \S \I}." - by hoare - finally show ?thesis . - qed - also have "|- ... ?while .{?inv \S \I & ~ \I ~= n}." - proof - let ?body = "\S := \S + \I; \I := \I + 1" - have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" - by simp - also have "|- .{\S + \I = ?sum (\I + 1)}. ?body .{?inv \S \I}." - by hoare - finally show "|- .{?inv \S \I & \I ~= n}. ?body .{?inv \S \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}. - \S := 0; \I := 1; - WHILE \I ~= n - INV .{\S = (SUM j<\I. j)}. - DO - \S := \S + \I; - \I := \I + 1 - OD - .{\S = (SUM jS := 0; \I := 1; - WHILE \I ~= n - INV .{\S = (SUM j<\I. j)}. - DO - \S := \S + \I; - \I := \I + 1 - OD - .{\S = (SUM j 'a time com" -primrec - "timeit (Basic f) = (Basic f; Basic(\s. s\time := Suc (time s)\))" - "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 \ n + n \ Suc (n * n)" - by (induct n) simp_all - -lemma "|- .{i = \I & \time = 0}. - timeit( - WHILE \I \ 0 - INV .{2*\time + \I*\I + 5*\I = i*i + 5*i}. - DO - \J := \I; - WHILE \J \ 0 - INV .{0 < \I & 2*\time + \I*\I + 3*\I + 2*\J - 2 = i*i + 5*i}. - DO \J := \J - 1 OD; - \I := \I - 1 - OD - ) .{2*\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 + "|- .{\(N_update (\_. (2 * \N))) : .{\N = 10}.}. \N := 2 * \N .{\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}. \N := 10 .{\N = 10}." + by hoare + +lemma "|- .{2 * \N = 10}. \N := 2 * \N .{\N = 10}." + by hoare + +lemma "|- .{\N = 5}. \N := 2 * \N .{\N = 10}." + by hoare simp + +lemma "|- .{\N + 1 = a + 1}. \N := \N + 1 .{\N = a + 1}." + by hoare + +lemma "|- .{\N = a}. \N := \N + 1 .{\N = a + 1}." + by hoare simp + +lemma "|- .{a = a & b = b}. \M := a; \N := b .{\M = a & \N = b}." + by hoare + +lemma "|- .{True}. \M := a; \N := b .{\M = a & \N = b}." + by hoare simp + +lemma +"|- .{\M = a & \N = b}. + \I := \M; \M := \N; \N := \I + .{\M = b & \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 "|- .{\N = a}. \N := \N .{\N = a}." + by hoare + +lemma "|- .{\x = a}. \x := \x .{\x = a}." + oops + +lemma + "Valid {s. x s = a} (Basic (\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 "|- .{\M = \N}. \M := \M + 1 .{\M ~= \N}." +proof - + have ".{\M = \N}. <= .{\M + 1 ~= \N}." + by auto + also have "|- ... \M := \M + 1 .{\M ~= \N}." + by hoare + finally show ?thesis . +qed + +lemma "|- .{\M = \N}. \M := \M + 1 .{\M ~= \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 "|- .{\M + 1 ~= \N}. \M := \M + 1 .{\M ~= \N}." + by hoare + finally show ?thesis . +qed + +lemma "|- .{\M = \N}. \M := \M + 1 .{\M ~= \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 + "|- .{\M = 0 & \S = 0}. + WHILE \M ~= a + DO \S := \S + b; \M := \M + 1 OD + .{\S = a * b}." +proof - + let "|- _ ?while _" = ?thesis + let ".{\?inv}." = ".{\S = \M * b}." + + have ".{\M = 0 & \S = 0}. <= .{\?inv}." by auto + also have "|- ... ?while .{\?inv & ~ (\M ~= a)}." + proof + let ?c = "\S := \S + b; \M := \M + 1" + have ".{\?inv & \M ~= a}. <= .{\S + b = (\M + 1) * b}." + by auto + also have "|- ... ?c .{\?inv}." by hoare + finally show "|- .{\?inv & \M ~= a}. ?c .{\?inv}." . + qed + also have "... <= .{\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 + "|- .{\M = 0 & \S = 0}. + WHILE \M ~= a + INV .{\S = \M * b}. + DO \S := \S + b; \M := \M + 1 OD + .{\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}. + \S := 0; \I := 1; + WHILE \I ~= n + DO + \S := \S + \I; + \I := \I + 1 + OD + .{\S = (SUM jS := 0; \I := 1 .{?inv \S \I}." + proof - + have "True --> 0 = ?sum 1" + by simp + also have "|- .{...}. \S := 0; \I := 1 .{?inv \S \I}." + by hoare + finally show ?thesis . + qed + also have "|- ... ?while .{?inv \S \I & ~ \I ~= n}." + proof + let ?body = "\S := \S + \I; \I := \I + 1" + have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" + by simp + also have "|- .{\S + \I = ?sum (\I + 1)}. ?body .{?inv \S \I}." + by hoare + finally show "|- .{?inv \S \I & \I ~= n}. ?body .{?inv \S \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}. + \S := 0; \I := 1; + WHILE \I ~= n + INV .{\S = (SUM j<\I. j)}. + DO + \S := \S + \I; + \I := \I + 1 + OD + .{\S = (SUM jS := 0; \I := 1; + WHILE \I ~= n + INV .{\S = (SUM j<\I. j)}. + DO + \S := \S + \I; + \I := \I + 1 + OD + .{\S = (SUM j 'a time com" +primrec + "timeit (Basic f) = (Basic f; Basic(\s. s\time := Suc (time s)\))" + "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 \ n + n \ Suc (n * n)" + by (induct n) simp_all + +lemma "|- .{i = \I & \time = 0}. + timeit( + WHILE \I \ 0 + INV .{2*\time + \I*\I + 5*\I = i*i + 5*i}. + DO + \J := \I; + WHILE \J \ 0 + INV .{0 < \I & 2*\time + \I*\I + 3*\I + 2*\J - 2 = i*i + 5*i}. + DO \J := \J - 1 OD; + \I := \I - 1 + OD + ) .{2*\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 \ L"} an order-preserving map. - Then @{text "\{x \ L | f(x) \ x}"} is a fixpoint of @{text f}. - - \textbf{Proof.} Let @{text "H = {x \ L | f(x) \ x}"} and @{text "a = - \H"}. For all @{text "x \ H"} we have @{text "a \ x"}, so @{text - "f(a) \ f(x) \ x"}. Thus @{text "f(a)"} is a lower bound of @{text - H}, whence @{text "f(a) \ 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)) \ - f(a)"}. This says @{text "f(a) \ H"}, so @{text "a \ 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 \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof - - { - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with `mono f` have "f ?a \ f x" .. - also from `x \ ?H` have "\ \ x" .. - finally have "f ?a \ x" . - } - then have "f ?a \ ?a" by (rule Inf_greatest) - { - also presume "\ \ f ?a" - finally (order_antisym) show ?thesis . - } - from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. - then have "f ?a \ ?H" .. - then show "?a \ 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 \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof (rule order_antisym) - show "f ?a \ ?a" - proof (rule Inf_greatest) - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with `mono f` have "f ?a \ f x" .. - also from `x \ ?H` have "\ \ x" .. - finally show "f ?a \ x" . - qed - show "?a \ f ?a" - proof (rule Inf_lower) - from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. - then show "f ?a \ ?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 \ L"} an order-preserving map. + Then @{text "\{x \ L | f(x) \ x}"} is a fixpoint of @{text f}. + + \textbf{Proof.} Let @{text "H = {x \ L | f(x) \ x}"} and @{text "a = + \H"}. For all @{text "x \ H"} we have @{text "a \ x"}, so @{text + "f(a) \ f(x) \ x"}. Thus @{text "f(a)"} is a lower bound of @{text + H}, whence @{text "f(a) \ 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)) \ + f(a)"}. This says @{text "f(a) \ H"}, so @{text "a \ 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 \ 'a" + assumes "mono f" + shows "\a. f a = a" +proof + let ?H = "{u. f u \ u}" + let ?a = "\?H" + show "f ?a = ?a" + proof - + { + fix x + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with `mono f` have "f ?a \ f x" .. + also from `x \ ?H` have "\ \ x" .. + finally have "f ?a \ x" . + } + then have "f ?a \ ?a" by (rule Inf_greatest) + { + also presume "\ \ f ?a" + finally (order_antisym) show ?thesis . + } + from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. + then have "f ?a \ ?H" .. + then show "?a \ 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 \ 'a" + assumes "mono f" + shows "\a. f a = a" +proof + let ?H = "{u. f u \ u}" + let ?a = "\?H" + show "f ?a = ?a" + proof (rule order_antisym) + show "f ?a \ ?a" + proof (rule Inf_greatest) + fix x + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with `mono f` have "f ?a \ f x" .. + also from `x \ ?H` have "\ \ x" .. + finally show "f ?a \ x" . + qed + show "?a \ f ?a" + proof (rule Inf_lower) + from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. + then show "f ?a \ ?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 \ 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 \ 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 \ 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 \ 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 = "\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 = "\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}