(* Author: Tobias Nipkow *) theory Def_Ass_Exp imports Vars begin subsection "Initialization-Sensitive Expressions Evaluation" types val = "nat" state = "name \ val option" fun aval :: "aexp \ state \ val option" where "aval (N i) s = Some i" | "aval (V x) s = s x" | "aval (Plus a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of (Some i\<^isub>1,Some i\<^isub>2) \ Some(i\<^isub>1+i\<^isub>2) | _ \ None)" fun bval :: "bexp \ state \ bool option" where "bval (B bv) s = Some bv" | "bval (Not b) s = (case bval b s of None \ None | Some bv \ Some(\ bv))" | "bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of (Some bv\<^isub>1, Some bv\<^isub>2) \ Some(bv\<^isub>1 & bv\<^isub>2) | _ \ None)" | "bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of (Some i\<^isub>1, Some i\<^isub>2) \ Some(i\<^isub>1 < i\<^isub>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