10 terminate because of automatic splitting of \isa{if}. |
10 terminate because of automatic splitting of \isa{if}. |
11 Let us look at an example:% |
11 Let us look at an example:% |
12 \end{isamarkuptext}% |
12 \end{isamarkuptext}% |
13 \isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
13 \isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
14 \isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
14 \isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
15 \ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}\isadigit{0}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
15 \ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
16 \begin{isamarkuptext}% |
16 \begin{isamarkuptext}% |
17 \noindent |
17 \noindent |
18 According to the measure function, the second argument should decrease with |
18 According to the measure function, the second argument should decrease with |
19 each recursive call. The resulting termination condition |
19 each recursive call. The resulting termination condition |
20 \begin{isabelle}% |
20 \begin{isabelle}% |
21 \ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n% |
21 \ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n% |
22 \end{isabelle} |
22 \end{isabelle} |
23 is provded automatically because it is already present as a lemma in the |
23 is provded automatically because it is already present as a lemma in the |
24 arithmetic library. Thus the recursion equation becomes a simplification |
24 arithmetic library. Thus the recursion equation becomes a simplification |
25 rule. Of course the equation is nonterminating if we are allowed to unfold |
25 rule. Of course the equation is nonterminating if we are allowed to unfold |
26 the recursive call inside the \isa{else} branch, which is why programming |
26 the recursive call inside the \isa{else} branch, which is why programming |
31 \begin{isabelle}% |
31 \begin{isabelle}% |
32 \ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k% |
32 \ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k% |
33 \end{isabelle} |
33 \end{isabelle} |
34 in one step to |
34 in one step to |
35 \begin{isabelle}% |
35 \begin{isabelle}% |
36 \ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k% |
36 \ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k% |
37 \end{isabelle} |
37 \end{isabelle} |
38 where the condition cannot be reduced further, and splitting leads to |
38 where the condition cannot be reduced further, and splitting leads to |
39 \begin{isabelle}% |
39 \begin{isabelle}% |
40 \ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}% |
40 \ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}% |
41 \end{isabelle} |
41 \end{isabelle} |
42 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by |
42 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by |
43 an \isa{if}, it is unfolded again, which leads to an infinite chain of |
43 an \isa{if}, it is unfolded again, which leads to an infinite chain of |
44 simplification steps. Fortunately, this problem can be avoided in many |
44 simplification steps. Fortunately, this problem can be avoided in many |
45 different ways. |
45 different ways. |
52 |
52 |
53 If possible, the definition should be given by pattern matching on the left |
53 If possible, the definition should be given by pattern matching on the left |
54 rather than \isa{if} on the right. In the case of \isa{gcd} the |
54 rather than \isa{if} on the right. In the case of \isa{gcd} the |
55 following alternative definition suggests itself:% |
55 following alternative definition suggests itself:% |
56 \end{isamarkuptext}% |
56 \end{isamarkuptext}% |
57 \isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
57 \isacommand{consts}\ gcd{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
58 \isacommand{recdef}\ gcd\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
58 \isacommand{recdef}\ gcd{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
59 \ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
59 \ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
60 \ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd\isadigit{1}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}% |
60 \ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isadigit{1}}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}% |
61 \begin{isamarkuptext}% |
61 \begin{isamarkuptext}% |
62 \noindent |
62 \noindent |
63 Note that the order of equations is important and hides the side condition |
63 Note that the order of equations is important and hides the side condition |
64 \isa{n\ {\isasymnoteq}\ \isadigit{0}}. Unfortunately, in general the case distinction |
64 \isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction |
65 may not be expressible by pattern matching. |
65 may not be expressible by pattern matching. |
66 |
66 |
67 A very simple alternative is to replace \isa{if} by \isa{case}, which |
67 A very simple alternative is to replace \isa{if} by \isa{case}, which |
68 is also available for \isa{bool} but is not split automatically:% |
68 is also available for \isa{bool} but is not split automatically:% |
69 \end{isamarkuptext}% |
69 \end{isamarkuptext}% |
70 \isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
70 \isacommand{consts}\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
71 \isacommand{recdef}\ gcd\isadigit{2}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
71 \isacommand{recdef}\ gcd{\isadigit{2}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline |
72 \ \ {\isachardoublequote}gcd\isadigit{2}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}\isadigit{0}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd\isadigit{2}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
72 \ \ {\isachardoublequote}gcd{\isadigit{2}}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
73 \begin{isamarkuptext}% |
73 \begin{isamarkuptext}% |
74 \noindent |
74 \noindent |
75 In fact, this is probably the neatest solution next to pattern matching. |
75 In fact, this is probably the neatest solution next to pattern matching. |
76 |
76 |
77 A final alternative is to replace the offending simplification rules by |
77 A final alternative is to replace the offending simplification rules by |
78 derived conditional ones. For \isa{gcd} it means we have to prove% |
78 derived conditional ones. For \isa{gcd} it means we have to prove% |
79 \end{isamarkuptext}% |
79 \end{isamarkuptext}% |
80 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
80 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
81 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
81 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
82 \isacommand{done}\isanewline |
82 \isacommand{done}\isanewline |
83 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline |
83 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline |
84 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
84 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
85 \isacommand{done}% |
85 \isacommand{done}% |
86 \begin{isamarkuptext}% |
86 \begin{isamarkuptext}% |
87 \noindent |
87 \noindent |
88 after which we can disable the original simplification rule:% |
88 after which we can disable the original simplification rule:% |