--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Sun Aug 06 15:26:53 2000 +0200
@@ -10,10 +10,10 @@
a fixed set of binary operations: instead the expression contains the
appropriate function itself.%
\end{isamarkuptext}%
-\isacommand{types}~'v~binop~=~{"}'v~{\isasymRightarrow}~'v~{\isasymRightarrow}~'v{"}\isanewline
-\isacommand{datatype}~('a,'v)expr~=~Cex~'v\isanewline
-~~~~~~~~~~~~~~~~~~~~~|~Vex~'a\isanewline
-~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}%
+\isacommand{types}\ 'v\ binop\ =\ {"}'v\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ 'v{"}\isanewline
+\isacommand{datatype}\ ('a,'v)expr\ =\ Cex\ 'v\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Vex\ 'a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Bex\ {"}'v\ binop{"}\ \ {"}('a,'v)expr{"}\ \ {"}('a,'v)expr{"}%
\begin{isamarkuptext}%
\noindent
The three constructors represent constants, variables and the application of
@@ -22,20 +22,20 @@
The value of an expression w.r.t.\ an environment that maps variables to
values is easily defined:%
\end{isamarkuptext}%
-\isacommand{consts}~value~::~{"}('a,'v)expr~{\isasymRightarrow}~('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~'v{"}\isanewline
+\isacommand{consts}\ value\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'v)\ {\isasymRightarrow}\ 'v{"}\isanewline
\isacommand{primrec}\isanewline
-{"}value~(Cex~v)~env~=~v{"}\isanewline
-{"}value~(Vex~a)~env~=~env~a{"}\isanewline
-{"}value~(Bex~f~e1~e2)~env~=~f~(value~e1~env)~(value~e2~env){"}%
+{"}value\ (Cex\ v)\ env\ =\ v{"}\isanewline
+{"}value\ (Vex\ a)\ env\ =\ env\ a{"}\isanewline
+{"}value\ (Bex\ f\ e1\ e2)\ env\ =\ f\ (value\ e1\ env)\ (value\ e2\ env){"}%
\begin{isamarkuptext}%
The stack machine has three instructions: load a constant value onto the
stack, load the contents of a certain address onto the stack, and apply a
binary operation to the two topmost elements of the stack, replacing them by
the result. As for \isa{expr}, addresses and values are type parameters:%
\end{isamarkuptext}%
-\isacommand{datatype}~('a,'v)~instr~=~Const~'v\isanewline
-~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline
-~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}%
+\isacommand{datatype}\ ('a,'v)\ instr\ =\ Const\ 'v\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Load\ 'a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Apply\ {"}'v\ binop{"}%
\begin{isamarkuptext}%
The execution of the stack machine is modelled by a function
\isa{exec} that takes a list of instructions, a store (modelled as a
@@ -44,13 +44,13 @@
and returns the stack at the end of the execution---the store remains
unchanged:%
\end{isamarkuptext}%
-\isacommand{consts}~exec~::~{"}('a,'v)instr~list~{\isasymRightarrow}~('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~'v~list{"}\isanewline
+\isacommand{consts}\ exec\ ::\ {"}('a,'v)instr\ list\ {\isasymRightarrow}\ ('a{\isasymRightarrow}'v)\ {\isasymRightarrow}\ 'v\ list\ {\isasymRightarrow}\ 'v\ list{"}\isanewline
\isacommand{primrec}\isanewline
-{"}exec~[]~s~vs~=~vs{"}\isanewline
-{"}exec~(i\#is)~s~vs~=~(case~i~of\isanewline
-~~~~Const~v~~{\isasymRightarrow}~exec~is~s~(v\#vs)\isanewline
-~~|~Load~a~~~{\isasymRightarrow}~exec~is~s~((s~a)\#vs)\isanewline
-~~|~Apply~f~~{\isasymRightarrow}~exec~is~s~((f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs)))){"}%
+{"}exec\ []\ s\ vs\ =\ vs{"}\isanewline
+{"}exec\ (i\#is)\ s\ vs\ =\ (case\ i\ of\isanewline
+\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ (v\#vs)\isanewline
+\ \ |\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ ((s\ a)\#vs)\isanewline
+\ \ |\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ ((f\ (hd\ vs)\ (hd(tl\ vs)))\#(tl(tl\ vs)))){"}%
\begin{isamarkuptext}%
\noindent
Recall that \isa{hd} and \isa{tl}
@@ -64,29 +64,29 @@
The compiler is a function from expressions to a list of instructions. Its
definition is pretty much obvious:%
\end{isamarkuptext}%
-\isacommand{consts}~comp~::~{"}('a,'v)expr~{\isasymRightarrow}~('a,'v)instr~list{"}\isanewline
+\isacommand{consts}\ comp\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a,'v)instr\ list{"}\isanewline
\isacommand{primrec}\isanewline
-{"}comp~(Cex~v)~~~~~~~=~[Const~v]{"}\isanewline
-{"}comp~(Vex~a)~~~~~~~=~[Load~a]{"}\isanewline
-{"}comp~(Bex~f~e1~e2)~=~(comp~e2)~@~(comp~e1)~@~[Apply~f]{"}%
+{"}comp\ (Cex\ v)\ \ \ \ \ \ \ =\ [Const\ v]{"}\isanewline
+{"}comp\ (Vex\ a)\ \ \ \ \ \ \ =\ [Load\ a]{"}\isanewline
+{"}comp\ (Bex\ f\ e1\ e2)\ =\ (comp\ e2)\ @\ (comp\ e1)\ @\ [Apply\ f]{"}%
\begin{isamarkuptext}%
Now we have to prove the correctness of the compiler, i.e.\ that the
execution of a compiled expression results in the value of the expression:%
\end{isamarkuptext}%
-\isacommand{theorem}~{"}exec~(comp~e)~s~[]~=~[value~e~s]{"}%
+\isacommand{theorem}\ {"}exec\ (comp\ e)\ s\ []\ =\ [value\ e\ s]{"}%
\begin{isamarkuptext}%
\noindent
This theorem needs to be generalized to%
\end{isamarkuptext}%
-\isacommand{theorem}~{"}{\isasymforall}vs.~exec~(comp~e)~s~vs~=~(value~e~s)~\#~vs{"}%
+\isacommand{theorem}\ {"}{\isasymforall}vs.\ exec\ (comp\ e)\ s\ vs\ =\ (value\ e\ s)\ \#\ vs{"}%
\begin{isamarkuptxt}%
\noindent
which is proved by induction on \isa{e} followed by simplification, once
we have the following lemma about executing the concatenation of two
instruction sequences:%
\end{isamarkuptxt}%
-\isacommand{lemma}~exec\_app[simp]:\isanewline
-~~{"}{\isasymforall}vs.~exec~(xs@ys)~s~vs~=~exec~ys~s~(exec~xs~s~vs){"}%
+\isacommand{lemma}\ exec\_app[simp]:\isanewline
+\ \ {"}{\isasymforall}vs.\ exec\ (xs@ys)\ s\ vs\ =\ exec\ ys\ s\ (exec\ xs\ s\ vs){"}%
\begin{isamarkuptxt}%
\noindent
This requires induction on \isa{xs} and ordinary simplification for the
@@ -94,14 +94,14 @@
that contains two \isa{case}-expressions over instructions. Thus we add
automatic case splitting as well, which finishes the proof:%
\end{isamarkuptxt}%
-\isacommand{by}(induct\_tac~xs,~simp,~simp~split:~instr.split)%
+\isacommand{by}(induct\_tac\ xs,\ simp,\ simp\ split:\ instr.split)%
\begin{isamarkuptext}%
\noindent
Note that because \isaindex{auto} performs simplification, it can
also be modified in the same way \isa{simp} can. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
-\isacommand{by}(induct\_tac~xs,~auto~split:~instr.split)%
+\isacommand{by}(induct\_tac\ xs,\ auto\ split:\ instr.split)%
\begin{isamarkuptext}%
\noindent
Although this is more compact, it is less clear for the reader of the proof.
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Sun Aug 06 15:26:53 2000 +0200
@@ -113,7 +113,7 @@
\end{ttbox}
\begin{exercise}
- Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
+ Define a function \isa{norma} of type @{typ"'a aexp => 'a aexp"} that
replaces \isa{IF}s with complex boolean conditions by nested
\isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
\isa{Neg} should be eliminated completely. Prove that \isa{norma}
--- a/doc-src/TutorialI/Datatype/Fundata.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Sun Aug 06 15:26:53 2000 +0200
@@ -9,11 +9,11 @@
\isa{bool}, the result is a binary tree; if it is instantiated to
\isa{nat}, we have an infinitely branching tree because each node
has as many subtrees as there are natural numbers. How can we possibly
-write down such a tree? Using functional notation! For example, the *}
-
-term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
-
-text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
+write down such a tree? Using functional notation! For example, the term
+\begin{quote}
+@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
+\end{quote}
+of type @{typ"(nat,nat)bigtree"} is the tree whose
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
has merely \isa{Tip}s as further subtrees.
@@ -28,8 +28,8 @@
text{*\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of \isa{map_bt} involve only subtrees obtained from
\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
-seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
-of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
+seasoned functional programmer might have written @{term"map_bt f o F"}
+instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by
Isabelle because the termination proof is not as obvious since
\isa{map_bt} is only partially applied.
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Sun Aug 06 15:26:53 2000 +0200
@@ -16,8 +16,8 @@
the command \isacommand{term}.
Parameter \isa{'a} is the type of variables and \isa{'b} the type of
function symbols.
-A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
- [Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
+ [Var y]]"}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
suitable values, e.g.\ numbers or strings.
What complicates the definition of \isa{term} is the nested occurrence of
@@ -64,7 +64,7 @@
text{*\noindent
Note that \isa{Var} is the identity substitution because by definition it
-leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
+leaves variables unchanged: @{term"subst Var (Var x) = Var x"}. Note also
that the type annotations are necessary because otherwise there is nothing in
the goal to enforce that both halves of the goal talk about the same type
parameters \isa{('a,'b)}. As a result, induction would fail
@@ -86,9 +86,5 @@
expressions as its argument: \isa{Sum "'a aexp list"}.
*}
(*<*)
-
-lemma "subst s (App f ts) = App f (map (subst s) ts)";
-by(induct_tac ts, auto);
-
end
(*>*)
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Sun Aug 06 15:26:53 2000 +0200
@@ -13,14 +13,14 @@
\end{itemize}
In Isabelle this becomes%
\end{isamarkuptext}%
-\isacommand{datatype}~'a~aexp~=~IF~~~{"}'a~bexp{"}~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
-~~~~~~~~~~~~~~~~~|~Sum~~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
-~~~~~~~~~~~~~~~~~|~Diff~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
-~~~~~~~~~~~~~~~~~|~Var~'a\isanewline
-~~~~~~~~~~~~~~~~~|~Num~nat\isanewline
-\isakeyword{and}~~~~~~'a~bexp~=~Less~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
-~~~~~~~~~~~~~~~~~|~And~~{"}'a~bexp{"}~{"}'a~bexp{"}\isanewline
-~~~~~~~~~~~~~~~~~|~Neg~~{"}'a~bexp{"}%
+\isacommand{datatype}\ 'a\ aexp\ =\ IF\ \ \ {"}'a\ bexp{"}\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Sum\ \ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Diff\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Var\ 'a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Num\ nat\isanewline
+\isakeyword{and}\ \ \ \ \ \ 'a\ bexp\ =\ Less\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ \ {"}'a\ bexp{"}\ {"}'a\ bexp{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Neg\ \ {"}'a\ bexp{"}%
\begin{isamarkuptext}%
\noindent
Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
@@ -29,8 +29,8 @@
expressions can be arithmetic comparisons, conjunctions and negations.
The semantics is fixed via two evaluation functions%
\end{isamarkuptext}%
-\isacommand{consts}~~evala~::~{"}'a~aexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~nat{"}\isanewline
-~~~~~~~~evalb~::~{"}'a~bexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~bool{"}%
+\isacommand{consts}\ \ evala\ ::\ {"}'a\ aexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ nat{"}\isanewline
+\ \ \ \ \ \ \ \ evalb\ ::\ {"}'a\ bexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ bool{"}%
\begin{isamarkuptext}%
\noindent
that take an expression and an environment (a mapping from variables \isa{'a} to values
@@ -40,22 +40,22 @@
section:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
-~~{"}evala~(IF~b~a1~a2)~env~=\isanewline
-~~~~~(if~evalb~b~env~then~evala~a1~env~else~evala~a2~env){"}\isanewline
-~~{"}evala~(Sum~a1~a2)~env~=~evala~a1~env~+~evala~a2~env{"}\isanewline
-~~{"}evala~(Diff~a1~a2)~env~=~evala~a1~env~-~evala~a2~env{"}\isanewline
-~~{"}evala~(Var~v)~env~=~env~v{"}\isanewline
-~~{"}evala~(Num~n)~env~=~n{"}\isanewline
+\ \ {"}evala\ (IF\ b\ a1\ a2)\ env\ =\isanewline
+\ \ \ \ \ (if\ evalb\ b\ env\ then\ evala\ a1\ env\ else\ evala\ a2\ env){"}\isanewline
+\ \ {"}evala\ (Sum\ a1\ a2)\ env\ =\ evala\ a1\ env\ +\ evala\ a2\ env{"}\isanewline
+\ \ {"}evala\ (Diff\ a1\ a2)\ env\ =\ evala\ a1\ env\ -\ evala\ a2\ env{"}\isanewline
+\ \ {"}evala\ (Var\ v)\ env\ =\ env\ v{"}\isanewline
+\ \ {"}evala\ (Num\ n)\ env\ =\ n{"}\isanewline
\isanewline
-~~{"}evalb~(Less~a1~a2)~env~=~(evala~a1~env~<~evala~a2~env){"}\isanewline
-~~{"}evalb~(And~b1~b2)~env~=~(evalb~b1~env~{\isasymand}~evalb~b2~env){"}\isanewline
-~~{"}evalb~(Neg~b)~env~=~({\isasymnot}~evalb~b~env){"}%
+\ \ {"}evalb\ (Less\ a1\ a2)\ env\ =\ (evala\ a1\ env\ <\ evala\ a2\ env){"}\isanewline
+\ \ {"}evalb\ (And\ b1\ b2)\ env\ =\ (evalb\ b1\ env\ {\isasymand}\ evalb\ b2\ env){"}\isanewline
+\ \ {"}evalb\ (Neg\ b)\ env\ =\ ({\isasymnot}\ evalb\ b\ env){"}%
\begin{isamarkuptext}%
\noindent
In the same fashion we also define two functions that perform substitution:%
\end{isamarkuptext}%
-\isacommand{consts}~substa~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~'b~aexp{"}\isanewline
-~~~~~~~substb~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~'b~bexp{"}%
+\isacommand{consts}\ substa\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ aexp\ {\isasymRightarrow}\ 'b\ aexp{"}\isanewline
+\ \ \ \ \ \ \ substb\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ bexp\ {\isasymRightarrow}\ 'b\ bexp{"}%
\begin{isamarkuptext}%
\noindent
The first argument is a function mapping variables to expressions, the
@@ -64,16 +64,16 @@
to \isa{'b}. Note that there are only arithmetic and no boolean variables.%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
-~~{"}substa~s~(IF~b~a1~a2)~=\isanewline
-~~~~~IF~(substb~s~b)~(substa~s~a1)~(substa~s~a2){"}\isanewline
-~~{"}substa~s~(Sum~a1~a2)~=~Sum~(substa~s~a1)~(substa~s~a2){"}\isanewline
-~~{"}substa~s~(Diff~a1~a2)~=~Diff~(substa~s~a1)~(substa~s~a2){"}\isanewline
-~~{"}substa~s~(Var~v)~=~s~v{"}\isanewline
-~~{"}substa~s~(Num~n)~=~Num~n{"}\isanewline
+\ \ {"}substa\ s\ (IF\ b\ a1\ a2)\ =\isanewline
+\ \ \ \ \ IF\ (substb\ s\ b)\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
+\ \ {"}substa\ s\ (Sum\ a1\ a2)\ =\ Sum\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
+\ \ {"}substa\ s\ (Diff\ a1\ a2)\ =\ Diff\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
+\ \ {"}substa\ s\ (Var\ v)\ =\ s\ v{"}\isanewline
+\ \ {"}substa\ s\ (Num\ n)\ =\ Num\ n{"}\isanewline
\isanewline
-~~{"}substb~s~(Less~a1~a2)~=~Less~(substa~s~a1)~(substa~s~a2){"}\isanewline
-~~{"}substb~s~(And~b1~b2)~=~And~(substb~s~b1)~(substb~s~b2){"}\isanewline
-~~{"}substb~s~(Neg~b)~=~Neg~(substb~s~b){"}%
+\ \ {"}substb\ s\ (Less\ a1\ a2)\ =\ Less\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
+\ \ {"}substb\ s\ (And\ b1\ b2)\ =\ And\ (substb\ s\ b1)\ (substb\ s\ b2){"}\isanewline
+\ \ {"}substb\ s\ (Neg\ b)\ =\ Neg\ (substb\ s\ b){"}%
\begin{isamarkuptext}%
Now we can prove a fundamental theorem about the interaction between
evaluation and substitution: applying a substitution $s$ to an expression $a$
@@ -84,14 +84,14 @@
theorem in the induction step. Therefore you need to state and prove both
theorems simultaneously:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}evala~(substa~s~a)~env~=~evala~a~({\isasymlambda}x.~evala~(s~x)~env)~{\isasymand}\isanewline
-~~~~~~~~evalb~(substb~s~b)~env~=~evalb~b~({\isasymlambda}x.~evala~(s~x)~env){"}\isanewline
-\isacommand{apply}(induct\_tac~a~\isakeyword{and}~b)%
+\isacommand{lemma}\ {"}evala\ (substa\ s\ a)\ env\ =\ evala\ a\ ({\isasymlambda}x.\ evala\ (s\ x)\ env)\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ evalb\ (substb\ s\ b)\ env\ =\ evalb\ b\ ({\isasymlambda}x.\ evala\ (s\ x)\ env){"}\isanewline
+\isacommand{apply}(induct\_tac\ a\ \isakeyword{and}\ b)%
\begin{isamarkuptxt}%
\noindent
The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
\end{isamarkuptxt}%
-\isacommand{by}~auto%
+\isacommand{by}\ auto%
\begin{isamarkuptext}%
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
an inductive proof expects a goal of the form
@@ -102,7 +102,7 @@
\end{ttbox}
\begin{exercise}
- Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
+ Define a function \isa{norma} of type \isa{'a\ aexp\ {\isasymRightarrow}\ 'a\ aexp} that
replaces \isa{IF}s with complex boolean conditions by nested
\isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
\isa{Neg} should be eliminated completely. Prove that \isa{norma}
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{datatype}~('a,'i)bigtree~=~Tip~|~Branch~'a~{"}'i~{\isasymRightarrow}~('a,'i)bigtree{"}%
+\isacommand{datatype}\ ('a,'i)bigtree\ =\ Tip\ |\ Branch\ 'a\ {"}'i\ {\isasymRightarrow}\ ('a,'i)bigtree{"}%
\begin{isamarkuptext}%
\noindent Parameter \isa{'a} is the type of values stored in
the \isa{Branch}es of the tree, whereas \isa{'i} is the index
@@ -7,33 +7,37 @@
\isa{bool}, the result is a binary tree; if it is instantiated to
\isa{nat}, we have an infinitely branching tree because each node
has as many subtrees as there are natural numbers. How can we possibly
-write down such a tree? Using functional notation! For example, the%
-\end{isamarkuptext}%
-\isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}%
-\begin{isamarkuptext}%
-\noindent of type \isa{(nat,nat)bigtree} is the tree whose
+write down such a tree? Using functional notation! For example, the term
+\begin{quote}
+
+\begin{isabelle}%
+Branch\ 0\ ({\isasymlambda}i.\ Branch\ i\ ({\isasymlambda}n.\ Tip))
+\end{isabelle}%
+
+\end{quote}
+of type \isa{(nat,\ nat)\ bigtree} is the tree whose
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
has merely \isa{Tip}s as further subtrees.
Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:%
\end{isamarkuptext}%
-\isacommand{consts}~map\_bt~::~{"}('a~{\isasymRightarrow}~'b)~{\isasymRightarrow}~('a,'i)bigtree~{\isasymRightarrow}~('b,'i)bigtree{"}\isanewline
+\isacommand{consts}\ map\_bt\ ::\ {"}('a\ {\isasymRightarrow}\ 'b)\ {\isasymRightarrow}\ ('a,'i)bigtree\ {\isasymRightarrow}\ ('b,'i)bigtree{"}\isanewline
\isacommand{primrec}\isanewline
-{"}map\_bt~f~Tip~~~~~~~~~~=~Tip{"}\isanewline
-{"}map\_bt~f~(Branch~a~F)~=~Branch~(f~a)~({\isasymlambda}i.~map\_bt~f~(F~i)){"}%
+{"}map\_bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ =\ Tip{"}\isanewline
+{"}map\_bt\ f\ (Branch\ a\ F)\ =\ Branch\ (f\ a)\ ({\isasymlambda}i.\ map\_bt\ f\ (F\ i)){"}%
\begin{isamarkuptext}%
\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of \isa{map_bt} involve only subtrees obtained from
\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
-seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
-of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
+seasoned functional programmer might have written \isa{map\_bt\ f\ {\isasymcirc}\ F}
+instead of \isa{{\isasymlambda}i.\ map\_bt\ f\ (F\ i)}, but the former is not accepted by
Isabelle because the termination proof is not as obvious since
\isa{map_bt} is only partially applied.
The following lemma has a canonical proof%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline
-\isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}%
+\isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline
+\isacommand{apply}(induct\_tac\ {"}T{"},\ auto)\isacommand{.}%
\begin{isamarkuptext}%
\noindent
but it is worth taking a look at the proof state after the induction step
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Sun Aug 06 15:26:53 2000 +0200
@@ -6,15 +6,14 @@
constructor. This is not the case any longer for the following model of terms
where function symbols can be applied to a list of arguments:%
\end{isamarkuptext}%
-\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term~list{"}%
+\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\ list{"}%
\begin{isamarkuptext}%
\noindent
Note that we need to quote \isa{term} on the left to avoid confusion with
the command \isacommand{term}.
Parameter \isa{'a} is the type of variables and \isa{'b} the type of
function symbols.
-A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
- [Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ [Var\ x,\ App\ g\ [Var\ y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
suitable values, e.g.\ numbers or strings.
What complicates the definition of \isa{term} is the nested occurrence of
@@ -37,15 +36,15 @@
lists, we need to define two substitution functions simultaneously:%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-subst~::~{"}('a{\isasymRightarrow}('a,'b)term)~{\isasymRightarrow}~('a,'b)term~~~~~~{\isasymRightarrow}~('a,'b)term{"}\isanewline
-substs::~{"}('a{\isasymRightarrow}('a,'b)term)~{\isasymRightarrow}~('a,'b)term~list~{\isasymRightarrow}~('a,'b)term~list{"}\isanewline
+subst\ ::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ \ \ \ \ \ {\isasymRightarrow}\ ('a,'b)term{"}\isanewline
+substs::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ list\ {\isasymRightarrow}\ ('a,'b)term\ list{"}\isanewline
\isanewline
\isacommand{primrec}\isanewline
-~~{"}subst~s~(Var~x)~=~s~x{"}\isanewline
-~~{"}subst~s~(App~f~ts)~=~App~f~(substs~s~ts){"}\isanewline
+\ \ {"}subst\ s\ (Var\ x)\ =\ s\ x{"}\isanewline
+\ \ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (substs\ s\ ts){"}\isanewline
\isanewline
-~~{"}substs~s~[]~=~[]{"}\isanewline
-~~{"}substs~s~(t~\#~ts)~=~subst~s~t~\#~substs~s~ts{"}%
+\ \ {"}substs\ s\ []\ =\ []{"}\isanewline
+\ \ {"}substs\ s\ (t\ \#\ ts)\ =\ subst\ s\ t\ \#\ substs\ s\ ts{"}%
\begin{isamarkuptext}%
\noindent
Similarly, when proving a statement about terms inductively, we need
@@ -53,13 +52,13 @@
the fact that the identity substitution does not change a term needs to be
strengthened and proved as follows:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}subst~~Var~t~~=~(t~::('a,'b)term)~~{\isasymand}\isanewline
-~~~~~~~~substs~Var~ts~=~(ts::('a,'b)term~list){"}\isanewline
-\isacommand{by}(induct\_tac~t~\isakeyword{and}~ts,~auto)%
+\isacommand{lemma}\ {"}subst\ \ Var\ t\ \ =\ (t\ ::('a,'b)term)\ \ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ substs\ Var\ ts\ =\ (ts::('a,'b)term\ list){"}\isanewline
+\isacommand{by}(induct\_tac\ t\ \isakeyword{and}\ ts,\ auto)%
\begin{isamarkuptext}%
\noindent
Note that \isa{Var} is the identity substitution because by definition it
-leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
+leaves variables unchanged: \isa{subst\ Var\ (Var\ x)\ =\ Var\ x}. Note also
that the type annotations are necessary because otherwise there is nothing in
the goal to enforce that both halves of the goal talk about the same type
parameters \isa{('a,'b)}. As a result, induction would fail
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
-\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
-\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
+\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\_list{"}\isanewline
+\isakeyword{and}\ ('a,'b)term\_list\ =\ Nil\ |\ Cons\ {"}('a,'b)term{"}\ {"}('a,'b)term\_list{"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Sun Aug 06 15:26:53 2000 +0200
@@ -14,17 +14,17 @@
| And boolex boolex;
text{*\noindent
-The two constants are represented by \isa{Const~True} and
-\isa{Const~False}. Variables are represented by terms of the form
-\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
+The two constants are represented by @{term"Const True"} and
+@{term"Const False"}. Variables are represented by terms of the form
+@{term"Var n"}, where @{term"n"} is a natural number (type \isa{nat}).
For example, the formula $P@0 \land \neg P@1$ is represented by the term
-\isa{And~(Var~0)~(Neg(Var~1))}.
+@{term"And (Var 0) (Neg(Var 1))"}.
\subsubsection{What is the value of a boolean expression?}
The value of a boolean expression depends on the value of its variables.
Hence the function \isa{value} takes an additional parameter, an {\em
- environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
+ environment} of type @{typ"nat => bool"}, which maps variables to
their values:
*}
@@ -93,8 +93,8 @@
More interesting is the transformation of If-expressions into a normal form
where the first argument of \isa{IF} cannot be another \isa{IF} but
must be a constant or variable. Such a normal form can be computed by
-repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
-\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
+repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by
+@{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following
primitive recursive functions perform this task:
*}
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Aug 06 15:26:53 2000 +0200
@@ -7,29 +7,29 @@
constants by negation and conjunction. The following datatype serves exactly
that purpose:%
\end{isamarkuptext}%
-\isacommand{datatype}~boolex~=~Const~bool~|~Var~nat~|~Neg~boolex\isanewline
-~~~~~~~~~~~~~~~~|~And~boolex~boolex%
+\isacommand{datatype}\ boolex\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ boolex\ boolex%
\begin{isamarkuptext}%
\noindent
-The two constants are represented by \isa{Const~True} and
-\isa{Const~False}. Variables are represented by terms of the form
-\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
+The two constants are represented by \isa{Const\ True} and
+\isa{Const\ False}. Variables are represented by terms of the form
+\isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
For example, the formula $P@0 \land \neg P@1$ is represented by the term
-\isa{And~(Var~0)~(Neg(Var~1))}.
+\isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}.
\subsubsection{What is the value of a boolean expression?}
The value of a boolean expression depends on the value of its variables.
Hence the function \isa{value} takes an additional parameter, an {\em
- environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
+ environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to
their values:%
\end{isamarkuptext}%
-\isacommand{consts}~value~::~{"}boolex~{\isasymRightarrow}~(nat~{\isasymRightarrow}~bool)~{\isasymRightarrow}~bool{"}\isanewline
+\isacommand{consts}\ value\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline
\isacommand{primrec}\isanewline
-{"}value~(Const~b)~env~=~b{"}\isanewline
-{"}value~(Var~x)~~~env~=~env~x{"}\isanewline
-{"}value~(Neg~b)~~~env~=~({\isasymnot}~value~b~env){"}\isanewline
-{"}value~(And~b~c)~env~=~(value~b~env~{\isasymand}~value~c~env){"}%
+{"}value\ (Const\ b)\ env\ =\ b{"}\isanewline
+{"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline
+{"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline
+{"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}%
\begin{isamarkuptext}%
\noindent
\subsubsection{If-expressions}
@@ -39,17 +39,17 @@
from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
(\isa{IF}):%
\end{isamarkuptext}%
-\isacommand{datatype}~ifex~=~CIF~bool~|~VIF~nat~|~IF~ifex~ifex~ifex%
+\isacommand{datatype}\ ifex\ =\ CIF\ bool\ |\ VIF\ nat\ |\ IF\ ifex\ ifex\ ifex%
\begin{isamarkuptext}%
\noindent
The evaluation if If-expressions proceeds as for \isa{boolex}:%
\end{isamarkuptext}%
-\isacommand{consts}~valif~::~{"}ifex~{\isasymRightarrow}~(nat~{\isasymRightarrow}~bool)~{\isasymRightarrow}~bool{"}\isanewline
+\isacommand{consts}\ valif\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline
\isacommand{primrec}\isanewline
-{"}valif~(CIF~b)~~~~env~=~b{"}\isanewline
-{"}valif~(VIF~x)~~~~env~=~env~x{"}\isanewline
-{"}valif~(IF~b~t~e)~env~=~(if~valif~b~env~then~valif~t~env\isanewline
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~else~valif~e~env){"}%
+{"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline
+{"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline
+{"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}%
\begin{isamarkuptext}%
\subsubsection{Transformation into and of If-expressions}
@@ -57,23 +57,23 @@
formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
translate from \isa{boolex} into \isa{ifex}:%
\end{isamarkuptext}%
-\isacommand{consts}~bool2if~::~{"}boolex~{\isasymRightarrow}~ifex{"}\isanewline
+\isacommand{consts}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline
\isacommand{primrec}\isanewline
-{"}bool2if~(Const~b)~=~CIF~b{"}\isanewline
-{"}bool2if~(Var~x)~~~=~VIF~x{"}\isanewline
-{"}bool2if~(Neg~b)~~~=~IF~(bool2if~b)~(CIF~False)~(CIF~True){"}\isanewline
-{"}bool2if~(And~b~c)~=~IF~(bool2if~b)~(bool2if~c)~(CIF~False){"}%
+{"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline
+{"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline
+{"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline
+{"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}%
\begin{isamarkuptext}%
\noindent
At last, we have something we can verify: that \isa{bool2if} preserves the
value of its argument:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}valif~(bool2if~b)~env~=~value~b~env{"}%
+\isacommand{lemma}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}%
\begin{isamarkuptxt}%
\noindent
The proof is canonical:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~b)\isanewline
+\isacommand{apply}(induct\_tac\ b)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
@@ -83,35 +83,35 @@
More interesting is the transformation of If-expressions into a normal form
where the first argument of \isa{IF} cannot be another \isa{IF} but
must be a constant or variable. Such a normal form can be computed by
-repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
-\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
+repeatedly replacing a subterm of the form \isa{IF\ (IF\ b\ x\ y)\ z\ u} by
+\isa{IF\ b\ (IF\ x\ z\ u)\ (IF\ y\ z\ u)}, which has the same value. The following
primitive recursive functions perform this task:%
\end{isamarkuptext}%
-\isacommand{consts}~normif~::~{"}ifex~{\isasymRightarrow}~ifex~{\isasymRightarrow}~ifex~{\isasymRightarrow}~ifex{"}\isanewline
+\isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline
\isacommand{primrec}\isanewline
-{"}normif~(CIF~b)~~~~t~e~=~IF~(CIF~b)~t~e{"}\isanewline
-{"}normif~(VIF~x)~~~~t~e~=~IF~(VIF~x)~t~e{"}\isanewline
-{"}normif~(IF~b~t~e)~u~f~=~normif~b~(normif~t~u~f)~(normif~e~u~f){"}\isanewline
+{"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline
+{"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline
+{"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline
\isanewline
-\isacommand{consts}~norm~::~{"}ifex~{\isasymRightarrow}~ifex{"}\isanewline
+\isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline
\isacommand{primrec}\isanewline
-{"}norm~(CIF~b)~~~~=~CIF~b{"}\isanewline
-{"}norm~(VIF~x)~~~~=~VIF~x{"}\isanewline
-{"}norm~(IF~b~t~e)~=~normif~b~(norm~t)~(norm~e){"}%
+{"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline
+{"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline
+{"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}%
\begin{isamarkuptext}%
\noindent
Their interplay is a bit tricky, and we leave it to the reader to develop an
intuitive understanding. Fortunately, Isabelle can help us to verify that the
transformation preserves the value of the expression:%
\end{isamarkuptext}%
-\isacommand{theorem}~{"}valif~(norm~b)~env~=~valif~b~env{"}%
+\isacommand{theorem}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}%
\begin{isamarkuptext}%
\noindent
The proof is canonical, provided we first show the following simplification
lemma (which also helps to understand what \isa{normif} does):%
\end{isamarkuptext}%
-\isacommand{lemma}~[simp]:\isanewline
-~~{"}{\isasymforall}t~e.~valif~(normif~b~t~e)~env~=~valif~(IF~b~t~e)~env{"}%
+\isacommand{lemma}\ [simp]:\isanewline
+\ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}%
\begin{isamarkuptext}%
\noindent
Note that the lemma does not have a name, but is implicitly used in the proof
@@ -120,18 +120,18 @@
But how can we be sure that \isa{norm} really produces a normal form in
the above sense? We define a function that tests If-expressions for normality%
\end{isamarkuptext}%
-\isacommand{consts}~normal~::~{"}ifex~{\isasymRightarrow}~bool{"}\isanewline
+\isacommand{consts}\ normal\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline
\isacommand{primrec}\isanewline
-{"}normal(CIF~b)~=~True{"}\isanewline
-{"}normal(VIF~x)~=~True{"}\isanewline
-{"}normal(IF~b~t~e)~=~(normal~t~{\isasymand}~normal~e~{\isasymand}\isanewline
-~~~~~(case~b~of~CIF~b~{\isasymRightarrow}~True~|~VIF~x~{\isasymRightarrow}~True~|~IF~x~y~z~{\isasymRightarrow}~False)){"}%
+{"}normal(CIF\ b)\ =\ True{"}\isanewline
+{"}normal(VIF\ x)\ =\ True{"}\isanewline
+{"}normal(IF\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline
+\ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}%
\begin{isamarkuptext}%
\noindent
and prove \isa{normal(norm b)}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
-\isacommand{lemma}[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
+\isacommand{lemma}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Sun Aug 06 15:26:53 2000 +0200
@@ -50,7 +50,7 @@
txt{*\noindent
If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
-\isa{rev xs}, just as required.
+@{term"rev xs"}, just as required.
In this particular instance it was easy to guess the right generalization,
but in more complex situations a good deal of creativity is needed. This is
@@ -67,7 +67,7 @@
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
-\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
+@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one:
*};
(*<*)oops;(*>*)
--- a/doc-src/TutorialI/Misc/asm_simp.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy Sun Aug 06 15:26:53 2000 +0200
@@ -10,9 +10,9 @@
by simp;
text{*\noindent
-The second assumption simplifies to \isa{xs = []}, which in turn
-simplifies the first assumption to \isa{zs = ys}, thus reducing the
-conclusion to \isa{ys = ys} and hence to \isa{True}.
+The second assumption simplifies to @{term"xs = []"}, which in turn
+simplifies the first assumption to @{term"zs = ys"}, thus reducing the
+conclusion to @{term"ys = ys"} and hence to \isa{True}.
In some cases this may be too much of a good thing and may lead to
nontermination:
@@ -22,7 +22,7 @@
txt{*\noindent
cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f x = g(f(g x))} extracted from the assumption
+simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
does not terminate. Isabelle notices certain simple forms of
nontermination but not this one. The problem can be circumvented by
explicitly telling the simplifier to ignore the assumptions:
--- a/doc-src/TutorialI/Misc/case_splits.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy Sun Aug 06 15:26:53 2000 +0200
@@ -63,7 +63,7 @@
locally as above, or by giving it the \isa{split} attribute globally:
*}
-theorems [split] = list.split;
+lemmas [split] = list.split;
text{*\noindent
The \isa{split} attribute can be removed with the \isa{del} modifier,
@@ -79,7 +79,7 @@
text{*\noindent
or globally:
*}
-theorems [split del] = list.split;
+lemmas [split del] = list.split;
(*<*)
end
--- a/doc-src/TutorialI/Misc/cond_rewr.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy Sun Aug 06 15:26:53 2000 +0200
@@ -13,8 +13,7 @@
text{*\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
sequence of methods. Assuming that the simplification rule
-*}(*<*)term(*>*) "(rev xs = []) = (xs = [])";
-text{*\noindent
+@{term"(rev xs = []) = (xs = [])"}
is present as well,
*}
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Sun Aug 06 15:26:53 2000 +0200
@@ -7,10 +7,10 @@
\isa{rev} reqires an extra argument where the result is accumulated
gradually, using only \isa{\#}:%
\end{isamarkuptext}%
-\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{consts}\ itrev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
\isacommand{primrec}\isanewline
-{"}itrev~[]~~~~~ys~=~ys{"}\isanewline
-{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
+{"}itrev\ []\ \ \ \ \ ys\ =\ ys{"}\isanewline
+{"}itrev\ (x\#xs)\ ys\ =\ itrev\ xs\ (x\#ys){"}%
\begin{isamarkuptext}%
\noindent The behaviour of \isa{itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
@@ -21,12 +21,12 @@
Naturally, we would like to show that \isa{itrev} does indeed reverse
its first argument provided the second one is empty:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
+\isacommand{lemma}\ {"}itrev\ xs\ []\ =\ rev\ xs{"}%
\begin{isamarkuptxt}%
\noindent
There is no choice as to the induction variable, and we immediately simplify:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs,~auto)%
+\isacommand{apply}(induct\_tac\ xs,\ auto)%
\begin{isamarkuptxt}%
\noindent
Unfortunately, this is not a complete success:
@@ -43,11 +43,11 @@
Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
just not true---the correct generalization is%
\end{isamarkuptxt}%
-\isacommand{lemma}~{"}itrev~xs~ys~=~rev~xs~@~ys{"}%
+\isacommand{lemma}\ {"}itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
\begin{isamarkuptxt}%
\noindent
If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
-\isa{rev xs}, just as required.
+\isa{rev\ xs}, just as required.
In this particular instance it was easy to guess the right generalization,
but in more complex situations a good deal of creativity is needed. This is
@@ -64,10 +64,10 @@
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
-\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
+\isa{a\ \#\ ys} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
-\isacommand{lemma}~{"}{\isasymforall}ys.~itrev~xs~ys~=~rev~xs~@~ys{"}%
+\isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
\begin{isamarkuptxt}%
\noindent
This time induction on \isa{xs} followed by simplification succeeds. This
--- a/doc-src/TutorialI/Misc/document/Tree.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Sun Aug 06 15:26:53 2000 +0200
@@ -4,19 +4,19 @@
\noindent
Define the datatype of binary trees%
\end{isamarkuptext}%
-\isacommand{datatype}~'a~tree~=~Tip~|~Node~{"}'a~tree{"}~'a~{"}'a~tree{"}%
+\isacommand{datatype}\ 'a\ tree\ =\ Tip\ |\ Node\ {"}'a\ tree{"}\ 'a\ {"}'a\ tree{"}%
\begin{isamarkuptext}%
\noindent
and a function \isa{mirror} that mirrors a binary tree
by swapping subtrees (recursively). Prove%
\end{isamarkuptext}%
-\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}%
+\isacommand{lemma}\ mirror\_mirror:\ {"}mirror(mirror\ t)\ =\ t{"}%
\begin{isamarkuptext}%
\noindent
Define a function \isa{flatten} that flattens a tree into a list
by traversing it in infix order. Prove%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}flatten(mirror~t)~=~rev(flatten~t){"}\end{isabelle}%
+\isacommand{lemma}\ {"}flatten(mirror\ t)\ =\ rev(flatten\ t){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Sun Aug 06 15:26:53 2000 +0200
@@ -7,11 +7,11 @@
A linear time version of \isa{flatten} again reqires an extra
argument, the accumulator:%
\end{isamarkuptext}%
-\isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}%
+\isacommand{consts}\ flatten2\ ::\ {"}'a\ tree\ =>\ 'a\ list\ =>\ 'a\ list{"}%
\begin{isamarkuptext}%
\noindent Define \isa{flatten2} and prove%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}%
+\isacommand{lemma}\ {"}flatten2\ t\ []\ =\ flatten\ t{"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/arith1.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{lemma}~{"}{\isasymlbrakk}~{\isasymnot}~m~<~n;~m~<~n+1~{\isasymrbrakk}~{\isasymLongrightarrow}~m~=~n{"}\isanewline
+\isacommand{lemma}\ {"}{\isasymlbrakk}\ {\isasymnot}\ m\ <\ n;\ m\ <\ n+1\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/arith2.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline
+\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline
\isacommand{by}(arith)\isanewline
\end{isabelle}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/arith3.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{lemma}~{"}n*n~=~n~{\isasymLongrightarrow}~n=0~{\isasymor}~n=1{"}\isanewline
+\isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/arith4.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith4.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{lemma}~{"}{\isasymnot}~m~<~n~{\isasymand}~m~<~n+1~{\isasymLongrightarrow}~m~=~n{"}\isanewline
+\isacommand{lemma}\ {"}{\isasymnot}\ m\ <\ n\ {\isasymand}\ m\ <\ n+1\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Sun Aug 06 15:26:53 2000 +0200
@@ -4,27 +4,27 @@
By default, assumptions are part of the simplification process: they are used
as simplification rules and are simplified themselves. For example:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline
-\isacommand{by}~simp%
+\isacommand{lemma}\ {"}{\isasymlbrakk}\ xs\ @\ zs\ =\ ys\ @\ xs;\ []\ @\ xs\ =\ []\ @\ []\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ =\ zs{"}\isanewline
+\isacommand{by}\ simp%
\begin{isamarkuptext}%
\noindent
-The second assumption simplifies to \isa{xs = []}, which in turn
-simplifies the first assumption to \isa{zs = ys}, thus reducing the
-conclusion to \isa{ys = ys} and hence to \isa{True}.
+The second assumption simplifies to \isa{xs\ =\ []}, which in turn
+simplifies the first assumption to \isa{zs\ =\ ys}, thus reducing the
+conclusion to \isa{ys\ =\ ys} and hence to \isa{True}.
In some cases this may be too much of a good thing and may lead to
nontermination:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}{\isasymforall}x.~f~x~=~g~(f~(g~x))~{\isasymLongrightarrow}~f~[]~=~f~[]~@~[]{"}%
+\isacommand{lemma}\ {"}{\isasymforall}x.\ f\ x\ =\ g\ (f\ (g\ x))\ {\isasymLongrightarrow}\ f\ []\ =\ f\ []\ @\ []{"}%
\begin{isamarkuptxt}%
\noindent
cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f x = g(f(g x))} extracted from the assumption
+simplification rule \isa{f\ x\ =\ g\ (f\ (g\ x))} extracted from the assumption
does not terminate. Isabelle notices certain simple forms of
nontermination but not this one. The problem can be circumvented by
explicitly telling the simplifier to ignore the assumptions:%
\end{isamarkuptxt}%
-\isacommand{by}(simp~(no\_asm))%
+\isacommand{by}(simp\ (no\_asm))%
\begin{isamarkuptext}%
\noindent
There are three options that influence the treatment of assumptions:
--- a/doc-src/TutorialI/Misc/document/case_splits.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex Sun Aug 06 15:26:53 2000 +0200
@@ -4,7 +4,7 @@
Goals containing \isaindex{if}-expressions are usually proved by case
distinction on the condition of the \isa{if}. For example the goal%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}{\isasymforall}xs.~if~xs~=~[]~then~rev~xs~=~[]~else~rev~xs~{\isasymnoteq}~[]{"}%
+\isacommand{lemma}\ {"}{\isasymforall}xs.\ if\ xs\ =\ []\ then\ rev\ xs\ =\ []\ else\ rev\ xs\ {\isasymnoteq}\ []{"}%
\begin{isamarkuptxt}%
\noindent
can be split into
@@ -13,7 +13,7 @@
\end{isabellepar}%
by a degenerate form of simplification%
\end{isamarkuptxt}%
-\isacommand{apply}(simp~only:~split:~split\_if)%
+\isacommand{apply}(simp\ only:\ split:\ split\_if)%
\begin{isamarkuptext}%
\noindent
where no simplification rules are included (\isa{only:} is followed by the
@@ -25,7 +25,7 @@
This splitting idea generalizes from \isa{if} to \isaindex{case}:%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~zs~|~y\#ys~{\isasymRightarrow}~y\#(ys@zs))~=~xs@zs{"}%
+\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ zs\ |\ y\#ys\ {\isasymRightarrow}\ y\#(ys@zs))\ =\ xs@zs{"}%
\begin{isamarkuptxt}%
\noindent
becomes
@@ -35,7 +35,7 @@
\end{isabellepar}%
by typing%
\end{isamarkuptxt}%
-\isacommand{apply}(simp~only:~split:~list.split)%
+\isacommand{apply}(simp\ only:\ split:\ list.split)%
\begin{isamarkuptext}%
\noindent
In contrast to \isa{if}-expressions, the simplifier does not split
@@ -43,7 +43,7 @@
in case of recursive datatypes. Again, if the \isa{only:} modifier is
dropped, the above goal is solved,%
\end{isamarkuptext}%
-\isacommand{by}(simp~split:~list.split)%
+\isacommand{by}(simp\ split:\ list.split)%
\begin{isamarkuptext}%
\noindent%
which \isacommand{apply}\isa{(simp)} alone will not do.
@@ -52,18 +52,18 @@
\isa{$t$.split} which can be declared to be a \bfindex{split rule} either
locally as above, or by giving it the \isa{split} attribute globally:%
\end{isamarkuptext}%
-\isacommand{theorems}~[split]~=~list.split%
+\isacommand{lemmas}\ [split]\ =\ list.split%
\begin{isamarkuptext}%
\noindent
The \isa{split} attribute can be removed with the \isa{del} modifier,
either locally%
\end{isamarkuptext}%
-\isacommand{apply}(simp~split~del:~split\_if)%
+\isacommand{apply}(simp\ split\ del:\ split\_if)%
\begin{isamarkuptext}%
\noindent
or globally:%
\end{isamarkuptext}%
-\isacommand{theorems}~[split~del]~=~list.split\isanewline
+\isacommand{lemmas}\ [split\ del]\ =\ list.split\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/cases.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
\isanewline
-\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
-\isacommand{apply}(case\_tac~xs)%
+\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline
+\isacommand{apply}(case\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent
results in the proof state
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Sun Aug 06 15:26:53 2000 +0200
@@ -4,19 +4,16 @@
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example%
\end{isamarkuptext}%
-\isacommand{lemma}~hd\_Cons\_tl[simp]:~{"}xs~{\isasymnoteq}~[]~~{\isasymLongrightarrow}~~hd~xs~\#~tl~xs~=~xs{"}\isanewline
-\isacommand{by}(case\_tac~xs,~simp,~simp)%
+\isacommand{lemma}\ hd\_Cons\_tl[simp]:\ {"}xs\ {\isasymnoteq}\ []\ \ {\isasymLongrightarrow}\ \ hd\ xs\ \#\ tl\ xs\ =\ xs{"}\isanewline
+\isacommand{by}(case\_tac\ xs,\ simp,\ simp)%
\begin{isamarkuptext}%
\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
-sequence of methods. Assuming that the simplification rule%
-\end{isamarkuptext}%
-~{"}(rev~xs~=~[])~=~(xs~=~[]){"}%
-\begin{isamarkuptext}%
-\noindent
+sequence of methods. Assuming that the simplification rule
+\isa{(rev\ xs\ =\ [])\ =\ (xs\ =\ [])}
is present as well,%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}%
+\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}%
\begin{isamarkuptext}%
\noindent
is proved by plain simplification:
--- a/doc-src/TutorialI/Misc/document/def_rewr.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Sun Aug 06 15:26:53 2000 +0200
@@ -9,19 +9,19 @@
enough lemmas that characterize the concept sufficiently for us to forget the
original definition. For example, given%
\end{isamarkuptext}%
-\isacommand{constdefs}~exor~::~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline
-~~~~~~~~~{"}exor~A~B~{\isasymequiv}~(A~{\isasymand}~{\isasymnot}B)~{\isasymor}~({\isasymnot}A~{\isasymand}~B){"}%
+\isacommand{constdefs}\ exor\ ::\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline
+\ \ \ \ \ \ \ \ \ {"}exor\ A\ B\ {\isasymequiv}\ (A\ {\isasymand}\ {\isasymnot}B)\ {\isasymor}\ ({\isasymnot}A\ {\isasymand}\ B){"}%
\begin{isamarkuptext}%
\noindent
we may want to prove%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}exor~A~({\isasymnot}A){"}%
+\isacommand{lemma}\ {"}exor\ A\ ({\isasymnot}A){"}%
\begin{isamarkuptxt}%
\noindent
There is a special method for \emph{unfolding} definitions, which we need to
get started:\indexbold{*unfold}\indexbold{definition!unfolding}%
\end{isamarkuptxt}%
-\isacommand{apply}(unfold~exor\_def)%
+\isacommand{apply}(unfold\ exor\_def)%
\begin{isamarkuptxt}%
\noindent
It unfolds the given list of definitions (here merely one) in all subgoals:
@@ -33,7 +33,7 @@
In case we want to expand a definition in the middle of a proof, we can
simply include it locally:%
\end{isamarkuptxt}%
-\isacommand{apply}(simp~add:~exor\_def)%
+\isacommand{apply}(simp\ add:\ exor\_def)%
\begin{isamarkuptext}%
\noindent
In fact, this one command proves the above lemma directly.
--- a/doc-src/TutorialI/Misc/document/fakenat.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex Sun Aug 06 15:26:53 2000 +0200
@@ -5,7 +5,7 @@
The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
numbers is predefined and behaves like%
\end{isamarkuptext}%
-\isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}%
+\isacommand{datatype}\ nat\ =\ 0\ |\ Suc\ nat\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,11 +1,11 @@
\begin{isabelle}%
-\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
-\isacommand{by}(simp~add:~Let\_def)%
+\isacommand{lemma}\ {"}(let\ xs\ =\ []\ in\ xs@ys@xs)\ =\ ys{"}\isanewline
+\isacommand{by}(simp\ add:\ Let\_def)%
\begin{isamarkuptext}%
If, in a particular context, there is no danger of a combinatorial explosion
of nested \isa{let}s one could even add \isa{Let_def} permanently:%
\end{isamarkuptext}%
-\isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
+\isacommand{lemmas}\ [simp]\ =\ Let\_def\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Sun Aug 06 15:26:53 2000 +0200
@@ -2,22 +2,25 @@
%
\begin{isamarkuptext}%
\noindent
-In particular, there are \isa{case}-expressions, for example%
-\end{isamarkuptext}%
-~{"}case~n~of~0~{\isasymRightarrow}~0~|~Suc~m~{\isasymRightarrow}~m{"}%
-\begin{isamarkuptext}%
-\noindent
+In particular, there are \isa{case}-expressions, for example
+\begin{quote}
+
+\begin{isabelle}%
+case\ n\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ m\ {\isasymRightarrow}\ m
+\end{isabelle}%
+
+\end{quote}
primitive recursion, for example%
\end{isamarkuptext}%
-\isacommand{consts}~sum~::~{"}nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{primrec}~{"}sum~0~=~0{"}\isanewline
-~~~~~~~~{"}sum~(Suc~n)~=~Suc~n~+~sum~n{"}%
+\isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline
+\ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}%
\begin{isamarkuptext}%
\noindent
and induction, for example%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}sum~n~+~sum~n~=~n*(Suc~n){"}\isanewline
-\isacommand{apply}(induct\_tac~n)\isanewline
+\isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline
+\isacommand{apply}(induct\_tac\ n)\isanewline
\isacommand{by}(auto)\isanewline
\end{isabelle}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/pairs.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,25 @@
\begin{isabelle}%
-~{"}let~(x,y)~=~f~z~in~(y,x){"}~{"}case~xs~of~[]~{\isasymRightarrow}~0~|~(x,y)\#zs~{\isasymRightarrow}~x+y{"}\isanewline
+%
+\begin{isamarkuptext}%
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
+ $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
+are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
+\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
+\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
+\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
+ $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
+
+It is possible to use (nested) tuples as patterns in abstractions, for
+example \isa{\isasymlambda(x,y,z).x+y+z} and
+\isa{\isasymlambda((x,y),z).x+y+z}.
+In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
+most variable binding constructs. Typical examples are
+\begin{quote}
+\isa{let\ (x,\ y)\ =\ f\ z\ in\ (y,\ x)}\\
+\isa{case\ xs\ of\ []\ {\isasymRightarrow}\ 0\ |\ (x,\ y)\ \#\ zs\ {\isasymRightarrow}\ x\ +\ y}
+\end{quote}
+Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
+\end{isamarkuptext}%
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
\isanewline
-~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~(m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
+\ \ \ \ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ (m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}%
\begin{isamarkuptext}%
\noindent\small
where \isa{dvd} means ``divides''.
@@ -8,7 +8,7 @@
right-hand side, which would introduce an inconsistency (why?). What you
should have written is%
\end{isamarkuptext}%
-~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
+\ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ ({\isasymforall}m.\ m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Sun Aug 06 15:26:53 2000 +0200
@@ -5,8 +5,8 @@
\ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
on:%
\end{isamarkuptext}%
-\isacommand{ML}~{"}set~trace\_simp{"}\isanewline
-\isacommand{lemma}~{"}rev~[a]~=~[]{"}\isanewline
+\isacommand{ML}\ {"}set\ trace\_simp{"}\isanewline
+\isacommand{lemma}\ {"}rev\ [a]\ =\ []{"}\isanewline
\isacommand{apply}(simp)%
\begin{isamarkuptxt}%
\noindent
@@ -35,7 +35,7 @@
invocations of the simplifier are often nested (e.g.\ when solving conditions
of rewrite rules). Thus it is advisable to reset it:%
\end{isamarkuptxt}%
-\isacommand{ML}~{"}reset~trace\_simp{"}\isanewline
+\isacommand{ML}\ {"}reset\ trace\_simp{"}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/types.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
-\isacommand{types}~number~~~~~~~=~nat\isanewline
-~~~~~~gate~~~~~~~~~=~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline
-~~~~~~('a,'b)alist~=~{"}('a~*~'b)list{"}%
+\isacommand{types}\ number\ \ \ \ \ \ \ =\ nat\isanewline
+\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ =\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline
+\ \ \ \ \ \ ('a,'b)alist\ =\ {"}('a\ *\ 'b)list{"}%
\begin{isamarkuptext}%
\noindent\indexbold{*types}%
Internally all synonyms are fully expanded. As a consequence Isabelle's
@@ -9,8 +9,8 @@
readability of theories. Synonyms can be used just like any other
type:%
\end{isamarkuptext}%
-\isacommand{consts}~nand~::~gate\isanewline
-~~~~~~~exor~::~gate%
+\isacommand{consts}\ nand\ ::\ gate\isanewline
+\ \ \ \ \ \ \ exor\ ::\ gate%
\begin{isamarkuptext}%
\subsection{Constant definitions}
\label{sec:ConstDefinitions}
@@ -19,20 +19,20 @@
The above constants \isa{nand} and \isa{exor} are non-recursive and can
therefore be defined directly by%
\end{isamarkuptext}%
-\isacommand{defs}~nand\_def:~{"}nand~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymand}~B){"}\isanewline
-~~~~~exor\_def:~{"}exor~A~B~{\isasymequiv}~A~{\isasymand}~{\isasymnot}B~{\isasymor}~{\isasymnot}A~{\isasymand}~B{"}%
+\isacommand{defs}\ nand\_def:\ {"}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymand}\ B){"}\isanewline
+\ \ \ \ \ exor\_def:\ {"}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{"}%
\begin{isamarkuptext}%
\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
\isa{exor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
-that should only be used in constant definitions.
+that must be used in constant definitions.
Declarations and definitions can also be merged%
\end{isamarkuptext}%
-\isacommand{constdefs}~nor~::~gate\isanewline
-~~~~~~~~~{"}nor~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymor}~B){"}\isanewline
-~~~~~~~~~~exor2~::~gate\isanewline
-~~~~~~~~~{"}exor2~A~B~{\isasymequiv}~(A~{\isasymor}~B)~{\isasymand}~({\isasymnot}A~{\isasymor}~{\isasymnot}B){"}%
+\isacommand{constdefs}\ nor\ ::\ gate\isanewline
+\ \ \ \ \ \ \ \ \ {"}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymor}\ B){"}\isanewline
+\ \ \ \ \ \ \ \ \ \ exor2\ ::\ gate\isanewline
+\ \ \ \ \ \ \ \ \ {"}exor2\ A\ B\ {\isasymequiv}\ (A\ {\isasymor}\ B)\ {\isasymand}\ ({\isasymnot}A\ {\isasymor}\ {\isasymnot}B){"}%
\begin{isamarkuptext}%
\noindent\indexbold{*constdefs}%
in which case the default name of each definition is \isa{$f$_def}, where
--- a/doc-src/TutorialI/Misc/fakenat.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/fakenat.thy Sun Aug 06 15:26:53 2000 +0200
@@ -7,7 +7,7 @@
numbers is predefined and behaves like
*}
-datatype nat = "0" | Suc nat
+datatype nat = 0 | Suc nat
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/let_rewr.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy Sun Aug 06 15:26:53 2000 +0200
@@ -8,7 +8,7 @@
If, in a particular context, there is no danger of a combinatorial explosion
of nested \isa{let}s one could even add \isa{Let_def} permanently:
*}
-theorems [simp] = Let_def;
+lemmas [simp] = Let_def;
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/natsum.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Sun Aug 06 15:26:53 2000 +0200
@@ -3,11 +3,9 @@
(*>*)
text{*\noindent
In particular, there are \isa{case}-expressions, for example
-*}
-
-(*<*)term(*>*) "case n of 0 \\<Rightarrow> 0 | Suc m \\<Rightarrow> m";
-
-text{*\noindent
+\begin{quote}
+@{term[display]"case n of 0 => 0 | Suc m => m"}
+\end{quote}
primitive recursion, for example
*}
--- a/doc-src/TutorialI/Misc/pairs.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Sun Aug 06 15:26:53 2000 +0200
@@ -1,8 +1,26 @@
(*<*)
theory pairs = Main:;
-term(*>*) "let (x,y) = f z in (y,x)";
+(*>*)
+text{*
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
+ $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
+are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
+\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
+\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
+\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
+ $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
+
+It is possible to use (nested) tuples as patterns in abstractions, for
+example \isa{\isasymlambda(x,y,z).x+y+z} and
+\isa{\isasymlambda((x,y),z).x+y+z}.
+In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
+most variable binding constructs. Typical examples are
+\begin{quote}
+@{term"let (x,y) = f z in (y,x)"}\\
+@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
+\end{quote}
+Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
+*}
(*<*)
-term(*>*) "case xs of [] \\<Rightarrow> 0 | (x,y)#zs \\<Rightarrow> x+y"
-(**)(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/types.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Sun Aug 06 15:26:53 2000 +0200
@@ -30,7 +30,7 @@
where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
\isa{exor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
-that should only be used in constant definitions.
+that must be used in constant definitions.
Declarations and definitions can also be merged
*}
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Sun Aug 06 15:26:53 2000 +0200
@@ -15,14 +15,14 @@
you are trying to establish holds for the left-hand side provided it holds
for all recursive calls on the right-hand side. Here is a simple example%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}%
+\isacommand{lemma}\ {"}map\ f\ (sep(x,xs))\ =\ sep(f\ x,\ map\ f\ xs){"}%
\begin{isamarkuptxt}%
\noindent
involving the predefined \isa{map} functional on lists: \isa{map f xs}
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
this lemma by recursion induction w.r.t. \isa{sep}:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~x~xs~rule:~sep.induct)%
+\isacommand{apply}(induct\_tac\ x\ xs\ rule:\ sep.induct)%
\begin{isamarkuptxt}%
\noindent
The resulting proof state has three subgoals corresponding to the three
@@ -36,7 +36,7 @@
\end{isabellepar}%
The rest is pure simplification:%
\end{isamarkuptxt}%
-\isacommand{by}~auto%
+\isacommand{by}\ auto%
\begin{isamarkuptext}%
Try proving the above lemma by structural induction, and you find that you
need an additional case distinction. What is worse, the names of variables
--- a/doc-src/TutorialI/Recdef/document/examples.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Sun Aug 06 15:26:53 2000 +0200
@@ -3,30 +3,30 @@
\begin{isamarkuptext}%
Here is a simple example, the Fibonacci function:%
\end{isamarkuptext}%
-\isacommand{consts}~fib~::~{"}nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~fib~{"}measure({\isasymlambda}n.~n){"}\isanewline
-~~{"}fib~0~=~0{"}\isanewline
-~~{"}fib~1~=~1{"}\isanewline
-~~{"}fib~(Suc(Suc~x))~=~fib~x~+~fib~(Suc~x){"}%
+\isacommand{consts}\ fib\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ fib\ {"}measure({\isasymlambda}n.\ n){"}\isanewline
+\ \ {"}fib\ 0\ =\ 0{"}\isanewline
+\ \ {"}fib\ 1\ =\ 1{"}\isanewline
+\ \ {"}fib\ (Suc(Suc\ x))\ =\ fib\ x\ +\ fib\ (Suc\ x){"}%
\begin{isamarkuptext}%
\noindent
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
+\isa{{\isasymlambda}n.\ n} which maps the argument of \isa{fib} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
argument of each recursive call. In the case of \isa{fib} this is
obviously true because the measure function is the identity and
-\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
-\isa{Suc~x}.
+\isa{Suc\ (Suc\ x)} is strictly greater than both \isa{x} and
+\isa{Suc\ x}.
Slightly more interesting is the insertion of a fixed element
between any two elements of a list:%
\end{isamarkuptext}%
-\isacommand{consts}~sep~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
-\isacommand{recdef}~sep~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline
-~~{"}sep(a,~[])~~~~~=~[]{"}\isanewline
-~~{"}sep(a,~[x])~~~~=~[x]{"}\isanewline
-~~{"}sep(a,~x\#y\#zs)~=~x~\#~a~\#~sep(a,y\#zs){"}%
+\isacommand{consts}\ sep\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
+\isacommand{recdef}\ sep\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
+\ \ {"}sep(a,\ [])\ \ \ \ \ =\ []{"}\isanewline
+\ \ {"}sep(a,\ [x])\ \ \ \ =\ [x]{"}\isanewline
+\ \ {"}sep(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep(a,y\#zs){"}%
\begin{isamarkuptext}%
\noindent
This time the measure is the length of the list, which decreases with the
@@ -34,18 +34,18 @@
Pattern matching need not be exhaustive:%
\end{isamarkuptext}%
-\isacommand{consts}~last~::~{"}'a~list~{\isasymRightarrow}~'a{"}\isanewline
-\isacommand{recdef}~last~{"}measure~({\isasymlambda}xs.~length~xs){"}\isanewline
-~~{"}last~[x]~~~~~~=~x{"}\isanewline
-~~{"}last~(x\#y\#zs)~=~last~(y\#zs){"}%
+\isacommand{consts}\ last\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}\isanewline
+\isacommand{recdef}\ last\ {"}measure\ ({\isasymlambda}xs.\ length\ xs){"}\isanewline
+\ \ {"}last\ [x]\ \ \ \ \ \ =\ x{"}\isanewline
+\ \ {"}last\ (x\#y\#zs)\ =\ last\ (y\#zs){"}%
\begin{isamarkuptext}%
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:%
\end{isamarkuptext}%
-\isacommand{consts}~sep1~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
-\isacommand{recdef}~sep1~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline
-~~{"}sep1(a,~x\#y\#zs)~=~x~\#~a~\#~sep1(a,y\#zs){"}\isanewline
-~~{"}sep1(a,~xs)~~~~~=~xs{"}%
+\isacommand{consts}\ sep1\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
+\isacommand{recdef}\ sep1\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
+\ \ {"}sep1(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep1(a,y\#zs){"}\isanewline
+\ \ {"}sep1(a,\ xs)\ \ \ \ \ =\ xs{"}%
\begin{isamarkuptext}%
\noindent
This defines exactly the same function as \isa{sep} above, i.e.\
@@ -60,18 +60,18 @@
arguments as in the following definition:
\end{warn}%
\end{isamarkuptext}%
-\isacommand{consts}~sep2~::~{"}'a~list~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a~list{"}\isanewline
-\isacommand{recdef}~sep2~{"}measure~length{"}\isanewline
-~~{"}sep2~(x\#y\#zs)~=~({\isasymlambda}a.~x~\#~a~\#~sep2~zs~a){"}\isanewline
-~~{"}sep2~xs~~~~~~~=~({\isasymlambda}a.~xs){"}%
+\isacommand{consts}\ sep2\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
+\isacommand{recdef}\ sep2\ {"}measure\ length{"}\isanewline
+\ \ {"}sep2\ (x\#y\#zs)\ =\ ({\isasymlambda}a.\ x\ \#\ a\ \#\ sep2\ zs\ a){"}\isanewline
+\ \ {"}sep2\ xs\ \ \ \ \ \ \ =\ ({\isasymlambda}a.\ xs){"}%
\begin{isamarkuptext}%
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
for the definition of non-recursive functions:%
\end{isamarkuptext}%
-\isacommand{consts}~swap12~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
-\isacommand{recdef}~swap12~{"}{\isabraceleft}{\isabraceright}{"}\isanewline
-~~{"}swap12~(x\#y\#zs)~=~y\#x\#zs{"}\isanewline
-~~{"}swap12~zs~~~~~~~=~zs{"}%
+\isacommand{consts}\ swap12\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
+\isacommand{recdef}\ swap12\ {"}{\isabraceleft}{\isabraceright}{"}\isanewline
+\ \ {"}swap12\ (x\#y\#zs)\ =\ y\#x\#zs{"}\isanewline
+\ \ {"}swap12\ zs\ \ \ \ \ \ \ =\ zs{"}%
\begin{isamarkuptext}%
\noindent
For non-recursive functions the termination measure degenerates to the empty
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Sun Aug 06 15:26:53 2000 +0200
@@ -8,17 +8,20 @@
terminate because of automatic splitting of \isa{if}.
Let us look at an example:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd~(m,~n)~=~(if~n=0~then~m~else~gcd(n,~m~mod~n)){"}%
+\isacommand{consts}\ gcd\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n)){"}%
\begin{isamarkuptext}%
\noindent
According to the measure function, the second argument should decrease with
-each recursive call. The resulting termination condition%
-\end{isamarkuptext}%
-~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~m~mod~n~<~n{"}%
-\begin{isamarkuptext}%
-\noindent
+each recursive call. The resulting termination condition
+\begin{quote}
+
+\begin{isabelle}%
+n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ m\ mod\ n\ <\ n
+\end{isabelle}%
+
+\end{quote}
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -26,24 +29,34 @@
languages and our simplifier don't do that. Unfortunately the simplifier does
something else which leads to the same problem: it splits \isa{if}s if the
condition simplifies to neither \isa{True} nor \isa{False}. For
-example, simplification reduces%
-\end{isamarkuptext}%
-~{"}gcd(m,n)~=~k{"}%
-\begin{isamarkuptext}%
-\noindent
-in one step to%
-\end{isamarkuptext}%
-~{"}(if~n=0~then~m~else~gcd(n,~m~mod~n))~=~k{"}%
-\begin{isamarkuptext}%
-\noindent
-where the condition cannot be reduced further, and splitting leads to%
-\end{isamarkuptext}%
-~{"}(n=0~{\isasymlongrightarrow}~m=k)~{\isasymand}~(n{\isasymnoteq}0~{\isasymlongrightarrow}~gcd(n,~m~mod~n)=k){"}%
-\begin{isamarkuptext}%
-\noindent
-Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
-Fortunately, this problem can be avoided in many different ways.
+example, simplification reduces
+\begin{quote}
+
+\begin{isabelle}%
+gcd\ (m,\ n)\ =\ k
+\end{isabelle}%
+
+\end{quote}
+in one step to
+\begin{quote}
+
+\begin{isabelle}%
+(if\ n\ =\ 0\ then\ m\ else\ gcd\ (n,\ m\ mod\ n))\ =\ k
+\end{isabelle}%
+
+\end{quote}
+where the condition cannot be reduced further, and splitting leads to
+\begin{quote}
+
+\begin{isabelle}%
+(n\ =\ 0\ {\isasymlongrightarrow}\ m\ =\ k)\ {\isasymand}\ (n\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (n,\ m\ mod\ n)\ =\ k)
+\end{isabelle}%
+
+\end{quote}
+Since the recursive call \isa{gcd\ (n,\ m\ mod\ n)} is no longer protected by
+an \isa{if}, it is unfolded again, which leads to an infinite chain of
+simplification steps. Fortunately, this problem can be avoided in many
+different ways.
The most radical solution is to disable the offending
\isa{split_if} as shown in the section on case splits in
@@ -55,10 +68,10 @@
rather than \isa{if} on the right. In the case of \isa{gcd} the
following alternative definition suggests itself:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd1~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd1~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd1~(m,~0)~=~m{"}\isanewline
-~~{"}gcd1~(m,~n)~=~gcd1(n,~m~mod~n){"}%
+\isacommand{consts}\ gcd1\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd1\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd1\ (m,\ 0)\ =\ m{"}\isanewline
+\ \ {"}gcd1\ (m,\ n)\ =\ gcd1(n,\ m\ mod\ n){"}%
\begin{isamarkuptext}%
\noindent
Note that the order of equations is important and hides the side condition
@@ -68,9 +81,9 @@
A very simple alternative is to replace \isa{if} by \isa{case}, which
is also available for \isa{bool} but is not split automatically:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd2~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd2~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd2(m,n)~=~(case~n=0~of~True~{\isasymRightarrow}~m~|~False~{\isasymRightarrow}~gcd2(n,m~mod~n)){"}%
+\isacommand{consts}\ gcd2\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd2\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd2(m,n)\ =\ (case\ n=0\ of\ True\ {\isasymRightarrow}\ m\ |\ False\ {\isasymRightarrow}\ gcd2(n,m\ mod\ n)){"}%
\begin{isamarkuptext}%
\noindent
In fact, this is probably the neatest solution next to pattern matching.
@@ -78,15 +91,15 @@
A final alternative is to replace the offending simplification rules by
derived conditional ones. For \isa{gcd} it means we have to prove%
\end{isamarkuptext}%
-\isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline
+\isacommand{lemma}\ [simp]:\ {"}gcd\ (m,\ 0)\ =\ m{"}\isanewline
\isacommand{by}(simp)\isanewline
-\isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline
+\isacommand{lemma}\ [simp]:\ {"}n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ gcd(m,\ n)\ =\ gcd(n,\ m\ mod\ n){"}\isanewline
\isacommand{by}(simp)%
\begin{isamarkuptext}%
\noindent
after which we can disable the original simplification rule:%
\end{isamarkuptext}%
-\isacommand{lemmas}~[simp~del]~=~gcd.simps\isanewline
+\isacommand{lemmas}\ [simp\ del]\ =\ gcd.simps\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Sun Aug 06 15:26:53 2000 +0200
@@ -15,9 +15,9 @@
(there is one for each recursive call) automatically. For example,
termination of the following artificial function%
\end{isamarkuptext}%
-\isacommand{consts}~f~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~f~{"}measure({\isasymlambda}(x,y).~x-y){"}\isanewline
-~~{"}f(x,y)~=~(if~x~{\isasymle}~y~then~x~else~f(x,y+1)){"}%
+\isacommand{consts}\ f\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ f\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
+\ \ {"}f(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ f(x,y+1)){"}%
\begin{isamarkuptext}%
\noindent
is not proved automatically (although maybe it should be). Isabelle prints a
@@ -25,7 +25,7 @@
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:%
\end{isamarkuptext}%
-\isacommand{lemma}~termi\_lem[simp]:~{"}{\isasymnot}~x~{\isasymle}~y~{\isasymLongrightarrow}~x~-~Suc~y~<~x~-~y{"}%
+\isacommand{lemma}\ termi\_lem[simp]:\ {"}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ -\ Suc\ y\ <\ x\ -\ y{"}%
\begin{isamarkuptxt}%
\noindent
It was not proved automatically because of the special nature of \isa{-}
@@ -38,16 +38,16 @@
we have turned our lemma into a simplification rule. Therefore our second
attempt to define our function will automatically take it into account:%
\end{isamarkuptext}%
-\isacommand{consts}~g~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~g~{"}measure({\isasymlambda}(x,y).~x-y){"}\isanewline
-~~{"}g(x,y)~=~(if~x~{\isasymle}~y~then~x~else~g(x,y+1)){"}%
+\isacommand{consts}\ g\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ g\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
+\ \ {"}g(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ g(x,y+1)){"}%
\begin{isamarkuptext}%
\noindent
This time everything works fine. Now \isa{g.simps} contains precisely the
stated recursion equation for \isa{g} and they are simplification
rules. Thus we can automatically prove%
\end{isamarkuptext}%
-\isacommand{theorem}~wow:~{"}g(1,0)~=~g(1,1){"}\isanewline
+\isacommand{theorem}\ wow:\ {"}g(1,0)\ =\ g(1,1){"}\isanewline
\isacommand{by}(simp)%
\begin{isamarkuptext}%
\noindent
@@ -57,7 +57,7 @@
simplification rule for the sake of the termination proof, we may want to
disable it again:%
\end{isamarkuptext}%
-\isacommand{lemmas}~[simp~del]~=~termi\_lem%
+\isacommand{lemmas}\ [simp\ del]\ =\ termi\_lem%
\begin{isamarkuptext}%
The attentive reader may wonder why we chose to call our function \isa{g}
rather than \isa{f} the second time around. The reason is that, despite
@@ -76,11 +76,11 @@
allows arbitrary wellfounded relations. For example, termination of
Ackermann's function requires the lexicographic product \isa{<*lex*>}:%
\end{isamarkuptext}%
-\isacommand{consts}~ack~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~ack~{"}measure(\%m.~m)~<*lex*>~measure(\%n.~n){"}\isanewline
-~~{"}ack(0,n)~~~~~~~~~=~Suc~n{"}\isanewline
-~~{"}ack(Suc~m,0)~~~~~=~ack(m,~1){"}\isanewline
-~~{"}ack(Suc~m,Suc~n)~=~ack(m,ack(Suc~m,n)){"}%
+\isacommand{consts}\ ack\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ ack\ {"}measure(\%m.\ m)\ <*lex*>\ measure(\%n.\ n){"}\isanewline
+\ \ {"}ack(0,n)\ \ \ \ \ \ \ \ \ =\ Suc\ n{"}\isanewline
+\ \ {"}ack(Suc\ m,0)\ \ \ \ \ =\ ack(m,\ 1){"}\isanewline
+\ \ {"}ack(Suc\ m,Suc\ n)\ =\ ack(m,ack(Suc\ m,n)){"}%
\begin{isamarkuptext}%
\noindent
For details see the manual~\cite{isabelle-HOL} and the examples in the
--- a/doc-src/TutorialI/Recdef/examples.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Sun Aug 06 15:26:53 2000 +0200
@@ -14,13 +14,13 @@
text{*\noindent
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
+@{term"%n. n"} which maps the argument of \isa{fib} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
argument of each recursive call. In the case of \isa{fib} this is
obviously true because the measure function is the identity and
-\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
-\isa{Suc~x}.
+@{term"Suc(Suc x)"} is strictly greater than both \isa{x} and
+@{term"Suc x"}.
Slightly more interesting is the insertion of a fixed element
between any two elements of a list:
--- a/doc-src/TutorialI/Recdef/simplification.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Sun Aug 06 15:26:53 2000 +0200
@@ -18,11 +18,9 @@
text{*\noindent
According to the measure function, the second argument should decrease with
each recursive call. The resulting termination condition
-*}
-
-(*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
-
-text{*\noindent
+\begin{quote}
+@{term[display]"n ~= 0 ==> m mod n < n"}
+\end{quote}
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -31,26 +29,21 @@
something else which leads to the same problem: it splits \isa{if}s if the
condition simplifies to neither \isa{True} nor \isa{False}. For
example, simplification reduces
-*}
-
-(*<*)term(*>*) "gcd(m,n) = k";
-
-text{*\noindent
+\begin{quote}
+@{term[display]"gcd(m,n) = k"}
+\end{quote}
in one step to
-*}
-
-(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
-
-text{*\noindent
+\begin{quote}
+@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
+\end{quote}
where the condition cannot be reduced further, and splitting leads to
-*}
-
-(*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
-
-text{*\noindent
-Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
-Fortunately, this problem can be avoided in many different ways.
+\begin{quote}
+@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
+\end{quote}
+Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
+an \isa{if}, it is unfolded again, which leads to an infinite chain of
+simplification steps. Fortunately, this problem can be avoided in many
+different ways.
The most radical solution is to disable the offending
\isa{split_if} as shown in the section on case splits in
--- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 06 15:26:53 2000 +0200
@@ -15,19 +15,19 @@
text{*\noindent
The datatype\index{*datatype} \isaindexbold{list} introduces two
constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
-empty list and the operator that adds an element to the front of a list. For
-example, the term \isa{Cons True (Cons False Nil)} is a value of type
-\isa{bool~list}, namely the list with the elements \isa{True} and
+empty~list and the operator that adds an element to the front of a list. For
+example, the term \isa{Cons True (Cons False Nil)} is a value of type
+@{typ"bool list"}, namely the list with the elements \isa{True} and
\isa{False}. Because this notation becomes unwieldy very quickly, the
datatype declaration is annotated with an alternative syntax: instead of
-\isa{Nil} and \isa{Cons~$x$~$xs$} we can write
+\isa{Nil} and \isa{Cons x xs} we can write
\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{$x$~\#~$xs$}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
alternative syntax is the standard syntax. Thus the list \isa{Cons True
-(Cons False Nil)} becomes \isa{True \# False \# []}. The annotation
+(Cons False Nil)} becomes @{term"True # False # []"}. The annotation
\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{$x$ \# $y$ \# $z$} is read as \isa{$x$
-\# ($y$ \# $z$)} and not as \isa{($x$ \# $y$) \# $z$}.
+the right, i.e.\ the term @{term"x # y # z"} is read as \isa{x
+\# (y \# z)} and not as \isa{(x \# y) \# z}.
\begin{warn}
Syntax annotations are a powerful but completely optional feature. You
@@ -48,8 +48,8 @@
(keyword \isacommand{consts}). (Apart from the declaration-before-use
restriction, the order of items in a theory file is unconstrained.) Function
\isa{app} is annotated with concrete syntax too. Instead of the prefix
-syntax \isa{app~$xs$~$ys$} the infix
-\isa{$xs$~\at~$ys$}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+syntax \isa{app xs ys} the infix
+@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
form. Both functions are defined recursively:
*}
@@ -190,8 +190,8 @@
The {\it assumptions} are the local assumptions for this subgoal and {\it
conclusion} is the actual proposition to be proved. Typical proof steps
that add new assumptions are induction or case distinction. In our example
-the only assumption is the induction hypothesis \isa{rev (rev list) =
- list}, where \isa{list} is a variable name chosen by Isabelle. If there
+the only assumption is the induction hypothesis @{term"rev (rev list) =
+ list"}, where \isa{list} is a variable name chosen by Isabelle. If there
are multiple assumptions, they are enclosed in the bracket pair
\indexboldpos{\isasymlbrakk}{$Isabrl} and
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{theory}~ToyList~=~PreList:%
+\isacommand{theory}\ ToyList\ =\ PreList:%
\begin{isamarkuptext}%
\noindent
HOL already has a predefined theory of lists called \isa{List} ---
@@ -9,25 +9,25 @@
theory that contains pretty much everything but lists, thus avoiding
ambiguities caused by defining lists twice.%
\end{isamarkuptext}%
-\isacommand{datatype}~'a~list~=~Nil~~~~~~~~~~~~~~~~~~~~~~~~~~({"}[]{"})\isanewline
-~~~~~~~~~~~~~~~~~|~Cons~'a~{"}'a~list{"}~~~~~~~~~~~~(\isakeyword{infixr}~{"}\#{"}~65)%
+\isacommand{datatype}\ 'a\ list\ =\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}[]{"})\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Cons\ 'a\ {"}'a\ list{"}\ \ \ \ \ \ \ \ \ \ \ \ (\isakeyword{infixr}\ {"}\#{"}\ 65)%
\begin{isamarkuptext}%
\noindent
The datatype\index{*datatype} \isaindexbold{list} introduces two
constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
-empty list and the operator that adds an element to the front of a list. For
-example, the term \isa{Cons True (Cons False Nil)} is a value of type
-\isa{bool~list}, namely the list with the elements \isa{True} and
+empty~list and the operator that adds an element to the front of a list. For
+example, the term \isa{Cons True (Cons False Nil)} is a value of type
+\isa{bool\ list}, namely the list with the elements \isa{True} and
\isa{False}. Because this notation becomes unwieldy very quickly, the
datatype declaration is annotated with an alternative syntax: instead of
-\isa{Nil} and \isa{Cons~$x$~$xs$} we can write
+\isa{Nil} and \isa{Cons x xs} we can write
\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{$x$~\#~$xs$}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{x\ \#\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
alternative syntax is the standard syntax. Thus the list \isa{Cons True
-(Cons False Nil)} becomes \isa{True \# False \# []}. The annotation
+(Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation
\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{$x$ \# $y$ \# $z$} is read as \isa{$x$
-\# ($y$ \# $z$)} and not as \isa{($x$ \# $y$) \# $z$}.
+the right, i.e.\ the term \isa{x\ \#\ y\ \#\ z} is read as \isa{x
+\# (y \# z)} and not as \isa{(x \# y) \# z}.
\begin{warn}
Syntax annotations are a powerful but completely optional feature. You
@@ -38,25 +38,25 @@
\end{warn}
Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
\end{isamarkuptext}%
-\isacommand{consts}~app~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}~~~(\isakeyword{infixr}~{"}@{"}~65)\isanewline
-~~~~~~~rev~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}%
+\isacommand{consts}\ app\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\ \ \ (\isakeyword{infixr}\ {"}@{"}\ 65)\isanewline
+\ \ \ \ \ \ \ rev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}%
\begin{isamarkuptext}%
\noindent
In contrast to ML, Isabelle insists on explicit declarations of all functions
(keyword \isacommand{consts}). (Apart from the declaration-before-use
restriction, the order of items in a theory file is unconstrained.) Function
\isa{app} is annotated with concrete syntax too. Instead of the prefix
-syntax \isa{app~$xs$~$ys$} the infix
-\isa{$xs$~\at~$ys$}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+syntax \isa{app xs ys} the infix
+\isa{xs\ @\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
form. Both functions are defined recursively:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
-{"}[]~@~ys~~~~~~~=~ys{"}\isanewline
-{"}(x~\#~xs)~@~ys~=~x~\#~(xs~@~ys){"}\isanewline
+{"}[]\ @\ ys\ \ \ \ \ \ \ =\ ys{"}\isanewline
+{"}(x\ \#\ xs)\ @\ ys\ =\ x\ \#\ (xs\ @\ ys){"}\isanewline
\isanewline
\isacommand{primrec}\isanewline
-{"}rev~[]~~~~~~~~=~[]{"}\isanewline
-{"}rev~(x~\#~xs)~~=~(rev~xs)~@~(x~\#~[]){"}%
+{"}rev\ []\ \ \ \ \ \ \ \ =\ []{"}\isanewline
+{"}rev\ (x\ \#\ xs)\ \ =\ (rev\ xs)\ @\ (x\ \#\ []){"}%
\begin{isamarkuptext}%
\noindent
The equations for \isa{app} and \isa{rev} hardly need comments:
@@ -94,7 +94,7 @@
To lessen this burden, quotation marks around a single identifier can be
dropped, unless the identifier happens to be a keyword, as in%
\end{isamarkuptext}%
-\isacommand{consts}~{"}end{"}~::~{"}'a~list~{\isasymRightarrow}~'a{"}%
+\isacommand{consts}\ {"}end{"}\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}%
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
@@ -114,7 +114,7 @@
Our goal is to show that reversing a list twice produces the original
list. The input line%
\end{isamarkuptext}%
-\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}%
+\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}%
\begin{isamarkuptxt}%
\index{*theorem|bold}\index{*simp (attribute)|bold}
\begin{itemize}
@@ -160,7 +160,7 @@
defined functions are best established by induction. In this case there is
not much choice except to induct on \isa{xs}:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs)%
+\isacommand{apply}(induct\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent\index{*induct_tac}%
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
@@ -183,8 +183,7 @@
The {\it assumptions} are the local assumptions for this subgoal and {\it
conclusion} is the actual proposition to be proved. Typical proof steps
that add new assumptions are induction or case distinction. In our example
-the only assumption is the induction hypothesis \isa{rev (rev list) =
- list}, where \isa{list} is a variable name chosen by Isabelle. If there
+the only assumption is the induction hypothesis \isa{rev\ (rev\ list)\ =\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
are multiple assumptions, they are enclosed in the bracket pair
\indexboldpos{\isasymlbrakk}{$Isabrl} and
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
@@ -213,7 +212,7 @@
proof}\indexbold{proof!abandon} (at the shell level type
\isacommand{oops}\indexbold{*oops}) we start a new proof:%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}%
\begin{isamarkuptxt}%
\noindent The keywords \isacommand{theorem}\index{*theorem} and
\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
@@ -225,7 +224,7 @@
\isa{ys}. Because \isa{\at} is defined by recursion on
the first argument, \isa{xs} is the correct one:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs)%
+\isacommand{apply}(induct\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent
This time not even the base case is solved automatically:%
@@ -246,8 +245,8 @@
This time the canonical proof procedure%
\end{isamarkuptext}%
-\isacommand{lemma}~app\_Nil2~[simp]:~{"}xs~@~[]~=~xs{"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ app\_Nil2\ [simp]:\ {"}xs\ @\ []\ =\ xs{"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{apply}(auto)%
\begin{isamarkuptxt}%
\noindent
@@ -272,8 +271,8 @@
Going back to the proof of the first lemma%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{apply}(auto)%
\begin{isamarkuptxt}%
\noindent
@@ -300,8 +299,8 @@
\begin{comment}
\isacommand{oops}%
\end{comment}
-\isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ app\_assoc\ [simp]:\ {"}(xs\ @\ ys)\ @\ zs\ =\ xs\ @\ (ys\ @\ zs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
@@ -309,15 +308,15 @@
Now we can go back and prove the first lemma%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
and then solve our main theorem:%
\end{isamarkuptext}%
-\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
--- a/doc-src/TutorialI/ToyList2/ToyList1 Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Sun Aug 06 15:26:53 2000 +0200
@@ -1,15 +1,15 @@
-theory ToyList = PreList:;
+theory ToyList = PreList:
datatype 'a list = Nil ("[]")
- | Cons 'a "'a list" (infixr "#" 65);
+ | Cons 'a "'a list" (infixr "#" 65)
consts app :: "'a list => 'a list => 'a list" (infixr "@" 65)
- rev :: "'a list => 'a list";
+ rev :: "'a list => 'a list"
primrec
"[] @ ys = ys"
-"(x # xs) @ ys = x # (xs @ ys)";
+"(x # xs) @ ys = x # (xs @ ys)"
primrec
"rev [] = []"
-"rev (x # xs) = (rev xs) @ (x # [])";
+"rev (x # xs) = (rev xs) @ (x # [])"
--- a/doc-src/TutorialI/ToyList2/ToyList2 Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList2 Sun Aug 06 15:26:53 2000 +0200
@@ -1,18 +1,18 @@
-lemma app_Nil2 [simp]: "xs @ [] = xs";
-apply(induct_tac xs);
-apply(auto);
-.;
+lemma app_Nil2 [simp]: "xs @ [] = xs"
+apply(induct_tac xs)
+apply(auto)
+.
-lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
-apply(induct_tac xs);
-by(auto);
+lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
+apply(induct_tac xs)
+by(auto)
-lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
-apply(induct_tac xs);
-by(auto);
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
+apply(induct_tac xs)
+by(auto)
-theorem rev_rev [simp]: "rev(rev xs) = xs";
-apply(induct_tac xs);
-by(auto);
+theorem rev_rev [simp]: "rev(rev xs) = xs"
+apply(induct_tac xs)
+by(auto)
-end;
+end
--- a/doc-src/TutorialI/Trie/Trie.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Sun Aug 06 15:26:53 2000 +0200
@@ -81,8 +81,8 @@
options:
*};
-theorems [simp] = Let_def;
-theorems [split] = option.split;
+lemmas [simp] = Let_def;
+lemmas [split] = option.split;
text{*\noindent
The reason becomes clear when looking (probably after a failed proof
@@ -105,7 +105,6 @@
\isa{as} is instantiated.
The start of the proof is completely conventional:
*};
-
apply(induct_tac as, auto);
txt{*\noindent
@@ -119,15 +118,13 @@
well now. It turns out that instead of induction, case distinction
suffices:
*};
-
-apply(case_tac[!] bs);
-by(auto);
+by(case_tac[!] bs, auto);
text{*\noindent
-Both \isaindex{case_tac} and \isaindex{induct_tac}
-take an optional first argument that specifies the range of subgoals they are
-applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
-subgoal numbers are also allowed.
+All methods ending in \isa{tac} take an optional first argument that
+specifies the range of subgoals they are applied to, where \isa{[!]} means all
+subgoals, i.e.\ \isa{[1-3]} in our case. Individual subgoal numbers,
+e.g. \isa{[2]} are also allowed.
This proof may look surprisingly straightforward. However, note that this
comes at a cost: the proof script is unreadable because the
--- a/doc-src/TutorialI/Trie/document/Trie.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Sun Aug 06 15:26:53 2000 +0200
@@ -70,8 +70,8 @@
expand all \isa{let}s and to split all \isa{case}-constructs over
options:%
\end{isamarkuptext}%
-\isacommand{theorems}\ [simp]\ =\ Let\_def\isanewline
-\isacommand{theorems}\ [split]\ =\ option.split%
+\isacommand{lemmas}\ [simp]\ =\ Let\_def\isanewline
+\isacommand{lemmas}\ [split]\ =\ option.split%
\begin{isamarkuptext}%
\noindent
The reason becomes clear when looking (probably after a failed proof
@@ -106,14 +106,13 @@
well now. It turns out that instead of induction, case distinction
suffices:%
\end{isamarkuptxt}%
-\isacommand{apply}(case\_tac[!]\ bs)\isanewline
-\isacommand{by}(auto)%
+\isacommand{by}(case\_tac[!]\ bs,\ auto)%
\begin{isamarkuptext}%
\noindent
-Both \isaindex{case_tac} and \isaindex{induct_tac}
-take an optional first argument that specifies the range of subgoals they are
-applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
-subgoal numbers are also allowed.
+All methods ending in \isa{tac} take an optional first argument that
+specifies the range of subgoals they are applied to, where \isa{[!]} means all
+subgoals, i.e.\ \isa{[1-3]} in our case. Individual subgoal numbers,
+e.g. \isa{[2]} are also allowed.
This proof may look surprisingly straightforward. However, note that this
comes at a cost: the proof script is unreadable because the
--- a/doc-src/TutorialI/appendix.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex Sun Aug 06 15:26:53 2000 +0200
@@ -118,179 +118,33 @@
\end{figure}
-\begin{figure}[htbp]
-
-%FIXME too long to be useful!??
-\begin{center}
-\begin{tabular}{|lll|}
-\hline
-\texttt{ML} &
-\texttt{ML_command} &
-\texttt{ML_setup} \\
-\texttt{also} &
-\texttt{apply} &
-\texttt{apply_end} \\
-\texttt{arities} &
-\texttt{assume} &
-\texttt{axclass} \\
-\texttt{axioms} &
-\texttt{back} &
-\texttt{by} \\
-\texttt{cannot_undo} &
-\texttt{case} &
-\texttt{cd} \\
-\texttt{chapter} &
-\texttt{classes} &
-\texttt{classrel} \\
-\texttt{clear_undos} &
-\texttt{coinductive} &
-\texttt{commit} \\
-\texttt{constdefs} &
-\texttt{consts} &
-\texttt{context} \\
-\texttt{datatype} &
-\texttt{def} &
-\texttt{defaultsort} \\
-\texttt{defer} &
-\texttt{defer_recdef} &
-\texttt{defs} \\
-\texttt{disable_pr} &
-\texttt{enable_pr} &
-\texttt{end} \\
-\texttt{exit} &
-\texttt{finally} &
-\texttt{fix} \\
-\texttt{from} &
-\texttt{global} &
-\texttt{have} \\
-\texttt{header} &
-\texttt{help} &
-\texttt{hence} \\
-\texttt{hide} &
-\texttt{inductive} &
-\texttt{inductive_cases} \\
-\texttt{init_toplevel} &
-\texttt{instance} &
-\texttt{judgment} \\
-\texttt{kill} &
-\texttt{kill_thy} &
-\texttt{lemma} \\
-\texttt{lemmas} &
-\texttt{let} &
-\texttt{local} \\
-\texttt{moreover} &
-\texttt{next} &
-\texttt{nonterminals} \\
-\texttt{note} &
-\texttt{obtain} &
-\texttt{oops} \\
-\texttt{oracle} &
-\texttt{parse_ast_translation} &
-\texttt{parse_translation} \\
-\texttt{pr} &
-\texttt{prefer} &
-\texttt{presume} \\
-\texttt{pretty_setmargin} &
-\texttt{primrec} &
-\texttt{print_ast_translation} \\
-\texttt{print_attributes} &
-\texttt{print_binds} &
-\texttt{print_cases} \\
-\texttt{print_claset} &
-\texttt{print_context} &
-\texttt{print_facts} \\
-\texttt{print_methods} &
-\texttt{print_simpset} &
-\texttt{print_syntax} \\
-\texttt{print_theorems} &
-\texttt{print_theory} &
-\texttt{print_translation} \\
-\texttt{proof} &
-\texttt{prop} &
-\texttt{pwd} \\
-\texttt{qed} &
-\texttt{quit} &
-\texttt{recdef} \\
-\texttt{record} &
-\texttt{redo} &
-\texttt{remove_thy} \\
-\texttt{rep_datatype} &
-\texttt{sect} &
-\texttt{section} \\
-\texttt{setup} &
-\texttt{show} &
-\texttt{sorry} \\
-\texttt{subsect} &
-\texttt{subsection} &
-\texttt{subsubsect} \\
-\texttt{subsubsection} &
-\texttt{syntax} &
-\texttt{term} \\
-\texttt{text} &
-\texttt{text_raw} &
-\texttt{then} \\
-\texttt{theorem} &
-\texttt{theorems} &
-\texttt{theory} \\
-\texttt{thm} &
-\texttt{thms_containing} &
-\texttt{thus} \\
-\texttt{token_translation} &
-\texttt{touch_all_thys} &
-\texttt{touch_child_thys} \\
-\texttt{touch_thy} &
-\texttt{translations} &
-\texttt{txt} \\
-\texttt{txt_raw} &
-\texttt{typ} &
-\texttt{typed_print_translation} \\
-\texttt{typedecl} &
-\texttt{typedef} &
-\texttt{types} \\
-\texttt{ultimately} &
-\texttt{undo} &
-\texttt{undos_proof} \\
-\texttt{update_thy} &
-\texttt{update_thy_only} &
-\texttt{use} \\
-\texttt{use_thy} &
-\texttt{use_thy_only} &
-\texttt{welcome} \\
-\texttt{with} &
- &
- \\
-\hline
-\end{tabular}
-\end{center}
-
-\begin{center}
-\begin{tabular}{|lllll|}
-\hline
-\texttt{and} &
-\texttt{binder} &
-\texttt{con_defs} &
-\texttt{concl} &
-\texttt{congs} \\
-\texttt{distinct} &
-\texttt{files} &
-\texttt{in} &
-\texttt{induction} &
-\texttt{infixl} \\
-\texttt{infixr} &
-\texttt{inject} &
-\texttt{intrs} &
-\texttt{is} &
-\texttt{monos} \\
-\texttt{output} &
-\texttt{where} &
- &
- &
- \\
-\hline
-\end{tabular}
-\end{center}
-
-
-\caption{Commands and minor keywords in HOL theories}
-\label{fig:keywords}
-\end{figure}
+%\begin{figure}[htbp]
+%\begin{center}
+%\begin{tabular}{|lllll|}
+%\hline
+%\texttt{and} &
+%\texttt{binder} &
+%\texttt{con_defs} &
+%\texttt{concl} &
+%\texttt{congs} \\
+%\texttt{distinct} &
+%\texttt{files} &
+%\texttt{in} &
+%\texttt{induction} &
+%\texttt{infixl} \\
+%\texttt{infixr} &
+%\texttt{inject} &
+%\texttt{intrs} &
+%\texttt{is} &
+%\texttt{monos} \\
+%\texttt{output} &
+%\texttt{where} &
+% &
+% &
+% \\
+%\hline
+%\end{tabular}
+%\end{center}
+%\caption{Minor keywords in HOL theories}
+%\label{fig:keywords}
+%\end{figure}
--- a/doc-src/TutorialI/basics.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/basics.tex Sun Aug 06 15:26:53 2000 +0200
@@ -65,7 +65,11 @@
\begin{center}\small
\url{http://isabelle.in.tum.de/library/}
\end{center}
-and is recommended browsing.
+and is recommended browsing. Note that most of the theories in the library
+are based on classical Isabelle without the Isar extension. This means that
+they look slightly different than the theories in this tutorial, and that all
+proofs are in separate ML files.
+
\begin{warn}
HOL contains a theory \ttindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
@@ -275,13 +279,11 @@
mathematical symbols. For those that do not, remember that ASCII-equivalents
are shown in figure~\ref{fig:ascii} in the appendix.
-Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
-for example Proof General, require each command to be terminated by a
-semicolon, whereas others, for example the shell level, do not. But even at
-the shell level it is advisable to use semicolons to enforce that a command
+Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
+Commands may but need not be terminated by semicolons.
+At the shell level it is advisable to use semicolons to enforce that a command
is executed immediately; otherwise Isabelle may wait for the next keyword
-before it knows that the command is complete. Note that for readibility
-reasons we often drop the final semicolon in the text.
+before it knows that the command is complete.
\section{Getting started}
@@ -296,3 +298,4 @@
type each command into the file first and then enter it into Isabelle by
copy-and-paste, thus ensuring that you have a complete record of your theory.
As mentioned above, Proof General offers a much superior interface.
+If you have installed Proof General, you can start it with \texttt{Isabelle}.
--- a/doc-src/TutorialI/fp.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Sun Aug 06 15:26:53 2000 +0200
@@ -5,12 +5,12 @@
constructs and proof procedures introduced are general purpose and recur in
any specification or verification task.
-The dedicated functional programmer should be warned: HOL offers only {\em
- total functional programming} --- all functions in HOL must be total; lazy
-data structures are not directly available. On the positive side, functions
-in HOL need not be computable: HOL is a specification language that goes well
-beyond what can be expressed as a program. However, for the time being we
-concentrate on the computable.
+The dedicated functional programmer should be warned: HOL offers only
+\emph{total functional programming} --- all functions in HOL must be total;
+lazy data structures are not directly available. On the positive side,
+functions in HOL need not be computable: HOL is a specification language that
+goes well beyond what can be expressed as a program. However, for the time
+being we concentrate on the computable.
\section{An introductory theory}
\label{sec:intro-theory}
@@ -119,10 +119,7 @@
named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
automatically loads all the required parent theories from their respective
files (which may take a moment, unless the theories are already loaded and
- the files have not been modified). The only time when you need to load a
- theory by hand is when you simply want to check if it loads successfully
- without wanting to make use of the theory itself. This you can do by typing
- \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
+ the files have not been modified).
If you suddenly discover that you need to modify a parent theory of your
current theory you must first abandon your current theory\indexbold{abandon
@@ -131,6 +128,11 @@
been modified you go back to your original theory. When its first line
\isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
modified parent is reloaded automatically.
+
+ The only time when you need to load a theory by hand is when you simply
+ want to check if it loads successfully without wanting to make use of the
+ theory itself. This you can do by typing
+ \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
\end{description}
Further commands are found in the Isabelle/Isar Reference Manual.
@@ -372,23 +374,7 @@
\subsection{Products}
-
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
- $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
-are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
-\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
-\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
-\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
- $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
-
-It is possible to use (nested) tuples as patterns in abstractions, for
-example \isa{\isasymlambda(x,y,z).x+y+z} and
-\isa{\isasymlambda((x,y),z).x+y+z}.
-In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
-most variable binding constructs. Typical examples are
-
-\input{Misc/document/pairs.tex}%
-Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
+\input{Misc/document/pairs.tex}
%FIXME move stuff below into section on proofs about products?
\begin{warn}
@@ -401,10 +387,13 @@
theorem proving with tuple patterns.
\end{warn}
-Finally note that products, like natural numbers, are datatypes, which means
+Note that products, like natural numbers, are datatypes, which means
in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
products (see \S\ref{proofs-about-products}).
+Instead of tuples with many components (where ``many'' is not much above 2),
+it is far preferable to use record types (see \S\ref{sec:records}).
+
\section{Definitions}
\label{sec:Definitions}
@@ -455,11 +444,11 @@
\label{sec:Simplification}
\index{simplification|(}
-So far we have proved our theorems by \isa{auto}, which ``simplifies'' all
-subgoals. In fact, \isa{auto} can do much more than that, except that it
-did not need to so far. However, when you go beyond toy examples, you need to
-understand the ingredients of \isa{auto}. This section covers the method
-that \isa{auto} always applies first, namely simplification.
+So far we have proved our theorems by \isa{auto}, which ``simplifies''
+\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
+that it did not need to so far. However, when you go beyond toy examples, you
+need to understand the ingredients of \isa{auto}. This section covers the
+method that \isa{auto} always applies first, namely simplification.
Simplification is one of the central theorem proving tools in Isabelle and
many other systems. The tool itself is called the \bfindex{simplifier}. The
@@ -505,8 +494,8 @@
The simplification attribute of theorems can be turned on and off as follows:
\begin{ttbox}
-theorems [simp] = \(list of theorem names\);
-theorems [simp del] = \(list of theorem names\);
+lemmas [simp] = \(list of theorem names\);
+lemmas [simp del] = \(list of theorem names\);
\end{ttbox}
As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification