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, 0 insertions, 69 deletions

diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
deleted file mode 100644
index d1f4aac265..0000000000
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ /dev/null
@@ -1,69 +0,0 @@
-Require Export NAxioms.
-
-Module StrongRecProperties (Import NBaseMod : NBaseSig).
-Module Export NBasePropMod := NBasePropFunct NBaseMod.
-Open Local Scope NatScope.
-
-Section StrongRecursion.
-
-Variable A : Set.
-Variable EA : relation A.
-
-Hypothesis EA_equiv : equiv A EA.
-
-Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A :=
-(recursion (fun _ : N => a)
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
-           (S x)) x.
-
-Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A,
-fun2_wd E (eq_fun E EA) EA f ->
-  fun2_wd E (eq_fun E EA) (eq_fun E EA)
-    (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)).
-Proof.
-unfold fun2_wd; intros f f_wd.
-intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'.
-assert (H : e y x = e y' x'). now apply e_wd. rewrite H.
-destruct (e y' x'); simpl.
-now apply f_wd. now apply Egg'.
-Qed.
-
-Theorem strong_rec_wd :
-forall a a', EA a a' ->
-  forall f f', eq_fun2 E (eq_fun E EA) EA f f' ->
-    forall x x', x == x' ->
-      EA (strong_rec a f x) (strong_rec a' f' x').
-Proof.
-intros a a' Eaa' f f' Eff' x x' Exx'.
-assert (H : eq_fun E EA
-  (recursion (fun _ : N => a)
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
-           (S x))
-  (recursion (fun _ : N => a')
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y))
-           (S x'))).
-apply recursion_wd with (EA := eq_fun E EA).
-unfold eq_fun; now intros.
-unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'.
-assert (H: e z y = e z' y'); [now apply e_wd|].
-rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp'].
-now rewrite Exx'.
-unfold strong_rec.
-now apply H.
-Qed.
-
-(* To do:
-Definition step_good (g : N -> (N -> A) -> A) :=
-  forall (x : N) (h1 h2 : N -> A),
-    (forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2).
-
-Theorem strong_recursion_fixpoint : forall a g, step_good g ->
-  let f x := (strong_rec a g x) in forall x, EA (f x) (g x f).
-*)
-
-End StrongRecursion.
-
-Implicit Arguments strong_rec [A].
-
-End StrongRecProperties.
-