Changeset 1882 for src/ASM/Status.ma
- Timestamp:
- Apr 6, 2012, 8:02:10 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Status.ma
r1666 r1882 510 510 λac: option Bit. 511 511 λov: Bit. 512 let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in 513 let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in 514 let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in 515 let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in 516 let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in 517 let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in 518 let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in 519 let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in 512 let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in 513 let old_cy ≝ get_index_v ?? sfr_psw O ? in 514 let old_ac ≝ get_index_v ?? sfr_psw 1 ? in 515 let old_fo ≝ get_index_v ?? sfr_psw 2 ? in 516 let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in 517 let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in 518 let old_ov ≝ get_index_v ?? sfr_psw 5 ? in 519 let old_ud ≝ get_index_v ?? sfr_psw 6 ? in 520 let old_p ≝ get_index_v ?? sfr_psw 7 ? in 520 521 let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in 521 522 set_8051_sfr ?? s SFR_PSW … … 1128 1129 qed. 1129 1130 1130 definition instruction_matches_identifier ≝1131 λy: Identifier.1132 λx: labelled_instruction.1133 match \fst x with1134 [ None ⇒ false1135 | Some x ⇒ eq_identifier ? x y1136 ].1137 1138 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝1139 match l with1140 [ nil ⇒ true1141 | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].1142 1143 lemma does_not_occur_None:1144 ∀id,i,list_instr.1145 does_not_occur id (list_instr@[〈None …,i〉]) =1146 does_not_occur id list_instr.1147 #id #i #list_instr elim list_instr1148 [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]1149 qed.1150 1151 lemma does_not_occur_Some:1152 ∀id,id',i,list_instr.1153 eq_identifier ? id' id = false →1154 does_not_occur id (list_instr@[〈Some ? id',i〉]) =1155 does_not_occur id list_instr.1156 #id #id' #i #list_instr elim list_instr1157 [ #H normalize in H ⊢ %; >H %1158 | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]1159 qed.1160 1161 lemma does_not_occur_absurd:1162 ∀id,i,list_instr.1163 does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.1164 #id #i #list_instr elim list_instr1165 [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)1166 >eq_identifier_refl %1167 | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]1168 qed.1169 1170 1171 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝1172 match l with1173 [ nil ⇒ false1174 | cons hd tl ⇒1175 if instruction_matches_identifier id hd then1176 does_not_occur id tl1177 else1178 occurs_exactly_once id tl ].1179 1180 lemma occurs_exactly_once_None:1181 ∀id,i,list_instr.1182 occurs_exactly_once id (list_instr@[〈None …,i〉]) =1183 occurs_exactly_once id list_instr.1184 #id #i #list_instr elim list_instr1185 [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]1186 qed.1187 1188 lemma occurs_exactly_once_Some:1189 ∀id,id',i,prefix.1190 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.1191 #id #id' #i #prefix elim prefix1192 [ whd in ⊢ (?% → ?);1193 change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);1194 @eq_identifier_elim normalize nodelta; /2/1195 | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);1196 cases he; normalize nodelta1197 [ #H @ (IH H)1198 | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);1199 @eq_identifier_elim #E normalize nodelta1200 [ destruct @eq_identifier_elim normalize nodelta;1201 /2/ #H >does_not_occur_Some /2/1202 | #H @IH @H]]]1203 qed.1204 1205 lemma occurs_exactly_once_Some_stronger:1206 ∀id,id',i,prefix.1207 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →1208 (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨1209 (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).1210 #id #id' #i #prefix elim prefix1211 [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);1212 @eq_identifier_elim #E1213 [ normalize //1214 | normalize #H @⊥ @H1215 ]1216 | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);1217 cases he; normalize nodelta1218 [ #H @ (IH H)1219 | #x @eq_identifier_elim #Heq1220 [ @eq_identifier_elim normalize nodelta1221 [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf1222 | #H >(does_not_occur_Some)1223 [ #H2 whd in match (does_not_occur ??);1224 change with (eq_identifier ???) in match (instruction_matches_identifier ??);1225 >Heq >eq_identifier_refl normalize nodelta1226 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);1227 change with (eq_identifier ???) in match (instruction_matches_identifier ??);1228 >eq_identifier_refl1229 normalize nodelta @H21230 | /2/1231 ]1232 ]1233 | normalize nodelta #H lapply (IH H) -IH -H;1234 @eq_identifier_elim #Heq21235 #Hor @orb_elim1236 [ <Heq2 in Hor; #Hor normalize in Hor;1237 whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);1238 >eq_identifier_false // normalize nodelta1239 cases (does_not_occur id' tl) in Hor; normalize nodelta //1240 | normalize nodelta whd in match (occurs_exactly_once ??);1241 change with (eq_identifier ???) in match (instruction_matches_identifier ??);1242 >eq_identifier_false //1243 ]1244 ]1245 ]1246 ]1247 qed.1248 1249 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝1250 match l with1251 [ nil ⇒ ?1252 | cons hd tl ⇒1253 if pred hd then1254 acc1255 else1256 index_of_internal A pred tl (S acc)1257 ].1258 cases not_implemented.1259 qed.1260 1261 1262 definition index_of ≝1263 λA.1264 λeq.1265 λl.1266 index_of_internal A eq l 0.1267 1268 lemma index_of_internal_None: ∀i,id,instr_list,n.1269 occurs_exactly_once id (instr_list@[〈None …,i〉]) →1270 index_of_internal ? (instruction_matches_identifier id) instr_list n =1271 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.1272 #i #id #instr_list elim instr_list1273 [ #n #abs whd in abs; cases abs1274 | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);1275 cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);1276 [ #H %1277 | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;1278 [ #_ % | #abs cases abs ]]]1279 qed.1280 1281 lemma index_of_internal_Some_miss: ∀i,id,id'.1282 eq_identifier ? id' id = false →1283 ∀instr_list,n.1284 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →1285 index_of_internal ? (instruction_matches_identifier id) instr_list n =1286 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.1287 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ1288 change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list1289 [ #n #abs cases abs1290 | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;1291 [ // | #K @IH //]]1292 qed.1293 1294 lemma index_of_internal_Some_hit: ∀i,id.1295 ∀instr_list,n.1296 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →1297 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n1298 = |instr_list| + n.1299 #i #id #instr_list elim instr_list1300 [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %1301 | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;1302 [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]1303 qed.1304 1305 1131 definition address_of_word_labels_code_mem ≝ 1306 λcode_mem .1132 λcode_mem : list labelled_instruction. 1307 1133 λid: Identifier. 1308 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).1134 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem). 1309 1135 1310 1136 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list. 1311 occurs_exactly_once id (instr_list@[〈None …,i〉]) →1137 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) → 1312 1138 address_of_word_labels_code_mem instr_list id = 1313 1139 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 1314 1140 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 1315 >(index_of_internal_None …H) %1141 >(index_of_internal_None ?????? H) % 1316 1142 qed. 1317 1143 1318 1144 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list. 1319 1145 eq_identifier ? id' id = false → 1320 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →1146 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) → 1321 1147 address_of_word_labels_code_mem instr_list id = 1322 1148 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 1323 1149 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 1324 >(index_of_internal_Some_miss …H) [ @refl | // ]1150 >(index_of_internal_Some_miss ???????? H) [ @refl | // ] 1325 1151 qed. 1326 1152 1327 1153 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list. 1328 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →1154 occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) → 1329 1155 address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id 1330 1156 = bitvector_of_nat … (|instr_list|). 1331 1157 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?); 1332 >(index_of_internal_Some_hit …H) <plus_n_O @refl1158 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl 1333 1159 qed. 1334 1160
Note: See TracChangeset
for help on using the changeset viewer.