commit by user andrea

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 5898be246e0e275d3f40fb095e9e851a37b734c6..638b7ac912797284c79183abe310d0c5df90d6b1 100644 (file)
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -3,51 +3,52 @@
 include "While/syntax.ma". 
 include "arithmetics/div_and_mod.ma". 
 
-
 (* state *)
 
-\ 5img class="anchor" src="icons/tick.png" id="state"\ 6definition 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]].
+
+definition update : state → Var → nat → state ≝ λs,v,a,v1. 
+  if eqvar v1 v then a else s v1.
 
-\ 5pre class="smallmargin" style="display: inline;"\ 6\ 5img class="anchor" src="icons/tick.png" id="evalA"\ 6let rec evalA a s ≝
+
+(* Semantics of Arithmetic expressions *)
+\ 5pre class="smallmargin" style="display: inline;"\ 6
+let rec evalA a s ≝
   match a with 
   [ Const n => n
   | Aid v => s v
-  | Add a b => evalA a s\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6evalA b s
-  | Sub a b => evalA a s\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6evalA b s
-  | Mul a b => evalA a s\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6evalA b s
-  | Div a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 (evalA a s) (evalA b s)
-  | Mod a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 (evalA a s) (evalA b s) 
+  | 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) 
   ]
  .
 
-\ 5img class="anchor" src="icons/tick.png" id="exA1"\ 6example exA1: \ 5a href="cic:/matita/While/semantics/evalA.fix(0,0,4)"\ 6evalA\ 5/a\ 6 ((\ 5a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"\ 6Const\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6)\ 5a href="cic:/fakeuri.def(1)" title="Aexp plus"\ 6+\ 5/a\ 6(\ 5a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"\ 6Const\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 63\ 5/a\ 6)) (λx.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 65\ 5/a\ 6.
-normalize //\ 5/pre\ 6. 
-
-(* 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
-.
-
- 
\ 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

diff --git a/weblib/test.ma b/weblib/test.ma
index 63a4794a140447e64cdfb4eb0eacf529c2759d88..922d36cc25cc155218d095eaccb4e511012c8c9c 100644 (file)
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -55,4 +55,4 @@
  *    examples that the user is encouraged to try after chapter1.ma)
  * 3) follow the instructions in the script.
  *
- *)
+ *)
\ No newline at end of file