Bitwise "or" for PosNum
.
Equations
- PosNum.lor PosNum.one (PosNum.bit0 q) = PosNum.bit1 q
- PosNum.lor PosNum.one x = x
- PosNum.lor (PosNum.bit0 p) PosNum.one = PosNum.bit1 p
- PosNum.lor x PosNum.one = x
- PosNum.lor (PosNum.bit0 p) (PosNum.bit0 q) = PosNum.bit0 (PosNum.lor p q)
- PosNum.lor (PosNum.bit0 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)
- PosNum.lor (PosNum.bit1 p) (PosNum.bit0 q) = PosNum.bit1 (PosNum.lor p q)
- PosNum.lor (PosNum.bit1 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)
Instances For
Bitwise "and" for PosNum
.
Equations
- PosNum.land PosNum.one (PosNum.bit0 q) = 0
- PosNum.land PosNum.one x = 1
- PosNum.land (PosNum.bit0 p) PosNum.one = 0
- PosNum.land x PosNum.one = 1
- PosNum.land (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit1 (PosNum.land p q)
Instances For
Bitwise fun a b ↦ a && !b
for PosNum
. For example, ldiff 5 9 = 4
:
101
1001
----
100
Equations
- PosNum.ldiff PosNum.one (PosNum.bit0 a) = 1
- PosNum.ldiff PosNum.one x = 0
- PosNum.ldiff (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.ldiff (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.ldiff (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)
Instances For
Bitwise "xor" for PosNum
.
Equations
- PosNum.lxor PosNum.one PosNum.one = 0
- PosNum.lxor PosNum.one (PosNum.bit0 q) = Num.pos (PosNum.bit1 q)
- PosNum.lxor PosNum.one (PosNum.bit1 q) = Num.pos (PosNum.bit0 q)
- PosNum.lxor (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit1 p)
- PosNum.lxor (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.lxor (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit1 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.lxor p q)
Instances For
a.testBit n
is true
iff the n
-th bit (starting from the LSB) in the binary representation
of a
is active. If the size of a
is less than n
, this evaluates to false
.
Equations
- PosNum.testBit PosNum.one 0 = true
- PosNum.testBit PosNum.one x = false
- PosNum.testBit (PosNum.bit0 a) 0 = false
- PosNum.testBit (PosNum.bit0 p) (Nat.succ n) = PosNum.testBit p n
- PosNum.testBit (PosNum.bit1 a) 0 = true
- PosNum.testBit (PosNum.bit1 p) (Nat.succ n) = PosNum.testBit p n
Instances For
n.oneBits 0
is the list of indices of active bits in the binary representation of n
.
Equations
- PosNum.oneBits PosNum.one x = [x]
- PosNum.oneBits (PosNum.bit0 p) x = PosNum.oneBits p (x + 1)
- PosNum.oneBits (PosNum.bit1 p) x = x :: PosNum.oneBits p (x + 1)
Instances For
Left-shift the binary representation of a PosNum
.
Equations
- PosNum.shiftl x 0 = x
- PosNum.shiftl x (Nat.succ n) = PosNum.shiftl (PosNum.bit0 x) n
Instances For
Right-shift the binary representation of a PosNum
.
Equations
- PosNum.shiftr x 0 = Num.pos x
- PosNum.shiftr PosNum.one x = 0
- PosNum.shiftr (PosNum.bit0 p) (Nat.succ n) = PosNum.shiftr p n
- PosNum.shiftr (PosNum.bit1 p) (Nat.succ n) = PosNum.shiftr p n
Instances For
Alternative representation of integers using a sign bit at the end.
The convention on sign here is to have the argument to msb
denote
the sign of the MSB itself, with all higher bits set to the negation
of this sign. The result is interpreted in two's complement.
13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true)))) -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))
As with Num
, a special case must be added for zero, which has no msb,
but by two's complement symmetry there is a second special case for -1.
Here the Bool
field indicates the sign of the number.
0 = ..0000000(base 2) = zero false -1 = ..1111111(base 2) = zero true
Instances For
The SNum
representation uses a bit string, essentially a list of 0 (false
) and 1 (true
) bits,
and the negation of the MSB is sign-extended to all higher bits.
Sign of a NzsNum
.
Equations
- NzsNum.sign (NzsNum.msb b) = !b
- NzsNum.sign (NzsNum.bit a p) = NzsNum.sign p
Instances For
Equations
- NzsNum.not (NzsNum.msb b) = NzsNum.msb (decide ¬b = true)
- NzsNum.not (NzsNum.bit a p) = NzsNum.bit (decide ¬a = true) (NzsNum.not p)
Instances For
Add an inactive bit at the end of a NzsNum
. This mimics PosNum.bit0
.
Instances For
Add an active bit at the end of a NzsNum
. This mimics PosNum.bit1
.
Instances For
Add a bit at the end of a SNum
. This mimics NzsNum.bit
.
Instances For
A dependent induction principle for NzsNum
, with base cases
0 : SNum
and (-1) : SNum
.
Equations
- NzsNum.drec' z s (NzsNum.msb b) = Eq.mpr (_ : C (SNum.nz (NzsNum.msb b)) = C (SNum.bit b (SNum.zero (decide ¬b = true)))) (s b (SNum.zero (decide ¬b = true)) (z (decide ¬b = true)))
- NzsNum.drec' z s (NzsNum.bit a p) = s a (SNum.nz p) (NzsNum.drec' z s p)
Instances For
SNum.testBit n a
is true
iff the n
-th bit (starting from the LSB) of a
is active.
If the size of a
is less than n
, this evaluates to false
.
Equations
- SNum.testBit 0 x = SNum.head x
- SNum.testBit (Nat.succ n) x = SNum.testBit n (SNum.tail x)
Instances For
SNum.czAdd a b n
is n + a - b
(where a
and b
should be read as either 0 or 1).
This is useful to implement the carry system in cAdd
.