*** empty log message ***
authornipkow
Tue Sep 12 15:43:15 2000 +0200 (2000-09-12)
changeset 99339feb1e0c4cb3
parent 9932 5b6305cab436
child 9934 aea053733eb0
*** empty log message ***
doc-src/TutorialI/CodeGen/CodeGen.thy
doc-src/TutorialI/Datatype/Fundata.thy
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Misc/pairs.thy
doc-src/TutorialI/Misc/types.thy
doc-src/TutorialI/Recdef/Nested1.thy
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Nested1.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/examples.thy
doc-src/TutorialI/Recdef/simplification.thy
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tricks.tex
     1.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Sep 12 14:59:44 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Sep 12 15:43:15 2000 +0200
     1.3 @@ -111,11 +111,11 @@
     1.4  
     1.5  text{*\noindent
     1.6  Note that because \isaindex{auto} performs simplification, it can
     1.7 -also be modified in the same way @{text"simp"} can. Thus the proof can be
     1.8 +also be modified in the same way @{text simp} can. Thus the proof can be
     1.9  rewritten as
    1.10  *}
    1.11  (*<*)
    1.12 -lemmas [simp del] = exec_app;
    1.13 +declare exec_app[simp del];
    1.14  lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.15  (*>*)
    1.16  by(induct_tac xs, auto split: instr.split);
     2.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Tue Sep 12 14:59:44 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Tue Sep 12 15:43:15 2000 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*<*)
     2.5  theory Fundata = Main:
     2.6  (*>*)
     2.7 -datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
     2.8 +datatype ('a,'i)bigtree = Tip | Branch 'a "'i \<Rightarrow> ('a,'i)bigtree"
     2.9  
    2.10  text{*\noindent
    2.11  Parameter @{typ"'a"} is the type of values stored in
    2.12 @@ -19,10 +19,10 @@
    2.13  Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
    2.14  *}
    2.15  
    2.16 -consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
    2.17 +consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
    2.18  primrec
    2.19  "map_bt f Tip          = Tip"
    2.20 -"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
    2.21 +"map_bt f (Branch a F) = Branch (f a) (\<lambda>i. map_bt f (F i))"
    2.22  
    2.23  text{*\noindent This is a valid \isacommand{primrec} definition because the
    2.24  recursive calls of @{term"map_bt"} involve only subtrees obtained from
    2.25 @@ -35,16 +35,18 @@
    2.26  The following lemma has a canonical proof  *}
    2.27  
    2.28  lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
    2.29 -by(induct_tac "T", simp_all)
    2.30 +by(induct_tac T, simp_all)
    2.31  
    2.32  text{*\noindent
    2.33 +%apply(induct_tac T);
    2.34 +%pr(latex xsymbols symbols)
    2.35  but it is worth taking a look at the proof state after the induction step
    2.36  to understand what the presence of the function type entails:
    2.37  \begin{isabelle}
    2.38 -~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
    2.39 -~2.~{\isasymAnd}a~F.\isanewline
    2.40 -~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    2.41 -~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    2.42 +\ \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
    2.43 +\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
    2.44 +\ \ \ \ \ \ \ {\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
    2.45 +\ \ \ \ \ \ \ 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}
    2.46  \end{isabelle}
    2.47  *}
    2.48  (*<*)
     3.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Tue Sep 12 14:59:44 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Tue Sep 12 15:43:15 2000 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  constructor. This is not the case any longer for the following model of terms
     3.5  where function symbols can be applied to a list of arguments:
     3.6  *}
     3.7 -
     3.8 +(*<*)hide const Var(*>*)
     3.9  datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
    3.10  
    3.11  text{*\noindent
    3.12 @@ -53,7 +53,7 @@
    3.13    "substs s (t # ts) = subst s t # substs s ts";
    3.14  
    3.15  text{*\noindent
    3.16 -You should ignore the label @{thm[source]subst_App} for the moment.
    3.17 +(Please ignore the label @{thm[source]subst_App} for the moment.)
    3.18  
    3.19  Similarly, when proving a statement about terms inductively, we need
    3.20  to prove a related statement about term lists simultaneously. For example,
    3.21 @@ -105,7 +105,7 @@
    3.22  simplification rule:
    3.23  *}
    3.24  
    3.25 -lemmas [simp del] = subst_App
    3.26 +declare subst_App [simp del]
    3.27  
    3.28  text{*\noindent
    3.29  The advantage is that now we have replaced @{term"substs"} by
     4.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Sep 12 14:59:44 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Sep 12 15:43:15 2000 +0200
     4.3 @@ -36,16 +36,18 @@
     4.4  The following lemma has a canonical proof%
     4.5  \end{isamarkuptext}%
     4.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
     4.7 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
     4.8 +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
     4.9  \begin{isamarkuptext}%
    4.10  \noindent
    4.11 +%apply(induct_tac T);
    4.12 +%pr(latex xsymbols symbols)
    4.13  but it is worth taking a look at the proof state after the induction step
    4.14  to understand what the presence of the function type entails:
    4.15  \begin{isabelle}
    4.16 -~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
    4.17 -~2.~{\isasymAnd}a~F.\isanewline
    4.18 -~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    4.19 -~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    4.20 +\ \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
    4.21 +\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
    4.22 +\ \ \ \ \ \ \ {\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
    4.23 +\ \ \ \ \ \ \ 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}
    4.24  \end{isabelle}%
    4.25  \end{isamarkuptext}%
    4.26  \end{isabellebody}%
     5.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Sep 12 14:59:44 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Sep 12 15:43:15 2000 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  the command \isacommand{term}.
     5.5  Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
     5.6  function symbols.
     5.7 -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
     5.8 +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
     5.9  suitable values, e.g.\ numbers or strings.
    5.10  
    5.11  What complicates the definition of \isa{term} is the nested occurrence of
    5.12 @@ -50,7 +50,7 @@
    5.13  \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
    5.14  \begin{isamarkuptext}%
    5.15  \noindent
    5.16 -You should ignore the label \isa{subst{\isacharunderscore}App} for the moment.
    5.17 +(Please ignore the label \isa{subst{\isacharunderscore}App} for the moment.)
    5.18  
    5.19  Similarly, when proving a statement about terms inductively, we need
    5.20  to prove a related statement about term lists simultaneously. For example,
    5.21 @@ -62,8 +62,8 @@
    5.22  \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
    5.23  \begin{isamarkuptext}%
    5.24  \noindent
    5.25 -Note that \isa{term{\isachardot}Var} is the identity substitution because by definition it
    5.26 -leaves variables unchanged: \isa{subst\ term{\isachardot}Var\ {\isacharparenleft}term{\isachardot}Var\ x{\isacharparenright}\ {\isacharequal}\ term{\isachardot}Var\ x}. Note also
    5.27 +Note that \isa{Var} is the identity substitution because by definition it
    5.28 +leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
    5.29  that the type annotations are necessary because otherwise there is nothing in
    5.30  the goal to enforce that both halves of the goal talk about the same type
    5.31  parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
    5.32 @@ -103,7 +103,7 @@
    5.33  What is more, we can now disable the old defining equation as a
    5.34  simplification rule:%
    5.35  \end{isamarkuptext}%
    5.36 -\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ subst{\isacharunderscore}App%
    5.37 +\isacommand{declare}\ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
    5.38  \begin{isamarkuptext}%
    5.39  \noindent
    5.40  The advantage is that now we have replaced \isa{substs} by
     6.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Tue Sep 12 14:59:44 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Tue Sep 12 15:43:15 2000 +0200
     6.3 @@ -2,9 +2,17 @@
     6.4  theory Ifexpr = Main:;
     6.5  (*>*)
     6.6  
     6.7 +subsection{*Case study: boolean expressions*}
     6.8 +
     6.9 +text{*\label{sec:boolex}
    6.10 +The aim of this case study is twofold: it shows how to model boolean
    6.11 +expressions and some algorithms for manipulating them, and it demonstrates
    6.12 +the constructs introduced above.
    6.13 +*}
    6.14 +
    6.15 +subsubsection{*How can we model boolean expressions?*}
    6.16 +
    6.17  text{*
    6.18 -\subsubsection{How can we model boolean expressions?}
    6.19 -
    6.20  We want to represent boolean expressions built up from variables and
    6.21  constants by negation and conjunction. The following datatype serves exactly
    6.22  that purpose:
    6.23 @@ -161,6 +169,23 @@
    6.24  theorem "normal(norm b)";
    6.25  apply(induct_tac b);
    6.26  by(auto);
    6.27 +(*>*)
    6.28  
    6.29 +text{*\medskip
    6.30 +How does one come up with the required lemmas? Try to prove the main theorems
    6.31 +without them and study carefully what @{text auto} leaves unproved. This has
    6.32 +to provide the clue.  The necessity of universal quantification
    6.33 +(@{text"\<forall>t e"}) in the two lemmas is explained in
    6.34 +\S\ref{sec:InductionHeuristics}
    6.35 +
    6.36 +\begin{exercise}
    6.37 +  We strengthen the definition of a @{term normal} If-expression as follows:
    6.38 +  the first argument of all @{term IF}s must be a variable. Adapt the above
    6.39 +  development to this changed requirement. (Hint: you may need to formulate
    6.40 +  some of the goals as implications (@{text"\<longrightarrow>"}) rather than
    6.41 +  equalities (@{text"="}).)
    6.42 +\end{exercise}
    6.43 +*}
    6.44 +(*<*)
    6.45  end
    6.46  (*>*)
     7.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Sep 12 14:59:44 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Sep 12 15:43:15 2000 +0200
     7.3 @@ -2,9 +2,18 @@
     7.4  \begin{isabellebody}%
     7.5  \def\isabellecontext{Ifexpr}%
     7.6  %
     7.7 +\isamarkupsubsection{Case study: boolean expressions}
     7.8 +%
     7.9  \begin{isamarkuptext}%
    7.10 -\subsubsection{How can we model boolean expressions?}
    7.11 -
    7.12 +\label{sec:boolex}
    7.13 +The aim of this case study is twofold: it shows how to model boolean
    7.14 +expressions and some algorithms for manipulating them, and it demonstrates
    7.15 +the constructs introduced above.%
    7.16 +\end{isamarkuptext}%
    7.17 +%
    7.18 +\isamarkupsubsubsection{How can we model boolean expressions?}
    7.19 +%
    7.20 +\begin{isamarkuptext}%
    7.21  We want to represent boolean expressions built up from variables and
    7.22  constants by negation and conjunction. The following datatype serves exactly
    7.23  that purpose:%
    7.24 @@ -133,7 +142,24 @@
    7.25  and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
    7.26  normality of \isa{normif}:%
    7.27  \end{isamarkuptext}%
    7.28 -\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}%
    7.29 +\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}%
    7.30 +\begin{isamarkuptext}%
    7.31 +\medskip
    7.32 +How does one come up with the required lemmas? Try to prove the main theorems
    7.33 +without them and study carefully what \isa{auto} leaves unproved. This has
    7.34 +to provide the clue.  The necessity of universal quantification
    7.35 +(\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
    7.36 +\S\ref{sec:InductionHeuristics}
    7.37 +
    7.38 +\begin{exercise}
    7.39 +  We strengthen the definition of a \isa{normal} If-expression as follows:
    7.40 +  the first argument of all \isa{IF}s must be a variable. Adapt the above
    7.41 +  development to this changed requirement. (Hint: you may need to formulate
    7.42 +  some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
    7.43 +  equalities (\isa{{\isacharequal}}).)
    7.44 +\end{exercise}%
    7.45 +\end{isamarkuptext}%
    7.46 +\end{isabellebody}%
    7.47  %%% Local Variables:
    7.48  %%% mode: latex
    7.49  %%% TeX-master: "root"
     8.1 --- a/doc-src/TutorialI/IsaMakefile	Tue Sep 12 14:59:44 2000 +0200
     8.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Sep 12 15:43:15 2000 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  
     8.5  ## targets
     8.6  
     8.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc styles
     8.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Misc styles
     8.9  images:
    8.10  test:
    8.11  all: default
    8.12 @@ -93,6 +93,14 @@
    8.13  	@rm -f tutorial.dvi
    8.14  
    8.15  
    8.16 +## HOL-Advanced
    8.17 +
    8.18 +HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
    8.19 +
    8.20 +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
    8.21 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
    8.22 +	@rm -f tutorial.dvi
    8.23 +
    8.24  ## HOL-Misc
    8.25  
    8.26  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    8.27 @@ -109,4 +117,4 @@
    8.28  ## clean
    8.29  
    8.30  clean:
    8.31 -	@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
    8.32 +	@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 
     9.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 14:59:44 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 15:43:15 2000 +0200
     9.3 @@ -17,7 +17,7 @@
     9.4  that is amenable to induction, but this is not always the case:
     9.5  *};
     9.6  
     9.7 -lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) = last xs";
     9.8 +lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";
     9.9  apply(induct_tac xs);
    9.10  
    9.11  txt{*\noindent
    9.12 @@ -49,7 +49,7 @@
    9.13  This means we should prove
    9.14  *};
    9.15  (*<*)oops;(*>*)
    9.16 -lemma hd_rev: "xs \\<noteq> [] \\<longrightarrow> hd(rev xs) = last xs";
    9.17 +lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
    9.18  (*<*)
    9.19  by(induct_tac xs, auto);
    9.20  (*>*)
    9.21 @@ -82,7 +82,7 @@
    9.22  Here is a simple example (which is proved by @{text"blast"}):
    9.23  *};
    9.24  
    9.25 -lemma simple: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
    9.26 +lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
    9.27  (*<*)by blast;(*>*)
    9.28  
    9.29  text{*\noindent
    9.30 @@ -105,7 +105,7 @@
    9.31  statement of your original lemma, thus avoiding the intermediate step:
    9.32  *};
    9.33  
    9.34 -lemma myrule[rulified]:  "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
    9.35 +lemma myrule[rulified]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
    9.36  (*<*)
    9.37  by blast;
    9.38  (*>*)
    9.39 @@ -134,8 +134,8 @@
    9.40  Structural induction on @{typ"nat"} is
    9.41  usually known as ``mathematical induction''. There is also ``complete
    9.42  induction'', where you must prove $P(n)$ under the assumption that $P(m)$
    9.43 -holds for all $m<n$. In Isabelle, this is the theorem @{thm [source] nat_less_induct}:
    9.44 -@{thm[display] nat_less_induct [no_vars]}
    9.45 +holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
    9.46 +@{thm[display]"nat_less_induct"[no_vars]}
    9.47  Here is an example of its application.
    9.48  *};
    9.49  
    9.50 @@ -152,10 +152,10 @@
    9.51  above, we have to phrase the proposition as follows to allow induction:
    9.52  *};
    9.53  
    9.54 -lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
    9.55 +lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
    9.56  
    9.57  txt{*\noindent
    9.58 -To perform induction on @{term"k"} using @{thm [source] nat_less_induct}, we use the same
    9.59 +To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same
    9.60  general induction method as for recursion induction (see
    9.61  \S\ref{sec:recdef-induction}):
    9.62  *};
    9.63 @@ -213,7 +213,7 @@
    9.64  we could have included this derivation in the original statement of the lemma:
    9.65  *};
    9.66  
    9.67 -lemma f_incr[rulified, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
    9.68 +lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
    9.69  (*<*)oops;(*>*)
    9.70  
    9.71  text{*
    9.72 @@ -242,49 +242,46 @@
    9.73  text{*\label{sec:derive-ind}
    9.74  Induction schemas are ordinary theorems and you can derive new ones
    9.75  whenever you wish.  This section shows you how to, using the example
    9.76 -of @{thm [source] nat_less_induct}. Assume we only have structural induction
    9.77 +of @{thm[source]nat_less_induct}. Assume we only have structural induction
    9.78  available for @{typ"nat"} and want to derive complete induction. This
    9.79  requires us to generalize the statement first:
    9.80  *};
    9.81  
    9.82 -lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> \\<forall>m<n. P m";
    9.83 +lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
    9.84  apply(induct_tac n);
    9.85  
    9.86  txt{*\noindent
    9.87  The base case is trivially true. For the induction step (@{prop"m <
    9.88 -Suc n"}) we distinguish two cases: @{prop"m < n"} is true by induction
    9.89 -hypothesis and @{prop"m = n"} follow from the assumption again using
    9.90 +Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
    9.91 +hypothesis and case @{prop"m = n"} follows from the assumption, again using
    9.92  the induction hypothesis:
    9.93  *};
    9.94 -
    9.95  apply(blast);
    9.96 -(* apply(blast elim:less_SucE); *)
    9.97 -ML"set quick_and_dirty"
    9.98 -sorry;
    9.99 -ML"reset quick_and_dirty"
   9.100 +by(blast elim:less_SucE)
   9.101  
   9.102  text{*\noindent
   9.103  The elimination rule @{thm[source]less_SucE} expresses the case distinction:
   9.104  @{thm[display]"less_SucE"[no_vars]}
   9.105  
   9.106  Now it is straightforward to derive the original version of
   9.107 -@{thm [source] nat_less_induct} by manipulting the conclusion of the above lemma:
   9.108 +@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
   9.109  instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
   9.110  remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
   9.111  happens automatically when we add the lemma as a new premise to the
   9.112  desired goal:
   9.113  *};
   9.114  
   9.115 -theorem nat_less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
   9.116 +theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
   9.117  by(insert induct_lem, blast);
   9.118  
   9.119 -text{*\noindent
   9.120 +text{*
   9.121  Finally we should mention that HOL already provides the mother of all
   9.122  inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
   9.123  @{thm[display]"wf_induct"[no_vars]}
   9.124  where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
   9.125 -For example @{thm [source] nat_less_induct} is the special case where @{term"r"} is
   9.126 -@{text"<"} on @{typ"nat"}. For details see the library.
   9.127 +For example, theorem @{thm[source]nat_less_induct} can be viewed (and
   9.128 +derived) as a special case of @{thm[source]wf_induct} where 
   9.129 +@{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.
   9.130  *};
   9.131  
   9.132  (*<*)
    10.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Sep 12 14:59:44 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Sep 12 15:43:15 2000 +0200
    10.3 @@ -227,15 +227,12 @@
    10.4  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
    10.5  \begin{isamarkuptxt}%
    10.6  \noindent
    10.7 -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
    10.8 -hypothesis and \isa{m\ {\isacharequal}\ n} follow from the assumption again using
    10.9 +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
   10.10 +hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
   10.11  the induction hypothesis:%
   10.12  \end{isamarkuptxt}%
   10.13  \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   10.14 -\isanewline
   10.15 -\isacommand{ML}{\isachardoublequote}set\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}\isanewline
   10.16 -\isacommand{sorry}\isanewline
   10.17 -\isacommand{ML}{\isachardoublequote}reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}%
   10.18 +\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
   10.19  \begin{isamarkuptext}%
   10.20  \noindent
   10.21  The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
   10.22 @@ -253,15 +250,15 @@
   10.23  \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
   10.24  \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
   10.25  \begin{isamarkuptext}%
   10.26 -\noindent
   10.27  Finally we should mention that HOL already provides the mother of all
   10.28  inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
   10.29  \begin{isabelle}%
   10.30  \ \ \ \ \ {\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%
   10.31  \end{isabelle}
   10.32  where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
   10.33 -For example \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is the special case where \isa{r} is
   10.34 -\isa{{\isacharless}} on \isa{nat}. For details see the library.%
   10.35 +For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
   10.36 +derived) as a special case of \isa{wf{\isacharunderscore}induct} where 
   10.37 +\isa{r} is \isa{{\isacharless}} on \isa{nat}. For details see the library.%
   10.38  \end{isamarkuptext}%
   10.39  \end{isabellebody}%
   10.40  %%% Local Variables:
    11.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Tue Sep 12 14:59:44 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Tue Sep 12 15:43:15 2000 +0200
    11.3 @@ -3,13 +3,14 @@
    11.4  \def\isabellecontext{pairs}%
    11.5  %
    11.6  \begin{isamarkuptext}%
    11.7 -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
    11.8 -  $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
    11.9 -are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
   11.10 -\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
   11.11 -\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
   11.12 -\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
   11.13 -  $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   11.14 +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   11.15 +\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
   11.16 +$\tau@i$. The components of a pair are extracted by \isa{fst} and
   11.17 +\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   11.18 +are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   11.19 +for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   11.20 +$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
   11.21 +\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   11.22  
   11.23  It is possible to use (nested) tuples as patterns in abstractions, for
   11.24  example \isa{\isasymlambda(x,y,z).x+y+z} and
    12.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Tue Sep 12 14:59:44 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Sep 12 15:43:15 2000 +0200
    12.3 @@ -1,10 +1,376 @@
    12.4  %
    12.5  \begin{isabellebody}%
    12.6  \def\isabellecontext{simp}%
    12.7 -\isanewline
    12.8 -\isacommand{theory}\ simp\ {\isacharequal}\ Main{\isacharcolon}\isanewline
    12.9 -\isanewline
   12.10 -\isacommand{end}\isanewline
   12.11 +%
   12.12 +\isamarkupsubsubsection{Simplification rules}
   12.13 +%
   12.14 +\begin{isamarkuptext}%
   12.15 +\indexbold{simplification rule}
   12.16 +To facilitate simplification, theorems can be declared to be simplification
   12.17 +rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp
   12.18 +  (attribute)}), in which case proofs by simplification make use of these
   12.19 +rules automatically. In addition the constructs \isacommand{datatype} and
   12.20 +\isacommand{primrec} (and a few others) invisibly declare useful
   12.21 +simplification rules. Explicit definitions are \emph{not} declared
   12.22 +simplification rules automatically!
   12.23 +
   12.24 +Not merely equations but pretty much any theorem can become a simplification
   12.25 +rule. The simplifier will try to make sense of it.  For example, a theorem
   12.26 +\isa{{\isasymnot}\ P} is automatically turned into \isa{P\ {\isacharequal}\ False}. The details
   12.27 +are explained in \S\ref{sec:SimpHow}.
   12.28 +
   12.29 +The simplification attribute of theorems can be turned on and off as follows:
   12.30 +\begin{quote}
   12.31 +\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
   12.32 +\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
   12.33 +\end{quote}
   12.34 +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
   12.35 +rules.  Those of a more specific nature (e.g.\ distributivity laws, which
   12.36 +alter the structure of terms considerably) should only be used selectively,
   12.37 +i.e.\ they should not be default simplification rules.  Conversely, it may
   12.38 +also happen that a simplification rule needs to be disabled in certain
   12.39 +proofs.  Frequent changes in the simplification status of a theorem may
   12.40 +indicate a badly designed theory.
   12.41 +\begin{warn}
   12.42 +  Simplification may not terminate, for example if both $f(x) = g(x)$ and
   12.43 +  $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
   12.44 +  to include simplification rules that can lead to nontermination, either on
   12.45 +  their own or in combination with other simplification rules.
   12.46 +\end{warn}%
   12.47 +\end{isamarkuptext}%
   12.48 +%
   12.49 +\isamarkupsubsubsection{The simplification method}
   12.50 +%
   12.51 +\begin{isamarkuptext}%
   12.52 +\index{*simp (method)|bold}
   12.53 +The general format of the simplification method is
   12.54 +\begin{quote}
   12.55 +\isa{simp} \textit{list of modifiers}
   12.56 +\end{quote}
   12.57 +where the list of \emph{modifiers} helps to fine tune the behaviour and may
   12.58 +be empty. Most if not all of the proofs seen so far could have been performed
   12.59 +with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
   12.60 +only the first subgoal and may thus need to be repeated---use
   12.61 +\isaindex{simp_all} to simplify all subgoals.
   12.62 +Note that \isa{simp} fails if nothing changes.%
   12.63 +\end{isamarkuptext}%
   12.64 +%
   12.65 +\isamarkupsubsubsection{Adding and deleting simplification rules}
   12.66 +%
   12.67 +\begin{isamarkuptext}%
   12.68 +If a certain theorem is merely needed in a few proofs by simplification,
   12.69 +we do not need to make it a global simplification rule. Instead we can modify
   12.70 +the set of simplification rules used in a simplification step by adding rules
   12.71 +to it and/or deleting rules from it. The two modifiers for this are
   12.72 +\begin{quote}
   12.73 +\isa{add{\isacharcolon}} \textit{list of theorem names}\\
   12.74 +\isa{del{\isacharcolon}} \textit{list of theorem names}
   12.75 +\end{quote}
   12.76 +In case you want to use only a specific list of theorems and ignore all
   12.77 +others:
   12.78 +\begin{quote}
   12.79 +\isa{only{\isacharcolon}} \textit{list of theorem names}
   12.80 +\end{quote}%
   12.81 +\end{isamarkuptext}%
   12.82 +%
   12.83 +\isamarkupsubsubsection{Assumptions}
   12.84 +%
   12.85 +\begin{isamarkuptext}%
   12.86 +\index{simplification!with/of assumptions}
   12.87 +By default, assumptions are part of the simplification process: they are used
   12.88 +as simplification rules and are simplified themselves. For example:%
   12.89 +\end{isamarkuptext}%
   12.90 +\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
   12.91 +\isacommand{by}\ simp%
   12.92 +\begin{isamarkuptext}%
   12.93 +\noindent
   12.94 +The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
   12.95 +simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
   12.96 +conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
   12.97 +
   12.98 +In some cases this may be too much of a good thing and may lead to
   12.99 +nontermination:%
  12.100 +\end{isamarkuptext}%
  12.101 +\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}%
  12.102 +\begin{isamarkuptxt}%
  12.103 +\noindent
  12.104 +cannot be solved by an unmodified application of \isa{simp} because the
  12.105 +simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
  12.106 +does not terminate. Isabelle notices certain simple forms of
  12.107 +nontermination but not this one. The problem can be circumvented by
  12.108 +explicitly telling the simplifier to ignore the assumptions:%
  12.109 +\end{isamarkuptxt}%
  12.110 +\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
  12.111 +\begin{isamarkuptext}%
  12.112 +\noindent
  12.113 +There are three options that influence the treatment of assumptions:
  12.114 +\begin{description}
  12.115 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
  12.116 + means that assumptions are completely ignored.
  12.117 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
  12.118 + means that the assumptions are not simplified but
  12.119 +  are used in the simplification of the conclusion.
  12.120 +\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
  12.121 + means that the assumptions are simplified but are not
  12.122 +  used in the simplification of each other or the conclusion.
  12.123 +\end{description}
  12.124 +Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
  12.125 +the above problematic subgoal.
  12.126 +
  12.127 +Note that only one of the above options is allowed, and it must precede all
  12.128 +other arguments.%
  12.129 +\end{isamarkuptext}%
  12.130 +%
  12.131 +\isamarkupsubsubsection{Rewriting with definitions}
  12.132 +%
  12.133 +\begin{isamarkuptext}%
  12.134 +\index{simplification!with definitions}
  12.135 +Constant definitions (\S\ref{sec:ConstDefinitions}) can
  12.136 +be used as simplification rules, but by default they are not.  Hence the
  12.137 +simplifier does not expand them automatically, just as it should be:
  12.138 +definitions are introduced for the purpose of abbreviating complex
  12.139 +concepts. Of course we need to expand the definitions initially to derive
  12.140 +enough lemmas that characterize the concept sufficiently for us to forget the
  12.141 +original definition. For example, given%
  12.142 +\end{isamarkuptext}%
  12.143 +\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
  12.144 +\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
  12.145 +\begin{isamarkuptext}%
  12.146 +\noindent
  12.147 +we may want to prove%
  12.148 +\end{isamarkuptext}%
  12.149 +\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
  12.150 +\begin{isamarkuptxt}%
  12.151 +\noindent
  12.152 +Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
  12.153 +get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
  12.154 +\end{isamarkuptxt}%
  12.155 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
  12.156 +\begin{isamarkuptxt}%
  12.157 +\noindent
  12.158 +In this particular case, the resulting goal
  12.159 +\begin{isabelle}
  12.160 +~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
  12.161 +\end{isabelle}
  12.162 +can be proved by simplification. Thus we could have proved the lemma outright%
  12.163 +\end{isamarkuptxt}%
  12.164 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
  12.165 +\begin{isamarkuptext}%
  12.166 +\noindent
  12.167 +Of course we can also unfold definitions in the middle of a proof.
  12.168 +
  12.169 +You should normally not turn a definition permanently into a simplification
  12.170 +rule because this defeats the whole purpose of an abbreviation.
  12.171 +
  12.172 +\begin{warn}
  12.173 +  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
  12.174 +  occurrences of $f$ with at least two arguments. Thus it is safer to define
  12.175 +  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
  12.176 +\end{warn}%
  12.177 +\end{isamarkuptext}%
  12.178 +%
  12.179 +\isamarkupsubsubsection{Simplifying let-expressions}
  12.180 +%
  12.181 +\begin{isamarkuptext}%
  12.182 +\index{simplification!of let-expressions}
  12.183 +Proving a goal containing \isaindex{let}-expressions almost invariably
  12.184 +requires the \isa{let}-con\-structs to be expanded at some point. Since
  12.185 +\isa{let}-\isa{in} is just syntactic sugar for a predefined constant
  12.186 +(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
  12.187 +\isa{Let{\isacharunderscore}def}:%
  12.188 +\end{isamarkuptext}%
  12.189 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
  12.190 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
  12.191 +\begin{isamarkuptext}%
  12.192 +If, in a particular context, there is no danger of a combinatorial explosion
  12.193 +of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
  12.194 +default:%
  12.195 +\end{isamarkuptext}%
  12.196 +\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
  12.197 +\isamarkupsubsubsection{Conditional equations}
  12.198 +%
  12.199 +\begin{isamarkuptext}%
  12.200 +So far all examples of rewrite rules were equations. The simplifier also
  12.201 +accepts \emph{conditional} equations, for example%
  12.202 +\end{isamarkuptext}%
  12.203 +\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
  12.204 +\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}%
  12.205 +\begin{isamarkuptext}%
  12.206 +\noindent
  12.207 +Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
  12.208 +sequence of methods. Assuming that the simplification rule
  12.209 +\isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
  12.210 +is present as well,%
  12.211 +\end{isamarkuptext}%
  12.212 +\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
  12.213 +\begin{isamarkuptext}%
  12.214 +\noindent
  12.215 +is proved by plain simplification:
  12.216 +the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
  12.217 +can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
  12.218 +because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
  12.219 +simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
  12.220 +assumption of the subgoal.%
  12.221 +\end{isamarkuptext}%
  12.222 +%
  12.223 +\isamarkupsubsubsection{Automatic case splits}
  12.224 +%
  12.225 +\begin{isamarkuptext}%
  12.226 +\indexbold{case splits}\index{*split|(}
  12.227 +Goals containing \isa{if}-expressions are usually proved by case
  12.228 +distinction on the condition of the \isa{if}. For example the goal%
  12.229 +\end{isamarkuptext}%
  12.230 +\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
  12.231 +\begin{isamarkuptxt}%
  12.232 +\noindent
  12.233 +can be split into
  12.234 +\begin{isabelle}
  12.235 +~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
  12.236 +\end{isabelle}
  12.237 +by a degenerate form of simplification%
  12.238 +\end{isamarkuptxt}%
  12.239 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
  12.240 +\begin{isamarkuptext}%
  12.241 +\noindent
  12.242 +where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
  12.243 +empty list of theorems) but the rule \isaindexbold{split_if} for
  12.244 +splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
  12.245 +case-splitting on \isa{if}s is almost always the right proof strategy, the
  12.246 +simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
  12.247 +on the initial goal above.
  12.248 +
  12.249 +This splitting idea generalizes from \isa{if} to \isaindex{case}:%
  12.250 +\end{isamarkuptext}%
  12.251 +\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}%
  12.252 +\begin{isamarkuptxt}%
  12.253 +\noindent
  12.254 +becomes
  12.255 +\begin{isabelle}\makeatother
  12.256 +~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
  12.257 +~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
  12.258 +\end{isabelle}
  12.259 +by typing%
  12.260 +\end{isamarkuptxt}%
  12.261 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
  12.262 +\begin{isamarkuptext}%
  12.263 +\noindent
  12.264 +In contrast to \isa{if}-expressions, the simplifier does not split
  12.265 +\isa{case}-expressions by default because this can lead to nontermination
  12.266 +in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
  12.267 +dropped, the above goal is solved,%
  12.268 +\end{isamarkuptext}%
  12.269 +\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
  12.270 +\begin{isamarkuptext}%
  12.271 +\noindent%
  12.272 +which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
  12.273 +
  12.274 +In general, every datatype $t$ comes with a theorem
  12.275 +$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
  12.276 +locally as above, or by giving it the \isa{split} attribute globally:%
  12.277 +\end{isamarkuptext}%
  12.278 +\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}%
  12.279 +\begin{isamarkuptext}%
  12.280 +\noindent
  12.281 +The \isa{split} attribute can be removed with the \isa{del} modifier,
  12.282 +either locally%
  12.283 +\end{isamarkuptext}%
  12.284 +\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
  12.285 +\begin{isamarkuptext}%
  12.286 +\noindent
  12.287 +or globally:%
  12.288 +\end{isamarkuptext}%
  12.289 +\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}%
  12.290 +\begin{isamarkuptext}%
  12.291 +The above split rules intentionally only affect the conclusion of a
  12.292 +subgoal.  If you want to split an \isa{if} or \isa{case}-expression in
  12.293 +the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
  12.294 +$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
  12.295 +\end{isamarkuptext}%
  12.296 +\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
  12.297 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
  12.298 +\begin{isamarkuptext}%
  12.299 +\noindent
  12.300 +In contrast to splitting the conclusion, this actually creates two
  12.301 +separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
  12.302 +\begin{isabelle}
  12.303 +\ \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
  12.304 +\ \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}
  12.305 +\end{isabelle}
  12.306 +If you need to split both in the assumptions and the conclusion,
  12.307 +use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
  12.308 +$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.
  12.309 +
  12.310 +\begin{warn}
  12.311 +  The simplifier merely simplifies the condition of an \isa{if} but not the
  12.312 +  \isa{then} or \isa{else} parts. The latter are simplified only after the
  12.313 +  condition reduces to \isa{True} or \isa{False}, or after splitting. The
  12.314 +  same is true for \isaindex{case}-expressions: only the selector is
  12.315 +  simplified at first, until either the expression reduces to one of the
  12.316 +  cases or it is split.
  12.317 +\end{warn}
  12.318 +
  12.319 +\index{*split|)}%
  12.320 +\end{isamarkuptext}%
  12.321 +%
  12.322 +\isamarkupsubsubsection{Arithmetic}
  12.323 +%
  12.324 +\begin{isamarkuptext}%
  12.325 +\index{arithmetic}
  12.326 +The simplifier routinely solves a small class of linear arithmetic formulae
  12.327 +(over type \isa{nat} and other numeric types): it only takes into account
  12.328 +assumptions and conclusions that are (possibly negated) (in)equalities
  12.329 +(\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus%
  12.330 +\end{isamarkuptext}%
  12.331 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
  12.332 +\begin{isamarkuptext}%
  12.333 +\noindent
  12.334 +is proved by simplification, whereas the only slightly more complex%
  12.335 +\end{isamarkuptext}%
  12.336 +\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
  12.337 +\begin{isamarkuptext}%
  12.338 +\noindent
  12.339 +is not proved by simplification and requires \isa{arith}.%
  12.340 +\end{isamarkuptext}%
  12.341 +%
  12.342 +\isamarkupsubsubsection{Tracing}
  12.343 +%
  12.344 +\begin{isamarkuptext}%
  12.345 +\indexbold{tracing the simplifier}
  12.346 +Using the simplifier effectively may take a bit of experimentation.  Set the
  12.347 +\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
  12.348 +on:%
  12.349 +\end{isamarkuptext}%
  12.350 +\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
  12.351 +\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
  12.352 +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
  12.353 +\begin{isamarkuptext}%
  12.354 +\noindent
  12.355 +produces the trace
  12.356 +
  12.357 +\begin{ttbox}\makeatother
  12.358 +Applying instance of rewrite rule:
  12.359 +rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
  12.360 +Rewriting:
  12.361 +rev [x] == rev [] @ [x]
  12.362 +Applying instance of rewrite rule:
  12.363 +rev [] == []
  12.364 +Rewriting:
  12.365 +rev [] == []
  12.366 +Applying instance of rewrite rule:
  12.367 +[] @ ?y == ?y
  12.368 +Rewriting:
  12.369 +[] @ [x] == [x]
  12.370 +Applying instance of rewrite rule:
  12.371 +?x3 \# ?t3 = ?t3 == False
  12.372 +Rewriting:
  12.373 +[x] = [] == False
  12.374 +\end{ttbox}
  12.375 +
  12.376 +In more complicated cases, the trace can be quite lenghty, especially since
  12.377 +invocations of the simplifier are often nested (e.g.\ when solving conditions
  12.378 +of rewrite rules). Thus it is advisable to reset it:%
  12.379 +\end{isamarkuptext}%
  12.380 +\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
  12.381  \end{isabellebody}%
  12.382  %%% Local Variables:
  12.383  %%% mode: latex
    13.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Tue Sep 12 14:59:44 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Sep 12 15:43:15 2000 +0200
    13.3 @@ -3,7 +3,7 @@
    13.4  \def\isabellecontext{types}%
    13.5  \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
    13.6  \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    13.7 -\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
    13.8 +\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
    13.9  \begin{isamarkuptext}%
   13.10  \noindent\indexbold{*types}%
   13.11  Internally all synonyms are fully expanded.  As a consequence Isabelle's
    14.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Tue Sep 12 14:59:44 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Tue Sep 12 15:43:15 2000 +0200
    14.3 @@ -2,13 +2,14 @@
    14.4  theory pairs = Main:;
    14.5  (*>*)
    14.6  text{*
    14.7 -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
    14.8 -  $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
    14.9 -are extracted by @{term"fst"} and @{term"snd"}: \isa{fst($x$,$y$) = $x$} and
   14.10 -\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
   14.11 -\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
   14.12 -\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
   14.13 -  $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   14.14 +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   14.15 +\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
   14.16 +$\tau@i$. The components of a pair are extracted by @{term"fst"} and
   14.17 +@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   14.18 +are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   14.19 +for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   14.20 +$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
   14.21 +\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
   14.22  
   14.23  It is possible to use (nested) tuples as patterns in abstractions, for
   14.24  example \isa{\isasymlambda(x,y,z).x+y+z} and
    15.1 --- a/doc-src/TutorialI/Misc/types.thy	Tue Sep 12 14:59:44 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/types.thy	Tue Sep 12 15:43:15 2000 +0200
    15.3 @@ -1,8 +1,8 @@
    15.4  (*<*)
    15.5  theory "types" = Main:;
    15.6  (*>*)types number       = nat
    15.7 -      gate         = "bool \\<Rightarrow> bool \\<Rightarrow> bool"
    15.8 -      ('a,'b)alist = "('a * 'b)list";
    15.9 +      gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
   15.10 +      ('a,'b)alist = "('a \<times> 'b)list";
   15.11  
   15.12  text{*\noindent\indexbold{*types}%
   15.13  Internally all synonyms are fully expanded.  As a consequence Isabelle's
   15.14 @@ -23,8 +23,8 @@
   15.15  therefore be defined directly by
   15.16  *}
   15.17  
   15.18 -defs nand_def: "nand A B \\<equiv> \\<not>(A \\<and> B)"
   15.19 -     exor_def: "exor A B \\<equiv> A \\<and> \\<not>B \\<or> \\<not>A \\<and> B";
   15.20 +defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
   15.21 +     exor_def: "exor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
   15.22  
   15.23  text{*\noindent%
   15.24  where \isacommand{defs}\indexbold{*defs} is a keyword and
   15.25 @@ -35,9 +35,9 @@
   15.26  *}
   15.27  
   15.28  constdefs nor :: gate
   15.29 -         "nor A B \\<equiv> \\<not>(A \\<or> B)"
   15.30 +         "nor A B \<equiv> \<not>(A \<or> B)"
   15.31            exor2 :: gate
   15.32 -         "exor2 A B \\<equiv> (A \\<or> B) \\<and> (\\<not>A \\<or> \\<not>B)";
   15.33 +         "exor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
   15.34  
   15.35  text{*\noindent\indexbold{*constdefs}%
   15.36  in which case the default name of each definition is $f$@{text"_def"}, where
    16.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy	Tue Sep 12 14:59:44 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy	Tue Sep 12 15:43:15 2000 +0200
    16.3 @@ -23,9 +23,9 @@
    16.4  However, the definition does not succeed. Isabelle complains about an
    16.5  unproved termination condition
    16.6  @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
    16.7 -where @{term"set"} returns the set of elements of a list (no special
    16.8 -knowledge of sets is required in the following) and @{text"term_list_size ::
    16.9 -term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
   16.10 +where @{term"set"} returns the set of elements of a list
   16.11 +and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
   16.12 +function automatically defined by Isabelle
   16.13  (when @{text"term"} was defined).  First we have to understand why the
   16.14  recursive call of @{term"trev"} underneath @{term"map"} leads to the above
   16.15  condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
    17.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 14:59:44 2000 +0200
    17.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 15:43:15 2000 +0200
    17.3 @@ -23,7 +23,6 @@
    17.4  @{term"trev"}:
    17.5  *};
    17.6  
    17.7 -lemmas [cong] = map_cong;
    17.8  lemma "trev(trev t) = t";
    17.9  apply(induct_tac t rule:trev.induct);
   17.10  txt{*\noindent
   17.11 @@ -32,12 +31,12 @@
   17.12  both of which are solved by simplification:
   17.13  *};
   17.14  
   17.15 -by(simp_all add:rev_map sym[OF map_compose]);
   17.16 +by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
   17.17  
   17.18  text{*\noindent
   17.19  If the proof of the induction step mystifies you, we recommend to go through
   17.20  the chain of simplification steps in detail; you will probably need the help of
   17.21 -@{text"trace_simp"}.
   17.22 +@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
   17.23  %\begin{quote}
   17.24  %{term[display]"trev(trev(App f ts))"}\\
   17.25  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
   17.26 @@ -84,5 +83,8 @@
   17.27  congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
   17.28  declaring a congruence rule for the simplifier does not make it
   17.29  available to \isacommand{recdef}, and vice versa. This is intentional.
   17.30 +%The simplifier's congruence rules cannot be used by recdef.
   17.31 +%For example the weak congruence rules for if and case would prevent
   17.32 +%recdef from generating sensible termination conditions.
   17.33  *};
   17.34  (*<*)end;(*>*)
    18.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Sep 12 14:59:44 2000 +0200
    18.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Sep 12 15:43:15 2000 +0200
    18.3 @@ -24,8 +24,9 @@
    18.4  \begin{isabelle}%
    18.5  \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
    18.6  \end{isabelle}
    18.7 -where \isa{set} returns the set of elements of a list (no special
    18.8 -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
    18.9 +where \isa{set} returns the set of elements of a list
   18.10 +and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
   18.11 +function automatically defined by Isabelle
   18.12  (when \isa{term} was defined).  First we have to understand why the
   18.13  recursive call of \isa{trev} underneath \isa{map} leads to the above
   18.14  condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
    19.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 14:59:44 2000 +0200
    19.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 15:43:15 2000 +0200
    19.3 @@ -17,7 +17,6 @@
    19.4  induction schema for type \isa{term} but the simpler one arising from
    19.5  \isa{trev}:%
    19.6  \end{isamarkuptext}%
    19.7 -\isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
    19.8  \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
    19.9  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
   19.10  \begin{isamarkuptxt}%
   19.11 @@ -29,12 +28,12 @@
   19.12  \end{isabelle}
   19.13  both of which are solved by simplification:%
   19.14  \end{isamarkuptxt}%
   19.15 -\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
   19.16 +\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
   19.17  \begin{isamarkuptext}%
   19.18  \noindent
   19.19  If the proof of the induction step mystifies you, we recommend to go through
   19.20  the chain of simplification steps in detail; you will probably need the help of
   19.21 -\isa{trace{\isacharunderscore}simp}.
   19.22 +\isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below.
   19.23  %\begin{quote}
   19.24  %{term[display]"trev(trev(App f ts))"}\\
   19.25  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
   19.26 @@ -82,7 +81,10 @@
   19.27  Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
   19.28  congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
   19.29  declaring a congruence rule for the simplifier does not make it
   19.30 -available to \isacommand{recdef}, and vice versa. This is intentional.%
   19.31 +available to \isacommand{recdef}, and vice versa. This is intentional.
   19.32 +%The simplifier's congruence rules cannot be used by recdef.
   19.33 +%For example the weak congruence rules for if and case would prevent
   19.34 +%recdef from generating sensible termination conditions.%
   19.35  \end{isamarkuptext}%
   19.36  \end{isabellebody}%
   19.37  %%% Local Variables:
    20.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Tue Sep 12 14:59:44 2000 +0200
    20.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Sep 12 15:43:15 2000 +0200
    20.3 @@ -24,7 +24,7 @@
    20.4  Slightly more interesting is the insertion of a fixed element
    20.5  between any two elements of a list:%
    20.6  \end{isamarkuptext}%
    20.7 -\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    20.8 +\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    20.9  \isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
   20.10  \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
   20.11  \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
   20.12 @@ -44,7 +44,7 @@
   20.13  Overlapping patterns are disambiguated by taking the order of equations into
   20.14  account, just as in functional programming:%
   20.15  \end{isamarkuptext}%
   20.16 -\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
   20.17 +\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
   20.18  \isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
   20.19  \ \ {\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
   20.20  \ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
    21.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Sep 12 14:59:44 2000 +0200
    21.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Sep 12 15:43:15 2000 +0200
    21.3 @@ -10,7 +10,7 @@
    21.4  terminate because of automatic splitting of \isa{if}.
    21.5  Let us look at an example:%
    21.6  \end{isamarkuptext}%
    21.7 -\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    21.8 +\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    21.9  \isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
   21.10  \ \ {\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}%
   21.11  \begin{isamarkuptext}%
   21.12 @@ -54,7 +54,7 @@
   21.13  rather than \isa{if} on the right. In the case of \isa{gcd} the
   21.14  following alternative definition suggests itself:%
   21.15  \end{isamarkuptext}%
   21.16 -\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   21.17 +\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   21.18  \isacommand{recdef}\ gcd\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
   21.19  \ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
   21.20  \ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd\isadigit{1}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
   21.21 @@ -67,7 +67,7 @@
   21.22  A very simple alternative is to replace \isa{if} by \isa{case}, which
   21.23  is also available for \isa{bool} but is not split automatically:%
   21.24  \end{isamarkuptext}%
   21.25 -\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   21.26 +\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   21.27  \isacommand{recdef}\ gcd\isadigit{2}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
   21.28  \ \ {\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}%
   21.29  \begin{isamarkuptext}%
   21.30 @@ -85,7 +85,7 @@
   21.31  \noindent
   21.32  after which we can disable the original simplification rule:%
   21.33  \end{isamarkuptext}%
   21.34 -\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
   21.35 +\isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
   21.36  \end{isabellebody}%
   21.37  %%% Local Variables:
   21.38  %%% mode: latex
    22.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Sep 12 14:59:44 2000 +0200
    22.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Sep 12 15:43:15 2000 +0200
    22.3 @@ -17,7 +17,7 @@
    22.4  (there is one for each recursive call) automatically. For example,
    22.5  termination of the following artificial function%
    22.6  \end{isamarkuptext}%
    22.7 -\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    22.8 +\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    22.9  \isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
   22.10  \ \ {\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}%
   22.11  \begin{isamarkuptext}%
   22.12 @@ -27,7 +27,7 @@
   22.13  have to prove it as a separate lemma before you attempt the definition
   22.14  of your function once more. In our case the required lemma is the obvious one:%
   22.15  \end{isamarkuptext}%
   22.16 -\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
   22.17 +\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
   22.18  \begin{isamarkuptxt}%
   22.19  \noindent
   22.20  It was not proved automatically because of the special nature of \isa{{\isacharminus}}
   22.21 @@ -37,30 +37,30 @@
   22.22  \begin{isamarkuptext}%
   22.23  \noindent
   22.24  Because \isacommand{recdef}'s termination prover involves simplification,
   22.25 -we have turned our lemma into a simplification rule. Therefore our second
   22.26 -attempt to define our function will automatically take it into account:%
   22.27 +we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
   22.28 +a simplification rule:%
   22.29  \end{isamarkuptext}%
   22.30 -\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   22.31 +\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   22.32  \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
   22.33 -\ \ {\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}%
   22.34 +\ \ {\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
   22.35 +{\isacharparenleft}\isakeyword{hints}\ simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}%
   22.36  \begin{isamarkuptext}%
   22.37  \noindent
   22.38  This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
   22.39  the stated recursion equation for \isa{g} and they are simplification
   22.40  rules. Thus we can automatically prove%
   22.41  \end{isamarkuptext}%
   22.42 -\isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
   22.43 +\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
   22.44  \isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
   22.45  \begin{isamarkuptext}%
   22.46  \noindent
   22.47  More exciting theorems require induction, which is discussed below.
   22.48  
   22.49 -Because lemma \isa{termi{\isacharunderscore}lem} above was only turned into a
   22.50 -simplification rule for the sake of the termination proof, we may want to
   22.51 -disable it again:%
   22.52 -\end{isamarkuptext}%
   22.53 -\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem%
   22.54 -\begin{isamarkuptext}%
   22.55 +If the termination proof requires a new lemma that is of general use, you can
   22.56 +turn it permanently into a simplification rule, in which case the above
   22.57 +\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
   22.58 +sufficiently general to warrant this distinction.
   22.59 +
   22.60  The attentive reader may wonder why we chose to call our function \isa{g}
   22.61  rather than \isa{f} the second time around. The reason is that, despite
   22.62  the failed termination proof, the definition of \isa{f} did not
   22.63 @@ -79,7 +79,7 @@
   22.64  allows arbitrary wellfounded relations. For example, termination of
   22.65  Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
   22.66  \end{isamarkuptext}%
   22.67 -\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   22.68 +\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   22.69  \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
   22.70  \ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
   22.71  \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
    23.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Tue Sep 12 14:59:44 2000 +0200
    23.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Sep 12 15:43:15 2000 +0200
    23.3 @@ -6,8 +6,8 @@
    23.4  Here is a simple example, the Fibonacci function:
    23.5  *}
    23.6  
    23.7 -consts fib :: "nat \\<Rightarrow> nat";
    23.8 -recdef fib "measure(\\<lambda>n. n)"
    23.9 +consts fib :: "nat \<Rightarrow> nat";
   23.10 +recdef fib "measure(\<lambda>n. n)"
   23.11    "fib 0 = 0"
   23.12    "fib 1 = 1"
   23.13    "fib (Suc(Suc x)) = fib x + fib (Suc x)";
   23.14 @@ -26,8 +26,8 @@
   23.15  between any two elements of a list:
   23.16  *}
   23.17  
   23.18 -consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
   23.19 -recdef sep "measure (\\<lambda>(a,xs). length xs)"
   23.20 +consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
   23.21 +recdef sep "measure (\<lambda>(a,xs). length xs)"
   23.22    "sep(a, [])     = []"
   23.23    "sep(a, [x])    = [x]"
   23.24    "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
   23.25 @@ -39,8 +39,8 @@
   23.26  Pattern matching need not be exhaustive:
   23.27  *}
   23.28  
   23.29 -consts last :: "'a list \\<Rightarrow> 'a";
   23.30 -recdef last "measure (\\<lambda>xs. length xs)"
   23.31 +consts last :: "'a list \<Rightarrow> 'a";
   23.32 +recdef last "measure (\<lambda>xs. length xs)"
   23.33    "last [x]      = x"
   23.34    "last (x#y#zs) = last (y#zs)";
   23.35  
   23.36 @@ -49,8 +49,8 @@
   23.37  account, just as in functional programming:
   23.38  *}
   23.39  
   23.40 -consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
   23.41 -recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
   23.42 +consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
   23.43 +recdef sep1 "measure (\<lambda>(a,xs). length xs)"
   23.44    "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
   23.45    "sep1(a, xs)     = xs";
   23.46  
   23.47 @@ -67,17 +67,17 @@
   23.48    arguments as in the following definition:
   23.49  \end{warn}
   23.50  *}
   23.51 -consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
   23.52 +consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
   23.53  recdef sep2 "measure length"
   23.54 -  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
   23.55 -  "sep2 xs       = (\\<lambda>a. xs)";
   23.56 +  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
   23.57 +  "sep2 xs       = (\<lambda>a. xs)";
   23.58  
   23.59  text{*
   23.60  Because of its pattern-matching syntax, \isacommand{recdef} is also useful
   23.61  for the definition of non-recursive functions:
   23.62  *}
   23.63  
   23.64 -consts swap12 :: "'a list \\<Rightarrow> 'a list";
   23.65 +consts swap12 :: "'a list \<Rightarrow> 'a list";
   23.66  recdef swap12 "{}"
   23.67    "swap12 (x#y#zs) = y#x#zs"
   23.68    "swap12 zs       = zs";
    24.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Sep 12 14:59:44 2000 +0200
    24.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Sep 12 15:43:15 2000 +0200
    24.3 @@ -11,7 +11,7 @@
    24.4  Let us look at an example:
    24.5  *}
    24.6  
    24.7 -consts gcd :: "nat*nat \\<Rightarrow> nat";
    24.8 +consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
    24.9  recdef gcd "measure (\\<lambda>(m,n).n)"
   24.10    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
   24.11  
   24.12 @@ -48,7 +48,7 @@
   24.13  following alternative definition suggests itself:
   24.14  *}
   24.15  
   24.16 -consts gcd1 :: "nat*nat \\<Rightarrow> nat";
   24.17 +consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
   24.18  recdef gcd1 "measure (\\<lambda>(m,n).n)"
   24.19    "gcd1 (m, 0) = m"
   24.20    "gcd1 (m, n) = gcd1(n, m mod n)";
   24.21 @@ -63,7 +63,7 @@
   24.22  is also available for @{typ"bool"} but is not split automatically:
   24.23  *}
   24.24  
   24.25 -consts gcd2 :: "nat*nat \\<Rightarrow> nat";
   24.26 +consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
   24.27  recdef gcd2 "measure (\\<lambda>(m,n).n)"
   24.28    "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
   24.29  
   24.30 @@ -83,7 +83,7 @@
   24.31  after which we can disable the original simplification rule:
   24.32  *}
   24.33  
   24.34 -lemmas [simp del] = gcd.simps;
   24.35 +declare gcd.simps [simp del]
   24.36  
   24.37  (*<*)
   24.38  end
    25.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Tue Sep 12 14:59:44 2000 +0200
    25.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Tue Sep 12 15:43:15 2000 +0200
    25.3 @@ -18,9 +18,9 @@
    25.4  termination of the following artificial function
    25.5  *}
    25.6  
    25.7 -consts f :: "nat*nat \\<Rightarrow> nat";
    25.8 -recdef f "measure(\\<lambda>(x,y). x-y)"
    25.9 -  "f(x,y) = (if x \\<le> y then x else f(x,y+1))";
   25.10 +consts f :: "nat\<times>nat \<Rightarrow> nat";
   25.11 +recdef f "measure(\<lambda>(x,y). x-y)"
   25.12 +  "f(x,y) = (if x \<le> y then x else f(x,y+1))";
   25.13  
   25.14  text{*\noindent
   25.15  is not proved automatically (although maybe it should be). Isabelle prints a
   25.16 @@ -29,7 +29,7 @@
   25.17  of your function once more. In our case the required lemma is the obvious one:
   25.18  *}
   25.19  
   25.20 -lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
   25.21 +lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
   25.22  
   25.23  txt{*\noindent
   25.24  It was not proved automatically because of the special nature of @{text"-"}
   25.25 @@ -40,13 +40,14 @@
   25.26  
   25.27  text{*\noindent
   25.28  Because \isacommand{recdef}'s termination prover involves simplification,
   25.29 -we have turned our lemma into a simplification rule. Therefore our second
   25.30 -attempt to define our function will automatically take it into account:
   25.31 +we include with our second attempt the hint to use @{thm[source]termi_lem} as
   25.32 +a simplification rule:
   25.33  *}
   25.34  
   25.35 -consts g :: "nat*nat \\<Rightarrow> nat";
   25.36 -recdef g "measure(\\<lambda>(x,y). x-y)"
   25.37 -  "g(x,y) = (if x \\<le> y then x else g(x,y+1))";
   25.38 +consts g :: "nat\<times>nat \<Rightarrow> nat";
   25.39 +recdef g "measure(\<lambda>(x,y). x-y)"
   25.40 +  "g(x,y) = (if x \<le> y then x else g(x,y+1))"
   25.41 +(hints simp: termi_lem)
   25.42  
   25.43  text{*\noindent
   25.44  This time everything works fine. Now @{thm[source]g.simps} contains precisely
   25.45 @@ -54,20 +55,17 @@
   25.46  rules. Thus we can automatically prove
   25.47  *}
   25.48  
   25.49 -theorem wow: "g(1,0) = g(1,1)";
   25.50 +theorem "g(1,0) = g(1,1)";
   25.51  by(simp);
   25.52  
   25.53  text{*\noindent
   25.54  More exciting theorems require induction, which is discussed below.
   25.55  
   25.56 -Because lemma @{thm[source]termi_lem} above was only turned into a
   25.57 -simplification rule for the sake of the termination proof, we may want to
   25.58 -disable it again:
   25.59 -*}
   25.60 +If the termination proof requires a new lemma that is of general use, you can
   25.61 +turn it permanently into a simplification rule, in which case the above
   25.62 +\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
   25.63 +sufficiently general to warrant this distinction.
   25.64  
   25.65 -lemmas [simp del] = termi_lem;
   25.66 -
   25.67 -text{*
   25.68  The attentive reader may wonder why we chose to call our function @{term"g"}
   25.69  rather than @{term"f"} the second time around. The reason is that, despite
   25.70  the failed termination proof, the definition of @{term"f"} did not
   25.71 @@ -87,7 +85,7 @@
   25.72  Ackermann's function requires the lexicographic product @{text"<*lex*>"}:
   25.73  *}
   25.74  
   25.75 -consts ack :: "nat*nat \\<Rightarrow> nat";
   25.76 +consts ack :: "nat\<times>nat \<Rightarrow> nat";
   25.77  recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
   25.78    "ack(0,n)         = Suc n"
   25.79    "ack(Suc m,0)     = ack(m, 1)"
    26.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Tue Sep 12 14:59:44 2000 +0200
    26.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Sep 12 15:43:15 2000 +0200
    26.3 @@ -81,8 +81,7 @@
    26.4  options:
    26.5  *};
    26.6  
    26.7 -lemmas [simp] = Let_def;
    26.8 -lemmas [split] = option.split;
    26.9 +declare Let_def[simp] option.split[split]
   26.10  
   26.11  text{*\noindent
   26.12  The reason becomes clear when looking (probably after a failed proof
    27.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Tue Sep 12 14:59:44 2000 +0200
    27.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Sep 12 15:43:15 2000 +0200
    27.3 @@ -72,8 +72,7 @@
    27.4  expand all \isa{let}s and to split all \isa{case}-constructs over
    27.5  options:%
    27.6  \end{isamarkuptext}%
    27.7 -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline
    27.8 -\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split%
    27.9 +\isacommand{declare}\ Let{\isacharunderscore}def{\isacharbrackleft}simp{\isacharbrackright}\ option{\isachardot}split{\isacharbrackleft}split{\isacharbrackright}%
   27.10  \begin{isamarkuptext}%
   27.11  \noindent
   27.12  The reason becomes clear when looking (probably after a failed proof
    28.1 --- a/doc-src/TutorialI/appendix.tex	Tue Sep 12 14:59:44 2000 +0200
    28.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Sep 12 15:43:15 2000 +0200
    28.3 @@ -55,7 +55,7 @@
    28.4  \hline\hline
    28.5  \indexboldpos{\isasymcirc}{$HOL1} &
    28.6  \indexboldpos{\isasymle}{$HOL2arithrel}&
    28.7 -&
    28.8 +\indexboldpos{\isasymtimes}{$IsaFun}&
    28.9  &
   28.10  &
   28.11  &
   28.12 @@ -66,7 +66,7 @@
   28.13   \\
   28.14  \ttindexbold{o} &
   28.15  \ttindexboldpos{<=}{$HOL2arithrel}&
   28.16 -&
   28.17 +\ttindexboldpos{*}{$HOL2arithfun} &
   28.18  &
   28.19  &
   28.20  &
    29.1 --- a/doc-src/TutorialI/basics.tex	Tue Sep 12 14:59:44 2000 +0200
    29.2 +++ b/doc-src/TutorialI/basics.tex	Tue Sep 12 15:43:15 2000 +0200
    29.3 @@ -73,7 +73,7 @@
    29.4  \begin{warn}
    29.5    HOL contains a theory \isaindexbold{Main}, the union of all the basic
    29.6    predefined theories like arithmetic, lists, sets, etc.\ (see the online
    29.7 -  library).  Unless you know what you are doing, always include \texttt{Main}
    29.8 +  library).  Unless you know what you are doing, always include \isa{Main}
    29.9    as a direct or indirect parent theory of all your theories.
   29.10  \end{warn}
   29.11  
    30.1 --- a/doc-src/TutorialI/fp.tex	Tue Sep 12 14:59:44 2000 +0200
    30.2 +++ b/doc-src/TutorialI/fp.tex	Tue Sep 12 15:43:15 2000 +0200
    30.3 @@ -225,29 +225,7 @@
    30.4  \end{warn}
    30.5  
    30.6  
    30.7 -\subsection{Case study: boolean expressions}
    30.8 -\label{sec:boolex}
    30.9 -
   30.10 -The aim of this case study is twofold: it shows how to model boolean
   30.11 -expressions and some algorithms for manipulating them, and it demonstrates
   30.12 -the constructs introduced above.
   30.13 -
   30.14  \input{Ifexpr/document/Ifexpr.tex}
   30.15 -\medskip
   30.16 -
   30.17 -How does one come up with the required lemmas? Try to prove the main theorems
   30.18 -without them and study carefully what \isa{auto} leaves unproved. This has
   30.19 -to provide the clue.  The necessity of universal quantification
   30.20 -(\isa{\isasymforall{}t e}) in the two lemmas is explained in
   30.21 -\S\ref{sec:InductionHeuristics}
   30.22 -
   30.23 -\begin{exercise}
   30.24 -  We strengthen the definition of a \isa{normal} If-expression as follows:
   30.25 -  the first argument of all \isa{IF}s must be a variable. Adapt the above
   30.26 -  development to this changed requirement. (Hint: you may need to formulate
   30.27 -  some of the goals as implications (\isasymimp) rather than equalities
   30.28 -  (\isa{=}).)
   30.29 -\end{exercise}
   30.30  
   30.31  \section{Some basic types}
   30.32  
   30.33 @@ -417,9 +395,10 @@
   30.34  \begin{ttbox}\makeatother
   30.35  (0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
   30.36  \end{ttbox}
   30.37 -This is also known as \bfindex{term rewriting} and the equations are referred
   30.38 -to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
   30.39 -because the terms do not necessarily become simpler in the process.
   30.40 +This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
   30.41 +equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
   30.42 +``Rewriting'' is more honest than ``simplification'' because the terms do not
   30.43 +necessarily become simpler in the process.
   30.44  
   30.45  \input{Misc/document/simp.tex}
   30.46  
   30.47 @@ -592,12 +571,4 @@
   30.48  
   30.49  \index{induction!recursion|)}
   30.50  \index{recursion induction|)}
   30.51 -
   30.52 -\subsection{Advanced forms of recursion}
   30.53 -\label{sec:advanced-recdef}
   30.54 -
   30.55 -\input{Recdef/document/Nested0.tex}
   30.56 -\input{Recdef/document/Nested1.tex}
   30.57 -\input{Recdef/document/Nested2.tex}
   30.58 -
   30.59  \index{*recdef|)}
    31.1 --- a/doc-src/TutorialI/tricks.tex	Tue Sep 12 14:59:44 2000 +0200
    31.2 +++ b/doc-src/TutorialI/tricks.tex	Tue Sep 12 15:43:15 2000 +0200
    31.3 @@ -1,36 +1,24 @@
    31.4 -\chapter{The Tricks of the Trade}
    31.5 -
    31.6 -\section{Simplification}
    31.7 -\label{sec:simplification-II}
    31.8 -\index{simplification|(}
    31.9 -
   31.10 -\subsection{Advanced features}
   31.11 -
   31.12 -\subsubsection{Congruence rules}
   31.13 -
   31.14 -
   31.15 -\subsubsection{Permutative rewrite rules}
   31.16 +%\chapter{The Tricks of the Trade}
   31.17 +\chapter{Advanced Simplification, Recursion, and Induction}
   31.18 +\markboth{}{CHAPTER 4: ADVANCED}
   31.19  
   31.20 -A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
   31.21 -side are the same up to renaming of variables.  The most common permutative
   31.22 -rule is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.
   31.23 -Such rules are problematic because once they apply, they can be used forever.
   31.24 -The simplifier is aware of this danger and treats permutative rules
   31.25 -separately. For details see~\cite{isabelle-ref}.
   31.26 -
   31.27 -
   31.28 +Although we have already learned a lot about simplification, recursion and
   31.29 +induction, there are some advanced proof techniques that we have not covered
   31.30 +yet and which are worth knowing about if you intend to beome a serious
   31.31 +(human) theorem prover. The three sections of this chapter are almost
   31.32 +independent of each other and can be read in any order. Only the notion of
   31.33 +\emph{congruence rules}, introduced in the section on simplification, is
   31.34 +required for parts of the section on recursion.
   31.35  
   31.36 -\subsection{How it works}
   31.37 -\label{sec:SimpHow}
   31.38 -
   31.39 -\subsubsection{Higher-order patterns}
   31.40 +\input{Advanced/document/simp.tex}
   31.41  
   31.42 -\subsubsection{Local assumptions}
   31.43 -
   31.44 -\subsubsection{The preprocessor}
   31.45 -
   31.46 -\index{simplification|)}
   31.47 -
   31.48 +\section{Advanced forms of recursion}
   31.49 +\label{sec:advanced-recdef}
   31.50 +\index{*recdef|(}
   31.51 +\input{Recdef/document/Nested0.tex}
   31.52 +\input{Recdef/document/Nested1.tex}
   31.53 +\input{Recdef/document/Nested2.tex}
   31.54 +\index{*recdef|)}
   31.55  
   31.56  \section{Advanced induction techniques}
   31.57  \label{sec:advanced-ind}