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