X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2Fr.ma;h=9e7ba97f5afbb4c03c5c358bcd4f9c02ad9f8dd3;hb=765eb07cafb8a06a5027f4569ad06d805aba2488;hp=d47a1dc58bd18c0dbf472e35bc2e40d2a78717cc;hpb=dcef667a444aa0f189225855c1433d26b65fb8b7;p=helm.git

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index d47a1dc58..9e7ba97f5 100644
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -58,10 +58,11 @@ axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z).
 axiom Rtimes_x_R1 : ∀x.x * R1 = x.
 axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
 
-pump 200.
+(*pump 200.*)
+pump 40.
 
 lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
-intros; demodulate all. (*autobatch paramodulation;*)
+intros; autobatch; 
 qed.
 
 (* commutative field *)
@@ -77,28 +78,28 @@ axiom trichotomy_Rlt : ∀x,y.x < y ∨ y < x ∨ x = y.
 
 lemma trans_Rle : ∀x,y,z:R.x ≤ y → y ≤ z → x ≤ z.
 intros;cases H
-[cases H1
+[cases H1; unfold; autobatch;
+|autobatch;]
+(*
  [left;autobatch
  |rewrite < H3;assumption]
-|rewrite > H2;assumption]
+|rewrite > H2;assumption]*)
 qed.
 
-axiom Rlt_plus_l : ∀x,y,z:R.x < y → z + x < z + y.
-axiom Rlt_times_l : ∀x,y,z:R.x < y → R0 < z → z*x < z*y.
+axiom Rlt_plus_l : ∀z,x,y:R.x < y → z + x < z + y.
+axiom Rlt_times_l : ∀z,x,y:R.x < y → R0 < z → z*x < z*y.
 
 (* FIXME: these should be lemmata *)
-axiom Rle_plus_l : ∀x,y,z:R.x ≤ y → z + x ≤ z + y.
-axiom Rle_times_l : ∀x,y,z:R.x ≤ y → R0 < z → z*x ≤ z*y.
+axiom Rle_plus_l : ∀z,x,y:R.x ≤ y → z + x ≤ z + y.
+axiom Rle_times_l : ∀z,x,y:R.x ≤ y → R0 < z → z*x ≤ z*y.
 
-lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z.
-intros;
-rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);
-autobatch;
+lemma Rle_plus_r : ∀z,x,y:R.x ≤ y → x + z ≤ y + z.
+intros; autobatch.
 qed.
 
-lemma Rle_times_r : ∀x,y,z:R.x ≤ y → R0 < z → x*z ≤ y*z.
+lemma Rle_times_r : ∀z,x,y:R.x ≤ y → R0 < z → x*z ≤ y*z.
 intros;
-rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
+(* rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); *)
 autobatch;
 qed.
 
@@ -203,18 +204,18 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; demodulate all.
-(*
+(*intro; autobatch paramodulation.*)  
+intros;
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 rewrite < assoc_Rplus;
 apply eq_f2;autobatch paramodulation;
-*)
+
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. demodulate all. (*
-auto paramodulation.
+intro. (*autobatch paramodulation.*) 
+
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
@@ -224,7 +225,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 apply eq_f2 [reflexivity]
 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
-*)
+
 qed.
 
 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
@@ -341,11 +342,11 @@ qed.
 
 lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x.
 intros;
-lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
+lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
 [ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
   lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
-  cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:
-    demodulate all;]
+  cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:autobatch
+(* end auto($Revision: 9716 $) proof: TIME=2.24 SIZE=100 DEPTH=100 *) ;]
   rewrite < Hcut; assumption;
  (*
  rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
@@ -361,7 +362,7 @@ lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
 qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros; lapply (Rlt_plus_l ?? (-b) H); applyS Hletin;
+intros; autobatch depth=4;
 (*
 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;