equal
deleted
inserted
replaced
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 proved automatically because it is already present as a lemma in |
24 arithmetic library. Thus the recursion equation becomes a simplification |
24 HOL\@. 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 |
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 |