Changeset 2124 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (8 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2111 r2124  
    191191
    192192axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
     193
     194axiom 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.
    193198
    194199lemma nat_of_bitvector_aux_injective:
     
    707712    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
    708713   
     714lemma 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
     719qed.
     720
    709721definition sign_bit : ∀n. BitVector n → bool ≝
    710722λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
     
    729741  ].
    730742
     743example 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.
     748qed.
     749
     750axiom 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  //
     760qed.
     761
     762axiom 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
     768axiom 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.