Changeset 351 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Dec 1, 2010, 4:30:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r350 r351 103 103 }. 104 104 105 n axiomsfr8051_index_nineteen:105 nlemma sfr8051_index_nineteen: 106 106 ∀i: SFR8051. 107 107 sfr_8051_index i < nineteen. 108 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); 109 napply less_than_or_equal_zero. 110 nqed. 108 111 109 n axiomsfr8052_index_five:112 nlemma sfr8052_index_five: 110 113 ∀i: SFR8052. 111 114 sfr_8052_index i < five. 115 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); 116 napply less_than_or_equal_zero. 117 nqed. 112 118 113 119 ndefinition set_clock ≝ … … 180 186 old_clock. 181 187 182 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".183 188 ndefinition get_8051_sfr ≝ 184 189 λs: Status. … … 186 191 let sfr ≝ special_function_registers_8051 s in 187 192 let index ≝ sfr_8051_index i in 188 get_index …sfr index ?.193 get_index ?? sfr index ?. 189 194 napply (sfr8051_index_nineteen i). 190 195 nqed. … … 195 200 let sfr ≝ special_function_registers_8052 s in 196 201 let index ≝ sfr_8052_index i in 197 get_index …sfr index ?.202 get_index ?? sfr index ?. 198 203 napply (sfr8052_index_five i). 199 204 nqed. … … 212 217 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 213 218 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 ? in219 set_index Byte nineteen old_special_function_registers_8051 index b ? in 215 220 let old_p1_latch ≝ p1_latch s in 216 221 let old_p3_latch ≝ p3_latch s in … … 242 247 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 243 248 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 ? in249 set_index Byte five old_special_function_registers_8052 index b ? in 245 250 let old_p1_latch ≝ p1_latch s in 246 251 let old_p3_latch ≝ p3_latch s in … … 374 379 old_p3_latch 375 380 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)".382 381 383 382 ndefinition get_cy_flag ≝ … … 887 886 nqed. 888 887 889 naxiom modulus_less_than: 890 ∀m,n: Nat. 891 (m mod n) < n. 888 ntheorem 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/] 902 nqed. 892 903 893 904 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → … … 991 1002 napply less_than_or_equal_zero; 992 1003 ####4,5: 993 napply (modulus_less_than address eight);1004 napply modulus_less_than; 994 1005 ##] 995 1006 nqed.
Note: See TracChangeset
for help on using the changeset viewer.