From ef335c7310bd175a2df936eb284fed6142ee0b6e Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 10 Apr 2013 11:43:43 +0000 Subject: [PATCH] commit by user andrea --- weblib/While/semantics.ma | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma index ec11cf2ec..5898be246 100644 --- 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 ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +img class="anchor" src="icons/tick.png" id="state"definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (* Semantics of Arithmetic expressions *) -pre class="smallmargin" style="display: inline;"let rec eval_Aexp a s ≝ +pre class="smallmargin" style="display: inline;"img class="anchor" src="icons/tick.png" id="evalA"let 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 sa title="natural plus" href="cic:/fakeuri.def(1)"+/aevalA b s + | Sub a b => evalA a sa title="natural minus" href="cic:/fakeuri.def(1)"-/aevalA b s + | Mul a b => evalA a sa title="natural times" href="cic:/fakeuri.def(1)"*/aevalA b s + | Div a b => a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a (evalA a s) (evalA b s) + | Mod a b => a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a (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). +img class="anchor" src="icons/tick.png" id="exA1"example exA1: a href="cic:/matita/While/semantics/evalA.fix(0,0,4)"evalA/a ((a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"2/a)a href="cic:/fakeuri.def(1)" title="Aexp plus"+/a(a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"3/a)) (λx.a title="natural number" href="cic:/fakeuri.def(1)"0/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"5/a. +normalize ///pre. (* Boolean expressions *) inductive Bexp : Type[0] ≝ @@ -50,4 +50,4 @@ inductive Cmd : Type[0] ≝ | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd . -/pre \ No newline at end of file + \ No newline at end of file -- 2.39.2