Changeset 2149 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jul 3, 2012, 4:19:38 AM (8 years ago)
Author:
sacerdot
Message:

Code shuffling to proper places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2124 r2149  
    179179 ]
    180180qed.
     181
     182axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
    181183
    182184axiom nat_of_bitvector_bitvector_of_nat_inverse:
     
    719721qed.
    720722
     723axiom le_to_le_nat_of_bitvector_add:
     724  ∀n,v,m1,m2.
     725    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
     726      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
     727      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     728
     729lemma lt_to_lt_nat_of_bitvector_add:
     730  ∀n,v,m1,m2.
     731    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
     732      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
     733      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     734#n #v #m1 #m2 #m2_ok #bounded #H
     735lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
     736#K @(transitive_le … (K H))
     737cases daemon (*CSC: TRUE, complete*)
     738qed.
     739
    721740definition sign_bit : ∀n. BitVector n → bool ≝
    722741λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
Note: See TracChangeset for help on using the changeset viewer.