X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fbyte8.ma;h=c49297e3a8a2e14f141a9d77e9dbd7b1475ec7e7;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=f3d2e10b441b23145c97bbcc38316f291664bb84;hpb=bbb941eb47625a07d36e0e45d6172cfa99bca027;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index f3d2e10b4..c49297e3a 100644
--- a/helm/software/matita/contribs/assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma
@@ -39,8 +39,7 @@ record byte8 : Type ≝
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
  for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y = 
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
 
 (* operatore = *)
 definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
@@ -151,7 +150,7 @@ definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 (* byte → naturali *)
 definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
 
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
 
 (* naturali → byte *)
 definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).
@@ -341,12 +340,12 @@ lemma nat_of_byte8_byte8_of_nat: ∀n. nat_of_byte8 (byte8_of_nat n) = n \mod 25
  rewrite > mod_plus in ⊢ (? ? % ?);
  rewrite > mod_plus in ⊢ (? ? ? %);
  apply eq_mod_to_eq_plus_mod;
- rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
- rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
+ rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch by divides_n_n];
+ rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch by divides_n_n];
  rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
  rewrite < mod_mod in ⊢ (? ? % ?);
   [ reflexivity
-  | autobatch
+  | autobatch by divides_n_n
   ].
 qed.
 
@@ -413,8 +412,11 @@ theorem plusb8nc_ok:
  rewrite > mod_plus;
  letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
-  [ autobatch | ];
- autobatch paramodulation.
+  [ unfold;apply le_S_S;apply le_O_n| ];
+ rewrite > K' in ⊢ (? ? ? (? (? ? %) ?));
+ rewrite < K in ⊢ (? ? ? (? (? % ?) ?));
+ rewrite < plus_n_O;
+ apply K;
 qed.
 
 lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
@@ -435,7 +437,7 @@ lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
     | unfold eq_b8;
       change in ⊢ (? ? (? % ?) ?) with (eq_ex x0 (exadecim_of_nat (S b/16)));
       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
-       [ autobatch
+       [ unfold; autobatch by le_S_S,le_O_n;
        | unfold in H1;
          apply le_S_S;
          assumption
@@ -448,12 +450,12 @@ lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
             unfold lt in H;
             rewrite < H2;
             clear H2; clear a; clear H1; clear Hcut;
-            apply (le_times_to_le 16) [ autobatch | ] ;
-            rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
-            rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
+            apply (le_times_to_le 16) [ autobatch by le_S_S,le_O_n;| ] ;
+            rewrite > (div_mod (S b) 16) in H;[2:unfold; autobatch by le_S_S,le_O_n;|]
+            rewrite > (div_mod 255 16) in H:(? ? %);[2:unfold; autobatch by le_S_S,le_O_n;|]
             lapply (le_to_le_plus_to_le ? ? ? ? ? H);
             [apply lt_S_to_le;
-             apply lt_mod_m_m;autobatch
+             apply lt_mod_m_m; unfold; apply le_S_S; apply le_O_n;
             |rewrite > sym_times;
              rewrite > sym_times in ⊢ (? ? %);
              normalize in ⊢ (? ? %);apply Hletin;
@@ -487,9 +489,9 @@ lemma eq_b8pred_S_a_a:
     rewrite > nat_of_exadecim_exadecim_of_nat in Hletin1;
     elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
     rewrite > H1;
-    rewrite > lt_O_to_div_times; [2: autobatch | ]
+    rewrite > lt_O_to_div_times; [2: unfold; apply le_S_S; apply le_O_n; | ]
     lapply (eq_f ? ? (λx.x/16) ? ? H1);
-    rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
+    rewrite > lt_O_to_div_times in Hletin; [2: unfold; apply le_S_S; apply le_O_n; | ]
     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
     rewrite > eq_mod_times_n_m_m_O in Hletin1;
     elim daemon
@@ -522,7 +524,7 @@ lemma plusb8nc_S:
  rewrite > eq_nat_of_byte8_n_nat_of_byte8_mod_n_256 in ⊢ (? ? ? %);
  rewrite > mod_plus in ⊢ (? ? (? %) ?);
  rewrite > mod_plus in ⊢ (? ? ? (? %));
- rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
+ rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: apply divides_n_n; | ];
  rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
  reflexivity.
 qed.