X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fbyte.ma;h=2bf233ec19d0686ea9b84cd6e06b7cf12dfe18b4;hb=1292d243af469c5cb3dcb3677d84012420de015e;hp=f97b13f293a131b4a2c7bb3b4c223aa37779e90d;hpb=792862d32bb2c8de0449c28691d93372313f2309;p=helm.git

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index f97b13f29..2bf233ec1 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;
@@ -63,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.
 
@@ -104,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.
@@ -114,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);
@@ -146,6 +150,7 @@ lemma plusbyte_ok:
  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
  rewrite > H; clear H;
  autobatch paramodulation.
+ *)
 qed.
 
 definition bpred ≝
@@ -278,9 +283,9 @@ lemma eq_bpred_S_a_a:
     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 | ]
+    rewrite > lt_O_to_div_times; [2: autobatch | ]
     lapply (eq_f ? ? (λx.x/16) ? ? H1);
-    rewrite > div_times_ltO in Hletin; [2: autobatch | ]
+    rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
     rewrite > eq_mod_times_n_m_m_O in Hletin1;
     elim daemon