changeset 10189 865918597b63 parent 10187 0376cccd9118 child 10190 871772d38b30
equal inserted replaced
10188:2899182af616 10189:865918597b63
    24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
    24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
    25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded
    25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded
    26 recursion|see{recursion, wellfounded}}.  A relation $<$ is
    26 recursion|see{recursion, wellfounded}}.  A relation $<$ is
    27 \bfindex{wellfounded} if it has no infinite descending chain $\cdots <  27 \bfindex{wellfounded} if it has no infinite descending chain$\cdots <
    28 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set  28 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
    29 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation
    29 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
    30 and $r$ the argument of some recursive call on the corresponding
    30 of an equation and $r$ the argument of some recursive call on the
    31 right-hand side, induces a wellfounded relation.  For a systematic
    31 corresponding right-hand side, induces a wellfounded relation.  For a
    32 account of termination proofs via wellfounded relations see, for
    32 systematic account of termination proofs via wellfounded relations
    33 example, \cite{Baader-Nipkow}.
    33 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes

    34 some of the theory of wellfounded relations. For example

    35 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is

    36 wellfounded.
    34
    37
    35 Each \isacommand{recdef} definition should be accompanied (after the
    38 Each \isacommand{recdef} definition should be accompanied (after the
    36 name of the function) by a wellfounded relation on the argument type
    39 name of the function) by a wellfounded relation on the argument type
    37 of the function. For example, @{term measure} is defined by
    40 of the function. For example, @{term measure} is defined by
    38 @{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
    41 @{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
    39 and it has been proved that @{term"measure f"} is always wellfounded.
    42 and it has been proved that @{term"measure f"} is always wellfounded.
    40
    43
    41 In addition to @{term measure}, the library provides
    44 In addition to @{term measure}, the library provides
    42 a number of further constructions for obtaining wellfounded relations.
    45 a number of further constructions for obtaining wellfounded relations.

    46 Above we have already met @{text"<*lex*>"} of type

    47 @{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"}

    48 Of course the lexicographic product can also be interated, as in the following

    49 function definition:

    50 *}
    43
    51
    44 wf proof auto if stndard constructions.
    52 consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"

    53 recdef contrived

    54   "measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)"

    55 "contrived(i,j,Suc k) = contrived(i,j,k)"

    56 "contrived(i,Suc j,0) = contrived(i,j,j)"

    57 "contrived(Suc i,0,0) = contrived(i,i,i)"

    58 "contrived(0,0,0)     = 0"

    59

    60 text{*

    61 Lexicographic products of measure functions already go a long way. A

    62 further useful construction is the embedding of some type in an

    63 existing wellfounded relation via the inverse image of a function:

    64 @{thm[display,show_types]inv_image_def[no_vars]}

    65 \begin{sloppypar}

    66 \noindent

    67 For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where

    68 @{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat}

    69 (as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}).

    70 \end{sloppypar}

    71

    72 %Finally there is also {finite_psubset} the proper subset relation on finite sets

    73

    74 All the above constructions are known to \isacommand{recdef}. Thus you

    75 will never have to prove wellfoundedness of any relation composed

    76 solely of these building blocks. But of course the proof of

    77 termination of your function definition, i.e.\ that the arguments

    78 decrease with every recursive call, may still require you to provide

    79 additional lemmas.

    80

    81 It is also possible to use your own wellfounded relations with \isacommand{recdef}.

    82 Here is a simplistic example:
    45 *}
    83 *}

    84

    85 consts f :: "nat \<Rightarrow> nat"

    86 recdef f "id(less_than)"

    87 "f 0 = 0"

    88 "f (Suc n) = f n"

    89

    90 text{*

    91 Since \isacommand{recdef} is not prepared for @{term id}, the identity

    92 function, this leads to the complaint that it could not prove

    93 @{prop"wf (id less_than)"}, the wellfoundedness of @{term"id

    94 less_than"}. We should first have proved that @{term id} preserves wellfoundedness

    95 *}

    96

    97 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"

    98 by simp;

    99

   100 text{*\noindent

   101 and should have added the following hint to our above definition:

   102 *}

   103 (*<*)

   104 consts g :: "nat \<Rightarrow> nat"

   105 recdef g "id(less_than)"

   106 "g 0 = 0"

   107 "g (Suc n) = g n"

   108 (*>*)

   109 (hints recdef_wf add: wf_id)
    46 (*<*)end(*>*)
   110 (*<*)end(*>*)