Ignore:
Timestamp:
Dec 1, 2010, 4:30:46 PM (10 years ago)
Author:
mulligan
Message:

No more axioms but the paralogisms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r350 r351  
    7878    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
    7979                  (modulus c_as_nat ((S (S Z)) * n)) +
    80                   c_as_nat) ((S (S Z)) * n) in
     80                  c_as_nat) ((S (S Z)) * n) in
    8181    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
    8282                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
    83                   c_as_nat) ((S (S Z))^(n - (S Z)))) in
     83                  c_as_nat) ((S (S Z))^(n - (S Z)))) in
    8484    let result ≝ modulus result_old ((S (S Z))^n) in
    85     let cy_flag ≝ (result_old ((S (S Z))^n)) in
     85    let cy_flag ≝ (result_old ((S (S Z))^n)) in
    8686    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    8787      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
     
    9898    let carry_as_nat ≝ nat_of_bool carry in
    9999    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
    100     let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in
    101     let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≤ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≤ carry_as_nat)) in
     100    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
     101    let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in
    102102    let old_result_1 ≝ b_as_nat - c_as_nat in
    103103    let old_result_2 ≝ old_result_1 - carry_as_nat in
    104104    let ov_flag ≝ exclusive_disjunction carry bit_six in
    105       match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with
     105      match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
    106106        [ false ⇒
    107107           let cy_flag ≝ false in
     
    120120  λb: BitVector n.
    121121    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
    122     let overflow ≝ b_as_nat (S (S Z))^n in
     122    let overflow ≝ b_as_nat (S (S Z))^n in
    123123      match overflow with
    124124        [ false ⇒ bitvector_of_nat n b_as_nat
     
    138138
    139139ndefinition bitvector_of_bool:
    140       ∀n: Nat. ∀b: Bool. BitVector n
     140      ∀n: Nat. ∀b: Bool. BitVector (S n)
    141141  λn: Nat.
    142142  λb: Bool.
    143     ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
    144   nrewrite > (plus_minus_inverse_right n ?);
    145   #H;
    146   nassumption;
     143    ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
     144  nrewrite > plus_minus_inverse_right
     145   [ napply (λx.x) | /2/]
    147146nqed.
    148147
Note: See TracChangeset for help on using the changeset viewer.