equal
deleted
inserted
replaced
17 |
17 |
18 text{*\noindent |
18 text{*\noindent |
19 According to the measure function, the second argument should decrease with |
19 According to the measure function, the second argument should decrease with |
20 each recursive call. The resulting termination condition |
20 each recursive call. The resulting termination condition |
21 @{term[display]"n ~= 0 ==> m mod n < n"} |
21 @{term[display]"n ~= 0 ==> m mod n < n"} |
22 is provded automatically because it is already present as a lemma in the |
22 is proved automatically because it is already present as a lemma in |
23 arithmetic library. Thus the recursion equation becomes a simplification |
23 HOL\@. Thus the recursion equation becomes a simplification |
24 rule. Of course the equation is nonterminating if we are allowed to unfold |
24 rule. Of course the equation is nonterminating if we are allowed to unfold |
25 the recursive call inside the @{text else} branch, which is why programming |
25 the recursive call inside the @{text else} branch, which is why programming |
26 languages and our simplifier don't do that. Unfortunately the simplifier does |
26 languages and our simplifier don't do that. Unfortunately the simplifier does |
27 something else which leads to the same problem: it splits @{text if}s if the |
27 something else which leads to the same problem: it splits @{text if}s if the |
28 condition simplifies to neither @{term True} nor @{term False}. For |
28 condition simplifies to neither @{term True} nor @{term False}. For |