*** empty log message ***
authornipkow
Wed Jan 24 12:29:10 2001 +0100 (2001-01-24)
changeset 109716852682eaf16
parent 10970 7917e66505a4
child 10972 af160f8d3bd7
*** empty log message ***
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/CTLind.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/CodeGen/CodeGen.thy
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Datatype/ABexpr.thy
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Datatype/document/unfoldnested.tex
doc-src/TutorialI/Datatype/unfoldnested.thy
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Misc/Itrev.thy
doc-src/TutorialI/Misc/document/Itrev.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Recdef/Induction.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/Types/Overloading2.thy
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*<*)theory CTL = Base:;(*>*)
     1.5  
     1.6 -subsection{*Computation Tree Logic---CTL*};
     1.7 +subsection{*Computation Tree Logic --- CTL*};
     1.8  
     1.9  text{*\label{sec:CTL}
    1.10  The semantics of PDL only needs reflexive transitive closure.
     2.1 --- a/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 24 11:59:15 2001 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 24 12:29:10 2001 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  
     2.5  text{*
     2.6  The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
     2.7 -that the assumption is left unchanged---otherwise the @{text"\<forall>p"} is turned
     2.8 +that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
     2.9  into a @{text"\<And>p"}, which would complicate matters below. As it is,
    2.10  @{thm[source]Avoid_in_lfp} is now
    2.11  @{thm[display]Avoid_in_lfp[no_vars]}
     3.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Wed Jan 24 11:59:15 2001 +0100
     3.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Wed Jan 24 12:29:10 2001 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (*<*)theory PDL = Base:(*>*)
     3.5  
     3.6 -subsection{*Propositional Dynamic Logic---PDL*}
     3.7 +subsection{*Propositional Dynamic Logic --- PDL*}
     3.8  
     3.9  text{*\index{PDL|(}
    3.10  The formulae of PDL are built up from atomic propositions via the customary
    3.11 @@ -68,7 +68,7 @@
    3.12  fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
    3.13  @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
    3.14  find it hard to see that @{term"mc(EF f)"} contains exactly those states from
    3.15 -which there is a path to a state where @{term f} is true, do not worry---that
    3.16 +which there is a path to a state where @{term f} is true, do not worry --- that
    3.17  will be proved in a moment.
    3.18  
    3.19  First we prove monotonicity of the function inside @{term lfp}
     4.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Jan 24 11:59:15 2001 +0100
     4.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Jan 24 12:29:10 2001 +0100
     4.3 @@ -2,7 +2,7 @@
     4.4  \begin{isabellebody}%
     4.5  \def\isabellecontext{CTL}%
     4.6  %
     4.7 -\isamarkupsubsection{Computation Tree Logic---CTL%
     4.8 +\isamarkupsubsection{Computation Tree Logic --- CTL%
     4.9  }
    4.10  %
    4.11  \begin{isamarkuptext}%
     5.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 24 11:59:15 2001 +0100
     5.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 24 12:29:10 2001 +0100
     5.3 @@ -128,7 +128,7 @@
     5.4  \isacommand{done}%
     5.5  \begin{isamarkuptext}%
     5.6  The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
     5.7 -that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
     5.8 +that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
     5.9  into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
    5.10  \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
    5.11  \begin{isabelle}%
     6.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 24 11:59:15 2001 +0100
     6.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 24 12:29:10 2001 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4  \begin{isabellebody}%
     6.5  \def\isabellecontext{PDL}%
     6.6  %
     6.7 -\isamarkupsubsection{Propositional Dynamic Logic---PDL%
     6.8 +\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
     6.9  }
    6.10  %
    6.11  \begin{isamarkuptext}%
    6.12 @@ -68,7 +68,7 @@
    6.13  fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
    6.14  \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
    6.15  find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
    6.16 -which there is a path to a state where \isa{f} is true, do not worry---that
    6.17 +which there is a path to a state where \isa{f} is true, do not worry --- that
    6.18  will be proved in a moment.
    6.19  
    6.20  First we prove monotonicity of the function inside \isa{lfp}
     7.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Wed Jan 24 11:59:15 2001 +0100
     7.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Wed Jan 24 12:29:10 2001 +0100
     7.3 @@ -49,7 +49,7 @@
     7.4  @{text"exec"} that takes a list of instructions, a store (modelled as a
     7.5  function from addresses to values, just like the environment for
     7.6  evaluating expressions), and a stack (modelled as a list) of values,
     7.7 -and returns the stack at the end of the execution---the store remains
     7.8 +and returns the stack at the end of the execution --- the store remains
     7.9  unchanged:
    7.10  *}
    7.11  
    7.12 @@ -110,15 +110,15 @@
    7.13  apply(induct_tac xs, simp, simp split: instr.split);
    7.14  (*<*)done(*>*)
    7.15  text{*\noindent
    7.16 -Note that because \isaindex{auto} performs simplification, it can
    7.17 -also be modified in the same way @{text simp} can. Thus the proof can be
    7.18 +Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
    7.19 +be modified in the same way @{text simp} can. Thus the proof can be
    7.20  rewritten as
    7.21  *}
    7.22  (*<*)
    7.23  declare exec_app[simp del];
    7.24  lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    7.25  (*>*)
    7.26 -apply(induct_tac xs, auto split: instr.split);
    7.27 +apply(induct_tac xs, simp_all split: instr.split);
    7.28  (*<*)done(*>*)
    7.29  text{*\noindent
    7.30  Although this is more compact, it is less clear for the reader of the proof.
     8.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 24 11:59:15 2001 +0100
     8.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 24 12:29:10 2001 +0100
     8.3 @@ -46,7 +46,7 @@
     8.4  \isa{exec} that takes a list of instructions, a store (modelled as a
     8.5  function from addresses to values, just like the environment for
     8.6  evaluating expressions), and a stack (modelled as a list) of values,
     8.7 -and returns the stack at the end of the execution---the store remains
     8.8 +and returns the stack at the end of the execution --- the store remains
     8.9  unchanged:%
    8.10  \end{isamarkuptext}%
    8.11  \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
    8.12 @@ -102,11 +102,11 @@
    8.13  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    8.14  \begin{isamarkuptext}%
    8.15  \noindent
    8.16 -Note that because \isaindex{auto} performs simplification, it can
    8.17 -also be modified in the same way \isa{simp} can. Thus the proof can be
    8.18 +Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
    8.19 +be modified in the same way \isa{simp} can. Thus the proof can be
    8.20  rewritten as%
    8.21  \end{isamarkuptext}%
    8.22 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    8.23 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    8.24  \begin{isamarkuptext}%
    8.25  \noindent
    8.26  Although this is more compact, it is less clear for the reader of the proof.
     9.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Jan 24 11:59:15 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Jan 24 12:29:10 2001 +0100
     9.3 @@ -28,13 +28,13 @@
     9.4  text{*\noindent
     9.5  Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
     9.6  except that we have fixed the values to be of type @{typ"nat"} and that we
     9.7 -have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean
     9.8 +have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
     9.9  expressions can be arithmetic comparisons, conjunctions and negations.
    9.10  The semantics is fixed via two evaluation functions
    9.11  *}
    9.12  
    9.13 -consts  evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
    9.14 -        evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
    9.15 +consts  evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
    9.16 +        evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
    9.17  
    9.18  text{*\noindent
    9.19  that take an expression and an environment (a mapping from variables @{typ"'a"} to values
    9.20 @@ -53,15 +53,15 @@
    9.21    "evala (Num n) env = n"
    9.22  
    9.23    "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
    9.24 -  "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
    9.25 -  "evalb (Neg b) env = (\\<not> evalb b env)"
    9.26 +  "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
    9.27 +  "evalb (Neg b) env = (\<not> evalb b env)"
    9.28  
    9.29  text{*\noindent
    9.30  In the same fashion we also define two functions that perform substitution:
    9.31  *}
    9.32  
    9.33 -consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
    9.34 -       substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
    9.35 +consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
    9.36 +       substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
    9.37  
    9.38  text{*\noindent
    9.39  The first argument is a function mapping variables to expressions, the
    9.40 @@ -93,8 +93,8 @@
    9.41  theorems simultaneously:
    9.42  *}
    9.43  
    9.44 -lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
    9.45 -        evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
    9.46 +lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
    9.47 +        evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
    9.48  apply(induct_tac a and b);
    9.49  
    9.50  txt{*\noindent
    9.51 @@ -110,7 +110,7 @@
    9.52  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    9.53  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    9.54  \begin{isabelle}
    9.55 -\isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"}
    9.56 +\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
    9.57  \end{isabelle}
    9.58  
    9.59  \begin{exercise}
    10.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Wed Jan 24 11:59:15 2001 +0100
    10.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Wed Jan 24 12:29:10 2001 +0100
    10.3 @@ -9,12 +9,12 @@
    10.4  where function symbols can be applied to a list of arguments:
    10.5  *}
    10.6  (*<*)hide const Var(*>*)
    10.7 -datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
    10.8 +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
    10.9  
   10.10  text{*\noindent
   10.11  Note that we need to quote @{text term} on the left to avoid confusion with
   10.12  the Isabelle command \isacommand{term}.
   10.13 -Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
   10.14 +Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of
   10.15  function symbols.
   10.16  A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
   10.17    [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
   10.18 @@ -41,8 +41,8 @@
   10.19  *}
   10.20  
   10.21  consts
   10.22 -subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term      \<Rightarrow> ('a,'b)term"
   10.23 -substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list";
   10.24 +subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term      \<Rightarrow> ('v,'f)term"
   10.25 +substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
   10.26  
   10.27  primrec
   10.28    "subst s (Var x) = s x"
   10.29 @@ -62,8 +62,8 @@
   10.30  strengthened and proved as follows:
   10.31  *}
   10.32  
   10.33 -lemma "subst  Var t  = (t ::('a,'b)term)  \<and>
   10.34 -        substs Var ts = (ts::('a,'b)term list)";
   10.35 +lemma "subst  Var t  = (t ::('v,'f)term)  \<and>
   10.36 +        substs Var ts = (ts::('v,'f)term list)";
   10.37  apply(induct_tac t and ts, simp_all);
   10.38  done
   10.39  
   10.40 @@ -72,7 +72,7 @@
   10.41  leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
   10.42  that the type annotations are necessary because otherwise there is nothing in
   10.43  the goal to enforce that both halves of the goal talk about the same type
   10.44 -parameters @{text"('a,'b)"}. As a result, induction would fail
   10.45 +parameters @{text"('v,'f)"}. As a result, induction would fail
   10.46  because the two halves of the goal would be unrelated.
   10.47  
   10.48  \begin{exercise}
   10.49 @@ -84,7 +84,7 @@
   10.50  its definition is found in theorem @{thm[source]o_def}).
   10.51  \end{exercise}
   10.52  \begin{exercise}\label{ex:trev-trev}
   10.53 -  Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}
   10.54 +  Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"}
   10.55  that recursively reverses the order of arguments of all function symbols in a
   10.56    term. Prove that @{prop"trev(trev t) = t"}.
   10.57  \end{exercise}
   10.58 @@ -120,7 +120,7 @@
   10.59  and to define functions with \isacommand{recdef} instead.
   10.60  The details are explained in \S\ref{sec:nested-recdef} below.
   10.61  
   10.62 -Of course, you may also combine mutual and nested recursion. For example,
   10.63 +Of course, you may also combine mutual and nested recursion of datatypes. For example,
   10.64  constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
   10.65  expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
   10.66  *}
    11.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 24 11:59:15 2001 +0100
    11.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 24 12:29:10 2001 +0100
    11.3 @@ -27,7 +27,7 @@
    11.4  \noindent
    11.5  Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
    11.6  except that we have fixed the values to be of type \isa{nat} and that we
    11.7 -have fixed the two binary operations \isa{aexp{\isachardot}Sum} and \isa{Diff}. Boolean
    11.8 +have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
    11.9  expressions can be arithmetic comparisons, conjunctions and negations.
   11.10  The semantics is fixed via two evaluation functions%
   11.11  \end{isamarkuptext}%
   11.12 @@ -100,7 +100,7 @@
   11.13  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
   11.14  where each variable $x@i$ is of type $\tau@i$. Induction is started by
   11.15  \begin{isabelle}
   11.16 -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isa{and} \dots\ \isa{and} $x@n$\isa{{\isacharparenright}}
   11.17 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
   11.18  \end{isabelle}
   11.19  
   11.20  \begin{exercise}
    12.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Jan 24 11:59:15 2001 +0100
    12.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Jan 24 12:29:10 2001 +0100
    12.3 @@ -8,12 +8,12 @@
    12.4  constructor. This is not the case any longer for the following model of terms
    12.5  where function symbols can be applied to a list of arguments:%
    12.6  \end{isamarkuptext}%
    12.7 -\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}%
    12.8 +\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}%
    12.9  \begin{isamarkuptext}%
   12.10  \noindent
   12.11  Note that we need to quote \isa{term} on the left to avoid confusion with
   12.12  the Isabelle command \isacommand{term}.
   12.13 -Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
   12.14 +Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of
   12.15  function symbols.
   12.16  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
   12.17  suitable values, e.g.\ numbers or strings.
   12.18 @@ -38,8 +38,8 @@
   12.19  lists, we need to define two substitution functions simultaneously:%
   12.20  \end{isamarkuptext}%
   12.21  \isacommand{consts}\isanewline
   12.22 -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
   12.23 -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
   12.24 +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
   12.25 +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
   12.26  \isanewline
   12.27  \isacommand{primrec}\isanewline
   12.28  \ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline
   12.29 @@ -58,8 +58,8 @@
   12.30  the fact that the identity substitution does not change a term needs to be
   12.31  strengthened and proved as follows:%
   12.32  \end{isamarkuptext}%
   12.33 -\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
   12.34 -\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
   12.35 +\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
   12.36 +\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
   12.37  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
   12.38  \isacommand{done}%
   12.39  \begin{isamarkuptext}%
   12.40 @@ -68,7 +68,7 @@
   12.41  leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
   12.42  that the type annotations are necessary because otherwise there is nothing in
   12.43  the goal to enforce that both halves of the goal talk about the same type
   12.44 -parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
   12.45 +parameters \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}}. As a result, induction would fail
   12.46  because the two halves of the goal would be unrelated.
   12.47  
   12.48  \begin{exercise}
   12.49 @@ -82,7 +82,7 @@
   12.50  its definition is found in theorem \isa{o{\isacharunderscore}def}).
   12.51  \end{exercise}
   12.52  \begin{exercise}\label{ex:trev-trev}
   12.53 -  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}
   12.54 +  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}
   12.55  that recursively reverses the order of arguments of all function symbols in a
   12.56    term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
   12.57  \end{exercise}
   12.58 @@ -118,7 +118,7 @@
   12.59  and to define functions with \isacommand{recdef} instead.
   12.60  The details are explained in \S\ref{sec:nested-recdef} below.
   12.61  
   12.62 -Of course, you may also combine mutual and nested recursion. For example,
   12.63 +Of course, you may also combine mutual and nested recursion of datatypes. For example,
   12.64  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
   12.65  expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
   12.66  \end{isamarkuptext}%
    13.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Wed Jan 24 11:59:15 2001 +0100
    13.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Wed Jan 24 12:29:10 2001 +0100
    13.3 @@ -1,8 +1,8 @@
    13.4  %
    13.5  \begin{isabellebody}%
    13.6  \def\isabellecontext{unfoldnested}%
    13.7 -\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
    13.8 -\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}%
    13.9 +\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
   13.10 +\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}%
   13.11  %%% Local Variables:
   13.12  %%% mode: latex
   13.13  %%% TeX-master: "root"
    14.1 --- a/doc-src/TutorialI/Datatype/unfoldnested.thy	Wed Jan 24 11:59:15 2001 +0100
    14.2 +++ b/doc-src/TutorialI/Datatype/unfoldnested.thy	Wed Jan 24 12:29:10 2001 +0100
    14.3 @@ -1,8 +1,8 @@
    14.4  (*<*)
    14.5  theory unfoldnested = Main:;
    14.6  (*>*)
    14.7 -datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
    14.8 -and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
    14.9 +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
   14.10 +and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
   14.11  (*<*)
   14.12  end
   14.13  (*>*)
    15.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Jan 24 11:59:15 2001 +0100
    15.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Jan 24 12:29:10 2001 +0100
    15.3 @@ -55,7 +55,7 @@
    15.4  datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
    15.5  
    15.6  text{*\noindent
    15.7 -The evaluation if If-expressions proceeds as for @{typ"boolex"}:
    15.8 +The evaluation of If-expressions proceeds as for @{typ"boolex"}:
    15.9  *}
   15.10  
   15.11  consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
    16.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jan 24 11:59:15 2001 +0100
    16.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jan 24 12:29:10 2001 +0100
    16.3 @@ -55,7 +55,7 @@
    16.4  \isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex%
    16.5  \begin{isamarkuptext}%
    16.6  \noindent
    16.7 -The evaluation if If-expressions proceeds as for \isa{boolex}:%
    16.8 +The evaluation of If-expressions proceeds as for \isa{boolex}:%
    16.9  \end{isamarkuptext}%
   16.10  \isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
   16.11  \isacommand{primrec}\isanewline
    17.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Wed Jan 24 11:59:15 2001 +0100
    17.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Jan 24 12:29:10 2001 +0100
    17.3 @@ -26,7 +26,7 @@
    17.4  The key heuristic, and the main point of this section, is to
    17.5  generalize the goal before induction. The reason is simple: if the goal is
    17.6  too specific, the induction hypothesis is too weak to allow the induction
    17.7 -step to go through. Let us now illustrate the idea with an example.
    17.8 +step to go through. Let us illustrate the idea with an example.
    17.9  
   17.10  Function @{term"rev"} has quadratic worst-case running time
   17.11  because it calls function @{text"@"} for each element of the list and
   17.12 @@ -61,7 +61,7 @@
   17.13  
   17.14  txt{*\noindent
   17.15  Unfortunately, this is not a complete success:
   17.16 -@{subgoals[display,indent=0,margin=65]}
   17.17 +@{subgoals[display,indent=0,margin=70]}
   17.18  Just as predicted above, the overall goal, and hence the induction
   17.19  hypothesis, is too weak to solve the induction step because of the fixed
   17.20  argument, @{term"[]"}.  This suggests a heuristic:
   17.21 @@ -69,7 +69,7 @@
   17.22  \emph{Generalize goals for induction by replacing constants by variables.}
   17.23  \end{quote}
   17.24  Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
   17.25 -just not true---the correct generalization is
   17.26 +just not true --- the correct generalization is
   17.27  *};
   17.28  (*<*)oops;(*>*)
   17.29  lemma "itrev xs ys = rev xs @ ys";
   17.30 @@ -112,13 +112,6 @@
   17.31  The variables that require generalization are typically those that 
   17.32  change in recursive calls.
   17.33  
   17.34 -In general, if you have tried the above heuristics and still find your
   17.35 -induction does not go through, and no obvious lemma suggests itself, you may
   17.36 -need to generalize your proposition even further. This requires insight into
   17.37 -the problem at hand and is beyond simple rules of thumb.  You
   17.38 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   17.39 -to learn about some advanced techniques for inductive proofs.
   17.40 -
   17.41  A final point worth mentioning is the orientation of the equation we just
   17.42  proved: the more complex notion (@{term itrev}) is on the left-hand
   17.43  side, the simpler one (@{term rev}) on the right-hand side. This constitutes
   17.44 @@ -130,6 +123,13 @@
   17.45  This heuristic is tricky to apply because it is not obvious that
   17.46  @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
   17.47  happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
   17.48 +
   17.49 +In general, if you have tried the above heuristics and still find your
   17.50 +induction does not go through, and no obvious lemma suggests itself, you may
   17.51 +need to generalize your proposition even further. This requires insight into
   17.52 +the problem at hand and is beyond simple rules of thumb.  You
   17.53 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   17.54 +to learn about some advanced techniques for inductive proofs.
   17.55  *}
   17.56  (*<*)
   17.57  end
    18.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 24 11:59:15 2001 +0100
    18.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 24 12:29:10 2001 +0100
    18.3 @@ -28,7 +28,7 @@
    18.4  The key heuristic, and the main point of this section, is to
    18.5  generalize the goal before induction. The reason is simple: if the goal is
    18.6  too specific, the induction hypothesis is too weak to allow the induction
    18.7 -step to go through. Let us now illustrate the idea with an example.
    18.8 +step to go through. Let us illustrate the idea with an example.
    18.9  
   18.10  Function \isa{rev} has quadratic worst-case running time
   18.11  because it calls function \isa{{\isacharat}} for each element of the list and
   18.12 @@ -62,8 +62,7 @@
   18.13  Unfortunately, this is not a complete success:
   18.14  \begin{isabelle}%
   18.15  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
   18.16 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
   18.17 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
   18.18 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
   18.19  \end{isabelle}
   18.20  Just as predicted above, the overall goal, and hence the induction
   18.21  hypothesis, is too weak to solve the induction step because of the fixed
   18.22 @@ -72,7 +71,7 @@
   18.23  \emph{Generalize goals for induction by replacing constants by variables.}
   18.24  \end{quote}
   18.25  Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
   18.26 -just not true---the correct generalization is%
   18.27 +just not true --- the correct generalization is%
   18.28  \end{isamarkuptxt}%
   18.29  \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
   18.30  \begin{isamarkuptxt}%
   18.31 @@ -114,13 +113,6 @@
   18.32  The variables that require generalization are typically those that 
   18.33  change in recursive calls.
   18.34  
   18.35 -In general, if you have tried the above heuristics and still find your
   18.36 -induction does not go through, and no obvious lemma suggests itself, you may
   18.37 -need to generalize your proposition even further. This requires insight into
   18.38 -the problem at hand and is beyond simple rules of thumb.  You
   18.39 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   18.40 -to learn about some advanced techniques for inductive proofs.
   18.41 -
   18.42  A final point worth mentioning is the orientation of the equation we just
   18.43  proved: the more complex notion (\isa{itrev}) is on the left-hand
   18.44  side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
   18.45 @@ -131,7 +123,14 @@
   18.46  \end{quote}
   18.47  This heuristic is tricky to apply because it is not obvious that
   18.48  \isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
   18.49 -happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
   18.50 +happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
   18.51 +
   18.52 +In general, if you have tried the above heuristics and still find your
   18.53 +induction does not go through, and no obvious lemma suggests itself, you may
   18.54 +need to generalize your proposition even further. This requires insight into
   18.55 +the problem at hand and is beyond simple rules of thumb.  You
   18.56 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   18.57 +to learn about some advanced techniques for inductive proofs.%
   18.58  \end{isamarkuptext}%
   18.59  \end{isabellebody}%
   18.60  %%% Local Variables:
    19.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jan 24 11:59:15 2001 +0100
    19.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jan 24 12:29:10 2001 +0100
    19.3 @@ -69,7 +69,8 @@
    19.4  For more complex goals, there is the special method \isaindexbold{arith}
    19.5  (which attacks the first subgoal). It proves arithmetic goals involving the
    19.6  usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
    19.7 -\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
    19.8 +\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
    19.9 +and the operations
   19.10  \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
   19.11  known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   19.12  For example,%
    20.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 24 11:59:15 2001 +0100
    20.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 24 12:29:10 2001 +0100
    20.3 @@ -52,7 +52,7 @@
    20.4  where the list of \emph{modifiers} fine tunes the behaviour and may
    20.5  be empty. Most if not all of the proofs seen so far could have been performed
    20.6  with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
    20.7 -only the first subgoal and may thus need to be repeated---use
    20.8 +only the first subgoal and may thus need to be repeated --- use
    20.9  \isaindex{simp_all} to simplify all subgoals.
   20.10  Note that \isa{simp} fails if nothing changes.%
   20.11  \end{isamarkuptext}%
   20.12 @@ -109,7 +109,7 @@
   20.13  \isacommand{done}%
   20.14  \begin{isamarkuptext}%
   20.15  \noindent
   20.16 -There are three options that influence the treatment of assumptions:
   20.17 +There are three modifiers that influence the treatment of assumptions:
   20.18  \begin{description}
   20.19  \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
   20.20   means that assumptions are completely ignored.
   20.21 @@ -122,7 +122,7 @@
   20.22  \end{description}
   20.23  Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
   20.24  the problematic subgoal above.
   20.25 -Note that only one of the options is allowed, and it must precede all
   20.26 +Note that only one of the modifiers is allowed, and it must precede all
   20.27  other arguments.%
   20.28  \end{isamarkuptext}%
   20.29  %
   20.30 @@ -169,13 +169,14 @@
   20.31  rule because this defeats the whole purpose of an abbreviation.
   20.32  
   20.33  \begin{warn}
   20.34 -  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
   20.35 -  occurrences of $f$ with at least two arguments. Thus it is safer to define
   20.36 -  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
   20.37 +  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
   20.38 +  occurrences of $f$ with at least two arguments. This may be helpful for unfolding
   20.39 +  $f$ selectively, but it may also get in the way. Defining
   20.40 +  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
   20.41  \end{warn}%
   20.42  \end{isamarkuptext}%
   20.43  %
   20.44 -\isamarkupsubsubsection{Simplifying Let-Expressions%
   20.45 +\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
   20.46  }
   20.47  %
   20.48  \begin{isamarkuptext}%
   20.49 @@ -360,7 +361,7 @@
   20.50  Applying instance of rewrite rule:
   20.51  rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
   20.52  Rewriting:
   20.53 -rev [x] == rev [] @ [x]
   20.54 +rev [a] == rev [] @ [a]
   20.55  Applying instance of rewrite rule:
   20.56  rev [] == []
   20.57  Rewriting:
   20.58 @@ -368,11 +369,11 @@
   20.59  Applying instance of rewrite rule:
   20.60  [] @ ?y == ?y
   20.61  Rewriting:
   20.62 -[] @ [x] == [x]
   20.63 +[] @ [a] == [a]
   20.64  Applying instance of rewrite rule:
   20.65  ?x3 \# ?t3 = ?t3 == False
   20.66  Rewriting:
   20.67 -[x] = [] == False
   20.68 +[a] = [] == False
   20.69  \end{ttbox}
   20.70  
   20.71  In more complicated cases, the trace can be quite lenghty, especially since
    21.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Jan 24 11:59:15 2001 +0100
    21.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Jan 24 12:29:10 2001 +0100
    21.3 @@ -69,7 +69,8 @@
    21.4  For more complex goals, there is the special method \isaindexbold{arith}
    21.5  (which attacks the first subgoal). It proves arithmetic goals involving the
    21.6  usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
    21.7 -@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
    21.8 +@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
    21.9 +and the operations
   21.10  @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
   21.11  known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   21.12  For example,
    22.1 --- a/doc-src/TutorialI/Misc/simp.thy	Wed Jan 24 11:59:15 2001 +0100
    22.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Wed Jan 24 12:29:10 2001 +0100
    22.3 @@ -49,7 +49,7 @@
    22.4  where the list of \emph{modifiers} fine tunes the behaviour and may
    22.5  be empty. Most if not all of the proofs seen so far could have been performed
    22.6  with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
    22.7 -only the first subgoal and may thus need to be repeated---use
    22.8 +only the first subgoal and may thus need to be repeated --- use
    22.9  \isaindex{simp_all} to simplify all subgoals.
   22.10  Note that @{text simp} fails if nothing changes.
   22.11  *}
   22.12 @@ -106,7 +106,7 @@
   22.13  done
   22.14  
   22.15  text{*\noindent
   22.16 -There are three options that influence the treatment of assumptions:
   22.17 +There are three modifiers that influence the treatment of assumptions:
   22.18  \begin{description}
   22.19  \item[@{text"(no_asm)"}]\indexbold{*no_asm}
   22.20   means that assumptions are completely ignored.
   22.21 @@ -119,7 +119,7 @@
   22.22  \end{description}
   22.23  Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
   22.24  the problematic subgoal above.
   22.25 -Note that only one of the options is allowed, and it must precede all
   22.26 +Note that only one of the modifiers is allowed, and it must precede all
   22.27  other arguments.
   22.28  *}
   22.29  
   22.30 @@ -165,13 +165,14 @@
   22.31  rule because this defeats the whole purpose of an abbreviation.
   22.32  
   22.33  \begin{warn}
   22.34 -  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
   22.35 -  occurrences of $f$ with at least two arguments. Thus it is safer to define
   22.36 -  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
   22.37 +  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
   22.38 +  occurrences of $f$ with at least two arguments. This may be helpful for unfolding
   22.39 +  $f$ selectively, but it may also get in the way. Defining
   22.40 +  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
   22.41  \end{warn}
   22.42  *}
   22.43  
   22.44 -subsubsection{*Simplifying Let-Expressions*}
   22.45 +subsubsection{*Simplifying {\tt\slshape let}-Expressions*}
   22.46  
   22.47  text{*\index{simplification!of let-expressions}
   22.48  Proving a goal containing \isaindex{let}-expressions almost invariably
   22.49 @@ -370,7 +371,7 @@
   22.50  Applying instance of rewrite rule:
   22.51  rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
   22.52  Rewriting:
   22.53 -rev [x] == rev [] @ [x]
   22.54 +rev [a] == rev [] @ [a]
   22.55  Applying instance of rewrite rule:
   22.56  rev [] == []
   22.57  Rewriting:
   22.58 @@ -378,11 +379,11 @@
   22.59  Applying instance of rewrite rule:
   22.60  [] @ ?y == ?y
   22.61  Rewriting:
   22.62 -[] @ [x] == [x]
   22.63 +[] @ [a] == [a]
   22.64  Applying instance of rewrite rule:
   22.65  ?x3 \# ?t3 = ?t3 == False
   22.66  Rewriting:
   22.67 -[x] = [] == False
   22.68 +[a] = [] == False
   22.69  \end{ttbox}
   22.70  
   22.71  In more complicated cases, the trace can be quite lenghty, especially since
    23.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Wed Jan 24 11:59:15 2001 +0100
    23.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Wed Jan 24 12:29:10 2001 +0100
    23.3 @@ -8,7 +8,7 @@
    23.4  equations) are simplification rules, we might like to prove something about
    23.5  our function. Since the function is recursive, the natural proof principle is
    23.6  again induction. But this time the structural form of induction that comes
    23.7 -with datatypes is unlikely to work well---otherwise we could have defined the
    23.8 +with datatypes is unlikely to work well --- otherwise we could have defined the
    23.9  function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
   23.10  proves a suitable induction rule $f$@{text".induct"} that follows the
   23.11  recursion pattern of the particular function $f$. We call this
   23.12 @@ -51,7 +51,7 @@
   23.13  \end{quote}\index{*induct_tac}%
   23.14  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
   23.15  name of a function that takes an $n$-tuple. Usually the subgoal will
   23.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
   23.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
   23.18  induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
   23.19  \begin{isabelle}
   23.20  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
    24.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Wed Jan 24 11:59:15 2001 +0100
    24.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Wed Jan 24 12:29:10 2001 +0100
    24.3 @@ -8,7 +8,7 @@
    24.4  equations) are simplification rules, we might like to prove something about
    24.5  our function. Since the function is recursive, the natural proof principle is
    24.6  again induction. But this time the structural form of induction that comes
    24.7 -with datatypes is unlikely to work well---otherwise we could have defined the
    24.8 +with datatypes is unlikely to work well --- otherwise we could have defined the
    24.9  function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
   24.10  proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
   24.11  recursion pattern of the particular function $f$. We call this
   24.12 @@ -53,7 +53,7 @@
   24.13  \end{quote}\index{*induct_tac}%
   24.14  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
   24.15  name of a function that takes an $n$-tuple. Usually the subgoal will
   24.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
   24.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
   24.18  induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
   24.19  \begin{isabelle}
   24.20  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
    25.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 24 11:59:15 2001 +0100
    25.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 24 12:29:10 2001 +0100
    25.3 @@ -30,7 +30,7 @@
    25.4  \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
    25.5  \begin{isamarkuptxt}%
    25.6  \noindent
    25.7 -It was not proved automatically because of the special nature of \isa{{\isacharminus}}
    25.8 +It was not proved automatically because of the special nature of subtraction
    25.9  on \isa{nat}. This requires more arithmetic than is tried by default:%
   25.10  \end{isamarkuptxt}%
   25.11  \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    26.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Wed Jan 24 11:59:15 2001 +0100
    26.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Jan 24 12:29:10 2001 +0100
    26.3 @@ -32,7 +32,7 @@
    26.4  lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
    26.5  
    26.6  txt{*\noindent
    26.7 -It was not proved automatically because of the special nature of @{text"-"}
    26.8 +It was not proved automatically because of the special nature of subtraction
    26.9  on @{typ"nat"}. This requires more arithmetic than is tried by default:
   26.10  *}
   26.11  
    27.1 --- a/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 11:59:15 2001 +0100
    27.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 12:29:10 2001 +0100
    27.3 @@ -71,7 +71,7 @@
    27.4  like this:
    27.5  \[  \infer{P\conj Q}{P & Q} \]
    27.6  The rule introduces the conjunction
    27.7 -symbol~($\conj$) in its conclusion.  Of course, in Isabelle proofs we
    27.8 +symbol~($\conj$) in its conclusion.  In Isabelle proofs we
    27.9  mainly  reason backwards.  When we apply this rule, the subgoal already has
   27.10  the form of a conjunction; the proof step makes this conjunction symbol
   27.11  disappear. 
   27.12 @@ -170,7 +170,7 @@
   27.13  \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
   27.14  \end{isabelle}
   27.15  When we use this sort of elimination rule backwards, it produces 
   27.16 -a case split.  (We have this before, in proofs by induction.)  The following  proof
   27.17 +a case split.  (We have seen this before, in proofs by induction.)  The following  proof
   27.18  illustrates the use of disjunction elimination.  
   27.19  \begin{isabelle}
   27.20  \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
   27.21 @@ -184,7 +184,7 @@
   27.22  We assume \isa{P\ \isasymor\ Q} and
   27.23  must prove \isa{Q\ \isasymor\ P}\@.  Our first step uses the disjunction
   27.24  elimination rule, \isa{disjE}.  The method {\isa{erule}}  applies an
   27.25 -elimination rule to the assumptions, searching for one that matches the
   27.26 +elimination rule, searching for an assumption that matches the
   27.27  rule's first premise.  Deleting that assumption, it
   27.28  return the subgoals for the remaining premises.  Most of the
   27.29  time, this is  the best way to use elimination rules; only rarely is there
   27.30 @@ -394,7 +394,7 @@
   27.31  As we have seen, Isabelle rules involve variables that begin  with a
   27.32  question mark. These are called \textbf{schematic} variables  and act as
   27.33  placeholders for terms. \textbf{Unification} refers to  the process of
   27.34 -making two terms identical, possibly by replacing  their variables by
   27.35 +making two terms identical, possibly by replacing their schematic variables by
   27.36  terms. The simplest case is when the two terms  are already the same. Next
   27.37  simplest is when the variables in only one of the term
   27.38   are replaced; this is called \textbf{pattern-matching}.  The
   27.39 @@ -440,7 +440,7 @@
   27.40  A typical substitution rule allows us to replace one term by 
   27.41  another if we know that two terms are equal. 
   27.42  \[ \infer{P[t/x]}{s=t & P[s/x]} \]
   27.43 -The conclusion uses a notation for substitution: $P[t/x]$ is the result of
   27.44 +The rule uses a notation for substitution: $P[t/x]$ is the result of
   27.45  replacing $x$ by~$t$ in~$P$.  The rule only substitutes in the positions
   27.46  designated by~$x$.  For example, it can
   27.47  derive symmetry of equality from reflexivity.  Using $x=s$ for~$P$
   27.48 @@ -566,7 +566,7 @@
   27.49  \isa{erule_tac} since above we used \isa{erule}.
   27.50  \begin{isabelle}
   27.51  \isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
   27.52 -\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ 
   27.53 +\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\ 
   27.54  \isakeyword{in}\ ssubst)
   27.55  \end{isabelle}
   27.56  %
   27.57 @@ -580,7 +580,7 @@
   27.58  An alternative to \isa{rule_tac} is to use \isa{rule} with the
   27.59  \isa{of} directive, described in \S\ref{sec:forward} below.   An
   27.60  advantage  of \isa{rule_tac} is that the instantiations may refer to 
   27.61 -variables bound in the current subgoal.
   27.62 +\isasymAnd-bound variables in the current subgoal.
   27.63  
   27.64  
   27.65  \section{Negation}
   27.66 @@ -632,7 +632,7 @@
   27.67  \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
   27.68  \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
   27.69  R"\isanewline
   27.70 -\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
   27.71 +\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
   27.72  contrapos_np)\isanewline
   27.73  \isacommand{apply}\ intro\isanewline
   27.74  \isacommand{by}\ (erule\ notE)
   27.75 @@ -664,7 +664,7 @@
   27.76  \isa{by} command.
   27.77  Now when Isabelle selects the first assumption, it tries to prove \isa{P\
   27.78  \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 
   27.79 -assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption.  That
   27.80 +assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption.  That
   27.81  concludes the proof.
   27.82  
   27.83  \medskip
   27.84 @@ -691,7 +691,8 @@
   27.85  \end{isabelle}
   27.86  Next we apply the {\isa{elim}} method, which repeatedly applies 
   27.87  elimination rules; here, the elimination rules given 
   27.88 -in the command.  One of the subgoals is trivial, leaving us with one other:
   27.89 +in the command.  One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
   27.90 +leaving us with one other:
   27.91  \begin{isabelle}
   27.92  \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
   27.93  \end{isabelle}
   27.94 @@ -704,8 +705,7 @@
   27.95  is robust: the \isa{conjI} forces the \isa{erule} to select a
   27.96  conjunction.  The two subgoals are the ones we would expect from applying
   27.97  conjunction introduction to
   27.98 -\isa{Q\
   27.99 -\isasymand\ R}:  
  27.100 +\isa{Q~\isasymand~R}:  
  27.101  \begin{isabelle}
  27.102  \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
  27.103  Q\isanewline
  27.104 @@ -926,10 +926,12 @@
  27.105  \end{isabelle}
  27.106  If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
  27.107  P(x)$ is also true.  It is a dual of the universal elimination rule, and
  27.108 -logic texts present it using the same notation for substitution.  The existential
  27.109 +logic texts present it using the same notation for substitution.
  27.110 +
  27.111 +The existential
  27.112  elimination rule looks like this
  27.113  in a logic text: 
  27.114 -\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
  27.115 +\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
  27.116  %
  27.117  It looks like this in Isabelle: 
  27.118  \begin{isabelle}
  27.119 @@ -953,17 +955,18 @@
  27.120  
  27.121  
  27.122  \section{Hilbert's Epsilon-Operator}
  27.123 +\label{sec:SOME}
  27.124  
  27.125 -Isabelle/HOL provides Hilbert's
  27.126 -$\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
  27.127 +HOL provides Hilbert's
  27.128 +$\varepsilon$-operator.  The term $\varepsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
  27.129  true, provided such a value exists.  Using this operator, we can express an
  27.130  existential destruction rule:
  27.131 -\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
  27.132 +\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
  27.133  This rule is seldom used, for it can cause exponential blow-up.  
  27.134  
  27.135  \subsection{Definite Descriptions}
  27.136  
  27.137 -In ASCII, we write \isa{SOME} for $\epsilon$.
  27.138 +In ASCII, we write \isa{SOME} for $\varepsilon$.
  27.139  \REMARK{the internal constant is \isa{Eps}}
  27.140  The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
  27.141  description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
  27.142 @@ -979,7 +982,7 @@
  27.143  prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
  27.144  description) and proceed to prove other facts.
  27.145  
  27.146 -Here is an example.  HOL defines \isa{inv},\indexbold{*inv (constant)}
  27.147 +Here is another example.  Isabelle/HOL defines \isa{inv},\indexbold{*inv (constant)}
  27.148  which expresses inverses of functions, as a definite
  27.149  description:
  27.150  \begin{isabelle}
  27.151 @@ -1025,7 +1028,6 @@
  27.152  \ 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
  27.153  \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
  27.154  \end{isabelle}
  27.155 -
  27.156  As always with \isa{some_equality}, we must show existence and
  27.157  uniqueness of the claimed solution,~\isa{k}.  Existence, the first
  27.158  subgoal, is trivial.  Uniqueness, the second subgoal, follows by antisymmetry:
  27.159 @@ -1063,6 +1065,7 @@
  27.160  \ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
  27.161  \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
  27.162  \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
  27.163 +
  27.164  \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
  27.165  \isasymLongrightarrow \ P\ x\ (?f\ x)
  27.166  \end{isabelle}
  27.167 @@ -1072,6 +1075,7 @@
  27.168  
  27.169  \begin{isabelle}
  27.170  \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
  27.171 +
  27.172  \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
  27.173  \end{isabelle}
  27.174  
  27.175 @@ -1141,7 +1145,8 @@
  27.176  \begin{isabelle}
  27.177  *** empty result sequence -- proof command failed
  27.178  \end{isabelle}
  27.179 -We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
  27.180 +If we interact with Isabelle via the shell interface,
  27.181 +we abandon a failed proof with the \isacommand{oops} command.
  27.182  
  27.183  \medskip 
  27.184  
  27.185 @@ -1301,7 +1306,7 @@
  27.186  \begin{isabelle}
  27.187  \isacommand{lemma}\
  27.188  [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
  27.189 -(xs=[]\ \isacharampersand\ ys=[])"\isanewline
  27.190 +(xs=[]\ \isasymand\ ys=[])"\isanewline
  27.191  \isacommand{apply}\ (induct_tac\ xs)\isanewline
  27.192  \isacommand{apply}\ (simp_all)\isanewline
  27.193  \isacommand{done}
  27.194 @@ -1314,7 +1319,7 @@
  27.195  (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
  27.196  \end{isabelle}
  27.197  A product is zero if and only if one of the factors is zero.  The
  27.198 -reasoning  involves a logical \textsc{or}.  Proving new rules for
  27.199 +reasoning  involves a disjunction.  Proving new rules for
  27.200  disjunctive reasoning  is hard, but translating to an actual disjunction
  27.201  works:  the classical reasoner handles disjunction properly.
  27.202  
  27.203 @@ -1490,8 +1495,8 @@
  27.204  We state it with the \isa{iff} attribute so that 
  27.205  Isabelle can use it to remove some occurrences of \isa{gcd}. 
  27.206  The theorem has a one-line 
  27.207 -proof using \isa{blast} supplied with four introduction 
  27.208 -rules: note the {\isa{intro}} attribute. The exclamation mark 
  27.209 +proof using \isa{blast} supplied with two additional introduction 
  27.210 +rules. The exclamation mark 
  27.211  ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 
  27.212  applied aggressively.  Rules given without the exclamation mark 
  27.213  are applied reluctantly and their uses can be undone if 
  27.214 @@ -1519,8 +1524,8 @@
  27.215  
  27.216  Of the latter methods, the most useful is {\isa{clarify}}. It performs 
  27.217  all obvious reasoning steps without splitting the goal into multiple 
  27.218 -parts. It does not apply rules that could render the 
  27.219 -goal unprovable (so-called unsafe rules). By performing the obvious 
  27.220 +parts. It does not apply unsafe rules that could render the 
  27.221 +goal unprovable. By performing the obvious 
  27.222  steps, {\isa{clarify}} lays bare the difficult parts of the problem, 
  27.223  where human intervention is necessary. 
  27.224  
  27.225 @@ -1568,7 +1573,7 @@
  27.226  That makes them slower but enables them to work correctly in the 
  27.227  presence of the more unusual features of Isabelle rules, such 
  27.228  as type classes and function unknowns. For example, recall the introduction rule
  27.229 -for Hilbert's epsilon-operator: 
  27.230 +for Hilbert's $\varepsilon$-operator: 
  27.231  \begin{isabelle}
  27.232  ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
  27.233  \rulename{someI}
  27.234 @@ -1796,7 +1801,7 @@
  27.235  instance of a rule by specifying facts for its premises.  Let us try
  27.236  it with this rule:
  27.237  \begin{isabelle}
  27.238 -\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
  27.239 +\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
  27.240  \isasymLongrightarrow\ ?k\ dvd\ ?m
  27.241  \rulename{relprime_dvd_mult}
  27.242  \end{isabelle}
  27.243 @@ -1809,7 +1814,7 @@
  27.244  We have evaluated an application of the \isa{gcd} function by
  27.245  simplification.  Expression evaluation  is not guaranteed to terminate, and
  27.246  certainly is not  efficient; Isabelle performs arithmetic operations by 
  27.247 -rewriting symbolic bit strings.  Here, however, the simplification takes
  27.248 +rewriting symbolic bit strings.  Here, however, the simplification above takes
  27.249  less than one second.  We can specify this new lemma to \isa{OF},
  27.250  generating an instance of \isa{relprime_dvd_mult}.  The expression
  27.251  \begin{isabelle}
  27.252 @@ -1826,7 +1831,7 @@
  27.253  \isasymlbrakk?k\ dvd\ ?m;\
  27.254  ?k\ dvd\ ?n\isasymrbrakk\
  27.255  \isasymLongrightarrow\ ?k\ dvd\
  27.256 -(?m\ +\ ?n)
  27.257 +?m\ +\ ?n
  27.258  \rulename{dvd_add}\isanewline
  27.259  ?m\ dvd\ ?m%
  27.260  \rulename{dvd_refl}
  27.261 @@ -1846,7 +1851,7 @@
  27.262  \end{isabelle}
  27.263  The result is 
  27.264  \begin{isabelle}
  27.265 -\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
  27.266 +\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
  27.267  \end{isabelle}
  27.268  
  27.269  You may have noticed that \isa{THEN} and \isa{OF} are based on 
  27.270 @@ -1933,7 +1938,7 @@
  27.271  \begin{isabelle}
  27.272  \isacommand{lemma}\
  27.273  relprime_dvd_mult:\isanewline
  27.274 -\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\
  27.275 +\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
  27.276  \isasymrbrakk\
  27.277  \isasymLongrightarrow\ k\ dvd\
  27.278  m"\isanewline
  27.279 @@ -1943,11 +1948,7 @@
  27.280  In the resulting subgoal, note how the equation has been 
  27.281  inserted: 
  27.282  \begin{isabelle}
  27.283 -\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
  27.284 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
  27.285 -m\isanewline
  27.286 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
  27.287 -\ \ \ \ \ m\ *\ gcd\
  27.288 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
  27.289  (k,\ n)\
  27.290  =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
  27.291  \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
  27.292 @@ -1956,12 +1957,8 @@
  27.293  utilizes the assumption \isa{gcd(k,n)\ =\
  27.294  1}. Here is the result: 
  27.295  \begin{isabelle}
  27.296 -\isasymlbrakk gcd\ (k,\
  27.297 -n)\ =\ 1;\ k\
  27.298 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
  27.299 -m\isanewline
  27.300 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
  27.301 -\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
  27.302 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
  27.303 +\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
  27.304  \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
  27.305  \end{isabelle}
  27.306  Simplification has yielded an equation for \isa{m} that will be used to
  27.307 @@ -2042,8 +2039,7 @@
  27.308  \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
  27.309  \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
  27.310  \end{isabelle}
  27.311 -
  27.312 -The first subgoal is trivial, but for the second Isabelle needs help to eliminate
  27.313 +The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
  27.314  the case
  27.315  \isa{z}=35.  The second invocation  of {\isa{subgoal_tac}} leaves two
  27.316  subgoals: 
  27.317 @@ -2056,8 +2052,8 @@
  27.318  \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
  27.319  \end{isabelle}
  27.320  
  27.321 -Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
  27.322 -the method {\isa{arith}}. For the second subgoal we apply the method \isa{force}, 
  27.323 +Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
  27.324 +(\isa{arith}). For the second subgoal we apply the method \isa{force}, 
  27.325  which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
  27.326  
  27.327  
    28.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Jan 24 11:59:15 2001 +0100
    28.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Jan 24 12:29:10 2001 +0100
    28.3 @@ -28,6 +28,7 @@
    28.4  \isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
    28.5  the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
    28.6  and not as @{text"(x # y) # z"}.
    28.7 +The @{text 65} is the priority of the infix @{text"#"}.
    28.8  
    28.9  \begin{warn}
   28.10    Syntax annotations are a powerful but optional feature. You
   28.11 @@ -44,9 +45,10 @@
   28.12  
   28.13  text{*
   28.14  \noindent
   28.15 -In contrast to ML, Isabelle insists on explicit declarations of all functions
   28.16 -(keyword \isacommand{consts}).  (Apart from the declaration-before-use
   28.17 -restriction, the order of items in a theory file is unconstrained.) Function
   28.18 +In contrast to many functional programming languages,
   28.19 +Isabelle insists on explicit declarations of all functions
   28.20 +(keyword \isacommand{consts}).  Apart from the declaration-before-use
   28.21 +restriction, the order of items in a theory file is unconstrained. Function
   28.22  @{text"app"} is annotated with concrete syntax too. Instead of the
   28.23  prefix syntax @{text"app xs ys"} the infix
   28.24  @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
   28.25 @@ -89,11 +91,11 @@
   28.26  \end{warn}
   28.27  
   28.28  A remark about syntax.  The textual definition of a theory follows a fixed
   28.29 -syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
   28.30 -Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   28.31 +syntax with keywords like \isacommand{datatype} and \isacommand{end}.
   28.32 +% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   28.33  Embedded in this syntax are the types and formulae of HOL, whose syntax is
   28.34 -extensible, e.g.\ by new user-defined infix operators
   28.35 -(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
   28.36 +extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
   28.37 +To distinguish the two levels, everything
   28.38  HOL-specific (terms and types) should be enclosed in
   28.39  \texttt{"}\dots\texttt{"}. 
   28.40  To lessen this burden, quotation marks around a single identifier can be
   28.41 @@ -179,10 +181,7 @@
   28.42  By default, induction acts on the first subgoal. The new proof state contains
   28.43  two subgoals, namely the base case (@{term[source]Nil}) and the induction step
   28.44  (@{term[source]Cons}):
   28.45 -\begin{isabelle}
   28.46 -~1.~rev~(rev~[])~=~[]\isanewline
   28.47 -~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
   28.48 -\end{isabelle}
   28.49 +@{subgoals[display,indent=0,margin=65]}
   28.50  
   28.51  The induction step is an example of the general format of a subgoal:
   28.52  \begin{isabelle}
   28.53 @@ -211,9 +210,7 @@
   28.54  ``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   28.55  to the equation @{prop"rev [] = []"}) and disappears; the simplified version
   28.56  of subgoal~2 becomes the new subgoal~1:
   28.57 -\begin{isabelle}
   28.58 -~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
   28.59 -\end{isabelle}
   28.60 +@{subgoals[display,indent=0,margin=70]}
   28.61  In order to simplify this subgoal further, a lemma suggests itself.
   28.62  *}
   28.63  (*<*)
   28.64 @@ -231,10 +228,10 @@
   28.65  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   28.66  
   28.67  txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
   28.68 -\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
   28.69 -the importance we attach to a proposition.  We use the words
   28.70 +\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
   28.71 +the importance we attach to a proposition.  Therefore we use the words
   28.72  \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
   28.73 -interchangeably.
   28.74 +interchangeably, too.
   28.75  
   28.76  There are two variables that we could induct on: @{term"xs"} and
   28.77  @{term"ys"}. Because @{text"@"} is defined by recursion on
   28.78 @@ -285,8 +282,8 @@
   28.79  
   28.80  % Instead of \isacommand{apply} followed by a dot, you can simply write
   28.81  % \isacommand{by}\indexbold{by}, which we do most of the time.
   28.82 -Notice that in lemma @{thm[source]app_Nil2}
   28.83 -(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
   28.84 +Notice that in lemma @{thm[source]app_Nil2},
   28.85 +as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
   28.86  replaced by the unknown @{text"?xs"}, just as explained in
   28.87  \S\ref{sec:variables}.
   28.88  
   28.89 @@ -326,7 +323,7 @@
   28.90  text{*
   28.91  \noindent
   28.92  succeeds without further ado.
   28.93 -Now we can go back and prove the first lemma
   28.94 +Now we can prove the first lemma
   28.95  *}
   28.96  
   28.97  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
    29.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Jan 24 11:59:15 2001 +0100
    29.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Jan 24 12:29:10 2001 +0100
    29.3 @@ -30,6 +30,7 @@
    29.4  \isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
    29.5  the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
    29.6  and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
    29.7 +The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
    29.8  
    29.9  \begin{warn}
   29.10    Syntax annotations are a powerful but optional feature. You
   29.11 @@ -44,9 +45,10 @@
   29.12  \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
   29.13  \begin{isamarkuptext}%
   29.14  \noindent
   29.15 -In contrast to ML, Isabelle insists on explicit declarations of all functions
   29.16 -(keyword \isacommand{consts}).  (Apart from the declaration-before-use
   29.17 -restriction, the order of items in a theory file is unconstrained.) Function
   29.18 +In contrast to many functional programming languages,
   29.19 +Isabelle insists on explicit declarations of all functions
   29.20 +(keyword \isacommand{consts}).  Apart from the declaration-before-use
   29.21 +restriction, the order of items in a theory file is unconstrained. Function
   29.22  \isa{app} is annotated with concrete syntax too. Instead of the
   29.23  prefix syntax \isa{app\ xs\ ys} the infix
   29.24  \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
   29.25 @@ -87,11 +89,11 @@
   29.26  \end{warn}
   29.27  
   29.28  A remark about syntax.  The textual definition of a theory follows a fixed
   29.29 -syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
   29.30 -Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   29.31 +syntax with keywords like \isacommand{datatype} and \isacommand{end}.
   29.32 +% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   29.33  Embedded in this syntax are the types and formulae of HOL, whose syntax is
   29.34 -extensible, e.g.\ by new user-defined infix operators
   29.35 -(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
   29.36 +extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
   29.37 +To distinguish the two levels, everything
   29.38  HOL-specific (terms and types) should be enclosed in
   29.39  \texttt{"}\dots\texttt{"}. 
   29.40  To lessen this burden, quotation marks around a single identifier can be
   29.41 @@ -174,9 +176,10 @@
   29.42  By default, induction acts on the first subgoal. The new proof state contains
   29.43  two subgoals, namely the base case (\isa{Nil}) and the induction step
   29.44  (\isa{Cons}):
   29.45 -\begin{isabelle}
   29.46 -~1.~rev~(rev~[])~=~[]\isanewline
   29.47 -~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
   29.48 +\begin{isabelle}%
   29.49 +\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
   29.50 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
   29.51 +\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%
   29.52  \end{isabelle}
   29.53  
   29.54  The induction step is an example of the general format of a subgoal:
   29.55 @@ -204,8 +207,9 @@
   29.56  ``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   29.57  to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
   29.58  of subgoal~2 becomes the new subgoal~1:
   29.59 -\begin{isabelle}
   29.60 -~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
   29.61 +\begin{isabelle}%
   29.62 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
   29.63 +\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%
   29.64  \end{isabelle}
   29.65  In order to simplify this subgoal further, a lemma suggests itself.%
   29.66  \end{isamarkuptxt}%
   29.67 @@ -221,10 +225,10 @@
   29.68  \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}%
   29.69  \begin{isamarkuptxt}%
   29.70  \noindent The keywords \isacommand{theorem}\index{*theorem} and
   29.71 -\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
   29.72 -the importance we attach to a proposition.  We use the words
   29.73 +\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
   29.74 +the importance we attach to a proposition.  Therefore we use the words
   29.75  \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
   29.76 -interchangeably.
   29.77 +interchangeably, too.
   29.78  
   29.79  There are two variables that we could induct on: \isa{xs} and
   29.80  \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
   29.81 @@ -272,8 +276,8 @@
   29.82  
   29.83  % Instead of \isacommand{apply} followed by a dot, you can simply write
   29.84  % \isacommand{by}\indexbold{by}, which we do most of the time.
   29.85 -Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
   29.86 -(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
   29.87 +Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
   29.88 +as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
   29.89  replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
   29.90  \S\ref{sec:variables}.
   29.91  
   29.92 @@ -313,7 +317,7 @@
   29.93  \begin{isamarkuptext}%
   29.94  \noindent
   29.95  succeeds without further ado.
   29.96 -Now we can go back and prove the first lemma%
   29.97 +Now we can prove the first lemma%
   29.98  \end{isamarkuptext}%
   29.99  \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
  29.100  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
    30.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Wed Jan 24 11:59:15 2001 +0100
    30.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Wed Jan 24 12:29:10 2001 +0100
    30.3 @@ -130,7 +130,7 @@
    30.4  This proof may look surprisingly straightforward. However, note that this
    30.5  comes at a cost: the proof script is unreadable because the intermediate
    30.6  proof states are invisible, and we rely on the (possibly brittle) magic of
    30.7 -@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
    30.8 +@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
    30.9  of the induction up in such a way that case distinction on @{term bs} makes
   30.10  sense and solves the proof. Part~\ref{Isar} shows you how to write readable
   30.11  and stable proofs.
    31.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Wed Jan 24 11:59:15 2001 +0100
    31.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Wed Jan 24 12:29:10 2001 +0100
    31.3 @@ -120,7 +120,7 @@
    31.4  This proof may look surprisingly straightforward. However, note that this
    31.5  comes at a cost: the proof script is unreadable because the intermediate
    31.6  proof states are invisible, and we rely on the (possibly brittle) magic of
    31.7 -\isa{auto} (\isa{simp{\isacharunderscore}all} will not do---try it) to split the subgoals
    31.8 +\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
    31.9  of the induction up in such a way that case distinction on \isa{bs} makes
   31.10  sense and solves the proof. Part~\ref{Isar} shows you how to write readable
   31.11  and stable proofs.%
    32.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 24 11:59:15 2001 +0100
    32.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 24 12:29:10 2001 +0100
    32.3 @@ -23,7 +23,7 @@
    32.4  text{*
    32.5  HOL comes with a number of overloaded constants and corresponding classes.
    32.6  The most important ones are listed in Table~\ref{tab:overloading}. They are
    32.7 -defined on all numeric types and somtimes on other types as well, for example
    32.8 +defined on all numeric types and sometimes on other types as well, for example
    32.9  @{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
   32.10  
   32.11  \begin{table}[htbp]
   32.12 @@ -34,9 +34,13 @@
   32.13  @{term 0} & @{text "'a::zero"} \\
   32.14  @{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
   32.15  @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
   32.16 +@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
   32.17  @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   32.18 +@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   32.19 +@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   32.20 +@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   32.21 +@{text"/"}  & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
   32.22  @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
   32.23 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
   32.24  @{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
   32.25  @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   32.26  @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
    33.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Jan 24 11:59:15 2001 +0100
    33.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Jan 24 12:29:10 2001 +0100
    33.3 @@ -25,7 +25,7 @@
    33.4  \begin{isamarkuptext}%
    33.5  HOL comes with a number of overloaded constants and corresponding classes.
    33.6  The most important ones are listed in Table~\ref{tab:overloading}. They are
    33.7 -defined on all numeric types and somtimes on other types as well, for example
    33.8 +defined on all numeric types and sometimes on other types as well, for example
    33.9  \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
   33.10  
   33.11  \begin{table}[htbp]
   33.12 @@ -36,9 +36,13 @@
   33.13  \isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
   33.14  \isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
   33.15  \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
   33.16 +\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
   33.17  \isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   33.18 +\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   33.19 +\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   33.20 +\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   33.21 +\isa{{\isacharslash}}  & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
   33.22  \isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
   33.23 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
   33.24  \isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
   33.25  \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   33.26  \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
    34.1 --- a/doc-src/TutorialI/basics.tex	Wed Jan 24 11:59:15 2001 +0100
    34.2 +++ b/doc-src/TutorialI/basics.tex	Wed Jan 24 12:29:10 2001 +0100
    34.3 @@ -2,7 +2,7 @@
    34.4  
    34.5  \section{Introduction}
    34.6  
    34.7 -This is a tutorial on how to use Isabelle/HOL as a specification and
    34.8 +This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and
    34.9  verification system. Isabelle is a generic system for implementing logical
   34.10  formalisms, and Isabelle/HOL is the specialization of Isabelle for
   34.11  HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
   34.12 @@ -15,13 +15,12 @@
   34.13  misled: HOL can express most mathematical concepts, and functional
   34.14  programming is just one particularly simple and ubiquitous instance.
   34.15  
   34.16 -This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
   34.17 -which is an extension of Isabelle~\cite{paulson-isa-book} with structured
   34.18 -proofs.\footnote{Thus the full name of the system should be
   34.19 -  Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
   34.20 -difference to classical Isabelle (which is the basis of another version of
   34.21 -this tutorial) is the replacement of the ML level by a dedicated language for
   34.22 -definitions and proofs.
   34.23 +Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
   34.24 +This has influenced some of HOL's concrete syntax but is otherwise
   34.25 +irrelevant for us because this tutorial is based on
   34.26 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle
   34.27 +with structured proofs.\footnote{Thus the full name of the system should be
   34.28 +  Isabelle/Isar/HOL, but that is a bit of a mouthful.}
   34.29  
   34.30  A tutorial is by definition incomplete.  Currently the tutorial only
   34.31  introduces the rudiments of Isar's proof language. To fully exploit the power
   34.32 @@ -74,7 +73,7 @@
   34.33    HOL contains a theory \isaindexbold{Main}, the union of all the basic
   34.34    predefined theories like arithmetic, lists, sets, etc.  
   34.35    Unless you know what you are doing, always include \isa{Main}
   34.36 -  as a direct or indirect parent theory of all your theories.
   34.37 +  as a direct or indirect parent of all your theories.
   34.38  \end{warn}
   34.39  
   34.40  
   34.41 @@ -122,7 +121,8 @@
   34.42  \end{ttbox}
   34.43  
   34.44  \noindent
   34.45 -This can be reversed by \texttt{ML "reset show_types"}. Various other flags
   34.46 +This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
   34.47 +which we introduce as we go along,
   34.48  can be set and reset in the same manner.\indexbold{flag!(re)setting}
   34.49  \end{warn}
   34.50  
   34.51 @@ -196,7 +196,7 @@
   34.52  should be familiar with to avoid certain syntactic traps. A particular
   34.53  problem for novices can be the priority of operators. If you are unsure, use
   34.54  additional parentheses. In those cases where Isabelle echoes your
   34.55 -input, you can see which parentheses are dropped---they were superfluous. If
   34.56 +input, you can see which parentheses are dropped --- they were superfluous. If
   34.57  you are unsure how to interpret Isabelle's output because you don't know
   34.58  where the (dropped) parentheses go, set the \rmindex{flag}
   34.59  \isaindexbold{show_brackets}:
   34.60 @@ -222,7 +222,7 @@
   34.61  \item
   34.62  Constructs with an opening but without a closing delimiter bind very weakly
   34.63  and should therefore be enclosed in parentheses if they appear in subterms, as
   34.64 -in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
   34.65 +in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
   34.66  \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
   34.67  \item
   34.68  Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
    35.1 --- a/doc-src/TutorialI/fp.tex	Wed Jan 24 11:59:15 2001 +0100
    35.2 +++ b/doc-src/TutorialI/fp.tex	Wed Jan 24 12:29:10 2001 +0100
    35.3 @@ -122,11 +122,11 @@
    35.4    the files have not been modified).
    35.5    
    35.6    If you suddenly discover that you need to modify a parent theory of your
    35.7 -  current theory you must first abandon your current theory\indexbold{abandon
    35.8 +  current theory, you must first abandon your current theory\indexbold{abandon
    35.9    theory}\indexbold{theory!abandon} (at the shell
   35.10    level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
   35.11 -  been modified you go back to your original theory. When its first line
   35.12 -  \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
   35.13 +  been modified, you go back to your original theory. When its first line
   35.14 +  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
   35.15    modified parent is reloaded automatically.
   35.16    
   35.17    The only time when you need to load a theory by hand is when you simply
   35.18 @@ -291,12 +291,12 @@
   35.19  \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
   35.20  that it did not need to so far. However, when you go beyond toy examples, you
   35.21  need to understand the ingredients of \isa{auto}.  This section covers the
   35.22 -method that \isa{auto} always applies first, namely simplification.
   35.23 +method that \isa{auto} always applies first, simplification.
   35.24  
   35.25  Simplification is one of the central theorem proving tools in Isabelle and
   35.26  many other systems. The tool itself is called the \bfindex{simplifier}. The
   35.27  purpose of this section is introduce the many features of the simplifier.
   35.28 -Anybody intending to use HOL should read this section. Later on
   35.29 +Anybody intending to perform proofs in HOL should read this section. Later on
   35.30  ({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
   35.31  little bit of how the simplifier works. The serious student should read that
   35.32  section as well, in particular in order to understand what happened if things
   35.33 @@ -359,7 +359,7 @@
   35.34  This declaration is a real can of worms.
   35.35  In HOL it must be ruled out because it requires a type
   35.36  \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
   35.37 -same cardinality---an impossibility. For the same reason it is not possible
   35.38 +same cardinality --- an impossibility. For the same reason it is not possible
   35.39  to allow recursion involving the type \isa{set}, which is isomorphic to
   35.40  \isa{t \isasymFun\ bool}.
   35.41  
   35.42 @@ -380,7 +380,7 @@
   35.43  \end{isabelle}
   35.44  do indeed make sense.  Note the different arrow,
   35.45  \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
   35.46 -expressing the type of \textbf{continuous} functions. 
   35.47 +expressing the type of \emph{continuous} functions. 
   35.48  There is even a version of LCF on top of HOL,
   35.49  called HOLCF~\cite{MuellerNvOS99}.
   35.50  
    36.1 --- a/doc-src/TutorialI/todo.tobias	Wed Jan 24 11:59:15 2001 +0100
    36.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Jan 24 12:29:10 2001 +0100
    36.3 @@ -89,10 +89,10 @@
    36.4  ==================
    36.5  
    36.6  Exercises
    36.7 -%\begin{exercise}
    36.8 -%Extend expressions by conditional expressions.
    36.9 -braucht wfrec!
   36.10 -%\end{exercise}
   36.11 +
   36.12 +For extensionality (in Sets chapter): prove
   36.13 +valif o norm = valif
   36.14 +in If-expression case study (Ifexpr)
   36.15  
   36.16  Nested inductive datatypes: another example/exercise:
   36.17   size(t) <= size(subst s t)?
    37.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Jan 24 11:59:15 2001 +0100
    37.2 +++ b/doc-src/TutorialI/tutorial.tex	Wed Jan 24 12:29:10 2001 +0100
    37.3 @@ -75,9 +75,9 @@
    37.4  
    37.5  \subsubsection*{Acknowledgements}
    37.6  This tutorial owes a lot to the constant discussions with and the valuable
    37.7 -feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
    37.8 +feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
    37.9  Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
   37.10 -and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
   37.11 +and Markus Wenzel. Stephan Merz was also kind enough to
   37.12  read and comment on a draft version.
   37.13  \clearfirst
   37.14  
   37.15 @@ -91,7 +91,7 @@
   37.16  \chapter{Theory Presentation}
   37.17  \chapter{Case Study: Verifying a Cryptographic Protocol}
   37.18  \chapter{Structured Proofs}
   37.19 -\chapter{Case Study: UNIX File-System Security}
   37.20 +%\chapter{Case Study: UNIX File-System Security}
   37.21  %\chapter{The Tricks of the Trade}
   37.22  \input{appendix}
   37.23