43158

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Def_Ass_Exp imports Vars


4 
begin


5 


6 
subsection "InitializationSensitive Expressions Evaluation"


7 

45212

8 
type_synonym state = "vname \<Rightarrow> val option"

43158

9 


10 


11 
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where


12 
"aval (N i) s = Some i" 


13 
"aval (V x) s = s x" 


14 
"aval (Plus a\<^isub>1 a\<^isub>2) s =


15 
(case (aval a\<^isub>1 s, aval a\<^isub>2 s) of


16 
(Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2)  _ \<Rightarrow> None)"


17 


18 


19 
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where

45200

20 
"bval (Bc v) s = Some v" 

43158

21 
"bval (Not b) s = (case bval b s of None \<Rightarrow> None  Some bv \<Rightarrow> Some(\<not> bv))" 


22 
"bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of


23 
(Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2)  _ \<Rightarrow> None)" 


24 
"bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of


25 
(Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2)  _ \<Rightarrow> None)"


26 


27 


28 
lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"


29 
by (induct a) auto


30 


31 
lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"


32 
by (induct b) (auto dest!: aval_Some)


33 


34 
end
