Changeset 363 for Deliverables


Ignore:
Timestamp:
Dec 2, 2010, 2:03:48 PM (9 years ago)
Author:
mulligan
Message:

Resolved conflicts. Added new get_index' which hides the proof obligation of get_index_v. Needed a new lemma to typecheck it.

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

Legend:

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

    r362 r363  
    1919            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2020                                                   (get_arg_8 s false addr2) false in
    21             let cy_flag ≝ get_index_v … flags Z ? in
    22             let ac_flag ≝ get_index_v … flags one ? in
    23             let ov_flag ≝ get_index_v … flags two ? in
     21            let cy_flag ≝ get_index' ? Z  ? flags in
     22            let ac_flag ≝ get_index' ? one ? flags in
     23            let ov_flag ≝ get_index' ? two ? flags in
    2424            let s ≝ set_arg_8 s ACC_A result in
    2525              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    2828            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2929                                                   (get_arg_8 s false addr2) old_cy_flag in
    30             let cy_flag ≝ get_index_v … flags Z ? in
    31             let ac_flag ≝ get_index_v … flags one ? in
    32             let ov_flag ≝ get_index_v … flags two ? in
     30            let cy_flag ≝ get_index' ? Z ? flags in
     31            let ac_flag ≝ get_index' ? one ? flags in
     32            let ov_flag ≝ get_index' ? two ? flags in
    3333            let s ≝ set_arg_8 s ACC_A result in
    3434              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    3737            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
    3838                                                   (get_arg_8 s false addr2) old_cy_flag in
    39             let cy_flag ≝ get_index_v … flags Z ? in
    40             let ac_flag ≝ get_index_v … flags one ? in
    41             let ov_flag ≝ get_index_v … flags two ? in
     39            let cy_flag ≝ get_index' ? Z ? flags in
     40            let ac_flag ≝ get_index' ? one ? flags in
     41            let ov_flag ≝ get_index' ? two ? flags in
    4242            let s ≝ set_arg_8 s ACC_A result in
    4343              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    142142              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
    143143                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
    144                 let cy_flag ≝ get_index_v … flags Z ? in
     144                let cy_flag ≝ get_index' ? Z ? flags in
    145145                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
    146146                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
     
    188188            let old_cy_flag ≝ get_cy_flag s in
    189189            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    190             let new_cy_flag ≝ get_index_v … old_acc Z ? in
    191             let new_acc ≝ shift_left … eight one old_acc old_cy_flag in
     190            let new_cy_flag ≝ get_index' ? Z ? old_acc in
     191            let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
    192192            let s ≝ set_arg_1 s CARRY new_cy_flag in
    193193              set_8051_sfr s SFR_ACC_A new_acc
     
    195195            let old_cy_flag ≝ get_cy_flag s in
    196196            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    197             let new_cy_flag ≝ get_index_v … old_acc seven ? in
    198             let new_acc ≝ shift_right … eight one old_acc old_cy_flag in
     197            let new_cy_flag ≝ get_index' ? seven ? old_acc in
     198            let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
    199199            let s ≝ set_arg_1 s CARRY new_cy_flag in
    200200              set_8051_sfr s SFR_ACC_A new_acc
     
    384384              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    385385              let 〈nu, nl〉 ≝ split ? four four pc_bu in
    386               let bit ≝ get_index_v … nl Z ? in
     386              let bit ≝ get_index' ? Z ? nl in
    387387              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
    388388              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     
    486486    in
    487487      s.
    488     ncases daemon;
     488    ##[##2,3,4,8,9,10,14,15,16,43,104,106:
     489         nnormalize;
     490         nrepeat (napply (less_than_or_equal_monotone));
     491         napply (less_than_or_equal_zero);
     492    ##|##23,28,29,30,31,32,33,34,35,36,37,38,39,40,64,65,66,
     493         67,68,69,70,71,72,73,74,75,76,79,80,81,82,117,118,119,
     494         120,121,122,123,124,125,126,127,128,129,130,131,132,
     495         133,139,140,141,142,143,144,145,146,147,148,149,150,
     496         151,152,153,154,155,156,162,163,164,165,166,167,168,
     497         169,170,171,172,173,174,175,176,177,178,179,180,181,
     498         182,183,184,185,186,187,188,189,190,191,192,193,194,
     499         195,196,197,198,199,200,201,202,203,204,205,206,207,
     500         208,209,210,211,212,213:
     501           nassumption;
     502    ##|
    489503nqed.
    490504
  • Deliverables/D4.1/Matita/Nat.ma

    r357 r363  
    653653  P (greater_than_b m n).
    654654 #m n; napply less_than_b_elim.
     655nqed.
     656
     657nlemma less_than_or_equal_plus:
     658  ∀n,m: Nat.
     659    n ≤ n + m.
     660  #n m.
     661  nelim n.
     662  //.
     663  #N H.
     664  napply (less_than_or_equal_monotone).
     665  /2/.
    655666nqed.
    656667
  • Deliverables/D4.1/Matita/Vector.ma

    r362 r363  
    5858nqed.
    5959
     60ndefinition get_index' ≝
     61  λA: Type[0].
     62  λn, m: Nat.
     63  λb: Vector A (S (n + m)).
     64    get_index_v A (S (n + m)) b n ?.
     65  nnormalize;
     66  napply less_than_or_equal_monotone;
     67  napply less_than_or_equal_plus;
     68nqed.
     69
    6070nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    61                    (v: Vector A n) (m: Nat) on m ≝
     71                          (v: Vector A n) (m: Nat) on m ≝
    6272  match m with
    6373    [ Z ⇒
Note: See TracChangeset for help on using the changeset viewer.