Changeset 985 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (8 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r961 r985  
    88include "arithmetics/nat.ma".
    99
    10 include "ASM/Util.ma".
     10include "ASM/FoldStuff.ma".
    1111include "ASM/Vector.ma".
    1212include "ASM/String.ma".
     
    2525
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     27(* Inversion                                                                  *)
     28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     29
     30lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     32 #n #hd #tl #abs @⊥ //
     33qed.
     34
     35lemma 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] // ]
     40qed.
     41
     42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2743(* Lookup.                                                                    *)
    2844(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    98114      notb c.
    99115
     116lemma 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 //
     123qed.
     124
    100125definition eq_bv ≝
    101126  λn: nat.
     
    118143#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
    119144qed.
    120    
     145
     146lemma 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  ]
     160qed.
     161
     162lemma 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/]
     164qed.
     165
     166lemma 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  ]
     174qed.
     175
     176lemma 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  ]
     195qed.
     196
    121197axiom bitvector_of_string:
    122198  ∀n: nat.
Note: See TracChangeset for help on using the changeset viewer.