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

less axioms

File:
1 edited

Legend:

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

    r345 r350  
    526526  λl: Bool.
    527527    let address ≝ nat_of_bitvector … b in
    528       if (decidable_equality address one_hundred_and_twenty_eight) then
     528      if (eq_n address one_hundred_and_twenty_eight) then
    529529        ?
    530       else if (decidable_equality address one_hundred_and_forty_four) then
     530      else if (eq_n address one_hundred_and_forty_four) then
    531531        if l then
    532532          (p1_latch s)
    533533        else
    534534          (get_8051_sfr s SFR_P1)
    535       else if (decidable_equality address one_hundred_and_sixty) then
     535      else if (eq_n address one_hundred_and_sixty) then
    536536        ?
    537       else if (decidable_equality address one_hundred_and_seventy_six) then
     537      else if (eq_n address one_hundred_and_seventy_six) then
    538538        if l then
    539539          (p3_latch s)
    540540        else
    541541          (get_8051_sfr s SFR_P3)
    542       else if (decidable_equality address one_hundred_and_fifty_three) then
     542      else if (eq_n address one_hundred_and_fifty_three) then
    543543        get_8051_sfr s SFR_SBUF
    544       else if (decidable_equality address one_hundred_and_thirty_eight) then
     544      else if (eq_n address one_hundred_and_thirty_eight) then
    545545        get_8051_sfr s SFR_TL0
    546       else if (decidable_equality address one_hundred_and_thirty_nine) then
     546      else if (eq_n address one_hundred_and_thirty_nine) then
    547547        get_8051_sfr s SFR_TL1
    548       else if (decidable_equality address one_hundred_and_forty) then
     548      else if (eq_n address one_hundred_and_forty) then
    549549        get_8051_sfr s SFR_TH0
    550       else if (decidable_equality address one_hundred_and_forty_one) then
     550      else if (eq_n address one_hundred_and_forty_one) then
    551551        get_8051_sfr s SFR_TH1
    552       else if (decidable_equality address two_hundred) then
     552      else if (eq_n address two_hundred) then
    553553        get_8052_sfr s SFR_T2CON
    554       else if (decidable_equality address two_hundred_and_two) then
     554      else if (eq_n address two_hundred_and_two) then
    555555        get_8052_sfr s SFR_RCAP2L
    556       else if (decidable_equality address two_hundred_and_three) then
     556      else if (eq_n address two_hundred_and_three) then
    557557        get_8052_sfr s SFR_RCAP2H
    558       else if (decidable_equality address two_hundred_and_four) then
     558      else if (eq_n address two_hundred_and_four) then
    559559        get_8052_sfr s SFR_TL2
    560       else if (decidable_equality address two_hundred_and_five) then
     560      else if (eq_n address two_hundred_and_five) then
    561561        get_8052_sfr s SFR_TH2
    562       else if (decidable_equality address one_hundred_and_thirty_five) then
     562      else if (eq_n address one_hundred_and_thirty_five) then
    563563        get_8051_sfr s SFR_PCON
    564       else if (decidable_equality address one_hundred_and_thirty_six) then
     564      else if (eq_n address one_hundred_and_thirty_six) then
    565565        get_8051_sfr s SFR_TCON
    566       else if (decidable_equality address one_hundred_and_thirty_seven) then
     566      else if (eq_n address one_hundred_and_thirty_seven) then
    567567        get_8051_sfr s SFR_TMOD
    568       else if (decidable_equality address one_hundred_and_fifty_two) then
     568      else if (eq_n address one_hundred_and_fifty_two) then
    569569        get_8051_sfr s SFR_SCON
    570       else if (decidable_equality address one_hundred_and_sixty_eight) then
     570      else if (eq_n address one_hundred_and_sixty_eight) then
    571571        get_8051_sfr s SFR_IE
    572       else if (decidable_equality address one_hundred_and_eighty_four) then
     572      else if (eq_n address one_hundred_and_eighty_four) then
    573573        get_8051_sfr s SFR_IP
    574       else if (decidable_equality address one_hundred_and_twenty_nine) then
     574      else if (eq_n address one_hundred_and_twenty_nine) then
    575575        get_8051_sfr s SFR_SP
    576       else if (decidable_equality address one_hundred_and_thirty) then
     576      else if (eq_n address one_hundred_and_thirty) then
    577577        get_8051_sfr s SFR_DPL
    578       else if (decidable_equality address one_hundred_and_thirty_one) then
     578      else if (eq_n address one_hundred_and_thirty_one) then
    579579        get_8051_sfr s SFR_DPH
    580       else if (decidable_equality address two_hundred_and_eight) then
     580      else if (eq_n address two_hundred_and_eight) then
    581581        get_8051_sfr s SFR_PSW
    582       else if (decidable_equality address two_hundred_and_twenty_four) then
     582      else if (eq_n address two_hundred_and_twenty_four) then
    583583        get_8051_sfr s SFR_ACC_A
    584       else if (decidable_equality address two_hundred_and_forty) then
     584      else if (eq_n address two_hundred_and_forty) then
    585585        get_8051_sfr s SFR_ACC_B
    586586      else
     
    594594  λv: Byte.
    595595    let address ≝ nat_of_bitvector … b in
    596       if (decidable_equality address one_hundred_and_twenty_eight) then
     596      if (eq_n address one_hundred_and_twenty_eight) then
    597597        ?
    598       else if (decidable_equality address one_hundred_and_forty_four) then
     598      else if (eq_n address one_hundred_and_forty_four) then
    599599        let status_1 ≝ set_8051_sfr s SFR_P1 v in
    600600        let status_2 ≝ set_p1_latch s v in
    601601          status_2
    602       else if (decidable_equality address one_hundred_and_sixty) then
     602      else if (eq_n address one_hundred_and_sixty) then
    603603        ?
    604       else if (decidable_equality address one_hundred_and_seventy_six) then
     604      else if (eq_n address one_hundred_and_seventy_six) then
    605605        let status_1 ≝ set_8051_sfr s SFR_P3 v in
    606606        let status_2 ≝ set_p3_latch s v in
    607607          status_2
    608       else if (decidable_equality address one_hundred_and_fifty_three) then
     608      else if (eq_n address one_hundred_and_fifty_three) then
    609609        set_8051_sfr s SFR_SBUF v
    610       else if (decidable_equality address one_hundred_and_thirty_eight) then
     610      else if (eq_n address one_hundred_and_thirty_eight) then
    611611        set_8051_sfr s SFR_TL0 v
    612       else if (decidable_equality address one_hundred_and_thirty_nine) then
     612      else if (eq_n address one_hundred_and_thirty_nine) then
    613613        set_8051_sfr s SFR_TL1 v
    614       else if (decidable_equality address one_hundred_and_forty) then
     614      else if (eq_n address one_hundred_and_forty) then
    615615        set_8051_sfr s SFR_TH0 v
    616       else if (decidable_equality address one_hundred_and_forty_one) then
     616      else if (eq_n address one_hundred_and_forty_one) then
    617617        set_8051_sfr s SFR_TH1 v
    618       else if (decidable_equality address two_hundred) then
     618      else if (eq_n address two_hundred) then
    619619        set_8052_sfr s SFR_T2CON v
    620       else if (decidable_equality address two_hundred_and_two) then
     620      else if (eq_n address two_hundred_and_two) then
    621621        set_8052_sfr s SFR_RCAP2L v
    622       else if (decidable_equality address two_hundred_and_three) then
     622      else if (eq_n address two_hundred_and_three) then
    623623        set_8052_sfr s SFR_RCAP2H v
    624       else if (decidable_equality address two_hundred_and_four) then
     624      else if (eq_n address two_hundred_and_four) then
    625625        set_8052_sfr s SFR_TL2 v
    626       else if (decidable_equality address two_hundred_and_five) then
     626      else if (eq_n address two_hundred_and_five) then
    627627        set_8052_sfr s SFR_TH2 v
    628       else if (decidable_equality address one_hundred_and_thirty_five) then
     628      else if (eq_n address one_hundred_and_thirty_five) then
    629629        set_8051_sfr s SFR_PCON v
    630       else if (decidable_equality address one_hundred_and_thirty_six) then
     630      else if (eq_n address one_hundred_and_thirty_six) then
    631631        set_8051_sfr s SFR_TCON v
    632       else if (decidable_equality address one_hundred_and_thirty_seven) then
     632      else if (eq_n address one_hundred_and_thirty_seven) then
    633633        set_8051_sfr s SFR_TMOD v
    634       else if (decidable_equality address one_hundred_and_fifty_two) then
     634      else if (eq_n address one_hundred_and_fifty_two) then
    635635        set_8051_sfr s SFR_SCON v
    636       else if (decidable_equality address one_hundred_and_sixty_eight) then
     636      else if (eq_n address one_hundred_and_sixty_eight) then
    637637        set_8051_sfr s SFR_IE v
    638       else if (decidable_equality address one_hundred_and_eighty_four) then
     638      else if (eq_n address one_hundred_and_eighty_four) then
    639639        set_8051_sfr s SFR_IP v
    640       else if (decidable_equality address one_hundred_and_twenty_nine) then
     640      else if (eq_n address one_hundred_and_twenty_nine) then
    641641        set_8051_sfr s SFR_SP v
    642       else if (decidable_equality address one_hundred_and_thirty) then
     642      else if (eq_n address one_hundred_and_thirty) then
    643643        set_8051_sfr s SFR_DPL v
    644       else if (decidable_equality address one_hundred_and_thirty_one) then
     644      else if (eq_n address one_hundred_and_thirty_one) then
    645645        set_8051_sfr s SFR_DPH v
    646       else if (decidable_equality address two_hundred_and_eight) then
     646      else if (eq_n address two_hundred_and_eight) then
    647647        set_8051_sfr s SFR_PSW v
    648       else if (decidable_equality address two_hundred_and_twenty_four) then
     648      else if (eq_n address two_hundred_and_twenty_four) then
    649649        set_8051_sfr s SFR_ACC_A v
    650       else if (decidable_equality address two_hundred_and_forty) then
     650      else if (eq_n address two_hundred_and_forty) then
    651651        set_8051_sfr s SFR_ACC_B v
    652652      else
     
    996996
    997997ndefinition load_code_memory ≝
    998  fold_lefti … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
     998 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
    999999
    10001000ndefinition load ≝
Note: See TracChangeset for help on using the changeset viewer.