*** empty log message ***
authornipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654458068404143
parent 10653 55f33da63366
child 10655 ddd33e0f4935
*** empty log message ***
doc-src/TutorialI/Advanced/Partial.thy
doc-src/TutorialI/Advanced/ROOT.ML
doc-src/TutorialI/Advanced/WFrec.thy
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/Advanced/document/Partial.tex
doc-src/TutorialI/Advanced/document/WFrec.tex
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/Inductive/Even.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/examples.thy
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Types/Axioms.thy
doc-src/TutorialI/Types/Overloading2.thy
doc-src/TutorialI/Types/Pairs.thy
doc-src/TutorialI/Types/Typedef.thy
doc-src/TutorialI/Types/document/Axioms.tex
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/document/Pairs.tex
doc-src/TutorialI/Types/document/Typedef.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -0,0 +1,213 @@
     1.4 +(*<*)theory Partial = While_Combinator:(*>*)
     1.5 +
     1.6 +text{*\noindent
     1.7 +Throughout the tutorial we have emphasized the fact that all functions
     1.8 +in HOL are total. Hence we cannot hope to define truly partial
     1.9 +functions. The best we can do are functions that are
    1.10 +\emph{underdefined}\index{underdefined function}:
    1.11 +for certain arguments we only know that a result
    1.12 +exists, but we don't know what it is. When defining functions that are
    1.13 +normally considered partial, underdefinedness turns out to be a very
    1.14 +reasonable alternative.
    1.15 +
    1.16 +We have already seen an instance of underdefinedness by means of
    1.17 +non-exhaustive pattern matching: the definition of @{term last} in
    1.18 +\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}
    1.19 +*}
    1.20 +
    1.21 +consts hd :: "'a list \<Rightarrow> 'a"
    1.22 +primrec "hd (x#xs) = x"
    1.23 +
    1.24 +text{*\noindent
    1.25 +although it generates a warning.
    1.26 +
    1.27 +Even ordinary definitions allow underdefinedness, this time by means of
    1.28 +preconditions:
    1.29 +*}
    1.30 +
    1.31 +constdefs minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.32 +"n \<le> m \<Longrightarrow> minus m n \<equiv> m - n"
    1.33 +
    1.34 +text{*
    1.35 +The rest of this section is devoted to the question of how to define
    1.36 +partial recursive functions by other means that non-exhaustive pattern
    1.37 +matching.
    1.38 +*}
    1.39 +
    1.40 +subsubsection{*Guarded recursion*}
    1.41 +
    1.42 +text{* Neither \isacommand{primrec} nor \isacommand{recdef} allow to
    1.43 +prefix an equation with a condition in the way ordinary definitions do
    1.44 +(see @{term minus} above). Instead we have to move the condition over
    1.45 +to the right-hand side of the equation. Given a partial function $f$
    1.46 +that should satisfy the recursion equation $f(x) = t$ over its domain
    1.47 +$dom(f)$, we turn this into the \isacommand{recdef}
    1.48 +@{prop[display]"f(x) = (if x \<in> dom(f) then t else arbitrary)"}
    1.49 +where @{term arbitrary} is a predeclared constant of type @{typ 'a}
    1.50 +which has no definition. Thus we know nothing about its value,
    1.51 +which is ideal for specifying underdefined functions on top of it.
    1.52 +
    1.53 +As a simple example we define division on @{typ nat}:
    1.54 +*}
    1.55 +
    1.56 +consts divi :: "nat \<times> nat \<Rightarrow> nat"
    1.57 +recdef divi "measure(\<lambda>(m,n). m)"
    1.58 +  "divi(m,n) = (if n = 0 then arbitrary else
    1.59 +                if m < n then 0 else divi(m-n,n)+1)"
    1.60 +
    1.61 +text{*\noindent Of course we could also have defined
    1.62 +@{term"divi(m,0)"} to be some specific number, for example 0. The
    1.63 +latter option is chosen for the predefined @{text div} function, which
    1.64 +simplifies proofs at the expense of moving further away from the
    1.65 +standard mathematical divison function.
    1.66 +
    1.67 +As a more substantial example we consider the problem of searching a graph.
    1.68 +For simplicity our graph is given by a function (@{term f}) of
    1.69 +type @{typ"'a \<Rightarrow> 'a"} which
    1.70 +maps each node to its successor, and the task is to find the end of a chain,
    1.71 +i.e.\ a node pointing to itself. Here is a first attempt:
    1.72 +@{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
    1.73 +This may be viewed as a fixed point finder or as one half of the well known
    1.74 +\emph{Union-Find} algorithm.
    1.75 +The snag is that it may not terminate if @{term f} has nontrivial cycles.
    1.76 +Phrased differently, the relation
    1.77 +*}
    1.78 +
    1.79 +constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set"
    1.80 +  "step1 f \<equiv> {(y,x). y = f x \<and> y \<noteq> x}"
    1.81 +
    1.82 +text{*\noindent
    1.83 +must be well-founded. Thus we make the following definition:
    1.84 +*}
    1.85 +
    1.86 +consts find :: "('a \<Rightarrow> 'a) \<times> 'a \<Rightarrow> 'a"
    1.87 +recdef find "same_fst (\<lambda>f. wf(step1 f)) step1"
    1.88 +  "find(f,x) = (if wf(step1 f)
    1.89 +                then if f x = x then x else find(f, f x)
    1.90 +                else arbitrary)"
    1.91 +(hints recdef_simp:same_fst_def step1_def)
    1.92 +
    1.93 +text{*\noindent
    1.94 +The recursion equation itself should be clear enough: it is our aborted
    1.95 +first attempt augmented with a check that there are no non-trivial loops.
    1.96 +
    1.97 +What complicates the termination proof is that the argument of
    1.98 +@{term find} is a pair. To express the required well-founded relation
    1.99 +we employ the predefined combinator @{term same_fst} of type
   1.100 +@{text[display]"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b\<times>'b)set) \<Rightarrow> (('a\<times>'b) \<times> ('a\<times>'b))set"}
   1.101 +defined as
   1.102 +@{thm[display]same_fst_def[no_vars]}
   1.103 +This combinator is designed for recursive functions on pairs where the first
   1.104 +component of the argument is passed unchanged to all recursive
   1.105 +calls. Given a constraint on the first component and a relation on the second
   1.106 +component, @{term same_fst} builds the required relation on pairs.
   1.107 +The theorem @{thm[display]wf_same_fst[no_vars]}
   1.108 +is known to the well-foundedness prover of \isacommand{recdef}.
   1.109 +Thus well-foundedness of the given relation is immediate.
   1.110 +Furthermore, each recursive call descends along the given relation:
   1.111 +the first argument stays unchanged and the second one descends along
   1.112 +@{term"step1 f"}. The proof merely requires unfolding of some definitions.
   1.113 +
   1.114 +Normally you will then derive the following conditional variant of and from
   1.115 +the recursion equation
   1.116 +*}
   1.117 +
   1.118 +lemma [simp]:
   1.119 +  "wf(step1 f) \<Longrightarrow> find(f,x) = (if f x = x then x else find(f, f x))"
   1.120 +by simp
   1.121 +
   1.122 +text{*\noindent and then disable the original recursion equation:*}
   1.123 +
   1.124 +declare find.simps[simp del]
   1.125 +
   1.126 +text{*
   1.127 +We can reason about such underdefined functions just like about any other
   1.128 +recursive function. Here is a simple example of recursion induction:
   1.129 +*}
   1.130 +
   1.131 +lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
   1.132 +apply(induct_tac f x rule:find.induct);
   1.133 +apply simp
   1.134 +done
   1.135 +
   1.136 +subsubsection{*The {\tt\slshape while} combinator*}
   1.137 +
   1.138 +text{*If the recursive function happens to be tail recursive, its
   1.139 +definition becomes a triviality if based on the predefined \isaindexbold{while}
   1.140 +combinator.  The latter lives in the library theory
   1.141 +\isa{While_Combinator}, which is not part of @{text Main} but needs to
   1.142 +be included explicitly among the ancestor theories.
   1.143 +
   1.144 +Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
   1.145 +and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}
   1.146 +That is, @{term"while b c s"} is equivalent to the imperative program
   1.147 +\begin{verbatim}
   1.148 +     x := s; while b(x) do x := c(x); return x
   1.149 +\end{verbatim}
   1.150 +In general, @{term s} will be a tuple (better still: a record). As an example
   1.151 +consider the tail recursive variant of function @{term find} above:
   1.152 +*}
   1.153 +
   1.154 +constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   1.155 +  "find2 f x \<equiv>
   1.156 +   fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"
   1.157 +
   1.158 +text{*\noindent
   1.159 +The loop operates on two ``local variables'' @{term x} and @{term x'}
   1.160 +containing the ``current'' and the ``next'' value of function @{term f}.
   1.161 +They are initalized with the global @{term x} and @{term"f x"}. At the
   1.162 +end @{term fst} selects the local @{term x}.
   1.163 +
   1.164 +This looks like we can define at least tail recursive functions
   1.165 +without bothering about termination after all. But there is no free
   1.166 +lunch: when proving properties of functions defined by @{term while},
   1.167 +termination rears its ugly head again. Here is
   1.168 +@{thm[source]while_rule}, the well known proof rule for total
   1.169 +correctness of loops expressed with @{term while}:
   1.170 +@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be
   1.171 +true of the initial state @{term s} and invariant under @{term c}
   1.172 +(premises 1 and 2).The post-condition @{term Q} must become true when
   1.173 +leaving the loop (premise 3). And each loop iteration must descend
   1.174 +along a well-founded relation @{term r} (premises 4 and 5).
   1.175 +
   1.176 +Let us now prove that @{term find2} does indeed find a fixed point. Instead
   1.177 +of induction we apply the above while rule, suitably instantiated.
   1.178 +Only the final premise of @{thm[source]while_rule} is left unproved
   1.179 +by @{text auto} but falls to @{text simp}:
   1.180 +*}
   1.181 +
   1.182 +lemma lem: "\<lbrakk> wf(step1 f); x' = f x \<rbrakk> \<Longrightarrow> \<exists>y y'.
   1.183 +   while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,x') = (y,y') \<and>
   1.184 +   y' = y \<and> f y = y"
   1.185 +apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
   1.186 +               r = "inv_image (step1 f) fst" in while_rule);
   1.187 +apply auto
   1.188 +apply(simp add:inv_image_def step1_def)
   1.189 +done
   1.190 +
   1.191 +text{*
   1.192 +The theorem itself is a simple consequence of this lemma:
   1.193 +*}
   1.194 +
   1.195 +theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"
   1.196 +apply(drule_tac x = x in lem)
   1.197 +apply(auto simp add:find2_def)
   1.198 +done
   1.199 +
   1.200 +text{* Let us conclude this section on partial functions by a
   1.201 +discussion of the merits of the @{term while} combinator. We have
   1.202 +already seen that the advantage (if it is one) of not having to
   1.203 +provide a termintion argument when defining a function via @{term
   1.204 +while} merely puts off the evil hour. On top of that, tail recursive
   1.205 +functions tend to be more complicated to reason about. So why use
   1.206 +@{term while} at all? The only reason is executability: the recursion
   1.207 +equation for @{term while} is a directly executable functional
   1.208 +program. This is in stark contrast to guarded recursion as introduced
   1.209 +above which requires an explicit test @{prop"x \<in> dom f"} in the
   1.210 +function body.  Unless @{term dom} is trivial, this leads to a
   1.211 +definition which is either not at all executable or prohibitively
   1.212 +expensive. Thus, if you are aiming for an efficiently executable definition
   1.213 +of a partial function, you are likely to need @{term while}.
   1.214 +*}
   1.215 +
   1.216 +(*<*)end(*>*)
     2.1 --- a/doc-src/TutorialI/Advanced/ROOT.ML	Wed Dec 13 09:32:55 2000 +0100
     2.2 +++ b/doc-src/TutorialI/Advanced/ROOT.ML	Wed Dec 13 09:39:53 2000 +0100
     2.3 @@ -1,3 +1,4 @@
     2.4  use "../settings.ML";
     2.5  use_thy "simp";
     2.6  use_thy "WFrec";
     2.7 +use_thy "Partial";
     3.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Dec 13 09:32:55 2000 +0100
     3.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Dec 13 09:39:53 2000 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  functions. Sometimes this can be quite inconvenient or even
     3.5  impossible. Fortunately, \isacommand{recdef} supports much more
     3.6  general definitions. For example, termination of Ackermann's function
     3.7 -can be shown by means of the lexicographic product @{text"<*lex*>"}:
     3.8 +can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
     3.9  *}
    3.10  
    3.11  consts ack :: "nat\<times>nat \<Rightarrow> nat";
    3.12 @@ -80,6 +80,7 @@
    3.13  
    3.14  text{*\noindent
    3.15  and should have appended the following hint to our above definition:
    3.16 +\indexbold{*recdef_wf}
    3.17  *}
    3.18  (*<*)
    3.19  consts g :: "nat \<Rightarrow> nat"
    3.20 @@ -87,5 +88,5 @@
    3.21  "g 0 = 0"
    3.22  "g (Suc n) = g n"
    3.23  (*>*)
    3.24 -(hints recdef_wf add: wf_id)
    3.25 +(hints recdef_wf: wf_id)
    3.26  (*<*)end(*>*)
     4.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Wed Dec 13 09:32:55 2000 +0100
     4.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Wed Dec 13 09:39:53 2000 +0100
     4.3 @@ -13,9 +13,10 @@
     4.4  \section{Advanced forms of recursion}
     4.5  \index{*recdef|(}
     4.6  
     4.7 -The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It
     4.8 -covers two topics: how to define recursive function over nested recursive datatypes
     4.9 -and how to establish termination by means other than measure functions.
    4.10 +The purpose of this section is to introduce advanced forms of
    4.11 +\isacommand{recdef}: how to define recursive function over nested recursive
    4.12 +datatypes, how to establish termination by means other than measure functions,
    4.13 +and how to deal with partial functions.
    4.14  
    4.15  If, after reading this section, you feel that the definition of recursive
    4.16  functions is overly and maybe unnecessarily complicated by the requirement of
    4.17 @@ -32,12 +33,17 @@
    4.18  \input{Recdef/document/Nested0.tex}
    4.19  \input{Recdef/document/Nested1.tex}
    4.20  \input{Recdef/document/Nested2.tex}
    4.21 -\index{*recdef|)}
    4.22  
    4.23  \subsection{Beyond measure}
    4.24  \label{sec:beyond-measure}
    4.25  \input{Advanced/document/WFrec.tex}
    4.26  
    4.27 +\subsection{Partial functions}
    4.28 +\index{partial function}
    4.29 +\input{Advanced/document/Partial.tex}
    4.30 +
    4.31 +\index{*recdef|)}
    4.32 +
    4.33  \section{Advanced induction techniques}
    4.34  \label{sec:advanced-ind}
    4.35  \index{induction|(}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Wed Dec 13 09:39:53 2000 +0100
     5.3 @@ -0,0 +1,225 @@
     5.4 +%
     5.5 +\begin{isabellebody}%
     5.6 +\def\isabellecontext{Partial}%
     5.7 +%
     5.8 +\begin{isamarkuptext}%
     5.9 +\noindent
    5.10 +Throughout the tutorial we have emphasized the fact that all functions
    5.11 +in HOL are total. Hence we cannot hope to define truly partial
    5.12 +functions. The best we can do are functions that are
    5.13 +\emph{underdefined}\index{underdefined function}:
    5.14 +for certain arguments we only know that a result
    5.15 +exists, but we don't know what it is. When defining functions that are
    5.16 +normally considered partial, underdefinedness turns out to be a very
    5.17 +reasonable alternative.
    5.18 +
    5.19 +We have already seen an instance of underdefinedness by means of
    5.20 +non-exhaustive pattern matching: the definition of \isa{last} in
    5.21 +\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%
    5.22 +\end{isamarkuptext}%
    5.23 +\isacommand{consts}\ hd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
    5.24 +\isacommand{primrec}\ {\isachardoublequote}hd\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}%
    5.25 +\begin{isamarkuptext}%
    5.26 +\noindent
    5.27 +although it generates a warning.
    5.28 +
    5.29 +Even ordinary definitions allow underdefinedness, this time by means of
    5.30 +preconditions:%
    5.31 +\end{isamarkuptext}%
    5.32 +\isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    5.33 +{\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}%
    5.34 +\begin{isamarkuptext}%
    5.35 +The rest of this section is devoted to the question of how to define
    5.36 +partial recursive functions by other means that non-exhaustive pattern
    5.37 +matching.%
    5.38 +\end{isamarkuptext}%
    5.39 +%
    5.40 +\isamarkupsubsubsection{Guarded recursion%
    5.41 +}
    5.42 +%
    5.43 +\begin{isamarkuptext}%
    5.44 +Neither \isacommand{primrec} nor \isacommand{recdef} allow to
    5.45 +prefix an equation with a condition in the way ordinary definitions do
    5.46 +(see \isa{minus} above). Instead we have to move the condition over
    5.47 +to the right-hand side of the equation. Given a partial function $f$
    5.48 +that should satisfy the recursion equation $f(x) = t$ over its domain
    5.49 +$dom(f)$, we turn this into the \isacommand{recdef}
    5.50 +\begin{isabelle}%
    5.51 +\ \ \ \ \ f\ x\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymin}\ dom\ f\ then\ t\ else\ arbitrary{\isacharparenright}%
    5.52 +\end{isabelle}
    5.53 +where \isa{arbitrary} is a predeclared constant of type \isa{{\isacharprime}a}
    5.54 +which has no definition. Thus we know nothing about its value,
    5.55 +which is ideal for specifying underdefined functions on top of it.
    5.56 +
    5.57 +As a simple example we define division on \isa{nat}:%
    5.58 +\end{isamarkuptext}%
    5.59 +\isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    5.60 +\isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
    5.61 +\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline
    5.62 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
    5.63 +\begin{isamarkuptext}%
    5.64 +\noindent Of course we could also have defined
    5.65 +\isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The
    5.66 +latter option is chosen for the predefined \isa{div} function, which
    5.67 +simplifies proofs at the expense of moving further away from the
    5.68 +standard mathematical divison function.
    5.69 +
    5.70 +As a more substantial example we consider the problem of searching a graph.
    5.71 +For simplicity our graph is given by a function (\isa{f}) of
    5.72 +type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
    5.73 +maps each node to its successor, and the task is to find the end of a chain,
    5.74 +i.e.\ a node pointing to itself. Here is a first attempt:
    5.75 +\begin{isabelle}%
    5.76 +\ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
    5.77 +\end{isabelle}
    5.78 +This may be viewed as a fixed point finder or as one half of the well known
    5.79 +\emph{Union-Find} algorithm.
    5.80 +The snag is that it may not terminate if \isa{f} has nontrivial cycles.
    5.81 +Phrased differently, the relation%
    5.82 +\end{isamarkuptext}%
    5.83 +\isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
    5.84 +\ \ {\isachardoublequote}step{\isadigit{1}}\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymand}\ y\ {\isasymnoteq}\ x{\isacharbraceright}{\isachardoublequote}%
    5.85 +\begin{isamarkuptext}%
    5.86 +\noindent
    5.87 +must be well-founded. Thus we make the following definition:%
    5.88 +\end{isamarkuptext}%
    5.89 +\isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
    5.90 +\isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline
    5.91 +\ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline
    5.92 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline
    5.93 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline
    5.94 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
    5.95 +\begin{isamarkuptext}%
    5.96 +\noindent
    5.97 +The recursion equation itself should be clear enough: it is our aborted
    5.98 +first attempt augmented with a check that there are no non-trivial loops.
    5.99 +
   5.100 +What complicates the termination proof is that the argument of
   5.101 +\isa{find} is a pair. To express the required well-founded relation
   5.102 +we employ the predefined combinator \isa{same{\isacharunderscore}fst} of type
   5.103 +\begin{isabelle}%
   5.104 +\ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%
   5.105 +\end{isabelle}
   5.106 +defined as
   5.107 +\begin{isabelle}%
   5.108 +\ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%
   5.109 +\end{isabelle}
   5.110 +This combinator is designed for recursive functions on pairs where the first
   5.111 +component of the argument is passed unchanged to all recursive
   5.112 +calls. Given a constraint on the first component and a relation on the second
   5.113 +component, \isa{same{\isacharunderscore}fst} builds the required relation on pairs.
   5.114 +The theorem \begin{isabelle}%
   5.115 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%
   5.116 +\end{isabelle}
   5.117 +is known to the well-foundedness prover of \isacommand{recdef}.
   5.118 +Thus well-foundedness of the given relation is immediate.
   5.119 +Furthermore, each recursive call descends along the given relation:
   5.120 +the first argument stays unchanged and the second one descends along
   5.121 +\isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions.
   5.122 +
   5.123 +Normally you will then derive the following conditional variant of and from
   5.124 +the recursion equation%
   5.125 +\end{isamarkuptext}%
   5.126 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
   5.127 +\ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
   5.128 +\isacommand{by}\ simp%
   5.129 +\begin{isamarkuptext}%
   5.130 +\noindent and then disable the original recursion equation:%
   5.131 +\end{isamarkuptext}%
   5.132 +\isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
   5.133 +\begin{isamarkuptext}%
   5.134 +We can reason about such underdefined functions just like about any other
   5.135 +recursive function. Here is a simple example of recursion induction:%
   5.136 +\end{isamarkuptext}%
   5.137 +\isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
   5.138 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
   5.139 +\isacommand{apply}\ simp\isanewline
   5.140 +\isacommand{done}%
   5.141 +\isamarkupsubsubsection{The {\tt\slshape while} combinator%
   5.142 +}
   5.143 +%
   5.144 +\begin{isamarkuptext}%
   5.145 +If the recursive function happens to be tail recursive, its
   5.146 +definition becomes a triviality if based on the predefined \isaindexbold{while}
   5.147 +combinator.  The latter lives in the library theory
   5.148 +\isa{While_Combinator}, which is not part of \isa{Main} but needs to
   5.149 +be included explicitly among the ancestor theories.
   5.150 +
   5.151 +Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
   5.152 +and satisfies the recursion equation \begin{isabelle}%
   5.153 +\ \ \ \ \ while\ b\ c\ s\ {\isacharequal}\ {\isacharparenleft}if\ b\ s\ then\ while\ b\ c\ {\isacharparenleft}c\ s{\isacharparenright}\ else\ s{\isacharparenright}%
   5.154 +\end{isabelle}
   5.155 +That is, \isa{while\ b\ c\ s} is equivalent to the imperative program
   5.156 +\begin{verbatim}
   5.157 +     x := s; while b(x) do x := c(x); return x
   5.158 +\end{verbatim}
   5.159 +In general, \isa{s} will be a tuple (better still: a record). As an example
   5.160 +consider the tail recursive variant of function \isa{find} above:%
   5.161 +\end{isamarkuptext}%
   5.162 +\isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
   5.163 +\ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
   5.164 +\ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   5.165 +\begin{isamarkuptext}%
   5.166 +\noindent
   5.167 +The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}
   5.168 +containing the ``current'' and the ``next'' value of function \isa{f}.
   5.169 +They are initalized with the global \isa{x} and \isa{f\ x}. At the
   5.170 +end \isa{fst} selects the local \isa{x}.
   5.171 +
   5.172 +This looks like we can define at least tail recursive functions
   5.173 +without bothering about termination after all. But there is no free
   5.174 +lunch: when proving properties of functions defined by \isa{while},
   5.175 +termination rears its ugly head again. Here is
   5.176 +\isa{while{\isacharunderscore}rule}, the well known proof rule for total
   5.177 +correctness of loops expressed with \isa{while}:
   5.178 +\begin{isabelle}%
   5.179 +\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
   5.180 +\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
   5.181 +\ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
   5.182 +\ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
   5.183 +\end{isabelle} \isa{P} needs to be
   5.184 +true of the initial state \isa{s} and invariant under \isa{c}
   5.185 +(premises 1 and 2).The post-condition \isa{Q} must become true when
   5.186 +leaving the loop (premise 3). And each loop iteration must descend
   5.187 +along a well-founded relation \isa{r} (premises 4 and 5).
   5.188 +
   5.189 +Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead
   5.190 +of induction we apply the above while rule, suitably instantiated.
   5.191 +Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved
   5.192 +by \isa{auto} but falls to \isa{simp}:%
   5.193 +\end{isamarkuptext}%
   5.194 +\isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}y\ y{\isacharprime}{\isachardot}\isanewline
   5.195 +\ \ \ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharprime}{\isacharparenright}\ {\isasymand}\isanewline
   5.196 +\ \ \ y{\isacharprime}\ {\isacharequal}\ y\ {\isasymand}\ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline
   5.197 +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline
   5.198 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline
   5.199 +\isacommand{apply}\ auto\isanewline
   5.200 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
   5.201 +\isacommand{done}%
   5.202 +\begin{isamarkuptext}%
   5.203 +The theorem itself is a simple consequence of this lemma:%
   5.204 +\end{isamarkuptext}%
   5.205 +\isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline
   5.206 +\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline
   5.207 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
   5.208 +\isacommand{done}%
   5.209 +\begin{isamarkuptext}%
   5.210 +Let us conclude this section on partial functions by a
   5.211 +discussion of the merits of the \isa{while} combinator. We have
   5.212 +already seen that the advantage (if it is one) of not having to
   5.213 +provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
   5.214 +functions tend to be more complicated to reason about. So why use
   5.215 +\isa{while} at all? The only reason is executability: the recursion
   5.216 +equation for \isa{while} is a directly executable functional
   5.217 +program. This is in stark contrast to guarded recursion as introduced
   5.218 +above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the
   5.219 +function body.  Unless \isa{dom} is trivial, this leads to a
   5.220 +definition which is either not at all executable or prohibitively
   5.221 +expensive. Thus, if you are aiming for an efficiently executable definition
   5.222 +of a partial function, you are likely to need \isa{while}.%
   5.223 +\end{isamarkuptext}%
   5.224 +\end{isabellebody}%
   5.225 +%%% Local Variables:
   5.226 +%%% mode: latex
   5.227 +%%% TeX-master: "root"
   5.228 +%%% End:
     6.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Dec 13 09:32:55 2000 +0100
     6.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Dec 13 09:39:53 2000 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  functions. Sometimes this can be quite inconvenient or even
     6.5  impossible. Fortunately, \isacommand{recdef} supports much more
     6.6  general definitions. For example, termination of Ackermann's function
     6.7 -can be shown by means of the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
     6.8 +can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
     6.9  \end{isamarkuptext}%
    6.10  \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    6.11  \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
    6.12 @@ -76,9 +76,10 @@
    6.13  \isacommand{by}\ simp%
    6.14  \begin{isamarkuptext}%
    6.15  \noindent
    6.16 -and should have appended the following hint to our above definition:%
    6.17 +and should have appended the following hint to our above definition:
    6.18 +\indexbold{*recdef_wf}%
    6.19  \end{isamarkuptext}%
    6.20 -{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf\ add{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%
    6.21 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%
    6.22  %%% Local Variables:
    6.23  %%% mode: latex
    6.24  %%% TeX-master: "root"
     7.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Wed Dec 13 09:32:55 2000 +0100
     7.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Dec 13 09:39:53 2000 +0100
     7.3 @@ -182,7 +182,7 @@
     7.4  text{*\noindent
     7.5  Element @{term"n+1"} on this path is some arbitrary successor
     7.6  @{term t} of element @{term n} such that @{term"P t"} holds.  Remember that @{text"SOME t. R t"}
     7.7 -is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
     7.8 +is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
     7.9  course, such a @{term t} may in general not exist, but that is of no
    7.10  concern to us since we will only use @{term path} in such cases where a
    7.11  suitable @{term t} does exist.
     8.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Dec 13 09:32:55 2000 +0100
     8.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Dec 13 09:39:53 2000 +0100
     8.3 @@ -139,7 +139,7 @@
     8.4  \noindent
     8.5  Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
     8.6  \isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
     8.7 -is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
     8.8 +is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
     8.9  course, such a \isa{t} may in general not exist, but that is of no
    8.10  concern to us since we will only use \isa{path} in such cases where a
    8.11  suitable \isa{t} does exist.
     9.1 --- a/doc-src/TutorialI/Inductive/Even.tex	Wed Dec 13 09:32:55 2000 +0100
     9.2 +++ b/doc-src/TutorialI/Inductive/Even.tex	Wed Dec 13 09:39:53 2000 +0100
     9.3 @@ -179,8 +179,10 @@
     9.4  \ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even%
     9.5  \end{isabelle}
     9.6  The first one is hopeless.  In general, rule inductions involving
     9.7 -non-trivial terms will probably go wrong.  The solution is easy provided
     9.8 -we have the necessary inverses, here subtraction:
     9.9 +non-trivial terms will probably go wrong. How to deal with such situations
    9.10 +in general is described in {\S}\ref{sec:ind-var-in-prems} below.
    9.11 +In the current case the solution is easy because
    9.12 +we have the necessary inverse, subtraction:
    9.13  \begin{isabelle}
    9.14  \isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline
    9.15  \isacommand{apply}\ (erule\ even.induct)\isanewline
    10.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Dec 13 09:32:55 2000 +0100
    10.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Dec 13 09:39:53 2000 +0100
    10.3 @@ -23,6 +23,9 @@
    10.4  	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    10.5  
    10.6  styles:
    10.7 +	@rm -f isabelle.sty
    10.8 +	@rm -f isabellesym.sty
    10.9 +	@rm -f pdfsetup.sty
   10.10  	@$(ISATOOL) latex -o sty >/dev/null
   10.11  	@rm -f pdfsetup.sty
   10.12  	@rm -f */document/isabelle.sty
   10.13 @@ -98,7 +101,8 @@
   10.14  
   10.15  HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
   10.16  
   10.17 -$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy
   10.18 +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
   10.19 +	Advanced/Partial.thy
   10.20  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
   10.21  	@rm -f tutorial.dvi
   10.22  
    11.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Dec 13 09:32:55 2000 +0100
    11.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Dec 13 09:39:53 2000 +0100
    11.3 @@ -290,8 +290,5 @@
    11.4  example theorem @{thm[source]nat_less_induct} can be viewed (and derived) as
    11.5  a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
    11.6  @{typ nat}. The details can be found in the HOL library.
    11.7 -*};
    11.8 -
    11.9 -(*<*)
   11.10 -end
   11.11 -(*>*)
   11.12 +*}
   11.13 +(*<*)end(*>*)
    12.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 13 09:32:55 2000 +0100
    12.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 13 09:39:53 2000 +0100
    12.3 @@ -29,7 +29,8 @@
    12.4  \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
    12.5  \isaindexbold{max} are predefined, as are the relations
    12.6  \indexboldpos{\isasymle}{$HOL2arithrel} and
    12.7 -\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
    12.8 +\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
    12.9 +\isa{m\ {\isacharless}\ n}. There is even a least number operation
   12.10  \isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
   12.11  Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
   12.12  and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
   12.13 @@ -69,7 +70,9 @@
   12.14  (which attacks the first subgoal). It proves arithmetic goals involving the
   12.15  usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
   12.16  \isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
   12.17 -\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. For example,%
   12.18 +\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
   12.19 +known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   12.20 +For example,%
   12.21  \end{isamarkuptext}%
   12.22  \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
   12.23  \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}%
   12.24 @@ -88,8 +91,8 @@
   12.25    of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   12.26    \isaindexbold{max} because they are first eliminated by case distinctions.
   12.27  
   12.28 -  \isa{arith} is incomplete even for the restricted class of formulae
   12.29 -  described above (known as ``linear arithmetic''). If divisibility plays a
   12.30 +  \isa{arith} is incomplete even for the restricted class of
   12.31 +  linear arithmetic formulae. If divisibility plays a
   12.32    role, it may fail to prove a valid formula, for example
   12.33    \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
   12.34  \end{warn}%
    13.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 13 09:32:55 2000 +0100
    13.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 13 09:39:53 2000 +0100
    13.3 @@ -27,7 +27,8 @@
    13.4  \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
    13.5  \isaindexbold{max} are predefined, as are the relations
    13.6  \indexboldpos{\isasymle}{$HOL2arithrel} and
    13.7 -\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
    13.8 +\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
    13.9 +@{prop"m<n"}. There is even a least number operation
   13.10  \isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
   13.11  Isabelle does not prove this completely automatically. Note that @{term 1}
   13.12  and @{term 2} are available as abbreviations for the corresponding
   13.13 @@ -69,7 +70,9 @@
   13.14  (which attacks the first subgoal). It proves arithmetic goals involving the
   13.15  usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
   13.16  @{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
   13.17 -@{text"+"}, @{text"-"}, @{term min} and @{term max}. For example,
   13.18 +@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
   13.19 +known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   13.20 +For example,
   13.21  *}
   13.22  
   13.23  lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
   13.24 @@ -92,8 +95,8 @@
   13.25    of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   13.26    \isaindexbold{max} because they are first eliminated by case distinctions.
   13.27  
   13.28 -  \isa{arith} is incomplete even for the restricted class of formulae
   13.29 -  described above (known as ``linear arithmetic''). If divisibility plays a
   13.30 +  \isa{arith} is incomplete even for the restricted class of
   13.31 +  linear arithmetic formulae. If divisibility plays a
   13.32    role, it may fail to prove a valid formula, for example
   13.33    @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
   13.34  \end{warn}
    14.1 --- a/doc-src/TutorialI/Misc/simp.thy	Wed Dec 13 09:32:55 2000 +0100
    14.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Wed Dec 13 09:39:53 2000 +0100
    14.3 @@ -227,7 +227,7 @@
    14.4  
    14.5  subsubsection{*Automatic case splits*}
    14.6  
    14.7 -text{*\indexbold{case splits}\index{*split|(}
    14.8 +text{*\indexbold{case splits}\index{*split (method, attr.)|(}
    14.9  Goals containing @{text"if"}-expressions are usually proved by case
   14.10  distinction on the condition of the @{text"if"}. For example the goal
   14.11  *}
   14.12 @@ -235,40 +235,39 @@
   14.13  lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
   14.14  
   14.15  txt{*\noindent
   14.16 -can be split by a degenerate form of simplification
   14.17 +can be split by a special method @{text split}:
   14.18  *}
   14.19  
   14.20 -apply(simp only: split: split_if);
   14.21 +apply(split split_if)
   14.22  
   14.23  txt{*\noindent
   14.24  @{subgoals[display,indent=0]}
   14.25 -where no simplification rules are included (@{text"only:"} is followed by the
   14.26 -empty list of theorems) but the rule \isaindexbold{split_if} for
   14.27 -splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
   14.28 +where \isaindexbold{split_if} is a theorem that expresses splitting of
   14.29 +@{text"if"}s. Because
   14.30  case-splitting on @{text"if"}s is almost always the right proof strategy, the
   14.31  simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
   14.32  on the initial goal above.
   14.33  
   14.34  This splitting idea generalizes from @{text"if"} to \isaindex{case}:
   14.35 -*}(*<*)oops;(*>*)
   14.36 -
   14.37 +*}(*<*)by simp(*>*)
   14.38  lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
   14.39 -apply(simp only: split: list.split);
   14.40 +apply(split list.split);
   14.41  
   14.42  txt{*
   14.43  @{subgoals[display,indent=0]}
   14.44  In contrast to @{text"if"}-expressions, the simplifier does not split
   14.45  @{text"case"}-expressions by default because this can lead to nontermination
   14.46 -in case of recursive datatypes. Again, if the @{text"only:"} modifier is
   14.47 -dropped, the above goal is solved,
   14.48 +in case of recursive datatypes. Therefore the simplifier has a modifier
   14.49 +@{text split} for adding further splitting rules explicitly. This means the
   14.50 +above lemma can be proved in one step by
   14.51  *}
   14.52  (*<*)oops;
   14.53  lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
   14.54  (*>*)
   14.55  apply(simp split: list.split);
   14.56  (*<*)done(*>*)
   14.57 -text{*\noindent%
   14.58 -which \isacommand{apply}@{text"(simp)"} alone will not do.
   14.59 +text{*\noindent
   14.60 +whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.
   14.61  
   14.62  In general, every datatype $t$ comes with a theorem
   14.63  $t$@{text".split"} which can be declared to be a \bfindex{split rule} either
   14.64 @@ -294,14 +293,19 @@
   14.65  declare list.split [split del]
   14.66  
   14.67  text{*
   14.68 +In polished proofs the @{text split} method is rarely used on its own
   14.69 +but always as part of the simplifier. However, if a goal contains
   14.70 +multiple splittable constructs, the @{text split} method can be
   14.71 +helpful in selectively exploring the effects of splitting.
   14.72 +
   14.73  The above split rules intentionally only affect the conclusion of a
   14.74  subgoal.  If you want to split an @{text"if"} or @{text"case"}-expression in
   14.75  the assumptions, you have to apply @{thm[source]split_if_asm} or
   14.76  $t$@{text".split_asm"}:
   14.77  *}
   14.78  
   14.79 -lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
   14.80 -apply(simp only: split: split_if_asm);
   14.81 +lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
   14.82 +apply(split split_if_asm)
   14.83  
   14.84  txt{*\noindent
   14.85  In contrast to splitting the conclusion, this actually creates two
   14.86 @@ -318,15 +322,12 @@
   14.87    same is true for \isaindex{case}-expressions: only the selector is
   14.88    simplified at first, until either the expression reduces to one of the
   14.89    cases or it is split.
   14.90 -\end{warn}
   14.91 -
   14.92 -\index{*split|)}
   14.93 +\end{warn}\index{*split (method, attr.)|)}
   14.94  *}
   14.95  (*<*)
   14.96  by(simp_all)
   14.97  (*>*)
   14.98  
   14.99 -
  14.100  subsubsection{*Arithmetic*}
  14.101  
  14.102  text{*\index{arithmetic}
    15.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Wed Dec 13 09:32:55 2000 +0100
    15.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Wed Dec 13 09:39:53 2000 +0100
    15.3 @@ -80,7 +80,7 @@
    15.4  
    15.5  text{*\noindent
    15.6  or declare them globally
    15.7 -by giving them the @{text recdef_cong} attribute as in
    15.8 +by giving them the \isaindexbold{recdef_cong} attribute as in
    15.9  *}
   15.10  
   15.11  declare map_cong[recdef_cong];
    16.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 13 09:32:55 2000 +0100
    16.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 13 09:39:53 2000 +0100
    16.3 @@ -75,7 +75,7 @@
    16.4  \begin{isamarkuptext}%
    16.5  \noindent
    16.6  or declare them globally
    16.7 -by giving them the \isa{recdef{\isacharunderscore}cong} attribute as in%
    16.8 +by giving them the \isaindexbold{recdef_cong} attribute as in%
    16.9  \end{isamarkuptext}%
   16.10  \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
   16.11  \begin{isamarkuptext}%
    17.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Wed Dec 13 09:32:55 2000 +0100
    17.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Wed Dec 13 09:39:53 2000 +0100
    17.3 @@ -33,6 +33,8 @@
    17.4  \noindent
    17.5  This time the measure is the length of the list, which decreases with the
    17.6  recursive call; the first component of the argument tuple is irrelevant.
    17.7 +The details of tupled $\lambda$-abstractions \isa{{\isasymlambda}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlsub n{\isacharparenright}} are
    17.8 +explained in \S\ref{sec:products}, but for now your intuition is all you need.
    17.9  
   17.10  Pattern matching need not be exhaustive:%
   17.11  \end{isamarkuptext}%
    18.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 13 09:32:55 2000 +0100
    18.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 13 09:39:53 2000 +0100
    18.3 @@ -39,7 +39,7 @@
    18.4  \noindent
    18.5  Because \isacommand{recdef}'s termination prover involves simplification,
    18.6  we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
    18.7 -a simplification rule:%
    18.8 +a simplification rule:\indexbold{*recdef_simp}%
    18.9  \end{isamarkuptext}%
   18.10  \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   18.11  \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
    19.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Wed Dec 13 09:32:55 2000 +0100
    19.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Wed Dec 13 09:39:53 2000 +0100
    19.3 @@ -35,6 +35,8 @@
    19.4  text{*\noindent
    19.5  This time the measure is the length of the list, which decreases with the
    19.6  recursive call; the first component of the argument tuple is irrelevant.
    19.7 +The details of tupled $\lambda$-abstractions @{text"\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)"} are
    19.8 +explained in \S\ref{sec:products}, but for now your intuition is all you need.
    19.9  
   19.10  Pattern matching need not be exhaustive:
   19.11  *}
    20.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Wed Dec 13 09:32:55 2000 +0100
    20.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Dec 13 09:39:53 2000 +0100
    20.3 @@ -42,7 +42,7 @@
    20.4  text{*\noindent
    20.5  Because \isacommand{recdef}'s termination prover involves simplification,
    20.6  we include with our second attempt the hint to use @{thm[source]termi_lem} as
    20.7 -a simplification rule:
    20.8 +a simplification rule:\indexbold{*recdef_simp}
    20.9  *}
   20.10  
   20.11  consts g :: "nat\<times>nat \<Rightarrow> nat";
    21.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Dec 13 09:32:55 2000 +0100
    21.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Dec 13 09:39:53 2000 +0100
    21.3 @@ -69,7 +69,8 @@
    21.4  \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
    21.5  particularly primitive kind where each recursive call peels off a datatype
    21.6  constructor from one of the arguments.  Thus the
    21.7 -recursion always terminates, i.e.\ the function is \bfindex{total}.
    21.8 +recursion always terminates, i.e.\ the function is \textbf{total}.
    21.9 +\index{total function}
   21.10  
   21.11  The termination requirement is absolutely essential in HOL, a logic of total
   21.12  functions. If we were to drop it, inconsistencies would quickly arise: the
    22.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Dec 13 09:32:55 2000 +0100
    22.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Dec 13 09:39:53 2000 +0100
    22.3 @@ -67,7 +67,8 @@
    22.4  \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
    22.5  particularly primitive kind where each recursive call peels off a datatype
    22.6  constructor from one of the arguments.  Thus the
    22.7 -recursion always terminates, i.e.\ the function is \bfindex{total}.
    22.8 +recursion always terminates, i.e.\ the function is \textbf{total}.
    22.9 +\index{total function}
   22.10  
   22.11  The termination requirement is absolutely essential in HOL, a logic of total
   22.12  functions. If we were to drop it, inconsistencies would quickly arise: the
    23.1 --- a/doc-src/TutorialI/Types/Axioms.thy	Wed Dec 13 09:32:55 2000 +0100
    23.2 +++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Dec 13 09:39:53 2000 +0100
    23.3 @@ -114,7 +114,7 @@
    23.4  Linear orders are an example of subclassing by construction, which is the most
    23.5  common case. It is also possible to prove additional subclass relationships
    23.6  later on, i.e.\ subclassing by proof. This is the topic of the following
    23.7 -section.
    23.8 +paragraph.
    23.9  *}
   23.10  
   23.11  subsubsection{*Strict orders*}
    24.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Dec 13 09:32:55 2000 +0100
    24.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Dec 13 09:39:53 2000 +0100
    24.3 @@ -37,11 +37,11 @@
    24.4  @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
    24.5  @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
    24.6  @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
    24.7 -@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} \\
    24.8 +@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & $\mid~\mid$\\
    24.9  @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   24.10  @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
   24.11  @{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
   24.12 -@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
   24.13 +@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"}
   24.14  \end{tabular}
   24.15  \caption{Overloaded constants in HOL}
   24.16  \label{tab:overloading}
    25.1 --- a/doc-src/TutorialI/Types/Pairs.thy	Wed Dec 13 09:32:55 2000 +0100
    25.2 +++ b/doc-src/TutorialI/Types/Pairs.thy	Wed Dec 13 09:39:53 2000 +0100
    25.3 @@ -39,7 +39,8 @@
    25.4  different terms).
    25.5  
    25.6  Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
    25.7 -@{term split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
    25.8 +@{term split}\indexbold{*split (constant)}
    25.9 +is the uncurrying function of type @{text"('a \<Rightarrow> 'b
   25.10  \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
   25.11  \begin{center}
   25.12  @{thm split_def}
   25.13 @@ -78,7 +79,7 @@
   25.14  *}
   25.15  
   25.16  lemma "(\<lambda>(x,y).y) p = snd p"
   25.17 -apply(simp only: split:split_split);
   25.18 +apply(split split_split);
   25.19  
   25.20  txt{*
   25.21  @{subgoals[display,indent=0]}
   25.22 @@ -191,10 +192,10 @@
   25.23  In case you would like to turn off this automatic splitting, just disable the
   25.24  responsible simplification rules:
   25.25  \begin{center}
   25.26 -@{thm split_paired_All}
   25.27 +@{thm split_paired_All[no_vars]}
   25.28  \hfill
   25.29  (@{thm[source]split_paired_All})\\
   25.30 -@{thm split_paired_Ex}
   25.31 +@{thm split_paired_Ex[no_vars]}
   25.32  \hfill
   25.33  (@{thm[source]split_paired_Ex})
   25.34  \end{center}
    26.1 --- a/doc-src/TutorialI/Types/Typedef.thy	Wed Dec 13 09:32:55 2000 +0100
    26.2 +++ b/doc-src/TutorialI/Types/Typedef.thy	Wed Dec 13 09:39:53 2000 +0100
    26.3 @@ -199,7 +199,7 @@
    26.4  @{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
    26.5  representation: *}
    26.6  
    26.7 -lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow>  Q(n::nat)";
    26.8 +lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow>  Q n";
    26.9  
   26.10  txt{*\noindent
   26.11  Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
    27.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex	Wed Dec 13 09:32:55 2000 +0100
    27.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Dec 13 09:39:53 2000 +0100
    27.3 @@ -118,7 +118,7 @@
    27.4  Linear orders are an example of subclassing by construction, which is the most
    27.5  common case. It is also possible to prove additional subclass relationships
    27.6  later on, i.e.\ subclassing by proof. This is the topic of the following
    27.7 -section.%
    27.8 +paragraph.%
    27.9  \end{isamarkuptext}%
   27.10  %
   27.11  \isamarkupsubsubsection{Strict orders%
    28.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Dec 13 09:32:55 2000 +0100
    28.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Dec 13 09:39:53 2000 +0100
    28.3 @@ -39,11 +39,11 @@
    28.4  \isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
    28.5  \isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
    28.6  \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
    28.7 -\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
    28.8 +\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & $\mid~\mid$\\
    28.9  \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   28.10  \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
   28.11  \isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
   28.12 -\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
   28.13 +\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}
   28.14  \end{tabular}
   28.15  \caption{Overloaded constants in HOL}
   28.16  \label{tab:overloading}
    29.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Wed Dec 13 09:32:55 2000 +0100
    29.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Wed Dec 13 09:39:53 2000 +0100
    29.3 @@ -44,7 +44,8 @@
    29.4  different terms).
    29.5  
    29.6  Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
    29.7 -\isa{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
    29.8 +\isa{split}\indexbold{*split (constant)}
    29.9 +is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
   29.10  \begin{center}
   29.11  \isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
   29.12  \hfill(\isa{split{\isacharunderscore}def})
   29.13 @@ -80,7 +81,7 @@
   29.14  rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:%
   29.15  \end{isamarkuptext}%
   29.16  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
   29.17 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}split{\isacharunderscore}split{\isacharparenright}%
   29.18 +\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}%
   29.19  \begin{isamarkuptxt}%
   29.20  \begin{isabelle}%
   29.21  \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p%
   29.22 @@ -184,10 +185,10 @@
   29.23  In case you would like to turn off this automatic splitting, just disable the
   29.24  responsible simplification rules:
   29.25  \begin{center}
   29.26 -\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ {\isacharquery}P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   29.27 +\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   29.28  \hfill
   29.29  (\isa{split{\isacharunderscore}paired{\isacharunderscore}All})\\
   29.30 -\isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ {\isacharquery}P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   29.31 +\isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   29.32  \hfill
   29.33  (\isa{split{\isacharunderscore}paired{\isacharunderscore}Ex})
   29.34  \end{center}%
    30.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex	Wed Dec 13 09:32:55 2000 +0100
    30.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex	Wed Dec 13 09:39:53 2000 +0100
    30.3 @@ -198,7 +198,7 @@
    30.4  \isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the
    30.5  representation:%
    30.6  \end{isamarkuptext}%
    30.7 -\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharcolon}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}%
    30.8 +\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharcolon}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}%
    30.9  \begin{isamarkuptxt}%
   30.10  \noindent
   30.11  Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
    31.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Dec 13 09:32:55 2000 +0100
    31.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Wed Dec 13 09:39:53 2000 +0100
    31.3 @@ -243,7 +243,7 @@
    31.4  operators.  The name \isa{zadd_ac} refers to the associativity and
    31.5  commutativity theorems for integer addition, while \isa{zmult_ac} has the
    31.6  analogous theorems for multiplication.  The prefix~\isa{z} in many theorem
    31.7 -names recalls the use of $\Bbb{Z}$ to denote the set of integers.
    31.8 +names recalls the use of $Z$ to denote the set of integers.
    31.9  
   31.10  For division and remainder, the treatment of negative divisors follows
   31.11  traditional mathematical practice: the sign of the remainder follows that
    32.1 --- a/doc-src/TutorialI/appendix.tex	Wed Dec 13 09:32:55 2000 +0100
    32.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Dec 13 09:39:53 2000 +0100
    32.3 @@ -96,34 +96,43 @@
    32.4  \label{fig:ascii}
    32.5  \end{figure}\indexbold{ASCII symbols}
    32.6  
    32.7 -
    32.8  \begin{figure}[htbp]
    32.9  \begin{center}
   32.10 -\begin{tabular}{|lllll|}
   32.11 +\begin{tabular}{|lllllllll|}
   32.12  \hline
   32.13  \texttt{ALL} &
   32.14 +\texttt{BIT} &
   32.15 +\texttt{CHR} &
   32.16 +\texttt{EX} &
   32.17 +\texttt{GOAL} &
   32.18 +\texttt{INT} &
   32.19 +\texttt{Int} &
   32.20 +\texttt{LEAST} &
   32.21 +\texttt{O} \\
   32.22 +\texttt{OFCLASS} &
   32.23 +\texttt{PI} &
   32.24 +\texttt{PROP} &
   32.25 +\texttt{SIGMA} &
   32.26 +\texttt{SOME} &
   32.27 +\texttt{TYPE} &
   32.28 +\texttt{UN} &
   32.29 +\texttt{Un} &\\
   32.30  \texttt{case} &
   32.31 +\texttt{choose} &
   32.32  \texttt{div} &
   32.33  \texttt{dvd} &
   32.34 -\texttt{else} \\
   32.35 -\texttt{EX} &
   32.36 +\texttt{else} &
   32.37 +\texttt{funcset} &
   32.38  \texttt{if} &
   32.39  \texttt{in} &
   32.40 -\texttt{INT} &
   32.41 -\texttt{Int} \\
   32.42 -\texttt{LEAST} &
   32.43 +\texttt{lam} \\
   32.44  \texttt{let} &
   32.45 +\texttt{mem} &
   32.46  \texttt{mod} &
   32.47 -\texttt{O} &
   32.48 -\texttt{o} \\
   32.49 +\texttt{o} &
   32.50  \texttt{of} &
   32.51  \texttt{op} &
   32.52 -\texttt{PROP} &
   32.53 -\texttt{SIGMA} &
   32.54 -\texttt{then} \\
   32.55 -\texttt{Times} &
   32.56 -\texttt{UN} &
   32.57 -\texttt{Un} &&\\
   32.58 +\texttt{then}&&\\
   32.59  \hline
   32.60  \end{tabular}
   32.61  \end{center}
    33.1 --- a/doc-src/TutorialI/fp.tex	Wed Dec 13 09:32:55 2000 +0100
    33.2 +++ b/doc-src/TutorialI/fp.tex	Wed Dec 13 09:39:53 2000 +0100
    33.3 @@ -206,7 +206,7 @@
    33.4  such that $C$ is a constructor of the datatype $t$ and all recursive calls of
    33.5  $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
    33.6  Isabelle immediately sees that $f$ terminates because one (fixed!) argument
    33.7 -becomes smaller with every recursive call. There must be exactly one equation
    33.8 +becomes smaller with every recursive call. There must be at most one equation
    33.9  for each constructor.  Their order is immaterial.
   33.10  A more general method for defining total recursive functions is introduced in
   33.11  {\S}\ref{sec:recdef}.
   33.12 @@ -472,7 +472,7 @@
   33.13  more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
   33.14  
   33.15  \subsection{Defining recursive functions}
   33.16 -
   33.17 +\label{sec:recdef-examples}
   33.18  \input{Recdef/document/examples.tex}
   33.19  
   33.20  \subsection{Proving termination}
    34.1 --- a/doc-src/TutorialI/todo.tobias	Wed Dec 13 09:32:55 2000 +0100
    34.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Dec 13 09:39:53 2000 +0100
    34.3 @@ -3,8 +3,6 @@
    34.4  
    34.5  Relation: comp -> composition
    34.6  
    34.7 -replace "simp only split" by "split_tac".
    34.8 -
    34.9  Add map_cong?? (upto 10% slower)
   34.10  
   34.11  Recdef: Get rid of function name in header.
   34.12 @@ -14,7 +12,7 @@
   34.13  -> new example in Recdef/termination
   34.14  
   34.15  a tactic for replacing a specific occurrence:
   34.16 -apply(substitute [2] thm)
   34.17 +apply(subst [2] thm)
   34.18  
   34.19  it would be nice if @term could deal with ?-vars.
   34.20  then a number of (unchecked!) @texts could be converted to @terms.
   34.21 @@ -37,16 +35,16 @@
   34.22  Minor fixes in the tutorial
   34.23  ===========================
   34.24  
   34.25 +adjust type of ^ in tab:overloading
   34.26 +
   34.27  explanation of term "contrapositive"/contraposition in Rules?
   34.28  Index the notion and maybe the rules contrapos_xy
   34.29  
   34.30 -Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
   34.31 -AdvancedInd section.
   34.32 +If Advanced and Types chapter ar swapped:
   34.33 +Make forward ref from ... = True in Axioms to preprocessor section.
   34.34  
   34.35  get rid of use_thy in tutorial?
   34.36  
   34.37 -Explain typographic conventions?
   34.38 -
   34.39  Orderings on numbers (with hint that it is overloaded):
   34.40  bounded quantifers ALL x<y, <=.
   34.41  
   34.42 @@ -78,6 +76,7 @@
   34.43  ==============================================
   34.44  
   34.45  Tacticals: , ? +
   34.46 +Note: + is used in typedef section!
   34.47  
   34.48  Mention that simp etc (big step tactics) insist on change?
   34.49  
   34.50 @@ -87,9 +86,6 @@
   34.51  A list of further useful commands (rules? tricks?)
   34.52  prefer, defer, print_simpset (-> print_simps?)
   34.53  
   34.54 -An overview of the automatic methods: simp, auto, fast, blast, force,
   34.55 -clarify, clarsimp (intro, elim?)
   34.56 -
   34.57  Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
   34.58  Where explained? Should go into a separate section as Inductive needs it as
   34.59  well.
   34.60 @@ -124,6 +120,15 @@
   34.61  Ind. sets: define ABC inductively and prove
   34.62  ABC = {rep A n @ rep B n @ rep C n. True}
   34.63  
   34.64 +Partial rekursive functions / Nontermination:
   34.65 +
   34.66 +Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
   34.67 +(What about sum? Is there one, a unique one?)
   34.68 +
   34.69 +Exercise
   34.70 +Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
   34.71 +Prove 0 <= i ==> sum i = i*(i+1) via while-rule
   34.72 +
   34.73  Possible examples/case studies
   34.74  ==============================
   34.75  
   34.76 @@ -145,6 +150,12 @@
   34.77  
   34.78  Sorting with comp-parameter and with type class (<)
   34.79  
   34.80 +Recdef:more example proofs:
   34.81 + if-normalization with measure function,
   34.82 + nested if-normalization,
   34.83 + quicksort
   34.84 + Trie?
   34.85 +
   34.86  New book by Bird?
   34.87  
   34.88  Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
   34.89 @@ -166,60 +177,7 @@
   34.90  
   34.91  A look at the library?
   34.92  Map.
   34.93 -If WF is discussed, make a link to it from AdvancedInd.
   34.94  
   34.95  Prototyping?
   34.96  
   34.97  ==============================================================
   34.98 -Recdef:
   34.99 -
  34.100 -nested recursion
  34.101 -more example proofs:
  34.102 - if-normalization with measure function,
  34.103 - nested if-normalization,
  34.104 - quicksort
  34.105 - Trie?
  34.106 -a case study?
  34.107 -
  34.108 -----------
  34.109 -
  34.110 -Partial rekursive functions / Nontermination
  34.111 -
  34.112 -What appears to be the problem:
  34.113 -axiom f n = f n + 1
  34.114 -lemma False
  34.115 -apply(cut_facts_tac axiom, simp).
  34.116 -
  34.117 -1. Guarded recursion
  34.118 -
  34.119 -Scheme:
  34.120 -f x = if $x \in dom(f)$ then ... else arbitrary
  34.121 -
  34.122 -Example: sum/fact: int -> int (for no good reason because we have nat)
  34.123 -
  34.124 -Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
  34.125 -(What about sum? Is there one, a unique one?)
  34.126 -
  34.127 -[Alternative: include argument that is counted down
  34.128 - f x n = if n=0 then None else ...
  34.129 -Refer to Boyer and Moore]
  34.130 -
  34.131 -More complex: same_fst
  34.132 -
  34.133 -chase(f,x) = if wf{(f x,x) . f x ~= x}
  34.134 -             then if f x = x then x else chase(f,f x)
  34.135 -             else arb
  34.136 -
  34.137 -Prove wf ==> f(chase(f,x)) = chase(f,x)
  34.138 -
  34.139 -2. While / Tail recursion
  34.140 -
  34.141 -chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
  34.142 -
  34.143 -==> unfold eqn for chase? Prove fixpoint property?
  34.144 -
  34.145 -Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
  34.146 -Prove 0 <= i ==> sum i = i*(i+1) via while-rule
  34.147 -
  34.148 -Mention prototyping?
  34.149 -==============================================================
    35.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:32:55 2000 +0100
    35.2 +++ b/doc-src/TutorialI/tutorial.tex	Wed Dec 13 09:39:53 2000 +0100
    35.3 @@ -45,8 +45,10 @@
    35.4  \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
    35.5  \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
    35.6  
    35.7 +\index{termination|see{total function}}
    35.8  \index{product type|see{pair}}
    35.9  \index{tuple|see{pair}}
   35.10 +\index{*<*lex*>|see{lexicographic product}}
   35.11  
   35.12  \underscoreoff
   35.13