Changeset 2673 for src/ASM/Arithmetic.ma
 Timestamp:
 Feb 18, 2013, 1:18:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2672 r2673 162 162 λn,v. nat_of_bitvector_aux n O v. 163 163 164 (* TODO: remove when standard library arithmetics/exp.ma is used in place 165 of definition in ASM/Util.ma *) 166 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. 167 #n #m (elim m) normalize // #a #Hind #posn 168 @(le_times 1 ? 1) /2 by / qed. 169 theorem le_exp: ∀n,m,p:nat. O < p → 170 n ≤m → p^n ≤ p^m. 171 @nat_elim2 #n #m 172 [#ltm #len @lt_O_exp // 173 #_ #len @False_ind /2 by absurd/ 174 #Hind #p #posp #lenm normalize @le_times // @Hind /2 by monotonic_pred/ 175 ] 176 qed. 177 164 178 lemma nat_of_bitvector_aux_lt_bound: 165 179 ∀n.∀v:BitVector n. ∀m,l:nat. … … 168 182 #n #hd #tl #IH #m #l #B cases hd normalize nodelta 169 183 @(transitive_le … (IH ? (S l) …)) 170 [2,4: /2 by le_exp/184 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/ 171 185 1,3: @(transitive_le … (2 * (S m))) 172 [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/186 [2,4: /2 by le_times/ 173 187 3: //  1: normalize <plus_n_O <plus_n_Sm // ]] 174 188 qed.
Note: See TracChangeset
for help on using the changeset viewer.