section "Arithmetic and Boolean Expressions" theory AExp imports Main "~~/src/HOL/Library/Extended_Real" begin subsection "Arithmetic Expressions" type_synonym vname = string type_synonym val = "ereal option" type_synonym state = "vname \ val" text_raw{*\snip{AExpaexpdef}{2}{1}{% *} datatype aexp = N ereal | V vname | Plus aexp aexp text_raw{*}%endsnip*} text_raw{*\snip{AExpavaldef}{1}{2}{% *} fun aval :: "aexp \ state \ val" where "aval (N n) s = Some n" | "aval (V x) s = s x" | "aval (Plus a\<^sub>1 a\<^sub>2) s = ( case (aval a\<^sub>1 s, aval a\<^sub>2 s) of (None, _) \ None | (_, None) \ None | (Some PInfty, Some MInfty) \ None | (Some MInfty, Some PInfty) \ None | (Some x, Some y) \ Some (x + y) ) " text_raw{*}%endsnip*} text {* A little syntax magic to write larger states compactly: *} definition null_state ("<>") where "null_state \ \x. 0" syntax "_State" :: "updbinds => 'a" ("<_>") translations "_State ms" == "_Update <> ms" "_State (_updbinds b bs)" <= "_Update (_State b) bs" text {* \noindent We can now write a series of updates to the function @{text "\x. 0"} compactly: *} lemma " = (<> (a := 1)) (b := (2::int))" by (rule refl) end