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