--- a/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 12:29:10 2001 +0100
@@ -1,6 +1,6 @@
(*<*)theory CTL = Base:;(*>*)
-subsection{*Computation Tree Logic---CTL*};
+subsection{*Computation Tree Logic --- CTL*};
text{*\label{sec:CTL}
The semantics of PDL only needs reflexive transitive closure.
--- a/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 24 12:29:10 2001 +0100
@@ -125,7 +125,7 @@
text{*
The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
-that the assumption is left unchanged---otherwise the @{text"\<forall>p"} is turned
+that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
into a @{text"\<And>p"}, which would complicate matters below. As it is,
@{thm[source]Avoid_in_lfp} is now
@{thm[display]Avoid_in_lfp[no_vars]}
--- a/doc-src/TutorialI/CTL/PDL.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy Wed Jan 24 12:29:10 2001 +0100
@@ -1,6 +1,6 @@
(*<*)theory PDL = Base:(*>*)
-subsection{*Propositional Dynamic Logic---PDL*}
+subsection{*Propositional Dynamic Logic --- PDL*}
text{*\index{PDL|(}
The formulae of PDL are built up from atomic propositions via the customary
@@ -68,7 +68,7 @@
fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
@{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
find it hard to see that @{term"mc(EF f)"} contains exactly those states from
-which there is a path to a state where @{term f} is true, do not worry---that
+which there is a path to a state where @{term f} is true, do not worry --- that
will be proved in a moment.
First we prove monotonicity of the function inside @{term lfp}
--- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 24 12:29:10 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{CTL}%
%
-\isamarkupsubsection{Computation Tree Logic---CTL%
+\isamarkupsubsection{Computation Tree Logic --- CTL%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 12:29:10 2001 +0100
@@ -128,7 +128,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
-that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
+that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
\begin{isabelle}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 12:29:10 2001 +0100
@@ -2,7 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{PDL}%
%
-\isamarkupsubsection{Propositional Dynamic Logic---PDL%
+\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
}
%
\begin{isamarkuptext}%
@@ -68,7 +68,7 @@
fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
-which there is a path to a state where \isa{f} is true, do not worry---that
+which there is a path to a state where \isa{f} is true, do not worry --- that
will be proved in a moment.
First we prove monotonicity of the function inside \isa{lfp}
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Jan 24 12:29:10 2001 +0100
@@ -49,7 +49,7 @@
@{text"exec"} that takes a list of instructions, a store (modelled as a
function from addresses to values, just like the environment for
evaluating expressions), and a stack (modelled as a list) of values,
-and returns the stack at the end of the execution---the store remains
+and returns the stack at the end of the execution --- the store remains
unchanged:
*}
@@ -110,15 +110,15 @@
apply(induct_tac xs, simp, simp split: instr.split);
(*<*)done(*>*)
text{*\noindent
-Note that because \isaindex{auto} performs simplification, it can
-also be modified in the same way @{text simp} can. Thus the proof can be
+Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
+be modified in the same way @{text simp} can. Thus the proof can be
rewritten as
*}
(*<*)
declare exec_app[simp del];
lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
(*>*)
-apply(induct_tac xs, auto split: instr.split);
+apply(induct_tac xs, simp_all split: instr.split);
(*<*)done(*>*)
text{*\noindent
Although this is more compact, it is less clear for the reader of the proof.
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 24 12:29:10 2001 +0100
@@ -46,7 +46,7 @@
\isa{exec} that takes a list of instructions, a store (modelled as a
function from addresses to values, just like the environment for
evaluating expressions), and a stack (modelled as a list) of values,
-and returns the stack at the end of the execution---the store remains
+and returns the stack at the end of the execution --- the store remains
unchanged:%
\end{isamarkuptext}%
\isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline
@@ -102,11 +102,11 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\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
+Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
+be modified in the same way \isa{simp} can. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\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 Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Wed Jan 24 12:29:10 2001 +0100
@@ -28,13 +28,13 @@
text{*\noindent
Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
except that we have fixed the values to be of type @{typ"nat"} and that we
-have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean
+have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
expressions can be arithmetic comparisons, conjunctions and negations.
The semantics is fixed via two evaluation functions
*}
-consts evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
- evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
+consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
+ evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
text{*\noindent
that take an expression and an environment (a mapping from variables @{typ"'a"} to values
@@ -53,15 +53,15 @@
"evala (Num n) env = n"
"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
- "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
- "evalb (Neg b) env = (\\<not> evalb b env)"
+ "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
+ "evalb (Neg b) env = (\<not> evalb b env)"
text{*\noindent
In the same fashion we also define two functions that perform substitution:
*}
-consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
- substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
+consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
+ substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
text{*\noindent
The first argument is a function mapping variables to expressions, the
@@ -93,8 +93,8 @@
theorems simultaneously:
*}
-lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
- evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
+lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
+ evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
apply(induct_tac a and b);
txt{*\noindent
@@ -110,7 +110,7 @@
\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
where each variable $x@i$ is of type $\tau@i$. Induction is started by
\begin{isabelle}
-\isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"}
+\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
\end{isabelle}
\begin{exercise}
--- a/doc-src/TutorialI/Datatype/Nested.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy Wed Jan 24 12:29:10 2001 +0100
@@ -9,12 +9,12 @@
where function symbols can be applied to a list of arguments:
*}
(*<*)hide const Var(*>*)
-datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
+datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
text{*\noindent
Note that we need to quote @{text term} on the left to avoid confusion with
the Isabelle command \isacommand{term}.
-Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
+Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of
function symbols.
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
[Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
@@ -41,8 +41,8 @@
*}
consts
-subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term \<Rightarrow> ('a,'b)term"
-substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list";
+subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term"
+substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
primrec
"subst s (Var x) = s x"
@@ -62,8 +62,8 @@
strengthened and proved as follows:
*}
-lemma "subst Var t = (t ::('a,'b)term) \<and>
- substs Var ts = (ts::('a,'b)term list)";
+lemma "subst Var t = (t ::('v,'f)term) \<and>
+ substs Var ts = (ts::('v,'f)term list)";
apply(induct_tac t and ts, simp_all);
done
@@ -72,7 +72,7 @@
leaves variables unchanged: @{prop"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 @{text"('a,'b)"}. As a result, induction would fail
+parameters @{text"('v,'f)"}. As a result, induction would fail
because the two halves of the goal would be unrelated.
\begin{exercise}
@@ -84,7 +84,7 @@
its definition is found in theorem @{thm[source]o_def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
- Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}
+ Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"}
that recursively reverses the order of arguments of all function symbols in a
term. Prove that @{prop"trev(trev t) = t"}.
\end{exercise}
@@ -120,7 +120,7 @@
and to define functions with \isacommand{recdef} instead.
The details are explained in \S\ref{sec:nested-recdef} below.
-Of course, you may also combine mutual and nested recursion. For example,
+Of course, you may also combine mutual and nested recursion of datatypes. For example,
constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
*}
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 24 12:29:10 2001 +0100
@@ -27,7 +27,7 @@
\noindent
Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
except that we have fixed the values to be of type \isa{nat} and that we
-have fixed the two binary operations \isa{aexp{\isachardot}Sum} and \isa{Diff}. Boolean
+have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
expressions can be arithmetic comparisons, conjunctions and negations.
The semantics is fixed via two evaluation functions%
\end{isamarkuptext}%
@@ -100,7 +100,7 @@
\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
where each variable $x@i$ is of type $\tau@i$. Induction is started by
\begin{isabelle}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isa{and} \dots\ \isa{and} $x@n$\isa{{\isacharparenright}}
+\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
\end{isabelle}
\begin{exercise}
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Jan 24 12:29:10 2001 +0100
@@ -8,12 +8,12 @@
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}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Note that we need to quote \isa{term} on the left to avoid confusion with
the Isabelle command \isacommand{term}.
-Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
+Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of
function symbols.
A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
suitable values, e.g.\ numbers or strings.
@@ -38,8 +38,8 @@
lists, we need to define two substitution functions simultaneously:%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
-substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}\isanewline
+subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\isanewline
+substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}\isanewline
\isanewline
\isacommand{primrec}\isanewline
\ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline
@@ -58,8 +58,8 @@
the fact that the identity substitution does not change a term needs to be
strengthened and proved as follows:%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
-\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
@@ -68,7 +68,7 @@
leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ 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{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
+parameters \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}}. As a result, induction would fail
because the two halves of the goal would be unrelated.
\begin{exercise}
@@ -82,7 +82,7 @@
its definition is found in theorem \isa{o{\isacharunderscore}def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
- Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term}
+ Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
that recursively reverses the order of arguments of all function symbols in a
term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
\end{exercise}
@@ -118,7 +118,7 @@
and to define functions with \isacommand{recdef} instead.
The details are explained in \S\ref{sec:nested-recdef} below.
-Of course, you may also combine mutual and nested recursion. For example,
+Of course, you may also combine mutual and nested recursion of datatypes. For example,
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 24 12:29:10 2001 +0100
@@ -1,8 +1,8 @@
%
\begin{isabellebody}%
\def\isabellecontext{unfoldnested}%
-\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
-\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
+\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 12:29:10 2001 +0100
@@ -1,8 +1,8 @@
(*<*)
theory unfoldnested = Main:;
(*>*)
-datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
-and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
+datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
+and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 12:29:10 2001 +0100
@@ -55,7 +55,7 @@
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
text{*\noindent
-The evaluation if If-expressions proceeds as for @{typ"boolex"}:
+The evaluation of If-expressions proceeds as for @{typ"boolex"}:
*}
consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 24 12:29:10 2001 +0100
@@ -55,7 +55,7 @@
\isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex%
\begin{isamarkuptext}%
\noindent
-The evaluation if If-expressions proceeds as for \isa{boolex}:%
+The evaluation of If-expressions proceeds as for \isa{boolex}:%
\end{isamarkuptext}%
\isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
--- a/doc-src/TutorialI/Misc/Itrev.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Jan 24 12:29:10 2001 +0100
@@ -26,7 +26,7 @@
The key heuristic, and the main point of this section, is to
generalize the goal before induction. The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
-step to go through. Let us now illustrate the idea with an example.
+step to go through. Let us illustrate the idea with an example.
Function @{term"rev"} has quadratic worst-case running time
because it calls function @{text"@"} for each element of the list and
@@ -61,7 +61,7 @@
txt{*\noindent
Unfortunately, this is not a complete success:
-@{subgoals[display,indent=0,margin=65]}
+@{subgoals[display,indent=0,margin=70]}
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed
argument, @{term"[]"}. This suggests a heuristic:
@@ -69,7 +69,7 @@
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
-just not true---the correct generalization is
+just not true --- the correct generalization is
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
@@ -112,13 +112,6 @@
The variables that require generalization are typically those that
change in recursive calls.
-In general, if you have tried the above heuristics and still find your
-induction does not go through, and no obvious lemma suggests itself, you may
-need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. You
-will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
-to learn about some advanced techniques for inductive proofs.
-
A final point worth mentioning is the orientation of the equation we just
proved: the more complex notion (@{term itrev}) is on the left-hand
side, the simpler one (@{term rev}) on the right-hand side. This constitutes
@@ -130,6 +123,13 @@
This heuristic is tricky to apply because it is not obvious that
@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
+
+In general, if you have tried the above heuristics and still find your
+induction does not go through, and no obvious lemma suggests itself, you may
+need to generalize your proposition even further. This requires insight into
+the problem at hand and is beyond simple rules of thumb. You
+will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
+to learn about some advanced techniques for inductive proofs.
*}
(*<*)
end
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 24 12:29:10 2001 +0100
@@ -28,7 +28,7 @@
The key heuristic, and the main point of this section, is to
generalize the goal before induction. The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
-step to go through. Let us now illustrate the idea with an example.
+step to go through. Let us illustrate the idea with an example.
Function \isa{rev} has quadratic worst-case running time
because it calls function \isa{{\isacharat}} for each element of the list and
@@ -62,8 +62,7 @@
Unfortunately, this is not a complete success:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed
@@ -72,7 +71,7 @@
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
-just not true---the correct generalization is%
+just not true --- the correct generalization is%
\end{isamarkuptxt}%
\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
\begin{isamarkuptxt}%
@@ -114,13 +113,6 @@
The variables that require generalization are typically those that
change in recursive calls.
-In general, if you have tried the above heuristics and still find your
-induction does not go through, and no obvious lemma suggests itself, you may
-need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. You
-will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
-to learn about some advanced techniques for inductive proofs.
-
A final point worth mentioning is the orientation of the equation we just
proved: the more complex notion (\isa{itrev}) is on the left-hand
side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
@@ -131,7 +123,14 @@
\end{quote}
This heuristic is tricky to apply because it is not obvious that
\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
-happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
+happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
+
+In general, if you have tried the above heuristics and still find your
+induction does not go through, and no obvious lemma suggests itself, you may
+need to generalize your proposition even further. This requires insight into
+the problem at hand and is beyond simple rules of thumb. You
+will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
+to learn about some advanced techniques for inductive proofs.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 12:29:10 2001 +0100
@@ -69,7 +69,8 @@
For more complex goals, there is the special method \isaindexbold{arith}
(which attacks the first subgoal). It proves arithmetic goals involving the
usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
-\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
+\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
+and the operations
\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
For example,%
--- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 12:29:10 2001 +0100
@@ -52,7 +52,7 @@
where the list of \emph{modifiers} fine tunes the behaviour and may
be empty. Most if not all of the proofs seen so far could have been performed
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
-only the first subgoal and may thus need to be repeated---use
+only the first subgoal and may thus need to be repeated --- use
\isaindex{simp_all} to simplify all subgoals.
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
@@ -109,7 +109,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-There are three options that influence the treatment of assumptions:
+There are three modifiers that influence the treatment of assumptions:
\begin{description}
\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
means that assumptions are completely ignored.
@@ -122,7 +122,7 @@
\end{description}
Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
the problematic subgoal above.
-Note that only one of the options is allowed, and it must precede all
+Note that only one of the modifiers is allowed, and it must precede all
other arguments.%
\end{isamarkuptext}%
%
@@ -169,13 +169,14 @@
rule because this defeats the whole purpose of an abbreviation.
\begin{warn}
- If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
- occurrences of $f$ with at least two arguments. Thus it is safer to define
- $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
+ If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
+ occurrences of $f$ with at least two arguments. This may be helpful for unfolding
+ $f$ selectively, but it may also get in the way. Defining
+ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying Let-Expressions%
+\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
}
%
\begin{isamarkuptext}%
@@ -360,7 +361,7 @@
Applying instance of rewrite rule:
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
Rewriting:
-rev [x] == rev [] @ [x]
+rev [a] == rev [] @ [a]
Applying instance of rewrite rule:
rev [] == []
Rewriting:
@@ -368,11 +369,11 @@
Applying instance of rewrite rule:
[] @ ?y == ?y
Rewriting:
-[] @ [x] == [x]
+[] @ [a] == [a]
Applying instance of rewrite rule:
?x3 \# ?t3 = ?t3 == False
Rewriting:
-[x] = [] == False
+[a] = [] == False
\end{ttbox}
In more complicated cases, the trace can be quite lenghty, especially since
--- a/doc-src/TutorialI/Misc/natsum.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Wed Jan 24 12:29:10 2001 +0100
@@ -69,7 +69,8 @@
For more complex goals, there is the special method \isaindexbold{arith}
(which attacks the first subgoal). It proves arithmetic goals involving the
usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
-@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
+@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
+and the operations
@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
For example,
--- a/doc-src/TutorialI/Misc/simp.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Wed Jan 24 12:29:10 2001 +0100
@@ -49,7 +49,7 @@
where the list of \emph{modifiers} fine tunes the behaviour and may
be empty. Most if not all of the proofs seen so far could have been performed
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
-only the first subgoal and may thus need to be repeated---use
+only the first subgoal and may thus need to be repeated --- use
\isaindex{simp_all} to simplify all subgoals.
Note that @{text simp} fails if nothing changes.
*}
@@ -106,7 +106,7 @@
done
text{*\noindent
-There are three options that influence the treatment of assumptions:
+There are three modifiers that influence the treatment of assumptions:
\begin{description}
\item[@{text"(no_asm)"}]\indexbold{*no_asm}
means that assumptions are completely ignored.
@@ -119,7 +119,7 @@
\end{description}
Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
the problematic subgoal above.
-Note that only one of the options is allowed, and it must precede all
+Note that only one of the modifiers is allowed, and it must precede all
other arguments.
*}
@@ -165,13 +165,14 @@
rule because this defeats the whole purpose of an abbreviation.
\begin{warn}
- If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
- occurrences of $f$ with at least two arguments. Thus it is safer to define
- $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
+ If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
+ occurrences of $f$ with at least two arguments. This may be helpful for unfolding
+ $f$ selectively, but it may also get in the way. Defining
+ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
\end{warn}
*}
-subsubsection{*Simplifying Let-Expressions*}
+subsubsection{*Simplifying {\tt\slshape let}-Expressions*}
text{*\index{simplification!of let-expressions}
Proving a goal containing \isaindex{let}-expressions almost invariably
@@ -370,7 +371,7 @@
Applying instance of rewrite rule:
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
Rewriting:
-rev [x] == rev [] @ [x]
+rev [a] == rev [] @ [a]
Applying instance of rewrite rule:
rev [] == []
Rewriting:
@@ -378,11 +379,11 @@
Applying instance of rewrite rule:
[] @ ?y == ?y
Rewriting:
-[] @ [x] == [x]
+[] @ [a] == [a]
Applying instance of rewrite rule:
?x3 \# ?t3 = ?t3 == False
Rewriting:
-[x] = [] == False
+[a] = [] == False
\end{ttbox}
In more complicated cases, the trace can be quite lenghty, especially since
--- a/doc-src/TutorialI/Recdef/Induction.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy Wed Jan 24 12:29:10 2001 +0100
@@ -8,7 +8,7 @@
equations) are simplification rules, we might like to prove something about
our function. Since the function is recursive, the natural proof principle is
again induction. But this time the structural form of induction that comes
-with datatypes is unlikely to work well---otherwise we could have defined the
+with datatypes is unlikely to work well --- otherwise we could have defined the
function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
proves a suitable induction rule $f$@{text".induct"} that follows the
recursion pattern of the particular function $f$. We call this
@@ -51,7 +51,7 @@
\end{quote}\index{*induct_tac}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
+contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 12:29:10 2001 +0100
@@ -8,7 +8,7 @@
equations) are simplification rules, we might like to prove something about
our function. Since the function is recursive, the natural proof principle is
again induction. But this time the structural form of induction that comes
-with datatypes is unlikely to work well---otherwise we could have defined the
+with datatypes is unlikely to work well --- otherwise we could have defined the
function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
recursion pattern of the particular function $f$. We call this
@@ -53,7 +53,7 @@
\end{quote}\index{*induct_tac}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
+contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
--- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 12:29:10 2001 +0100
@@ -30,7 +30,7 @@
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-It was not proved automatically because of the special nature of \isa{{\isacharminus}}
+It was not proved automatically because of the special nature of subtraction
on \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 12:29:10 2001 +0100
@@ -32,7 +32,7 @@
lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
txt{*\noindent
-It was not proved automatically because of the special nature of @{text"-"}
+It was not proved automatically because of the special nature of subtraction
on @{typ"nat"}. This requires more arithmetic than is tried by default:
*}
--- a/doc-src/TutorialI/Rules/rules.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Wed Jan 24 12:29:10 2001 +0100
@@ -71,7 +71,7 @@
like this:
\[ \infer{P\conj Q}{P & Q} \]
The rule introduces the conjunction
-symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we
+symbol~($\conj$) in its conclusion. In Isabelle proofs we
mainly reason backwards. When we apply this rule, the subgoal already has
the form of a conjunction; the proof step makes this conjunction symbol
disappear.
@@ -170,7 +170,7 @@
\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
\end{isabelle}
When we use this sort of elimination rule backwards, it produces
-a case split. (We have this before, in proofs by induction.) The following proof
+a case split. (We have seen this before, in proofs by induction.) The following proof
illustrates the use of disjunction elimination.
\begin{isabelle}
\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\
@@ -184,7 +184,7 @@
We assume \isa{P\ \isasymor\ Q} and
must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
elimination rule, \isa{disjE}. The method {\isa{erule}} applies an
-elimination rule to the assumptions, searching for one that matches the
+elimination rule, searching for an assumption that matches the
rule's first premise. Deleting that assumption, it
return the subgoals for the remaining premises. Most of the
time, this is the best way to use elimination rules; only rarely is there
@@ -394,7 +394,7 @@
As we have seen, Isabelle rules involve variables that begin with a
question mark. These are called \textbf{schematic} variables and act as
placeholders for terms. \textbf{Unification} refers to the process of
-making two terms identical, possibly by replacing their variables by
+making two terms identical, possibly by replacing their schematic variables by
terms. The simplest case is when the two terms are already the same. Next
simplest is when the variables in only one of the term
are replaced; this is called \textbf{pattern-matching}. The
@@ -440,7 +440,7 @@
A typical substitution rule allows us to replace one term by
another if we know that two terms are equal.
\[ \infer{P[t/x]}{s=t & P[s/x]} \]
-The conclusion uses a notation for substitution: $P[t/x]$ is the result of
+The rule uses a notation for substitution: $P[t/x]$ is the result of
replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions
designated by~$x$. For example, it can
derive symmetry of equality from reflexivity. Using $x=s$ for~$P$
@@ -566,7 +566,7 @@
\isa{erule_tac} since above we used \isa{erule}.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
-\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\
+\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\
\isakeyword{in}\ ssubst)
\end{isabelle}
%
@@ -580,7 +580,7 @@
An alternative to \isa{rule_tac} is to use \isa{rule} with the
\isa{of} directive, described in \S\ref{sec:forward} below. An
advantage of \isa{rule_tac} is that the instantiations may refer to
-variables bound in the current subgoal.
+\isasymAnd-bound variables in the current subgoal.
\section{Negation}
@@ -632,7 +632,7 @@
\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
R"\isanewline
-\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
+\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
contrapos_np)\isanewline
\isacommand{apply}\ intro\isanewline
\isacommand{by}\ (erule\ notE)
@@ -664,7 +664,7 @@
\isa{by} command.
Now when Isabelle selects the first assumption, it tries to prove \isa{P\
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the
-assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That
+assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That
concludes the proof.
\medskip
@@ -691,7 +691,8 @@
\end{isabelle}
Next we apply the {\isa{elim}} method, which repeatedly applies
elimination rules; here, the elimination rules given
-in the command. One of the subgoals is trivial, leaving us with one other:
+in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
+leaving us with one other:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
\end{isabelle}
@@ -704,8 +705,7 @@
is robust: the \isa{conjI} forces the \isa{erule} to select a
conjunction. The two subgoals are the ones we would expect from applying
conjunction introduction to
-\isa{Q\
-\isasymand\ R}:
+\isa{Q~\isasymand~R}:
\begin{isabelle}
\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
Q\isanewline
@@ -926,10 +926,12 @@
\end{isabelle}
If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
P(x)$ is also true. It is a dual of the universal elimination rule, and
-logic texts present it using the same notation for substitution. The existential
+logic texts present it using the same notation for substitution.
+
+The existential
elimination rule looks like this
in a logic text:
-\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
+\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
%
It looks like this in Isabelle:
\begin{isabelle}
@@ -953,17 +955,18 @@
\section{Hilbert's Epsilon-Operator}
+\label{sec:SOME}
-Isabelle/HOL provides Hilbert's
-$\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
+HOL provides Hilbert's
+$\varepsilon$-operator. The term $\varepsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
true, provided such a value exists. Using this operator, we can express an
existential destruction rule:
-\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
+\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
This rule is seldom used, for it can cause exponential blow-up.
\subsection{Definite Descriptions}
-In ASCII, we write \isa{SOME} for $\epsilon$.
+In ASCII, we write \isa{SOME} for $\varepsilon$.
\REMARK{the internal constant is \isa{Eps}}
The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
description}: when \isa{P} is satisfied by a unique value,~\isa{a}.
@@ -979,7 +982,7 @@
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
description) and proceed to prove other facts.
-Here is an example. HOL defines \isa{inv},\indexbold{*inv (constant)}
+Here is another example. Isabelle/HOL defines \isa{inv},\indexbold{*inv (constant)}
which expresses inverses of functions, as a definite
description:
\begin{isabelle}
@@ -1025,7 +1028,6 @@
\ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
\end{isabelle}
-
As always with \isa{some_equality}, we must show existence and
uniqueness of the claimed solution,~\isa{k}. Existence, the first
subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry:
@@ -1063,6 +1065,7 @@
\ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
\isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
\isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
+
\ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
\isasymLongrightarrow \ P\ x\ (?f\ x)
\end{isabelle}
@@ -1072,6 +1075,7 @@
\begin{isabelle}
\isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
+
\ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
\end{isabelle}
@@ -1141,7 +1145,8 @@
\begin{isabelle}
*** empty result sequence -- proof command failed
\end{isabelle}
-We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
+If we interact with Isabelle via the shell interface,
+we abandon a failed proof with the \isacommand{oops} command.
\medskip
@@ -1301,7 +1306,7 @@
\begin{isabelle}
\isacommand{lemma}\
[iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
-(xs=[]\ \isacharampersand\ ys=[])"\isanewline
+(xs=[]\ \isasymand\ ys=[])"\isanewline
\isacommand{apply}\ (induct_tac\ xs)\isanewline
\isacommand{apply}\ (simp_all)\isanewline
\isacommand{done}
@@ -1314,7 +1319,7 @@
(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
\end{isabelle}
A product is zero if and only if one of the factors is zero. The
-reasoning involves a logical \textsc{or}. Proving new rules for
+reasoning involves a disjunction. Proving new rules for
disjunctive reasoning is hard, but translating to an actual disjunction
works: the classical reasoner handles disjunction properly.
@@ -1490,8 +1495,8 @@
We state it with the \isa{iff} attribute so that
Isabelle can use it to remove some occurrences of \isa{gcd}.
The theorem has a one-line
-proof using \isa{blast} supplied with four introduction
-rules: note the {\isa{intro}} attribute. The exclamation mark
+proof using \isa{blast} supplied with two additional introduction
+rules. The exclamation mark
({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
applied aggressively. Rules given without the exclamation mark
are applied reluctantly and their uses can be undone if
@@ -1519,8 +1524,8 @@
Of the latter methods, the most useful is {\isa{clarify}}. It performs
all obvious reasoning steps without splitting the goal into multiple
-parts. It does not apply rules that could render the
-goal unprovable (so-called unsafe rules). By performing the obvious
+parts. It does not apply unsafe rules that could render the
+goal unprovable. By performing the obvious
steps, {\isa{clarify}} lays bare the difficult parts of the problem,
where human intervention is necessary.
@@ -1568,7 +1573,7 @@
That makes them slower but enables them to work correctly in the
presence of the more unusual features of Isabelle rules, such
as type classes and function unknowns. For example, recall the introduction rule
-for Hilbert's epsilon-operator:
+for Hilbert's $\varepsilon$-operator:
\begin{isabelle}
?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
\rulename{someI}
@@ -1796,7 +1801,7 @@
instance of a rule by specifying facts for its premises. Let us try
it with this rule:
\begin{isabelle}
-\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
+\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
\isasymLongrightarrow\ ?k\ dvd\ ?m
\rulename{relprime_dvd_mult}
\end{isabelle}
@@ -1809,7 +1814,7 @@
We have evaluated an application of the \isa{gcd} function by
simplification. Expression evaluation is not guaranteed to terminate, and
certainly is not efficient; Isabelle performs arithmetic operations by
-rewriting symbolic bit strings. Here, however, the simplification takes
+rewriting symbolic bit strings. Here, however, the simplification above takes
less than one second. We can specify this new lemma to \isa{OF},
generating an instance of \isa{relprime_dvd_mult}. The expression
\begin{isabelle}
@@ -1826,7 +1831,7 @@
\isasymlbrakk?k\ dvd\ ?m;\
?k\ dvd\ ?n\isasymrbrakk\
\isasymLongrightarrow\ ?k\ dvd\
-(?m\ +\ ?n)
+?m\ +\ ?n
\rulename{dvd_add}\isanewline
?m\ dvd\ ?m%
\rulename{dvd_refl}
@@ -1846,7 +1851,7 @@
\end{isabelle}
The result is
\begin{isabelle}
-\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
+\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
\end{isabelle}
You may have noticed that \isa{THEN} and \isa{OF} are based on
@@ -1933,7 +1938,7 @@
\begin{isabelle}
\isacommand{lemma}\
relprime_dvd_mult:\isanewline
-\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\
+\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
\isasymrbrakk\
\isasymLongrightarrow\ k\ dvd\
m"\isanewline
@@ -1943,11 +1948,7 @@
In the resulting subgoal, note how the equation has been
inserted:
\begin{isabelle}
-\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
-dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
-m\isanewline
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
-\ \ \ \ \ m\ *\ gcd\
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
(k,\ n)\
=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
@@ -1956,12 +1957,8 @@
utilizes the assumption \isa{gcd(k,n)\ =\
1}. Here is the result:
\begin{isabelle}
-\isasymlbrakk gcd\ (k,\
-n)\ =\ 1;\ k\
-dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
-m\isanewline
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
-\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
+\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
\end{isabelle}
Simplification has yielded an equation for \isa{m} that will be used to
@@ -2042,8 +2039,7 @@
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
\end{isabelle}
-
-The first subgoal is trivial, but for the second Isabelle needs help to eliminate
+The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
the case
\isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
subgoals:
@@ -2056,8 +2052,8 @@
\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
\end{isabelle}
-Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
-the method {\isa{arith}}. For the second subgoal we apply the method \isa{force},
+Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
+(\isa{arith}). For the second subgoal we apply the method \isa{force},
which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
--- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Wed Jan 24 12:29:10 2001 +0100
@@ -28,6 +28,7 @@
\isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
and not as @{text"(x # y) # z"}.
+The @{text 65} is the priority of the infix @{text"#"}.
\begin{warn}
Syntax annotations are a powerful but optional feature. You
@@ -44,9 +45,10 @@
text{*
\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
+In contrast to many functional programming languages,
+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
@{text"app"} is annotated with concrete syntax too. Instead of the
prefix syntax @{text"app xs ys"} the infix
@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
@@ -89,11 +91,11 @@
\end{warn}
A remark about syntax. The textual definition of a theory follows a fixed
-syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
-Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
+syntax with keywords like \isacommand{datatype} and \isacommand{end}.
+% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
Embedded in this syntax are the types and formulae of HOL, whose syntax is
-extensible, e.g.\ by new user-defined infix operators
-(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
+extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
+To distinguish the two levels, everything
HOL-specific (terms and types) should be enclosed in
\texttt{"}\dots\texttt{"}.
To lessen this burden, quotation marks around a single identifier can be
@@ -179,10 +181,7 @@
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (@{term[source]Nil}) and the induction step
(@{term[source]Cons}):
-\begin{isabelle}
-~1.~rev~(rev~[])~=~[]\isanewline
-~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
The induction step is an example of the general format of a subgoal:
\begin{isabelle}
@@ -211,9 +210,7 @@
``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
to the equation @{prop"rev [] = []"}) and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
-\begin{isabelle}
-~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
-\end{isabelle}
+@{subgoals[display,indent=0,margin=70]}
In order to simplify this subgoal further, a lemma suggests itself.
*}
(*<*)
@@ -231,10 +228,10 @@
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
-\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
-the importance we attach to a proposition. We use the words
+\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
+the importance we attach to a proposition. Therefore we use the words
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
-interchangeably.
+interchangeably, too.
There are two variables that we could induct on: @{term"xs"} and
@{term"ys"}. Because @{text"@"} is defined by recursion on
@@ -285,8 +282,8 @@
% Instead of \isacommand{apply} followed by a dot, you can simply write
% \isacommand{by}\indexbold{by}, which we do most of the time.
-Notice that in lemma @{thm[source]app_Nil2}
-(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
+Notice that in lemma @{thm[source]app_Nil2},
+as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
replaced by the unknown @{text"?xs"}, just as explained in
\S\ref{sec:variables}.
@@ -326,7 +323,7 @@
text{*
\noindent
succeeds without further ado.
-Now we can go back and prove the first lemma
+Now we can prove the first lemma
*}
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 12:29:10 2001 +0100
@@ -30,6 +30,7 @@
\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
+The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
\begin{warn}
Syntax annotations are a powerful but optional feature. You
@@ -44,9 +45,10 @@
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
\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
+In contrast to many functional programming languages,
+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\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
@@ -87,11 +89,11 @@
\end{warn}
A remark about syntax. The textual definition of a theory follows a fixed
-syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
-Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
+syntax with keywords like \isacommand{datatype} and \isacommand{end}.
+% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
Embedded in this syntax are the types and formulae of HOL, whose syntax is
-extensible, e.g.\ by new user-defined infix operators
-(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
+extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
+To distinguish the two levels, everything
HOL-specific (terms and types) should be enclosed in
\texttt{"}\dots\texttt{"}.
To lessen this burden, quotation marks around a single identifier can be
@@ -174,9 +176,10 @@
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (\isa{Nil}) and the induction step
(\isa{Cons}):
-\begin{isabelle}
-~1.~rev~(rev~[])~=~[]\isanewline
-~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
\end{isabelle}
The induction step is an example of the general format of a subgoal:
@@ -204,8 +207,9 @@
``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
-\begin{isabelle}
-~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
\end{isabelle}
In order to simplify this subgoal further, a lemma suggests itself.%
\end{isamarkuptxt}%
@@ -221,10 +225,10 @@
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent The keywords \isacommand{theorem}\index{*theorem} and
-\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
-the importance we attach to a proposition. We use the words
+\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
+the importance we attach to a proposition. Therefore we use the words
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
-interchangeably.
+interchangeably, too.
There are two variables that we could induct on: \isa{xs} and
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
@@ -272,8 +276,8 @@
% Instead of \isacommand{apply} followed by a dot, you can simply write
% \isacommand{by}\indexbold{by}, which we do most of the time.
-Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
-(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
+Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
+as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
\S\ref{sec:variables}.
@@ -313,7 +317,7 @@
\begin{isamarkuptext}%
\noindent
succeeds without further ado.
-Now we can go back and prove the first lemma%
+Now we can prove the first lemma%
\end{isamarkuptext}%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 12:29:10 2001 +0100
@@ -130,7 +130,7 @@
This proof may look surprisingly straightforward. However, note that this
comes at a cost: the proof script is unreadable because the intermediate
proof states are invisible, and we rely on the (possibly brittle) magic of
-@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
+@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on @{term bs} makes
sense and solves the proof. Part~\ref{Isar} shows you how to write readable
and stable proofs.
--- a/doc-src/TutorialI/Trie/document/Trie.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Jan 24 12:29:10 2001 +0100
@@ -120,7 +120,7 @@
This proof may look surprisingly straightforward. However, note that this
comes at a cost: the proof script is unreadable because the intermediate
proof states are invisible, and we rely on the (possibly brittle) magic of
-\isa{auto} (\isa{simp{\isacharunderscore}all} will not do---try it) to split the subgoals
+\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on \isa{bs} makes
sense and solves the proof. Part~\ref{Isar} shows you how to write readable
and stable proofs.%
--- a/doc-src/TutorialI/Types/Overloading2.thy Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy Wed Jan 24 12:29:10 2001 +0100
@@ -23,7 +23,7 @@
text{*
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading}. They are
-defined on all numeric types and somtimes on other types as well, for example
+defined on all numeric types and sometimes on other types as well, for example
@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
\begin{table}[htbp]
@@ -34,9 +34,13 @@
@{term 0} & @{text "'a::zero"} \\
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
+@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
+@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
+@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
+@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
+@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jan 24 12:29:10 2001 +0100
@@ -25,7 +25,7 @@
\begin{isamarkuptext}%
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading}. They are
-defined on all numeric types and somtimes on other types as well, for example
+defined on all numeric types and sometimes on other types as well, for example
\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
\begin{table}[htbp]
@@ -36,9 +36,13 @@
\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
+\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
+\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
+\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
+\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
+\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
-\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
--- a/doc-src/TutorialI/basics.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Wed Jan 24 12:29:10 2001 +0100
@@ -2,7 +2,7 @@
\section{Introduction}
-This is a tutorial on how to use Isabelle/HOL as a specification and
+This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and
verification system. Isabelle is a generic system for implementing logical
formalisms, and Isabelle/HOL is the specialization of Isabelle for
HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
@@ -15,13 +15,12 @@
misled: HOL can express most mathematical concepts, and functional
programming is just one particularly simple and ubiquitous instance.
-This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
-which is an extension of Isabelle~\cite{paulson-isa-book} with structured
-proofs.\footnote{Thus the full name of the system should be
- Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
-difference to classical Isabelle (which is the basis of another version of
-this tutorial) is the replacement of the ML level by a dedicated language for
-definitions and proofs.
+Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
+This has influenced some of HOL's concrete syntax but is otherwise
+irrelevant for us because this tutorial is based on
+Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle
+with structured proofs.\footnote{Thus the full name of the system should be
+ Isabelle/Isar/HOL, but that is a bit of a mouthful.}
A tutorial is by definition incomplete. Currently the tutorial only
introduces the rudiments of Isar's proof language. To fully exploit the power
@@ -74,7 +73,7 @@
HOL contains a theory \isaindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.
Unless you know what you are doing, always include \isa{Main}
- as a direct or indirect parent theory of all your theories.
+ as a direct or indirect parent of all your theories.
\end{warn}
@@ -122,7 +121,8 @@
\end{ttbox}
\noindent
-This can be reversed by \texttt{ML "reset show_types"}. Various other flags
+This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
+which we introduce as we go along,
can be set and reset in the same manner.\indexbold{flag!(re)setting}
\end{warn}
@@ -196,7 +196,7 @@
should be familiar with to avoid certain syntactic traps. A particular
problem for novices can be the priority of operators. If you are unsure, use
additional parentheses. In those cases where Isabelle echoes your
-input, you can see which parentheses are dropped---they were superfluous. If
+input, you can see which parentheses are dropped --- they were superfluous. If
you are unsure how to interpret Isabelle's output because you don't know
where the (dropped) parentheses go, set the \rmindex{flag}
\isaindexbold{show_brackets}:
@@ -222,7 +222,7 @@
\item
Constructs with an opening but without a closing delimiter bind very weakly
and should therefore be enclosed in parentheses if they appear in subterms, as
-in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
+in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
\item
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
--- a/doc-src/TutorialI/fp.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Wed Jan 24 12:29:10 2001 +0100
@@ -122,11 +122,11 @@
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
+ current theory, you must first abandon your current theory\indexbold{abandon
theory}\indexbold{theory!abandon} (at the shell
level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
- been modified you go back to your original theory. When its first line
- \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
+ been modified, you go back to your original theory. When its first line
+ \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
modified parent is reloaded automatically.
The only time when you need to load a theory by hand is when you simply
@@ -291,12 +291,12 @@
\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.
+method that \isa{auto} always applies first, 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
purpose of this section is introduce the many features of the simplifier.
-Anybody intending to use HOL should read this section. Later on
+Anybody intending to perform proofs in HOL should read this section. Later on
({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
little bit of how the simplifier works. The serious student should read that
section as well, in particular in order to understand what happened if things
@@ -359,7 +359,7 @@
This declaration is a real can of worms.
In HOL it must be ruled out because it requires a type
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
-same cardinality---an impossibility. For the same reason it is not possible
+same cardinality --- an impossibility. For the same reason it is not possible
to allow recursion involving the type \isa{set}, which is isomorphic to
\isa{t \isasymFun\ bool}.
@@ -380,7 +380,7 @@
\end{isabelle}
do indeed make sense. Note the different arrow,
\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
-expressing the type of \textbf{continuous} functions.
+expressing the type of \emph{continuous} functions.
There is even a version of LCF on top of HOL,
called HOLCF~\cite{MuellerNvOS99}.
--- a/doc-src/TutorialI/todo.tobias Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Wed Jan 24 12:29:10 2001 +0100
@@ -89,10 +89,10 @@
==================
Exercises
-%\begin{exercise}
-%Extend expressions by conditional expressions.
-braucht wfrec!
-%\end{exercise}
+
+For extensionality (in Sets chapter): prove
+valif o norm = valif
+in If-expression case study (Ifexpr)
Nested inductive datatypes: another example/exercise:
size(t) <= size(subst s t)?
--- a/doc-src/TutorialI/tutorial.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/tutorial.tex Wed Jan 24 12:29:10 2001 +0100
@@ -75,9 +75,9 @@
\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
-feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
+feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
-and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
+and Markus Wenzel. Stephan Merz was also kind enough to
read and comment on a draft version.
\clearfirst
@@ -91,7 +91,7 @@
\chapter{Theory Presentation}
\chapter{Case Study: Verifying a Cryptographic Protocol}
\chapter{Structured Proofs}
-\chapter{Case Study: UNIX File-System Security}
+%\chapter{Case Study: UNIX File-System Security}
%\chapter{The Tricks of the Trade}
\input{appendix}