doc-src/TutorialI/Advanced/Partial.thy
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 12815 1f073030b97a
child 15904 a6fb4ddc05c7
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10654
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*<*)theory Partial = While_Combinator:(*>*)
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
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
    52
(see @{term minus} above). Instead we have to move the condition over
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
11285
3826c51d980e *** empty log message ***
nipkow
parents: 11277
diff changeset
   120
f"}. The proof requires unfolding the definition of @{term step1},
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
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   160
consider the following definition of function @{term 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
458068404143 *** empty log message ***
nipkow
parents:
diff changeset
   184
Let us now prove that @{term find2} does indeed find a fixed point. Instead
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(*>*)