From d0ca084ce6e466c68e3c6288cd7da67411154d6e Mon Sep 17 00:00:00 2001 From: emakarov Date: Tue, 25 Sep 2007 13:13:41 +0000 Subject: An update on theories/Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10142 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Abstract/NAxioms.v | 39 +++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 theories/Numbers/Natural/Abstract/NAxioms.v (limited to 'theories/Numbers/Natural/Abstract/NAxioms.v') diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v new file mode 100644 index 000000000..a30c81682 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -0,0 +1,39 @@ +Require Export NumPrelude. +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type NAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. +Open Local Scope NatIntScope. + +Notation N := NZ (only parsing). +Notation E := NZE (only parsing). + +Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A. +Implicit Arguments recursion [A]. + +Axiom pred_0 : P 0 == 0. + +Axiom recursion_wd : forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x == x' -> + EA (recursion a f x) (recursion a' f' x'). + +Axiom recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. + +Axiom recursion_succ : + forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). + +End NAxiomsSig. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) -- cgit v1.2.3