Changeset 961 for src/Clight/casts.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/casts.ma
r824 r961 1 include "common/ Integers.ma".1 include "common/Values.ma". 2 2 3 3 definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ … … 5 5 6 6 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉. 7 #A #n #x elim x //7 #A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ] 8 8 qed. 9 9 … … 82 82 lemma truncate_tail : ∀m,n,v. 83 83 truncate (S m) n v = truncate m n (tail … v). 84 // 84 #m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl 85 85 qed. 86 86 … … 118 118 qed. 119 119 120 definition sign_bit : ∀n. BitVector n → bool ≝121 λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].122 123 120 definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝ 124 121 λm,n,v. pad_vector ? (sign_bit ? v) ?? v. 125 122 126 123 lemma truncate_sign : ∀m,n,x. 127 124 truncate m n (sign … x) = x. … … 178 175 #m #n #x @(vector_inv_n … x) #h #t elim n 179 176 [ @refl 180 | #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl177 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl 181 178 ] qed. 182 179
Note: See TracChangeset
for help on using the changeset viewer.