15 |
15 |
16 In general, Isabelle may not be able to prove all termination condition |
16 In general, Isabelle may not be able to prove all termination condition |
17 (there is one for each recursive call) automatically. For example, |
17 (there is one for each recursive call) automatically. For example, |
18 termination of the following artificial function% |
18 termination of the following artificial function% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
20 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
21 \isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
21 \isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
22 \ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
22 \ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
23 \begin{isamarkuptext}% |
23 \begin{isamarkuptext}% |
24 \noindent |
24 \noindent |
25 is not proved automatically (although maybe it should be). Isabelle prints a |
25 is not proved automatically (although maybe it should be). Isabelle prints a |
26 kind of error message showing you what it was unable to prove. You will then |
26 kind of error message showing you what it was unable to prove. You will then |
27 have to prove it as a separate lemma before you attempt the definition |
27 have to prove it as a separate lemma before you attempt the definition |
28 of your function once more. In our case the required lemma is the obvious one:% |
28 of your function once more. In our case the required lemma is the obvious one:% |
29 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
30 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}% |
30 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}% |
31 \begin{isamarkuptxt}% |
31 \begin{isamarkuptxt}% |
32 \noindent |
32 \noindent |
33 It was not proved automatically because of the special nature of \isa{{\isacharminus}} |
33 It was not proved automatically because of the special nature of \isa{{\isacharminus}} |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
35 \end{isamarkuptxt}% |
35 \end{isamarkuptxt}% |
36 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}% |
36 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}% |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 \noindent |
38 \noindent |
39 Because \isacommand{recdef}'s termination prover involves simplification, |
39 Because \isacommand{recdef}'s termination prover involves simplification, |
40 we have turned our lemma into a simplification rule. Therefore our second |
40 we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as |
41 attempt to define our function will automatically take it into account:% |
41 a simplification rule:% |
42 \end{isamarkuptext}% |
42 \end{isamarkuptext}% |
43 \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
43 \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
44 \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
44 \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
45 \ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
45 \ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
|
46 {\isacharparenleft}\isakeyword{hints}\ simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}% |
46 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
47 \noindent |
48 \noindent |
48 This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely |
49 This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely |
49 the stated recursion equation for \isa{g} and they are simplification |
50 the stated recursion equation for \isa{g} and they are simplification |
50 rules. Thus we can automatically prove% |
51 rules. Thus we can automatically prove% |
51 \end{isamarkuptext}% |
52 \end{isamarkuptext}% |
52 \isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
53 \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
53 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
54 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
54 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
55 \noindent |
56 \noindent |
56 More exciting theorems require induction, which is discussed below. |
57 More exciting theorems require induction, which is discussed below. |
57 |
58 |
58 Because lemma \isa{termi{\isacharunderscore}lem} above was only turned into a |
59 If the termination proof requires a new lemma that is of general use, you can |
59 simplification rule for the sake of the termination proof, we may want to |
60 turn it permanently into a simplification rule, in which case the above |
60 disable it again:% |
61 \isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not |
61 \end{isamarkuptext}% |
62 sufficiently general to warrant this distinction. |
62 \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem% |
63 |
63 \begin{isamarkuptext}% |
|
64 The attentive reader may wonder why we chose to call our function \isa{g} |
64 The attentive reader may wonder why we chose to call our function \isa{g} |
65 rather than \isa{f} the second time around. The reason is that, despite |
65 rather than \isa{f} the second time around. The reason is that, despite |
66 the failed termination proof, the definition of \isa{f} did not |
66 the failed termination proof, the definition of \isa{f} did not |
67 fail, and thus we could not define it a second time. However, all theorems |
67 fail, and thus we could not define it a second time. However, all theorems |
68 about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition |
68 about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition |
77 |
77 |
78 Although all the above examples employ measure functions, \isacommand{recdef} |
78 Although all the above examples employ measure functions, \isacommand{recdef} |
79 allows arbitrary wellfounded relations. For example, termination of |
79 allows arbitrary wellfounded relations. For example, termination of |
80 Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
80 Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
81 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |
82 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
82 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
83 \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 |
83 \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 |
84 \ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline |
84 \ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline |
85 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
85 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
86 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
86 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
87 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |