*** empty log message ***
authornipkow
Mon Oct 09 10:18:21 2000 +0200 (2000-10-09)
changeset 1017159d6633835fa
parent 10170 dfff821d2949
child 10172 3daeda3d3cd0
*** empty log message ***
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/document/CTL.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/Fundata.thy
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Misc/arith1.thy
doc-src/TutorialI/Misc/arith2.thy
doc-src/TutorialI/Misc/case_exprs.thy
doc-src/TutorialI/Misc/document/arith2.tex
doc-src/TutorialI/Misc/document/case_exprs.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/Nested1.thy
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/simplification.thy
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/ToyList2/ToyList2
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  \chapter{Advanced Simplification, Recursion, and Induction}
     1.5 -\markboth{}{CHAPTER 4: ADVANCED}
     1.6 +\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION ...}
     1.7  
     1.8  Although we have already learned a lot about simplification, recursion and
     1.9  induction, there are some advanced proof techniques that we have not covered
     2.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 09:33:45 2000 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 10:18:21 2000 +0200
     2.3 @@ -291,12 +291,13 @@
     2.4  text{*
     2.5  Function @{term path} has fulfilled its purpose now and can be forgotten
     2.6  about. It was merely defined to provide the witness in the proof of the
     2.7 -@{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know
     2.8 +@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
     2.9  that we could have given the witness without having to define a new function:
    2.10  the term
    2.11  @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
    2.12 +is extensionally equal to @{term"path s P"},
    2.13  where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
    2.14 -equations we omit, is extensionally equal to @{term"path s P"}.
    2.15 +equations we omit.
    2.16  *};
    2.17  (*<*)
    2.18  lemma infinity_lemma:
    2.19 @@ -372,6 +373,18 @@
    2.20  done
    2.21  
    2.22  text{*
    2.23 +The above language is not quite CTL. The latter also includes an
    2.24 +until-operator, usually written as an infix @{text U}. The formula
    2.25 +@{term"f U g"} means ``@{term f} until @{term g}''.
    2.26 +It is not definable in terms of the other operators!
    2.27 +\begin{exercise}
    2.28 +Extend the datatype of formulae by the until operator with semantics
    2.29 +@{text[display]"s \<Turnstile> f U g = (............)"}
    2.30 +and model checking algorithm
    2.31 +@{text[display]"mc(f U g) = (............)"}
    2.32 +Prove that the equivalence between semantics and model checking still holds.
    2.33 +\end{exercise}
    2.34 +
    2.35  Let us close this section with a few words about the executability of @{term mc}.
    2.36  It is clear that if all sets are finite, they can be represented as lists and the usual
    2.37  set operations are easily implemented. Only @{term lfp} requires a little thought.
     3.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 09:33:45 2000 +0200
     3.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 10:18:21 2000 +0200
     3.3 @@ -187,4 +187,34 @@
     3.4  apply(induct_tac f);
     3.5  apply(auto simp add:EF_lemma);
     3.6  done;
     3.7 -(*<*)end(*>*)
     3.8 +
     3.9 +text{*
    3.10 +\begin{exercise}
    3.11 +@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
    3.12 +as that is the ASCII equivalent of @{text"\<exists>"}}
    3.13 +(``there exists a next state such that'') with the intended semantics
    3.14 +@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
    3.15 +Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
    3.16 +
    3.17 +Show that the semantics for @{term EF} satisfies the following recursion equation:
    3.18 +@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
    3.19 +\end{exercise}
    3.20 +*}
    3.21 +(*<*)
    3.22 +theorem main: "mc f = {s. s \<Turnstile> f}";
    3.23 +apply(induct_tac f);
    3.24 +apply(auto simp add:EF_lemma);
    3.25 +done;
    3.26 +
    3.27 +lemma aux: "s \<Turnstile> f = (s : mc f)";
    3.28 +apply(simp add:main);
    3.29 +done;
    3.30 +
    3.31 +lemma "(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> Neg(AX(Neg(EF f))))";
    3.32 +apply(simp only:aux);
    3.33 +apply(simp);
    3.34 +apply(rule ssubst[OF lfp_Tarski[OF mono_ef]], fast);
    3.35 +done
    3.36 +
    3.37 +end
    3.38 +(*>*)
     4.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 09:33:45 2000 +0200
     4.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 10:18:21 2000 +0200
     4.3 @@ -188,7 +188,7 @@
     4.4  holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
     4.5  is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
     4.6  \begin{isabelle}%
     4.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
     4.8 +\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
     4.9  \end{isabelle}
    4.10  When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
    4.11  \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
    4.12 @@ -220,14 +220,15 @@
    4.13  \begin{isamarkuptext}%
    4.14  Function \isa{path} has fulfilled its purpose now and can be forgotten
    4.15  about. It was merely defined to provide the witness in the proof of the
    4.16 -\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
    4.17 +\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
    4.18  that we could have given the witness without having to define a new function:
    4.19  the term
    4.20  \begin{isabelle}%
    4.21  \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
    4.22  \end{isabelle}
    4.23 +is extensionally equal to \isa{path\ s\ P},
    4.24  where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
    4.25 -equations we omit, is extensionally equal to \isa{path\ s\ P}.%
    4.26 +equations we omit.%
    4.27  \end{isamarkuptext}%
    4.28  %
    4.29  \begin{isamarkuptext}%
    4.30 @@ -271,6 +272,22 @@
    4.31  \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline
    4.32  \isacommand{done}%
    4.33  \begin{isamarkuptext}%
    4.34 +The above language is not quite CTL. The latter also includes an
    4.35 +until-operator, usually written as an infix \isa{U}. The formula
    4.36 +\isa{f\ U\ g} means ``\isa{f} until \isa{g}''.
    4.37 +It is not definable in terms of the other operators!
    4.38 +\begin{exercise}
    4.39 +Extend the datatype of formulae by the until operator with semantics
    4.40 +\begin{isabelle}%
    4.41 +\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
    4.42 +\end{isabelle}
    4.43 +and model checking algorithm
    4.44 +\begin{isabelle}%
    4.45 +\ \ \ \ \ mc{\isacharparenleft}f\ U\ g{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
    4.46 +\end{isabelle}
    4.47 +Prove that the equivalence between semantics and model checking still holds.
    4.48 +\end{exercise}
    4.49 +
    4.50  Let us close this section with a few words about the executability of \isa{mc}.
    4.51  It is clear that if all sets are finite, they can be represented as lists and the usual
    4.52  set operations are easily implemented. Only \isa{lfp} requires a little thought.
     5.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 09:33:45 2000 +0200
     5.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 10:18:21 2000 +0200
     5.3 @@ -173,7 +173,24 @@
     5.4  \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
     5.5  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
     5.6  \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
     5.7 -\isacommand{done}\end{isabellebody}%
     5.8 +\isacommand{done}%
     5.9 +\begin{isamarkuptext}%
    5.10 +\begin{exercise}
    5.11 +\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
    5.12 +as that is the ASCII equivalent of \isa{{\isasymexists}}}
    5.13 +(``there exists a next state such that'') with the intended semantics
    5.14 +\begin{isabelle}%
    5.15 +\ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
    5.16 +\end{isabelle}
    5.17 +Fortunately, \isa{EN\ f} can already be expressed as a PDL formula. How?
    5.18 +
    5.19 +Show that the semantics for \isa{EF} satisfies the following recursion equation:
    5.20 +\begin{isabelle}%
    5.21 +\ \ \ \ \ s\ {\isasymTurnstile}\ EF\ f\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymor}\ s\ {\isasymTurnstile}\ EN\ {\isacharparenleft}EF\ f{\isacharparenright}{\isacharparenright}%
    5.22 +\end{isabelle}
    5.23 +\end{exercise}%
    5.24 +\end{isamarkuptext}%
    5.25 +\end{isabellebody}%
    5.26  %%% Local Variables:
    5.27  %%% mode: latex
    5.28  %%% TeX-master: "root"
     6.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Oct 09 09:33:45 2000 +0200
     6.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Oct 09 10:18:21 2000 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  appropriate function itself.
     6.5  *}
     6.6  
     6.7 -types 'v binop = "'v \\<Rightarrow> 'v \\<Rightarrow> 'v";
     6.8 +types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
     6.9  datatype ('a,'v)expr = Cex 'v
    6.10                       | Vex 'a
    6.11                       | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
    6.12 @@ -27,7 +27,7 @@
    6.13  values is easily defined:
    6.14  *}
    6.15  
    6.16 -consts value :: "('a,'v)expr \\<Rightarrow> ('a \\<Rightarrow> 'v) \\<Rightarrow> 'v";
    6.17 +consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v";
    6.18  primrec
    6.19  "value (Cex v) env = v"
    6.20  "value (Vex a) env = env a"
    6.21 @@ -53,13 +53,13 @@
    6.22  unchanged:
    6.23  *}
    6.24  
    6.25 -consts exec :: "('a,'v)instr list \\<Rightarrow> ('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> 'v list";
    6.26 +consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list";
    6.27  primrec
    6.28  "exec [] s vs = vs"
    6.29  "exec (i#is) s vs = (case i of
    6.30 -    Const v  \\<Rightarrow> exec is s (v#vs)
    6.31 -  | Load a   \\<Rightarrow> exec is s ((s a)#vs)
    6.32 -  | Apply f  \\<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
    6.33 +    Const v  \<Rightarrow> exec is s (v#vs)
    6.34 +  | Load a   \<Rightarrow> exec is s ((s a)#vs)
    6.35 +  | Apply f  \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
    6.36  
    6.37  text{*\noindent
    6.38  Recall that @{term"hd"} and @{term"tl"}
    6.39 @@ -74,7 +74,7 @@
    6.40  definition is pretty much obvious:
    6.41  *}
    6.42  
    6.43 -consts comp :: "('a,'v)expr \\<Rightarrow> ('a,'v)instr list";
    6.44 +consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list";
    6.45  primrec
    6.46  "comp (Cex v)       = [Const v]"
    6.47  "comp (Vex a)       = [Load a]"
    6.48 @@ -90,7 +90,7 @@
    6.49  This theorem needs to be generalized to
    6.50  *}
    6.51  
    6.52 -theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    6.53 +theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    6.54  
    6.55  txt{*\noindent
    6.56  which is proved by induction on @{term"e"} followed by simplification, once
    6.57 @@ -99,7 +99,7 @@
    6.58  *}
    6.59  (*<*)oops;(*>*)
    6.60  lemma exec_app[simp]:
    6.61 -  "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    6.62 +  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    6.63  
    6.64  txt{*\noindent
    6.65  This requires induction on @{term"xs"} and ordinary simplification for the
    6.66 @@ -107,8 +107,8 @@
    6.67  that contains two @{text"case"}-expressions over instructions. Thus we add
    6.68  automatic case splitting as well, which finishes the proof:
    6.69  *}
    6.70 -by(induct_tac xs, simp, simp split: instr.split);
    6.71 -
    6.72 +apply(induct_tac xs, simp, simp split: instr.split);
    6.73 +(*<*)done(*>*)
    6.74  text{*\noindent
    6.75  Note that because \isaindex{auto} performs simplification, it can
    6.76  also be modified in the same way @{text simp} can. Thus the proof can be
    6.77 @@ -116,10 +116,10 @@
    6.78  *}
    6.79  (*<*)
    6.80  declare exec_app[simp del];
    6.81 -lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    6.82 +lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    6.83  (*>*)
    6.84 -by(induct_tac xs, auto split: instr.split);
    6.85 -
    6.86 +apply(induct_tac xs, auto split: instr.split);
    6.87 +(*<*)done(*>*)
    6.88  text{*\noindent
    6.89  Although this is more compact, it is less clear for the reader of the proof.
    6.90  
    6.91 @@ -129,7 +129,7 @@
    6.92  its instance.
    6.93  *}
    6.94  (*<*)
    6.95 -theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    6.96 +theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    6.97  by(induct_tac e, auto);
    6.98  end
    6.99  (*>*)
     7.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Oct 09 09:33:45 2000 +0200
     7.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Oct 09 10:18:21 2000 +0200
     7.3 @@ -98,14 +98,14 @@
     7.4  that contains two \isa{case}-expressions over instructions. Thus we add
     7.5  automatic case splitting as well, which finishes the proof:%
     7.6  \end{isamarkuptxt}%
     7.7 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
     7.8 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
     7.9  \begin{isamarkuptext}%
    7.10  \noindent
    7.11  Note that because \isaindex{auto} performs simplification, it can
    7.12  also be modified in the same way \isa{simp} can. Thus the proof can be
    7.13  rewritten as%
    7.14  \end{isamarkuptext}%
    7.15 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    7.16 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
    7.17  \begin{isamarkuptext}%
    7.18  \noindent
    7.19  Although this is more compact, it is less clear for the reader of the proof.
     8.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Mon Oct 09 09:33:45 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Mon Oct 09 10:18:21 2000 +0200
     8.3 @@ -101,7 +101,8 @@
     8.4  The resulting 8 goals (one for each constructor) are proved in one fell swoop:
     8.5  *}
     8.6  
     8.7 -by simp_all;
     8.8 +apply simp_all;
     8.9 +(*<*)done(*>*)
    8.10  
    8.11  text{*
    8.12  In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
     9.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 09:33:45 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 10:18:21 2000 +0200
     9.3 @@ -35,7 +35,8 @@
     9.4  The following lemma has a canonical proof  *}
     9.5  
     9.6  lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
     9.7 -by(induct_tac T, simp_all)
     9.8 +apply(induct_tac T, simp_all)
     9.9 +done
    9.10  
    9.11  text{*\noindent
    9.12  %apply(induct_tac T);
    10.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Mon Oct 09 09:33:45 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Mon Oct 09 10:18:21 2000 +0200
    10.3 @@ -12,18 +12,18 @@
    10.4  datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
    10.5  
    10.6  text{*\noindent
    10.7 -Note that we need to quote @{text"term"} on the left to avoid confusion with
    10.8 -the command \isacommand{term}.
    10.9 +Note that we need to quote @{text term} on the left to avoid confusion with
   10.10 +the Isabelle command \isacommand{term}.
   10.11  Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
   10.12  function symbols.
   10.13  A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
   10.14 -  [Var y]]"}, where @{term"f"}, @{term"g"}, @{term"x"}, @{term"y"} are
   10.15 +  [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
   10.16  suitable values, e.g.\ numbers or strings.
   10.17  
   10.18 -What complicates the definition of @{text"term"} is the nested occurrence of
   10.19 -@{text"term"} inside @{text"list"} on the right-hand side. In principle,
   10.20 +What complicates the definition of @{text term} is the nested occurrence of
   10.21 +@{text term} inside @{text list} on the right-hand side. In principle,
   10.22  nested recursion can be eliminated in favour of mutual recursion by unfolding
   10.23 -the offending datatypes, here @{text"list"}. The result for @{text"term"}
   10.24 +the offending datatypes, here @{text list}. The result for @{text term}
   10.25  would be something like
   10.26  \medskip
   10.27  
   10.28 @@ -33,7 +33,7 @@
   10.29  \noindent
   10.30  Although we do not recommend this unfolding to the user, it shows how to
   10.31  simulate nested recursion by mutual recursion.
   10.32 -Now we return to the initial definition of @{text"term"} using
   10.33 +Now we return to the initial definition of @{text term} using
   10.34  nested recursion.
   10.35  
   10.36  Let us define a substitution function on terms. Because terms involve term
   10.37 @@ -41,8 +41,8 @@
   10.38  *}
   10.39  
   10.40  consts
   10.41 -subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
   10.42 -substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
   10.43 +subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term      \<Rightarrow> ('a,'b)term"
   10.44 +substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list";
   10.45  
   10.46  primrec
   10.47    "subst s (Var x) = s x"
   10.48 @@ -53,7 +53,8 @@
   10.49    "substs s (t # ts) = subst s t # substs s ts";
   10.50  
   10.51  text{*\noindent
   10.52 -(Please ignore the label @{thm[source]subst_App} for the moment.)
   10.53 +Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.
   10.54 +The significance of this device will become apparent below.
   10.55  
   10.56  Similarly, when proving a statement about terms inductively, we need
   10.57  to prove a related statement about term lists simultaneously. For example,
   10.58 @@ -61,12 +62,13 @@
   10.59  strengthened and proved as follows:
   10.60  *}
   10.61  
   10.62 -lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
   10.63 +lemma "subst  Var t  = (t ::('a,'b)term)  \<and>
   10.64          substs Var ts = (ts::('a,'b)term list)";
   10.65 -by(induct_tac t and ts, simp_all);
   10.66 +apply(induct_tac t and ts, simp_all);
   10.67 +done
   10.68  
   10.69  text{*\noindent
   10.70 -Note that @{term"Var"} is the identity substitution because by definition it
   10.71 +Note that @{term Var} is the identity substitution because by definition it
   10.72  leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
   10.73  that the type annotations are necessary because otherwise there is nothing in
   10.74  the goal to enforce that both halves of the goal talk about the same type
   10.75 @@ -82,14 +84,14 @@
   10.76  its definition is found in theorem @{thm[source]o_def}).
   10.77  \end{exercise}
   10.78  \begin{exercise}\label{ex:trev-trev}
   10.79 -  Define a function @{text"trev"} of type @{typ"('a,'b)term => ('a,'b)term"}
   10.80 +  Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}
   10.81  that recursively reverses the order of arguments of all function symbols in a
   10.82    term. Prove that @{prop"trev(trev t) = t"}.
   10.83  \end{exercise}
   10.84  
   10.85  The experienced functional programmer may feel that our above definition of
   10.86 -@{term"subst"} is unnecessarily complicated in that @{term"substs"} is
   10.87 -completely unnecessary. The @{term"App"}-case can be defined directly as
   10.88 +@{term subst} is unnecessarily complicated in that @{term substs} is
   10.89 +completely unnecessary. The @{term App}-case can be defined directly as
   10.90  @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
   10.91  where @{term"map"} is the standard list function such that
   10.92  @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
   10.93 @@ -98,7 +100,8 @@
   10.94  *}
   10.95  
   10.96  lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
   10.97 -by(induct_tac ts, simp_all)
   10.98 +apply(induct_tac ts, simp_all)
   10.99 +done
  10.100  
  10.101  text{*\noindent
  10.102  What is more, we can now disable the old defining equation as a
  10.103 @@ -108,19 +111,19 @@
  10.104  declare subst_App [simp del]
  10.105  
  10.106  text{*\noindent
  10.107 -The advantage is that now we have replaced @{term"substs"} by
  10.108 -@{term"map"}, we can profit from the large number of pre-proved lemmas
  10.109 -about @{term"map"}.  Unfortunately inductive proofs about type
  10.110 -@{text"term"} are still awkward because they expect a conjunction. One
  10.111 +The advantage is that now we have replaced @{term substs} by
  10.112 +@{term map}, we can profit from the large number of pre-proved lemmas
  10.113 +about @{term map}.  Unfortunately inductive proofs about type
  10.114 +@{text term} are still awkward because they expect a conjunction. One
  10.115  could derive a new induction principle as well (see
  10.116  \S\ref{sec:derive-ind}), but turns out to be simpler to define
  10.117  functions by \isacommand{recdef} instead of \isacommand{primrec}.
  10.118  The details are explained in \S\ref{sec:advanced-recdef} below.
  10.119  
  10.120  Of course, you may also combine mutual and nested recursion. For example,
  10.121 -constructor @{text"Sum"} in \S\ref{sec:datatype-mut-rec} could take a list of
  10.122 -expressions as its argument: @{text"Sum"}~@{typ[quotes]"'a aexp list"}.
  10.123 +constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
  10.124 +expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
  10.125  *}
  10.126  (*<*)
  10.127  end
  10.128 -(*>*)
  10.129 +(*>*)
  10.130 \ No newline at end of file
    11.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Oct 09 09:33:45 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Oct 09 10:18:21 2000 +0200
    11.3 @@ -93,7 +93,7 @@
    11.4  \noindent
    11.5  The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
    11.6  \end{isamarkuptxt}%
    11.7 -\isacommand{by}\ simp{\isacharunderscore}all%
    11.8 +\isacommand{apply}\ simp{\isacharunderscore}all%
    11.9  \begin{isamarkuptext}%
   11.10  In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
   11.11  an inductive proof expects a goal of the form
    12.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 09 09:33:45 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 09 10:18:21 2000 +0200
    12.3 @@ -36,7 +36,8 @@
    12.4  The following lemma has a canonical proof%
    12.5  \end{isamarkuptext}%
    12.6  \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
    12.7 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
    12.8 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
    12.9 +\isacommand{done}%
   12.10  \begin{isamarkuptext}%
   12.11  \noindent
   12.12  %apply(induct_tac T);
    13.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 09:33:45 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 10:18:21 2000 +0200
    13.3 @@ -12,7 +12,7 @@
    13.4  \begin{isamarkuptext}%
    13.5  \noindent
    13.6  Note that we need to quote \isa{term} on the left to avoid confusion with
    13.7 -the command \isacommand{term}.
    13.8 +the Isabelle command \isacommand{term}.
    13.9  Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
   13.10  function symbols.
   13.11  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
   13.12 @@ -50,7 +50,8 @@
   13.13  \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
   13.14  \begin{isamarkuptext}%
   13.15  \noindent
   13.16 -(Please ignore the label \isa{subst{\isacharunderscore}App} for the moment.)
   13.17 +Individual equations in a primrec definition may be named as shown for \isa{subst{\isacharunderscore}App}.
   13.18 +The significance of this device will become apparent below.
   13.19  
   13.20  Similarly, when proving a statement about terms inductively, we need
   13.21  to prove a related statement about term lists simultaneously. For example,
   13.22 @@ -59,7 +60,8 @@
   13.23  \end{isamarkuptext}%
   13.24  \isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
   13.25  \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
   13.26 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
   13.27 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
   13.28 +\isacommand{done}%
   13.29  \begin{isamarkuptext}%
   13.30  \noindent
   13.31  Note that \isa{Var} is the identity substitution because by definition it
   13.32 @@ -97,7 +99,8 @@
   13.33  that the suggested equation holds:%
   13.34  \end{isamarkuptext}%
   13.35  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
   13.36 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
   13.37 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
   13.38 +\isacommand{done}%
   13.39  \begin{isamarkuptext}%
   13.40  \noindent
   13.41  What is more, we can now disable the old defining equation as a
    14.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Mon Oct 09 09:33:45 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Mon Oct 09 10:18:21 2000 +0200
    14.3 @@ -92,7 +92,8 @@
    14.4  *}
    14.5  
    14.6  apply(induct_tac b);
    14.7 -by(auto);
    14.8 +apply(auto);
    14.9 +done
   14.10  
   14.11  text{*\noindent
   14.12  In fact, all proofs in this case study look exactly like this. Hence we do
    15.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Oct 09 09:33:45 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Oct 09 10:18:21 2000 +0200
    15.3 @@ -85,7 +85,8 @@
    15.4  The proof is canonical:%
    15.5  \end{isamarkuptxt}%
    15.6  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
    15.7 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    15.8 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
    15.9 +\isacommand{done}%
   15.10  \begin{isamarkuptext}%
   15.11  \noindent
   15.12  In fact, all proofs in this case study look exactly like this. Hence we do
    16.1 --- a/doc-src/TutorialI/Misc/arith1.thy	Mon Oct 09 09:33:45 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/arith1.thy	Mon Oct 09 10:18:21 2000 +0200
    16.3 @@ -1,7 +1,7 @@
    16.4  (*<*)
    16.5  theory arith1 = Main:;
    16.6  (*>*)
    16.7 -lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
    16.8 +lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
    16.9  (**)(*<*)
   16.10  by(auto);
   16.11  end
    17.1 --- a/doc-src/TutorialI/Misc/arith2.thy	Mon Oct 09 09:33:45 2000 +0200
    17.2 +++ b/doc-src/TutorialI/Misc/arith2.thy	Mon Oct 09 10:18:21 2000 +0200
    17.3 @@ -2,7 +2,8 @@
    17.4  theory arith2 = Main:;
    17.5  (*>*)
    17.6  lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
    17.7 -by(arith);
    17.8 +apply(arith);
    17.9  (**)(*<*)
   17.10 +done
   17.11  end
   17.12  (*>*)
    18.1 --- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 09:33:45 2000 +0200
    18.2 +++ b/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 10:18:21 2000 +0200
    18.3 @@ -65,8 +65,8 @@
    18.4  which is solved automatically:
    18.5  *}
    18.6  
    18.7 -by(auto)
    18.8 -
    18.9 +apply(auto)
   18.10 +(*<*)done(*>*)
   18.11  text{*
   18.12  Note that we do not need to give a lemma a name if we do not intend to refer
   18.13  to it explicitly in the future.
    19.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Oct 09 09:33:45 2000 +0200
    19.2 +++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Oct 09 10:18:21 2000 +0200
    19.3 @@ -2,7 +2,7 @@
    19.4  \begin{isabellebody}%
    19.5  \def\isabellecontext{arith2}%
    19.6  \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    19.7 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
    19.8 +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    19.9  \end{isabellebody}%
   19.10  %%% Local Variables:
   19.11  %%% mode: latex
    20.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 09:33:45 2000 +0200
    20.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 10:18:21 2000 +0200
    20.3 @@ -71,7 +71,7 @@
    20.4  \end{isabelle}
    20.5  which is solved automatically:%
    20.6  \end{isamarkuptxt}%
    20.7 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
    20.8 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
    20.9  \begin{isamarkuptext}%
   20.10  Note that we do not need to give a lemma a name if we do not intend to refer
   20.11  to it explicitly in the future.%
    21.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 09 09:33:45 2000 +0200
    21.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 09 10:18:21 2000 +0200
    21.3 @@ -19,7 +19,8 @@
    21.4  \end{isamarkuptext}%
    21.5  \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
    21.6  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
    21.7 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
    21.8 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
    21.9 +\isacommand{done}\isanewline
   21.10  \end{isabellebody}%
   21.11  %%% Local Variables:
   21.12  %%% mode: latex
    22.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Oct 09 09:33:45 2000 +0200
    22.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Oct 09 10:18:21 2000 +0200
    22.3 @@ -81,7 +81,8 @@
    22.4  as simplification rules and are simplified themselves. For example:%
    22.5  \end{isamarkuptext}%
    22.6  \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
    22.7 -\isacommand{by}\ simp%
    22.8 +\isacommand{apply}\ simp\isanewline
    22.9 +\isacommand{done}%
   22.10  \begin{isamarkuptext}%
   22.11  \noindent
   22.12  The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
   22.13 @@ -100,7 +101,8 @@
   22.14  nontermination but not this one. The problem can be circumvented by
   22.15  explicitly telling the simplifier to ignore the assumptions:%
   22.16  \end{isamarkuptxt}%
   22.17 -\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
   22.18 +\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline
   22.19 +\isacommand{done}%
   22.20  \begin{isamarkuptext}%
   22.21  \noindent
   22.22  There are three options that influence the treatment of assumptions:
   22.23 @@ -152,9 +154,9 @@
   22.24  \begin{isabelle}
   22.25  ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
   22.26  \end{isabelle}
   22.27 -can be proved by simplification. Thus we could have proved the lemma outright%
   22.28 +can be proved by simplification. Thus we could have proved the lemma outright by%
   22.29  \end{isamarkuptxt}%
   22.30 -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
   22.31 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
   22.32  \begin{isamarkuptext}%
   22.33  \noindent
   22.34  Of course we can also unfold definitions in the middle of a proof.
   22.35 @@ -180,7 +182,8 @@
   22.36  \isa{Let{\isacharunderscore}def}:%
   22.37  \end{isamarkuptext}%
   22.38  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
   22.39 -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
   22.40 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
   22.41 +\isacommand{done}%
   22.42  \begin{isamarkuptext}%
   22.43  If, in a particular context, there is no danger of a combinatorial explosion
   22.44  of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
   22.45 @@ -194,7 +197,8 @@
   22.46  accepts \emph{conditional} equations, for example%
   22.47  \end{isamarkuptext}%
   22.48  \isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   22.49 -\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}%
   22.50 +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}\isanewline
   22.51 +\isacommand{done}%
   22.52  \begin{isamarkuptext}%
   22.53  \noindent
   22.54  Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
   22.55 @@ -259,7 +263,7 @@
   22.56  in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
   22.57  dropped, the above goal is solved,%
   22.58  \end{isamarkuptext}%
   22.59 -\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
   22.60 +\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
   22.61  \begin{isamarkuptext}%
   22.62  \noindent%
   22.63  which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
    23.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 09 09:33:45 2000 +0200
    23.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 09 10:18:21 2000 +0200
    23.3 @@ -17,7 +17,8 @@
    23.4  
    23.5  lemma "sum n + sum n = n*(Suc n)";
    23.6  apply(induct_tac n);
    23.7 -by(auto);
    23.8 +apply(auto);
    23.9 +done
   23.10  
   23.11  (*<*)
   23.12  end
    24.1 --- a/doc-src/TutorialI/Misc/simp.thy	Mon Oct 09 09:33:45 2000 +0200
    24.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Mon Oct 09 10:18:21 2000 +0200
    24.3 @@ -79,8 +79,9 @@
    24.4  as simplification rules and are simplified themselves. For example:
    24.5  *}
    24.6  
    24.7 -lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
    24.8 -by simp;
    24.9 +lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";
   24.10 +apply simp;
   24.11 +done
   24.12  
   24.13  text{*\noindent
   24.14  The second assumption simplifies to @{term"xs = []"}, which in turn
   24.15 @@ -91,7 +92,7 @@
   24.16  nontermination:
   24.17  *}
   24.18  
   24.19 -lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
   24.20 +lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
   24.21  
   24.22  txt{*\noindent
   24.23  cannot be solved by an unmodified application of @{text"simp"} because the
   24.24 @@ -101,7 +102,8 @@
   24.25  explicitly telling the simplifier to ignore the assumptions:
   24.26  *}
   24.27  
   24.28 -by(simp (no_asm));
   24.29 +apply(simp (no_asm));
   24.30 +done
   24.31  
   24.32  text{*\noindent
   24.33  There are three options that influence the treatment of assumptions:
   24.34 @@ -134,14 +136,14 @@
   24.35  original definition. For example, given
   24.36  *}
   24.37  
   24.38 -constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
   24.39 -         "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
   24.40 +constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   24.41 +         "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
   24.42  
   24.43  text{*\noindent
   24.44  we may want to prove
   24.45  *}
   24.46  
   24.47 -lemma "exor A (\\<not>A)";
   24.48 +lemma "exor A (\<not>A)";
   24.49  
   24.50  txt{*\noindent
   24.51  Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
   24.52 @@ -155,10 +157,10 @@
   24.53  \begin{isabelle}
   24.54  ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
   24.55  \end{isabelle}
   24.56 -can be proved by simplification. Thus we could have proved the lemma outright
   24.57 -*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
   24.58 -by(simp add: exor_def)
   24.59 -
   24.60 +can be proved by simplification. Thus we could have proved the lemma outright by
   24.61 +*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
   24.62 +apply(simp add: exor_def)
   24.63 +(*<*)done(*>*)
   24.64  text{*\noindent
   24.65  Of course we can also unfold definitions in the middle of a proof.
   24.66  
   24.67 @@ -183,7 +185,8 @@
   24.68  *}
   24.69  
   24.70  lemma "(let xs = [] in xs@ys@xs) = ys";
   24.71 -by(simp add: Let_def);
   24.72 +apply(simp add: Let_def);
   24.73 +done
   24.74  
   24.75  text{*
   24.76  If, in a particular context, there is no danger of a combinatorial explosion
   24.77 @@ -199,8 +202,9 @@
   24.78  accepts \emph{conditional} equations, for example
   24.79  *}
   24.80  
   24.81 -lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
   24.82 -by(case_tac xs, simp, simp);
   24.83 +lemma hd_Cons_tl[simp]: "xs \<noteq> []  \<Longrightarrow>  hd xs # tl xs = xs";
   24.84 +apply(case_tac xs, simp, simp);
   24.85 +done
   24.86  
   24.87  text{*\noindent
   24.88  Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
   24.89 @@ -209,7 +213,7 @@
   24.90  is present as well,
   24.91  *}
   24.92  
   24.93 -lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
   24.94 +lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
   24.95  (*<*)
   24.96  by(simp);
   24.97  (*>*)
   24.98 @@ -230,7 +234,7 @@
   24.99  distinction on the condition of the @{text"if"}. For example the goal
  24.100  *}
  24.101  
  24.102 -lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
  24.103 +lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
  24.104  
  24.105  txt{*\noindent
  24.106  can be split into
  24.107 @@ -254,7 +258,7 @@
  24.108  This splitting idea generalizes from @{text"if"} to \isaindex{case}:
  24.109  *}
  24.110  
  24.111 -lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
  24.112 +lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
  24.113  txt{*\noindent
  24.114  becomes
  24.115  \begin{isabelle}\makeatother
  24.116 @@ -274,10 +278,10 @@
  24.117  dropped, the above goal is solved,
  24.118  *}
  24.119  (*<*)
  24.120 -lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
  24.121 +lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
  24.122  (*>*)
  24.123 -by(simp split: list.split);
  24.124 -
  24.125 +apply(simp split: list.split);
  24.126 +(*<*)done(*>*)
  24.127  text{*\noindent%
  24.128  which \isacommand{apply}@{text"(simp)"} alone will not do.
  24.129  
  24.130 @@ -350,14 +354,14 @@
  24.131  (@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus
  24.132  *}
  24.133  
  24.134 -lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n"
  24.135 +lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
  24.136  (*<*)by(auto)(*>*)
  24.137  
  24.138  text{*\noindent
  24.139  is proved by simplification, whereas the only slightly more complex
  24.140  *}
  24.141  
  24.142 -lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
  24.143 +lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
  24.144  (*<*)by(arith)(*>*)
  24.145  
  24.146  text{*\noindent
    25.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 09:33:45 2000 +0200
    25.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 10:18:21 2000 +0200
    25.3 @@ -41,7 +41,8 @@
    25.4  The rest is pure simplification:
    25.5  *}
    25.6  
    25.7 -by simp_all;
    25.8 +apply simp_all;
    25.9 +done
   25.10  
   25.11  text{*
   25.12  Try proving the above lemma by structural induction, and you find that you
    26.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 09:33:45 2000 +0200
    26.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 10:18:21 2000 +0200
    26.3 @@ -4,12 +4,12 @@
    26.4  consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
    26.5  
    26.6  text{*\noindent
    26.7 -Although the definition of @{term"trev"} is quite natural, we will have
    26.8 +Although the definition of @{term trev} is quite natural, we will have
    26.9  overcome a minor difficulty in convincing Isabelle of is termination.
   26.10  It is precisely this difficulty that is the \textit{raison d'\^etre} of
   26.11  this subsection.
   26.12  
   26.13 -Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
   26.14 +Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
   26.15  simplifies matters because we are now free to use the recursion equation
   26.16  suggested at the end of \S\ref{sec:nested-datatype}:
   26.17  *};
   26.18 @@ -19,22 +19,22 @@
   26.19   "trev (App f ts) = App f (rev(map trev ts))";
   26.20  
   26.21  text{*\noindent
   26.22 -Remember that function @{term"size"} is defined for each \isacommand{datatype}.
   26.23 +Remember that function @{term size} is defined for each \isacommand{datatype}.
   26.24  However, the definition does not succeed. Isabelle complains about an
   26.25  unproved termination condition
   26.26  @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
   26.27 -where @{term"set"} returns the set of elements of a list
   26.28 +where @{term set} returns the set of elements of a list
   26.29  and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
   26.30  function automatically defined by Isabelle
   26.31 -(when @{text"term"} was defined).  First we have to understand why the
   26.32 -recursive call of @{term"trev"} underneath @{term"map"} leads to the above
   26.33 -condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
   26.34 -will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
   26.35 -condition expresses that the size of the argument @{term"t : set ts"} of any
   26.36 -recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
   26.37 +(when @{text term} was defined).  First we have to understand why the
   26.38 +recursive call of @{term trev} underneath @{term map} leads to the above
   26.39 +condition. The reason is that \isacommand{recdef} ``knows'' that @{term map}
   26.40 +will apply @{term trev} only to elements of @{term ts}. Thus the above
   26.41 +condition expresses that the size of the argument @{prop"t : set ts"} of any
   26.42 +recursive call of @{term trev} is strictly less than @{prop"size(App f ts) =
   26.43  Suc(term_list_size ts)"}.  We will now prove the termination condition and
   26.44  continue with our definition.  Below we return to the question of how
   26.45 -\isacommand{recdef} ``knows'' about @{term"map"}.
   26.46 +\isacommand{recdef} ``knows'' about @{term map}.
   26.47  *};
   26.48  
   26.49  (*<*)
    27.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Oct 09 09:33:45 2000 +0200
    27.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Mon Oct 09 10:18:21 2000 +0200
    27.3 @@ -78,7 +78,7 @@
    27.4  recdef dummy "{}"
    27.5  "dummy n = n"
    27.6  (*>*)
    27.7 -(hints cong: map_cong)
    27.8 +(hints recdef_cong: map_cong)
    27.9  
   27.10  text{*\noindent
   27.11  or declare them globally
   27.12 @@ -88,11 +88,11 @@
   27.13  declare map_cong[recdef_cong];
   27.14  
   27.15  text{*
   27.16 -Note that the global @{text cong} and @{text recdef_cong} attributes are
   27.17 +Note that the @{text cong} and @{text recdef_cong} attributes are
   27.18  intentionally kept apart because they control different activities, namely
   27.19 -simplification and making recursive definitions. The local @{text cong} in
   27.20 -the hints section of \isacommand{recdef} is merely short for @{text
   27.21 -recdef_cong}.
   27.22 +simplification and making recursive definitions.
   27.23 +% The local @{text cong} in
   27.24 +% the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}.
   27.25  %The simplifier's congruence rules cannot be used by recdef.
   27.26  %For example the weak congruence rules for if and case would prevent
   27.27  %recdef from generating sensible termination conditions.
    28.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 09:33:45 2000 +0200
    28.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 10:18:21 2000 +0200
    28.3 @@ -38,7 +38,8 @@
    28.4  \end{isabelle}
    28.5  The rest is pure simplification:%
    28.6  \end{isamarkuptxt}%
    28.7 -\isacommand{by}\ simp{\isacharunderscore}all%
    28.8 +\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
    28.9 +\isacommand{done}%
   28.10  \begin{isamarkuptext}%
   28.11  Try proving the above lemma by structural induction, and you find that you
   28.12  need an additional case distinction. What is worse, the names of variables
    29.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 09:33:45 2000 +0200
    29.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 10:18:21 2000 +0200
    29.3 @@ -72,7 +72,7 @@
    29.4  rules, you can either append a hint locally
    29.5  to the specific occurrence of \isacommand{recdef}%
    29.6  \end{isamarkuptext}%
    29.7 -{\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
    29.8 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
    29.9  \begin{isamarkuptext}%
   29.10  \noindent
   29.11  or declare them globally
   29.12 @@ -80,10 +80,11 @@
   29.13  \end{isamarkuptext}%
   29.14  \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
   29.15  \begin{isamarkuptext}%
   29.16 -Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
   29.17 +Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
   29.18  intentionally kept apart because they control different activities, namely
   29.19 -simplification and making recursive definitions. The local \isa{cong} in
   29.20 -the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
   29.21 +simplification and making recursive definitions.
   29.22 +% The local \isa{cong} in
   29.23 +% the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
   29.24  %The simplifier's congruence rules cannot be used by recdef.
   29.25  %For example the weak congruence rules for if and case would prevent
   29.26  %recdef from generating sensible termination conditions.%
    30.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 09 09:33:45 2000 +0200
    30.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 09 10:18:21 2000 +0200
    30.3 @@ -23,7 +23,7 @@
    30.4  is provded automatically because it is already present as a lemma in the
    30.5  arithmetic library. Thus the recursion equation becomes a simplification
    30.6  rule. Of course the equation is nonterminating if we are allowed to unfold
    30.7 -the recursive call inside the \isa{if} branch, which is why programming
    30.8 +the recursive call inside the \isa{else} branch, which is why programming
    30.9  languages and our simplifier don't do that. Unfortunately the simplifier does
   30.10  something else which leads to the same problem: it splits \isa{if}s if the
   30.11  condition simplifies to neither \isa{True} nor \isa{False}. For
   30.12 @@ -78,9 +78,11 @@
   30.13  derived conditional ones. For \isa{gcd} it means we have to prove%
   30.14  \end{isamarkuptext}%
   30.15  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
   30.16 -\isacommand{by}{\isacharparenleft}simp{\isacharparenright}\isanewline
   30.17 +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   30.18 +\isacommand{done}\isanewline
   30.19  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
   30.20 -\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
   30.21 +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   30.22 +\isacommand{done}%
   30.23  \begin{isamarkuptext}%
   30.24  \noindent
   30.25  after which we can disable the original simplification rule:%
    31.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Oct 09 09:33:45 2000 +0200
    31.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Oct 09 10:18:21 2000 +0200
    31.3 @@ -33,7 +33,8 @@
    31.4  It was not proved automatically because of the special nature of \isa{{\isacharminus}}
    31.5  on \isa{nat}. This requires more arithmetic than is tried by default:%
    31.6  \end{isamarkuptxt}%
    31.7 -\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
    31.8 +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    31.9 +\isacommand{done}%
   31.10  \begin{isamarkuptext}%
   31.11  \noindent
   31.12  Because \isacommand{recdef}'s termination prover involves simplification,
   31.13 @@ -51,7 +52,8 @@
   31.14  rules. Thus we can automatically prove%
   31.15  \end{isamarkuptext}%
   31.16  \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
   31.17 -\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
   31.18 +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   31.19 +\isacommand{done}%
   31.20  \begin{isamarkuptext}%
   31.21  \noindent
   31.22  More exciting theorems require induction, which is discussed below.
    32.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 09:33:45 2000 +0200
    32.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 10:18:21 2000 +0200
    32.3 @@ -7,12 +7,12 @@
    32.4  equations become simplification rules, just as with
    32.5  \isacommand{primrec}. In most cases this works fine, but there is a subtle
    32.6  problem that must be mentioned: simplification may not
    32.7 -terminate because of automatic splitting of @{text"if"}.
    32.8 +terminate because of automatic splitting of @{text if}.
    32.9  Let us look at an example:
   32.10  *}
   32.11  
   32.12 -consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
   32.13 -recdef gcd "measure (\\<lambda>(m,n).n)"
   32.14 +consts gcd :: "nat\<times>nat \<Rightarrow> nat";
   32.15 +recdef gcd "measure (\<lambda>(m,n).n)"
   32.16    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
   32.17  
   32.18  text{*\noindent
   32.19 @@ -22,10 +22,10 @@
   32.20  is provded automatically because it is already present as a lemma in the
   32.21  arithmetic library. Thus the recursion equation becomes a simplification
   32.22  rule. Of course the equation is nonterminating if we are allowed to unfold
   32.23 -the recursive call inside the @{text"if"} branch, which is why programming
   32.24 +the recursive call inside the @{text else} branch, which is why programming
   32.25  languages and our simplifier don't do that. Unfortunately the simplifier does
   32.26 -something else which leads to the same problem: it splits @{text"if"}s if the
   32.27 -condition simplifies to neither @{term"True"} nor @{term"False"}. For
   32.28 +something else which leads to the same problem: it splits @{text if}s if the
   32.29 +condition simplifies to neither @{term True} nor @{term False}. For
   32.30  example, simplification reduces
   32.31  @{term[display]"gcd(m,n) = k"}
   32.32  in one step to
   32.33 @@ -33,23 +33,23 @@
   32.34  where the condition cannot be reduced further, and splitting leads to
   32.35  @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
   32.36  Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
   32.37 -an @{text"if"}, it is unfolded again, which leads to an infinite chain of
   32.38 +an @{text if}, it is unfolded again, which leads to an infinite chain of
   32.39  simplification steps. Fortunately, this problem can be avoided in many
   32.40  different ways.
   32.41  
   32.42  The most radical solution is to disable the offending
   32.43  @{thm[source]split_if} as shown in the section on case splits in
   32.44  \S\ref{sec:Simplification}.  However, we do not recommend this because it
   32.45 -means you will often have to invoke the rule explicitly when @{text"if"} is
   32.46 +means you will often have to invoke the rule explicitly when @{text if} is
   32.47  involved.
   32.48  
   32.49  If possible, the definition should be given by pattern matching on the left
   32.50 -rather than @{text"if"} on the right. In the case of @{term"gcd"} the
   32.51 +rather than @{text if} on the right. In the case of @{term gcd} the
   32.52  following alternative definition suggests itself:
   32.53  *}
   32.54  
   32.55 -consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
   32.56 -recdef gcd1 "measure (\\<lambda>(m,n).n)"
   32.57 +consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
   32.58 +recdef gcd1 "measure (\<lambda>(m,n).n)"
   32.59    "gcd1 (m, 0) = m"
   32.60    "gcd1 (m, n) = gcd1(n, m mod n)";
   32.61  
   32.62 @@ -59,25 +59,27 @@
   32.63  @{prop"n ~= 0"}. Unfortunately, in general the case distinction
   32.64  may not be expressible by pattern matching.
   32.65  
   32.66 -A very simple alternative is to replace @{text"if"} by @{text"case"}, which
   32.67 +A very simple alternative is to replace @{text if} by @{text case}, which
   32.68  is also available for @{typ"bool"} but is not split automatically:
   32.69  *}
   32.70  
   32.71 -consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
   32.72 -recdef gcd2 "measure (\\<lambda>(m,n).n)"
   32.73 -  "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
   32.74 +consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
   32.75 +recdef gcd2 "measure (\<lambda>(m,n).n)"
   32.76 +  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
   32.77  
   32.78  text{*\noindent
   32.79  In fact, this is probably the neatest solution next to pattern matching.
   32.80  
   32.81  A final alternative is to replace the offending simplification rules by
   32.82 -derived conditional ones. For @{term"gcd"} it means we have to prove
   32.83 +derived conditional ones. For @{term gcd} it means we have to prove
   32.84  *}
   32.85  
   32.86  lemma [simp]: "gcd (m, 0) = m";
   32.87 -by(simp);
   32.88 -lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
   32.89 -by(simp);
   32.90 +apply(simp);
   32.91 +done
   32.92 +lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
   32.93 +apply(simp);
   32.94 +done
   32.95  
   32.96  text{*\noindent
   32.97  after which we can disable the original simplification rule:
    33.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Mon Oct 09 09:33:45 2000 +0200
    33.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Mon Oct 09 10:18:21 2000 +0200
    33.3 @@ -36,7 +36,8 @@
    33.4  on @{typ"nat"}. This requires more arithmetic than is tried by default:
    33.5  *}
    33.6  
    33.7 -by(arith);
    33.8 +apply(arith);
    33.9 +done
   33.10  
   33.11  text{*\noindent
   33.12  Because \isacommand{recdef}'s termination prover involves simplification,
   33.13 @@ -51,12 +52,13 @@
   33.14  
   33.15  text{*\noindent
   33.16  This time everything works fine. Now @{thm[source]g.simps} contains precisely
   33.17 -the stated recursion equation for @{term"g"} and they are simplification
   33.18 +the stated recursion equation for @{term g} and they are simplification
   33.19  rules. Thus we can automatically prove
   33.20  *}
   33.21  
   33.22  theorem "g(1,0) = g(1,1)";
   33.23 -by(simp);
   33.24 +apply(simp);
   33.25 +done
   33.26  
   33.27  text{*\noindent
   33.28  More exciting theorems require induction, which is discussed below.
   33.29 @@ -66,17 +68,17 @@
   33.30  \isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
   33.31  sufficiently general to warrant this distinction.
   33.32  
   33.33 -The attentive reader may wonder why we chose to call our function @{term"g"}
   33.34 -rather than @{term"f"} the second time around. The reason is that, despite
   33.35 -the failed termination proof, the definition of @{term"f"} did not
   33.36 +The attentive reader may wonder why we chose to call our function @{term g}
   33.37 +rather than @{term f} the second time around. The reason is that, despite
   33.38 +the failed termination proof, the definition of @{term f} did not
   33.39  fail, and thus we could not define it a second time. However, all theorems
   33.40 -about @{term"f"}, for example @{thm[source]f.simps}, carry as a precondition
   33.41 +about @{term f}, for example @{thm[source]f.simps}, carry as a precondition
   33.42  the unproved termination condition. Moreover, the theorems
   33.43  @{thm[source]f.simps} are not simplification rules. However, this mechanism
   33.44  allows a delayed proof of termination: instead of proving
   33.45  @{thm[source]termi_lem} up front, we could prove 
   33.46  it later on and then use it to remove the preconditions from the theorems
   33.47 -about @{term"f"}. In most cases this is more cumbersome than proving things
   33.48 +about @{term f}. In most cases this is more cumbersome than proving things
   33.49  up front.
   33.50  %FIXME, with one exception: nested recursion.
   33.51  
    34.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Oct 09 09:33:45 2000 +0200
    34.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Mon Oct 09 10:18:21 2000 +0200
    34.3 @@ -281,14 +281,17 @@
    34.4  We still need to confirm that the proof is now finished:
    34.5  *}
    34.6  
    34.7 -.
    34.8 +done
    34.9  
   34.10 -text{*\noindent\indexbold{$Isar@\texttt{.}}%
   34.11 -As a result of that final dot, Isabelle associates the lemma
   34.12 -just proved with its name. Instead of \isacommand{apply}
   34.13 -followed by a dot, you can simply write \isacommand{by}\indexbold{by},
   34.14 -which we do most of the time. Notice that in lemma @{thm[source]app_Nil2}
   34.15 -(as printed out after the final dot) the free variable @{term"xs"} has been
   34.16 +text{*\noindent\indexbold{done}%
   34.17 +As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
   34.18 +with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
   34.19 +if it is obvious from the context that the proof is finished.
   34.20 +
   34.21 +% Instead of \isacommand{apply} followed by a dot, you can simply write
   34.22 +% \isacommand{by}\indexbold{by}, which we do most of the time.
   34.23 +Notice that in lemma @{thm[source]app_Nil2}
   34.24 +(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
   34.25  replaced by the unknown @{text"?xs"}, just as explained in
   34.26  \S\ref{sec:variables}.
   34.27  
   34.28 @@ -326,7 +329,8 @@
   34.29  
   34.30  lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
   34.31  apply(induct_tac xs);
   34.32 -by(auto);
   34.33 +apply(auto);
   34.34 +done
   34.35  
   34.36  text{*
   34.37  \noindent
   34.38 @@ -336,7 +340,8 @@
   34.39  
   34.40  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   34.41  apply(induct_tac xs);
   34.42 -by(auto);
   34.43 +apply(auto);
   34.44 +done
   34.45  
   34.46  text{*\noindent
   34.47  and then solve our main theorem:
   34.48 @@ -344,7 +349,8 @@
   34.49  
   34.50  theorem rev_rev [simp]: "rev(rev xs) = xs";
   34.51  apply(induct_tac xs);
   34.52 -by(auto);
   34.53 +apply(auto);
   34.54 +done
   34.55  
   34.56  text{*\noindent
   34.57  The final \isacommand{end} tells Isabelle to close the current theory because
    35.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 09 09:33:45 2000 +0200
    35.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 09 10:18:21 2000 +0200
    35.3 @@ -261,14 +261,17 @@
    35.4  
    35.5  We still need to confirm that the proof is now finished:%
    35.6  \end{isamarkuptxt}%
    35.7 -\isacommand{{\isachardot}}%
    35.8 +\isacommand{done}%
    35.9  \begin{isamarkuptext}%
   35.10 -\noindent\indexbold{$Isar@\texttt{.}}%
   35.11 -As a result of that final dot, Isabelle associates the lemma
   35.12 -just proved with its name. Instead of \isacommand{apply}
   35.13 -followed by a dot, you can simply write \isacommand{by}\indexbold{by},
   35.14 -which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
   35.15 -(as printed out after the final dot) the free variable \isa{xs} has been
   35.16 +\noindent\indexbold{done}%
   35.17 +As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
   35.18 +with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
   35.19 +if it is obvious from the context that the proof is finished.
   35.20 +
   35.21 +% Instead of \isacommand{apply} followed by a dot, you can simply write
   35.22 +% \isacommand{by}\indexbold{by}, which we do most of the time.
   35.23 +Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
   35.24 +(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
   35.25  replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
   35.26  \S\ref{sec:variables}.
   35.27  
   35.28 @@ -302,7 +305,8 @@
   35.29  \end{isamarkuptext}%
   35.30  \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
   35.31  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   35.32 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   35.33 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
   35.34 +\isacommand{done}%
   35.35  \begin{isamarkuptext}%
   35.36  \noindent
   35.37  succeeds without further ado.
   35.38 @@ -310,14 +314,16 @@
   35.39  \end{isamarkuptext}%
   35.40  \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
   35.41  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   35.42 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   35.43 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
   35.44 +\isacommand{done}%
   35.45  \begin{isamarkuptext}%
   35.46  \noindent
   35.47  and then solve our main theorem:%
   35.48  \end{isamarkuptext}%
   35.49  \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   35.50  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   35.51 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   35.52 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
   35.53 +\isacommand{done}%
   35.54  \begin{isamarkuptext}%
   35.55  \noindent
   35.56  The final \isacommand{end} tells Isabelle to close the current theory because
    36.1 --- a/doc-src/TutorialI/ToyList2/ToyList2	Mon Oct 09 09:33:45 2000 +0200
    36.2 +++ b/doc-src/TutorialI/ToyList2/ToyList2	Mon Oct 09 10:18:21 2000 +0200
    36.3 @@ -1,18 +1,21 @@
    36.4  lemma app_Nil2 [simp]: "xs @ [] = xs"
    36.5  apply(induct_tac xs)
    36.6  apply(auto)
    36.7 -.
    36.8 +done
    36.9  
   36.10  lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
   36.11  apply(induct_tac xs)
   36.12 -by(auto)
   36.13 +apply(auto)
   36.14 +done
   36.15  
   36.16  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
   36.17  apply(induct_tac xs)
   36.18 -by(auto)
   36.19 +apply(auto)
   36.20 +done
   36.21  
   36.22  theorem rev_rev [simp]: "rev(rev xs) = xs"
   36.23  apply(induct_tac xs)
   36.24 -by(auto)
   36.25 +apply(auto)
   36.26 +done
   36.27  
   36.28  end
    37.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Mon Oct 09 09:33:45 2000 +0200
    37.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Mon Oct 09 10:18:21 2000 +0200
    37.3 @@ -18,8 +18,8 @@
    37.4  We define two selector functions:
    37.5  *};
    37.6  
    37.7 -consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
    37.8 -       alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
    37.9 +consts value :: "('a,'v)trie \<Rightarrow> 'v option"
   37.10 +       alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list";
   37.11  primrec "value(Trie ov al) = ov";
   37.12  primrec "alist(Trie ov al) = al";
   37.13  
   37.14 @@ -27,7 +27,7 @@
   37.15  Association lists come with a generic lookup function:
   37.16  *};
   37.17  
   37.18 -consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
   37.19 +consts   assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option";
   37.20  primrec "assoc [] x = None"
   37.21          "assoc (p#ps) x =
   37.22             (let (a,b) = p in if a=x then Some b else assoc ps x)";
   37.23 @@ -39,20 +39,21 @@
   37.24  recursion on the search string argument:
   37.25  *};
   37.26  
   37.27 -consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
   37.28 +consts   lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option";
   37.29  primrec "lookup t [] = value t"
   37.30          "lookup t (a#as) = (case assoc (alist t) a of
   37.31 -                              None \\<Rightarrow> None
   37.32 -                            | Some at \\<Rightarrow> lookup at as)";
   37.33 +                              None \<Rightarrow> None
   37.34 +                            | Some at \<Rightarrow> lookup at as)";
   37.35  
   37.36  text{*
   37.37  As a first simple property we prove that looking up a string in the empty
   37.38 -trie @{term"Trie None []"} always returns @{term"None"}. The proof merely
   37.39 +trie @{term"Trie None []"} always returns @{term None}. The proof merely
   37.40  distinguishes the two cases whether the search string is empty or not:
   37.41  *};
   37.42  
   37.43  lemma [simp]: "lookup (Trie None []) as = None";
   37.44 -by(case_tac as, simp_all);
   37.45 +apply(case_tac as, simp_all);
   37.46 +done
   37.47  
   37.48  text{*
   37.49  Things begin to get interesting with the definition of an update function
   37.50 @@ -60,24 +61,24 @@
   37.51  associated with that string:
   37.52  *};
   37.53  
   37.54 -consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
   37.55 +consts update :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie";
   37.56  primrec
   37.57    "update t []     v = Trie (Some v) (alist t)"
   37.58    "update t (a#as) v =
   37.59       (let tt = (case assoc (alist t) a of
   37.60 -                  None \\<Rightarrow> Trie None [] | Some at \\<Rightarrow> at)
   37.61 +                  None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
   37.62        in Trie (value t) ((a,update tt as v)#alist t))";
   37.63  
   37.64  text{*\noindent
   37.65  The base case is obvious. In the recursive case the subtrie
   37.66 -@{term"tt"} associated with the first letter @{term"a"} is extracted,
   37.67 +@{term tt} associated with the first letter @{term a} is extracted,
   37.68  recursively updated, and then placed in front of the association list.
   37.69 -The old subtrie associated with @{term"a"} is still in the association list
   37.70 -but no longer accessible via @{term"assoc"}. Clearly, there is room here for
   37.71 +The old subtrie associated with @{term a} is still in the association list
   37.72 +but no longer accessible via @{term assoc}. Clearly, there is room here for
   37.73  optimizations!
   37.74  
   37.75 -Before we start on any proofs about @{term"update"} we tell the simplifier to
   37.76 -expand all @{text"let"}s and to split all @{text"case"}-constructs over
   37.77 +Before we start on any proofs about @{term update} we tell the simplifier to
   37.78 +expand all @{text let}s and to split all @{text case}-constructs over
   37.79  options:
   37.80  *};
   37.81  
   37.82 @@ -85,23 +86,23 @@
   37.83  
   37.84  text{*\noindent
   37.85  The reason becomes clear when looking (probably after a failed proof
   37.86 -attempt) at the body of @{term"update"}: it contains both
   37.87 -@{text"let"} and a case distinction over type @{text"option"}.
   37.88 +attempt) at the body of @{term update}: it contains both
   37.89 +@{text let} and a case distinction over type @{text option}.
   37.90  
   37.91 -Our main goal is to prove the correct interaction of @{term"update"} and
   37.92 -@{term"lookup"}:
   37.93 +Our main goal is to prove the correct interaction of @{term update} and
   37.94 +@{term lookup}:
   37.95  *};
   37.96  
   37.97 -theorem "\\<forall>t v bs. lookup (update t as v) bs =
   37.98 +theorem "\<forall>t v bs. lookup (update t as v) bs =
   37.99                      (if as=bs then Some v else lookup t bs)";
  37.100  
  37.101  txt{*\noindent
  37.102 -Our plan is to induct on @{term"as"}; hence the remaining variables are
  37.103 +Our plan is to induct on @{term as}; hence the remaining variables are
  37.104  quantified. From the definitions it is clear that induction on either
  37.105 -@{term"as"} or @{term"bs"} is required. The choice of @{term"as"} is merely
  37.106 -guided by the intuition that simplification of @{term"lookup"} might be easier
  37.107 -if @{term"update"} has already been simplified, which can only happen if
  37.108 -@{term"as"} is instantiated.
  37.109 +@{term as} or @{term bs} is required. The choice of @{term as} is merely
  37.110 +guided by the intuition that simplification of @{term lookup} might be easier
  37.111 +if @{term update} has already been simplified, which can only happen if
  37.112 +@{term as} is instantiated.
  37.113  The start of the proof is completely conventional:
  37.114  *};
  37.115  apply(induct_tac as, auto);
  37.116 @@ -113,14 +114,15 @@
  37.117  ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
  37.118  ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs
  37.119  \end{isabelle}
  37.120 -Clearly, if we want to make headway we have to instantiate @{term"bs"} as
  37.121 +Clearly, if we want to make headway we have to instantiate @{term bs} as
  37.122  well now. It turns out that instead of induction, case distinction
  37.123  suffices:
  37.124  *};
  37.125 -by(case_tac[!] bs, auto);
  37.126 +apply(case_tac[!] bs, auto);
  37.127 +done
  37.128  
  37.129  text{*\noindent
  37.130 -All methods ending in @{text"tac"} take an optional first argument that
  37.131 +All methods ending in @{text tac} take an optional first argument that
  37.132  specifies the range of subgoals they are applied to, where @{text"[!]"} means
  37.133  all subgoals, i.e.\ @{text"[1-3]"} in our case. Individual subgoal numbers,
  37.134  e.g. @{text"[2]"} are also allowed.
  37.135 @@ -128,8 +130,8 @@
  37.136  This proof may look surprisingly straightforward. However, note that this
  37.137  comes at a cost: the proof script is unreadable because the intermediate
  37.138  proof states are invisible, and we rely on the (possibly brittle) magic of
  37.139 -@{text"auto"} (@{text"simp_all"} will not do---try it) to split the subgoals
  37.140 -of the induction up in such a way that case distinction on @{term"bs"} makes
  37.141 +@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
  37.142 +of the induction up in such a way that case distinction on @{term bs} makes
  37.143  sense and solves the proof. Part~\ref{Isar} shows you how to write readable
  37.144  and stable proofs.
  37.145  *};
    38.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Oct 09 09:33:45 2000 +0200
    38.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Oct 09 10:18:21 2000 +0200
    38.3 @@ -46,7 +46,8 @@
    38.4  distinguishes the two cases whether the search string is empty or not:%
    38.5  \end{isamarkuptext}%
    38.6  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
    38.7 -\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
    38.8 +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
    38.9 +\isacommand{done}%
   38.10  \begin{isamarkuptext}%
   38.11  Things begin to get interesting with the definition of an update function
   38.12  that adds a new (string,value) pair to a trie, overwriting the old value
   38.13 @@ -107,7 +108,8 @@
   38.14  well now. It turns out that instead of induction, case distinction
   38.15  suffices:%
   38.16  \end{isamarkuptxt}%
   38.17 -\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}%
   38.18 +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}\isanewline
   38.19 +\isacommand{done}%
   38.20  \begin{isamarkuptext}%
   38.21  \noindent
   38.22  All methods ending in \isa{tac} take an optional first argument that
    39.1 --- a/doc-src/TutorialI/appendix.tex	Mon Oct 09 09:33:45 2000 +0200
    39.2 +++ b/doc-src/TutorialI/appendix.tex	Mon Oct 09 10:18:21 2000 +0200
    39.3 @@ -5,80 +5,90 @@
    39.4  
    39.5  \begin{figure}[htbp]
    39.6  \begin{center}
    39.7 -\begin{tabular}{|ccccccccccc|}
    39.8 +\begin{tabular}{|l|l|l|}
    39.9  \hline
   39.10 -\indexboldpos{\isasymand}{$HOL0and} &
   39.11 -\indexboldpos{\isasymor}{$HOL0or} &
   39.12 -\indexboldpos{\isasymimp}{$HOL0imp} &
   39.13 -\indexboldpos{\isasymnot}{$HOL0not} &
   39.14 -\indexboldpos{\isasymnoteq}{$HOL0noteq} &
   39.15 -\indexboldpos{\isasymforall}{$HOL0All} &
   39.16 -\isasymforall &
   39.17 -\indexboldpos{\isasymexists}{$HOL0Ex} &
   39.18 -\isasymexists &
   39.19 -\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
   39.20 -\isasymuniqex \\
   39.21 -\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
   39.22 -\texttt{|}\index{$HOL0or@\ttor|bold} &
   39.23 -\ttindexboldpos{-->}{$HOL0imp} &
   39.24 -\verb$~$\index{$HOL0not@\verb$~$|bold} &
   39.25 -\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
   39.26 -\ttindexbold{ALL} &
   39.27 -\texttt{!}\index{$HOL0All@\ttall|bold} &
   39.28 -\ttindexbold{EX} &
   39.29 -\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
   39.30 -\ttEXU\index{EXX@\ttEXU|bold} &
   39.31 -\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
   39.32 -\hline\hline
   39.33  \indexboldpos{\isasymlbrakk}{$Isabrl} &
   39.34 +\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
   39.35 +\verb$\<lbrakk>$ \\
   39.36  \indexboldpos{\isasymrbrakk}{$Isabrr} &
   39.37 +\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
   39.38 +\verb$\<rbrakk>$ \\
   39.39  \indexboldpos{\isasymImp}{$IsaImp} &
   39.40 +\ttindexboldpos{==>}{$IsaImp} &
   39.41 +\verb$\<Longrightarrow>$ \\
   39.42  \indexboldpos{\isasymAnd}{$IsaAnd} &
   39.43 +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
   39.44 +\verb$\<And>$ \\
   39.45  \indexboldpos{\isasymequiv}{$IsaEq} &
   39.46 +\ttindexboldpos{==}{$IsaEq} &
   39.47 +\verb$\<equiv>$ \\
   39.48  \indexboldpos{\isasymlambda}{$Isalam} &
   39.49 -\indexboldpos{\isasymFun}{$IsaFun}&
   39.50 -&
   39.51 -&
   39.52 -&
   39.53 -\\
   39.54 -\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
   39.55 -\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
   39.56 -\ttindexboldpos{==>}{$IsaImp} &
   39.57 -\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
   39.58 -\ttindexboldpos{==}{$IsaEq} &
   39.59  \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
   39.60 -\ttindexboldpos{=>}{$IsaFun}&
   39.61 -&
   39.62 -&
   39.63 -&
   39.64 - \\
   39.65 -\hline\hline
   39.66 +\verb$\<lambda>$ \\
   39.67 +\indexboldpos{\isasymFun}{$IsaFun} &
   39.68 +\ttindexboldpos{=>}{$IsaFun} &
   39.69 +\verb$\<Rightarrow>$ \\
   39.70 +\indexboldpos{\isasymand}{$HOL0and} &
   39.71 +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
   39.72 +\verb$\<and>$ \\
   39.73 +\indexboldpos{\isasymor}{$HOL0or} &
   39.74 +\texttt{|}\index{$HOL0or@\ttor|bold} &
   39.75 +\verb$\<or>$ \\
   39.76 +\indexboldpos{\isasymimp}{$HOL0imp} &
   39.77 +\ttindexboldpos{-->}{$HOL0imp} &
   39.78 +\verb$\<longrightarrow>$ \\
   39.79 +\indexboldpos{\isasymnot}{$HOL0not} &
   39.80 +\verb$~$\index{$HOL0not@\verb$~$|bold} &
   39.81 +\verb$\<not>$ \\
   39.82 +\indexboldpos{\isasymnoteq}{$HOL0noteq} &
   39.83 +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
   39.84 +\verb$\<noteq>$ \\
   39.85 +\indexboldpos{\isasymforall}{$HOL0All} &
   39.86 +\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
   39.87 +\verb$\<forall>$ \\
   39.88 +\indexboldpos{\isasymexists}{$HOL0Ex} &
   39.89 +\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
   39.90 +\verb$\<exists>$ \\
   39.91 +\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
   39.92 +\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
   39.93 +\verb$\<exists>!$\\
   39.94 +\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
   39.95 +\ttindexbold{SOME} &
   39.96 +\verb$\<?>$\\
   39.97  \indexboldpos{\isasymcirc}{$HOL1} &
   39.98 +\ttindexbold{o} &
   39.99 +\verb$\<?>$\\
  39.100  \indexboldpos{\isasymle}{$HOL2arithrel}&
  39.101 +\ttindexboldpos{<=}{$HOL2arithrel}&
  39.102 +\verb$\<le>$\\
  39.103  \indexboldpos{\isasymtimes}{$IsaFun}&
  39.104 -&
  39.105 -&
  39.106 -&
  39.107 -&
  39.108 -&
  39.109 -&
  39.110 -&
  39.111 - \\
  39.112 -\ttindexbold{o} &
  39.113 -\ttindexboldpos{<=}{$HOL2arithrel}&
  39.114  \ttindexboldpos{*}{$HOL2arithfun} &
  39.115 -&
  39.116 -&
  39.117 -&
  39.118 -&
  39.119 -&
  39.120 -&
  39.121 -&
  39.122 -\\
  39.123 +\verb$\<times>$\\
  39.124 +\indexboldpos{\isasymin}{$HOL3Set}&
  39.125 +\ttindexboldpos{:}{$HOL3Set} &
  39.126 +\verb$\<in>$\\
  39.127 +? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
  39.128 +\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
  39.129 +\verb$\<notin>$\\
  39.130 +\indexboldpos{\isasymsubseteq}{$HOL3Set}&
  39.131 +\verb$<=$ &
  39.132 +\verb$\<subseteq>$\\
  39.133 +\indexboldpos{\isasymunion}{$HOL3Set}&
  39.134 +\ttindexbold{Un} &
  39.135 +\verb$\<union>$\\
  39.136 +\indexboldpos{\isasyminter}{$HOL3Set}&
  39.137 +\ttindexbold{Int} &
  39.138 +\verb$\<inter>$\\
  39.139 +\indexboldpos{\isasymUnion}{$HOL3Set}&
  39.140 +\ttindexbold{UN}, \ttindexbold{Union} &
  39.141 +\verb$\<Union>$\\
  39.142 +\indexboldpos{\isasymInter}{$HOL3Set}&
  39.143 +\ttindexbold{INT}, \ttindexbold{Inter} &
  39.144 +\verb$\<Inter>$\\
  39.145  \hline
  39.146  \end{tabular}
  39.147  \end{center}
  39.148 -\caption{Mathematical symbols and their ASCII-equivalents}
  39.149 +\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
  39.150  \label{fig:ascii}
  39.151  \end{figure}\indexbold{ASCII symbols}
  39.152  
    40.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Oct 09 09:33:45 2000 +0200
    40.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 09 10:18:21 2000 +0200
    40.3 @@ -65,7 +65,7 @@
    40.4  
    40.5  \input{basics}
    40.6  \input{fp}
    40.7 -%\input{CTL/ctl}
    40.8 +\input{CTL/ctl}
    40.9  \input{Advanced/advanced}
   40.10  %\chapter{The Tricks of the Trade}
   40.11  \input{appendix}