From 9a3b49d3584873c77a39107cb5ee4f1e6010e43c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 17 Jul 2007 10:00:30 +0000
Subject: [PATCH] fixed includes and added notation for bytes

---
 helm/software/matita/library/assembly/byte.ma |  8 ++-
 .../matita/library/assembly/exadecimal.ma     |  4 +-
 helm/software/matita/library/assembly/test.ma | 70 +++++++++----------
 helm/software/matita/library/assembly/vm.ma   |  8 ++-
 4 files changed, 47 insertions(+), 43 deletions(-)

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 4d050e0cd..8c7be0308 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -14,13 +14,17 @@
 
 set "baseuri" "cic:/matita/assembly/byte".
 
-include "exadecimal.ma".
+include "assembly/exadecimal.ma".
 
 record byte : Type ≝ {
  bh: exadecimal;
  bl: exadecimal
 }.
 
+notation "〈 x, y 〉" non associative with precedence 80 for @{ 'mk_byte $x $y }.
+interpretation "mk_byte" 'mk_byte x y = 
+ (cic:/matita/assembly/byte/byte.ind#xpointer(1/1/1) x y).
+
 definition eqbyte ≝
  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 
@@ -205,7 +209,7 @@ qed.
 
 
 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
- ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
+ ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b))) = false.
  intros;
  unfold byte_of_nat;
  cut (b < 15 ∨ b ≥ 15);
diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index 7dfd42bb1..fb1a14ede 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/assembly/exadecimal/".
 
-include "extra.ma".
+include "assembly/extra.ma".
 
 inductive exadecimal : Type ≝
    x0: exadecimal
@@ -927,4 +927,4 @@ lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
  intros;
  rewrite > exadecimal_of_nat_mod;
  rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
-*)
\ No newline at end of file
+*)
diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index 1fd030efb..a917e34ff 100644
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/matita/library/assembly/test.ma
@@ -14,30 +14,24 @@
 
 set "baseuri" "cic:/matita/assembly/test/".
 
-include "vm.ma".
-
-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).
+include "assembly/vm.ma".
 
 definition mult_source : list byte ≝
-  [#LDAi; mk_byte x0 x0; (* A := 0 *)
-   #STAd; mk_byte x2 x0; (* Z := A *)
-   #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
-   #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
-   #LDAd; mk_byte x2 x0; (* A := Z *)
-   #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
-   #ADDd; mk_byte x1 xE; (* A += X *)
-   #STAd; mk_byte x2 x0; (* Z := A *)
-   #BRA;  mk_byte xF x2; (* goto l1 *)
-   #LDAd; mk_byte x2 x0].(* (l2) *)
+  [#LDAi; 〈x0, x0〉; (* A := 0 *)
+   #STAd; 〈x2, x0〉; (* Z := A *)
+   #LDAd; 〈x1, xF〉; (* (l1) A := Y *)
+   #BEQ;  〈x0, xA〉; (* if A == 0 then goto l2 *)
+   #LDAd; 〈x2, x0〉; (* A := Z *)
+   #DECd; 〈x1, xF〉; (* Y := Y - 1 *)
+   #ADDd; 〈x1, xE〉; (* A += X *)
+   #STAd; 〈x2, x0〉; (* Z := A *)
+   #BRA;  〈xF, x2〉; (* goto l1 *)
+   #LDAd; 〈x2, x0〉].(* (l2) *)
 
 definition mult_memory ≝
  λx,y.λa:addr.
      match leb a 29 with
-      [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
+      [ true ⇒ nth ? mult_source 〈x0, x0〉 a
       | false ⇒
          match eqb a 30 with
           [ true ⇒ x
@@ -47,11 +41,11 @@ definition mult_memory ≝
 
 definition mult_status ≝
  λx,y.
-  mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
+  mk_status 〈x0, x0〉 0 0 false false (mult_memory x y) 0.
 
 lemma test_O_O:
   let i ≝ 14 in
-  let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
+  let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in
    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
  normalize;
  split;
@@ -59,8 +53,8 @@ lemma test_O_O:
 qed.
 
 lemma test_0_2:
-  let x ≝ mk_byte x0 x0 in
-  let y ≝ mk_byte x0 x2 in
+  let x ≝ 〈x0, x0〉 in
+  let y ≝ 〈x0, x2〉 in
   let i ≝ 14 + 23 * nat_of_byte y in
   let s ≝ execute (mult_status x y) i in
    pc s = 20 ∧ mem s 32 = plusbytenc x x.
@@ -71,14 +65,14 @@ qed.
 
 lemma test_x_1:
  ∀x.
-  let y ≝ mk_byte x0 x1 in
+  let y ≝ 〈x0, x1〉 in
   let i ≝ 14 + 23 * nat_of_byte y in
   let s ≝ execute (mult_status x y) i in
    pc s = 20 ∧ mem s 32 = x.
  intros;
  split;
   [ reflexivity
-  | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
+  | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x);
     rewrite > plusbytenc_O_x;
     reflexivity
   ].
@@ -86,7 +80,7 @@ qed.
 
 lemma test_x_2:
  ∀x.
-  let y ≝ mk_byte x0 x2 in
+  let y ≝ 〈x0, x2〉 in
   let i ≝ 14 + 23 * nat_of_byte y in
   let s ≝ execute (mult_status x y) i in
    pc s = 20 ∧ mem s 32 = plusbytenc x x.
@@ -94,7 +88,7 @@ lemma test_x_2:
  split;
   [ reflexivity
   | change in ⊢ (? ? % ?) with
-     (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
+     (plusbytenc (plusbytenc 〈x0, x0〉 x) x);
     rewrite > plusbytenc_O_x;
     reflexivity
   ].
@@ -104,7 +98,7 @@ lemma loop_invariant':
  ∀x,y:byte.∀j:nat. j ≤ y →
   execute (mult_status x y) (5 + 23*j)
    =
-    mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
+    mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈x0, x0〉 (byte_of_nat (x*j)))
      (plusbytec (byte_of_nat (x*pred j)) x)
      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
       (byte_of_nat (x * j)))
@@ -121,7 +115,7 @@ lemma loop_invariant':
       rewrite < minus_n_O;
       normalize in ⊢ (? ? (? (? ? %) ?) ?);
       whd in ⊢ (? ? % ?);
-      change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 (mk_byte x0 x0) a);
+      change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a);
       change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31
         (byte_of_nat y)) 32 (byte_of_nat 0) a);
       change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
@@ -154,7 +148,7 @@ lemma loop_invariant':
            letin K ≝
             (breakpoint
               (mk_status (byte_of_nat (x*n)) 4 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+               (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
                (plusbytec (byte_of_nat (x*pred n)) x)
                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
                (byte_of_nat (x*n))) O)
@@ -171,7 +165,7 @@ lemma loop_invariant':
            letin K ≝
             (breakpoint
               (mk_status (byte_of_nat (S a)) 6 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+               (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
                (plusbytec (byte_of_nat (x*pred n)) x)
                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
                  (byte_of_nat (x*n))) O)
@@ -186,7 +180,7 @@ lemma loop_invariant':
            letin K ≝
             (breakpoint
               (mk_status (byte_of_nat (S a)) 8 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+               (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
                (plusbytec (byte_of_nat (x*pred n)) x)
                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
                  (byte_of_nat (x*n))) O)
@@ -196,12 +190,12 @@ lemma loop_invariant':
            whd in ⊢ (? ? (? % ?) ?);
            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
+           change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
            (* instruction DECd *)
            letin K ≝
             (breakpoint
              (mk_status (byte_of_nat (x*n)) 10 O
-              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+              (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
               (plusbytec (byte_of_nat (x*pred n)) x)
                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
                 (byte_of_nat (x*n))) O)
@@ -222,7 +216,7 @@ lemma loop_invariant':
            letin K ≝
             (breakpoint
              (mk_status (byte_of_nat (x*n)) 12
-              O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
+              O (eqbyte 〈x0, x0〉 (byte_of_nat (y-S n)))
               (plusbytec (byte_of_nat (x*pred n)) x)
               (update
                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
@@ -244,7 +238,7 @@ lemma loop_invariant':
            letin K ≝
             (breakpoint
              (mk_status (byte_of_nat (x*S n)) 14 O
-              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
+              (eqbyte 〈x0, x0〉 (byte_of_nat (x*S n)))
               (plusbytec (byte_of_nat (x*n)) x)
                (update
                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
@@ -316,10 +310,10 @@ theorem test_x_y:
   let i ≝ 14 + 23 * y in
    execute (mult_status x y) i =
     mk_status (byte_of_nat (x*y)) 20 0
-     (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
+     (eqbyte 〈x0, x0〉 (byte_of_nat (x*y)))
      (plusbytec (byte_of_nat (x*pred y)) x)
      (update
-       (update (mult_memory x y) 31 (mk_byte x0 x0))
+       (update (mult_memory x y) 31 〈x0, x0〉)
        32 (byte_of_nat (x*y)))
      0.
  intros;
@@ -335,7 +329,7 @@ theorem test_x_y:
         | intro;
           change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
-           update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
+           update (update (mult_memory x y) 31 〈x0, x0〉) 32
 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
           apply inj_update; intro;
           apply inj_update; intro;
diff --git a/helm/software/matita/library/assembly/vm.ma b/helm/software/matita/library/assembly/vm.ma
index 239146a07..162b5df0f 100644
--- a/helm/software/matita/library/assembly/vm.ma
+++ b/helm/software/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;
-- 
2.39.2