Changeset 961 for src/Clight/casts.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/Clight/casts.ma (modified) (5 diffs)

src/Clight/casts.ma

@@ -1 @@
-include "common/Integers.ma".
+include "common/Values.ma".
 
 definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
@@ -5 +5 @@
 
 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
-#A #n #x elim x //
+#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
 qed.
 
@@ -82 +82 @@
 lemma truncate_tail : ∀m,n,v.
   truncate (S m) n v = truncate m n (tail … v).
-  //
+#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
   qed.
 
@@ -118 +118 @@
 qed.
 
-definition sign_bit : ∀n. BitVector n → bool ≝
-λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
-
 definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
 λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
-
+ 
 lemma truncate_sign : ∀m,n,x.
   truncate m n (sign … x) = x.
@@ -178 +175 @@
 #m #n #x @(vector_inv_n … x) #h #t elim n
 [ @refl
-| #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl
+| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
 ] qed.