Theory AExp

section "Arithmetic and Boolean Expressions"

theory AExp imports Main begin

subsection "Arithmetic Expressions"

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"

datatype aexp = N int | V vname | Plus aexp aexp | Times aexp aexp | Div aexp aexp

fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a⇩1 a⇩2) s = aval a⇩1 s + aval a⇩2 s"|
"aval (Times a⇩1 a⇩2) s = aval a⇩1 s * aval a⇩2 s"|
"aval (Div a⇩1 a⇩2) s = aval a⇩1 s div aval a⇩2 s"


value "aval (Plus (V ''x'') (N 5)) (λx. if x = ''x'' then 7 else 0)"

text ‹The same state more concisely:›
value "aval (Plus (V ''x'') (N 5)) ((λx. 0) (''x'':= 7))"

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"
 
end