Changeset 2200

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

Unmodified
Removed
• src/ASM/BitVectorZ.ma

 r1516 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 ≝ 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. | #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.
• src/joint/linearise.ma

 r2182 include "joint/TranslateUtils_paolo.ma". include "utilities/hide.ma". definition graph_to_lin_statement : #p#globals * [//] * // qed. definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf. definition hide_Prop : Prop → Prop ≝ λP.P. interpretation "hide proof" 'hide p = (hide_prf ? p). interpretation "hide Prop" 'hide p = (hide_Prop p). (* discard all elements passing test, return first element failing it *)