1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{fun{\isadigit{0}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \subsection{Definition} |
|
20 \label{sec:fun-examples} |
|
21 |
|
22 Here is a simple example, the \rmindex{Fibonacci function}:% |
|
23 \end{isamarkuptext}% |
|
24 \isamarkuptrue% |
|
25 \isacommand{fun}\isamarkupfalse% |
|
26 \ fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
27 {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
28 {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
29 {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib\ x\ {\isaliteral{2B}{\isacharplus}}\ fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
30 \begin{isamarkuptext}% |
|
31 \noindent |
|
32 This resembles ordinary functional programming languages. Note the obligatory |
|
33 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and |
|
34 defines the function in one go. Isabelle establishes termination automatically |
|
35 because \isa{fib}'s argument decreases in every recursive call. |
|
36 |
|
37 Slightly more interesting is the insertion of a fixed element |
|
38 between any two elements of a list:% |
|
39 \end{isamarkuptext}% |
|
40 \isamarkuptrue% |
|
41 \isacommand{fun}\isamarkupfalse% |
|
42 \ sep\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
43 {\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
44 {\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
45 {\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
46 \begin{isamarkuptext}% |
|
47 \noindent |
|
48 This time the length of the list decreases with the |
|
49 recursive call; the first argument is irrelevant for termination. |
|
50 |
|
51 Pattern matching\index{pattern matching!and \isacommand{fun}} |
|
52 need not be exhaustive and may employ wildcards:% |
|
53 \end{isamarkuptext}% |
|
54 \isamarkuptrue% |
|
55 \isacommand{fun}\isamarkupfalse% |
|
56 \ last\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
57 {\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
58 {\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
59 \begin{isamarkuptext}% |
|
60 Overlapping patterns are disambiguated by taking the order of equations into |
|
61 account, just as in functional programming:% |
|
62 \end{isamarkuptext}% |
|
63 \isamarkuptrue% |
|
64 \isacommand{fun}\isamarkupfalse% |
|
65 \ sep{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
66 {\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
67 {\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ xs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}% |
|
68 \begin{isamarkuptext}% |
|
69 \noindent |
|
70 To guarantee that the second equation can only be applied if the first |
|
71 one does not match, Isabelle internally replaces the second equation |
|
72 by the two possibilities that are left: \isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and |
|
73 \isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}. Thus the functions \isa{sep} and |
|
74 \isa{sep{\isadigit{1}}} are identical. |
|
75 |
|
76 Because of its pattern matching syntax, \isacommand{fun} is also useful |
|
77 for the definition of non-recursive functions:% |
|
78 \end{isamarkuptext}% |
|
79 \isamarkuptrue% |
|
80 \isacommand{fun}\isamarkupfalse% |
|
81 \ swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
82 {\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{23}{\isacharhash}}x{\isaliteral{23}{\isacharhash}}zs{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
83 {\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{22}{\isachardoublequoteclose}}% |
|
84 \begin{isamarkuptext}% |
|
85 After a function~$f$ has been defined via \isacommand{fun}, |
|
86 its defining equations (or variants derived from them) are available |
|
87 under the name $f$\isa{{\isaliteral{2E}{\isachardot}}simps} as theorems. |
|
88 For example, look (via \isacommand{thm}) at |
|
89 \isa{sep{\isaliteral{2E}{\isachardot}}simps} and \isa{sep{\isadigit{1}}{\isaliteral{2E}{\isachardot}}simps} to see that they define |
|
90 the same function. What is more, those equations are automatically declared as |
|
91 simplification rules. |
|
92 |
|
93 \subsection{Termination} |
|
94 |
|
95 Isabelle's automatic termination prover for \isacommand{fun} has a |
|
96 fixed notion of the \emph{size} (of type \isa{nat}) of an |
|
97 argument. The size of a natural number is the number itself. The size |
|
98 of a list is its length. For the general case see \S\ref{sec:general-datatype}. |
|
99 A recursive function is accepted if \isacommand{fun} can |
|
100 show that the size of one fixed argument becomes smaller with each |
|
101 recursive call. |
|
102 |
|
103 More generally, \isacommand{fun} allows any \emph{lexicographic |
|
104 combination} of size measures in case there are multiple |
|
105 arguments. For example, the following version of \rmindex{Ackermann's |
|
106 function} is accepted:% |
|
107 \end{isamarkuptext}% |
|
108 \isamarkuptrue% |
|
109 \isacommand{fun}\isamarkupfalse% |
|
110 \ ack{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
111 {\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
112 {\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
113 {\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}ack{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}% |
|
114 \begin{isamarkuptext}% |
|
115 The order of arguments has no influence on whether |
|
116 \isacommand{fun} can prove termination of a function. For more details |
|
117 see elsewhere~\cite{bulwahnKN07}. |
|
118 |
|
119 \subsection{Simplification} |
|
120 \label{sec:fun-simplification} |
|
121 |
|
122 Upon a successful termination proof, the recursion equations become |
|
123 simplification rules, just as with \isacommand{primrec}. |
|
124 In most cases this works fine, but there is a subtle |
|
125 problem that must be mentioned: simplification may not |
|
126 terminate because of automatic splitting of \isa{if}. |
|
127 \index{*if expressions!splitting of} |
|
128 Let us look at an example:% |
|
129 \end{isamarkuptext}% |
|
130 \isamarkuptrue% |
|
131 \isacommand{fun}\isamarkupfalse% |
|
132 \ gcd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
133 {\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
134 \begin{isamarkuptext}% |
|
135 \noindent |
|
136 The second argument decreases with each recursive call. |
|
137 The termination condition |
|
138 \begin{isabelle}% |
|
139 \ \ \ \ \ n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ mod\ n\ {\isaliteral{3C}{\isacharless}}\ n% |
|
140 \end{isabelle} |
|
141 is proved automatically because it is already present as a lemma in |
|
142 HOL\@. Thus the recursion equation becomes a simplification |
|
143 rule. Of course the equation is nonterminating if we are allowed to unfold |
|
144 the recursive call inside the \isa{else} branch, which is why programming |
|
145 languages and our simplifier don't do that. Unfortunately the simplifier does |
|
146 something else that leads to the same problem: it splits |
|
147 each \isa{if}-expression unless its |
|
148 condition simplifies to \isa{True} or \isa{False}. For |
|
149 example, simplification reduces |
|
150 \begin{isabelle}% |
|
151 \ \ \ \ \ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ k% |
|
152 \end{isabelle} |
|
153 in one step to |
|
154 \begin{isabelle}% |
|
155 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k% |
|
156 \end{isabelle} |
|
157 where the condition cannot be reduced further, and splitting leads to |
|
158 \begin{isabelle}% |
|
159 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}% |
|
160 \end{isabelle} |
|
161 Since the recursive call \isa{gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}} is no longer protected by |
|
162 an \isa{if}, it is unfolded again, which leads to an infinite chain of |
|
163 simplification steps. Fortunately, this problem can be avoided in many |
|
164 different ways. |
|
165 |
|
166 The most radical solution is to disable the offending theorem |
|
167 \isa{split{\isaliteral{5F}{\isacharunderscore}}if}, |
|
168 as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this |
|
169 approach: you will often have to invoke the rule explicitly when |
|
170 \isa{if} is involved. |
|
171 |
|
172 If possible, the definition should be given by pattern matching on the left |
|
173 rather than \isa{if} on the right. In the case of \isa{gcd} the |
|
174 following alternative definition suggests itself:% |
|
175 \end{isamarkuptext}% |
|
176 \isamarkuptrue% |
|
177 \isacommand{fun}\isamarkupfalse% |
|
178 \ gcd{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
179 {\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
180 {\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd{\isadigit{1}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
181 \begin{isamarkuptext}% |
|
182 \noindent |
|
183 The order of equations is important: it hides the side condition |
|
184 \isa{n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}}. Unfortunately, not all conditionals can be |
|
185 expressed by pattern matching. |
|
186 |
|
187 A simple alternative is to replace \isa{if} by \isa{case}, |
|
188 which is also available for \isa{bool} and is not split automatically:% |
|
189 \end{isamarkuptext}% |
|
190 \isamarkuptrue% |
|
191 \isacommand{fun}\isamarkupfalse% |
|
192 \ gcd{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
193 {\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{2}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ m\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ gcd{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
194 \begin{isamarkuptext}% |
|
195 \noindent |
|
196 This is probably the neatest solution next to pattern matching, and it is |
|
197 always available. |
|
198 |
|
199 A final alternative is to replace the offending simplification rules by |
|
200 derived conditional ones. For \isa{gcd} it means we have to prove |
|
201 these lemmas:% |
|
202 \end{isamarkuptext}% |
|
203 \isamarkuptrue% |
|
204 \isacommand{lemma}\isamarkupfalse% |
|
205 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
206 % |
|
207 \isadelimproof |
|
208 % |
|
209 \endisadelimproof |
|
210 % |
|
211 \isatagproof |
|
212 \isacommand{apply}\isamarkupfalse% |
|
213 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline |
|
214 \isacommand{done}\isamarkupfalse% |
|
215 % |
|
216 \endisatagproof |
|
217 {\isafoldproof}% |
|
218 % |
|
219 \isadelimproof |
|
220 \isanewline |
|
221 % |
|
222 \endisadelimproof |
|
223 \isanewline |
|
224 \isacommand{lemma}\isamarkupfalse% |
|
225 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
226 % |
|
227 \isadelimproof |
|
228 % |
|
229 \endisadelimproof |
|
230 % |
|
231 \isatagproof |
|
232 \isacommand{apply}\isamarkupfalse% |
|
233 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline |
|
234 \isacommand{done}\isamarkupfalse% |
|
235 % |
|
236 \endisatagproof |
|
237 {\isafoldproof}% |
|
238 % |
|
239 \isadelimproof |
|
240 % |
|
241 \endisadelimproof |
|
242 % |
|
243 \begin{isamarkuptext}% |
|
244 \noindent |
|
245 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. |
|
246 Now we can disable the original simplification rule:% |
|
247 \end{isamarkuptext}% |
|
248 \isamarkuptrue% |
|
249 \isacommand{declare}\isamarkupfalse% |
|
250 \ gcd{\isaliteral{2E}{\isachardot}}simps\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}% |
|
251 \begin{isamarkuptext}% |
|
252 \index{induction!recursion|(} |
|
253 \index{recursion induction|(} |
|
254 |
|
255 \subsection{Induction} |
|
256 \label{sec:fun-induction} |
|
257 |
|
258 Having defined a function we might like to prove something about it. |
|
259 Since the function is recursive, the natural proof principle is |
|
260 again induction. But this time the structural form of induction that comes |
|
261 with datatypes is unlikely to work well --- otherwise we could have defined the |
|
262 function by \isacommand{primrec}. Therefore \isacommand{fun} automatically |
|
263 proves a suitable induction rule $f$\isa{{\isaliteral{2E}{\isachardot}}induct} that follows the |
|
264 recursion pattern of the particular function $f$. We call this |
|
265 \textbf{recursion induction}. Roughly speaking, it |
|
266 requires you to prove for each \isacommand{fun} equation that the property |
|
267 you are trying to establish holds for the left-hand side provided it holds |
|
268 for all recursive calls on the right-hand side. Here is a simple example |
|
269 involving the predefined \isa{map} functional on lists:% |
|
270 \end{isamarkuptext}% |
|
271 \isamarkuptrue% |
|
272 \isacommand{lemma}\isamarkupfalse% |
|
273 \ {\isaliteral{22}{\isachardoublequoteopen}}map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
274 \isadelimproof |
|
275 % |
|
276 \endisadelimproof |
|
277 % |
|
278 \isatagproof |
|
279 % |
|
280 \begin{isamarkuptxt}% |
|
281 \noindent |
|
282 Note that \isa{map\ f\ xs} |
|
283 is the result of applying \isa{f} to all elements of \isa{xs}. We prove |
|
284 this lemma by recursion induction over \isa{sep}:% |
|
285 \end{isamarkuptxt}% |
|
286 \isamarkuptrue% |
|
287 \isacommand{apply}\isamarkupfalse% |
|
288 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ x\ xs\ rule{\isaliteral{3A}{\isacharcolon}}\ sep{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}% |
|
289 \begin{isamarkuptxt}% |
|
290 \noindent |
|
291 The resulting proof state has three subgoals corresponding to the three |
|
292 clauses for \isa{sep}: |
|
293 \begin{isabelle}% |
|
294 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
295 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
296 \ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x\ y\ zs{\isaliteral{2E}{\isachardot}}\isanewline |
|
297 \isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
|
298 \isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
|
299 \end{isabelle} |
|
300 The rest is pure simplification:% |
|
301 \end{isamarkuptxt}% |
|
302 \isamarkuptrue% |
|
303 \isacommand{apply}\isamarkupfalse% |
|
304 \ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
|
305 \isacommand{done}\isamarkupfalse% |
|
306 % |
|
307 \endisatagproof |
|
308 {\isafoldproof}% |
|
309 % |
|
310 \isadelimproof |
|
311 % |
|
312 \endisadelimproof |
|
313 % |
|
314 \begin{isamarkuptext}% |
|
315 \noindent The proof goes smoothly because the induction rule |
|
316 follows the recursion of \isa{sep}. Try proving the above lemma by |
|
317 structural induction, and you find that you need an additional case |
|
318 distinction. |
|
319 |
|
320 In general, the format of invoking recursion induction is |
|
321 \begin{quote} |
|
322 \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $x@1 \dots x@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $f$\isa{{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}} |
|
323 \end{quote}\index{*induct_tac (method)}% |
|
324 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
|
325 name of a function that takes $n$ arguments. Usually the subgoal will |
|
326 contain the term $f x@1 \dots x@n$ but this need not be the case. The |
|
327 induction rules do not mention $f$ at all. Here is \isa{sep{\isaliteral{2E}{\isachardot}}induct}: |
|
328 \begin{isabelle} |
|
329 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
|
330 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline |
|
331 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
|
332 {\isasymLongrightarrow}~P~u~v% |
|
333 \end{isabelle} |
|
334 It merely says that in order to prove a property \isa{P} of \isa{u} and |
|
335 \isa{v} you need to prove it for the three cases where \isa{v} is the |
|
336 empty list, the singleton list, and the list with at least two elements. |
|
337 The final case has an induction hypothesis: you may assume that \isa{P} |
|
338 holds for the tail of that list. |
|
339 \index{induction!recursion|)} |
|
340 \index{recursion induction|)}% |
|
341 \end{isamarkuptext}% |
|
342 \isamarkuptrue% |
|
343 % |
|
344 \isadelimtheory |
|
345 % |
|
346 \endisadelimtheory |
|
347 % |
|
348 \isatagtheory |
|
349 % |
|
350 \endisatagtheory |
|
351 {\isafoldtheory}% |
|
352 % |
|
353 \isadelimtheory |
|
354 % |
|
355 \endisadelimtheory |
|
356 \end{isabellebody}% |
|
357 %%% Local Variables: |
|
358 %%% mode: latex |
|
359 %%% TeX-master: "root" |
|
360 %%% End: |
|