equal
deleted
inserted
replaced
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{if} branch, which is why programming |
26 the recursive call inside the \isa{else} branch, which is why programming |
27 languages and our simplifier don't do that. Unfortunately the simplifier does |
27 languages and our simplifier don't do that. Unfortunately the simplifier does |
28 something else which leads to the same problem: it splits \isa{if}s if the |
28 something else which leads to the same problem: it splits \isa{if}s if the |
29 condition simplifies to neither \isa{True} nor \isa{False}. For |
29 condition simplifies to neither \isa{True} nor \isa{False}. For |
30 example, simplification reduces |
30 example, simplification reduces |
31 \begin{isabelle}% |
31 \begin{isabelle}% |
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{by}{\isacharparenleft}simp{\isacharparenright}\isanewline |
81 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
82 \isacommand{done}\isanewline |
82 \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 |
83 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
84 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
85 \isacommand{done}% |
84 \begin{isamarkuptext}% |
86 \begin{isamarkuptext}% |
85 \noindent |
87 \noindent |
86 after which we can disable the original simplification rule:% |
88 after which we can disable the original simplification rule:% |
87 \end{isamarkuptext}% |
89 \end{isamarkuptext}% |
88 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
90 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |