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

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 |