Changeset 2200 for src/ASM

Timestamp:

Jul 17, 2012, 6:00:03 PM (8 years ago)

Author:

tranquil

Message:

• updated joint semantics: generation of linear and graph semantics
• opened two axioms in BitVectorZ

File:

• src/ASM/BitVectorZ.ma (modified) (3 diffs)

src/ASM/BitVectorZ.ma

@@ -3 +3 @@
 include "ASM/BitVector.ma".
 include "ASM/Arithmetic.ma".
+include "utilities/binary/division.ma".
 
 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.
 #n #bv normalize
-lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
+lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/
 qed.
 
@@ -150 +151 @@
 | #t whd in ⊢ (?%?); //
 ] qed.
+
+(* TODO *)
+axiom Z_of_unsigned_bitvector_of_Z : 
+  ∀n,z.
+  Z_of_unsigned_bitvector n (bitvector_of_Z n z) =
+  modZ z (Z_two_power_nat n).
+
+axiom bitvector_of_Z_of_unsigned_bitvector : 
+  ∀n,bv.
+  bitvector_of_Z n (Z_of_unsigned_bitvector n bv) = bv.