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{\isasymlbrakk}{$Isabrl} &
39.11 +\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
39.12 +\verb$\<lbrakk>$ \\
39.13 +\indexboldpos{\isasymrbrakk}{$Isabrr} &
39.14 +\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
39.15 +\verb$\<rbrakk>$ \\
39.16 +\indexboldpos{\isasymImp}{$IsaImp} &
39.17 +\ttindexboldpos{==>}{$IsaImp} &
39.18 +\verb$\<Longrightarrow>$ \\
39.19 +\indexboldpos{\isasymAnd}{$IsaAnd} &
39.20 +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
39.21 +\verb$\<And>$ \\
39.22 +\indexboldpos{\isasymequiv}{$IsaEq} &
39.23 +\ttindexboldpos{==}{$IsaEq} &
39.24 +\verb$\<equiv>$ \\
39.25 +\indexboldpos{\isasymlambda}{$Isalam} &
39.26 +\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
39.27 +\verb$\<lambda>$ \\
39.28 +\indexboldpos{\isasymFun}{$IsaFun} &
39.29 +\ttindexboldpos{=>}{$IsaFun} &
39.30 +\verb$\<Rightarrow>$ \\
39.31 \indexboldpos{\isasymand}{$HOL0and} &
39.32 +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
39.33 +\verb$\<and>$ \\
39.34 \indexboldpos{\isasymor}{$HOL0or} &
39.35 +\texttt{|}\index{$HOL0or@\ttor|bold} &
39.36 +\verb$\<or>$ \\
39.37 \indexboldpos{\isasymimp}{$HOL0imp} &
39.38 +\ttindexboldpos{-->}{$HOL0imp} &
39.39 +\verb$\<longrightarrow>$ \\
39.40 \indexboldpos{\isasymnot}{$HOL0not} &
39.41 +\verb$~$\index{$HOL0not@\verb$~$|bold} &
39.42 +\verb$\<not>$ \\
39.43 \indexboldpos{\isasymnoteq}{$HOL0noteq} &
39.44 +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
39.45 +\verb$\<noteq>$ \\
39.46 \indexboldpos{\isasymforall}{$HOL0All} &
39.47 -\isasymforall &
39.48 +\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
39.49 +\verb$\<forall>$ \\
39.50 \indexboldpos{\isasymexists}{$HOL0Ex} &
39.51 -\isasymexists &
39.52 +\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
39.53 +\verb$\<exists>$ \\
39.54 \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
39.55 -\isasymuniqex \\
39.56 -\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
39.57 -\texttt{|}\index{$HOL0or@\ttor|bold} &
39.58 -\ttindexboldpos{-->}{$HOL0imp} &
39.59 -\verb$~$\index{$HOL0not@\verb$~$|bold} &
39.60 -\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
39.61 -\ttindexbold{ALL} &
39.62 -\texttt{!}\index{$HOL0All@\ttall|bold} &
39.63 -\ttindexbold{EX} &
39.64 -\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
39.65 -\ttEXU\index{EXX@\ttEXU|bold} &
39.66 -\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
39.67 -\hline\hline
39.68 -\indexboldpos{\isasymlbrakk}{$Isabrl} &
39.69 -\indexboldpos{\isasymrbrakk}{$Isabrr} &
39.70 -\indexboldpos{\isasymImp}{$IsaImp} &
39.71 -\indexboldpos{\isasymAnd}{$IsaAnd} &
39.72 -\indexboldpos{\isasymequiv}{$IsaEq} &
39.73 -\indexboldpos{\isasymlambda}{$Isalam} &
39.74 -\indexboldpos{\isasymFun}{$IsaFun}&
39.75 -&
39.76 -&
39.77 -&
39.78 -\\
39.79 -\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
39.80 -\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
39.81 -\ttindexboldpos{==>}{$IsaImp} &
39.82 -\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
39.83 -\ttindexboldpos{==}{$IsaEq} &
39.84 -\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
39.85 -\ttindexboldpos{=>}{$IsaFun}&
39.86 -&
39.87 -&
39.88 -&
39.89 - \\
39.90 -\hline\hline
39.91 +\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
39.92 +\verb$\<exists>!$\\
39.93 +\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
39.94 +\ttindexbold{SOME} &
39.95 +\verb$\<?>$\\
39.96 \indexboldpos{\isasymcirc}{$HOL1} &
39.97 +\ttindexbold{o} &
39.98 +\verb$\<?>$\\
39.99 \indexboldpos{\isasymle}{$HOL2arithrel}&
39.100 +\ttindexboldpos{<=}{$HOL2arithrel}&
39.101 +\verb$\<le>$\\
39.102 \indexboldpos{\isasymtimes}{$IsaFun}&
39.103 -&
39.104 -&
39.105 -&
39.106 -&
39.107 -&
39.108 -&
39.109 -&
39.110 - \\
39.111 -\ttindexbold{o} &
39.112 -\ttindexboldpos{<=}{$HOL2arithrel}&
39.113 \ttindexboldpos{*}{$HOL2arithfun} &
39.114 -&
39.115 -&
39.116 -&
39.117 -&
39.118 -&
39.119 -&
39.120 -&
39.121 -\\
39.122 +\verb$\<times>$\\
39.123 +\indexboldpos{\isasymin}{$HOL3Set}&
39.124 +\ttindexboldpos{:}{$HOL3Set} &
39.125 +\verb$\<in>$\\
39.126 +? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
39.127 +\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
39.128 +\verb$\<notin>$\\
39.129 +\indexboldpos{\isasymsubseteq}{$HOL3Set}&
39.130 +\verb$<=$ &
39.131 +\verb$\<subseteq>$\\
39.132 +\indexboldpos{\isasymunion}{$HOL3Set}&
39.133 +\ttindexbold{Un} &
39.134 +\verb$\<union>$\\
39.135 +\indexboldpos{\isasyminter}{$HOL3Set}&
39.136 +\ttindexbold{Int} &
39.137 +\verb$\<inter>$\\
39.138 +\indexboldpos{\isasymUnion}{$HOL3Set}&
39.139 +\ttindexbold{UN}, \ttindexbold{Union} &
39.140 +\verb$\<Union>$\\
39.141 +\indexboldpos{\isasymInter}{$HOL3Set}&
39.142 +\ttindexbold{INT}, \ttindexbold{Inter} &
39.143 +\verb$\<Inter>$\\
39.144 \hline
39.145 \end{tabular}
39.146 \end{center}
39.147 -\caption{Mathematical symbols and their ASCII-equivalents}
39.148 +\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
39.149 \label{fig:ascii}
39.150 \end{figure}\indexbold{ASCII symbols}
39.151
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}