X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2Fauto%2Fnat%2Fminimization.ma;h=61cbaf45a865caed93ffc31ae4cb0afbc84978db;hb=a180bddcd4a8f35de3d7292162ba05d0077723aa;hp=84d6b4181a8e27a68ef167f2c618e003a0192e23;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/matita/library_auto/auto/nat/minimization.ma b/helm/software/matita/library_auto/auto/nat/minimization.ma
index 84d6b4181..61cbaf45a 100644
--- a/helm/software/matita/library_auto/auto/nat/minimization.ma
+++ b/helm/software/matita/library_auto/auto/nat/minimization.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/library_auto/nat/minimization".
+set "baseuri" "cic:/matita/library_autobatch/nat/minimization".
 
 include "auto/nat/minus.ma".
 
@@ -26,7 +26,7 @@ let rec max i f \def
 
 theorem max_O_f : \forall f: nat \to bool. max O f = O.
 intro. simplify.
-elim (f O); auto.
+elim (f O); autobatch.
 (*[ simplify.
   reflexivity
 | simplify.
@@ -37,7 +37,7 @@ qed.
 theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
 (f (S n) = true \land max (S n) f = (S n)) \lor 
 (f (S n) = false \land max (S n) f = max n f).
-intros.simplify.elim (f (S n));auto.
+intros.simplify.elim (f (S n));autobatch.
 (*[ simplify.
   left.
   split;reflexivity
@@ -54,7 +54,7 @@ elim n
 [ rewrite > max_O_f.
   apply le_n
 | simplify.
-  elim (f (S n1));simplify;auto.
+  elim (f (S n1));simplify;autobatch.
   (*[ simplify.
     apply le_n
   | simplify.
@@ -73,7 +73,7 @@ elim H
   [ apply H2
   | cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor 
     (f (S n1) = false \land max (S n1) f = max n1 f))
-    [ elim Hcut;elim H3;rewrite > H5;auto
+    [ elim Hcut;elim H3;rewrite > H5;autobatch
       (*[ elim H3.
         rewrite > H5.
         apply le_S.
@@ -92,11 +92,11 @@ theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
 m\le n \to f m = true \to m \le max n f.
 intros 3.
 elim n
-[ auto.
+[ autobatch.
   (*apply (le_n_O_elim m H).
   apply le_O_n.*)
 | apply (le_n_Sm_elim m n1 H1);intro
-  [ apply (trans_le ? (max n1 f)); auto
+  [ apply (trans_le ? (max n1 f)); autobatch
     (*[ apply H
       [apply le_S_S_to_le.
         assumption
@@ -108,7 +108,7 @@ elim n
   | simplify.
     rewrite < H3.
     rewrite > H2.
-    auto
+    autobatch
     (*simplify.
     apply le_n.*)
   ]
@@ -128,7 +128,7 @@ elim n
   elim H1.
   generalize in match H3.
   apply (le_n_O_elim a H2).
-  auto
+  autobatch
   (*intro.
   simplify.
   rewrite > H4.
@@ -140,7 +140,7 @@ elim n
   [ true \Rightarrow (S n1)
   | false  \Rightarrow (max n1 f)])) = true))
   
-  [ auto
+  [ autobatch
     (*simplify.
     intro.
     assumption.*)
@@ -153,22 +153,22 @@ elim n
     apply (le_n_Sm_elim a n1 H4)
     [ intros.
       apply (ex_intro nat ? a).
-      auto
+      autobatch
       (*split
       [ apply le_S_S_to_le.
         assumption.
       | assumption.
       ]*)
     | intros.
-      (* una chiamata di auto in questo punto genera segmentation fault*)
+      (* una chiamata di autobatch in questo punto genera segmentation fault*)
       apply False_ind.
-      (* una chiamata di auto in questo punto genera segmentation fault*)
+      (* una chiamata di autobatch in questo punto genera segmentation fault*)
       apply not_eq_true_false.
-      (* una chiamata di auto in questo punto genera segmentation fault*)
+      (* una chiamata di autobatch in questo punto genera segmentation fault*)
       rewrite < H2.
-      (* una chiamata di auto in questo punto genera segmentation fault*)
+      (* una chiamata di autobatch in questo punto genera segmentation fault*)
       rewrite < H7.
-      (* una chiamata di auto in questo punto genera segmentation fault*)
+      (* una chiamata di autobatch in questo punto genera segmentation fault*)
       rewrite > H6. 
       reflexivity.
     ]
@@ -181,7 +181,7 @@ theorem lt_max_to_false : \forall f:nat \to bool.
 \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
 intros 2.
 elim n
-[ absurd (le m O);auto
+[ absurd (le m O);autobatch
   (*[ assumption
   | cut (O < m)
     [ apply (lt_O_n_elim m Hcut).
@@ -202,14 +202,14 @@ elim n
   | elim H3.
     apply (le_n_Sm_elim m n1 H2)
     [ intro.
-      apply H;auto
+      apply H;autobatch
       (*[ rewrite < H6.
         assumption
       | apply le_S_S_to_le.
         assumption
       ]*)
     | intro.
-      auto
+      autobatch
       (*rewrite > H7.
       assumption*)
     ]
@@ -230,14 +230,14 @@ definition min : nat \to (nat \to bool) \to nat \def
 theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
 min_aux O i f = i.
 intros.simplify.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
   in loop): dopo circa 3 minuti non era ancora terminata.
  *)
 rewrite < minus_n_O.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
   in loop): dopo circa 3 minuti non era ancora terminata.
  *)
-elim (f i); auto.
+elim (f i); autobatch.
 (*[ reflexivity.
   simplify
 | reflexivity
@@ -247,14 +247,14 @@ qed.
 theorem min_O_f : \forall f:nat \to bool.
 min O f = O.
 intro.
-(* una chiamata di auto a questo punto NON conclude la dimostrazione*)
+(* una chiamata di autobatch a questo punto NON conclude la dimostrazione*)
 apply (min_aux_O_f f O).
 qed.
 
 theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
 (f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor 
 (f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
-intros.simplify.elim (f (n - (S i)));auto.
+intros.simplify.elim (f (n - (S i)));autobatch.
 (*[ simplify.
   left.
   split;reflexivity.
@@ -273,7 +273,7 @@ elim off
   elim H1.
   elim H2.
   cut (a = m)
-  [ auto.
+  [ autobatch.
     (*rewrite > (min_aux_O_f f).
     rewrite < Hcut.
     assumption*)
@@ -288,7 +288,7 @@ elim off
   (f (m-(S n)) = b) \to (f (match b in bool with
   [ true \Rightarrow m-(S n)
   | false  \Rightarrow (min_aux n m f)])) = true))
-  [ auto
+  [ autobatch
     (*simplify.
     intro.
     assumption.*)
@@ -300,8 +300,8 @@ elim off
     elim H4.
     elim (le_to_or_lt_eq (m-(S n)) a H6)
     [ apply (ex_intro nat ? a).
-      split;auto
-      (*[ auto.split
+      split;autobatch
+      (*[ autobatch.split
         [ apply lt_minus_S_n_to_le_minus_n.
           assumption
         | assumption
@@ -309,7 +309,7 @@ elim off
       | assumption
       ]*)
     | absurd (f a = false)
-      [ (* una chiamata di auto in questo punto genera segmentation fault*)
+      [ (* una chiamata di autobatch in questo punto genera segmentation fault*)
         rewrite < H8.
         assumption.
       | rewrite > H5.
@@ -344,7 +344,7 @@ elim off
   | elim H3.
     elim (le_to_or_lt_eq (n -(S n1)) m)
     [ apply H
-      [ auto
+      [ autobatch
         (*apply lt_minus_S_n_to_le_minus_n.
         assumption*)
       | rewrite < H6.
@@ -363,17 +363,17 @@ theorem le_min_aux : \forall f:nat \to bool.
 intros 3.
 elim off
 [ rewrite < minus_n_O.
-  auto
+  autobatch
   (*rewrite > (min_aux_O_f f n).
   apply le_n.*)
 | elim (min_aux_S f n1 n)
   [ elim H1.
-    auto
+    autobatch
     (*rewrite > H3.
     apply le_n.*)
   | elim H1.
     rewrite > H3.
-    auto
+    autobatch
     (*apply (trans_le (n-(S n1)) (n-n1))
     [ apply monotonic_le_minus_r.
       apply le_n_Sn.
@@ -389,14 +389,14 @@ intros.
 elim off
 [ simplify.
   rewrite < minus_n_O.
-  elim (f n);auto
+  elim (f n);autobatch
   (*[simplify.
     apply le_n.
   | simplify.
     apply le_n.
   ]*)
 | simplify.
-  elim (f (n -(S n1)));simplify;auto
+  elim (f (n -(S n1)));simplify;autobatch
   (*[ apply le_plus_to_minus.
     rewrite < sym_plus.
     apply le_plus_n