(* new script *)
include "While/syntax.ma".
-include "arithmetics/div_and_mod.ma.
-
+include "arithmetics/div_and_mod.ma".
(* state *)
-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.
+definition state ≝ Var → nat.
-(* Semantics of Arithmetic expressions *)
+definition eqvar ≝ λv1,v2.
+ match v1 with
+ [Id n => match v2 with [Id m => eqb n m]].
-\ 5pre class="smallmargin" style="display: inline;"\ 6let rec eval_Aexp a s ≝
+definition update : state → Var → nat → state ≝ λs,v,a,v1.
+ if eqvar v1 v then a else s v1.
+
+(* Semantics of Arithmetic expressions *)
+\ 5pre class="smallmargin" style="display: inline;"\ 6let rec evalA a s ≝
match a with
- | Const n => n
+ [ 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
+ | Add a b => evalA a s+evalA b s
+ | Sub a b => evalA a s-evalA b s
+ | Mul a b => evalA a s*evalA b s
+ | Div a b => div (evalA a s) (evalA b s)
+ | Mod a b => mod (evalA a s) (evalA b s)
+ ]
.
-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
+example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.\ 5span style="text-decoration: underline;"\ 61\ 5/span\ 6) = \ 5span style="text-decoration: underline;"\ 65\ 5/span\ 6.
+normalize // qed
+
+let rec evalB b s ≝
+ match b with
+ [ BFalse => false
+ | BTtrue => true
+ | BNot b => ¬(evalB b s)
+ | BAnd b1 b2 => evalB b1 s ∧ evalB b2 s
+ | BOr b1 b2 => evalB b1 s ∨ evalB b2 s \ 5pre class="smallmargin" style="display: inline;"\ 6\ 5/pre\ 6
+ | Eq a1 a2 => eqb (evalA a1 s) (evalA a2 s)
+ | LE a1 a2 => leb (evalA a1 s) (evalA a2 s)
+ ].
+
+inductive Cmd_sem: Cmd → state → state\ 5pre class="smallmargin" style="display: inline;"\ 6→ Prop\ 5/pre\ 6≝
+ | Skip_sem : \forall s. Cmd_sem Skip s s
+ | Assign_sem : \forall s,v,a. Cmd_sem (Assign v a) s (update s v (evalA a s))
+ | Seq_sem : \forall c1,c2,s1,s2,s3. Cmd_sem c1 s1 s2 \to Cmd_sem c2 s2 s3 \to Cmd_sem (Seq c1 c2) s1 s3
+ | If_sem_true : \forall b,ct,cf,s,st. evalB b s = true \to Cmd_sem ct s st \to Cmd_sem (If b ct cf) s st
+ | If_sem_false : \forall b,ct,cf,s,sf. evalB b s = false \to Cmd_sem cf s sf \to Cmd_sem (If b ct cf) s sf
+ | While_true : \forall b,c,s,s1,s2. evalB b s = true \to Cmd_sem c s s1 \to Cmd_sem (While b c) s1 s2 \to Cmd_sem (While b c) s s2
+ | While_false : \forall b,c,s. evalB b s = false \to Cmd_sem (While b c) s s
+.\ 5/pre\ 6
\ No newline at end of file