# Changeset 351 for Deliverables/D4.1/Matita

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

No more axioms but the paralogisms.

Location:
Deliverables/D4.1/Matita
Files:
6 edited

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

 r350 let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) + (modulus c_as_nat ((S (S Z)) * n)) + c_as_nat) ≥ ((S (S Z)) * n) in c_as_nat) ≳ ((S (S Z)) * n) in let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) + (modulus c_as_nat ((S (S Z))^(n - (S Z)))) + c_as_nat) ≥ ((S (S Z))^(n - (S Z)))) in c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in let result ≝ modulus result_old ((S (S Z))^n) in let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result)) let carry_as_nat ≝ nat_of_bool carry in let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in 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 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in 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 let old_result_1 ≝ b_as_nat - c_as_nat in let old_result_2 ≝ old_result_1 - carry_as_nat in let ov_flag ≝ exclusive_disjunction carry bit_six in match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with [ false ⇒ let cy_flag ≝ false in λb: BitVector n. let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in let overflow ≝ b_as_nat ≥ (S (S Z))^n in let overflow ≝ b_as_nat ≳ (S (S Z))^n in match overflow with [ false ⇒ bitvector_of_nat n b_as_nat ndefinition bitvector_of_bool: ∀n: Nat. ∀b: Bool. BitVector n ≝ ∀n: Nat. ∀b: Bool. BitVector (S n) ≝ λn: Nat. λb: Bool. ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). nrewrite > (plus_minus_inverse_right n ?); #H; nassumption; ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). nrewrite > plus_minus_inverse_right [ napply (λx.x) | /2/] nqed.
• ## Deliverables/D4.1/Matita/BitVector.ma

 r349 let bitvector ≝ bitvector_of_list biglist in let difference ≝ n - size in match greater_than_b size n with [ true ⇒ max n | false ⇒ ? (pad difference size bitvector) ]. nnormalize. nrewrite > (plus_minus_inverse_right n ?). #H. nassumption. less_than_or_equal_b_elim … (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉)) (λH:¬(size ≤ n). max n). nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption. nqed.
• ## Deliverables/D4.1/Matita/Exponential.ma

 r268 nqed. (* naxiom exponential_addition_exponential_multiplication: ∀m, n, o: Nat. (m^n) * (m^o) = m^(n + o). (* nlemma exponential_exponential_multiplication: ∀m, n, o: Nat.
• ## Deliverables/D4.1/Matita/Interpret.ma

 r347 include "Arithmetic.ma". include "List.ma". alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)". ndefinition sign_extension: Byte → Word ≝ let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in let 〈nu, nl〉 ≝ split ? four four pc_bu in let bit ≝ cic:/matita/ng/Vector/get_index.fix(0,3,2) ? ? nl Z ? in let bit ≝ get_index_bv ? nl Z ? in let 〈relevant1, relevant2〉 ≝ split ? three eight a in let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
• ## Deliverables/D4.1/Matita/Nat.ma

 r350 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). *) notation "hvbox(n break ≲ m)" non associative with precedence 47 for @{ 'less_than_or_equalb \$n \$m }. interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m). ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). *) notation "hvbox(n break ≳ m)" non associative with precedence 47 for @{ 'greater_than_or_equalb \$n \$m }. interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m). (* Add Boolean versions.                                                      *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) naxiom plus_minus_inverse_left: (*naxiom plus_minus_inverse_left: ∀m, n: Nat. (m + n) - n = m. *) ntheorem less_than_or_equal_monotone: ∀m, n: Nat. nqed. ntheorem succ_less_than_or_equal_injective: ntheorem less_than_or_equal_injective: ∀m, n: Nat. (S m) ≤ (S n) → m ≤ n. nqed. naxiom plus_minus_inverse_right: ∀m, n: Nat. (m - n) + n = m. ntheorem succ_less_than_injective: ∀m, n: Nat. #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nqed. naxiom less_than_or_equal_injective: ∀m, n: Nat. S m ≤ S n → m ≤ n. (* nlemma less_than_or_equal_zero_equal_zero: nqed. nlemma succ_injective: ∀m, n: Nat. S m = S n → m = n. #m n H; napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with [refl ⇒ ? ]); @; nqed. ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'. //; nqed. ntheorem plus_minus_inverse_right: ∀m, n: Nat. n ≤ m → (m - n) + n = m. #m; nelim m [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1); #K; ncases (K H3) | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/; #w; nrewrite < succ_plus; /4/. ##] nqed. (* nlemma succ_injective: ∀m, n: Nat. S m = S n → m = n. #m n. nelim m. #H. ninversion H. #H. ndestruct nlemma plus_minus_associate: #N H. *) ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n. #m; nelim m; //; #y H1 z; ncases z; nnormalize [ #H; ndestruct | /3/ ] nqed. ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n). #m; nelim m; nnormalize [ #n H; ndestruct | #y H1 z; ncases z; nnormalize [ #H; ndestruct | /3/ ] /2/. nqed. ndefinition less_than_or_equal_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (less_than_or_equal_b m n). #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); nlapply (less_than_or_equal_b_complete m n); ncases (less_than_or_equal_b m n); /3/. nqed. ndefinition greater_than_or_equal_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) → P (greater_than_or_equal_b m n). #m n; napply less_than_or_equal_b_elim; nqed. ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n. #m; nelim m [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ] ##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K; napply less_than_or_equal_monotone; napply H; napply K ] nqed. ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n). #m; nelim m [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/. nqed. ndefinition less_than_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) → P (less_than_b m n). #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n); ncases (less_than_b m n); /3/. nqed. ndefinition greater_than_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) → P (greater_than_b m n). #m n; napply less_than_b_elim. nqed.
• ## Deliverables/D4.1/Matita/Status.ma

 r350 }. naxiom sfr8051_index_nineteen: nlemma sfr8051_index_nineteen: ∀i: SFR8051. sfr_8051_index i < nineteen. #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); napply less_than_or_equal_zero. nqed. naxiom sfr8052_index_five: nlemma sfr8052_index_five: ∀i: SFR8052. sfr_8052_index i < five. #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); napply less_than_or_equal_zero. nqed. ndefinition set_clock ≝ old_clock. alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)". ndefinition get_8051_sfr ≝ λs: Status. let sfr ≝ special_function_registers_8051 s in let index ≝ sfr_8051_index i in get_index … sfr index ?. get_index ?? sfr index ?. napply (sfr8051_index_nineteen i). nqed. let sfr ≝ special_function_registers_8052 s in let index ≝ sfr_8052_index i in get_index … sfr index ?. get_index ?? sfr index ?. napply (sfr8052_index_five i). nqed. let old_special_function_registers_8052 ≝ special_function_registers_8052 s in let new_special_function_registers_8051 ≝ cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in set_index Byte nineteen old_special_function_registers_8051 index b ? in let old_p1_latch ≝ p1_latch s in let old_p3_latch ≝ p3_latch s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in let new_special_function_registers_8052 ≝ cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in set_index Byte five old_special_function_registers_8052 index b ? in let old_p1_latch ≝ p1_latch s in let old_p3_latch ≝ p3_latch s in old_p3_latch old_clock. naxiom less_than_or_equal_monotone: ∀m, n: Nat. m ≤ n → S m ≤ S n. alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)". ndefinition get_cy_flag ≝ nqed. naxiom modulus_less_than: ∀m,n: Nat. (m mod n) < n. ntheorem modulus_less_than: ∀m,n: Nat. (m mod (S n)) < S n. #n m; nnormalize; napply less_than_or_equal_monotone; nlapply (ltoe_refl n); ngeneralize in ⊢ (?%? → ?(??%?)?); nelim n in ⊢ (∀_:?. ??% → ?(?%??)?) [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize [ // | #H K; ninversion K [ #H1; ndestruct; // | #x H1 H2 H3; ndestruct ]##] ##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/; ncases n; nnormalize; //; #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m; nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //; #q K2; napply H; /3/] nqed. ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → napply less_than_or_equal_zero; ##|##4,5: napply (modulus_less_than address eight); napply modulus_less_than; ##] nqed.
Note: See TracChangeset for help on using the changeset viewer.