 Timestamp:
 Jun 15, 2011, 4:15:52 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r949 r961 344 344 λb, c: BitVector n. 345 345 full_add n b c false. 346 347 definition sign_bit : ∀n. BitVector n → bool ≝ 348 λn,v. match v with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]. 349 350 definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝ 351 λm,n,v. pad_vector ? (sign_bit ? v) ?? v. 352 353 definition zero_ext : ∀m,n. BitVector m → BitVector n ≝ 354 λm,n. 355 match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with 356 [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v) 357  nat_eq n' ⇒ λv. v 358  nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v)) 359 ]. 360 361 definition sign_ext : ∀m,n. BitVector m → BitVector n ≝ 362 λm,n. 363 match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with 364 [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v) 365  nat_eq n' ⇒ λv. v 366  nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v)) 367 ]. 368 
src/ASM/BitVector.ma
r868 r961 110 110 #Q * *; normalize /3/ 111 111 qed. 112 113 lemma eq_bv_true: ∀n,v. eq_bv n v v = true. 114 @eq_v_true * @refl 115 qed. 116 117 lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. 118 #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct  @NE ] 119 qed. 112 120 113 121 axiom bitvector_of_string: 
src/ASM/Vector.ma
r889 r961 477 477 ] qed. 478 478 479 lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true. 480 #A #f #f_true #n #v elim v 481 [ // 482  #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl 483 ] qed. 484 485 lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'. 486 #A #n #h #t #t' * #NE % #E @NE >E @refl 487 qed. 488 489 lemma eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false. 490 #A #f #f_true #n elim n 491 [ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl 492  #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t' 493 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/ 494 ] qed. 495 479 496 (* ===================================== *) 480 497 (* Subvectors. *)
Note: See TracChangeset
for help on using the changeset viewer.