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

No more axioms but the paralogisms.

File:
1 edited

Legend:

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

    r350 r351  
    103103}.
    104104
    105 naxiom sfr8051_index_nineteen:
     105nlemma sfr8051_index_nineteen:
    106106  ∀i: SFR8051.
    107107    sfr_8051_index i < nineteen.
     108 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
     109 napply less_than_or_equal_zero.
     110nqed.
    108111   
    109 naxiom sfr8052_index_five:
     112nlemma sfr8052_index_five:
    110113  ∀i: SFR8052.
    111114    sfr_8052_index i < five.
     115 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
     116 napply less_than_or_equal_zero.
     117nqed.
    112118   
    113119ndefinition set_clock ≝
     
    180186                old_clock.
    181187
    182 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
    183188ndefinition get_8051_sfr ≝
    184189  λs: Status.
     
    186191    let sfr ≝ special_function_registers_8051 s in
    187192    let index ≝ sfr_8051_index i in
    188       get_index sfr index ?.
     193      get_index ?? sfr index ?.
    189194    napply (sfr8051_index_nineteen i).
    190195nqed.
     
    195200    let sfr ≝ special_function_registers_8052 s in
    196201    let index ≝ sfr_8052_index i in
    197       get_index sfr index ?.
     202      get_index ?? sfr index ?.
    198203    napply (sfr8052_index_five i).
    199204nqed.
     
    212217    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    213218    let new_special_function_registers_8051 ≝
    214       cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
     219      set_index Byte nineteen old_special_function_registers_8051 index b ? in
    215220    let old_p1_latch ≝ p1_latch s in
    216221    let old_p3_latch ≝ p3_latch s in
     
    242247    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    243248    let new_special_function_registers_8052 ≝
    244       cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
     249      set_index Byte five old_special_function_registers_8052 index b ? in
    245250    let old_p1_latch ≝ p1_latch s in
    246251    let old_p3_latch ≝ p3_latch s in
     
    374379                old_p3_latch
    375380                old_clock.
    376                
    377 naxiom less_than_or_equal_monotone:
    378   ∀m, n: Nat.
    379     m ≤ n → S m ≤ S n.
    380    
    381 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
    382381               
    383382ndefinition get_cy_flag ≝
     
    887886nqed.
    888887
    889 naxiom modulus_less_than:
    890   ∀m,n: Nat.
    891     (m mod n) < n.
     888ntheorem modulus_less_than:
     889  ∀m,n: Nat. (m mod (S n)) < S n.
     890 #n m; nnormalize; napply less_than_or_equal_monotone;
     891 nlapply (ltoe_refl n);
     892 ngeneralize in ⊢ (?%? → ?(??%?)?);
     893 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
     894  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
     895     [ // | #H K; ninversion K [ #H1; ndestruct; // | #x H1 H2 H3; ndestruct ]##]
     896##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
     897     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
     898       ncases n; nnormalize; //;
     899       #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m;
     900       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
     901       #q K2; napply H; /3/]
     902nqed.
    892903
    893904ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
     
    9911002          napply less_than_or_equal_zero;
    9921003      ##|##4,5:
    993           napply (modulus_less_than address eight);
     1004          napply modulus_less_than;
    9941005      ##]
    9951006nqed.
Note: See TracChangeset for help on using the changeset viewer.