(*<*) theory simplification imports Main begin (*>*)
text‹ Once we have proved all the termination conditions, the \isacommand{recdef} recursion equations become simplification rules, just as with \isacommand{primrec}. In most cases this works fine, but there is a subtle problem that must be mentioned: simplification may not terminate because of automatic splitting of ‹if›. \index{*if expressions!splitting of} Let us look at an example: ›
consts gcd :: "nat×nat ==> nat" recdef gcd "measure (λ(m,n).n)" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
text‹\noindent According to the measure function, the second argument should decrease with each recursive call. The resulting termination condition @{term[display]"n ~= (0::nat) ==> m mod n 🚫"} is proved automatically because it is already present as a lemma in HOL\@. Thus the recursion equation becomes a simplification rule. Of course the equation is nonterminating if we are allowed to unfold the recursive call inside the ‹else› b
languages and our simplifier don't do that. Unfortunately the simplifier does
something else that leads to the same problem: it splits
each ‹if›-expression unless its
condition simplifies to @{term True} or @{term False}. For
example, simplification reduces
@{term[display]"gcd(m,n) = k"} in one step to
@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"} where the condition cannot be reduced further, and splitting leads to
@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
an ‹if›, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.
The most radical solution isto disable the offending theorem
@{thm[source]if_split},
as shown in\S\ref{sec:AutoCaseSplits}. However, we do not recommend this
approach: you will often havetoinvoke the rule explicitly when ‹if›is involved.
If possible, the definition should be given by pattern matching on the left
rather than ‹if› on the right. In the case of @{term gcd} the
following alternative definition suggests itself: ›
text‹\noindent The order of equations is important: it hides the side condition @{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction may not be expressible by pattern matching. A simple alternative is to replace ‹if› b
which isalso available for @{typ bool} andis not split automatically: ›
consts gcd2 :: "nat×nat ==> nat" recdef gcd2 "measure (λ(m,n).n)" "gcd2(m,n) = (case n=0 of True ==> m | False ==> gcd2(n,m mod n))"
text‹\noindent This is probably the neatest solution next to pattern matching, and it is always available. A final alternative is to replace the offending simplification rules by derived conditional ones. For @{term gcd} it means we have to prove these lemmas: ›
lemma [simp]: "gcd (m, 0) = m" apply(simp) done
lemma [simp]: "n ≠ 0 ==> gcd(m, n) = gcd(n, m mod n)" apply(simp) done
text‹\noindent Simplification terminates for these proofs because the condition of the ‹if› s
Now we can disable the original simplification rule: ›
declare gcd.simps [simp del]
(*<*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-04-27)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
