Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

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

1 files changed, 23 insertions, 1 deletions

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 5f38d57b87..eab33051d4 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,7 +10,7 @@
 
 
 Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec
- Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def Zdiv_def.
+ Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def Zdiv_def Zdigits_def.
 
 Local Open Scope Z_scope.
 
@@ -191,6 +191,28 @@ Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b.
 Definition quot := Zquot.
 Definition rem := Zrem.
 
+(** Bitwise operations *)
+
+Definition testbit_spec := Ztestbit_spec.
+Definition testbit_neg_r := Ztestbit_neg_r.
+Definition shiftr_spec := Zshiftr_spec.
+Definition shiftl_spec_low := Zshiftl_spec_low.
+Definition shiftl_spec_high := Zshiftl_spec_high.
+Definition land_spec := Zand_spec.
+Definition lor_spec := Zor_spec.
+Definition ldiff_spec := Zdiff_spec.
+Definition lxor_spec := Zxor_spec.
+Definition div2_spec := Zdiv2'_spec.
+
+Definition testbit := Ztestbit.
+Definition shiftl := Zshiftl.
+Definition shiftr := Zshiftr.
+Definition land := Zand.
+Definition lor := Zor.
+Definition ldiff := Zdiff.
+Definition lxor := Zxor.
+Definition div2 := Zdiv2'.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).