Changeset 2124 for src/ASM/Arithmetic.ma
 Timestamp:
 Jun 27, 2012, 4:23:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2111 r2124 191 191 192 192 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. 193 194 axiom eq_bitvector_of_nat_to_eq: 195 ∀n,n1,n2. 196 n1 < 2^n → n2 < 2^n → 197 bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2. 193 198 194 199 lemma nat_of_bitvector_aux_injective: … … 707 712 add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q). 708 713 714 lemma add_bitvector_of_nat_Sm: 715 ∀n, m: nat. 716 add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = 717 bitvector_of_nat n (S m). 718 #n #m @add_bitvector_of_nat_plus 719 qed. 720 709 721 definition sign_bit : ∀n. BitVector n → bool ≝ 710 722 λn,v. match v with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]. … … 729 741 ]. 730 742 743 example sub_minus_one_seven_eight: 744 ∀v: BitVector 7. 745 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 746 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 747 cases daemon. 748 qed. 749 750 axiom sub16_with_carry_overflow: 751 ∀left, right, result: BitVector 16. 752 ∀flags: BitVector 3. 753 ∀upper: BitVector 9. 754 ∀lower: BitVector 7. 755 sub_16_with_carry left right false = 〈result, flags〉 → 756 vsplit bool 9 7 result = 〈upper, lower〉 → 757 get_index_v bool 3 flags 2 ? = true → 758 upper = [[true; true; true; true; true; true; true; true; true]]. 759 // 760 qed. 761 762 axiom sub_16_to_add_16_8_0: 763 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 764 get_index' ? 2 0 flags = false → 765 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 766 v1 = add ? v2 (sign_extension (false:::v3)). 767 768 axiom sub_16_to_add_16_8_1: 769 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 770 get_index' ? 2 0 flags = true → 771 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 772 v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracChangeset
for help on using the changeset viewer.