(* new script *)
-include "While/syntax.ma".
+include "While/syntax.ma".
+include "arithmetics/div_and_mod.ma.
(* state *)
-definition state ≝ \
\ No newline at end of file
+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.
+
+(* Semantics of Arithmetic expressions *)
+
+\ 5pre class="smallmargin" style="display: inline;"\ 6let rec eval_Aexp a s ≝
+ match a with
+ | Const n => n
+ | Aid v => s v
+ | Add a b => a+b
+ | Sub a b => a-b
+ | Mul a b => a*b
+ | Div a b => div a b
+ | Mod a b => mod a b
+ .
+
+interpretation "Aexp plus" 'plus x y = (Add x y).
+interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp times" 'times x y = (Mul x y).
+
+(* Boolean expressions *)
+inductive Bexp : Type[0] ≝
+ | BFalse : Bexp
+ | BTtrue : Bexp
+ | BNot : Bexp → Bexp
+ | BAnd : Bexp → Bexp → Bexp
+ | BOr : Bexp → Bexp → Bexp
+ | 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
+ | 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
+.
+
+interpretation "Bexp not" 'not x = (BNot x).
+interpretation "Bexp and" 'and x y = (BAnd x y).
+interpretation "Bexp or" 'or x y = (BOr x y).
+interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
+
+(* Commands *)
+inductive Cmd : Type[0] ≝
+ | Skip : Cmd
+ | Assign : Var → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Cmd
+ | Seq : Cmd → Cmd → Cmd
+ | If : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd → Cmd
+ | While : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd
+.
+
+\ 5/pre\ 6
\ No newline at end of file
projects / helm.git / blobdiff