doc-src/TutorialI/Advanced/WFrec.thy
author nipkow
Wed, 11 Oct 2000 13:15:04 +0200
changeset 10189 865918597b63
parent 10187 0376cccd9118
child 10190 871772d38b30
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10187
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*<*)theory WFrec = Main:(*>*)
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     2
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     3
text{*\noindent
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     4
So far, all recursive definitions where shown to terminate via measure
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     5
functions. Sometimes this can be quite inconvenient or even
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     6
impossible. Fortunately, \isacommand{recdef} supports much more
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     7
general definitions. For example, termination of Ackermann's function
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     8
can be shown by means of the lexicographic product @{text"<*lex*>"}:
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
     9
*}
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    10
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    11
consts ack :: "nat\<times>nat \<Rightarrow> nat";
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    12
recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    13
  "ack(0,n)         = Suc n"
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    14
  "ack(Suc m,0)     = ack(m, 1)"
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    15
  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    16
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    17
text{*\noindent
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    18
The lexicographic product decreases if either its first component
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    19
decreases (as in the second equation and in the outer call in the
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    20
third equation) or its first component stays the same and the second
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    21
component decreases (as in the inner call in the third equation).
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    22
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    23
In general, \isacommand{recdef} supports termination proofs based on
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    24
arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    25
recursion}\indexbold{recursion!wellfounded}\index{wellfounded
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    26
recursion|see{recursion, wellfounded}}.  A relation $<$ is
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    27
\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    28
a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
10189
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    29
of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    30
of an equation and $r$ the argument of some recursive call on the
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    31
corresponding right-hand side, induces a wellfounded relation.  For a
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    32
systematic account of termination proofs via wellfounded relations
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    33
see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    34
some of the theory of wellfounded relations. For example
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    35
@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    36
wellfounded.
10187
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    37
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    38
Each \isacommand{recdef} definition should be accompanied (after the
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    39
name of the function) by a wellfounded relation on the argument type
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    40
of the function. For example, @{term measure} is defined by
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    41
@{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    42
and it has been proved that @{term"measure f"} is always wellfounded.
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    43
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    44
In addition to @{term measure}, the library provides
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    45
a number of further constructions for obtaining wellfounded relations.
10189
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    46
Above we have already met @{text"<*lex*>"} of type
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    47
@{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    48
Of course the lexicographic product can also be interated, as in the following
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    49
function definition:
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    50
*}
10187
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    51
10189
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    52
consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    53
recdef contrived
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    54
  "measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    55
"contrived(i,j,Suc k) = contrived(i,j,k)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    56
"contrived(i,Suc j,0) = contrived(i,j,j)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    57
"contrived(Suc i,0,0) = contrived(i,i,i)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    58
"contrived(0,0,0)     = 0"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    59
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    60
text{*
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    61
Lexicographic products of measure functions already go a long way. A
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    62
further useful construction is the embedding of some type in an
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    63
existing wellfounded relation via the inverse image of a function:
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    64
@{thm[display,show_types]inv_image_def[no_vars]}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    65
\begin{sloppypar}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    66
\noindent
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    67
For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    68
@{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    69
(as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}).
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    70
\end{sloppypar}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    71
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    72
%Finally there is also {finite_psubset} the proper subset relation on finite sets
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    73
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    74
All the above constructions are known to \isacommand{recdef}. Thus you
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    75
will never have to prove wellfoundedness of any relation composed
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    76
solely of these building blocks. But of course the proof of
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    77
termination of your function definition, i.e.\ that the arguments
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    78
decrease with every recursive call, may still require you to provide
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    79
additional lemmas.
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    80
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    81
It is also possible to use your own wellfounded relations with \isacommand{recdef}.
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    82
Here is a simplistic example:
10187
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
    83
*}
10189
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    84
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    85
consts f :: "nat \<Rightarrow> nat"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    86
recdef f "id(less_than)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    87
"f 0 = 0"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    88
"f (Suc n) = f n"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    89
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    90
text{*
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    91
Since \isacommand{recdef} is not prepared for @{term id}, the identity
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    92
function, this leads to the complaint that it could not prove
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    93
@{prop"wf (id less_than)"}, the wellfoundedness of @{term"id
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    94
less_than"}. We should first have proved that @{term id} preserves wellfoundedness
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    95
*}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    96
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    97
lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    98
by simp;
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
    99
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   100
text{*\noindent
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   101
and should have added the following hint to our above definition:
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   102
*}
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   103
(*<*)
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   104
consts g :: "nat \<Rightarrow> nat"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   105
recdef g "id(less_than)"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   106
"g 0 = 0"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   107
"g (Suc n) = g n"
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   108
(*>*)
865918597b63 *** empty log message ***
nipkow
parents: 10187
diff changeset
   109
(hints recdef_wf add: wf_id)
10187
0376cccd9118 *** empty log message ***
nipkow
parents:
diff changeset
   110
(*<*)end(*>*)