- Timestamp:
- Jul 17, 2012, 6:00:03 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVectorZ.ma
r1516 r2200 3 3 include "ASM/BitVector.ma". 4 4 include "ASM/Arithmetic.ma". 5 include "utilities/binary/division.ma". 5 6 6 7 let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ … … 124 125 theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n. 125 126 #n #bv normalize 126 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 /127 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/ 127 128 qed. 128 129 … … 150 151 | #t whd in ⊢ (?%?); // 151 152 ] qed. 153 154 (* TODO *) 155 axiom Z_of_unsigned_bitvector_of_Z : 156 ∀n,z. 157 Z_of_unsigned_bitvector n (bitvector_of_Z n z) = 158 modZ z (Z_two_power_nat n). 159 160 axiom bitvector_of_Z_of_unsigned_bitvector : 161 ∀n,bv. 162 bitvector_of_Z n (Z_of_unsigned_bitvector n bv) = bv.
Note: See TracChangeset
for help on using the changeset viewer.