Theory Def_Init_Exp

(* Author: Tobias Nipkow *)

theory Def_Init_Exp
imports Vars

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 a1 a2) s =
  (case (aval a1 s, aval a2 s) of
     (Some i1,Some i2)  Some(i1+i2) | _  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 b1 b2) s = (case (bval b1 s, bval b2 s) of
  (Some bv1, Some bv2)  Some(bv1 & bv2) | _  None)" |
"bval (Less a1 a2) s = (case (aval a1 s, aval a2 s) of
 (Some i1, Some i2)  Some(i1 < i2) | _  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)