--- a/src/HOL/Isar_Examples/Basic_Logic.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Tue Oct 07 20:59:46 2014 +0200
@@ -4,19 +4,19 @@
Basic propositional and quantifier reasoning.
*)
-header {* Basic logical reasoning *}
+header \<open>Basic logical reasoning\<close>
theory Basic_Logic
imports Main
begin
-subsection {* Pure backward reasoning *}
+subsection \<open>Pure backward reasoning\<close>
-text {* In order to get a first idea of how Isabelle/Isar proof
+text \<open>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. *}
+ should require little extra explanations.\<close>
lemma I: "A \<longrightarrow> A"
proof
@@ -51,14 +51,14 @@
qed
qed
-text {* Isar provides several ways to fine-tune the reasoning,
+text \<open>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.\<close>
lemma "A \<longrightarrow> A"
proof
@@ -66,42 +66,42 @@
show A by fact+
qed
-text {* In fact, concluding any (sub-)proof already involves solving
+text \<open>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.\<close>
lemma "A \<longrightarrow> A"
proof
qed
-text {* Note that the \isacommand{proof} command refers to the @{text
+text \<open>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. *}
+ proof with empty body, so the proof may be further pruned.\<close>
lemma "A \<longrightarrow> A"
by rule
-text {* Proof by a single rule may be abbreviated as double-dot. *}
+text \<open>Proof by a single rule may be abbreviated as double-dot.\<close>
lemma "A \<longrightarrow> A" ..
-text {* Thus we have arrived at an adequate representation of the
+text \<open>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.} *}
+ introduction.}\<close>
-text {* Let us also reconsider @{text K}. Its statement is composed
+text \<open>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.}\<close>
lemma "A \<longrightarrow> B \<longrightarrow> A"
proof (intro impI)
@@ -109,12 +109,12 @@
show A by fact
qed
-text {* Again, the body may be collapsed. *}
+text \<open>Again, the body may be collapsed.\<close>
lemma "A \<longrightarrow> B \<longrightarrow> A"
by (intro impI)
-text {* Just like @{text rule}, the @{text intro} and @{text elim}
+text \<open>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
@@ -127,18 +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}.\<close>
-subsection {* Variations of backward vs.\ forward reasoning *}
+subsection \<open>Variations of backward vs.\ forward reasoning\<close>
-text {* Certainly, any proof may be performed in backward-style only.
+text \<open>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.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
@@ -150,70 +150,70 @@
qed
qed
-text {* Above, the @{text "conjunct_1/2"} projection rules had to be
+text \<open>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. *}
+ @{text conjE} rule here.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
show "B \<and> A"
proof
- from `A \<and> B` show B ..
- from `A \<and> B` show A ..
+ from \<open>A \<and> B\<close> show B ..
+ from \<open>A \<and> B\<close> show A ..
qed
qed
-text {* In the next version, we move the forward step one level
+text \<open>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.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
then show "B \<and> A"
- proof -- {* rule @{text conjE} of @{text "A \<and> B"} *}
+ proof -- \<open>rule @{text conjE} of @{text "A \<and> B"}\<close>
assume B A
- then show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}
+ then show ?thesis .. -- \<open>rule @{text conjI} of @{text "B \<and> A"}\<close>
qed
qed
-text {* In the subsequent version we flatten the structure of the main
+text \<open>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. *}
+ decomposition step is left as backward.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
- from `A \<and> B` have A ..
- from `A \<and> B` have B ..
- from `B` `A` show "B \<and> A" ..
+ from \<open>A \<and> B\<close> have A ..
+ from \<open>A \<and> B\<close> have B ..
+ from \<open>B\<close> \<open>A\<close> show "B \<and> A" ..
qed
-text {* We can still push forward-reasoning a bit further, even at the
+text \<open>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. *}
+ step to do nothing here, by referring to the ``-'' proof method.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof -
{
assume "A \<and> B"
- from `A \<and> B` have A ..
- from `A \<and> B` have B ..
- from `B` `A` have "B \<and> A" ..
+ from \<open>A \<and> B\<close> have A ..
+ from \<open>A \<and> B\<close> have B ..
+ from \<open>B\<close> \<open>A\<close> have "B \<and> A" ..
}
- then show ?thesis .. -- {* rule @{text impI} *}
+ then show ?thesis .. -- \<open>rule @{text impI}\<close>
qed
-text {* \medskip With these examples we have shifted through a whole
+text \<open>\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
@@ -226,11 +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.\<close>
-text {* For our example the most appropriate way of reasoning is
+text \<open>For our example the most appropriate way of reasoning is
probably the middle one, with conjunction introduction done after
- elimination. *}
+ elimination.\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
@@ -244,32 +244,32 @@
-subsection {* A few examples from ``Introduction to Isabelle'' *}
+subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
-text {* We rephrase some of the basic reasoning examples of
- \cite{isabelle-intro}, using HOL rather than FOL. *}
+text \<open>We rephrase some of the basic reasoning examples of
+ @{cite "isabelle-intro"}, using HOL rather than FOL.\<close>
-subsubsection {* A propositional proof *}
+subsubsection \<open>A propositional proof\<close>
-text {* We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof
+text \<open>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. *}
+ explicit case-analysis on the two \emph{identical} cases.\<close>
lemma "P \<or> P \<longrightarrow> P"
proof
assume "P \<or> P"
then show P
- proof -- {*
+ proof -- \<open>
rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
- *}
+\<close>
assume P show P by fact
next
assume P show P by fact
qed
qed
-text {* Case splits are \emph{not} hardwired into the Isar language as
+text \<open>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.
@@ -289,7 +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.\<close>
lemma "P \<or> P \<longrightarrow> P"
proof
@@ -302,10 +302,10 @@
qed
qed
-text {* Again, the rather vacuous body of the proof may be collapsed.
+text \<open>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. *}
+ double-dot proof as follows.\<close>
lemma "P \<or> P \<longrightarrow> P"
proof
@@ -314,9 +314,9 @@
qed
-subsubsection {* A quantifier proof *}
+subsubsection \<open>A quantifier proof\<close>
-text {* To illustrate quantifier reasoning, let us prove @{text
+text \<open>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.
@@ -326,27 +326,27 @@
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.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
assume "\<exists>x. P (f x)"
then show "\<exists>y. P y"
- proof (rule exE) -- {*
+ proof (rule exE) -- \<open>
rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
- *}
+\<close>
fix a
assume "P (f a)" (is "P ?witness")
then show ?thesis by (rule exI [of P ?witness])
qed
qed
-text {* While explicit rule instantiation may occasionally improve
+text \<open>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.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
@@ -359,10 +359,10 @@
qed
qed
-text {* Explicit @{text \<exists>}-elimination as seen above can become quite
+text \<open>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.\<close>
lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
@@ -371,21 +371,21 @@
then show "\<exists>y. P y" ..
qed
-text {* Technically, \isakeyword{obtain} is similar to
+text \<open>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. *}
+ to the parameters introduced there.\<close>
-subsubsection {* Deriving rules in Isabelle *}
+subsubsection \<open>Deriving rules in Isabelle\<close>
-text {* We derive the conjunction elimination rule from the
+text \<open>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. *}
+ transparently.\<close>
theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
proof -
--- a/src/HOL/Isar_Examples/Cantor.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,16 +2,16 @@
Author: Markus Wenzel, TU Muenchen
*)
-header {* Cantor's Theorem *}
+header \<open>Cantor's Theorem\<close>
theory Cantor
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 \<open>\footnote{This is an Isar version of the final example of
+ the Isabelle/HOL manual @{cite "isabelle-HOL"}.}\<close>
-text {* Cantor's Theorem states that every set has more subsets than
+text \<open>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}}
@@ -22,7 +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}$.\<close>
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
@@ -36,30 +36,30 @@
assume "y \<in> f y"
assume "y \<in> ?S"
then have "y \<notin> f y" ..
- with `y : f y` show ?thesis by contradiction
+ with \<open>y : f y\<close> show ?thesis by contradiction
next
assume "y \<notin> ?S"
assume "y \<notin> f y"
then have "y \<in> ?S" ..
- with `y \<notin> ?S` show ?thesis by contradiction
+ with \<open>y \<notin> ?S\<close> show ?thesis by contradiction
qed
qed
qed
-text {* How much creativity is required? As it happens, Isabelle can
+text \<open>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. *}
+ set theory.\<close>
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
by best
-text {* While this establishes the same theorem internally, we do not
+text \<open>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.\<close>
end
--- a/src/HOL/Isar_Examples/Drinker.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,17 +2,17 @@
Author: Makarius
*)
-header {* The Drinker's Principle *}
+header \<open>The Drinker's Principle\<close>
theory Drinker
imports Main
begin
-text {* Here is another example of classical reasoning: the Drinker's
+text \<open>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.\<close>
lemma de_Morgan:
assumes "\<not> (\<forall>x. P x)"
@@ -25,10 +25,10 @@
proof (rule classical)
assume "\<not> P x"
then have "\<exists>x. \<not> P x" ..
- with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
+ with \<open>\<not> (\<exists>x. \<not> P x)\<close> show ?thesis by contradiction
qed
qed
- with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
+ with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction
qed
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Oct 07 20:59:46 2014 +0200
@@ -4,40 +4,40 @@
Correctness of a simple expression/stack-machine compiler.
*)
-header {* Correctness of a simple expression compiler *}
+header \<open>Correctness of a simple expression compiler\<close>
theory Expr_Compiler
imports Main
begin
-text {* This is a (rather trivial) example of program verification.
+text \<open>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. *}
+ semantics.\<close>
-subsection {* Binary operations *}
+subsection \<open>Binary operations\<close>
-text {* Binary operations are just functions over some type of values.
+text \<open>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. *}
+ ``shallow embedding'' here.\<close>
type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
-subsection {* Expressions *}
+subsection \<open>Expressions\<close>
-text {* The language of expressions is defined as an inductive type,
+text \<open>The language of expressions is defined as an inductive type,
consisting of variables, constants, and binary operations on
- expressions. *}
+ expressions.\<close>
datatype (dead 'adr, dead '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 \<open>Evaluation (wrt.\ some environment of variable assignments) is
+ defined by primitive recursion over the structure of expressions.\<close>
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where
@@ -46,18 +46,18 @@
| "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
-subsection {* Machine *}
+subsection \<open>Machine\<close>
-text {* Next we model a simple stack machine, with three
- instructions. *}
+text \<open>Next we model a simple stack machine, with three
+ instructions.\<close>
datatype (dead 'adr, dead 'val) instr =
Const 'val
| Load 'adr
| Apply "'val binop"
-text {* Execution of a list of stack machine instructions is easily
- defined as follows. *}
+text \<open>Execution of a list of stack machine instructions is easily
+ defined as follows.\<close>
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
where
@@ -73,10 +73,10 @@
where "execute instrs env = hd (exec instrs [] env)"
-subsection {* Compiler *}
+subsection \<open>Compiler\<close>
-text {* We are ready to define the compilation function of expressions
- to lists of stack machine instructions. *}
+text \<open>We are ready to define the compilation function of expressions
+ to lists of stack machine instructions.\<close>
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
where
@@ -85,9 +85,9 @@
| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
-text {* The main result of this development is the correctness theorem
+text \<open>The main result of this development is the correctness theorem
for @{text compile}. We first establish a lemma about @{text exec}
- and list append. *}
+ and list append.\<close>
lemma exec_append:
"exec (xs @ ys) stack env =
@@ -127,11 +127,11 @@
qed
-text {* \bigskip In the proofs above, the @{text simp} method does
+text \<open>\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. *}
+ time. Thus we get a better idea of what is actually going on.\<close>
lemma exec_append':
"exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
@@ -158,7 +158,7 @@
next
case (Load adr)
from Cons show ?case
- by simp -- {* same as above *}
+ by simp -- \<open>same as above\<close>
next
case (Apply fn)
have "exec ((Apply fn # xs) @ ys) s env =
@@ -188,7 +188,7 @@
finally show ?case .
next
case (Constant val s)
- show ?case by simp -- {* same as above *}
+ show ?case by simp -- \<open>same as above\<close>
next
case (Binop fn e1 e2 s)
have "exec (compile (Binop fn e1 e2)) s env =
--- a/src/HOL/Isar_Examples/Fibonacci.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Tue Oct 07 20:59:46 2014 +0200
@@ -12,21 +12,21 @@
(Addison-Wesley, 1989)
*)
-header {* Fib and Gcd commute *}
+header \<open>Fib and Gcd commute\<close>
theory Fibonacci
imports "../Number_Theory/Primes"
begin
-text_raw {* \footnote{Isar version by Gertrud Bauer. Original tactic
+text_raw \<open>\footnote{Isar version by Gertrud Bauer. Original tactic
script by Larry Paulson. A few proofs of laws taken from
- \cite{Concrete-Math}.} *}
+ @{cite "Concrete-Math"}.}\<close>
declare One_nat_def [simp]
-subsection {* Fibonacci numbers *}
+subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0"
@@ -37,7 +37,7 @@
by (induct n rule: fib.induct) simp_all
-text {* Alternative induction rule. *}
+text \<open>Alternative induction rule.\<close>
theorem fib_induct:
fixes n :: nat
@@ -45,14 +45,14 @@
by (induct rule: fib.induct) simp_all
-subsection {* Fib and gcd commute *}
+subsection \<open>Fib and gcd commute\<close>
-text {* A few laws taken from \cite{Concrete-Math}. *}
+text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
lemma fib_add:
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
(is "?P n")
- -- {* see \cite[page 280]{Concrete-Math} *}
+ -- \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
@@ -93,7 +93,7 @@
assume "0 < n"
then have "gcd (n * k + m) n = gcd n (m mod n)"
by (simp add: gcd_non_0_nat add.commute)
- also from `0 < n` have "\<dots> = gcd m n"
+ also from \<open>0 < n\<close> have "\<dots> = gcd m n"
by (simp add: gcd_non_0_nat)
finally show ?thesis .
qed
@@ -124,7 +124,7 @@
proof -
have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
by (simp add: gcd_fib_add)
- also from `m \<le> n` have "n - m + m = n"
+ also from \<open>m \<le> n\<close> have "n - m + m = n"
by simp
finally show ?thesis .
qed
@@ -145,12 +145,12 @@
next
case False
then have "m \<le> n" by simp
- from `0 < m` and False have "n - m < n"
+ from \<open>0 < m\<close> 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
also have "\<dots> = gcd (fib m) (fib n)"
- using `m \<le> n` by (rule gcd_fib_diff)
+ using \<open>m \<le> n\<close> by (rule gcd_fib_diff)
finally have "gcd (fib m) (fib ((n - m) mod m)) =
gcd (fib m) (fib n)" .
with False show ?thesis by simp
--- a/src/HOL/Isar_Examples/Group.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Group.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,26 +2,26 @@
Author: Markus Wenzel, TU Muenchen
*)
-header {* Basic group theory *}
+header \<open>Basic group theory\<close>
theory Group
imports Main
begin
-subsection {* Groups and calculational reasoning *}
+subsection \<open>Groups and calculational reasoning\<close>
-text {* Groups over signature $({\times} :: \alpha \To \alpha \To
+text \<open>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. *}
+ parent class $\idt{times}$ is provided by the basic HOL theory.\<close>
class group = times + one + inverse +
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 \<open>The group axioms only state the properties of left one and
+ inverse, the right versions may be derived as follows.\<close>
theorem (in group) group_right_inverse: "x * inverse x = 1"
proof -
@@ -44,9 +44,9 @@
finally show ?thesis .
qed
-text {* With \name{group-right-inverse} already available,
+text \<open>With \name{group-right-inverse} already available,
\name{group-right-one}\label{thm:group-right-one} is now established
- much easier. *}
+ much easier.\<close>
theorem (in group) group_right_one: "x * 1 = x"
proof -
@@ -61,7 +61,7 @@
finally show ?thesis .
qed
-text {* \medskip The calculational proof style above follows typical
+text \<open>\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
@@ -81,8 +81,7 @@
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.
-*}
+ demonstrated below.\<close>
theorem (in group) "x * 1 = x"
proof -
@@ -90,58 +89,57 @@
by (simp only: group_left_inverse)
note calculation = this
- -- {* first calculational step: init calculation register *}
+ -- \<open>first calculational step: init calculation register\<close>
have "\<dots> = x * inverse x * x"
by (simp only: group_assoc)
note calculation = trans [OF calculation this]
- -- {* general calculational step: compose with transitivity rule *}
+ -- \<open>general calculational step: compose with transitivity rule\<close>
have "\<dots> = 1 * x"
by (simp only: group_right_inverse)
note calculation = trans [OF calculation this]
- -- {* general calculational step: compose with transitivity rule *}
+ -- \<open>general calculational step: compose with transitivity rule\<close>
have "\<dots> = x"
by (simp only: group_left_one)
note calculation = trans [OF calculation this]
- -- {* final calculational step: compose with transitivity rule \dots *}
+ -- \<open>final calculational step: compose with transitivity rule \dots\<close>
from calculation
- -- {* \dots\ and pick up the final result *}
+ -- \<open>\dots\ and pick up the final result\<close>
show ?thesis .
qed
-text {* Note that this scheme of calculations is not restricted to
+text \<open>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. *}
+ unification.\<close>
-subsection {* Groups as monoids *}
+subsection \<open>Groups as monoids\<close>
-text {* Monoids over signature $({\times} :: \alpha \To \alpha \To
- \alpha, \idt{one} :: \alpha)$ are defined like this.
-*}
+text \<open>Monoids over signature $({\times} :: \alpha \To \alpha \To
+ \alpha, \idt{one} :: \alpha)$ are defined like this.\<close>
class monoid = times + one +
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
+text \<open>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. *}
+ $\idt{group} \subseteq \idt{monoid}$ properly as follows.\<close>
instance group < monoid
by intro_classes
@@ -149,18 +147,18 @@
rule group_left_one,
rule group_right_one)
-text {* The \isacommand{instance} command actually is a version of
+text \<open>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. *}
+ type signature extension behind the scenes.\<close>
-subsection {* More theorems of group theory *}
+subsection \<open>More theorems of group theory\<close>
-text {* The one element is already uniquely determined by preserving
- an \emph{arbitrary} group element. *}
+text \<open>The one element is already uniquely determined by preserving
+ an \emph{arbitrary} group element.\<close>
theorem (in group) group_one_equality:
assumes eq: "e * x = x"
@@ -179,7 +177,7 @@
finally show ?thesis .
qed
-text {* Likewise, the inverse is already determined by the cancel property. *}
+text \<open>Likewise, the inverse is already determined by the cancel property.\<close>
theorem (in group) group_inverse_equality:
assumes eq: "x' * x = 1"
@@ -198,7 +196,7 @@
finally show ?thesis .
qed
-text {* The inverse operation has some further characteristic properties. *}
+text \<open>The inverse operation has some further characteristic properties.\<close>
theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
proof (rule group_inverse_equality)
--- a/src/HOL/Isar_Examples/Group_Context.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,13 +2,13 @@
Author: Makarius
*)
-header {* Some algebraic identities derived from group axioms -- theory context version *}
+header \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
theory Group_Context
imports Main
begin
-text {* hypothetical group axiomatization *}
+text \<open>hypothetical group axiomatization\<close>
context
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
@@ -19,7 +19,7 @@
and left_inverse: "inverse x ** x = one"
begin
-text {* some consequences *}
+text \<open>some consequences\<close>
lemma right_inverse: "x ** inverse x = one"
proof -
--- a/src/HOL/Isar_Examples/Group_Notepad.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,7 +2,7 @@
Author: Makarius
*)
-header {* Some algebraic identities derived from group axioms -- proof notepad version *}
+header \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
theory Group_Notepad
imports Main
@@ -10,7 +10,7 @@
notepad
begin
- txt {* hypothetical group axiomatization *}
+ txt \<open>hypothetical group axiomatization\<close>
fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
and one :: "'a"
@@ -19,7 +19,7 @@
and left_one: "\<And>x. one ** x = x"
and left_inverse: "\<And>x. inverse x ** x = one"
- txt {* some consequences *}
+ txt \<open>some consequences\<close>
have right_inverse: "\<And>x. x ** inverse x = one"
proof -
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Tue Oct 07 20:59:46 2014 +0200
@@ -4,19 +4,19 @@
A formulation of Hoare logic suitable for Isar.
*)
-header {* Hoare Logic *}
+header \<open>Hoare Logic\<close>
theory Hoare
imports Main
begin
-subsection {* Abstract syntax and semantics *}
+subsection \<open>Abstract syntax and semantics\<close>
-text {* The following abstract syntax and semantics of Hoare Logic
+text \<open>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 @{file "~~/src/HOL/Hoare"} and
- \cite{Nipkow:1998:Winskel}. *}
+ @{cite \<open>\S6\<close> "Winskel:1993"}. See also @{file "~~/src/HOL/Hoare"} and
+ @{cite "Nipkow:1998:Winskel"}.\<close>
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
@@ -58,16 +58,16 @@
by (simp add: Valid_def)
-subsection {* Primitive Hoare rules *}
+subsection \<open>Primitive Hoare rules\<close>
-text {* From the semantics defined above, we derive the standard set
- of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.
+text \<open>From the semantics defined above, we derive the standard set
+ of primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "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}. *}
+ and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.\<close>
theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
proof
@@ -78,10 +78,8 @@
with s show "s' \<in> P" by simp
qed
-text {*
- The rules for sequential commands and semantic consequences are
- established in a straight forward manner as follows.
-*}
+text \<open>The rules for sequential commands and semantic consequences are
+ established in a straight forward manner as follows.\<close>
theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
proof
@@ -106,9 +104,9 @@
with QQ' show "s' \<in> Q'" ..
qed
-text {* The rule for conditional commands is directly reflected by the
+text \<open>The rule for conditional commands is directly reflected by the
corresponding semantics; in the proof we just have to look closely
- which cases apply. *}
+ which cases apply.\<close>
theorem cond:
assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
@@ -136,12 +134,12 @@
qed
qed
-text {* The @{text while} rule is slightly less trivial --- it is the
+text \<open>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}. *}
+ of the semantics of \texttt{WHILE}.\<close>
theorem while:
assumes body: "\<turnstile> (P \<inter> b) c P"
@@ -165,9 +163,9 @@
qed
-subsection {* Concrete syntax for assertions *}
+subsection \<open>Concrete syntax for assertions\<close>
-text {* We now introduce concrete syntax for describing commands (with
+text \<open>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
@@ -176,9 +174,9 @@
would select (or even update) components from the state.
We will see some examples later in the concrete rules and
- applications. *}
+ applications.\<close>
-text {* The following specification of syntax and translations is for
+text \<open>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
@@ -186,7 +184,7 @@
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 @{ML Syntax_Trans.quote_tr}, and
- @{ML Syntax_Trans.quote_tr'},). *}
+ @{ML Syntax_Trans.quote_tr'},).\<close>
syntax
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
@@ -208,19 +206,19 @@
"WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
-parse_translation {*
+parse_translation \<open>
let
fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
| quote_tr ts = raise TERM ("quote_tr", ts);
in [(@{syntax_const "_quote"}, K quote_tr)] end
-*}
+\<close>
-text {* As usual in Isabelle syntax translations, the part for
+text \<open>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. *}
+ things for yourself.\<close>
-print_translation {*
+print_translation \<open>
let
fun quote_tr' f (t :: ts) =
Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
@@ -242,18 +240,18 @@
(@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
(@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
end
-*}
+\<close>
-subsection {* Rules for single-step proof \label{sec:hoare-isar} *}
+subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
-text {* We are now ready to introduce a set of Hoare rules to be used
+text \<open>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. *}
+ or predicates. Reversed order is supported as well.\<close>
lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
by (unfold Valid_def) blast
@@ -280,10 +278,10 @@
by (simp add: Valid_def)
-text {* Identity and basic assignments.\footnote{The $\idt{hoare}$
+text \<open>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.} *}
+ additional verification conditions.}\<close>
lemma skip [intro?]: "\<turnstile> P SKIP P"
proof -
@@ -294,9 +292,9 @@
lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
by (rule basic)
-text {* Note that above formulation of assignment corresponds to our
+text \<open>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
+ 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
@@ -304,17 +302,17 @@
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.} *}
+ instance of record fields introduced so far.}\<close>
-text {* Sequential composition --- normalizing with associativity
- achieves proper of chunks of code verified separately. *}
+text \<open>Sequential composition --- normalizing with associativity
+ achieves proper of chunks of code verified separately.\<close>
lemmas [trans, intro?] = seq
lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
by (auto simp add: Valid_def)
-text {* Conditional statements. *}
+text \<open>Conditional statements.\<close>
lemmas [trans, intro?] = cond
@@ -324,7 +322,7 @@
\<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
by (rule cond) (simp_all add: Valid_def)
-text {* While statements --- with optional invariant. *}
+text \<open>While statements --- with optional invariant.\<close>
lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
by (rule while)
@@ -344,9 +342,9 @@
by (simp add: while Collect_conj_eq Collect_neg_eq)
-subsection {* Verification conditions \label{sec:hoare-vcg} *}
+subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
-text {* We now load the \emph{original} ML file for proof scripts and
+text \<open>We now load the \emph{original} ML file for proof scripts and
tactic definition for the Hoare Verification Condition Generator
(see @{file "~~/src/HOL/Hoare/"}). As far as we
are concerned here, the result is a proof method \name{hoare}, which
@@ -355,7 +353,7 @@
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. *}
+ with meta-variables or parameters, for example.\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp add: Valid_def)
@@ -393,11 +391,11 @@
ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
-method_setup hoare = {*
- Scan.succeed (fn ctxt =>
+method_setup hoare =
+ \<open>Scan.succeed (fn ctxt =>
(SIMPLE_METHOD'
- (Hoare.hoare_tac ctxt
- (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] ))))) *}
+ (Hoare.hoare_tac ctxt
+ (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\<close>
"verification condition generator for Hoare logic"
end
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Oct 07 20:59:46 2014 +0200
@@ -1,14 +1,14 @@
-header {* Using Hoare Logic *}
+header \<open>Using Hoare Logic\<close>
theory Hoare_Ex
imports Hoare
begin
-subsection {* State spaces *}
+subsection \<open>State spaces\<close>
-text {* First of all we provide a store of program variables that
+text \<open>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. *}
+ things may happen when attempting to work with undeclared variables.\<close>
record vars =
I :: nat
@@ -16,29 +16,29 @@
N :: nat
S :: nat
-text {* While all of our variables happen to have the same type,
+text \<open>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. *}
+ state space later.\<close>
-subsection {* Basic examples *}
+subsection \<open>Basic examples\<close>
-text {* We look at few trivialities involving assignment and
+text \<open>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. *}
+ our formulation of Hoare Logic.\<close>
-text {* Using the basic @{text assign} rule directly is a bit
- cumbersome. *}
+text \<open>Using the basic @{text assign} rule directly is a bit
+ cumbersome.\<close>
lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
by (rule assign)
-text {* Certainly we want the state modification already done, e.g.\
+text \<open>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. *}
+ ``obvious'' consequences as well.\<close>
lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
by hoare
@@ -67,10 +67,10 @@
\<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
by hoare simp
-text {* It is important to note that statements like the following one
+text \<open>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. *}
+ relating record selectors and updates schematically.\<close>
lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
by hoare
@@ -80,13 +80,13 @@
lemma
"Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
- -- {* same statement without concrete syntax *}
+ -- \<open>same statement without concrete syntax\<close>
oops
-text {* In the following assignments we make use of the consequence
+text \<open>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. *}
+ \name{hoare} method is able to handle this case, too.\<close>
lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
@@ -100,8 +100,8 @@
lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
- -- {* inclusion of assertions expressed in ``pure'' logic, *}
- -- {* without mentioning the state space *}
+ -- \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
+ -- \<open>without mentioning the state space\<close>
by simp
also have "\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
by hoare
@@ -112,12 +112,12 @@
by hoare simp
-subsection {* Multiplication by addition *}
+subsection \<open>Multiplication by addition\<close>
-text {* We now do some basic examples of actual \texttt{WHILE}
+text \<open>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. *}
+ structured proof based on single-step Hoare rules.\<close>
lemma
"\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -141,10 +141,10 @@
finally show ?thesis .
qed
-text {* The subsequent version of the proof applies the @{text hoare}
+text \<open>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. *}
+ specify the \texttt{WHILE} loop invariant in the original statement.\<close>
lemma
"\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -155,17 +155,17 @@
by hoare auto
-subsection {* Summing natural numbers *}
+subsection \<open>Summing natural numbers\<close>
-text {* We verify an imperative program to sum natural numbers up to a
+text \<open>We verify an imperative program to sum natural numbers up to a
given limit. First some functional definition for proper
- specification of the problem. *}
+ specification of the problem.\<close>
-text {* The following proof is quite explicit in the individual steps
+text \<open>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. *}
+ the state space.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -203,9 +203,9 @@
finally show ?thesis .
qed
-text {* The next version uses the @{text hoare} method, while still
+text \<open>The next version uses the @{text hoare} method, while still
explaining the resulting proof obligations in an abstract,
- structured manner. *}
+ structured manner.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -235,8 +235,8 @@
qed
qed
-text {* Certainly, this proof may be done fully automatic as well,
- provided that the invariant is given beforehand. *}
+text \<open>Certainly, this proof may be done fully automatic as well,
+ provided that the invariant is given beforehand.\<close>
theorem
"\<turnstile> \<lbrace>True\<rbrace>
@@ -251,10 +251,10 @@
by hoare auto
-subsection {* Time *}
+subsection \<open>Time\<close>
-text {* A simple embedding of time in Hoare logic: function @{text
- timeit} inserts an extra variable to keep track of the elapsed time. *}
+text \<open>A simple embedding of time in Hoare logic: function @{text
+ timeit} inserts an extra variable to keep track of the elapsed time.\<close>
record tstate = time :: nat
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Oct 07 20:59:46 2014 +0200
@@ -4,17 +4,17 @@
Typical textbook proof example.
*)
-header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
+header \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
theory Knaster_Tarski
imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin
-subsection {* Prose version *}
+subsection \<open>Prose version\<close>
-text {* According to the textbook \cite[pages
- 93--94]{davey-priestley}, the Knaster-Tarski fixpoint theorem is as
+text \<open>According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"},
+ the Knaster-Tarski fixpoint theorem is as
follows.\footnote{We have dualized the argument, and tuned the
notation a little bit.}
@@ -28,16 +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)"}.\<close>
-subsection {* Formal versions *}
+subsection \<open>Formal versions\<close>
-text {* The Isar proof below closely follows the original
+text \<open>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. *}
+ and several bends in the course of reasoning.\<close>
theorem Knaster_Tarski:
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -52,8 +52,8 @@
fix x
assume "x \<in> ?H"
then have "?a \<le> x" by (rule Inf_lower)
- with `mono f` have "f ?a \<le> f x" ..
- also from `x \<in> ?H` have "\<dots> \<le> x" ..
+ with \<open>mono f\<close> have "f ?a \<le> f x" ..
+ also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
finally have "f ?a \<le> x" .
}
then have "f ?a \<le> ?a" by (rule Inf_greatest)
@@ -61,13 +61,13 @@
also presume "\<dots> \<le> f ?a"
finally (order_antisym) show ?thesis .
}
- from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+ from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
then have "f ?a \<in> ?H" ..
then show "?a \<le> f ?a" by (rule Inf_lower)
qed
qed
-text {* Above we have used several advanced Isar language elements,
+text \<open>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.
@@ -75,7 +75,7 @@
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.\<close>
theorem Knaster_Tarski':
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -91,13 +91,13 @@
fix x
assume "x \<in> ?H"
then have "?a \<le> x" by (rule Inf_lower)
- with `mono f` have "f ?a \<le> f x" ..
- also from `x \<in> ?H` have "\<dots> \<le> x" ..
+ with \<open>mono f\<close> have "f ?a \<le> f x" ..
+ also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
finally show "f ?a \<le> x" .
qed
show "?a \<le> f ?a"
proof (rule Inf_lower)
- from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+ from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
then show "f ?a \<in> ?H" ..
qed
qed
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Tue Oct 07 20:59:46 2014 +0200
@@ -3,16 +3,16 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
*)
-header {* The Mutilated Checker Board Problem *}
+header \<open>The Mutilated Checker Board Problem\<close>
theory Mutilated_Checkerboard
imports Main
begin
-text {* The Mutilated Checker Board Problem, formalized inductively.
- See \cite{paulson-mutilated-board} for the original tactic script version. *}
+text \<open>The Mutilated Checker Board Problem, formalized inductively.
+ See @{cite "paulson-mutilated-board"} for the original tactic script version.\<close>
-subsection {* Tilings *}
+subsection \<open>Tilings\<close>
inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
for A :: "'a set set"
@@ -21,7 +21,7 @@
| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
-text "The union of two disjoint tilings is a tiling."
+text \<open>The union of two disjoint tilings is a tiling.\<close>
lemma tiling_Un:
assumes "t \<in> tiling A"
@@ -30,21 +30,21 @@
shows "t \<union> u \<in> tiling A"
proof -
let ?T = "tiling A"
- from `t \<in> ?T` and `t \<inter> u = {}`
+ from \<open>t \<in> ?T\<close> and \<open>t \<inter> u = {}\<close>
show "t \<union> u \<in> ?T"
proof (induct t)
case empty
- with `u \<in> ?T` show "{} \<union> u \<in> ?T" by simp
+ with \<open>u \<in> ?T\<close> show "{} \<union> u \<in> ?T" by simp
next
case (Un a t)
show "(a \<union> t) \<union> u \<in> ?T"
proof -
have "a \<union> (t \<union> u) \<in> ?T"
- using `a \<in> A`
+ using \<open>a \<in> A\<close>
proof (rule tiling.Un)
- from `(a \<union> t) \<inter> u = {}` have "t \<inter> u = {}" by blast
+ from \<open>(a \<union> t) \<inter> u = {}\<close> have "t \<inter> u = {}" by blast
then show "t \<union> u \<in> ?T" by (rule Un)
- from `a \<subseteq> - t` and `(a \<union> t) \<inter> u = {}`
+ from \<open>a \<subseteq> - t\<close> and \<open>(a \<union> t) \<inter> u = {}\<close>
show "a \<subseteq> - (t \<union> u)" by blast
qed
also have "a \<union> (t \<union> u) = (a \<union> t) \<union> u"
@@ -55,7 +55,7 @@
qed
-subsection {* Basic properties of ``below'' *}
+subsection \<open>Basic properties of ``below''\<close>
definition below :: "nat \<Rightarrow> nat set"
where "below n = {i. i < n}"
@@ -77,7 +77,7 @@
lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
-subsection {* Basic properties of ``evnodd'' *}
+subsection \<open>Basic properties of ``evnodd''\<close>
definition evnodd :: "(nat \<times> nat) set \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
where "evnodd A b = A \<inter> {(i, j). (i + j) mod 2 = b}"
@@ -109,7 +109,7 @@
by (simp add: evnodd_def)
-subsection {* Dominoes *}
+subsection \<open>Dominoes\<close>
inductive_set domino :: "(nat \<times> nat) set set"
where
@@ -164,7 +164,7 @@
shows "\<exists>i j. evnodd d b = {(i, j)}" (is "?P d")
using assms
proof induct
- from `b < 2` have b_cases: "b = 0 \<or> b = 1" by arith
+ from \<open>b < 2\<close> have b_cases: "b = 0 \<or> b = 1" by arith
fix i j
note [simp] = evnodd_empty evnodd_insert mod_Suc
from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
@@ -182,7 +182,7 @@
qed
-subsection {* Tilings of dominoes *}
+subsection \<open>Tilings of dominoes\<close>
lemma tiling_domino_finite:
assumes t: "t \<in> tiling domino" (is "t \<in> ?T")
@@ -193,7 +193,7 @@
fix a t assume "?F t"
assume "a \<in> domino"
then have "?F a" by (rule domino_finite)
- from this and `?F t` show "?F (a \<union> t)" by (rule finite_UnI)
+ from this and \<open>?F t\<close> show "?F (a \<union> t)" by (rule finite_UnI)
qed
lemma tiling_domino_01:
@@ -206,8 +206,8 @@
next
case (Un a t)
let ?e = evnodd
- note hyp = `card (?e t 0) = card (?e t 1)`
- and at = `a \<subseteq> - t`
+ note hyp = \<open>card (?e t 0) = card (?e t 1)\<close>
+ and at = \<open>a \<subseteq> - t\<close>
have card_suc:
"\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
proof -
@@ -216,14 +216,14 @@
have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
also obtain i j where e: "?e a b = {(i, j)}"
proof -
- from `a \<in> domino` and `b < 2`
+ from \<open>a \<in> domino\<close> and \<open>b < 2\<close>
have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton)
then show ?thesis by (blast intro: that)
qed
also have "\<dots> \<union> ?e t b = insert (i, j) (?e t b)" by simp
also have "card \<dots> = Suc (card (?e t b))"
proof (rule card_insert_disjoint)
- from `t \<in> tiling domino` have "finite t"
+ from \<open>t \<in> tiling domino\<close> have "finite t"
by (rule tiling_domino_finite)
then show "finite (?e t b)"
by (rule evnodd_finite)
@@ -240,7 +240,7 @@
qed
-subsection {* Main theorem *}
+subsection \<open>Main theorem\<close>
definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
where
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Oct 07 20:59:46 2014 +0200
@@ -1,10 +1,10 @@
-header {* Nested datatypes *}
+header \<open>Nested datatypes\<close>
theory Nested_Datatype
imports Main
begin
-subsection {* Terms and substitution *}
+subsection \<open>Terms and substitution\<close>
datatype ('a, 'b) "term" =
Var 'a
@@ -20,7 +20,7 @@
lemmas subst_simps = subst_term.simps subst_term_list.simps
-text {* \medskip A simple lemma about composition of substitutions. *}
+text \<open>\medskip A simple lemma about composition of substitutions.\<close>
lemma
"subst_term (subst_term f1 \<circ> f2) t =
@@ -52,7 +52,7 @@
qed
-subsection {* Alternative induction *}
+subsection \<open>Alternative induction\<close>
lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
proof (induct t rule: term.induct)
--- a/src/HOL/Isar_Examples/Peirce.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,13 +2,13 @@
Author: Markus Wenzel, TU Muenchen
*)
-header {* Peirce's Law *}
+header \<open>Peirce's Law\<close>
theory Peirce
imports Main
begin
-text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
+text \<open>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.
@@ -17,7 +17,7 @@
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.} *}
+ well.}\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -28,13 +28,13 @@
have "A \<longrightarrow> B"
proof
assume A
- with `\<not> A` show B by contradiction
+ with \<open>\<not> A\<close> show B by contradiction
qed
- with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
+ with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
qed
qed
-text {* In the subsequent version the reasoning is rearranged by means
+text \<open>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.
@@ -46,7 +46,7 @@
\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. *}
+ are solved immediately.\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -54,18 +54,18 @@
show A
proof (rule classical)
presume "A \<longrightarrow> B"
- with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
+ with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
next
assume "\<not> A"
show "A \<longrightarrow> B"
proof
assume A
- with `\<not> A` show B by contradiction
+ with \<open>\<not> A\<close> show B by contradiction
qed
qed
qed
-text {* Note that the goals stemming from weak assumptions may be even
+text \<open>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
@@ -80,6 +80,6 @@
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. *}
+ eventually demanding even some backtracking.\<close>
end
--- a/src/HOL/Isar_Examples/Puzzle.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy Tue Oct 07 20:59:46 2014 +0200
@@ -1,16 +1,16 @@
-header {* An old chestnut *}
+header \<open>An old chestnut\<close>
theory Puzzle
imports Main
begin
-text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''.
+text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''.
Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
- script by Tobias Nipkow.} *}
+ script by Tobias Nipkow.}\<close>
-text {* \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$
+text \<open>\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. *}
+ Demonstrate that $f$ is the identity.\<close>
theorem
assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
@@ -28,7 +28,7 @@
also from f_ax have "\<dots> < f n" by (simp only: Suc)
finally have "f m < f n" .
with less have "m \<le> f m" .
- also note `\<dots> < f n`
+ also note \<open>\<dots> < f n\<close>
finally have "m < f n" .
then have "n \<le> f n" by (simp only: Suc)
then show ?thesis .
--- a/src/HOL/Isar_Examples/Summation.thy Tue Oct 07 20:43:18 2014 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy Tue Oct 07 20:59:46 2014 +0200
@@ -2,23 +2,23 @@
Author: Markus Wenzel
*)
-header {* Summing natural numbers *}
+header \<open>Summing natural numbers\<close>
theory Summation
imports Main
begin
-text {* Subsequently, we prove some summation laws of natural numbers
+text \<open>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. *}
+ with calculational proof.\<close>
-subsection {* Summation laws *}
+subsection \<open>Summation laws\<close>
-text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times
+text \<open>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$. *}
+ equation multiplied by $2$.\<close>
theorem sum_of_naturals:
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -35,7 +35,7 @@
by simp
qed
-text {* The above proof is a typical instance of mathematical
+text \<open>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
@@ -71,11 +71,11 @@
$x:A$ instead.
\end{enumerate}
-*}
+\<close>
-text {* \medskip We derive further summation laws for odds, squares,
+text \<open>\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. *}
+ calculation is the same as before.\<close>
theorem sum_of_odds:
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -93,9 +93,9 @@
by simp
qed
-text {* Subsequently we require some additional tweaking of Isabelle
+text \<open>Subsequently we require some additional tweaking of Isabelle
built-in arithmetic simplifications, such as bringing in
- distributivity by hand. *}
+ distributivity by hand.\<close>
lemmas distrib = add_mult_distrib add_mult_distrib2
@@ -132,7 +132,7 @@
by simp
qed
-text {* Note that in contrast to older traditions of tactical proof
+text \<open>Note that in contrast to older traditions of tactical proof
scripts, the structured proof applies induction on the original,
unsimplified statement. This allows to state the induction cases
robustly and conveniently. Simplification (or other automated)
@@ -143,6 +143,6 @@
$\idt{simp}$ or $\idt{auto}$ should normally be never used as
initial proof methods with a nested sub-proof to address the
automatically produced situation, but only as terminal ones to solve
- sub-problems. *}
+ sub-problems.\<close>
end