Changeset 2200 for src/ASM/BitVectorZ.ma


Ignore:
Timestamp:
Jul 17, 2012, 6:00:03 PM (7 years ago)
Author:
tranquil
Message:
  • updated joint semantics: generation of linear and graph semantics
  • opened two axioms in BitVectorZ
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorZ.ma

    r1516 r2200  
    33include "ASM/BitVector.ma".
    44include "ASM/Arithmetic.ma".
     5include "utilities/binary/division.ma".
    56
    67let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
     
    124125theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n.
    125126#n #bv normalize
    126 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
     127lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/
    127128qed.
    128129
     
    150151| #t whd in ⊢ (?%?); //
    151152] qed.
     153
     154(* TODO *)
     155axiom 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
     160axiom 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.