Changeset 363
 Timestamp:
 Dec 2, 2010, 2:03:48 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r362 r363 19 19 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 20 20 (get_arg_8 s false addr2) false in 21 let cy_flag ≝ get_index _v … flags Z ?in22 let ac_flag ≝ get_index _v … flags one ?in23 let ov_flag ≝ get_index _v … flags two ?in21 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 24 24 let s ≝ set_arg_8 s ACC_A result in 25 25 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 28 28 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 29 29 (get_arg_8 s false addr2) old_cy_flag in 30 let cy_flag ≝ get_index _v … flags Z ?in31 let ac_flag ≝ get_index _v … flags one ?in32 let ov_flag ≝ get_index _v … flags two ?in30 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 33 33 let s ≝ set_arg_8 s ACC_A result in 34 34 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 37 37 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1) 38 38 (get_arg_8 s false addr2) old_cy_flag in 39 let cy_flag ≝ get_index _v … flags Z ?in40 let ac_flag ≝ get_index _v … flags one ?in41 let ov_flag ≝ get_index _v … flags two ?in39 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 42 42 let s ≝ set_arg_8 s ACC_A result in 43 43 set_flags s cy_flag (Just Bit ac_flag) ov_flag … … 142 142 if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then 143 143 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 ?in144 let cy_flag ≝ get_index' ? Z ? flags in 145 145 let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in 146 146 if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then … … 188 188 let old_cy_flag ≝ get_cy_flag s in 189 189 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 190 let new_cy_flag ≝ get_index _v … old_acc Z ?in191 let new_acc ≝ shift_left …eight one old_acc old_cy_flag in190 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 192 192 let s ≝ set_arg_1 s CARRY new_cy_flag in 193 193 set_8051_sfr s SFR_ACC_A new_acc … … 195 195 let old_cy_flag ≝ get_cy_flag s in 196 196 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 197 let new_cy_flag ≝ get_index _v … old_acc seven ?in198 let new_acc ≝ shift_right …eight one old_acc old_cy_flag in197 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 199 199 let s ≝ set_arg_1 s CARRY new_cy_flag in 200 200 set_8051_sfr s SFR_ACC_A new_acc … … 384 384 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in 385 385 let 〈nu, nl〉 ≝ split ? four four pc_bu in 386 let bit ≝ get_index _v … nl Z ?in386 let bit ≝ get_index' ? Z ? nl in 387 387 let 〈relevant1, relevant2〉 ≝ split ? three eight a in 388 388 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in … … 486 486 in 487 487 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 ## 489 503 nqed. 490 504 
Deliverables/D4.1/Matita/Nat.ma
r357 r363 653 653 P (greater_than_b m n). 654 654 #m n; napply less_than_b_elim. 655 nqed. 656 657 nlemma 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/. 655 666 nqed. 656 667 
Deliverables/D4.1/Matita/Vector.ma
r362 r363 58 58 nqed. 59 59 60 ndefinition 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; 68 nqed. 69 60 70 nlet 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 ≝ 62 72 match m with 63 73 [ Z ⇒
Note: See TracChangeset
for help on using the changeset viewer.