Quelle  Def_Init_Exp.thy   Sprache: Isabelle

(* 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\<^sub>1 a\<^sub>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\<^sub>1 b\<^sub>2) s = (case (bval b\<^sub>1 s, bval b\<^sub>2 s) of
  (Some bv🚫1, Some bv🚫2) ==> Some(bv🚫1 & bv🚫2) | _ ==> None)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (case (aval a\<^sub>1 s, aval a\<^sub>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