Changeset 1870 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Apr 3, 2012, 2:52:10 PM (8 years ago)
Author:
boender
Message:
  • changed sigma00 in Assembly to use foldl_strong + proved invariants
  • commented out sigma00_append
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1646 r1870  
    161161definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
    162162  λn,v. nat_of_bitvector_aux n O v.
    163    
     163
     164lemma bitvector_of_nat_ok:
     165  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
     166 #n elim n -n
     167 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
     168 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
     169 ]
     170qed.
     171
     172lemma bitvector_of_nat_abs:
     173  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
     174 #n #x #y #Hx #Hy #Heq @notb_elim
     175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
     176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
     177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
     178 | #H / by I/
     179 ]
     180qed.
     181
    164182definition two_complement_negation ≝
    165183  λn: nat.
Note: See TracChangeset for help on using the changeset viewer.