1.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 12 16:05:12 2001 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 12 16:07:20 2001 +0100
1.3 @@ -34,7 +34,7 @@
1.4 matching.%
1.5 \end{isamarkuptext}%
1.6 %
1.7 -\isamarkupsubsubsection{Guarded recursion%
1.8 +\isamarkupsubsubsection{Guarded Recursion%
1.9 }
1.10 %
1.11 \begin{isamarkuptext}%
1.12 @@ -61,8 +61,8 @@
1.13 \noindent Of course we could also have defined
1.14 \isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The
1.15 latter option is chosen for the predefined \isa{div} function, which
1.16 -simplifies proofs at the expense of moving further away from the
1.17 -standard mathematical divison function.
1.18 +simplifies proofs at the expense of deviating from the
1.19 +standard mathematical division function.
1.20
1.21 As a more substantial example we consider the problem of searching a graph.
1.22 For simplicity our graph is given by a function (\isa{f}) of
1.23 @@ -135,13 +135,13 @@
1.24 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
1.25 \isacommand{apply}\ simp\isanewline
1.26 \isacommand{done}%
1.27 -\isamarkupsubsubsection{The {\tt\slshape while} combinator%
1.28 +\isamarkupsubsubsection{The {\tt\slshape while} Combinator%
1.29 }
1.30 %
1.31 \begin{isamarkuptext}%
1.32 If the recursive function happens to be tail recursive, its
1.33 definition becomes a triviality if based on the predefined \isaindexbold{while}
1.34 -combinator. The latter lives in the library theory
1.35 +combinator. The latter lives in the Library theory
1.36 \isa{While_Combinator}, which is not part of \isa{Main} but needs to
1.37 be included explicitly among the ancestor theories.
1.38
1.39 @@ -179,18 +179,18 @@
1.40 \ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
1.41 \end{isabelle} \isa{P} needs to be
1.42 true of the initial state \isa{s} and invariant under \isa{c}
1.43 -(premises 1 and 2).The post-condition \isa{Q} must become true when
1.44 -leaving the loop (premise 3). And each loop iteration must descend
1.45 -along a well-founded relation \isa{r} (premises 4 and 5).
1.46 +(premises 1 and~2). The post-condition \isa{Q} must become true when
1.47 +leaving the loop (premise~3). And each loop iteration must descend
1.48 +along a well-founded relation \isa{r} (premises 4 and~5).
1.49
1.50 Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead
1.51 of induction we apply the above while rule, suitably instantiated.
1.52 Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved
1.53 by \isa{auto} but falls to \isa{simp}:%
1.54 \end{isamarkuptext}%
1.55 -\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
1.56 -\ \ \ 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
1.57 -\ \ \ y{\isacharprime}\ {\isacharequal}\ y\ {\isasymand}\ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline
1.58 +\isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
1.59 +\ \ \ {\isasymexists}y{\isachardot}\ 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{\isacharparenright}\ {\isasymand}\isanewline
1.60 +\ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline
1.61 \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
1.62 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline
1.63 \isacommand{apply}\ auto\isanewline
1.64 @@ -214,8 +214,8 @@
1.65 program. This is in stark contrast to guarded recursion as introduced
1.66 above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the
1.67 function body. Unless \isa{dom} is trivial, this leads to a
1.68 -definition which is either not at all executable or prohibitively
1.69 -expensive. Thus, if you are aiming for an efficiently executable definition
1.70 +definition that is impossible to execute (or prohibitively slow).
1.71 +Thus, if you are aiming for an efficiently executable definition
1.72 of a partial function, you are likely to need \isa{while}.%
1.73 \end{isamarkuptext}%
1.74 \end{isabellebody}%