doc-src/TutorialI/Advanced/WFrec.thy
changeset 10190 871772d38b30
parent 10189 865918597b63
child 10241 e0428c2778f1
equal deleted inserted replaced
10189:865918597b63 10190:871772d38b30
    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 wellfounded.
    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 wellfounded relation on the argument type
    40 of the function. For example, @{term 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 wellfounded.
    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 wellfounded relations.