1section \<open>Lazy evaluation within the logic\<close> 2theory Lazy_Eval 3imports 4 Complex_Main 5begin 6 7text \<open> 8 This is infrastructure to lazily evaluate an expression (typically something corecursive) 9 within the logic by simple rewriting. A signature of supported (co-)datatype constructures 10 upon which pattern matching is allowed and a list of function equations that are used in 11 rewriting must be provided. 12 13 One can then e.\,g.\ determine whether a given pattern matches a given expression. To do this, 14 the expression will be rewritten using the given function equations until enough constructors 15 have been exposed to decide whether the pattern matches. 16 17 This infrastructure was developed specifically for evaluating Multiseries expressions, but 18 can, in principle, be used for other purposes as well. 19\<close> 20 21lemma meta_eq_TrueE: "PROP P \<equiv> Trueprop True \<Longrightarrow> PROP P" by simp 22 23datatype cmp_result = LT | EQ | GT 24 25definition COMPARE :: "real \<Rightarrow> real \<Rightarrow> cmp_result" where 26 "COMPARE x y = (if x < y then LT else if x > y then GT else EQ)" 27 28lemma COMPARE_intros: 29 "x < y \<Longrightarrow> COMPARE x y \<equiv> LT" "x > y \<Longrightarrow> COMPARE x y \<equiv> GT" "x = y \<Longrightarrow> COMPARE x y \<equiv> EQ" 30 by (simp_all add: COMPARE_def) 31 32primrec CMP_BRANCH :: "cmp_result \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where 33 "CMP_BRANCH LT x y z = x" 34| "CMP_BRANCH EQ x y z = y" 35| "CMP_BRANCH GT x y z = z" 36 37ML_file \<open>lazy_eval.ML\<close> 38 39end