X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fassembly%2Fvm.ma;h=30d073144c486c8040f37d170f09673490cab525;hb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;hp=dac755c82c54484fb506596c11a7435a5e0eb857;hpb=5fe5171fa142cdd9370819e233c013b599b5d76c;p=helm.git

diff --git a/matita/library/assembly/vm.ma b/matita/library/assembly/vm.ma
index dac755c82..30d073144 100644
--- a/matita/library/assembly/vm.ma
+++ b/matita/library/assembly/vm.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/assembly/vm/".
 
-include "byte.ma".
+include "assembly/byte.ma".
 
 definition addr ≝ nat.
 
@@ -95,6 +95,12 @@ definition byte_of_opcode : opcode → byte ≝
   in
    aux opcodemap.
 
+notation "hvbox(# break a)"
+  non associative with precedence 80
+for @{ 'byte_of_opcode $a }.
+interpretation "byte_of_opcode" 'byte_of_opcode a =
+ (cic:/matita/assembly/vm/byte_of_opcode.con a).
+
 record status : Type ≝ {
   acc : byte;
   pc  : addr;
@@ -105,12 +111,31 @@ record status : Type ≝ {
   clk : nat
 }.
 
+notation "{hvbox('Acc' ≝ acc ; break 'Pc' ≝ pc ; break 'Spc' ≝ spc ; break 'Fz' ≝ fz ; break 'Fc' ≝ fc ; break  'M' ≝ m ; break 'Clk' ≝ clk)}"
+non associative with precedence 80 for
+ @{ 'mkstatus $acc $pc $spc $fz $fc $m $clk }.
+ 
+interpretation "mk_status" 'mkstatus acc pc spc fz fc m clk =
+ (cic:/matita/assembly/vm/status.ind#xpointer(1/1/1) acc pc spc fz fc m clk).
+
 definition update ≝
  λf: addr → byte.λa.λv.λx.
   match eqb x a with
    [ true ⇒ v
    | false ⇒ f x ].
 
+notation "hvbox(m break {a ↦ break v})" non associative with precedence 80 for 
+ @{ 'update $m $a $v }.
+ 
+notation "hvbox(m break {a ↦ break v} \nbsp x)" non associative with precedence 80 for 
+ @{ 'update4 $m $a $v $x }.
+ 
+interpretation "update" 'update m a v =
+  (cic:/matita/assembly/vm/update.con m a v).
+
+interpretation "update4" 'update4 m a v x =
+  (cic:/matita/assembly/vm/update.con m a v x).
+
 lemma update_update_a_a:
  ∀s,a,v1,v2,b.
   update (update s a v1) a v2 b = update s a v2 b.
@@ -139,6 +164,38 @@ lemma update_update_a_b:
  ].
 qed.
 
+lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
+ intros;
+ unfold update;
+ apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
+  [ rewrite > (eqb_true_to_eq ? ? H);
+    reflexivity
+  | reflexivity
+  ]
+qed.
+
+lemma inj_update:
+ ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
+ intros;
+ unfold update;
+ apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
+  [ reflexivity
+  | apply H;
+    intro;
+    autobatch
+  ]
+qed.
+
+lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
+ intros;
+ unfold update;
+ rewrite > not_eq_to_eqb_false; simplify;
+  [ reflexivity
+  | intro;
+    autobatch
+  ]
+qed.
+
 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
 
 definition tick ≝