# Changeset 350 for Deliverables

Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (10 years ago)
Message:

less axioms

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

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

 r349 nqed. ndefinition full_add: ∀n: Nat. ∀b, c: BitVector n. ∀d: Bit. fold_left_i ? ? ( λb1, b2: Bool. λd. ndefinition full_add ≝ λn: Nat. λb, c: BitVector n. λd: Bit. fold_right2_i ? ? ? ( λn. λb1, b2: Bool. λd: Bit × (BitVector n). let 〈c1,r〉 ≝ d in 〈inclusive_disjunction (conjunction b1 b2) (conjunction c1 (inclusive_disjunction b1 b2)), (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉) b c 〈c, [ ]〉. (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[]) (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) 〈d, [[ ]]〉 ? b c. ndefinition half_add ≝
• ## Deliverables/D4.1/Matita/List.ma

 r349 ##| nnormalize in p; nnormalize; napply (succ_less_than_or_equal_injective ? ?); nassumption; /2/; ##] nqed.
• ## Deliverables/D4.1/Matita/Nat.ma

 r349 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). (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). *) ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ λm, n: Nat. n ≤ m. less_than_or_equal_b n m. notation "hvbox(n break ≥ m)" 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). (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). *) (* Add Boolean versions.                                                      *) interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). nlet rec less_than_b (m: Nat) (n: Nat) on m ≝ match m with [ Z ⇒ match n with [ Z ⇒ false | S o ⇒ true ] | S o ⇒ match n with [ Z ⇒ false | S p ⇒ less_than_b o p ] ]. (* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *) ndefinition greater_than_b ≝ λm, n: Nat. less_than_b n m. (* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ match n ≤ p with match less_than_or_equal_b n p with [ true ⇒ Z | false ⇒ nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ match n ≤ p with match less_than_or_equal_b n p with [ true ⇒ n | false ⇒ (m + n) - n = m. naxiom less_than_or_equal_monotone: ntheorem less_than_or_equal_monotone: ∀m, n: Nat. m ≤ n → (S m) ≤ (S n). naxiom succ_less_than_or_equal_injective: #m n H; nelim H; /2/. nqed. nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l. #n m l H H1; nelim H1; /2/. nqed. ntheorem succ_less_than_or_equal_injective: ∀m, n: Nat. (S m) ≤ (S n) → m ≤ n. #m n H; nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]); napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]); nnormalize; /3/. nqed. naxiom plus_minus_inverse_right: (m - n) + n = m. naxiom greater_than_b: Nat → Nat → Bool. naxiom less_than_b: Nat → Nat → Bool. naxiom succ_less_than_injective: ntheorem succ_less_than_injective: ∀m, n: Nat. less_than_p (S m) (S n) → m < n. naxiom nothing_less_than_Z: /2/. nqed. nlemma not_less_than_S_Z: ∀m,n: Nat. S m ≤ n → ¬ (n = Z). #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ] nqed. ntheorem nothing_less_than_Z: ∀m: Nat. ¬(m < Z). #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
• ## Deliverables/D4.1/Matita/Status.ma

 r345 λl: Bool. let address ≝ nat_of_bitvector … b in if (decidable_equality address one_hundred_and_twenty_eight) then if (eq_n address one_hundred_and_twenty_eight) then ? else if (decidable_equality address one_hundred_and_forty_four) then else if (eq_n address one_hundred_and_forty_four) then if l then (p1_latch s) else (get_8051_sfr s SFR_P1) else if (decidable_equality address one_hundred_and_sixty) then else if (eq_n address one_hundred_and_sixty) then ? else if (decidable_equality address one_hundred_and_seventy_six) then else if (eq_n address one_hundred_and_seventy_six) then if l then (p3_latch s) else (get_8051_sfr s SFR_P3) else if (decidable_equality address one_hundred_and_fifty_three) then else if (eq_n address one_hundred_and_fifty_three) then get_8051_sfr s SFR_SBUF else if (decidable_equality address one_hundred_and_thirty_eight) then else if (eq_n address one_hundred_and_thirty_eight) then get_8051_sfr s SFR_TL0 else if (decidable_equality address one_hundred_and_thirty_nine) then else if (eq_n address one_hundred_and_thirty_nine) then get_8051_sfr s SFR_TL1 else if (decidable_equality address one_hundred_and_forty) then else if (eq_n address one_hundred_and_forty) then get_8051_sfr s SFR_TH0 else if (decidable_equality address one_hundred_and_forty_one) then else if (eq_n address one_hundred_and_forty_one) then get_8051_sfr s SFR_TH1 else if (decidable_equality address two_hundred) then else if (eq_n address two_hundred) then get_8052_sfr s SFR_T2CON else if (decidable_equality address two_hundred_and_two) then else if (eq_n address two_hundred_and_two) then get_8052_sfr s SFR_RCAP2L else if (decidable_equality address two_hundred_and_three) then else if (eq_n address two_hundred_and_three) then get_8052_sfr s SFR_RCAP2H else if (decidable_equality address two_hundred_and_four) then else if (eq_n address two_hundred_and_four) then get_8052_sfr s SFR_TL2 else if (decidable_equality address two_hundred_and_five) then else if (eq_n address two_hundred_and_five) then get_8052_sfr s SFR_TH2 else if (decidable_equality address one_hundred_and_thirty_five) then else if (eq_n address one_hundred_and_thirty_five) then get_8051_sfr s SFR_PCON else if (decidable_equality address one_hundred_and_thirty_six) then else if (eq_n address one_hundred_and_thirty_six) then get_8051_sfr s SFR_TCON else if (decidable_equality address one_hundred_and_thirty_seven) then else if (eq_n address one_hundred_and_thirty_seven) then get_8051_sfr s SFR_TMOD else if (decidable_equality address one_hundred_and_fifty_two) then else if (eq_n address one_hundred_and_fifty_two) then get_8051_sfr s SFR_SCON else if (decidable_equality address one_hundred_and_sixty_eight) then else if (eq_n address one_hundred_and_sixty_eight) then get_8051_sfr s SFR_IE else if (decidable_equality address one_hundred_and_eighty_four) then else if (eq_n address one_hundred_and_eighty_four) then get_8051_sfr s SFR_IP else if (decidable_equality address one_hundred_and_twenty_nine) then else if (eq_n address one_hundred_and_twenty_nine) then get_8051_sfr s SFR_SP else if (decidable_equality address one_hundred_and_thirty) then else if (eq_n address one_hundred_and_thirty) then get_8051_sfr s SFR_DPL else if (decidable_equality address one_hundred_and_thirty_one) then else if (eq_n address one_hundred_and_thirty_one) then get_8051_sfr s SFR_DPH else if (decidable_equality address two_hundred_and_eight) then else if (eq_n address two_hundred_and_eight) then get_8051_sfr s SFR_PSW else if (decidable_equality address two_hundred_and_twenty_four) then else if (eq_n address two_hundred_and_twenty_four) then get_8051_sfr s SFR_ACC_A else if (decidable_equality address two_hundred_and_forty) then else if (eq_n address two_hundred_and_forty) then get_8051_sfr s SFR_ACC_B else λv: Byte. let address ≝ nat_of_bitvector … b in if (decidable_equality address one_hundred_and_twenty_eight) then if (eq_n address one_hundred_and_twenty_eight) then ? else if (decidable_equality address one_hundred_and_forty_four) then else if (eq_n address one_hundred_and_forty_four) then let status_1 ≝ set_8051_sfr s SFR_P1 v in let status_2 ≝ set_p1_latch s v in status_2 else if (decidable_equality address one_hundred_and_sixty) then else if (eq_n address one_hundred_and_sixty) then ? else if (decidable_equality address one_hundred_and_seventy_six) then else if (eq_n address one_hundred_and_seventy_six) then let status_1 ≝ set_8051_sfr s SFR_P3 v in let status_2 ≝ set_p3_latch s v in status_2 else if (decidable_equality address one_hundred_and_fifty_three) then else if (eq_n address one_hundred_and_fifty_three) then set_8051_sfr s SFR_SBUF v else if (decidable_equality address one_hundred_and_thirty_eight) then else if (eq_n address one_hundred_and_thirty_eight) then set_8051_sfr s SFR_TL0 v else if (decidable_equality address one_hundred_and_thirty_nine) then else if (eq_n address one_hundred_and_thirty_nine) then set_8051_sfr s SFR_TL1 v else if (decidable_equality address one_hundred_and_forty) then else if (eq_n address one_hundred_and_forty) then set_8051_sfr s SFR_TH0 v else if (decidable_equality address one_hundred_and_forty_one) then else if (eq_n address one_hundred_and_forty_one) then set_8051_sfr s SFR_TH1 v else if (decidable_equality address two_hundred) then else if (eq_n address two_hundred) then set_8052_sfr s SFR_T2CON v else if (decidable_equality address two_hundred_and_two) then else if (eq_n address two_hundred_and_two) then set_8052_sfr s SFR_RCAP2L v else if (decidable_equality address two_hundred_and_three) then else if (eq_n address two_hundred_and_three) then set_8052_sfr s SFR_RCAP2H v else if (decidable_equality address two_hundred_and_four) then else if (eq_n address two_hundred_and_four) then set_8052_sfr s SFR_TL2 v else if (decidable_equality address two_hundred_and_five) then else if (eq_n address two_hundred_and_five) then set_8052_sfr s SFR_TH2 v else if (decidable_equality address one_hundred_and_thirty_five) then else if (eq_n address one_hundred_and_thirty_five) then set_8051_sfr s SFR_PCON v else if (decidable_equality address one_hundred_and_thirty_six) then else if (eq_n address one_hundred_and_thirty_six) then set_8051_sfr s SFR_TCON v else if (decidable_equality address one_hundred_and_thirty_seven) then else if (eq_n address one_hundred_and_thirty_seven) then set_8051_sfr s SFR_TMOD v else if (decidable_equality address one_hundred_and_fifty_two) then else if (eq_n address one_hundred_and_fifty_two) then set_8051_sfr s SFR_SCON v else if (decidable_equality address one_hundred_and_sixty_eight) then else if (eq_n address one_hundred_and_sixty_eight) then set_8051_sfr s SFR_IE v else if (decidable_equality address one_hundred_and_eighty_four) then else if (eq_n address one_hundred_and_eighty_four) then set_8051_sfr s SFR_IP v else if (decidable_equality address one_hundred_and_twenty_nine) then else if (eq_n address one_hundred_and_twenty_nine) then set_8051_sfr s SFR_SP v else if (decidable_equality address one_hundred_and_thirty) then else if (eq_n address one_hundred_and_thirty) then set_8051_sfr s SFR_DPL v else if (decidable_equality address one_hundred_and_thirty_one) then else if (eq_n address one_hundred_and_thirty_one) then set_8051_sfr s SFR_DPH v else if (decidable_equality address two_hundred_and_eight) then else if (eq_n address two_hundred_and_eight) then set_8051_sfr s SFR_PSW v else if (decidable_equality address two_hundred_and_twenty_four) then else if (eq_n address two_hundred_and_twenty_four) then set_8051_sfr s SFR_ACC_A v else if (decidable_equality address two_hundred_and_forty) then else if (eq_n address two_hundred_and_forty) then set_8051_sfr s SFR_ACC_B v else ndefinition load_code_memory ≝ fold_lefti … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen). fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen). ndefinition load ≝
• ## Deliverables/D4.1/Matita/Test.ma

 r347 nqed. ndefinition testfinal ≝ execute five teststatus. ndefinition testfinal ≝ execute one teststatus. nlemma hoo: (*half_add ? (program_counter teststatus)*) (bitvector_of_nat sixteen (S Z)) = (bitvector_of_nat sixteen (S Z)). (*half_add (code_memory teststatus) (program_counter teststatus). *) nwhd in ⊢ (??%?); nlemma hoo: testfinal = testfinal. nwhd in ⊢ (???%); nwhd in ⊢ (??%?); nnormalize; @. nqed.
• ## Deliverables/D4.1/Matita/Vector.ma

 r340 ]. nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) (f: A → B → C → C) (c: C) (v: Vector A n) (q: Vector B n) on v ≝ (match v return λx.λ_. x = n → C with nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0]) (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat) (v: Vector A n) (q: Vector B n) on v : C n ≝ (match v return λx.λ_. x = n → C n with [ Empty ⇒ match q return λx.λ_. Z = x → C with match q return λx.λ_. Z = x → C x with [ Empty ⇒ λprf: Z = Z. c | Cons o hd tl ⇒ λabsd. ? | Cons o hd tl ⇒ λabsd. ⊥ ] | Cons o hd tl ⇒ match q return λx.λ_. S o = x → C with [ Empty ⇒ λabsd: S o = Z. ? match q return λx.λ_. S o = x → C x with [ Empty ⇒ λabsd: S o = Z. ⊥ | Cons p hd' tl' ⇒ λprf: S o = S p. fold_right_i A B C o f (f hd hd' c) tl ? (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉ ] ]) (refl ? n). ##[##1,2: ndestruct; ##| ndestruct (prf); napply tl'; ##] ndestruct; //. nqed.
Note: See TracChangeset for help on using the changeset viewer.