commit by user andrea

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index ec11cf2ec002457254c6a2094ce13bbd0a1a5155..5898be246e0e275d3f40fb095e9e851a37b734c6 100644 (file)
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -1,29 +1,29 @@
 (* 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.
+\ 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.
 
 (* Semantics of Arithmetic expressions *)
 
-\ 5pre class="smallmargin" style="display: inline;"\ 6let rec eval_Aexp a s ≝
+\ 5pre class="smallmargin" style="display: inline;"\ 6\ 5img class="anchor" src="icons/tick.png" id="evalA"\ 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\ 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) 
+  ]
  .
 
-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).
+\ 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] ≝
@@ -50,4 +50,4 @@ inductive Cmd : Type[0] ≝
   | 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
+ 
\ No newline at end of file