# Changeset 1870 for src/ASM/Arithmetic.ma

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

Unmodified
Added
Removed
• ## src/ASM/Arithmetic.ma

 r1646 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ λn,v. nat_of_bitvector_aux n O v. lemma bitvector_of_nat_ok: ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. #n elim n -n [ #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 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) ] qed. lemma bitvector_of_nat_abs: ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y). #n #x #y #Hx #Hy #Heq @notb_elim lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/ | #H / by I/ ] qed. definition two_complement_negation ≝ λn: nat.
Note: See TracChangeset for help on using the changeset viewer.