--- a/src/HOL/Isar_Examples/Basic_Logic.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Thu Jul 01 18:31:46 2010 +0200
@@ -13,12 +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 @{text I}, @{text K},
- and @{text S}. The following (rather explicit) proofs should
- require little extra explanations.
-*}
+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
@@ -53,15 +51,14 @@
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.
+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.
-*}
+ dot. *}
lemma "A --> A"
proof
@@ -69,51 +66,42 @@
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
+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.
-*}
+ 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.
-*}
+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.
-*}
+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 {* 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
+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.}
-*}
+ goal's premises.} *}
lemma "A --> B --> A"
proof (intro impI)
@@ -121,16 +109,13 @@
show A by fact
qed
-text {*
- Again, the body may be collapsed.
-*}
+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
+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
@@ -142,21 +127,18 @@
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}.
-*}
+ 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
+text {* Certainly, any proof may be performed in backward-style only.
+ On the other hand, small steps of reasoning are often more naturally
expressed in forward-style. Isar supports both backward and forward
reasoning as a first-class concept. In order to demonstrate the
difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
- The first version is purely backward.
-*}
+ The first version is purely backward. *}
lemma "A & B --> B & A"
proof
@@ -168,14 +150,13 @@
qed
qed
-text {*
- Above, the @{text "conjunct_1/2"} projection rules had to be named
- explicitly, since the goals @{text B} and @{text A} did not provide
- any structural clue. This may be avoided using \isacommand{from} to
- focus on the @{text "A \<and> B"} assumption as the current facts,
- enabling the use of double-dot proofs. Note that \isacommand{from}
- already does forward-chaining, involving the \name{conjE} rule here.
-*}
+text {* Above, the @{text "conjunct_1/2"} projection rules had to be
+ named explicitly, since the goals @{text B} and @{text A} did not
+ provide any structural clue. This may be avoided using
+ \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
+ current facts, enabling the use of double-dot proofs. Note that
+ \isacommand{from} already does forward-chaining, involving the
+ @{text conjE} rule here. *}
lemma "A & B --> B & A"
proof
@@ -187,15 +168,13 @@
qed
qed
-text {*
- In the next version, we move the forward step one level upwards.
- Forward-chaining from the most recent facts is indicated by the
- \isacommand{then} command. Thus the proof of @{text "B \<and> A"} from
- @{text "A \<and> B"} actually becomes an elimination, rather than an
+text {* In the next version, we move the forward step one level
+ upwards. Forward-chaining from the most recent facts is indicated
+ by the \isacommand{then} command. Thus the proof of @{text "B \<and> A"}
+ from @{text "A \<and> B"} actually becomes an elimination, rather than an
introduction. The resulting proof structure directly corresponds to
that of the @{text conjE} rule, including the repeated goal
- proposition that is abbreviated as @{text ?thesis} below.
-*}
+ proposition that is abbreviated as @{text ?thesis} below. *}
lemma "A & B --> B & A"
proof
@@ -207,11 +186,9 @@
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.
-*}
+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
@@ -221,11 +198,9 @@
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.
-*}
+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 -
@@ -235,15 +210,14 @@
from `A & B` have B ..
from `B` `A` have "B & A" ..
}
- then show ?thesis .. -- {* rule \name{impI} *}
+ then show ?thesis .. -- {* rule @{text 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).
+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
@@ -252,14 +226,11 @@
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.
-*}
+ 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.
-*}
+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
@@ -275,18 +246,15 @@
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.
-*}
+text {* We rephrase some of the basic reasoning examples of
+ \cite{isabelle-intro}, using HOL rather than FOL. *}
+
subsubsection {* A propositional proof *}
-text {*
- We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof below
- involves forward-chaining from @{text "P \<or> P"}, followed by an
- explicit case-analysis on the two \emph{identical} cases.
-*}
+text {* We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof
+ below involves forward-chaining from @{text "P \<or> P"}, followed by an
+ explicit case-analysis on the two \emph{identical} cases. *}
lemma "P | P --> P"
proof
@@ -301,10 +269,9 @@
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.
+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
@@ -322,8 +289,7 @@
\medskip In our example the situation is even simpler, since the two
cases actually coincide. Consequently the proof may be rephrased as
- follows.
-*}
+ follows. *}
lemma "P | P --> P"
proof
@@ -336,12 +302,10 @@
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.
-*}
+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
@@ -352,26 +316,24 @@
subsubsection {* A quantifier proof *}
-text {*
- To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
- x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any @{text a}
- with @{text "P (f a)"} may be taken as a witness for the second
- existential statement.
+text {* To illustrate quantifier reasoning, let us prove @{text
+ "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any
+ @{text a} with @{text "P (f a)"} may be taken as a witness for the
+ second existential statement.
The first proof is rather verbose, exhibiting quite a lot of
(redundant) detail. It gives explicit rules, even with some
instantiation. Furthermore, we encounter two new language elements:
the \isacommand{fix} command augments the context by some new
``arbitrary, but fixed'' element; the \isacommand{is} annotation
- binds term abbreviations by higher-order pattern matching.
-*}
+ 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}}$}
+ rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
*}
fix a
assume "P (f a)" (is "P ?witness")
@@ -379,14 +341,12 @@
qed
qed
-text {*
- While explicit rule instantiation may occasionally improve
+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.
-*}
+ the text as follows. *}
lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
@@ -399,12 +359,10 @@
qed
qed
-text {*
- Explicit @{text \<exists>}-elimination as seen above can become quite
+text {* Explicit @{text \<exists>}-elimination as seen above can become quite
cumbersome in practice. The derived Isar language element
``\isakeyword{obtain}'' provides a more handsome way to do
- generalized existence reasoning.
-*}
+ generalized existence reasoning. *}
lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
@@ -413,26 +371,21 @@
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.
-*}
-
+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.
-*}
+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 -
--- a/src/HOL/Isar_Examples/Cantor.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,14 +8,11 @@
imports Main
begin
-text_raw {*
- \footnote{This is an Isar version of the final example of the
- Isabelle/HOL manual \cite{isabelle-HOL}.}
-*}
+text_raw {* \footnote{This is an Isar version of the final example of
+ the Isabelle/HOL manual \cite{isabelle-HOL}.} *}
-text {*
- Cantor's Theorem states that every set has more subsets than it has
- elements. It has become a favorite basic example in pure
+text {* Cantor's Theorem states that every set has more subsets than
+ it has elements. It has become a favorite basic example in pure
higher-order logic since it is so easily expressed: \[\all{f::\alpha
\To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
\all{x::\alpha} f \ap x \not= S\]
@@ -25,8 +22,7 @@
every function from $\alpha$ to its powerset, some subset is outside
its range. The Isabelle/Isar proofs below uses HOL's set theory,
with the type $\alpha \ap \idt{set}$ and the operator
- $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
-*}
+ $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
theorem "EX S. S ~: range (f :: 'a => 'a set)"
proof
@@ -48,24 +44,20 @@
qed
qed
-text {*
- How much creativity is required? As it happens, Isabelle can prove
- this theorem automatically using best-first search. Depth-first
- search would diverge, but best-first search successfully navigates
- through the large search space. The context of Isabelle's classical
- prover contains rules for the relevant constructs of HOL's set
- theory.
-*}
+text {* How much creativity is required? As it happens, Isabelle can
+ prove this theorem automatically using best-first search.
+ Depth-first search would diverge, but best-first search successfully
+ navigates through the large search space. The context of Isabelle's
+ classical prover contains rules for the relevant constructs of HOL's
+ set theory. *}
theorem "EX S. S ~: range (f :: 'a => 'a set)"
by best
-text {*
- While this establishes the same theorem internally, we do not get
- any idea of how the proof actually works. There is currently no way
- to transform internal system-level representations of Isabelle
+text {* While this establishes the same theorem internally, we do not
+ get any idea of how the proof actually works. There is currently no
+ way to transform internal system-level representations of Isabelle
proofs back into Isar text. Writing intelligible proof documents
- really is a creative process, after all.
-*}
+ really is a creative process, after all. *}
end
--- a/src/HOL/Isar_Examples/Drinker.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,24 +8,21 @@
imports Main
begin
-text {*
- Here is another example of classical reasoning: the Drinker's
+text {* Here is another example of classical reasoning: the Drinker's
Principle says that for some person, if he is drunk, everybody else
is drunk!
- We first prove a classical part of de-Morgan's law.
-*}
+ We first prove a classical part of de-Morgan's law. *}
-lemma deMorgan:
+lemma de_Morgan:
assumes "\<not> (\<forall>x. P x)"
shows "\<exists>x. \<not> P x"
- using prems
+ using assms
proof (rule contrapos_np)
assume a: "\<not> (\<exists>x. \<not> P x)"
show "\<forall>x. P x"
proof
- fix x
- show "P x"
+ fix x show "P x"
proof (rule classical)
assume "\<not> P x"
then have "\<exists>x. \<not> P x" ..
@@ -41,12 +38,12 @@
then show ?thesis ..
next
assume "\<not> (\<forall>x. drunk x)"
- then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
+ then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
then obtain a where a: "\<not> drunk a" ..
have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
proof
assume "drunk a"
- with a show "\<forall>x. drunk x" by (contradiction)
+ with a show "\<forall>x. drunk x" by contradiction
qed
then show ?thesis ..
qed
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Jul 01 18:31:46 2010 +0200
@@ -10,20 +10,17 @@
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.
-*}
+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.
-*}
+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"
@@ -31,85 +28,71 @@
subsection {* Expressions *}
-text {*
- The language of expressions is defined as an inductive type,
- consisting of variables, constants, and binary operations on
- 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"
+ 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.
-*}
+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
+primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
+where
"eval (Variable x) env = env x"
- "eval (Constant c) env = c"
- "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+| "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.
-*}
+text {* Next we model a simple stack machine, with three
+ instructions. *}
datatype ('adr, 'val) instr =
- Const 'val |
- Load 'adr |
- Apply "'val binop"
+ Const 'val
+ | Load 'adr
+ | Apply "'val binop"
-text {*
- Execution of a list of stack machine instructions is easily defined
- as follows.
-*}
+text {* Execution of a list of stack machine instructions is easily
+ defined as follows. *}
-consts
+primrec
exec :: "(('adr, 'val) instr) list
=> 'val list => ('adr => 'val) => 'val list"
-
-primrec
+where
"exec [] stack env = stack"
- "exec (instr # instrs) stack env =
+| "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)"
-definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" where
- "execute instrs env == hd (exec instrs [] env)"
+definition
+ execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+ where "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"
+text {* We are ready to define the compilation function of expressions
+ to lists of stack machine instructions. *}
primrec
+ compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+where
"compile (Variable x) = [Load x]"
- "compile (Constant c) = [Const c]"
- "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+| "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.
-*}
+text {* The main result of this development is the correctness theorem
+ for @{text compile}. We first establish a lemma about @{text exec}
+ and list append. *}
lemma exec_append:
"exec (xs @ ys) stack env =
@@ -146,13 +129,11 @@
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.
-*}
+text {* \bigskip In the proofs above, the @{text 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"
@@ -221,8 +202,7 @@
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 from exec_compile have "exec (compile e) [] env = [eval e env]" .
also have "hd ... = eval e env" by simp
finally show ?thesis .
qed
--- a/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 18:31:46 2010 +0200
@@ -15,22 +15,20 @@
header {* Fib and Gcd commute *}
theory Fibonacci
-imports Primes
+imports "../Old_Number_Theory/Primes"
begin
-text_raw {*
- \footnote{Isar version by Gertrud Bauer. Original tactic script by
- Larry Paulson. A few proofs of laws taken from
- \cite{Concrete-Math}.}
-*}
+text_raw {* \footnote{Isar version by Gertrud Bauer. Original tactic
+ script by Larry Paulson. A few proofs of laws taken from
+ \cite{Concrete-Math}.} *}
subsection {* Fibonacci numbers *}
fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0"
- | "fib (Suc 0) = 1"
- | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "0 < fib (Suc n)"
by (induct n rule: fib.induct) simp_all
@@ -102,7 +100,7 @@
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
by (simp add: gcd_commute)
also have "fib (n + k + 1)
- = fib (k + 1) * fib (n + 1) + fib k * fib n"
+ = fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
@@ -139,18 +137,17 @@
case False then have "m <= n" by simp
from `0 < m` and False have "n - m < n" by simp
with hyp have "gcd (fib m) (fib ((n - m) mod m))
- = gcd (fib m) (fib (n - m))" by simp
+ = gcd (fib m) (fib (n - m))" by simp
also have "... = gcd (fib m) (fib n)"
using `m <= n` by (rule gcd_fib_diff)
finally have "gcd (fib m) (fib ((n - m) mod m)) =
- gcd (fib m) (fib n)" .
+ gcd (fib m) (fib n)" .
with False show ?thesis by simp
qed
finally show ?thesis .
qed
qed
-
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
proof (induct m n rule: gcd_induct)
fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
--- a/src/HOL/Isar_Examples/Group.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Group.thy Thu Jul 01 18:31:46 2010 +0200
@@ -10,92 +10,83 @@
subsection {* Groups and calculational reasoning *}
-text {*
- Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
- \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
- as an axiomatic type class as follows. Note that the parent class
- $\idt{times}$ is provided by the basic HOL theory.
-*}
-
-notation Groups.one ("one")
+text {* Groups over signature $({\times} :: \alpha \To \alpha \To
+ \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$
+ are defined as an axiomatic type class as follows. Note that the
+ parent class $\idt{times}$ is provided by the basic HOL theory. *}
class group = times + one + inverse +
- assumes group_assoc: "(x * y) * z = x * (y * z)"
- assumes group_left_one: "one * x = x"
- assumes group_left_inverse: "inverse x * x = one"
+ assumes group_assoc: "(x * y) * z = x * (y * z)"
+ and group_left_one: "1 * x = x"
+ and group_left_inverse: "inverse x * x = 1"
-text {*
- The group axioms only state the properties of left one and inverse,
- the right versions may be derived as follows.
-*}
+text {* The group axioms only state the properties of left one and
+ inverse, the right versions may be derived as follows. *}
-theorem group_right_inverse: "x * inverse x = (one::'a::group)"
+theorem (in group) group_right_inverse: "x * inverse x = 1"
proof -
- have "x * inverse x = one * (x * inverse x)"
+ have "x * inverse x = 1 * (x * inverse x)"
by (simp only: group_left_one)
- also have "... = one * x * inverse x"
+ also have "... = 1 * x * inverse x"
by (simp only: group_assoc)
also have "... = inverse (inverse x) * inverse x * x * inverse x"
by (simp only: group_left_inverse)
also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
by (simp only: group_assoc)
- also have "... = inverse (inverse x) * one * inverse x"
+ also have "... = inverse (inverse x) * 1 * inverse x"
by (simp only: group_left_inverse)
- also have "... = inverse (inverse x) * (one * inverse x)"
+ also have "... = inverse (inverse x) * (1 * inverse x)"
by (simp only: group_assoc)
also have "... = inverse (inverse x) * inverse x"
by (simp only: group_left_one)
- also have "... = one"
+ also have "... = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
qed
-text {*
- With \name{group-right-inverse} already available,
- \name{group-right-one}\label{thm:group-right-one} is now established
- much easier.
-*}
+text {* With \name{group-right-inverse} already available,
+ \name{group-right-one}\label{thm:group-right-one} is now established
+ much easier. *}
-theorem group_right_one: "x * one = (x::'a::group)"
+theorem (in group) group_right_one: "x * 1 = x"
proof -
- have "x * one = x * (inverse x * x)"
+ have "x * 1 = x * (inverse x * x)"
by (simp only: group_left_inverse)
also have "... = x * inverse x * x"
by (simp only: group_assoc)
- also have "... = one * x"
+ also have "... = 1 * x"
by (simp only: group_right_inverse)
also have "... = x"
by (simp only: group_left_one)
finally show ?thesis .
qed
-text {*
- \medskip The calculational proof style above follows typical
- presentations given in any introductory course on algebra. The basic
- technique is to form a transitive chain of equations, which in turn
- are established by simplifying with appropriate rules. The low-level
- logical details of equational reasoning are left implicit.
+text {* \medskip The calculational proof style above follows typical
+ presentations given in any introductory course on algebra. The
+ basic technique is to form a transitive chain of equations, which in
+ turn are established by simplifying with appropriate rules. The
+ low-level logical details of equational reasoning are left implicit.
- Note that ``$\dots$'' is just a special term variable that is bound
- automatically to the argument\footnote{The argument of a curried
- infix expression happens to be its right-hand side.} of the last fact
- achieved by any local assumption or proven statement. In contrast to
- $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the
- proof is finished, though.
+ Note that ``$\dots$'' is just a special term variable that is bound
+ automatically to the argument\footnote{The argument of a curried
+ infix expression happens to be its right-hand side.} of the last
+ fact achieved by any local assumption or proven statement. In
+ contrast to $\var{thesis}$, the ``$\dots$'' variable is bound
+ \emph{after} the proof is finished, though.
- There are only two separate Isar language elements for calculational
- proofs: ``\isakeyword{also}'' for initial or intermediate
- calculational steps, and ``\isakeyword{finally}'' for exhibiting the
- result of a calculation. These constructs are not hardwired into
- Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
- Expanding the \isakeyword{also} and \isakeyword{finally} derived
- language elements, calculations may be simulated by hand as
- demonstrated below.
+ There are only two separate Isar language elements for calculational
+ proofs: ``\isakeyword{also}'' for initial or intermediate
+ calculational steps, and ``\isakeyword{finally}'' for exhibiting the
+ result of a calculation. These constructs are not hardwired into
+ Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
+ Expanding the \isakeyword{also} and \isakeyword{finally} derived
+ language elements, calculations may be simulated by hand as
+ demonstrated below.
*}
-theorem "x * one = (x::'a::group)"
+theorem (in group) "x * 1 = x"
proof -
- have "x * one = x * (inverse x * x)"
+ have "x * 1 = x * (inverse x * x)"
by (simp only: group_left_inverse)
note calculation = this
@@ -107,7 +98,7 @@
note calculation = trans [OF calculation this]
-- {* general calculational step: compose with transitivity rule *}
- have "... = one * x"
+ have "... = 1 * x"
by (simp only: group_right_inverse)
note calculation = trans [OF calculation this]
@@ -124,129 +115,119 @@
show ?thesis .
qed
-text {*
- Note that this scheme of calculations is not restricted to plain
- transitivity. Rules like anti-symmetry, or even forward and backward
- substitution work as well. For the actual implementation of
- \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
- separate context information of ``transitivity'' rules. Rule
- selection takes place automatically by higher-order unification.
-*}
+text {* Note that this scheme of calculations is not restricted to
+ plain transitivity. Rules like anti-symmetry, or even forward and
+ backward substitution work as well. For the actual implementation
+ of \isacommand{also} and \isacommand{finally}, Isabelle/Isar
+ maintains separate context information of ``transitivity'' rules.
+ Rule selection takes place automatically by higher-order
+ unification. *}
subsection {* Groups as monoids *}
-text {*
- Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
- \idt{one} :: \alpha)$ are defined like this.
+text {* Monoids over signature $({\times} :: \alpha \To \alpha \To
+ \alpha, \idt{one} :: \alpha)$ are defined like this.
*}
class monoid = times + one +
- assumes monoid_assoc: "(x * y) * z = x * (y * z)"
- assumes monoid_left_one: "one * x = x"
- assumes monoid_right_one: "x * one = x"
+ assumes monoid_assoc: "(x * y) * z = x * (y * z)"
+ and monoid_left_one: "1 * x = x"
+ and monoid_right_one: "x * 1 = x"
-text {*
- Groups are \emph{not} yet monoids directly from the definition. For
- monoids, \name{right-one} had to be included as an axiom, but for
- groups both \name{right-one} and \name{right-inverse} are derivable
- from the other axioms. With \name{group-right-one} derived as a
- theorem of group theory (see page~\pageref{thm:group-right-one}), we
- may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
- as follows.
-*}
+text {* Groups are \emph{not} yet monoids directly from the
+ definition. For monoids, \name{right-one} had to be included as an
+ axiom, but for groups both \name{right-one} and \name{right-inverse}
+ are derivable from the other axioms. With \name{group-right-one}
+ derived as a theorem of group theory (see
+ page~\pageref{thm:group-right-one}), we may still instantiate
+ $\idt{group} \subseteq \idt{monoid}$ properly as follows. *}
instance group < monoid
- by (intro_classes,
- rule group_assoc,
- rule group_left_one,
- rule group_right_one)
+ by intro_classes
+ (rule group_assoc,
+ rule group_left_one,
+ rule group_right_one)
-text {*
- The \isacommand{instance} command actually is a version of
- \isacommand{theorem}, setting up a goal that reflects the intended
- class relation (or type constructor arity). Thus any Isar proof
- language element may be involved to establish this statement. When
- concluding the proof, the result is transformed into the intended
- type signature extension behind the scenes.
-*}
+text {* The \isacommand{instance} command actually is a version of
+ \isacommand{theorem}, setting up a goal that reflects the intended
+ class relation (or type constructor arity). Thus any Isar proof
+ language element may be involved to establish this statement. When
+ concluding the proof, the result is transformed into the intended
+ type signature extension behind the scenes. *}
+
subsection {* More theorems of group theory *}
-text {*
- The one element is already uniquely determined by preserving an
- \emph{arbitrary} group element.
-*}
+text {* The one element is already uniquely determined by preserving
+ an \emph{arbitrary} group element. *}
-theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
+theorem (in group) group_one_equality:
+ assumes eq: "e * x = x"
+ shows "1 = e"
proof -
- assume eq: "e * x = x"
- have "one = x * inverse x"
+ have "1 = x * inverse x"
by (simp only: group_right_inverse)
also have "... = (e * x) * inverse x"
by (simp only: eq)
also have "... = e * (x * inverse x)"
by (simp only: group_assoc)
- also have "... = e * one"
+ also have "... = e * 1"
by (simp only: group_right_inverse)
also have "... = e"
by (simp only: group_right_one)
finally show ?thesis .
qed
-text {*
- Likewise, the inverse is already determined by the cancel property.
-*}
+text {* Likewise, the inverse is already determined by the cancel property. *}
-theorem group_inverse_equality:
- "x' * x = one ==> inverse x = (x'::'a::group)"
+theorem (in group) group_inverse_equality:
+ assumes eq: "x' * x = 1"
+ shows "inverse x = x'"
proof -
- assume eq: "x' * x = one"
- have "inverse x = one * inverse x"
+ have "inverse x = 1 * inverse x"
by (simp only: group_left_one)
also have "... = (x' * x) * inverse x"
by (simp only: eq)
also have "... = x' * (x * inverse x)"
by (simp only: group_assoc)
- also have "... = x' * one"
+ also have "... = x' * 1"
by (simp only: group_right_inverse)
also have "... = x'"
by (simp only: group_right_one)
finally show ?thesis .
qed
-text {*
- The inverse operation has some further characteristic properties.
-*}
+text {* The inverse operation has some further characteristic properties. *}
-theorem group_inverse_times:
- "inverse (x * y) = inverse y * inverse (x::'a::group)"
+theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
proof (rule group_inverse_equality)
- show "(inverse y * inverse x) * (x * y) = one"
+ show "(inverse y * inverse x) * (x * y) = 1"
proof -
have "(inverse y * inverse x) * (x * y) =
(inverse y * (inverse x * x)) * y"
by (simp only: group_assoc)
- also have "... = (inverse y * one) * y"
+ also have "... = (inverse y * 1) * y"
by (simp only: group_left_inverse)
also have "... = inverse y * y"
by (simp only: group_right_one)
- also have "... = one"
+ also have "... = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
qed
qed
-theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
+theorem (in group) inverse_inverse: "inverse (inverse x) = x"
proof (rule group_inverse_equality)
show "x * inverse x = one"
by (simp only: group_right_inverse)
qed
-theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
+theorem (in group) inverse_inject:
+ assumes eq: "inverse x = inverse y"
+ shows "x = y"
proof -
- assume eq: "inverse x = inverse y"
- have "x = x * one"
+ have "x = x * 1"
by (simp only: group_right_one)
also have "... = x * (inverse y * y)"
by (simp only: group_left_inverse)
@@ -254,7 +235,7 @@
by (simp only: eq)
also have "... = (x * inverse x) * y"
by (simp only: group_assoc)
- also have "... = one * y"
+ also have "... = 1 * y"
by (simp only: group_right_inverse)
also have "... = y"
by (simp only: group_left_one)
--- a/src/HOL/Isar_Examples/Hoare.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Jul 01 18:31:46 2010 +0200
@@ -13,14 +13,12 @@
subsection {* Abstract syntax and semantics *}
-text {*
- The following abstract syntax and semantics of Hoare Logic over
- \texttt{WHILE} programs closely follows the existing tradition in
- Isabelle/HOL of formalizing the presentation given in
- \cite[\S6]{Winskel:1993}. See also
- \url{http://isabelle.in.tum.de/library/Hoare/} and
- \cite{Nipkow:1998:Winskel}.
-*}
+text {* The following abstract syntax and semantics of Hoare Logic
+ over \texttt{WHILE} programs closely follows the existing tradition
+ in Isabelle/HOL of formalizing the presentation given in
+ \cite[\S6]{Winskel:1993}. See also
+ \url{http://isabelle.in.tum.de/library/Hoare/} and
+ \cite{Nipkow:1998:Winskel}. *}
types
'a bexp = "'a set"
@@ -32,33 +30,31 @@
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a assn" "'a com"
-abbreviation
- Skip ("SKIP") where
- "SKIP == Basic id"
+abbreviation Skip ("SKIP")
+ where "SKIP == Basic id"
types
'a sem = "'a => 'a => bool"
-consts
- iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
+primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
+where
"iter 0 b S s s' = (s ~: b & s = s')"
- "iter (Suc n) b S s s' =
- (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
+| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
-consts
- Sem :: "'a com => 'a sem"
-primrec
+primrec Sem :: "'a com => 'a sem"
+where
"Sem (Basic f) s s' = (s' = f s)"
- "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
- "Sem (Cond b c1 c2) s s' =
+| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
+| "Sem (Cond b c1 c2) s s' =
(if s : b then Sem c1 s s' else Sem c2 s s')"
- "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
+| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
-definition Valid :: "'a bexp => 'a com => 'a bexp => bool" ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) where
- "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
+definition
+ Valid :: "'a bexp => 'a com => 'a bexp => bool"
+ ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
+ where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
-notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
lemma ValidI [intro?]:
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
@@ -71,22 +67,20 @@
subsection {* Primitive Hoare rules *}
-text {*
- From the semantics defined above, we derive the standard set of
- primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}. Usually,
- variant forms of these rules are applied in actual proof, see also
- \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
+text {* From the semantics defined above, we derive the standard set
+ of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.
+ Usually, variant forms of these rules are applied in actual proof,
+ see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
- \medskip The \name{basic} rule represents any kind of atomic access
- to the state space. This subsumes the common rules of \name{skip}
- and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.
-*}
+ \medskip The \name{basic} rule represents any kind of atomic access
+ to the state space. This subsumes the common rules of \name{skip}
+ and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
theorem basic: "|- {s. f s : P} (Basic f) P"
proof
fix s s' assume s: "s : {s. f s : P}"
assume "Sem (Basic f) s s'"
- hence "s' = f s" by simp
+ then have "s' = f s" by simp
with s show "s' : P" by simp
qed
@@ -117,11 +111,9 @@
with QQ' show "s' : Q'" ..
qed
-text {*
- The rule for conditional commands is directly reflected by the
- corresponding semantics; in the proof we just have to look closely
- which cases apply.
-*}
+text {* The rule for conditional commands is directly reflected by the
+ corresponding semantics; in the proof we just have to look closely
+ which cases apply. *}
theorem cond:
"|- (P Int b) c1 Q ==> |- (P Int -b) c2 Q ==> |- P (Cond b c1 c2) Q"
@@ -147,14 +139,12 @@
qed
qed
-text {*
- The \name{while} rule is slightly less trivial --- it is the only one
- based on recursion, which is expressed in the semantics by a
- Kleene-style least fixed-point construction. The auxiliary statement
- below, which is by induction on the number of iterations is the main
- point to be proven; the rest is by routine application of the
- semantics of \texttt{WHILE}.
-*}
+text {* The @{text while} rule is slightly less trivial --- it is the
+ only one based on recursion, which is expressed in the semantics by
+ a Kleene-style least fixed-point construction. The auxiliary
+ statement below, which is by induction on the number of iterations
+ is the main point to be proven; the rest is by routine application
+ of the semantics of \texttt{WHILE}. *}
theorem while:
assumes body: "|- (P Int b) c P"
@@ -166,12 +156,11 @@
from this and s show "s' : P Int -b"
proof (induct n arbitrary: s)
case 0
- thus ?case by auto
+ then show ?case by auto
next
case (Suc n)
then obtain s'' where b: "s : b" and sem: "Sem c s s''"
- and iter: "iter n b (Sem c) s'' s'"
- by auto
+ and iter: "iter n b (Sem c) s'' s'" by auto
from Suc and b have "s : P Int b" by simp
with body sem have "s'' : P" ..
with iter show ?case by (rule Suc)
@@ -181,30 +170,26 @@
subsection {* Concrete syntax for assertions *}
-text {*
- We now introduce concrete syntax for describing commands (with
- embedded expressions) and assertions. The basic technique is that of
- semantic ``quote-antiquote''. A \emph{quotation} is a syntactic
- entity delimited by an implicit abstraction, say over the state
- space. An \emph{antiquotation} is a marked expression within a
- quotation that refers the implicit argument; a typical antiquotation
- would select (or even update) components from the state.
+text {* We now introduce concrete syntax for describing commands (with
+ embedded expressions) and assertions. The basic technique is that of
+ semantic ``quote-antiquote''. A \emph{quotation} is a syntactic
+ entity delimited by an implicit abstraction, say over the state
+ space. An \emph{antiquotation} is a marked expression within a
+ quotation that refers the implicit argument; a typical antiquotation
+ would select (or even update) components from the state.
- We will see some examples later in the concrete rules and
- applications.
-*}
+ We will see some examples later in the concrete rules and
+ applications. *}
-text {*
- The following specification of syntax and translations is for
- Isabelle experts only; feel free to ignore it.
+text {* The following specification of syntax and translations is for
+ Isabelle experts only; feel free to ignore it.
- While the first part is still a somewhat intelligible specification
- of the concrete syntactic representation of our Hoare language, the
- actual ``ML drivers'' is quite involved. Just note that the we
- re-use the basic quote/antiquote translations as already defined in
- Isabelle/Pure (see \verb,Syntax.quote_tr, and
- \verb,Syntax.quote_tr',).
-*}
+ While the first part is still a somewhat intelligible specification
+ of the concrete syntactic representation of our Hoare language, the
+ actual ``ML drivers'' is quite involved. Just note that the we
+ re-use the basic quote/antiquote translations as already defined in
+ Isabelle/Pure (see \verb,Syntax.quote_tr, and
+ \verb,Syntax.quote_tr',). *}
syntax
"_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000)
@@ -238,11 +223,10 @@
in [(@{syntax_const "_quote"}, quote_tr)] end
*}
-text {*
- As usual in Isabelle syntax translations, the part for printing is
- more complicated --- we cannot express parts as macro rules as above.
- Don't look here, unless you have to do similar things for yourself.
-*}
+text {* As usual in Isabelle syntax translations, the part for
+ printing is more complicated --- we cannot express parts as macro
+ rules as above. Don't look here, unless you have to do similar
+ things for yourself. *}
print_translation {*
let
@@ -277,15 +261,13 @@
subsection {* Rules for single-step proof \label{sec:hoare-isar} *}
-text {*
- We are now ready to introduce a set of Hoare rules to be used in
- single-step structured proofs in Isabelle/Isar. We refer to the
- concrete syntax introduce above.
+text {* We are now ready to introduce a set of Hoare rules to be used
+ in single-step structured proofs in Isabelle/Isar. We refer to the
+ concrete syntax introduce above.
- \medskip Assertions of Hoare Logic may be manipulated in
- calculational proofs, with the inclusion expressed in terms of sets
- or predicates. Reversed order is supported as well.
-*}
+ \medskip Assertions of Hoare Logic may be manipulated in
+ calculational proofs, with the inclusion expressed in terms of sets
+ or predicates. Reversed order is supported as well. *}
lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
by (unfold Valid_def) blast
@@ -312,49 +294,41 @@
by (simp add: Valid_def)
-text {*
- Identity and basic assignments.\footnote{The $\idt{hoare}$ method
- introduced in \S\ref{sec:hoare-vcg} is able to provide proper
- instances for any number of basic assignments, without producing
- additional verification conditions.}
-*}
+text {* Identity and basic assignments.\footnote{The $\idt{hoare}$
+ method introduced in \S\ref{sec:hoare-vcg} is able to provide proper
+ instances for any number of basic assignments, without producing
+ additional verification conditions.} *}
lemma skip [intro?]: "|- P SKIP P"
proof -
have "|- {s. id s : P} SKIP P" by (rule basic)
- thus ?thesis by simp
+ then show ?thesis by simp
qed
lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
by (rule basic)
-text {*
- Note that above formulation of assignment corresponds to our
- preferred way to model state spaces, using (extensible) record types
- in HOL \cite{Naraschewski-Wenzel:1998:HOOL}. For any record field
- $x$, Isabelle/HOL provides a functions $x$ (selector) and
- $\idt{x{\dsh}update}$ (update). Above, there is only a place-holder
- appearing for the latter kind of function: due to concrete syntax
- \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
- to the external nature of HOL record fields, we could not even state
- a general theorem relating selector and update functions (if this
- were required here); this would only work for any particular instance
- of record fields introduced so far.}
-*}
+text {* Note that above formulation of assignment corresponds to our
+ preferred way to model state spaces, using (extensible) record types
+ in HOL \cite{Naraschewski-Wenzel:1998:HOOL}. For any record field
+ $x$, Isabelle/HOL provides a functions $x$ (selector) and
+ $\idt{x{\dsh}update}$ (update). Above, there is only a place-holder
+ appearing for the latter kind of function: due to concrete syntax
+ \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that
+ due to the external nature of HOL record fields, we could not even
+ state a general theorem relating selector and update functions (if
+ this were required here); this would only work for any particular
+ instance of record fields introduced so far.} *}
-text {*
- Sequential composition --- normalizing with associativity achieves
- proper of chunks of code verified separately.
-*}
+text {* Sequential composition --- normalizing with associativity
+ achieves proper of chunks of code verified separately. *}
lemmas [trans, intro?] = seq
lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
by (auto simp add: Valid_def)
-text {*
- Conditional statements.
-*}
+text {* Conditional statements. *}
lemmas [trans, intro?] = cond
@@ -364,9 +338,7 @@
==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
by (rule cond) (simp_all add: Valid_def)
-text {*
- While statements --- with optional invariant.
-*}
+text {* While statements --- with optional invariant. *}
lemma [intro?]:
"|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
@@ -390,18 +362,16 @@
subsection {* Verification conditions \label{sec:hoare-vcg} *}
-text {*
- We now load the \emph{original} ML file for proof scripts and tactic
- definition for the Hoare Verification Condition Generator (see
- \url{http://isabelle.in.tum.de/library/Hoare/}). As far as we are
- concerned here, the result is a proof method \name{hoare}, which may
- be applied to a Hoare Logic assertion to extract purely logical
- verification conditions. It is important to note that the method
- requires \texttt{WHILE} loops to be fully annotated with invariants
- beforehand. Furthermore, only \emph{concrete} pieces of code are
- handled --- the underlying tactic fails ungracefully if supplied with
- meta-variables or parameters, for example.
-*}
+text {* We now load the \emph{original} ML file for proof scripts and
+ tactic definition for the Hoare Verification Condition Generator
+ (see \url{http://isabelle.in.tum.de/library/Hoare/}). As far as we
+ are concerned here, the result is a proof method \name{hoare}, which
+ may be applied to a Hoare Logic assertion to extract purely logical
+ verification conditions. It is important to note that the method
+ requires \texttt{WHILE} loops to be fully annotated with invariants
+ beforehand. Furthermore, only \emph{concrete} pieces of code are
+ handled --- the underlying tactic fails ungracefully if supplied
+ with meta-variables or parameters, for example. *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp add: Valid_def)
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Jul 01 18:31:46 2010 +0200
@@ -6,11 +6,9 @@
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.
-*}
+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
@@ -18,37 +16,29 @@
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.
-*}
+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 {* 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.
-*}
+text {* Using the basic @{text assign} rule directly is a bit
+ cumbersome. *}
-lemma
- "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+lemma "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
by (rule assign)
-text {*
- Certainly we want the state modification already done, e.g.\ by
- simplification. The \name{hoare} method performs the basic state
- update for us; we may apply the Simplifier afterwards to achieve
- ``obvious'' consequences as well.
-*}
+text {* Certainly we want the state modification already done, e.g.\
+ by simplification. The \name{hoare} method performs the basic state
+ update for us; we may apply the Simplifier afterwards to achieve
+ ``obvious'' consequences as well. *}
lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
by hoare
@@ -77,12 +67,10 @@
.{\<acute>M = b & \<acute>N = a}."
by hoare simp
-text {*
- It is important to note that statements like the following one can
- only be proven for each individual program variable. Due to the
- extra-logical nature of record fields, we cannot formulate a theorem
- relating record selectors and updates schematically.
-*}
+text {* It is important to note that statements like the following one
+ can only be proven for each individual program variable. Due to the
+ extra-logical nature of record fields, we cannot formulate a theorem
+ relating record selectors and updates schematically. *}
lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
by hoare
@@ -96,11 +84,9 @@
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.
-*}
+text {* In the following assignments we make use of the consequence
+ rule in order to achieve the intended precondition. Certainly, the
+ \name{hoare} method is able to handle this case, too. *}
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
proof -
@@ -128,12 +114,10 @@
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.
-*}
+text {* We now do some basic examples of actual \texttt{WHILE}
+ programs. This one is a loop for calculating the product of two
+ natural numbers, by iterated addition. We first give detailed
+ structured proof based on single-step Hoare rules. *}
lemma
"|- .{\<acute>M = 0 & \<acute>S = 0}.
@@ -157,12 +141,10 @@
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.
-*}
+text {* The subsequent version of the proof applies the @{text hoare}
+ method to reduce the Hoare statement to a purely logical problem
+ that can be solved fully automatically. Note that we have to
+ specify the \texttt{WHILE} loop invariant in the original statement. *}
lemma
"|- .{\<acute>M = 0 & \<acute>S = 0}.
@@ -175,21 +157,15 @@
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 {* 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]
+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. *}
theorem
"|- .{True}.
@@ -227,10 +203,9 @@
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.
-*}
+text {* The next version uses the @{text hoare} method, while still
+ explaining the resulting proof obligations in an abstract,
+ structured manner. *}
theorem
"|- .{True}.
@@ -251,17 +226,15 @@
show "?inv 0 1" by simp
next
fix s i assume "?inv s i & i ~= n"
- thus "?inv (s + i) (i + 1)" by simp
+ then show "?inv (s + i) (i + 1)" by simp
next
fix s i assume "?inv s i & ~ i ~= n"
- thus "s = ?sum n" by simp
+ then show "s = ?sum n" by simp
qed
qed
-text {*
- Certainly, this proof may be done fully automatic as well, provided
- that the invariant is given beforehand.
-*}
+text {* Certainly, this proof may be done fully automatic as well,
+ provided that the invariant is given beforehand. *}
theorem
"|- .{True}.
@@ -278,21 +251,19 @@
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.
-*}
+text{* A simple embedding of time in Hoare logic: function @{text
+ timeit} inserts an extra variable to keep track of the elapsed time. *}
record tstate = time :: nat
types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
-consts timeit :: "'a time com \<Rightarrow> 'a time com"
-primrec
+primrec timeit :: "'a time com \<Rightarrow> 'a time com"
+where
"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)"
+| "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
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Thu Jul 01 18:31:46 2010 +0200
@@ -13,10 +13,10 @@
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.}
+text {* According to the textbook \cite[pages
+ 93--94]{davey-priestley}, the Knaster-Tarski fixpoint theorem is as
+ follows.\footnote{We have dualized the argument, and tuned the
+ notation a little bit.}
\textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a
complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
@@ -28,19 +28,16 @@
H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove
the reverse one (!) and thereby complete the proof that @{text a} is
a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
- f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
-*}
+ f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}. *}
subsection {* Formal versions *}
-text {*
- The Isar proof below closely follows the original presentation.
- Virtually all of the prose narration has been rephrased in terms of
- formal Isar language elements. Just as many textbook-style proofs,
- there is a strong bias towards forward proof, and several bends in
- the course of reasoning.
-*}
+text {* The Isar proof below closely follows the original
+ presentation. Virtually all of the prose narration has been
+ rephrased in terms of formal Isar language elements. Just as many
+ textbook-style proofs, there is a strong bias towards forward proof,
+ and several bends in the course of reasoning. *}
theorem Knaster_Tarski:
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -70,17 +67,15 @@
qed
qed
-text {*
- Above we have used several advanced Isar language elements, such as
- explicit block structure and weak assumptions. Thus we have
+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.
-*}
+ the most basic features of the Isar language. *}
theorem Knaster_Tarski':
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Jul 01 18:31:46 2010 +0200
@@ -9,27 +9,26 @@
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.
-*}
+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"
+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"
+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 = {}"
+ assumes "t : tiling A"
+ and "u : tiling A"
+ and "t Int u = {}"
shows "t Un u : tiling A"
proof -
let ?T = "tiling A"
@@ -60,8 +59,8 @@
subsection {* Basic properties of ``below'' *}
-definition below :: "nat => nat set" where
- "below n == {i. i < n}"
+definition below :: "nat => nat set"
+ where "below n = {i. i < n}"
lemma below_less_iff [iff]: "(i: below k) = (i < k)"
by (simp add: below_def)
@@ -74,8 +73,8 @@
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)"
+ "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
@@ -83,27 +82,26 @@
subsection {* Basic properties of ``evnodd'' *}
-definition evnodd :: "(nat * nat) set => nat => (nat * nat) set" where
- "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
+definition evnodd :: "(nat * nat) set => nat => (nat * nat) set"
+ where "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)"
+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)
+ unfolding evnodd_def by (rule Int_lower1)
lemma evnoddD: "x : evnodd A b ==> x : A"
- by (rule subsetD, rule evnodd_subset)
+ by (rule subsetD) (rule evnodd_subset)
lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
- by (rule finite_subset, rule evnodd_subset)
+ 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
+ unfolding evnodd_def by blast
lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
- by (unfold evnodd_def) blast
+ unfolding evnodd_def by blast
lemma evnodd_empty: "evnodd {} b = {}"
by (simp add: evnodd_def)
@@ -116,11 +114,10 @@
subsection {* Dominoes *}
-inductive_set
- domino :: "(nat * nat) set set"
- where
- horiz: "{(i, j), (i, j + 1)} : domino"
- | vertl: "{(i, j), (i + 1, j)} : domino"
+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"
@@ -165,9 +162,10 @@
qed
lemma domino_singleton:
- assumes d: "d : domino" and "b < 2"
+ assumes "d : domino"
+ and "b < 2"
shows "EX i j. evnodd d b = {(i, j)}" (is "?P d")
- using d
+ using assms
proof induct
from `b < 2` have b_cases: "b = 0 | b = 1" by arith
fix i j
@@ -177,9 +175,9 @@
qed
lemma domino_finite:
- assumes d: "d: domino"
+ assumes "d: domino"
shows "finite d"
- using d
+ using assms
proof induct
fix i j :: nat
show "finite {(i, j), (i, j + 1)}" by (intro finite.intros)
@@ -245,8 +243,9 @@
subsection {* Main theorem *}
-definition mutilated_board :: "nat => nat => (nat * nat) set" where
- "mutilated_board m n ==
+definition mutilated_board :: "nat => nat => (nat * nat) set"
+where
+ "mutilated_board m n =
below (2 * (m + 1)) <*> below (2 * (n + 1))
- {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
@@ -256,7 +255,7 @@
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)
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Thu Jul 01 18:31:46 2010 +0200
@@ -10,8 +10,10 @@
Var 'a
| App 'b "('a, 'b) term list"
-primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
- subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
+primrec
+ subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
+ subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+where
"subst_term f (Var a) = f a"
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
| "subst_term_list f [] = []"
@@ -19,18 +21,18 @@
lemmas subst_simps = subst_term_subst_term_list.simps
-text {*
- \medskip A simple lemma about composition of substitutions.
-*}
+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)"
+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)"
+ subst_term f1 (subst_term f2 t)"
proof -
let "?P t" = ?thesis
let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
--- a/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,17 +8,16 @@
imports Main
begin
-text {*
- We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is
- an inherently non-intuitionistic statement, so its proof will
- certainly involve some form of classical contradiction.
+text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
+ This is an inherently non-intuitionistic statement, so its proof
+ will certainly involve some form of classical contradiction.
- The first proof is again a well-balanced combination of plain
- backward and forward reasoning. The actual classical step is where
- the negated goal may be introduced as additional assumption. This
- eventually leads to a contradiction.\footnote{The rule involved there
- is negation elimination; it holds in intuitionistic logic as well.}
-*}
+ The first proof is again a well-balanced combination of plain
+ backward and forward reasoning. The actual classical step is where
+ the negated goal may be introduced as additional assumption. This
+ eventually leads to a contradiction.\footnote{The rule involved
+ there is negation elimination; it holds in intuitionistic logic as
+ well.} *}
theorem "((A --> B) --> A) --> A"
proof
@@ -35,21 +34,19 @@
qed
qed
-text {*
- In the subsequent version the reasoning is rearranged by means of
- ``weak assumptions'' (as introduced by \isacommand{presume}). Before
- assuming the negated goal $\neg A$, its intended consequence $A \impl
- B$ is put into place in order to solve the main problem.
- Nevertheless, we do not get anything for free, but have to establish
- $A \impl B$ later on. The overall effect is that of a logical
- \emph{cut}.
+text {* In the subsequent version the reasoning is rearranged by means
+ of ``weak assumptions'' (as introduced by \isacommand{presume}).
+ Before assuming the negated goal $\neg A$, its intended consequence
+ $A \impl B$ is put into place in order to solve the main problem.
+ Nevertheless, we do not get anything for free, but have to establish
+ $A \impl B$ later on. The overall effect is that of a logical
+ \emph{cut}.
- Technically speaking, whenever some goal is solved by
- \isacommand{show} in the context of weak assumptions then the latter
- give rise to new subgoals, which may be established separately. In
- contrast, strong assumptions (as introduced by \isacommand{assume})
- are solved immediately.
-*}
+ Technically speaking, whenever some goal is solved by
+ \isacommand{show} in the context of weak assumptions then the latter
+ give rise to new subgoals, which may be established separately. In
+ contrast, strong assumptions (as introduced by \isacommand{assume})
+ are solved immediately. *}
theorem "((A --> B) --> A) --> A"
proof
@@ -68,23 +65,21 @@
qed
qed
-text {*
- Note that the goals stemming from weak assumptions may be even left
- until qed time, where they get eventually solved ``by assumption'' as
- well. In that case there is really no fundamental difference between
- the two kinds of assumptions, apart from the order of reducing the
- individual parts of the proof configuration.
+text {* Note that the goals stemming from weak assumptions may be even
+ left until qed time, where they get eventually solved ``by
+ assumption'' as well. In that case there is really no fundamental
+ difference between the two kinds of assumptions, apart from the
+ order of reducing the individual parts of the proof configuration.
- Nevertheless, the ``strong'' mode of plain assumptions is quite
- important in practice to achieve robustness of proof text
- interpretation. By forcing both the conclusion \emph{and} the
- assumptions to unify with the pending goal to be solved, goal
- selection becomes quite deterministic. For example, decomposition
- with rules of the ``case-analysis'' type usually gives rise to
- several goals that only differ in there local contexts. With strong
- assumptions these may be still solved in any order in a predictable
- way, while weak ones would quickly lead to great confusion,
- eventually demanding even some backtracking.
-*}
+ Nevertheless, the ``strong'' mode of plain assumptions is quite
+ important in practice to achieve robustness of proof text
+ interpretation. By forcing both the conclusion \emph{and} the
+ assumptions to unify with the pending goal to be solved, goal
+ selection becomes quite deterministic. For example, decomposition
+ with rules of the ``case-analysis'' type usually gives rise to
+ several goals that only differ in there local contexts. With strong
+ assumptions these may be still solved in any order in a predictable
+ way, while weak ones would quickly lead to great confusion,
+ eventually demanding even some backtracking. *}
end
--- a/src/HOL/Isar_Examples/Puzzle.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy Thu Jul 01 18:31:46 2010 +0200
@@ -4,17 +4,13 @@
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.}
-*}
+text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''.
+ Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
+ script by Tobias Nipkow.} *}
-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.
-*}
+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
assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
--- a/src/HOL/Isar_Examples/Summation.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy Thu Jul 01 18:31:46 2010 +0200
@@ -8,28 +8,22 @@
imports Main
begin
-text_raw {*
- \footnote{This example is somewhat reminiscent of the
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
- discussed in \cite{isabelle-ref} in the context of permutative
- rewrite rules and ordered rewriting.}
-*}
+text_raw {* \footnote{This example is somewhat reminiscent of the
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
+ discussed in \cite{isabelle-ref} in the context of permutative
+ rewrite rules and ordered rewriting.} *}
-text {*
- Subsequently, we prove some summation laws of natural numbers
- (including odds, squares, and cubes). These examples demonstrate how
- plain natural deduction (including induction) may be combined with
- calculational proof.
-*}
+text {* Subsequently, we prove some summation laws of natural numbers
+ (including odds, squares, and cubes). These examples demonstrate
+ how plain natural deduction (including induction) may be combined
+ with calculational proof. *}
subsection {* Summation laws *}
-text {*
- The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
- 1)/2$. Avoiding formal reasoning about division we prove this
- equation multiplied by $2$.
-*}
+text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times
+ (n + 1)/2$. Avoiding formal reasoning about division we prove this
+ equation multiplied by $2$. *}
theorem sum_of_naturals:
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -43,48 +37,47 @@
finally show "?P (Suc n)" by simp
qed
-text {*
- The above proof is a typical instance of mathematical induction. The
- main statement is viewed as some $\var{P} \ap n$ that is split by the
- induction method into base case $\var{P} \ap 0$, and step case
- $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
+text {* The above proof is a typical instance of mathematical
+ induction. The main statement is viewed as some $\var{P} \ap n$
+ that is split by the induction method into base case $\var{P} \ap
+ 0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap
+ n)$ for arbitrary $n$.
- The step case is established by a short calculation in forward
- manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
- the thesis, the final result is achieved by transformations involving
- basic arithmetic reasoning (using the Simplifier). The main point is
- where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
- introduced in order to replace a certain subterm. So the
- ``transitivity'' rule involved here is actual \emph{substitution}.
- Also note how the occurrence of ``\dots'' in the subsequent step
- documents the position where the right-hand side of the hypothesis
- got filled in.
+ The step case is established by a short calculation in forward
+ manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
+ the thesis, the final result is achieved by transformations
+ involving basic arithmetic reasoning (using the Simplifier). The
+ main point is where the induction hypothesis $\var{S} \ap n = n
+ \times (n + 1)$ is introduced in order to replace a certain subterm.
+ So the ``transitivity'' rule involved here is actual
+ \emph{substitution}. Also note how the occurrence of ``\dots'' in
+ the subsequent step documents the position where the right-hand side
+ of the hypothesis got filled in.
- \medskip A further notable point here is integration of calculations
- with plain natural deduction. This works so well in Isar for two
- reasons.
- \begin{enumerate}
+ \medskip A further notable point here is integration of calculations
+ with plain natural deduction. This works so well in Isar for two
+ reasons.
+ \begin{enumerate}
+
+ \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+ calculational chains may be just anything. There is nothing special
+ about \isakeyword{have}, so the natural deduction element
+ \isakeyword{assume} works just as well.
- \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
- calculational chains may be just anything. There is nothing special
- about \isakeyword{have}, so the natural deduction element
- \isakeyword{assume} works just as well.
+ \item There are two \emph{separate} primitives for building natural
+ deduction contexts: \isakeyword{fix}~$x$ and
+ \isakeyword{assume}~$A$. Thus it is possible to start reasoning
+ with some new ``arbitrary, but fixed'' elements before bringing in
+ the actual assumption. In contrast, natural deduction is
+ occasionally formalized with basic context elements of the form
+ $x:A$ instead.
- \item There are two \emph{separate} primitives for building natural
- deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
- Thus it is possible to start reasoning with some new ``arbitrary, but
- fixed'' elements before bringing in the actual assumption. In
- contrast, natural deduction is occasionally formalized with basic
- context elements of the form $x:A$ instead.
-
- \end{enumerate}
+ \end{enumerate}
*}
-text {*
- \medskip We derive further summation laws for odds, squares, and
- cubes as follows. The basic technique of induction plus calculation
- is the same as before.
-*}
+text {* \medskip We derive further summation laws for odds, squares,
+ and cubes as follows. The basic technique of induction plus
+ calculation is the same as before. *}
theorem sum_of_odds:
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -98,11 +91,9 @@
finally show "?P (Suc n)" by simp
qed
-text {*
- Subsequently we require some additional tweaking of Isabelle built-in
- arithmetic simplifications, such as bringing in distributivity by
- hand.
-*}
+text {* Subsequently we require some additional tweaking of Isabelle
+ built-in arithmetic simplifications, such as bringing in
+ distributivity by hand. *}
lemmas distrib = add_mult_distrib add_mult_distrib2
@@ -116,7 +107,7 @@
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)
+ (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
finally show "?P (Suc n)" by simp
qed
@@ -134,25 +125,23 @@
finally show "?P (Suc n)" by simp
qed
-text {*
- Comparing these examples with the tactic script version
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
- an important difference of how induction vs.\ simplification is
- applied. While \cite[\S10]{isabelle-ref} advises for these examples
- that ``induction should not be applied until the goal is in the
- simplest form'' this would be a very bad idea in our setting.
+text {* Comparing these examples with the tactic script version
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
+ an important difference of how induction vs.\ simplification is
+ applied. While \cite[\S10]{isabelle-ref} advises for these examples
+ that ``induction should not be applied until the goal is in the
+ simplest form'' this would be a very bad idea in our setting.
- Simplification normalizes all arithmetic expressions involved,
- producing huge intermediate goals. With applying induction
- afterwards, the Isar proof text would have to reflect the emerging
- configuration by appropriate sub-proofs. This would result in badly
- structured, low-level technical reasoning, without any good idea of
- the actual point.
+ Simplification normalizes all arithmetic expressions involved,
+ producing huge intermediate goals. With applying induction
+ afterwards, the Isar proof text would have to reflect the emerging
+ configuration by appropriate sub-proofs. This would result in badly
+ structured, low-level technical reasoning, without any good idea of
+ the actual point.
- \medskip As a general rule of good proof style, automatic methods
- such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
- initial proof methods, but only as terminal ones, solving certain
- goals completely.
-*}
+ \medskip As a general rule of good proof style, automatic methods
+ such as $\idt{simp}$ or $\idt{auto}$ should normally be never used
+ as initial proof methods, but only as terminal ones, solving certain
+ goals completely. *}
end