1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Partial}% |
3 \def\isabellecontext{Partial}% |
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \noindent |
6 \noindent Throughout the tutorial we have emphasized the fact |
7 Throughout the tutorial we have emphasized the fact that all functions |
7 that all functions in HOL are total. Hence we cannot hope to define |
8 in HOL are total. Hence we cannot hope to define truly partial |
8 truly partial functions but must totalize them. A straightforward |
9 functions. The best we can do are functions that are |
9 totalization is to lift the result type of the function from $\tau$ to |
10 \emph{underdefined}\index{underdefined function}: |
10 $\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is |
11 for certain arguments we only know that a result |
11 returned if the function is applied to an argument not in its |
12 exists, but we do not know what it is. When defining functions that are |
12 domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example. |
13 normally considered partial, underdefinedness turns out to be a very |
13 We do not pursue this schema further because it should be clear |
14 reasonable alternative. |
14 how it works. Its main drawback is that the result of such a lifted |
|
15 function has to be unpacked first before it can be processed |
|
16 further. Its main advantage is that you can distinguish if the |
|
17 function was applied to an argument in its domain or not. If you do |
|
18 not need to make this distinction, for example because the function is |
|
19 never used outside its domain, it is easier to work with |
|
20 \emph{underdefined}\index{underdefined function} functions: for |
|
21 certain arguments we only know that a result exists, but we do not |
|
22 know what it is. When defining functions that are normally considered |
|
23 partial, underdefinedness turns out to be a very reasonable |
|
24 alternative. |
15 |
25 |
16 We have already seen an instance of underdefinedness by means of |
26 We have already seen an instance of underdefinedness by means of |
17 non-exhaustive pattern matching: the definition of \isa{last} in |
27 non-exhaustive pattern matching: the definition of \isa{last} in |
18 \S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}% |
28 \S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}% |
19 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
62 latter option is chosen for the predefined \isa{div} function, which |
72 latter option is chosen for the predefined \isa{div} function, which |
63 simplifies proofs at the expense of deviating from the |
73 simplifies proofs at the expense of deviating from the |
64 standard mathematical division function. |
74 standard mathematical division function. |
65 |
75 |
66 As a more substantial example we consider the problem of searching a graph. |
76 As a more substantial example we consider the problem of searching a graph. |
67 For simplicity our graph is given by a function (\isa{f}) of |
77 For simplicity our graph is given by a function \isa{f} of |
68 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which |
78 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which |
69 maps each node to its successor, i.e.\ the graph is really a tree. |
79 maps each node to its successor, i.e.\ the graph is really a tree. |
70 The task is to find the end of a chain, modelled by a node pointing to |
80 The task is to find the end of a chain, modelled by a node pointing to |
71 itself. Here is a first attempt: |
81 itself. Here is a first attempt: |
72 \begin{isabelle}% |
82 \begin{isabelle}% |
91 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% |
101 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}% |
92 \begin{isamarkuptext}% |
102 \begin{isamarkuptext}% |
93 \noindent |
103 \noindent |
94 The recursion equation itself should be clear enough: it is our aborted |
104 The recursion equation itself should be clear enough: it is our aborted |
95 first attempt augmented with a check that there are no non-trivial loops. |
105 first attempt augmented with a check that there are no non-trivial loops. |
96 |
106 To express the required well-founded relation we employ the |
97 What complicates the termination proof is that the argument of \isa{find} |
|
98 is a pair. To express the required well-founded relation we employ the |
|
99 predefined combinator \isa{same{\isacharunderscore}fst} of type |
107 predefined combinator \isa{same{\isacharunderscore}fst} of type |
100 \begin{isabelle}% |
108 \begin{isabelle}% |
101 \ \ \ \ \ {\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% |
109 \ \ \ \ \ {\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% |
102 \end{isabelle} |
110 \end{isabelle} |
103 defined as |
111 defined as |
186 Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead |
194 Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead |
187 of induction we apply the above while rule, suitably instantiated. |
195 of induction we apply the above while rule, suitably instantiated. |
188 Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved |
196 Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved |
189 by \isa{auto} but falls to \isa{simp}:% |
197 by \isa{auto} but falls to \isa{simp}:% |
190 \end{isamarkuptext}% |
198 \end{isamarkuptext}% |
191 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline |
199 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
192 \ \ \ {\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 |
200 \ \ {\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}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline |
193 \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
201 \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
194 \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 |
202 \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 |
195 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline |
203 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline |
196 \isacommand{apply}\ auto\isanewline |
204 \isacommand{apply}\ auto\isanewline |
197 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline |
205 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline |