Changeset 985 for src/ASM/BitVector.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r961 r985 8 8 include "arithmetics/nat.ma". 9 9 10 include "ASM/ Util.ma".10 include "ASM/FoldStuff.ma". 11 11 include "ASM/Vector.ma". 12 12 include "ASM/String.ma". … … 25 25 26 26 (* ===================================== *) 27 (* Inversion *) 28 (* ===================================== *) 29 30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 32 #n #hd #tl #abs @⊥ // 33 qed. 34 35 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 36 ∃hd.∃tl.v ≃ VCons bool n hd tl. 37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 38 [ #abs @⊥ // 39  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 40 qed. 41 42 (* ===================================== *) 27 43 (* Lookup. *) 28 44 (* ===================================== *) … … 98 114 notb c. 99 115 116 lemma eq_b_eq: 117 ∀b, c. 118 eq_b b c = true → b = c. 119 #b #c 120 cases b 121 cases c 122 normalize // 123 qed. 124 100 125 definition eq_bv ≝ 101 126 λn: nat. … … 118 143 #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct  @NE ] 119 144 qed. 120 145 146 lemma eq_bv_refl: 147 ∀n,v. eq_bv n v v = true. 148 #n #v 149 elim v 150 [ // 151  #n #hd #tl #ih 152 normalize 153 cases hd 154 [ normalize 155 @ ih 156  normalize 157 @ ih 158 ] 159 ] 160 qed. 161 162 lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1. 163 #n #v1 #v2 @(eq_bv_elim … v1 v2) [//  #H >eq_bv_false /2/] 164 qed. 165 166 lemma eq_eq_bv: 167 ∀n, v, q. 168 v = q → eq_bv n v q = true. 169 #n #v 170 elim v 171 [ #q #h <h normalize % 172  #n #hd #tl #ih #q #h >h // 173 ] 174 qed. 175 176 lemma eq_bv_eq: 177 ∀n, v, q. 178 eq_bv n v q = true → v = q. 179 #n #v #q generalize in match v 180 elim q 181 [ #v #h @BitVector_O 182  #n #hd #tl #ih #v' #h 183 cases (BitVector_Sn ? v') 184 #hd' * #tl' #jmeq >jmeq in h; 185 #new_h 186 change in new_h with ((andb ? ?) = ?); 187 cases(conjunction_true … new_h) 188 #eq_heads #eq_tails 189 whd in eq_heads:(??(??(%))?); 190 cases(eq_b_eq … eq_heads) 191 whd in eq_tails:(??(?????(%))?); 192 change in eq_tails with (eq_bv ??? = ?); 193 <(ih tl') // 194 ] 195 qed. 196 121 197 axiom bitvector_of_string: 122 198 ∀n: nat.
Note: See TracChangeset
for help on using the changeset viewer.