summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 16 Nov 2005 19:34:19 +0100 | |

changeset 18193 | 54419506df9e |

parent 18192 | 6e2fd2d276d3 |

child 18194 | 940515d2fa26 |

tuned document;

--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Nov 16 19:34:19 2005 +0100 @@ -13,10 +13,10 @@ 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 $I$, $K$, and $S$. The - following (rather explicit) proofs should require little extra - explanations. + 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" @@ -45,7 +45,7 @@ assume A show C proof (rule mp) - show "B --> C" by (rule mp) + show "B --> C" by (rule mp) show B by (rule mp) qed qed @@ -53,12 +53,13 @@ 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. + 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. + First of all, proof by assumption may be abbreviated as a single + dot. *} lemma "A --> A" @@ -68,11 +69,11 @@ 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. + 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" @@ -80,36 +81,37 @@ qed text {* - Note that the \isacommand{proof} command refers to the $\idt{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. + 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. + 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.} + 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 $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. + 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 $\idt{intro}$ proof method repeatedly decomposes a goal's - conclusion.\footnote{The dual method is $\idt{elim}$, acting on a - goal's premises.} + 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" @@ -119,41 +121,40 @@ qed text {* - Again, the body may be collapsed. + Again, the body may be collapsed. *} lemma "A --> B --> A" by (intro impI) text {* - Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{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, $\idt{intro}$ and $\idt{elim}$ would be typically - restricted to certain structures by giving a few rules only, e.g.\ - \isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip - implications and universal quantifiers. + 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 $\idt{intro}$ and $\idt{elim}$. In contrast, - terminal steps that solve a goal completely are usually performed by - actual automated proof methods (such as - \isacommand{by}~$\idt{blast}$). + 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 $A \conj B \impl B \conj - A$. + 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. + The first version is purely backward. *} lemma "A & B --> B & A" @@ -167,13 +168,13 @@ qed text {* - Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named - explicitly, since the goals $B$ and $A$ did not provide any - structural clue. This may be avoided using \isacommand{from} to - focus on $\idt{prems}$ (i.e.\ the $A \conj 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. + 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 @{text prems} (i.e.\ 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" @@ -187,29 +188,29 @@ 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 $B \conj A$ from $A - \conj B$ actually becomes an elimination, rather than an - introduction. The resulting proof structure directly corresponds to - that of the $\name{conjE}$ rule, including the repeated goal - proposition that is abbreviated as $\var{thesis}$ below. + 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 \name{conjE} of $A \conj B$ *} + proof -- {* rule @{text conjE} of @{text "A \<and> B"} *} assume A B - show ?thesis .. -- {* rule \name{conjI} of $B \conj A$ *} + 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. + 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" @@ -221,9 +222,9 @@ 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. + 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" @@ -238,29 +239,29 @@ 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). + \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. + 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. - This reads even more concisely using \isacommand{thus}, which - abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same - vein, \isacommand{hence} abbreviates - \isacommand{then}~\isacommand{have}.} + For our example the most appropriate way of reasoning is probably + the middle one, with conjunction introduction done after + elimination. This reads even more concisely using + \isacommand{thus}, which abbreviates + \isacommand{then}~\isacommand{show}.\footnote{In the same vein, + \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.} *} lemma "A & B --> B & A" @@ -278,16 +279,16 @@ 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. + 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 $P \disj P \impl P$. The proof below - involves forward-chaining from $P \disj P$, followed by an explicit - case-analysis on the two \emph{identical} cases. + 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" @@ -295,7 +296,7 @@ assume "P | P" thus P proof -- {* - rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} + rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} *} assume P show P . next @@ -304,27 +305,27 @@ 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. + 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. + \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. + 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. + \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" @@ -339,10 +340,10 @@ 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. + 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" @@ -355,17 +356,17 @@ subsubsection {* A quantifier proof *} text {* - To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap - x)) \impl (\ex x P \ap x)$. Informally, this holds because any $a$ - with $P \ap (f \ap a)$ may be taken as a witness for the second - existential statement. + 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. + 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)" @@ -382,12 +383,12 @@ 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. + 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)" @@ -402,10 +403,10 @@ qed text {* - Explicit $\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. + 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)" @@ -416,13 +417,13 @@ 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. + 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. *} @@ -430,10 +431,10 @@ 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. + 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" @@ -448,12 +449,12 @@ qed text {* - Note that classic Isabelle handles higher rules in a slightly - different way. The tactic script as given in \cite{isabelle-intro} - for the same example of \name{conjE} depends on the primitive - \texttt{goal} command to decompose the rule into premises and - conclusion. The actual result would then emerge by discharging of - the context at \texttt{qed} time. + Note that classic Isabelle handles higher rules in a slightly + different way. The tactic script as given in \cite{isabelle-intro} + for the same example of \name{conjE} depends on the primitive + \texttt{goal} command to decompose the rule into premises and + conclusion. The actual result would then emerge by discharging of + the context at \texttt{qed} time. *} end

--- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Nov 16 19:34:19 2005 +0100 @@ -131,7 +131,7 @@ theorem correctness: "execute (compile e) env = eval e env" proof - - have "!!stack. exec (compile e) stack env = eval e env # stack" + have "\<And>stack. exec (compile e) stack env = eval e env # stack" proof (induct e) case Variable show ?case by simp next @@ -187,8 +187,7 @@ theorem correctness': "execute (compile e) env = eval e env" proof - - have exec_compile: - "!!stack. exec (compile e) stack env = eval e env # stack" + 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"

--- a/src/HOL/Isar_examples/Hoare.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/Hoare.thy Wed Nov 16 19:34:19 2005 +0100 @@ -411,36 +411,37 @@ *} lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" -by (auto simp:Valid_def) + by (auto simp add: Valid_def) lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q" -by (auto simp:Valid_def) + by (auto simp: Valid_def) lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R" -by (auto simp:Valid_def) + by (auto simp: Valid_def) lemma CondRule: - "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} - \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" -by (auto simp:Valid_def) + "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')} + \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q" + by (auto simp: Valid_def) -lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==> - (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"; -apply(induct n) - apply clarsimp -apply(simp (no_asm_use)) -apply blast -done +lemma iter_aux: " + \<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==> + (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)" + apply(induct n) + apply clarsimp + apply (simp (no_asm_use)) + apply blast + done lemma WhileRule: - "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" -apply (clarsimp simp:Valid_def) -apply(drule iter_aux) - prefer 2 apply assumption - apply blast -apply blast -done - + "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q" + apply (clarsimp simp: Valid_def) + apply (drule iter_aux) + prefer 2 + apply assumption + apply blast + apply blast + done ML {* val Valid_def = thm "Valid_def" *} use "~~/src/HOL/Hoare/hoare.ML"

--- a/src/HOL/Isar_examples/HoareEx.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/HoareEx.thy Wed Nov 16 19:34:19 2005 +0100 @@ -274,31 +274,31 @@ .{\<acute>S = (SUM j<n. j)}." by hoare auto -subsection{*Time*} + +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. + 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>" +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(%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)" - + "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 lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" + by (induct n) simp_all lemma "|- .{i = \<acute>I & \<acute>time = 0}. timeit( @@ -312,17 +312,17 @@ \<acute>I := \<acute>I - 1 OD ) .{2*\<acute>time = i*i + 5*i}." -apply simp -apply hoare - apply simp + apply simp + apply hoare + apply simp + apply clarsimp + apply clarsimp + apply arith + prefer 2 apply clarsimp - apply clarsimp + apply (clarsimp simp: nat_distrib) + apply (frule lem) apply arith - prefer 2 - apply clarsimp -apply (clarsimp simp:nat_distrib) -apply(frule lem) -apply arith -done + done end

--- a/src/HOL/Isar_examples/Puzzle.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/Puzzle.thy Wed Nov 16 19:34:19 2005 +0100 @@ -4,13 +4,15 @@ theory Puzzle imports Main begin text_raw {* - \footnote{A question from ``Bundeswettbewerb Mathematik''. Original - pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by - Tobias Nipkow.} + \footnote{A question from ``Bundeswettbewerb Mathematik''. Original + pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by + Tobias Nipkow.} +*} - \medskip \textbf{Problem.} Given some function $f\colon \Nat \to - \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all - $n$. Demonstrate that $f$ is the identity. +text {* + \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such + that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. + Demonstrate that $f$ is the identity. *} theorem

--- a/src/HOL/Isar_examples/Summation.thy Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/Summation.thy Wed Nov 16 19:34:19 2005 +0100 @@ -113,7 +113,8 @@ proof (induct n) show "?P 0" by simp next - fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib) + fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" + by (simp add: distrib) also assume "?S n = n * (n + 1) * (2 * n + 1)" also have "... + 6 * (n + 1)^Suc (Suc 0) = (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)

--- a/src/HOL/Isar_examples/document/root.tex Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/document/root.tex Wed Nov 16 19:34:19 2005 +0100 @@ -13,11 +13,11 @@ \maketitle \begin{abstract} - Isar offers a high-level proof (and theory) language for Isabelle. We give - various examples of Isabelle/Isar proof developments, ranging from simple - demonstrations of certain language features to a bit more advanced - applications. Note that the ``real'' applications of Isar are found - elsewhere. + Isar offers a high-level proof (and theory) language for Isabelle. + We give various examples of Isabelle/Isar proof developments, + ranging from simple demonstrations of certain language features to a + bit more advanced applications. The ``real'' applications of + Isabelle/Isar are found elsewhere. \end{abstract} \tableofcontents

--- a/src/HOL/Isar_examples/document/style.tex Wed Nov 16 17:50:35 2005 +0100 +++ b/src/HOL/Isar_examples/document/style.tex Wed Nov 16 19:34:19 2005 +0100 @@ -3,6 +3,7 @@ \documentclass[11pt,a4paper]{article} \usepackage{ifthen,proof,isabelle,isabellesym} +\isabellestyle{it} \usepackage{pdfsetup}\urlstyle{rm} \renewcommand{\isamarkupheader}[1]{\section{#1}} @@ -27,7 +28,7 @@ \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;} \newcommand{\all}[1]{\forall #1\dt\;} \newcommand{\ex}[1]{\exists #1\dt\;} -\newcommand{\impl}{\rightarrow} +\newcommand{\impl}{\to} \newcommand{\conj}{\land} \newcommand{\disj}{\lor} \newcommand{\Impl}{\Longrightarrow}