Changeset 2032 for src/Clight/casts.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/casts.ma
r1599 r2032 2 2 3 3 definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ 4 λm,n,x. \snd ( split … x).5 6 lemma split_O_n : ∀A,n,x.split A O n x = 〈[[ ]], x〉.4 λm,n,x. \snd (vsplit … x). 5 6 lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉. 7 7 #A #n cases n [ #x @(vector_inv_n … x) @refl  #m #x @(vector_inv_n … x) // ] 8 8 qed. 9 9 10 10 lemma truncate_eq : ∀n,x. truncate 0 n x = x. 11 #n #x normalize > split_O_n @refl11 #n #x normalize >vsplit_O_n @refl 12 12 qed. 13 13 … … 66 66 qed. 67 67 68 lemma split_eq' : ∀A,m,n,v. split A m n v =split' A m n v.68 lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v. 69 69 #A #m cases m 70 70 [ #n cases n … … 75 75 ] qed. 76 76 77 lemma split_left : ∀A,m,n,h,t.78 split A (S m) n (h:::t) = (let 〈l,r〉 ≝split A m n t in 〈h:::l,r〉).79 #A #m #n #h #t normalize > split_eq' @refl77 lemma vsplit_left : ∀A,m,n,h,t. 78 vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉). 79 #A #m #n #h #t normalize >vsplit_eq' @refl 80 80 qed. 81 81 82 82 lemma truncate_head : ∀m,n,h,t. 83 83 truncate (S m) n (h:::t) = truncate m n t. 84 #m #n #h #t normalize > split_eq' cases (split' bool m n t) //84 #m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) // 85 85 qed. 86 86
Note: See TracChangeset
for help on using the changeset viewer.