Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 8 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 7ace860f38..3146b9c2c3 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -3,13 +3,13 @@ Require Export NumPrelude.
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
-Parameter Inline E : Z -> Z -> Prop.
+Parameter Inline Zeq : Z -> Z -> Prop.
 Parameter Inline e : Z -> Z -> bool.
 
-Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
-Axiom E_equiv : equiv Z E.
+Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom E_equiv : equiv Z Zeq.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 E_equiv)
  symmetry proved by (proj2 (proj2 E_equiv))
  transitivity proved by (proj1 (proj2 E_equiv))
@@ -17,15 +17,15 @@ as E_rel.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
-Notation "x == y" := (E x y) (at level 70) : IntScope.
-Notation "x # y" := (~ E x y) (at level 70) : IntScope.
+Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
+Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
 
 End ZDomainSignature.
 
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
+Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
 Proof.
 intros x x' Exx' y y' Eyy'.
 case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
@@ -49,7 +49,7 @@ Qed.
 
 Declare Left Step ZE_stepl.
 
-(* The right step lemma is just transitivity of E *)
+(* The right step lemma is just transitivity of Zeq *)
 Declare Right Step (proj1 (proj2 E_equiv)).
 
 End ZDomainProperties.