X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=50b7d1221bfdca8211184a664add8c73aa392bd5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=74fd74e7455de4b999461b2944efcd952fe96ad1;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 74fd74e74..50b7d1221 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -27,7 +27,7 @@ interpretation "not divides" 'ndivides n m =
  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
 
 theorem reflexive_divides : reflexive nat divides.
-simplify.
+unfold reflexive.
 intros.
 exact (witness x x (S O) (times_n_SO x)).
 qed.
@@ -150,6 +150,23 @@ assumption.
 apply (decidable_le n m).
 qed.
 
+theorem antisymmetric_divides: antisymmetric nat divides.
+unfold antisymmetric.intros.elim H. elim H1.
+apply (nat_case1 n2).intro.
+rewrite > H3.rewrite > H2.rewrite > H4.
+rewrite < times_n_O.reflexivity.
+intros.
+apply (nat_case1 n).intro.
+rewrite > H2.rewrite > H3.rewrite > H5.
+rewrite < times_n_O.reflexivity.
+intros.
+apply antisymmetric_le.
+rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
+rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
+qed.
+
 (* divides le *)
 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 intros. elim H1.rewrite > H2.cut (O < n2).
@@ -189,7 +206,7 @@ match eqb (m \mod n) O with
 | false \Rightarrow n \ndivides m].
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.
-intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 qed.
 
 theorem divides_b_true_to_divides :
@@ -322,11 +339,11 @@ definition prime : nat \to  Prop \def
 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 
 theorem not_prime_O: \lnot (prime O).
-simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
 qed.
 
 theorem not_prime_SO: \lnot (prime (S O)).
-simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 qed.
 
 (* smallest factor *)
@@ -373,10 +390,10 @@ theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 intro.
 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
 intro.apply (nat_case m).intro.
-simplify.apply le_n.
+simplify.unfold lt.apply le_n.
 intros.apply (trans_lt ? (S O)).
-simplify. apply le_n.
-apply lt_SO_smallest_factor.simplify. apply le_S_S.
+unfold lt.apply le_n.
+apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
 apply le_S_S.apply le_O_n.
 qed.
 
@@ -397,7 +414,7 @@ apply (ex_intro nat ? (S(S m1))).
 split.split.
 apply le_minus_m.apply le_n.
 rewrite > mod_n_n.reflexivity.
-apply (trans_lt ? (S O)).apply (le_n (S O)).simplify.
+apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
 apply le_S_S.apply le_S_S.apply le_O_n.
 qed.
   
@@ -406,9 +423,9 @@ theorem le_smallest_factor_n :
 intro.apply (nat_case n).simplify.reflexivity.
 intro.apply (nat_case m).simplify.reflexivity.
 intro.apply divides_to_le.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
@@ -442,7 +459,7 @@ absurd (m \divides n).
 apply (transitive_divides m (smallest_factor n)).
 assumption.
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. exact H.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
 apply lt_smallest_factor_to_not_divides.
 exact H.assumption.assumption.assumption.
 apply divides_to_le.
@@ -464,7 +481,7 @@ change with
 smallest_factor (S(S m1)) = (S(S m1))).
 intro.elim H.apply H2.
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)).simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
 apply lt_SO_smallest_factor.
 assumption.
 qed.
@@ -500,8 +517,8 @@ match primeb n with
 [ true \Rightarrow prime n
 | false \Rightarrow \lnot (prime n)].
 intro.
-apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
-intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
+intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 intro.
 change with 
 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
@@ -511,7 +528,7 @@ apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
 intro.change with (prime (S(S m1))).
 rewrite < H.
 apply prime_smallest_factor_n.
-simplify.apply le_S_S.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
 intro.change with (\lnot (prime (S(S m1)))).
 change with (prime (S(S m1)) \to False).
 intro.apply H.