1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{WFrec}% |
3 \def\isabellecontext{WFrec}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \begin{isamarkuptext}% |
6 \begin{isamarkuptext}% |
6 \noindent |
7 \noindent |
7 So far, all recursive definitions were shown to terminate via measure |
8 So far, all recursive definitions were shown to terminate via measure |
8 functions. Sometimes this can be inconvenient or |
9 functions. Sometimes this can be inconvenient or |
9 impossible. Fortunately, \isacommand{recdef} supports much more |
10 impossible. Fortunately, \isacommand{recdef} supports much more |
10 general definitions. For example, termination of Ackermann's function |
11 general definitions. For example, termination of Ackermann's function |
11 can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
12 can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
12 \end{isamarkuptext}% |
13 \end{isamarkuptext}% |
|
14 \isamarkuptrue% |
13 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
15 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
|
16 \isamarkupfalse% |
14 \isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
17 \isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
15 \ \ {\isachardoublequote}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline |
18 \ \ {\isachardoublequote}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline |
16 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
19 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
17 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
20 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
21 % |
18 \begin{isamarkuptext}% |
22 \begin{isamarkuptext}% |
19 \noindent |
23 \noindent |
20 The lexicographic product decreases if either its first component |
24 The lexicographic product decreases if either its first component |
21 decreases (as in the second equation and in the outer call in the |
25 decreases (as in the second equation and in the outer call in the |
22 third equation) or its first component stays the same and the second |
26 third equation) or its first component stays the same and the second |
40 example, \isa{measure\ f} is always well-founded. The lexicographic |
44 example, \isa{measure\ f} is always well-founded. The lexicographic |
41 product of two well-founded relations is again well-founded, which we relied |
45 product of two well-founded relations is again well-founded, which we relied |
42 on when defining Ackermann's function above. |
46 on when defining Ackermann's function above. |
43 Of course the lexicographic product can also be iterated:% |
47 Of course the lexicographic product can also be iterated:% |
44 \end{isamarkuptext}% |
48 \end{isamarkuptext}% |
|
49 \isamarkuptrue% |
45 \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
50 \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
|
51 \isamarkupfalse% |
46 \isacommand{recdef}\ contrived\isanewline |
52 \isacommand{recdef}\ contrived\isanewline |
47 \ \ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequote}\isanewline |
53 \ \ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequote}\isanewline |
48 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline |
54 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline |
49 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline |
55 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline |
50 {\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline |
56 {\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline |
51 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}% |
57 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse% |
|
58 % |
52 \begin{isamarkuptext}% |
59 \begin{isamarkuptext}% |
53 Lexicographic products of measure functions already go a long |
60 Lexicographic products of measure functions already go a long |
54 way. Furthermore, you may embed a type in an |
61 way. Furthermore, you may embed a type in an |
55 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you |
62 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you |
56 will never have to prove well-foundedness of any relation composed |
63 will never have to prove well-foundedness of any relation composed |
62 It is also possible to use your own well-founded relations with |
69 It is also possible to use your own well-founded relations with |
63 \isacommand{recdef}. For example, the greater-than relation can be made |
70 \isacommand{recdef}. For example, the greater-than relation can be made |
64 well-founded by cutting it off at a certain point. Here is an example |
71 well-founded by cutting it off at a certain point. Here is an example |
65 of a recursive function that calls itself with increasing values up to ten:% |
72 of a recursive function that calls itself with increasing values up to ten:% |
66 \end{isamarkuptext}% |
73 \end{isamarkuptext}% |
|
74 \isamarkuptrue% |
67 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
75 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
|
76 \isamarkupfalse% |
68 \isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline |
77 \isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline |
69 {\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
78 {\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
79 % |
70 \begin{isamarkuptext}% |
80 \begin{isamarkuptext}% |
71 \noindent |
81 \noindent |
72 Since \isacommand{recdef} is not prepared for the relation supplied above, |
82 Since \isacommand{recdef} is not prepared for the relation supplied above, |
73 Isabelle rejects the definition. We should first have proved that |
83 Isabelle rejects the definition. We should first have proved that |
74 our relation was well-founded:% |
84 our relation was well-founded:% |
75 \end{isamarkuptext}% |
85 \end{isamarkuptext}% |
76 \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}% |
86 \isamarkuptrue% |
|
87 \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% |
|
88 % |
77 \begin{isamarkuptxt}% |
89 \begin{isamarkuptxt}% |
78 \noindent |
90 \noindent |
79 The proof is by showing that our relation is a subset of another well-founded |
91 The proof is by showing that our relation is a subset of another well-founded |
80 relation: one given by a measure function.\index{*wf_subset (theorem)}% |
92 relation: one given by a measure function.\index{*wf_subset (theorem)}% |
81 \end{isamarkuptxt}% |
93 \end{isamarkuptxt}% |
82 \isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}% |
94 \isamarkuptrue% |
|
95 \isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% |
|
96 % |
83 \begin{isamarkuptxt}% |
97 \begin{isamarkuptxt}% |
84 \begin{isabelle}% |
98 \begin{isabelle}% |
85 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
99 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
86 \end{isabelle} |
100 \end{isabelle} |
87 |
101 |
88 \noindent |
102 \noindent |
89 The inclusion remains to be proved. After unfolding some definitions, |
103 The inclusion remains to be proved. After unfolding some definitions, |
90 we are left with simple arithmetic:% |
104 we are left with simple arithmetic:% |
91 \end{isamarkuptxt}% |
105 \end{isamarkuptxt}% |
92 \isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
106 \isamarkuptrue% |
|
107 \isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
|
108 % |
93 \begin{isamarkuptxt}% |
109 \begin{isamarkuptxt}% |
94 \begin{isabelle}% |
110 \begin{isabelle}% |
95 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b% |
111 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b% |
96 \end{isabelle} |
112 \end{isabelle} |
97 |
113 |
98 \noindent |
114 \noindent |
99 And that is dispatched automatically:% |
115 And that is dispatched automatically:% |
100 \end{isamarkuptxt}% |
116 \end{isamarkuptxt}% |
101 \isacommand{by}\ arith% |
117 \isamarkuptrue% |
|
118 \isacommand{by}\ arith\isamarkupfalse% |
|
119 % |
102 \begin{isamarkuptext}% |
120 \begin{isamarkuptext}% |
103 \noindent |
121 \noindent |
104 |
122 |
105 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
123 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
106 crucial hint to our definition:% |
124 crucial hint to our definition:% |
107 \end{isamarkuptext}% |
125 \end{isamarkuptext}% |
108 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
126 \isamarkuptrue% |
|
127 \isamarkupfalse% |
|
128 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}\isamarkupfalse% |
|
129 % |
109 \begin{isamarkuptext}% |
130 \begin{isamarkuptext}% |
110 \noindent |
131 \noindent |
111 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
132 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
112 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
133 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
113 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
134 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
114 termination proof, where we have less control. A tailor-made termination |
135 termination proof, where we have less control. A tailor-made termination |
115 relation makes even more sense when it can be used in several function |
136 relation makes even more sense when it can be used in several function |
116 declarations.% |
137 declarations.% |
117 \end{isamarkuptext}% |
138 \end{isamarkuptext}% |
|
139 \isamarkuptrue% |
|
140 \isamarkupfalse% |
118 \end{isabellebody}% |
141 \end{isabellebody}% |
119 %%% Local Variables: |
142 %%% Local Variables: |
120 %%% mode: latex |
143 %%% mode: latex |
121 %%% TeX-master: "root" |
144 %%% TeX-master: "root" |
122 %%% End: |
145 %%% End: |