X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2Fauto%2Fnat%2Fminus.ma;h=8a3d893f172d163e6cf7e9853603d06d36d8e11d;hb=d4302f43737034a69bd475e5f46e8d126229375e;hp=e7b01f9da74d4935ded46ccb73d5e633f34ab83c;hpb=797f9ece92237a8d583a0c32ef4fa755299f9949;p=helm.git

diff --git a/helm/software/matita/library_auto/auto/nat/minus.ma b/helm/software/matita/library_auto/auto/nat/minus.ma
index e7b01f9da..8a3d893f1 100644
--- a/helm/software/matita/library_auto/auto/nat/minus.ma
+++ b/helm/software/matita/library_auto/auto/nat/minus.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/library_auto/nat/minus".
+set "baseuri" "cic:/matita/library_autobatch/nat/minus".
 
 include "auto/nat/le_arith.ma".
 include "auto/nat/compare.ma".
@@ -27,12 +27,12 @@ let rec minus n m \def
         | (S q) \Rightarrow minus p q ]].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/library_auto/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
 
 theorem minus_n_O: \forall n:nat.n=n-O.
 intros.
 elim n;
-auto. (* applico auto su entrambi i goal aperti*)
+autobatch. (* applico autobatch su entrambi i goal aperti*)
 (*simplify;reflexivity.*)
 qed.
 
@@ -47,7 +47,7 @@ qed.
 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
 intro.
 elim n
-[ auto
+[ autobatch
   (*simplify.reflexivity.*)
 | elim H.
   reflexivity
@@ -60,15 +60,15 @@ intros 2.
 apply (nat_elim2
 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)));intros
 [ apply (le_n_O_elim n1 H).
-  auto
+  autobatch
   (*simplify.
   reflexivity.*)
-| auto
+| autobatch
   (*simplify.
   reflexivity.*)
 | rewrite < H
   [ reflexivity
-  | auto
+  | autobatch
     (*apply le_S_S_to_le. 
     assumption.*)
   ]
@@ -81,15 +81,15 @@ intros 2.
 apply (nat_elim2
 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m));intros
 [ apply (le_n_O_elim ? H).
-  auto
+  autobatch
   (*simplify.
   rewrite < minus_n_O.
   reflexivity.*)
-| auto
+| autobatch
   (*simplify.
   reflexivity.*)
 | simplify.
-  auto
+  autobatch
   (*apply H.
   apply le_S_S_to_le.
   assumption.*)
@@ -103,7 +103,7 @@ elim m
 [ rewrite < minus_n_O.
   apply plus_n_O.
 | elim n2
-  [ auto
+  [ autobatch
     (*simplify.
     apply minus_n_n.*)
   | rewrite < plus_n_Sm.
@@ -119,7 +119,7 @@ intros 2.
 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
 [ apply (le_n_O_elim n1 H).
   reflexivity
-| auto
+| autobatch
   (*simplify.
   rewrite < plus_n_O.
   reflexivity.*)
@@ -128,7 +128,7 @@ apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
   simplify.
   apply eq_f.
   rewrite < sym_plus.
-  auto
+  autobatch
   (*apply H.
   apply le_S_S_to_le.
   assumption.*)
@@ -137,7 +137,7 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
-intros.apply (trans_eq ? ? ((n-m)+m));auto.
+intros.apply (trans_eq ? ? ((n-m)+m));autobatch.
 (*[ apply plus_minus_m_m.
   apply H.
 | elim H1.
@@ -152,7 +152,7 @@ apply (inj_plus_r m).
 rewrite < H.
 rewrite < sym_plus.
 symmetry.
-auto.
+autobatch.
 (*apply plus_minus_m_m.
 rewrite > H.
 rewrite > sym_plus.
@@ -172,7 +172,7 @@ apply (lt_O_n_elim n H).
 intro.
 apply (lt_O_n_elim m H1).
 intro.
-auto.
+autobatch.
 (*simplify.reflexivity.*)
 qed.
 
@@ -180,11 +180,11 @@ theorem eq_minus_n_m_O: \forall n,m:nat.
 n \leq m \to n-m = O.
 intros 2.
 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
-[ auto
+[ autobatch
   (*simplify.
   reflexivity.*)
 | apply False_ind.
-  auto
+  autobatch
   (*apply not_le_Sn_O.
   goal 15.*) (*prima goal 13*) 
 (* effettuando un'esecuzione passo-passo, quando si arriva a dover 
@@ -198,7 +198,7 @@ apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
  *)
   (*apply H.*)
 | simplify.
-  auto
+  autobatch
   (*apply H.
   apply le_S_S_to_le. 
   apply H1.*)
@@ -209,7 +209,7 @@ theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 intros.
 elim H
 [ elim (minus_Sn_n n).apply le_n
-| rewrite > minus_Sn_m;auto
+| rewrite > minus_Sn_m;autobatch
   (*apply le_S.assumption.
   apply lt_to_le.assumption.*)
 ]
@@ -222,7 +222,7 @@ intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))));intros
   | rewrite < minus_n_O.
     apply le_n.
   ]
-| auto 
+| autobatch 
   (*simplify.apply le_n_Sn.*)
 | simplify.apply H.
 ]
@@ -230,7 +230,7 @@ qed.
 
 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. 
 intros 3.
-auto.
+autobatch.
 (*simplify.
 intro.
 apply (trans_le (m-n) (S (m-(S n))) p).
@@ -240,14 +240,14 @@ qed.
 
 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n));intros
-[ auto
+[ autobatch
   (*rewrite < minus_n_O.
   apply le_n.*)
-| auto
+| autobatch
   (*simplify.
   apply le_n.*)
 | simplify.
-  auto
+  autobatch
   (*apply le_S.
   assumption.*)
 ]
@@ -260,7 +260,7 @@ intro.
 apply (lt_O_n_elim m H1).
 intro.
 simplify.
-auto.
+autobatch.
 (*unfold lt.
 apply le_S_S.
 apply le_minus_m.*)
@@ -276,7 +276,7 @@ apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m))
   assumption
 | simplify.
   intros.
-  auto
+  autobatch
   (*apply le_S_S.
   apply H.
   assumption.*)
@@ -295,11 +295,11 @@ apply (nat_elim2
 | rewrite < minus_n_O.
   apply le_minus_m.
 | elim a
-  [ auto
+  [ autobatch
     (*simplify.
     apply le_n.*)
   | simplify.
-    auto
+    autobatch
     (*apply H.
     apply le_S_S_to_le.
     assumption.*)
@@ -324,12 +324,12 @@ theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
 intros 2.
 apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)))
 [ intros.
-  auto
+  autobatch
   (*simplify.
   apply le_O_n.*)
 | intros 2.
   rewrite < plus_n_O.
-  auto
+  autobatch
   (*intro.
   simplify.
   assumption.*)
@@ -348,17 +348,17 @@ intros 3.
 apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))));intro
 [ rewrite < plus_n_O.
   rewrite < minus_n_O.
-  auto
+  autobatch
   (*intro.
   assumption.*)
 | intro.
   cut (n=O)
-  [ auto
+  [ autobatch
     (*rewrite > Hcut.
     apply le_O_n.*)
   | apply sym_eq. 
     apply le_n_O_to_eq.
-    auto
+    autobatch
     (*apply (trans_le ? (n+(S n1)))
     [ rewrite < sym_plus.
       apply le_plus_n
@@ -381,7 +381,7 @@ apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)))
 [ intro.
   rewrite < plus_n_O.
   rewrite < minus_n_O.
-  auto
+  autobatch
   (*intro.
   assumption.*)
 | simplify.
@@ -393,7 +393,7 @@ apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)))
   unfold lt.
   apply le_S_S.
   rewrite < plus_n_Sm.
-  auto
+  autobatch
   (*apply H.
   apply H1.*)
 ]
@@ -404,15 +404,15 @@ unfold distributive.
 intros.
 apply ((leb_elim z y));intro
 [ cut (x*(y-z)+x*z = (x*y-x*z)+x*z)
-    [ auto
+    [ autobatch
       (*apply (inj_plus_l (x*z)).
       assumption.*)
     | apply (trans_eq nat ? (x*y))
       [ rewrite < distr_times_plus.
-        auto
+        autobatch
         (*rewrite < (plus_minus_m_m ? ? H).
         reflexivity.*)
-      | rewrite < plus_minus_m_m;auto
+      | rewrite < plus_minus_m_m;autobatch
         (*[ reflexivity.
         | apply le_times_r.
           assumption.
@@ -421,17 +421,17 @@ apply ((leb_elim z y));intro
     ]
 | rewrite > eq_minus_n_m_O
   [ rewrite > (eq_minus_n_m_O (x*y))
-    [ auto
+    [ autobatch
       (*rewrite < sym_times.
       simplify.
       reflexivity.*)
     | apply le_times_r.
       apply lt_to_le.
-      auto
+      autobatch
       (*apply not_le_to_lt.
       assumption.*)
     ]
-  | auto
+  | autobatch
     (*apply lt_to_le.
     apply not_le_to_lt.
     assumption.*)
@@ -447,7 +447,7 @@ intros.
 apply plus_to_minus.
 rewrite > sym_plus in \vdash (? ? ? %).
 rewrite > assoc_plus.
-auto.
+autobatch.
 (*rewrite < plus_minus_m_m.
 reflexivity.
 assumption.
@@ -464,7 +464,7 @@ cut (m+p \le n \or m+p \nleq n)
     rewrite > (sym_plus p).
     rewrite < plus_minus_m_m
     [ rewrite > sym_plus.
-      rewrite < plus_minus_m_m ; auto
+      rewrite < plus_minus_m_m ; autobatch
       (*[ reflexivity.
       | apply (trans_le ? (m+p))
         [ rewrite < sym_plus.
@@ -482,11 +482,11 @@ cut (m+p \le n \or m+p \nleq n)
       | apply le_plus_to_minus.
         apply lt_to_le.
         rewrite < sym_plus.
-        auto
+        autobatch
         (*apply not_le_to_lt. 
         assumption.*)
       ]
-    | auto
+    | autobatch
       (*apply lt_to_le.
       apply not_le_to_lt.
       assumption.*)          
@@ -504,7 +504,7 @@ apply plus_to_minus.
 rewrite < assoc_plus.
 rewrite < plus_minus_m_m;
 [ rewrite < sym_plus.
-  auto
+  autobatch
   (*rewrite < plus_minus_m_m
   [ reflexivity
   | assumption