X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fbyte.ma;h=f2d1dc1566b7194903c2eda58d1eafd853a37ff9;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=4d050e0cda93fadd1d08b10b07b5268cbde01e48;hpb=ee24d241030e7577e5456f6dd151faf7622b86ce;p=helm.git

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 4d050e0cd..f2d1dc156 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').
 
@@ -38,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;
@@ -59,7 +66,7 @@ lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
     simplify in Hf:(? ? %);
     assumption
-  | autobatch
+  | apply le_times_r. apply H'.
   ]
 qed.
 
@@ -100,7 +107,7 @@ lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
     rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
     rewrite > divides_to_eq_mod_mod_mod;
      [ reflexivity
-     | autobatch
+     | apply (witness ? ? 16). reflexivity.
      ]
   ]
 qed.
@@ -110,7 +117,8 @@ lemma plusbyte_ok:
   match plusbyte b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
    ].
- intros;
+ intros; elim daemon.
+ (* 
  unfold plusbyte;
  generalize in match (plusex_ok (bl b1) (bl b2) c);
  elim (plusex (bl b1) (bl b2) c);
@@ -142,6 +150,7 @@ lemma plusbyte_ok:
  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
  rewrite > H; clear H;
  autobatch paramodulation.
+ *)
 qed.
 
 definition bpred ≝
@@ -214,11 +223,8 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); 
       rewrite > eq_eqex_S_x0_false;
        [ elim (eqex (bh (mk_byte x0 x0))
-(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
-(*
- alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
-         rewrite > andb_sym;
-*)
+          (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));
+         simplify;
          reflexivity
        | assumption
        ]
@@ -246,7 +252,7 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
              apply lt_mod_m_m;autobatch
             |rewrite > sym_times;
              rewrite > sym_times in ⊢ (? ? %); (* just to speed up qed *)
-             normalize in \vdash (? ? %);apply Hletin;
+             normalize in ⊢ (? ? %);apply Hletin;
             ]
           ] 
        ]
@@ -255,9 +261,10 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
   ].
 qed.
 
+axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
+
 lemma eq_bpred_S_a_a:
  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
-(*
  intros;
  unfold bpred;
  apply (bool_elim ? (eqex (bl (byte_of_nat (S a))) x0)); intros;
@@ -268,26 +275,40 @@ lemma eq_bpred_S_a_a:
     unfold byte_of_nat;
     change with (mk_byte (xpred (exadecimal_of_nat (S a/16))) xF =
                  mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
-    
-    
-  |
- change in ⊢ (? ? match ? % ? in bool return ? with [true\rArr ?|false\rArr ?] ?);
- unfold byte_of_nat;
- unfold bpred;
- simplify;
-*)
-elim daemon. (*
- intros;
- unfold byte_of_nat;
- cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
-  [ elim Hcut;
-     [ 
-     |
-     ]
-  | autobatch
-  ].*)
+    lapply (eqex_true_to_eq ? ? H1); clear H1;
+    unfold byte_of_nat in Hletin;
+    change in Hletin with (exadecimal_of_nat (S a) = x0);
+    lapply (eq_f ? ? nat_of_exadecimal ? ? Hletin); clear Hletin;
+    normalize in Hletin1:(? ? ? %);
+    rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
+    elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
+    rewrite > H1;
+    rewrite > div_times_ltO; [2: autobatch | ]
+    lapply (eq_f ? ? (λx.x/16) ? ? H1);
+    rewrite > div_times_ltO in Hletin; [2: autobatch | ]
+    lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
+    rewrite > eq_mod_times_n_m_m_O in Hletin1;
+    elim daemon
+  | change with (mk_byte (bh (byte_of_nat (S a))) (xpred (bl (byte_of_nat (S a))))
+    = byte_of_nat a);
+    unfold byte_of_nat;
+    change with (mk_byte (exadecimal_of_nat (S a/16)) (xpred (exadecimal_of_nat (S a)))
+    = mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
+    lapply (eqex_false_to_not_eq ? ? H1);
+    unfold byte_of_nat in Hletin;
+    change in Hletin with (exadecimal_of_nat (S a) ≠ x0);
+    cut (nat_of_exadecimal (exadecimal_of_nat (S a)) ≠ 0);
+     [2: intro;
+       apply Hletin;
+       lapply (eq_f ? ? exadecimal_of_nat ? ? H2);
+       rewrite > exadecimal_of_nat_nat_of_exadecimal in Hletin1;
+       apply Hletin1
+     | ];
+     
+    elim daemon
+  ]
 qed.
- 
+
 lemma plusbytenc_S:
  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
  intros;