doc-src/TutorialI/Advanced/WFrec.thy
changeset 10241 e0428c2778f1
parent 10190 871772d38b30
child 10396 5ab08609e6c8
equal deleted inserted replaced
10240:9ac0fe356ea7 10241:e0428c2778f1
    19 decreases (as in the second equation and in the outer call in the
    19 decreases (as in the second equation and in the outer call in the
    20 third equation) or its first component stays the same and the second
    20 third equation) or its first component stays the same and the second
    21 component decreases (as in the inner call in the third equation).
    21 component decreases (as in the inner call in the third equation).
    22 
    22 
    23 In general, \isacommand{recdef} supports termination proofs based on
    23 In general, \isacommand{recdef} supports termination proofs based on
    24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
    24 arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
    25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded
    25 recursion}\indexbold{recursion!well-founded}\index{well-founded
    26 recursion|see{recursion, wellfounded}}.  A relation $<$ is
    26 recursion|see{recursion, well-founded}}.  A relation $<$ is
    27 \bfindex{wellfounded} if it has no infinite descending chain $\cdots <
    27 \bfindex{well-founded} 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
    29 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
    30 of an equation and $r$ the argument of some recursive call on the
    30 of an equation and $r$ the argument of some recursive call on the
    31 corresponding right-hand side, induces a wellfounded relation.  For a
    31 corresponding right-hand side, induces a well-founded relation.  For a
    32 systematic account of termination proofs via wellfounded relations
    32 systematic account of termination proofs via well-founded relations
    33 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
    33 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
    34 some of the theory of wellfounded relations. For example
    34 some of the theory of well-founded relations. For example
    35 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
    35 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
    36 wellfounded.
    36 well-founded.
    37 
    37 
    38 Each \isacommand{recdef} definition should be accompanied (after the
    38 Each \isacommand{recdef} definition should be accompanied (after the
    39 name of the function) by a wellfounded relation on the argument type
    39 name of the function) by a well-founded relation on the argument type
    40 of the function. For example, \isaindexbold{measure} is defined by
    40 of the function. For example, \isaindexbold{measure} is defined by
    41 @{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}"}
    42 and it has been proved that @{term"measure f"} is always wellfounded.
    42 and it has been proved that @{term"measure f"} is always well-founded.
    43 
    43 
    44 In addition to @{term measure}, the library provides
    44 In addition to @{term measure}, the library provides
    45 a number of further constructions for obtaining wellfounded relations.
    45 a number of further constructions for obtaining well-founded relations.
    46 Above we have already met @{text"<*lex*>"} of type
    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"}
    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
    48 Of course the lexicographic product can also be interated, as in the following
    49 function definition:
    49 function definition:
    50 *}
    50 *}
    58 "contrived(0,0,0)     = 0"
    58 "contrived(0,0,0)     = 0"
    59 
    59 
    60 text{*
    60 text{*
    61 Lexicographic products of measure functions already go a long way. A
    61 Lexicographic products of measure functions already go a long way. A
    62 further useful construction is the embedding of some type in an
    62 further useful construction is the embedding of some type in an
    63 existing wellfounded relation via the inverse image of a function:
    63 existing well-founded relation via the inverse image of a function:
    64 @{thm[display,show_types]inv_image_def[no_vars]}
    64 @{thm[display,show_types]inv_image_def[no_vars]}
    65 \begin{sloppypar}
    65 \begin{sloppypar}
    66 \noindent
    66 \noindent
    67 For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where
    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}
    68 @{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat}
    70 \end{sloppypar}
    70 \end{sloppypar}
    71 
    71 
    72 %Finally there is also {finite_psubset} the proper subset relation on finite sets
    72 %Finally there is also {finite_psubset} the proper subset relation on finite sets
    73 
    73 
    74 All the above constructions are known to \isacommand{recdef}. Thus you
    74 All the above constructions are known to \isacommand{recdef}. Thus you
    75 will never have to prove wellfoundedness of any relation composed
    75 will never have to prove well-foundedness of any relation composed
    76 solely of these building blocks. But of course the proof of
    76 solely of these building blocks. But of course the proof of
    77 termination of your function definition, i.e.\ that the arguments
    77 termination of your function definition, i.e.\ that the arguments
    78 decrease with every recursive call, may still require you to provide
    78 decrease with every recursive call, may still require you to provide
    79 additional lemmas.
    79 additional lemmas.
    80 
    80 
    81 It is also possible to use your own wellfounded relations with \isacommand{recdef}.
    81 It is also possible to use your own well-founded relations with \isacommand{recdef}.
    82 Here is a simplistic example:
    82 Here is a simplistic example:
    83 *}
    83 *}
    84 
    84 
    85 consts f :: "nat \<Rightarrow> nat"
    85 consts f :: "nat \<Rightarrow> nat"
    86 recdef f "id(less_than)"
    86 recdef f "id(less_than)"
    88 "f (Suc n) = f n"
    88 "f (Suc n) = f n"
    89 
    89 
    90 text{*
    90 text{*
    91 Since \isacommand{recdef} is not prepared for @{term id}, the identity
    91 Since \isacommand{recdef} is not prepared for @{term id}, the identity
    92 function, this leads to the complaint that it could not prove
    92 function, this leads to the complaint that it could not prove
    93 @{prop"wf (id less_than)"}, the wellfoundedness of @{term"id
    93 @{prop"wf (id less_than)"}, the well-foundedness of @{term"id
    94 less_than"}. We should first have proved that @{term id} preserves wellfoundedness
    94 less_than"}. We should first have proved that @{term id} preserves well-foundedness
    95 *}
    95 *}
    96 
    96 
    97 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
    97 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
    98 by simp;
    98 by simp;
    99 
    99