weblib/While/semantics.ma

   1 (* new script *)
   2
   3 include "While/syntax.ma".
   4 include "arithmetics/div_and_mod.ma".
   5
   6
   7 (* state *)
   8
   9 \ 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.
  10
  11 (* Semantics of Arithmetic expressions *)
  12
  13 \ 5pre class="smallmargin" style="display: inline;"\ 6\ 5img class="anchor" src="icons/tick.png" id="evalA"\ 6let rec evalA a s ≝
  14   match a with
  15   [ Const n => n
  16   | Aid v => s v
  17   | Add a b => evalA a s\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6evalA b s
  18   | Sub a b => evalA a s\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6evalA b s
  19   | Mul a b => evalA a s\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6evalA b s
  20   | Div a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 (evalA a s) (evalA b s)
  21   | Mod a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 (evalA a s) (evalA b s)
  22   ]
  23  .
  24
  25 \ 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.
  26 normalize //\ 5/pre\ 6.
  27
  28 (* Boolean expressions *)
  29 inductive Bexp : Type[0] ≝
  30   | BFalse : Bexp
  31   | BTtrue : Bexp
  32   | BNot : Bexp → Bexp
  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
  37 .
  38
  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).
  43
  44 (* Commands *)
  45 inductive Cmd : Type[0] ≝
  46   | Skip : Cmd
  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
  51 .
  52
  53