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 a1 a2) s = aval a1 s + aval a2 s"|
"aval (Times a1 a2) s = aval a1 s * aval a2 s"|
"aval (Div a1 a2) s = aval a1 s div aval a2 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
¤ Dauer der Verarbeitung: 0.7 Sekunden
¤
*© Formatika GbR, Deutschland
