summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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. |