Theory HOL-Real_Asymp.Lazy_Eval

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