Changeset 265 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 23, 2010, 5:05:46 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r259 r265 85 85 }. 86 86 87 alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)". 87 ncheck special_function_registers_8051. 88 89 naxiom sfr8051_index_nineteen: 90 ∀i: SFR8051. 91 sfr_8051_index i < nineteen. 92 93 naxiom sfr8052_index_five: 94 ∀i: SFR8052. 95 sfr_8052_index i < five. 96 97 ndefinition get_8051_sfr ≝ 98 λs: Status. 99 λi: SFR8051. 100 let sfr ≝ special_function_registers_8051 s in 101 let index ≝ sfr_8051_index i in 102 get_index … sfr index ?. 103 napply (sfr8051_index_nineteen i). 104 nqed. 105 106 ndefinition get_8052_sfr ≝ 107 λs: Status. 108 λi: SFR8052. 109 let sfr ≝ special_function_registers_8052 s in 110 let index ≝ sfr_8052_index i in 111 get_index … sfr index ?. 112 napply (sfr8052_index_five i). 113 nqed. 88 114 89 115 ndefinition set_8051_sfr ≝ … … 91 117 λi: SFR8051. 92 118 λb: Byte. 93 let index ≝ sfr_8051_status i in 94 let 119 let index ≝ sfr_8051_index i in 120 let old_code_memory ≝ code_memory s in 121 let old_low_internal_ram ≝ low_internal_ram s in 122 let old_high_internal_ram ≝ high_internal_ram s in 123 let old_external_ram ≝ external_ram s in 124 let old_program_counter ≝ program_counter s in 125 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 126 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 127 let new_special_function_registers_8051 ≝ 128 cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in 129 mk_Status old_code_memory 130 old_low_internal_ram 131 old_high_internal_ram 132 old_external_ram 133 old_program_counter 134 new_special_function_registers_8051 135 old_special_function_registers_8052. 136 napply (sfr8051_index_nineteen i). 137 nqed. 138 139 ndefinition set_8052_sfr ≝ 140 λs: Status. 141 λi: SFR8052. 142 λb: Byte. 143 let index ≝ sfr_8052_index i in 144 let old_code_memory ≝ code_memory s in 145 let old_low_internal_ram ≝ low_internal_ram s in 146 let old_high_internal_ram ≝ high_internal_ram s in 147 let old_external_ram ≝ external_ram s in 148 let old_program_counter ≝ program_counter s in 149 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 150 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 151 let new_special_function_registers_8052 ≝ 152 cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in 153 mk_Status old_code_memory 154 old_low_internal_ram 155 old_high_internal_ram 156 old_external_ram 157 old_program_counter 158 old_special_function_registers_8051 159 new_special_function_registers_8052. 160 napply (sfr8052_index_five i). 161 nqed. 162 163 ndefinition set_program_counter ≝ 164 λs: Status. 165 λi: SFR8052. 166 λw: Word. 167 let index ≝ sfr_8052_index i in 168 let old_code_memory ≝ code_memory s in 169 let old_low_internal_ram ≝ low_internal_ram s in 170 let old_high_internal_ram ≝ high_internal_ram s in 171 let old_external_ram ≝ external_ram s in 172 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 173 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 174 mk_Status old_code_memory 175 old_low_internal_ram 176 old_high_internal_ram 177 old_external_ram 178 w 179 old_special_function_registers_8051 180 old_special_function_registers_8052. 181 182 ndefinition set_code_memory ≝ 183 λs: Status. 184 λi: SFR8052. 185 λr: BitVectorTrie Byte sixteen. 186 let index ≝ sfr_8052_index i in 187 let old_low_internal_ram ≝ low_internal_ram s in 188 let old_high_internal_ram ≝ high_internal_ram s in 189 let old_external_ram ≝ external_ram s in 190 let old_program_counter ≝ program_counter s in 191 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 192 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 193 mk_Status r 194 old_low_internal_ram 195 old_high_internal_ram 196 old_external_ram 197 old_program_counter 198 old_special_function_registers_8051 199 old_special_function_registers_8052. 200 201 ndefinition set_low_internal_ram ≝ 202 λs: Status. 203 λi: SFR8052. 204 λr: BitVectorTrie Byte seven. 205 let index ≝ sfr_8052_index i in 206 let old_code_memory ≝ code_memory s in 207 let old_high_internal_ram ≝ high_internal_ram s in 208 let old_external_ram ≝ external_ram s in 209 let old_program_counter ≝ program_counter s in 210 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 211 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 212 mk_Status old_code_memory 213 r 214 old_high_internal_ram 215 old_external_ram 216 old_program_counter 217 old_special_function_registers_8051 218 old_special_function_registers_8052. 219 220 ndefinition get_cy_flag ≝ 221 λs: Status. 222 let sfr ≝ special_function_registers_8051 s in 223 let psw ≝ get_index … (get_8051_index SFR_PSW) s ? in 224 get_index … Z psw ?. 225 226 ndefinition set_high_internal_ram ≝ 227 λs: Status. 228 λi: SFR8052. 229 λr: BitVectorTrie Byte seven. 230 let index ≝ sfr_8052_index i in 231 let old_code_memory ≝ code_memory s in 232 let old_low_internal_ram ≝ low_internal_ram s in 233 let old_high_internal_ram ≝ high_internal_ram s in 234 let old_external_ram ≝ external_ram s in 235 let old_program_counter ≝ program_counter s in 236 let old_special_function_registers_8051 ≝ special_function_registers_8051 s in 237 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 238 mk_Status old_code_memory 239 old_low_internal_ram 240 r 241 old_external_ram 242 old_program_counter 243 old_special_function_registers_8051 244 old_special_function_registers_8052. 95 245 96 246 ndefinition initialise_status ≝ 
Deliverables/D4.1/Matita/Nat.ma
r261 r265 57 57 (* Add Boolean versions. *) 58 58 ndefinition less_than_p ≝ 59 λm, n: Nat. 60 m ≤ n ∧ ¬(m = n). 59 λm: Nat. 60 λn: Nat. 61 less_than_or_equal_p (S m) n. 61 62 62 63 notation "hvbox(n break < m)" 
Deliverables/D4.1/Matita/Vector.ma
r262 r265 40 40 naxiom succ_less_than_injective: 41 41 ∀m, n: Nat. 42 S m < S n→ m < n.42 less_than_p (S m) (S n) → m < n. 43 43 44 44 naxiom nothing_less_than_Z:
Note: See TracChangeset
for help on using the changeset viewer.