3 include "While/syntax.ma".
4 include "arithmetics/div_and_mod.ma.
9 definition state ≝
\ 5a href="cic:/matita/While/syntax/Var.ind(1,0,0)"
\ 6Var
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
11 (* Semantics of Arithmetic expressions *)
13 \ 5pre class="smallmargin" style="display: inline;"
\ 6let rec eval_Aexp a s ≝
24 interpretation "Aexp plus" 'plus x y = (Add x y).
25 interpretation "Aexp minus" 'plus x y = (Sub x y).
26 interpretation "Aexp times" 'times x y = (Mul x y).
28 (* Boolean expressions *)
29 inductive Bexp : Type[0] ≝
33 | BAnd : Bexp → Bexp → Bexp
34 | BOr : Bexp → Bexp → Bexp
35 | Eq :
\ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"
\ 6Aexp
\ 5/a
\ 6 →
\ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"
\ 6Aexp
\ 5/a
\ 6 → Bexp
36 | LE :
\ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"
\ 6Aexp
\ 5/a
\ 6 →
\ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"
\ 6Aexp
\ 5/a
\ 6 → Bexp
39 interpretation "Bexp not" 'not x = (BNot x).
40 interpretation "Bexp and" 'and x y = (BAnd x y).
41 interpretation "Bexp or" 'or x y = (BOr x y).
42 interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
45 inductive Cmd : Type[0] ≝
47 | Assign : Var →
\ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"
\ 6Aexp
\ 5/a
\ 6 → Cmd
48 | Seq : Cmd → Cmd → Cmd
49 | If :
\ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"
\ 6Bexp
\ 5/a
\ 6 → Cmd → Cmd → Cmd
50 | While :
\ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"
\ 6Bexp
\ 5/a
\ 6 → Cmd → Cmd