Changeset 2672 for src/ASM


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

One less axiom on bitvectors.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2664 r2672  
    166166  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
    167167qed. 
    168 
    169 lemma nat_of_bitvector_lt_bound:
    170   ∀n: nat.
    171   ∀b: BitVector n.
    172     nat_of_bitvector n b < 2^n.
    173   #n #b cases daemon
    174 qed.
    175168
    176169lemma sublist_tal_pc_list_all_program_counter_list:
  • 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.