equal
deleted
inserted
replaced
8 \isacommand{primrec}. In most cases this works fine, but there is a subtle |
8 \isacommand{primrec}. In most cases this works fine, but there is a subtle |
9 problem that must be mentioned: simplification may not |
9 problem that must be mentioned: simplification may not |
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{\isacharasterisk}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 |
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{\isacharasterisk}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 |
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{\isacharasterisk}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. |
83 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
83 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
84 \begin{isamarkuptext}% |
84 \begin{isamarkuptext}% |
85 \noindent |
85 \noindent |
86 after which we can disable the original simplification rule:% |
86 after which we can disable the original simplification rule:% |
87 \end{isamarkuptext}% |
87 \end{isamarkuptext}% |
88 \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline |
88 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
89 \end{isabellebody}% |
89 \end{isabellebody}% |
90 %%% Local Variables: |
90 %%% Local Variables: |
91 %%% mode: latex |
91 %%% mode: latex |
92 %%% TeX-master: "root" |
92 %%% TeX-master: "root" |
93 %%% End: |
93 %%% End: |