From: Enrico Tassi Date: Fri, 25 May 2007 08:27:39 +0000 (+0000) Subject: auto --> autobatch X-Git-Tag: 0.4.95@7852~436 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a3ced7cc547cc4f4566c4c68c35b0de1aabf7f0;p=helm.git auto --> autobatch --- diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma index 288e0626d..44823fc81 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma @@ -102,9 +102,9 @@ theorem trans_eq : \forall A:Type. \forall x,y,z:A. x=y \to y=z \to x=z. qed. theorem plus_reg_l: \forall n,m,p. n + m = n + p \to m = p. - intros. apply plus_reg_l; auto. + intros. apply plus_reg_l; autobatch. qed. theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m. - intros. apply plus_le_reg_l; auto. + intros. apply plus_le_reg_l; autobatch. qed. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index 3a48e5987..b39e419ad 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -21,7 +21,7 @@ include "Lift/defs.ma". theorem lift_inv_sort_1: \forall l, i, h, x. Lift l i (sort h) x \to x = sort h. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem lift_inv_lref_1: \forall l, i, j1, x. @@ -54,7 +54,7 @@ qed. theorem lift_inv_sort_2: \forall l, i, x, h. Lift l i x (sort h) \to x = sort h. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem lift_inv_lref_2: \forall l, i, x, j2. diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma index 54ab40ae7..0007f3bc1 100644 --- a/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/matita/contribs/RELATIONAL/NLE/inv.ma @@ -18,11 +18,11 @@ include "NLE/defs.ma". theorem nle_inv_succ_1: \forall x,y. x < y \to \exists z. y = succ z \land x <= z. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem nle_inv_succ_zero: \forall x. x < zero \to False. @@ -30,7 +30,7 @@ theorem nle_inv_succ_zero: \forall x. x < zero \to False. qed. theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem nle_inv_succ_2: \forall y,x. x <= succ y \to diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma index 78ca2e569..d90adb926 100644 --- a/matita/contribs/RELATIONAL/NLE/nplus.ma +++ b/matita/contribs/RELATIONAL/NLE/nplus.ma @@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/nplus". include "NLE/defs.ma". theorem nle_nplus: \forall p, q, r. (p + q == r) \to q <= r. - intros. elim H; clear H q r; auto. + intros. elim H; clear H q r; autobatch. qed. axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma index ae1d47870..5299d5790 100644 --- a/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -19,7 +19,7 @@ include "NPlus/defs.ma". (* Inversion lemmas *********************************************************) theorem nplus_inv_zero_1: \forall q,r. (zero + q == r) \to q = r. - intros. elim H; clear H q r; auto. + intros. elim H; clear H q r; autobatch. qed. theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to @@ -31,7 +31,7 @@ theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to qed. theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to @@ -41,7 +41,7 @@ qed. theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to p = zero \land q = zero. - intros. inversion H; clear H; intros; subst. auto. + intros. inversion H; clear H; intros; subst. autobatch. qed. theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to @@ -55,25 +55,25 @@ qed. theorem nplus_inv_succ_2_3: \forall p,q,r. (p + (succ q) == (succ r)) \to p + q == r. intros. - lapply linear nplus_inv_succ_2 to H. decompose. subst. auto. + lapply linear nplus_inv_succ_2 to H. decompose. subst. autobatch. qed. theorem nplus_inv_succ_1_3: \forall p,q,r. ((succ p) + q == (succ r)) \to p + q == r. intros. - lapply linear nplus_inv_succ_1 to H. decompose. subst. auto. + lapply linear nplus_inv_succ_1 to H. decompose. subst. autobatch. qed. theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero. intros 2. elim q; clear q; [ lapply linear nplus_inv_zero_2 to H | lapply linear nplus_inv_succ_2_3 to H1 - ]; auto. + ]; autobatch. qed. theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero. intros 1. elim p; clear p; [ lapply linear nplus_inv_zero_1 to H | lapply linear nplus_inv_succ_1_3 to H1. - ]; auto. + ]; autobatch. qed. diff --git a/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma index 1ca191339..62b934865 100644 --- a/matita/dama/ordered_sets.ma +++ b/matita/dama/ordered_sets.ma @@ -330,7 +330,7 @@ theorem tail_inf_increasing: assumption | unfold y; simplify; - auto paramodulation library + autobatch paramodulation library ] ]. qed. diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma index 5def3ec47..165f9ce30 100644 --- a/matita/tests/fguidi.ma +++ b/matita/tests/fguidi.ma @@ -84,8 +84,8 @@ theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to intros 4. elim H; clear H x y. apply eq_gen_S_O. exact m. elim H1. auto paramodulation. clear H2. cut (n = m). -elim Hcut. apply ex_intro. exact n1. split; auto. -apply eq_gen_S_S. auto. +elim Hcut. apply ex_intro. exact n1. split; autobatch. +apply eq_gen_S_S. autobatch. qed. theorem le_gen_S_x: \forall m,x. (le (S m) x) \to