Quelle Lazy_Eval.thy Sprache: Isabelle

section ‹Lazy evaluation within the logic›
theory Lazy_Eval
imports
  Complex_Main
begin

text ‹
This is infrastructure to lazily evaluate an expression (typically something corecursive)
within the logic by simple rewriting. A signature of supported (co-)datatype constructures
upon which pattern matching is allowed and a list of function equations that are used in
rewriting must be provided.

One can then e.\,g.\ determine whether a given pattern matches a given expression. To do this,
the expression will be rewritten using the given function equations until enough constructors
have been exposed to decide whether the pattern matches.

This infrastructure was developed specifically for evaluating Multiseries expressions, but
can, in principle, be used for other purposes as well.
›

lemma meta_eq_TrueE: "PROP P ≡ Trueprop True ==> PROP P" by simp

datatype cmp_result = LT | EQ | GT

definition COMPARE :: "real → real → cmp_result" where
  "COMPARE x y = (if x < y then LT else if x > y then GT else EQ)"

lemma COMPARE_intros:
  "x < y ==> COMPARE x y ≡ LT" "x > y ==> COMPARE x y ≡ GT" "x = y ==> COMPARE x y ≡ EQ"
  by (simp_all add: COMPARE_def)

primrec CMP_BRANCH :: "cmp_result → 'a → 'a → 'a → 'a" where
  "CMP_BRANCH LT x y z = x"
| "CMP_BRANCH EQ x y z = y"
| "CMP_BRANCH GT x y z = z"

ML_file ‹lazy_eval.ML›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-09-27) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

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.