- character: we adjusted some "autobatch" parameters

[helm.git] / helm / software / matita / contribs / character / preamble.ma

diff --git a/helm/software/matita/contribs/character/preamble.ma b/helm/software/matita/contribs/character/preamble.ma
index ac3f19c6eecbc6bf9778db48491e6ca33f353c8a..34ac9671e9595811e3f253081701ac5a384aba95 100644 (file)
--- a/helm/software/matita/contribs/character/preamble.ma
+++ b/helm/software/matita/contribs/character/preamble.ma
@@ -17,55 +17,53 @@ include "nat/relevant_equations.ma".
 
 alias num (instance 0) = "natural number".
 
-theorem plus_inv_O3: \forall m,n. 0 = n + m \to 0 = n \land 0 = m.
+theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
  intros 2; elim n names 0; clear n; simplify; intros;
  [ autobatch | destruct ].
 qed. 
 
-theorem times_inv_O3_S: \forall x,y. 0 = x * (S y) -> x = 0.
- intros; rewrite < times_n_Sm in H; 
+theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
+ intros; rewrite < times_n_Sm in H;
  lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
 qed. 
 
-theorem not_3_divides_1: \forall n. 1 = n * 3 \to False.
+theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
  intros 1; rewrite > sym_times; simplify;
  elim n names 0; simplify; intros; destruct;
  rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
 qed.
 
-theorem le_inv_S_S: \forall m,n. S m <= S n \to m <= n.
+theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n.
  intros; inversion H; clear H; intros; destruct; autobatch.
 qed.
 
-theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x.
+theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
  simplify; intros; destruct;
- rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3.
+ rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch.
 qed.
 
-theorem times_inv_S_m_SS: \forall k,n,m. S n = m * (S (S k)) \to m \le n.
+theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
  intros 3; elim m names 0; clear m; simplify; intros; destruct;
  clear H; apply le_S_S; rewrite < sym_times; simplify;
  autobatch depth = 2.
 qed.
 
-theorem plus_3_S3n: \forall n. S (S n * 3) = 3 + S (n * 3).
- intros; simplify; autobatch.
+theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
+ intros; simplify; autobatch depth = 1.
 qed. 
 
-theorem times_exp_x_y_Sz: \forall x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
+theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
  intros; simplify; autobatch depth = 1.
 qed.  
 
-definition acc_nat \def \lambda P:nat \to Prop. \lambda n. 
-                   \forall m. m <= n \to P m.
+definition acc_nat: (nat → Prop) → nat →Prop ≝
+   λP:nat→Prop. λn. ∀m. m ≤ n → P m.
 
-theorem wf_le: \forall P. 
-               P 0 \to (\forall n. acc_nat P n \to P (S n)) \to
-               \forall n. acc_nat P n.
+theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
  unfold acc_nat; intros 4; elim n names 0; clear n;
  [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
  | intros 3; elim m; clear m; intros; clear H3;
-   [ clear H H1; autobatch
+   [ clear H H1; autobatch depth = 2
    | clear H; lapply linear le_inv_S_S to H4;
      apply H1; clear H1; intros;
      apply H2; clear H2; autobatch depth = 2
@@ -73,10 +71,8 @@ theorem wf_le: \forall P.
  ].
 qed.
 
-theorem wf_nat_ind: \forall P:nat \to Prop.
-                    P O \to
-                    (\forall n. (\forall m. m <= n \to P m) \to P (S n)) \to
-                    \forall n. P n.
+theorem wf_nat_ind: 
+   ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
  intros; lapply linear depth=2 wf_le to H, H1 as H0; 
- unfold acc_nat in H0; apply (H0 n n); autobatch.
+ unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1.
 qed.