From 006db2fb5a2ccd6e5043b6809a620ac96603648c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jul 2007 09:15:31 +0000
Subject: [PATCH] Super-nice notation for the assembly stuff.

---
 helm/software/matita/library/assembly/byte.ma |  3 ++
 helm/software/matita/library/assembly/test.ma | 31 ++++++++++++++++---
 helm/software/matita/library/assembly/vm.ma   | 19 ++++++++++++
 3 files changed, 49 insertions(+), 4 deletions(-)

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index f97b13f29..583051e27 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -42,6 +42,9 @@ coercion cic:/matita/assembly/byte/nat_of_byte.con.
 definition byte_of_nat ≝
  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
 
+interpretation "byte_of_nat" 'byte_of_opcode a =
+ (cic:/matita/assembly/byte/byte_of_nat.con a).
+
 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
  intros;
  elim b;
diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index a917e34ff..1bbc1e710 100644
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/matita/library/assembly/test.ma
@@ -43,6 +43,24 @@ definition mult_status ≝
  λx,y.
   mk_status 〈x0, x0〉 0 0 false false (mult_memory x y) 0.
 
+notation " 'M' \sub (x y)" non associative with precedence 80 for 
+ @{ 'memory $x $y }.
+ 
+interpretation "mult_memory" 'memory x y = 
+  (cic:/matita/assembly/test/mult_memory.con x y).
+
+notation " 'M' \sub (x y) \nbsp a" non associative with precedence 80 for 
+ @{ 'memory4 $x $y $a }.
+ 
+interpretation "mult_memory4" 'memory4 x y a = 
+  (cic:/matita/assembly/test/mult_memory.con x y a).
+  
+notation " \Sigma \sub (x y)" non associative with precedence 80 for 
+ @{ 'status $x $y }.
+
+interpretation "mult_status" 'status x y =
+  (cic:/matita/assembly/test/mult_status.con x y).
+
 lemma test_O_O:
   let i ≝ 14 in
   let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in
@@ -52,6 +70,7 @@ lemma test_O_O:
  reflexivity.
 qed.
 
+(*
 lemma test_0_2:
   let x ≝ 〈x0, x0〉 in
   let y ≝ 〈x0, x2〉 in
@@ -62,6 +81,7 @@ lemma test_0_2:
  split;
  reflexivity.
 qed.
+*)
 
 lemma test_x_1:
  ∀x.
@@ -78,6 +98,7 @@ lemma test_x_1:
   ].
 qed.
 
+(*
 lemma test_x_2:
  ∀x.
   let y ≝ 〈x0, x2〉 in
@@ -93,6 +114,7 @@ lemma test_x_2:
     reflexivity
   ].
 qed.
+*)
 
 lemma loop_invariant':
  ∀x,y:byte.∀j:nat. j ≤ y →
@@ -114,7 +136,6 @@ lemma loop_invariant':
     | intro;
       rewrite < minus_n_O;
       normalize in ⊢ (? ? (? (? ? %) ?) ?);
-      whd in ⊢ (? ? % ?);
       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);
@@ -289,7 +310,7 @@ lemma loop_invariant':
             [ apply (y - S n)
             | split;
                [ rewrite < (minus_S_S y n);
-                 autobatch
+                 apply (minus_Sn_m (nat_of_byte y) (S n) H1)
                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
                  autobatch
@@ -305,12 +326,13 @@ lemma loop_invariant':
   ]   
 qed.
 
+
 theorem test_x_y:
  ∀x,y:byte.
   let i ≝ 14 + 23 * y in
    execute (mult_status x y) i =
-    mk_status (byte_of_nat (x*y)) 20 0
-     (eqbyte 〈x0, x0〉 (byte_of_nat (x*y)))
+    mk_status (#(x*y)) 20 0
+     (eqbyte 〈x0, x0〉 (#(x*y)))
      (plusbytec (byte_of_nat (x*pred y)) x)
      (update
        (update (mult_memory x y) 31 〈x0, x0〉)
@@ -327,6 +349,7 @@ theorem test_x_y:
        apply status_eq;
         [1,2,3,4,5,7: normalize; reflexivity
         | intro;
+        letin xxx \def ((mult_memory x y) { a ↦ x }).
           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 〈x0, x0〉) 32
diff --git a/helm/software/matita/library/assembly/vm.ma b/helm/software/matita/library/assembly/vm.ma
index 162b5df0f..30d073144 100644
--- a/helm/software/matita/library/assembly/vm.ma
+++ b/helm/software/matita/library/assembly/vm.ma
@@ -111,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.
-- 
2.39.2