Changeset 2672 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Feb 16, 2013, 6:49:13 PM (8 years ago)
Author:
sacerdot
Message:

One less axiom on bitvectors.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2311 r2672  
    161161definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
    162162  λn,v. nat_of_bitvector_aux n O v.
     163
     164lemma nat_of_bitvector_aux_lt_bound:
     165 ∀n.∀v:BitVector n. ∀m,l:nat.
     166  m < 2^l → nat_of_bitvector_aux n m v < 2^(n+l).
     167 #n #v elim v normalize // -n
     168 #n #hd #tl #IH #m #l #B cases hd normalize nodelta
     169 @(transitive_le … (IH ? (S l) …))
     170 [2,4: /2 by le_exp/
     171 |1,3: @(transitive_le … (2 * (S m)))
     172  [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/
     173  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
     174qed. 
     175
     176lemma nat_of_bitvector_lt_bound:
     177 ∀n: nat. ∀b: BitVector n. nat_of_bitvector n b < 2^n.
     178 #n #b lapply (nat_of_bitvector_aux_lt_bound n b 0 0 ?) // <plus_n_O //
     179qed.
    163180
    164181lemma bitvector_of_nat_ok:
Note: See TracChangeset for help on using the changeset viewer.