equal
deleted
inserted
replaced
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. |