doc-src/TutorialI/Advanced/Partial.thy
author wenzelm
Wed, 19 Oct 2005 21:52:07 +0200
changeset 17914 99ead7a7eb42
parent 15904 a6fb4ddc05c7
child 19248 25bb0a883ac5
permissions -rw-r--r--
fix headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 15904
diff changeset
     1
(*<*)theory Partial imports While_Combinator begin(*>*)
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
     2
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
     3
text{*\noindent Throughout this tutorial, we have emphasized
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
     4
that all functions in HOL are total.  We cannot hope to define
11310
51e70b7bc315 spelling check
paulson
parents: 11285
diff changeset
     5
truly partial functions, but must make them total.  A straightforward
51e70b7bc315 spelling check
paulson
parents: 11285
diff changeset
     6
method is to lift the result type of the function from $\tau$ to
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
     7
$\tau$~@{text option} (see \ref{sec:option}), where @{term None} is
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
     8
returned if the function is applied to an argument not in its
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
     9
domain. Function @{term assoc} in \S\ref{sec:Trie} is a simple example.
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    10
We do not pursue this schema further because it should be clear
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    11
how it works. Its main drawback is that the result of such a lifted
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    12
function has to be unpacked first before it can be processed
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    13
further. Its main advantage is that you can distinguish if the
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    14
function was applied to an argument in its domain or not. If you do
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    15
not need to make this distinction, for example because the function is
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    16
never used outside its domain, it is easier to work with
11428
332347b9b942 tidying the index
paulson
parents: 11310
diff changeset
    17
\emph{underdefined}\index{functions!underdefined} functions: for
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    18
certain arguments we only know that a result exists, but we do not
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    19
know what it is. When defining functions that are normally considered
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    20
partial, underdefinedness turns out to be a very reasonable
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    21
alternative.
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    22
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    23
We have already seen an instance of underdefinedness by means of
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    24
non-exhaustive pattern matching: the definition of @{term last} in
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    25
\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    26
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    27
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    28
consts hd :: "'a list \<Rightarrow> 'a"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    29
primrec "hd (x#xs) = x"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    30
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    31
text{*\noindent
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    32
although it generates a warning.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    33
Even ordinary definitions allow underdefinedness, this time by means of
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    34
preconditions:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    35
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    36
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    37
constdefs minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    38
"n \<le> m \<Longrightarrow> minus m n \<equiv> m - n"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    39
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    40
text{*
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    41
The rest of this section is devoted to the question of how to define
11256
49afcce3bada *** empty log message ***
nipkow
parents: 11196
diff changeset
    42
partial recursive functions by other means than non-exhaustive pattern
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    43
matching.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    44
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    45
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
    46
subsubsection{*Guarded Recursion*}
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    47
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    48
text{* 
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    49
\index{recursion!guarded}%
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    50
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    51
prefix an equation with a condition in the way ordinary definitions do
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
    52
(see @{const minus} above). Instead we have to move the condition over
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    53
to the right-hand side of the equation. Given a partial function $f$
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    54
that should satisfy the recursion equation $f(x) = t$ over its domain
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    55
$dom(f)$, we turn this into the \isacommand{recdef}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    56
@{prop[display]"f(x) = (if x \<in> dom(f) then t else arbitrary)"}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    57
where @{term arbitrary} is a predeclared constant of type @{typ 'a}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    58
which has no definition. Thus we know nothing about its value,
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    59
which is ideal for specifying underdefined functions on top of it.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    60
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    61
As a simple example we define division on @{typ nat}:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    62
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    63
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    64
consts divi :: "nat \<times> nat \<Rightarrow> nat"
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    65
recdef divi "measure(\<lambda>(m,n). m)"
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    66
  "divi(m,0) = arbitrary"
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    67
  "divi(m,n) = (if m < n then 0 else divi(m-n,n)+1)"
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    68
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    69
text{*\noindent Of course we could also have defined
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    70
@{term"divi(m,0)"} to be some specific number, for example 0. The
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    71
latter option is chosen for the predefined @{text div} function, which
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
    72
simplifies proofs at the expense of deviating from the
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
    73
standard mathematical division function.
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    74
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    75
As a more substantial example we consider the problem of searching a graph.
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
    76
For simplicity our graph is given by a function @{term f} of
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    77
type @{typ"'a \<Rightarrow> 'a"} which
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    78
maps each node to its successor; the graph has out-degree 1.
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
    79
The task is to find the end of a chain, modelled by a node pointing to
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
    80
itself. Here is a first attempt:
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    81
@{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    82
This may be viewed as a fixed point finder or as the second half of the well
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    83
known \emph{Union-Find} algorithm.
11149
e258b536a137 *** empty log message ***
nipkow
parents: 10885
diff changeset
    84
The snag is that it may not terminate if @{term f} has non-trivial cycles.
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    85
Phrased differently, the relation
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    86
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    87
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    88
constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    89
  "step1 f \<equiv> {(y,x). y = f x \<and> y \<noteq> x}"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    90
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    91
text{*\noindent
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    92
must be well-founded. Thus we make the following definition:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    93
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    94
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    95
consts find :: "('a \<Rightarrow> 'a) \<times> 'a \<Rightarrow> 'a"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    96
recdef find "same_fst (\<lambda>f. wf(step1 f)) step1"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    97
  "find(f,x) = (if wf(step1 f)
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    98
                then if f x = x then x else find(f, f x)
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    99
                else arbitrary)"
11285
3826c51d980e *** empty log message ***
nipkow
parents: 11277
diff changeset
   100
(hints recdef_simp: step1_def)
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   101
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   102
text{*\noindent
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   103
The recursion equation itself should be clear enough: it is our aborted
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   104
first attempt augmented with a check that there are no non-trivial loops.
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
   105
To express the required well-founded relation we employ the
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   106
predefined combinator @{term same_fst} of type
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   107
@{text[display]"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b\<times>'b)set) \<Rightarrow> (('a\<times>'b) \<times> ('a\<times>'b))set"}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   108
defined as
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   109
@{thm[display]same_fst_def[no_vars]}
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   110
This combinator is designed for
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   111
recursive functions on pairs where the first component of the argument is
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   112
passed unchanged to all recursive calls. Given a constraint on the first
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   113
component and a relation on the second component, @{term same_fst} builds the
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   114
required relation on pairs.  The theorem
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   115
@{thm[display]wf_same_fst[no_vars]}
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   116
is known to the well-foundedness prover of \isacommand{recdef}.  Thus
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   117
well-foundedness of the relation given to \isacommand{recdef} is immediate.
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   118
Furthermore, each recursive call descends along that relation: the first
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   119
argument stays unchanged and the second one descends along @{term"step1
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
   120
f"}. The proof requires unfolding the definition of @{const step1},
11285
3826c51d980e *** empty log message ***
nipkow
parents: 11277
diff changeset
   121
as specified in the \isacommand{hints} above.
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   122
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   123
Normally you will then derive the following conditional variant from
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   124
the recursion equation:
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   125
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   126
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   127
lemma [simp]:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   128
  "wf(step1 f) \<Longrightarrow> find(f,x) = (if f x = x then x else find(f, f x))"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   129
by simp
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   130
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   131
text{*\noindent Then you should disable the original recursion equation:*}
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   132
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   133
declare find.simps[simp del]
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   134
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   135
text{*
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   136
Reasoning about such underdefined functions is like that for other
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   137
recursive functions.  Here is a simple example of recursion induction:
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   138
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   139
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   140
lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
12815
wenzelm
parents: 12334
diff changeset
   141
apply(induct_tac f x rule: find.induct);
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   142
apply simp
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   143
done
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   144
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
   145
subsubsection{*The {\tt\slshape while} Combinator*}
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   146
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   147
text{*If the recursive function happens to be tail recursive, its
11428
332347b9b942 tidying the index
paulson
parents: 11310
diff changeset
   148
definition becomes a triviality if based on the predefined \cdx{while}
12332
aea72a834c85 *** empty log message ***
nipkow
parents: 11636
diff changeset
   149
combinator.  The latter lives in the Library theory \thydx{While_Combinator}.
aea72a834c85 *** empty log message ***
nipkow
parents: 11636
diff changeset
   150
% which is not part of {text Main} but needs to
aea72a834c85 *** empty log message ***
nipkow
parents: 11636
diff changeset
   151
% be included explicitly among the ancestor theories.
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   152
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   153
Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   154
and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   155
That is, @{term"while b c s"} is equivalent to the imperative program
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   156
\begin{verbatim}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   157
     x := s; while b(x) do x := c(x); return x
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   158
\end{verbatim}
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   159
In general, @{term s} will be a tuple or record.  As an example
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
   160
consider the following definition of function @{const find}:
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   161
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   162
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   163
constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   164
  "find2 f x \<equiv>
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   165
   fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   166
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   167
text{*\noindent
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   168
The loop operates on two ``local variables'' @{term x} and @{term x'}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   169
containing the ``current'' and the ``next'' value of function @{term f}.
11310
51e70b7bc315 spelling check
paulson
parents: 11285
diff changeset
   170
They are initialized with the global @{term x} and @{term"f x"}. At the
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   171
end @{term fst} selects the local @{term x}.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   172
11158
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   173
Although the definition of tail recursive functions via @{term while} avoids
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   174
termination proofs, there is no free lunch. When proving properties of
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   175
functions defined by @{term while}, termination rears its ugly head
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   176
again. Here is \tdx{while_rule}, the well known proof rule for total
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   177
correctness of loops expressed with @{term while}:
11158
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   178
@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be true of
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   179
the initial state @{term s} and invariant under @{term c} (premises 1
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   180
and~2). The post-condition @{term Q} must become true when leaving the loop
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   181
(premise~3). And each loop iteration must descend along a well-founded
5652018b809a *** empty log message ***
nipkow
parents: 11157
diff changeset
   182
relation @{term r} (premises 4 and~5).
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   183
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 12815
diff changeset
   184
Let us now prove that @{const find2} does indeed find a fixed point. Instead
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   185
of induction we apply the above while rule, suitably instantiated.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   186
Only the final premise of @{thm[source]while_rule} is left unproved
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   187
by @{text auto} but falls to @{text simp}:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   188
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   189
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
   190
lemma lem: "wf(step1 f) \<Longrightarrow>
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11256
diff changeset
   191
  \<exists>y. while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x) = (y,y) \<and>
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
   192
       f y = y"
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   193
apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   194
               r = "inv_image (step1 f) fst" in while_rule);
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   195
apply auto
12815
wenzelm
parents: 12334
diff changeset
   196
apply(simp add: inv_image_def step1_def)
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   197
done
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   198
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   199
text{*
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   200
The theorem itself is a simple consequence of this lemma:
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   201
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   202
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   203
theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   204
apply(drule_tac x = x in lem)
12815
wenzelm
parents: 12334
diff changeset
   205
apply(auto simp add: find2_def)
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   206
done
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   207
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   208
text{* Let us conclude this section on partial functions by a
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   209
discussion of the merits of the @{term while} combinator. We have
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   210
already seen that the advantage of not having to
11310
51e70b7bc315 spelling check
paulson
parents: 11285
diff changeset
   211
provide a termination argument when defining a function via @{term
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   212
while} merely puts off the evil hour. On top of that, tail recursive
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   213
functions tend to be more complicated to reason about. So why use
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   214
@{term while} at all? The only reason is executability: the recursion
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   215
equation for @{term while} is a directly executable functional
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   216
program. This is in stark contrast to guarded recursion as introduced
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   217
above which requires an explicit test @{prop"x \<in> dom f"} in the
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   218
function body.  Unless @{term dom} is trivial, this leads to a
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 11158
diff changeset
   219
definition that is impossible to execute or prohibitively slow.
10885
90695f46440b lcp's pass over the book, chapters 1-8
paulson
parents: 10654
diff changeset
   220
Thus, if you are aiming for an efficiently executable definition
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   221
of a partial function, you are likely to need @{term while}.
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   222
*}
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   223
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   224
(*<*)end(*>*)