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, 16 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index dc2d27fa4..021ac29ee 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -56,10 +56,16 @@ Module Type NType.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
  Parameter gcd : t -> t -> t.
- Parameter shiftr : t -> t -> t.
- Parameter shiftl : t -> t -> t.
  Parameter even : t -> bool.
  Parameter odd : t -> bool.
+ Parameter testbit : t -> t -> bool.
+ Parameter shiftr : t -> t -> t.
+ Parameter shiftl : t -> t -> t.
+ Parameter land : t -> t -> t.
+ Parameter lor : t -> t -> t.
+ Parameter ldiff : t -> t -> t.
+ Parameter lxor : t -> t -> t.
+ Parameter div2 : t -> t.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -84,10 +90,16 @@ Module Type NType.
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p].
- Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p].
  Parameter spec_even: forall x, even x = Zeven_bool [x].
  Parameter spec_odd: forall x, odd x = Zodd_bool [x].
+ Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
 
 End NType.