Quelle simplification.thy

Sprache: Isabelle

(*<*)
theory simplification imports Main begin
(*>*)

text‹
we have proved all the termination conditions, the \isacommand{recdef}
equations become simplification rules, just as with
isacommand{primrec}. In most cases this works fine, but there is a subtle
that must be mentioned: simplification may not
because of automatic splitting of ‹if›.
index{*if expressions!splitting of}
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
to the measure function, the second argument should decrease with
recursive call. The resulting termination condition
{term[display]"n ~= (0::nat) ==> m mod n < n"}
proved automatically because it is already present as a lemma in
\@. Thus the recursion equation becomes a simplification
. Of course the equation is nonterminating if we are allowed to unfold
recursive call inside the ‹else› branch, which is why programming
and our simplifier don't do that. Unfortunately the simplifier does
else that leads to the same problem: it splits
‹if›-expression unless its
simplifies to @{term True} or @{term False}. For
, simplification reduces
{term[display]"gcd(m,n) = k"}
one step to
{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
the condition cannot be reduced further, and splitting leads to
{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
‹if›, it is unfolded again, which leads to an infinite chain of
steps. Fortunately, this problem can be avoided in many
ways.

most radical solution is to disable the offending theorem
{thm[source]if_split},
shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
: you will often have to invoke the rule explicitly when
‹if› is involved.

possible, the definition should be given by pattern matching on the left
than ‹if› on the right. In the case of @{term gcd} the
alternative definition suggests itself:
›

consts gcd1 :: "nat×nat ==> nat"
recdef gcd1 "measure (λ(m,n).n)"
  "gcd1 (m, 0) = m"
  "gcd1 (m, n) = gcd1(n, m mod n)"

text‹\noindent
order of equations is important: it hides the side condition
{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction
not be expressible by pattern matching.

simple alternative is to replace ‹if› by ‹case›,
is also available for @{typ bool} and is 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
is probably the neatest solution next to pattern matching, and it is
available.

final alternative is to replace the offending simplification rules by
conditional ones. For @{term gcd} it means we have to prove
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
terminates for these proofs because the condition of the ‹if› simplifies to @{term True} or @{term False}.
we can disable the original simplification rule:
›

declare gcd.simps [simp del]

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.