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 these lemmas:% |
79 \end{isamarkuptext}% |
80 \end{isamarkuptext}% |
80 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
81 \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 |
82 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
82 \isacommand{done}\isanewline |
83 \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 |
84 \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 |
85 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
85 \isacommand{done}% |
86 \isacommand{done}% |
86 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |
87 \noindent |
88 \noindent |
88 after which we can disable the original simplification rule:% |
89 Now we can disable the original simplification rule:% |
89 \end{isamarkuptext}% |
90 \end{isamarkuptext}% |
90 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
91 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
91 \end{isabellebody}% |
92 \end{isabellebody}% |
92 %%% Local Variables: |
93 %%% Local Variables: |
93 %%% mode: latex |
94 %%% mode: latex |