Changeset 2672 for src

Timestamp:

Feb 16, 2013, 6:49:13 PM (7 years ago)

Author:

sacerdot

Message:

One less axiom on bitvectors.

Location:

src/ASM

Files:

• ASMCosts.ma (modified) (1 diff)
• Arithmetic.ma (modified) (1 diff)

src/ASM/ASMCosts.ma

@@ -166 +166 @@
   @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
 qed.  
-
-lemma nat_of_bitvector_lt_bound:
-  ∀n: nat.
-  ∀b: BitVector n.
-    nat_of_bitvector n b < 2^n.
-  #n #b cases daemon
-qed.
 
 lemma sublist_tal_pc_list_all_program_counter_list:

src/ASM/Arithmetic.ma

@@ -161 +161 @@
 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
   λn,v. nat_of_bitvector_aux n O v.
+
+lemma nat_of_bitvector_aux_lt_bound:
+ ∀n.∀v:BitVector n. ∀m,l:nat.
+  m < 2^l → nat_of_bitvector_aux n m v < 2^(n+l).
+ #n #v elim v normalize // -n
+ #n #hd #tl #IH #m #l #B cases hd normalize nodelta
+ @(transitive_le … (IH ? (S l) …))
+ [2,4: /2 by le_exp/
+ |1,3: @(transitive_le … (2 * (S m)))
+  [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/
+  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
+qed.  
+
+lemma nat_of_bitvector_lt_bound:
+ ∀n: nat. ∀b: BitVector n. nat_of_bitvector n b < 2^n.
+ #n #b lapply (nat_of_bitvector_aux_lt_bound n b 0 0 ?) // <plus_n_O //
+qed.
 
 lemma bitvector_of_nat_ok: