Theory Def_Init_Exp

(* Author: Tobias Nipkow *)

theory Def_Init_Exp
imports Vars
begin

subsection "Initialization-Sensitive Expressions Evaluation"

type_synonym state = "vname ⇒ val option"


fun aval :: "aexp ⇒ state ⇒ val option" where
"aval (N i) s = Some i" |
"aval (V x) s = s x" |
"aval (Plus a⇩1 a⇩2) s =
  (case (aval a⇩1 s, aval a⇩2 s) of
     (Some i⇩1,Some i⇩2) ⇒ Some(i⇩1+i⇩2) | _ ⇒ None)"


fun bval :: "bexp ⇒ state ⇒ bool option" where
"bval (Bc v) s = Some v" |
"bval (Not b) s = (case bval b s of None ⇒ None | Some bv ⇒ Some(¬ bv))" |
"bval (And b⇩1 b⇩2) s = (case (bval b⇩1 s, bval b⇩2 s) of
  (Some bv⇩1, Some bv⇩2) ⇒ Some(bv⇩1 & bv⇩2) | _ ⇒ None)" |
"bval (Less a⇩1 a⇩2) s = (case (aval a⇩1 s, aval a⇩2 s) of
 (Some i⇩1, Some i⇩2) ⇒ Some(i⇩1 < i⇩2) | _ ⇒ None)"


lemma aval_Some: "vars a ⊆ dom s ⟹ ∃ i. aval a s = Some i"
by (induct a) auto

lemma bval_Some: "vars b ⊆ dom s ⟹ ∃ bv. bval b s = Some bv"
by (induct b) (auto dest!: aval_Some)

end