--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Sep 12 15:43:15 2000 +0200
@@ -111,11 +111,11 @@
text{*\noindent
Note that because \isaindex{auto} performs simplification, it can
-also be modified in the same way @{text"simp"} can. Thus the proof can be
+also be modified in the same way @{text simp} can. Thus the proof can be
rewritten as
*}
(*<*)
-lemmas [simp del] = exec_app;
+declare exec_app[simp del];
lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
(*>*)
by(induct_tac xs, auto split: instr.split);
--- a/doc-src/TutorialI/Datatype/Fundata.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Tue Sep 12 15:43:15 2000 +0200
@@ -1,7 +1,7 @@
(*<*)
theory Fundata = Main:
(*>*)
-datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
+datatype ('a,'i)bigtree = Tip | Branch 'a "'i \<Rightarrow> ('a,'i)bigtree"
text{*\noindent
Parameter @{typ"'a"} is the type of values stored in
@@ -19,10 +19,10 @@
Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
*}
-consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
+consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
primrec
"map_bt f Tip = Tip"
-"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
+"map_bt f (Branch a F) = Branch (f a) (\<lambda>i. map_bt f (F i))"
text{*\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of @{term"map_bt"} involve only subtrees obtained from
@@ -35,16 +35,18 @@
The following lemma has a canonical proof *}
lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
-by(induct_tac "T", simp_all)
+by(induct_tac T, simp_all)
text{*\noindent
+%apply(induct_tac T);
+%pr(latex xsymbols symbols)
but it is worth taking a look at the proof state after the induction step
to understand what the presence of the function type entails:
\begin{isabelle}
-~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
-~2.~{\isasymAnd}a~F.\isanewline
-~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
-~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
+\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
+\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
\end{isabelle}
*}
(*<*)
--- a/doc-src/TutorialI/Datatype/Nested.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Tue Sep 12 15:43:15 2000 +0200
@@ -8,7 +8,7 @@
constructor. This is not the case any longer for the following model of terms
where function symbols can be applied to a list of arguments:
*}
-
+(*<*)hide const Var(*>*)
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
text{*\noindent
@@ -53,7 +53,7 @@
"substs s (t # ts) = subst s t # substs s ts";
text{*\noindent
-You should ignore the label @{thm[source]subst_App} for the moment.
+(Please ignore the label @{thm[source]subst_App} for the moment.)
Similarly, when proving a statement about terms inductively, we need
to prove a related statement about term lists simultaneously. For example,
@@ -105,7 +105,7 @@
simplification rule:
*}
-lemmas [simp del] = subst_App
+declare subst_App [simp del]
text{*\noindent
The advantage is that now we have replaced @{term"substs"} by
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Sep 12 15:43:15 2000 +0200
@@ -36,16 +36,18 @@
The following lemma has a canonical proof%
\end{isamarkuptext}%
\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
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
+%apply(induct_tac T);
+%pr(latex xsymbols symbols)
but it is worth taking a look at the proof state after the induction step
to understand what the presence of the function type entails:
\begin{isabelle}
-~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
-~2.~{\isasymAnd}a~F.\isanewline
-~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
-~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
+\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
+\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
\end{isabelle}%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Sep 12 15:43:15 2000 +0200
@@ -15,7 +15,7 @@
the command \isacommand{term}.
Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
function symbols.
-A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}term{\isachardot}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}term{\isachardot}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
suitable values, e.g.\ numbers or strings.
What complicates the definition of \isa{term} is the nested occurrence of
@@ -50,7 +50,7 @@
\ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-You should ignore the label \isa{subst{\isacharunderscore}App} for the moment.
+(Please ignore the label \isa{subst{\isacharunderscore}App} for the moment.)
Similarly, when proving a statement about terms inductively, we need
to prove a related statement about term lists simultaneously. For example,
@@ -62,8 +62,8 @@
\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-Note that \isa{term{\isachardot}Var} is the identity substitution because by definition it
-leaves variables unchanged: \isa{subst\ term{\isachardot}Var\ {\isacharparenleft}term{\isachardot}Var\ x{\isacharparenright}\ {\isacharequal}\ term{\isachardot}Var\ x}. Note also
+Note that \isa{Var} is the identity substitution because by definition it
+leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
that the type annotations are necessary because otherwise there is nothing in
the goal to enforce that both halves of the goal talk about the same type
parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
@@ -103,7 +103,7 @@
What is more, we can now disable the old defining equation as a
simplification rule:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ subst{\isacharunderscore}App%
+\isacommand{declare}\ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
\begin{isamarkuptext}%
\noindent
The advantage is that now we have replaced \isa{substs} by
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Tue Sep 12 15:43:15 2000 +0200
@@ -2,9 +2,17 @@
theory Ifexpr = Main:;
(*>*)
+subsection{*Case study: boolean expressions*}
+
+text{*\label{sec:boolex}
+The aim of this case study is twofold: it shows how to model boolean
+expressions and some algorithms for manipulating them, and it demonstrates
+the constructs introduced above.
+*}
+
+subsubsection{*How can we model boolean expressions?*}
+
text{*
-\subsubsection{How can we model boolean expressions?}
-
We want to represent boolean expressions built up from variables and
constants by negation and conjunction. The following datatype serves exactly
that purpose:
@@ -161,6 +169,23 @@
theorem "normal(norm b)";
apply(induct_tac b);
by(auto);
+(*>*)
+text{*\medskip
+How does one come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what @{text auto} leaves unproved. This has
+to provide the clue. The necessity of universal quantification
+(@{text"\<forall>t e"}) in the two lemmas is explained in
+\S\ref{sec:InductionHeuristics}
+
+\begin{exercise}
+ We strengthen the definition of a @{term normal} If-expression as follows:
+ the first argument of all @{term IF}s must be a variable. Adapt the above
+ development to this changed requirement. (Hint: you may need to formulate
+ some of the goals as implications (@{text"\<longrightarrow>"}) rather than
+ equalities (@{text"="}).)
+\end{exercise}
+*}
+(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Sep 12 15:43:15 2000 +0200
@@ -2,9 +2,18 @@
\begin{isabellebody}%
\def\isabellecontext{Ifexpr}%
%
+\isamarkupsubsection{Case study: boolean expressions}
+%
\begin{isamarkuptext}%
-\subsubsection{How can we model boolean expressions?}
-
+\label{sec:boolex}
+The aim of this case study is twofold: it shows how to model boolean
+expressions and some algorithms for manipulating them, and it demonstrates
+the constructs introduced above.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{How can we model boolean expressions?}
+%
+\begin{isamarkuptext}%
We want to represent boolean expressions built up from variables and
constants by negation and conjunction. The following datatype serves exactly
that purpose:%
@@ -133,7 +142,24 @@
and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
-\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\medskip
+How does one come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what \isa{auto} leaves unproved. This has
+to provide the clue. The necessity of universal quantification
+(\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
+\S\ref{sec:InductionHeuristics}
+
+\begin{exercise}
+ We strengthen the definition of a \isa{normal} If-expression as follows:
+ the first argument of all \isa{IF}s must be a variable. Adapt the above
+ development to this changed requirement. (Hint: you may need to formulate
+ some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
+ equalities (\isa{{\isacharequal}}).)
+\end{exercise}%
+\end{isamarkuptext}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/IsaMakefile Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Tue Sep 12 15:43:15 2000 +0200
@@ -4,7 +4,7 @@
## targets
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc styles
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Misc styles
images:
test:
all: default
@@ -93,6 +93,14 @@
@rm -f tutorial.dvi
+## HOL-Advanced
+
+HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
+
+$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
+ @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
+ @rm -f tutorial.dvi
+
## HOL-Misc
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
@@ -109,4 +117,4 @@
## clean
clean:
- @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz
+ @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 15:43:15 2000 +0200
@@ -17,7 +17,7 @@
that is amenable to induction, but this is not always the case:
*};
-lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) = last xs";
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";
apply(induct_tac xs);
txt{*\noindent
@@ -49,7 +49,7 @@
This means we should prove
*};
(*<*)oops;(*>*)
-lemma hd_rev: "xs \\<noteq> [] \\<longrightarrow> hd(rev xs) = last xs";
+lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
(*<*)
by(induct_tac xs, auto);
(*>*)
@@ -82,7 +82,7 @@
Here is a simple example (which is proved by @{text"blast"}):
*};
-lemma simple: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)by blast;(*>*)
text{*\noindent
@@ -105,7 +105,7 @@
statement of your original lemma, thus avoiding the intermediate step:
*};
-lemma myrule[rulified]: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rulified]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)
by blast;
(*>*)
@@ -134,8 +134,8 @@
Structural induction on @{typ"nat"} is
usually known as ``mathematical induction''. There is also ``complete
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem @{thm [source] nat_less_induct}:
-@{thm[display] nat_less_induct [no_vars]}
+holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
+@{thm[display]"nat_less_induct"[no_vars]}
Here is an example of its application.
*};
@@ -152,10 +152,10 @@
above, we have to phrase the proposition as follows to allow induction:
*};
-lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
+lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
txt{*\noindent
-To perform induction on @{term"k"} using @{thm [source] nat_less_induct}, we use the same
+To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same
general induction method as for recursion induction (see
\S\ref{sec:recdef-induction}):
*};
@@ -213,7 +213,7 @@
we could have included this derivation in the original statement of the lemma:
*};
-lemma f_incr[rulified, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
+lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
(*<*)oops;(*>*)
text{*
@@ -242,49 +242,46 @@
text{*\label{sec:derive-ind}
Induction schemas are ordinary theorems and you can derive new ones
whenever you wish. This section shows you how to, using the example
-of @{thm [source] nat_less_induct}. Assume we only have structural induction
+of @{thm[source]nat_less_induct}. Assume we only have structural induction
available for @{typ"nat"} and want to derive complete induction. This
requires us to generalize the statement first:
*};
-lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> \\<forall>m<n. P m";
+lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
apply(induct_tac n);
txt{*\noindent
The base case is trivially true. For the induction step (@{prop"m <
-Suc n"}) we distinguish two cases: @{prop"m < n"} is true by induction
-hypothesis and @{prop"m = n"} follow from the assumption again using
+Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
+hypothesis and case @{prop"m = n"} follows from the assumption, again using
the induction hypothesis:
*};
-
apply(blast);
-(* apply(blast elim:less_SucE); *)
-ML"set quick_and_dirty"
-sorry;
-ML"reset quick_and_dirty"
+by(blast elim:less_SucE)
text{*\noindent
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
@{thm[display]"less_SucE"[no_vars]}
Now it is straightforward to derive the original version of
-@{thm [source] nat_less_induct} by manipulting the conclusion of the above lemma:
+@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:
*};
-theorem nat_less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
+theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
by(insert induct_lem, blast);
-text{*\noindent
+text{*
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
@{thm[display]"wf_induct"[no_vars]}
where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
-For example @{thm [source] nat_less_induct} is the special case where @{term"r"} is
-@{text"<"} on @{typ"nat"}. For details see the library.
+For example, theorem @{thm[source]nat_less_induct} can be viewed (and
+derived) as a special case of @{thm[source]wf_induct} where
+@{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.
*};
(*<*)
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Sep 12 15:43:15 2000 +0200
@@ -227,15 +227,12 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-The base case is trivially true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: \isa{m\ {\isacharless}\ n} is true by induction
-hypothesis and \isa{m\ {\isacharequal}\ n} follow from the assumption again using
+The base case is trivially true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
+hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
the induction hypothesis:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isanewline
-\isacommand{ML}{\isachardoublequote}set\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}\isanewline
-\isacommand{sorry}\isanewline
-\isacommand{ML}{\isachardoublequote}reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}%
+\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
@@ -253,15 +250,15 @@
\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
-\noindent
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}
where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
-For example \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is the special case where \isa{r} is
-\isa{{\isacharless}} on \isa{nat}. For details see the library.%
+For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
+derived) as a special case of \isa{wf{\isacharunderscore}induct} where
+\isa{r} is \isa{{\isacharless}} on \isa{nat}. For details see the library.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Sep 12 15:43:15 2000 +0200
@@ -3,13 +3,14 @@
\def\isabellecontext{pairs}%
%
\begin{isamarkuptext}%
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
- $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
-are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
-\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
-\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
-\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
- $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
+\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by \isa{fst} and
+\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
+for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
+$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
+\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
It is possible to use (nested) tuples as patterns in abstractions, for
example \isa{\isasymlambda(x,y,z).x+y+z} and
--- a/doc-src/TutorialI/Misc/document/simp.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Sep 12 15:43:15 2000 +0200
@@ -1,10 +1,376 @@
%
\begin{isabellebody}%
\def\isabellecontext{simp}%
-\isanewline
-\isacommand{theory}\ simp\ {\isacharequal}\ Main{\isacharcolon}\isanewline
-\isanewline
-\isacommand{end}\isanewline
+%
+\isamarkupsubsubsection{Simplification rules}
+%
+\begin{isamarkuptext}%
+\indexbold{simplification rule}
+To facilitate simplification, theorems can be declared to be simplification
+rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp
+ (attribute)}), in which case proofs by simplification make use of these
+rules automatically. In addition the constructs \isacommand{datatype} and
+\isacommand{primrec} (and a few others) invisibly declare useful
+simplification rules. Explicit definitions are \emph{not} declared
+simplification rules automatically!
+
+Not merely equations but pretty much any theorem can become a simplification
+rule. The simplifier will try to make sense of it. For example, a theorem
+\isa{{\isasymnot}\ P} is automatically turned into \isa{P\ {\isacharequal}\ False}. The details
+are explained in \S\ref{sec:SimpHow}.
+
+The simplification attribute of theorems can be turned on and off as follows:
+\begin{quote}
+\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
+\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
+\end{quote}
+As a rule of thumb, equations that really simplify (like \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}) should be made simplification
+rules. Those of a more specific nature (e.g.\ distributivity laws, which
+alter the structure of terms considerably) should only be used selectively,
+i.e.\ they should not be default simplification rules. Conversely, it may
+also happen that a simplification rule needs to be disabled in certain
+proofs. Frequent changes in the simplification status of a theorem may
+indicate a badly designed theory.
+\begin{warn}
+ Simplification may not terminate, for example if both $f(x) = g(x)$ and
+ $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
+ to include simplification rules that can lead to nontermination, either on
+ their own or in combination with other simplification rules.
+\end{warn}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{The simplification method}
+%
+\begin{isamarkuptext}%
+\index{*simp (method)|bold}
+The general format of the simplification method is
+\begin{quote}
+\isa{simp} \textit{list of modifiers}
+\end{quote}
+where the list of \emph{modifiers} helps to fine tune the behaviour and may
+be empty. Most if not all of the proofs seen so far could have been performed
+with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
+only the first subgoal and may thus need to be repeated---use
+\isaindex{simp_all} to simplify all subgoals.
+Note that \isa{simp} fails if nothing changes.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Adding and deleting simplification rules}
+%
+\begin{isamarkuptext}%
+If a certain theorem is merely needed in a few proofs by simplification,
+we do not need to make it a global simplification rule. Instead we can modify
+the set of simplification rules used in a simplification step by adding rules
+to it and/or deleting rules from it. The two modifiers for this are
+\begin{quote}
+\isa{add{\isacharcolon}} \textit{list of theorem names}\\
+\isa{del{\isacharcolon}} \textit{list of theorem names}
+\end{quote}
+In case you want to use only a specific list of theorems and ignore all
+others:
+\begin{quote}
+\isa{only{\isacharcolon}} \textit{list of theorem names}
+\end{quote}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Assumptions}
+%
+\begin{isamarkuptext}%
+\index{simplification!with/of assumptions}
+By default, assumptions are part of the simplification process: they are used
+as simplification rules and are simplified themselves. For example:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\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
+\isacommand{by}\ simp%
+\begin{isamarkuptext}%
+\noindent
+The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
+simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
+conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
+
+In some cases this may be too much of a good thing and may lead to
+nontermination:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+cannot be solved by an unmodified application of \isa{simp} because the
+simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
+does not terminate. Isabelle notices certain simple forms of
+nontermination but not this one. The problem can be circumvented by
+explicitly telling the simplifier to ignore the assumptions:%
+\end{isamarkuptxt}%
+\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+There are three options that influence the treatment of assumptions:
+\begin{description}
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
+ means that assumptions are completely ignored.
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
+ means that the assumptions are not simplified but
+ are used in the simplification of the conclusion.
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
+ means that the assumptions are simplified but are not
+ used in the simplification of each other or the conclusion.
+\end{description}
+Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
+the above problematic subgoal.
+
+Note that only one of the above options is allowed, and it must precede all
+other arguments.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Rewriting with definitions}
+%
+\begin{isamarkuptext}%
+\index{simplification!with definitions}
+Constant definitions (\S\ref{sec:ConstDefinitions}) can
+be used as simplification rules, but by default they are not. Hence the
+simplifier does not expand them automatically, just as it should be:
+definitions are introduced for the purpose of abbreviating complex
+concepts. Of course we need to expand the definitions initially to derive
+enough lemmas that characterize the concept sufficiently for us to forget the
+original definition. For example, given%
+\end{isamarkuptext}%
+\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+we may want to prove%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
+get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+In this particular case, the resulting goal
+\begin{isabelle}
+~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
+\end{isabelle}
+can be proved by simplification. Thus we could have proved the lemma outright%
+\end{isamarkuptxt}%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Of course we can also unfold definitions in the middle of a proof.
+
+You should normally not turn a definition permanently into a simplification
+rule because this defeats the whole purpose of an abbreviation.
+
+\begin{warn}
+ If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
+ occurrences of $f$ with at least two arguments. Thus it is safer to define
+ $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
+\end{warn}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Simplifying let-expressions}
+%
+\begin{isamarkuptext}%
+\index{simplification!of let-expressions}
+Proving a goal containing \isaindex{let}-expressions almost invariably
+requires the \isa{let}-con\-structs to be expanded at some point. Since
+\isa{let}-\isa{in} is just syntactic sugar for a predefined constant
+(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
+\isa{Let{\isacharunderscore}def}:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptext}%
+If, in a particular context, there is no danger of a combinatorial explosion
+of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
+default:%
+\end{isamarkuptext}%
+\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
+\isamarkupsubsubsection{Conditional equations}
+%
+\begin{isamarkuptext}%
+So far all examples of rewrite rules were equations. The simplifier also
+accepts \emph{conditional} equations, for example%
+\end{isamarkuptext}%
+\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
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
+sequence of methods. Assuming that the simplification rule
+\isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
+is present as well,%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+is proved by plain simplification:
+the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
+can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
+because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
+simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
+assumption of the subgoal.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Automatic case splits}
+%
+\begin{isamarkuptext}%
+\indexbold{case splits}\index{*split|(}
+Goals containing \isa{if}-expressions are usually proved by case
+distinction on the condition of the \isa{if}. For example the goal%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+can be split into
+\begin{isabelle}
+~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
+\end{isabelle}
+by a degenerate form of simplification%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
+empty list of theorems) but the rule \isaindexbold{split_if} for
+splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
+case-splitting on \isa{if}s is almost always the right proof strategy, the
+simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
+on the initial goal above.
+
+This splitting idea generalizes from \isa{if} to \isaindex{case}:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+becomes
+\begin{isabelle}\makeatother
+~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
+~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
+\end{isabelle}
+by typing%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+In contrast to \isa{if}-expressions, the simplifier does not split
+\isa{case}-expressions by default because this can lead to nontermination
+in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
+dropped, the above goal is solved,%
+\end{isamarkuptext}%
+\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent%
+which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
+
+In general, every datatype $t$ comes with a theorem
+$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
+locally as above, or by giving it the \isa{split} attribute globally:%
+\end{isamarkuptext}%
+\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}%
+\begin{isamarkuptext}%
+\noindent
+The \isa{split} attribute can be removed with the \isa{del} modifier,
+either locally%
+\end{isamarkuptext}%
+\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+or globally:%
+\end{isamarkuptext}%
+\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}%
+\begin{isamarkuptext}%
+The above split rules intentionally only affect the conclusion of a
+subgoal. If you want to split an \isa{if} or \isa{case}-expression in
+the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
+$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+In contrast to splitting the conclusion, this actually creates two
+separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
+\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
+\end{isabelle}
+If you need to split both in the assumptions and the conclusion,
+use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
+$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.
+
+\begin{warn}
+ The simplifier merely simplifies the condition of an \isa{if} but not the
+ \isa{then} or \isa{else} parts. The latter are simplified only after the
+ condition reduces to \isa{True} or \isa{False}, or after splitting. The
+ same is true for \isaindex{case}-expressions: only the selector is
+ simplified at first, until either the expression reduces to one of the
+ cases or it is split.
+\end{warn}
+
+\index{*split|)}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Arithmetic}
+%
+\begin{isamarkuptext}%
+\index{arithmetic}
+The simplifier routinely solves a small class of linear arithmetic formulae
+(over type \isa{nat} and other numeric types): it only takes into account
+assumptions and conclusions that are (possibly negated) (in)equalities
+(\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+is proved by simplification, whereas the only slightly more complex%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+is not proved by simplification and requires \isa{arith}.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Tracing}
+%
+\begin{isamarkuptext}%
+\indexbold{tracing the simplifier}
+Using the simplifier effectively may take a bit of experimentation. Set the
+\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+on:%
+\end{isamarkuptext}%
+\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+produces the trace
+
+\begin{ttbox}\makeatother
+Applying instance of rewrite rule:
+rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
+Rewriting:
+rev [x] == rev [] @ [x]
+Applying instance of rewrite rule:
+rev [] == []
+Rewriting:
+rev [] == []
+Applying instance of rewrite rule:
+[] @ ?y == ?y
+Rewriting:
+[] @ [x] == [x]
+Applying instance of rewrite rule:
+?x3 \# ?t3 = ?t3 == False
+Rewriting:
+[x] = [] == False
+\end{ttbox}
+
+In more complicated cases, the trace can be quite lenghty, especially since
+invocations of the simplifier are often nested (e.g.\ when solving conditions
+of rewrite rules). Thus it is advisable to reset it:%
+\end{isamarkuptext}%
+\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/types.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Sep 12 15:43:15 2000 +0200
@@ -3,7 +3,7 @@
\def\isabellecontext{types}%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
+\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent\indexbold{*types}%
Internally all synonyms are fully expanded. As a consequence Isabelle's
--- a/doc-src/TutorialI/Misc/pairs.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Tue Sep 12 15:43:15 2000 +0200
@@ -2,13 +2,14 @@
theory pairs = Main:;
(*>*)
text{*
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
- $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
-are extracted by @{term"fst"} and @{term"snd"}: \isa{fst($x$,$y$) = $x$} and
-\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
-\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
-\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
- $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
+\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by @{term"fst"} and
+@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
+for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
+$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
+\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
It is possible to use (nested) tuples as patterns in abstractions, for
example \isa{\isasymlambda(x,y,z).x+y+z} and
--- a/doc-src/TutorialI/Misc/types.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Tue Sep 12 15:43:15 2000 +0200
@@ -1,8 +1,8 @@
(*<*)
theory "types" = Main:;
(*>*)types number = nat
- gate = "bool \\<Rightarrow> bool \\<Rightarrow> bool"
- ('a,'b)alist = "('a * 'b)list";
+ gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
+ ('a,'b)alist = "('a \<times> 'b)list";
text{*\noindent\indexbold{*types}%
Internally all synonyms are fully expanded. As a consequence Isabelle's
@@ -23,8 +23,8 @@
therefore be defined directly by
*}
-defs nand_def: "nand A B \\<equiv> \\<not>(A \\<and> B)"
- exor_def: "exor A B \\<equiv> A \\<and> \\<not>B \\<or> \\<not>A \\<and> B";
+defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
+ exor_def: "exor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
text{*\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and
@@ -35,9 +35,9 @@
*}
constdefs nor :: gate
- "nor A B \\<equiv> \\<not>(A \\<or> B)"
+ "nor A B \<equiv> \<not>(A \<or> B)"
exor2 :: gate
- "exor2 A B \\<equiv> (A \\<or> B) \\<and> (\\<not>A \\<or> \\<not>B)";
+ "exor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
text{*\noindent\indexbold{*constdefs}%
in which case the default name of each definition is $f$@{text"_def"}, where
--- a/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 12 15:43:15 2000 +0200
@@ -23,9 +23,9 @@
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-where @{term"set"} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and @{text"term_list_size ::
-term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
+where @{term"set"} returns the set of elements of a list
+and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
+function automatically defined by Isabelle
(when @{text"term"} was defined). First we have to understand why the
recursive call of @{term"trev"} underneath @{term"map"} leads to the above
condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
--- a/doc-src/TutorialI/Recdef/Nested2.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue Sep 12 15:43:15 2000 +0200
@@ -23,7 +23,6 @@
@{term"trev"}:
*};
-lemmas [cong] = map_cong;
lemma "trev(trev t) = t";
apply(induct_tac t rule:trev.induct);
txt{*\noindent
@@ -32,12 +31,12 @@
both of which are solved by simplification:
*};
-by(simp_all add:rev_map sym[OF map_compose]);
+by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
text{*\noindent
If the proof of the induction step mystifies you, we recommend to go through
the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}.
+@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -84,5 +83,8 @@
congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
declaring a congruence rule for the simplifier does not make it
available to \isacommand{recdef}, and vice versa. This is intentional.
+%The simplifier's congruence rules cannot be used by recdef.
+%For example the weak congruence rules for if and case would prevent
+%recdef from generating sensible termination conditions.
*};
(*<*)end;(*>*)
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Sep 12 15:43:15 2000 +0200
@@ -24,8 +24,9 @@
\begin{isabelle}%
\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
\end{isabelle}
-where \isa{set} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
+where \isa{set} returns the set of elements of a list
+and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
+function automatically defined by Isabelle
(when \isa{term} was defined). First we have to understand why the
recursive call of \isa{trev} underneath \isa{map} leads to the above
condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 15:43:15 2000 +0200
@@ -17,7 +17,6 @@
induction schema for type \isa{term} but the simpler one arising from
\isa{trev}:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
\isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -29,12 +28,12 @@
\end{isabelle}
both of which are solved by simplification:%
\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
If the proof of the induction step mystifies you, we recommend to go through
the chain of simplification steps in detail; you will probably need the help of
-\isa{trace{\isacharunderscore}simp}.
+\isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -82,7 +81,10 @@
Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
declaring a congruence rule for the simplifier does not make it
-available to \isacommand{recdef}, and vice versa. This is intentional.%
+available to \isacommand{recdef}, and vice versa. This is intentional.
+%The simplifier's congruence rules cannot be used by recdef.
+%For example the weak congruence rules for if and case would prevent
+%recdef from generating sensible termination conditions.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Sep 12 15:43:15 2000 +0200
@@ -24,7 +24,7 @@
Slightly more interesting is the insertion of a fixed element
between any two elements of a list:%
\end{isamarkuptext}%
-\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
\isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
@@ -44,7 +44,7 @@
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:%
\end{isamarkuptext}%
-\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Sep 12 15:43:15 2000 +0200
@@ -10,7 +10,7 @@
terminate because of automatic splitting of \isa{if}.
Let us look at an example:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}\isadigit{0}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
@@ -54,7 +54,7 @@
rather than \isa{if} on the right. In the case of \isa{gcd} the
following alternative definition suggests itself:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ gcd\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd\isadigit{1}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
@@ -67,7 +67,7 @@
A very simple alternative is to replace \isa{if} by \isa{case}, which
is also available for \isa{bool} but is not split automatically:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ gcd\isadigit{2}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}gcd\isadigit{2}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}\isadigit{0}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd\isadigit{2}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
@@ -85,7 +85,7 @@
\noindent
after which we can disable the original simplification rule:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
+\isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Sep 12 15:43:15 2000 +0200
@@ -17,7 +17,7 @@
(there is one for each recursive call) automatically. For example,
termination of the following artificial function%
\end{isamarkuptext}%
-\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
@@ -27,7 +27,7 @@
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:%
\end{isamarkuptext}%
-\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
+\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
It was not proved automatically because of the special nature of \isa{{\isacharminus}}
@@ -37,30 +37,30 @@
\begin{isamarkuptext}%
\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
-we have turned our lemma into a simplification rule. Therefore our second
-attempt to define our function will automatically take it into account:%
+we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
+a simplification rule:%
\end{isamarkuptext}%
-\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+{\isacharparenleft}\isakeyword{hints}\ simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
the stated recursion equation for \isa{g} and they are simplification
rules. Thus we can automatically prove%
\end{isamarkuptext}%
-\isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
More exciting theorems require induction, which is discussed below.
-Because lemma \isa{termi{\isacharunderscore}lem} above was only turned into a
-simplification rule for the sake of the termination proof, we may want to
-disable it again:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem%
-\begin{isamarkuptext}%
+If the termination proof requires a new lemma that is of general use, you can
+turn it permanently into a simplification rule, in which case the above
+\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
+sufficiently general to warrant this distinction.
+
The attentive reader may wonder why we chose to call our function \isa{g}
rather than \isa{f} the second time around. The reason is that, despite
the failed termination proof, the definition of \isa{f} did not
@@ -79,7 +79,7 @@
allows arbitrary wellfounded relations. For example, termination of
Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
\end{isamarkuptext}%
-\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Recdef/examples.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Tue Sep 12 15:43:15 2000 +0200
@@ -6,8 +6,8 @@
Here is a simple example, the Fibonacci function:
*}
-consts fib :: "nat \\<Rightarrow> nat";
-recdef fib "measure(\\<lambda>n. n)"
+consts fib :: "nat \<Rightarrow> nat";
+recdef fib "measure(\<lambda>n. n)"
"fib 0 = 0"
"fib 1 = 1"
"fib (Suc(Suc x)) = fib x + fib (Suc x)";
@@ -26,8 +26,8 @@
between any two elements of a list:
*}
-consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
-recdef sep "measure (\\<lambda>(a,xs). length xs)"
+consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
+recdef sep "measure (\<lambda>(a,xs). length xs)"
"sep(a, []) = []"
"sep(a, [x]) = [x]"
"sep(a, x#y#zs) = x # a # sep(a,y#zs)";
@@ -39,8 +39,8 @@
Pattern matching need not be exhaustive:
*}
-consts last :: "'a list \\<Rightarrow> 'a";
-recdef last "measure (\\<lambda>xs. length xs)"
+consts last :: "'a list \<Rightarrow> 'a";
+recdef last "measure (\<lambda>xs. length xs)"
"last [x] = x"
"last (x#y#zs) = last (y#zs)";
@@ -49,8 +49,8 @@
account, just as in functional programming:
*}
-consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
-recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
+consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
+recdef sep1 "measure (\<lambda>(a,xs). length xs)"
"sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
"sep1(a, xs) = xs";
@@ -67,17 +67,17 @@
arguments as in the following definition:
\end{warn}
*}
-consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
+consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
recdef sep2 "measure length"
- "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
- "sep2 xs = (\\<lambda>a. xs)";
+ "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
+ "sep2 xs = (\<lambda>a. xs)";
text{*
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
for the definition of non-recursive functions:
*}
-consts swap12 :: "'a list \\<Rightarrow> 'a list";
+consts swap12 :: "'a list \<Rightarrow> 'a list";
recdef swap12 "{}"
"swap12 (x#y#zs) = y#x#zs"
"swap12 zs = zs";
--- a/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 12 15:43:15 2000 +0200
@@ -11,7 +11,7 @@
Let us look at an example:
*}
-consts gcd :: "nat*nat \\<Rightarrow> nat";
+consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd "measure (\\<lambda>(m,n).n)"
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
@@ -48,7 +48,7 @@
following alternative definition suggests itself:
*}
-consts gcd1 :: "nat*nat \\<Rightarrow> nat";
+consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd1 "measure (\\<lambda>(m,n).n)"
"gcd1 (m, 0) = m"
"gcd1 (m, n) = gcd1(n, m mod n)";
@@ -63,7 +63,7 @@
is also available for @{typ"bool"} but is not split automatically:
*}
-consts gcd2 :: "nat*nat \\<Rightarrow> nat";
+consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd2 "measure (\\<lambda>(m,n).n)"
"gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
@@ -83,7 +83,7 @@
after which we can disable the original simplification rule:
*}
-lemmas [simp del] = gcd.simps;
+declare gcd.simps [simp del]
(*<*)
end
--- a/doc-src/TutorialI/Recdef/termination.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Tue Sep 12 15:43:15 2000 +0200
@@ -18,9 +18,9 @@
termination of the following artificial function
*}
-consts f :: "nat*nat \\<Rightarrow> nat";
-recdef f "measure(\\<lambda>(x,y). x-y)"
- "f(x,y) = (if x \\<le> y then x else f(x,y+1))";
+consts f :: "nat\<times>nat \<Rightarrow> nat";
+recdef f "measure(\<lambda>(x,y). x-y)"
+ "f(x,y) = (if x \<le> y then x else f(x,y+1))";
text{*\noindent
is not proved automatically (although maybe it should be). Isabelle prints a
@@ -29,7 +29,7 @@
of your function once more. In our case the required lemma is the obvious one:
*}
-lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
+lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
txt{*\noindent
It was not proved automatically because of the special nature of @{text"-"}
@@ -40,13 +40,14 @@
text{*\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
-we have turned our lemma into a simplification rule. Therefore our second
-attempt to define our function will automatically take it into account:
+we include with our second attempt the hint to use @{thm[source]termi_lem} as
+a simplification rule:
*}
-consts g :: "nat*nat \\<Rightarrow> nat";
-recdef g "measure(\\<lambda>(x,y). x-y)"
- "g(x,y) = (if x \\<le> y then x else g(x,y+1))";
+consts g :: "nat\<times>nat \<Rightarrow> nat";
+recdef g "measure(\<lambda>(x,y). x-y)"
+ "g(x,y) = (if x \<le> y then x else g(x,y+1))"
+(hints simp: termi_lem)
text{*\noindent
This time everything works fine. Now @{thm[source]g.simps} contains precisely
@@ -54,20 +55,17 @@
rules. Thus we can automatically prove
*}
-theorem wow: "g(1,0) = g(1,1)";
+theorem "g(1,0) = g(1,1)";
by(simp);
text{*\noindent
More exciting theorems require induction, which is discussed below.
-Because lemma @{thm[source]termi_lem} above was only turned into a
-simplification rule for the sake of the termination proof, we may want to
-disable it again:
-*}
+If the termination proof requires a new lemma that is of general use, you can
+turn it permanently into a simplification rule, in which case the above
+\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
+sufficiently general to warrant this distinction.
-lemmas [simp del] = termi_lem;
-
-text{*
The attentive reader may wonder why we chose to call our function @{term"g"}
rather than @{term"f"} the second time around. The reason is that, despite
the failed termination proof, the definition of @{term"f"} did not
@@ -87,7 +85,7 @@
Ackermann's function requires the lexicographic product @{text"<*lex*>"}:
*}
-consts ack :: "nat*nat \\<Rightarrow> nat";
+consts ack :: "nat\<times>nat \<Rightarrow> nat";
recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
"ack(0,n) = Suc n"
"ack(Suc m,0) = ack(m, 1)"
--- a/doc-src/TutorialI/Trie/Trie.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Tue Sep 12 15:43:15 2000 +0200
@@ -81,8 +81,7 @@
options:
*};
-lemmas [simp] = Let_def;
-lemmas [split] = option.split;
+declare Let_def[simp] option.split[split]
text{*\noindent
The reason becomes clear when looking (probably after a failed proof
--- a/doc-src/TutorialI/Trie/document/Trie.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Sep 12 15:43:15 2000 +0200
@@ -72,8 +72,7 @@
expand all \isa{let}s and to split all \isa{case}-constructs over
options:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline
-\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split%
+\isacommand{declare}\ Let{\isacharunderscore}def{\isacharbrackleft}simp{\isacharbrackright}\ option{\isachardot}split{\isacharbrackleft}split{\isacharbrackright}%
\begin{isamarkuptext}%
\noindent
The reason becomes clear when looking (probably after a failed proof
--- a/doc-src/TutorialI/appendix.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex Tue Sep 12 15:43:15 2000 +0200
@@ -55,7 +55,7 @@
\hline\hline
\indexboldpos{\isasymcirc}{$HOL1} &
\indexboldpos{\isasymle}{$HOL2arithrel}&
-&
+\indexboldpos{\isasymtimes}{$IsaFun}&
&
&
&
@@ -66,7 +66,7 @@
\\
\ttindexbold{o} &
\ttindexboldpos{<=}{$HOL2arithrel}&
-&
+\ttindexboldpos{*}{$HOL2arithfun} &
&
&
&
--- a/doc-src/TutorialI/basics.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/basics.tex Tue Sep 12 15:43:15 2000 +0200
@@ -73,7 +73,7 @@
\begin{warn}
HOL contains a theory \isaindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
- library). Unless you know what you are doing, always include \texttt{Main}
+ library). Unless you know what you are doing, always include \isa{Main}
as a direct or indirect parent theory of all your theories.
\end{warn}
--- a/doc-src/TutorialI/fp.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Tue Sep 12 15:43:15 2000 +0200
@@ -225,29 +225,7 @@
\end{warn}
-\subsection{Case study: boolean expressions}
-\label{sec:boolex}
-
-The aim of this case study is twofold: it shows how to model boolean
-expressions and some algorithms for manipulating them, and it demonstrates
-the constructs introduced above.
-
\input{Ifexpr/document/Ifexpr.tex}
-\medskip
-
-How does one come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what \isa{auto} leaves unproved. This has
-to provide the clue. The necessity of universal quantification
-(\isa{\isasymforall{}t e}) in the two lemmas is explained in
-\S\ref{sec:InductionHeuristics}
-
-\begin{exercise}
- We strengthen the definition of a \isa{normal} If-expression as follows:
- the first argument of all \isa{IF}s must be a variable. Adapt the above
- development to this changed requirement. (Hint: you may need to formulate
- some of the goals as implications (\isasymimp) rather than equalities
- (\isa{=}).)
-\end{exercise}
\section{Some basic types}
@@ -417,9 +395,10 @@
\begin{ttbox}\makeatother
(0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
\end{ttbox}
-This is also known as \bfindex{term rewriting} and the equations are referred
-to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
-because the terms do not necessarily become simpler in the process.
+This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
+equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
+``Rewriting'' is more honest than ``simplification'' because the terms do not
+necessarily become simpler in the process.
\input{Misc/document/simp.tex}
@@ -592,12 +571,4 @@
\index{induction!recursion|)}
\index{recursion induction|)}
-
-\subsection{Advanced forms of recursion}
-\label{sec:advanced-recdef}
-
-\input{Recdef/document/Nested0.tex}
-\input{Recdef/document/Nested1.tex}
-\input{Recdef/document/Nested2.tex}
-
\index{*recdef|)}
--- a/doc-src/TutorialI/tricks.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/tricks.tex Tue Sep 12 15:43:15 2000 +0200
@@ -1,36 +1,24 @@
-\chapter{The Tricks of the Trade}
-
-\section{Simplification}
-\label{sec:simplification-II}
-\index{simplification|(}
-
-\subsection{Advanced features}
-
-\subsubsection{Congruence rules}
-
-
-\subsubsection{Permutative rewrite rules}
+%\chapter{The Tricks of the Trade}
+\chapter{Advanced Simplification, Recursion, and Induction}
+\markboth{}{CHAPTER 4: ADVANCED}
-A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
-side are the same up to renaming of variables. The most common permutative
-rule is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$.
-Such rules are problematic because once they apply, they can be used forever.
-The simplifier is aware of this danger and treats permutative rules
-separately. For details see~\cite{isabelle-ref}.
-
-
+Although we have already learned a lot about simplification, recursion and
+induction, there are some advanced proof techniques that we have not covered
+yet and which are worth knowing about if you intend to beome a serious
+(human) theorem prover. The three sections of this chapter are almost
+independent of each other and can be read in any order. Only the notion of
+\emph{congruence rules}, introduced in the section on simplification, is
+required for parts of the section on recursion.
-\subsection{How it works}
-\label{sec:SimpHow}
-
-\subsubsection{Higher-order patterns}
+\input{Advanced/document/simp.tex}
-\subsubsection{Local assumptions}
-
-\subsubsection{The preprocessor}
-
-\index{simplification|)}
-
+\section{Advanced forms of recursion}
+\label{sec:advanced-recdef}
+\index{*recdef|(}
+\input{Recdef/document/Nested0.tex}
+\input{Recdef/document/Nested1.tex}
+\input{Recdef/document/Nested2.tex}
+\index{*recdef|)}
\section{Advanced induction techniques}
\label{sec:advanced-ind}