summaryrefslogtreecommitdiff
path: root/theories/Logic/Classical_Pred_Set.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/Logic/Classical_Pred_Set.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/Logic/Classical_Pred_Set.v')
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Pred_Set.v47
1 files changed, 12 insertions, 35 deletions
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index c8f87fe8..2a5f03ec 100755..100644
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -6,11 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Classical_Pred_Set.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+(*i $Id: Classical_Pred_Set.v 8642 2006-03-17 10:09:02Z notin $ i*)
+
+(** This file is obsolete, use Classical_Pred_Type.v via Classical.v
+instead *)
(** Classical Predicate Logic on Set*)
-Require Import Classical_Prop.
+Require Import Classical_Pred_Type.
Section Generic.
Variable U : Set.
@@ -19,52 +22,26 @@ Variable U : Set.
Lemma not_all_ex_not :
forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.
-Proof.
-unfold not in |- *; intros P notall.
-apply NNPP; unfold not in |- *.
-intro abs.
-cut (forall n:U, P n); auto.
-intro n; apply NNPP.
-unfold not in |- *; intros.
-apply abs; exists n; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_all_ex_not U).
Lemma not_all_not_ex :
forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n.
-Proof.
-intros P H.
-elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
-apply NNPP; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_all_not_ex U).
Lemma not_ex_all_not :
forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof.
-unfold not in |- *; intros P notex n abs.
-apply notex.
-exists n; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_ex_all_not U).
Lemma not_ex_not_all :
forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
-Proof.
-intros P H n.
-apply NNPP.
-red in |- *; intro K; apply H; exists n; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_ex_not_all U).
Lemma ex_not_not_all :
forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof.
-unfold not in |- *; intros P exnot allP.
-elim exnot; auto.
-Qed.
+Proof (Classical_Pred_Type.ex_not_not_all U).
Lemma all_not_not_ex :
forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
-Proof.
-unfold not in |- *; intros P allnot exP; elim exP; intros n p.
-apply allnot with n; auto.
-Qed.
+Proof (Classical_Pred_Type.all_not_not_ex U).
-End Generic. \ No newline at end of file
+End Generic.