Changeset 2124 for src/ASM/BitVector.ma
 Timestamp:
 Jun 27, 2012, 4:23:54 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r2122 r2124 236 236 String. 237 237 238 example sub_minus_one_seven_eight: 239 ∀v: BitVector 7. 240 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 241 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 242 cases daemon. 243 qed. 244 245 axiom sub16_with_carry_overflow: 246 ∀left, right, result: BitVector 16. 247 ∀flags: BitVector 3. 248 ∀upper: BitVector 9. 249 ∀lower: BitVector 7. 250 sub_16_with_carry left right false = 〈result, flags〉 → 251 vsplit bool 9 7 result = 〈upper, lower〉 → 252 get_index_v bool 3 flags 2 ? = true → 253 upper = [[true; true; true; true; true; true; true; true; true]]. 254 // 255 qed. 256 257 axiom sub_16_to_add_16_8_0: 258 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 259 get_index' ? 2 0 flags = false → 260 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 261 v1 = add ? v2 (sign_extension (false:::v3)). 262 263 axiom sub_16_to_add_16_8_1: 264 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 265 get_index' ? 2 0 flags = true → 266 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 267 v1 = add ? v2 (sign_extension (true:::v3)). 238 definition bitvector_3_cases: 239 ∀b: BitVector 3. 240 ∃l, c, r: bool. 241 b ≃ [[l; c; r]]. 242 #b 243 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 244 [1: 245 #absurd @⊥ b @(destruct_bug_fix_1 2) 246 >absurd % 247 2: 248 #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} 249 cut (n = 2) 250 [1: 251 @destruct_bug_fix_2 252 >size_refl % 253 2: 254 #n_refl >n_refl in tl; #V 255 @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) 256 [1: 257 #absurd @⊥ V @(destruct_bug_fix_1 1) 258 >absurd % 259 2: 260 #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} 261 cut (n' = 1) 262 [1: 263 @destruct_bug_fix_2 >size_refl' % 264 2: 265 #n_refl' >n_refl' in tl'; #V' 266 @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) 267 [1: 268 #absurd @⊥ V' @(destruct_bug_fix_1 0) 269 >absurd % 270 2: 271 #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} 272 cut (n'' = 0) 273 [1: 274 @destruct_bug_fix_2 >size_refl'' % 275 2: 276 #n_refl'' >n_refl'' in tl''; #tl''' 277 >(Vector_O … tl''') % 278 ] 279 ] 280 ] 281 ] 282 ] 283 ] 284 qed. 285 286 lemma bitvector_3_elim_prop: 287 ∀P: BitVector 3 → Prop. 288 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → 289 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → 290 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 291 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 292 cases (bitvector_3_cases … H9) #l #assm cases assm 293 assm #c #assm cases assm 294 assm #r #assm cases assm destruct 295 cases l cases c cases r assumption 296 qed.
Note: See TracChangeset
for help on using the changeset viewer.