Changeset 1518
 Timestamp:
 Nov 21, 2011, 11:15:06 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1516 r1518 1014 1014 @ le_O_n 1015 1015 1,2,4,5: 1016 applymodulus_less_than1016 @modulus_less_than 1017 1017 ] 1018 1018 qed. … … 1086 1086 lemma snd_fetch_pseudo_instruction: 1087 1087 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)). 1088 #l #ppc whd in ⊢ (??%?) whd in ⊢ (?? match % with [_ ⇒ ?]?)@pair_elim'1088 #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim' 1089 1089 #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H 1090 generalize in match (pair_destruct_2 ????? H) normalize #K >K %1090 generalize in match (pair_destruct_2 ????? H); normalize #K >K % 1091 1091 qed. 1092 1092 … … 1109 1109 does_not_occur id list_instr. 1110 1110 #id #i #list_instr elim list_instr 1111 [ %  #hd #tl #IH whd in ⊢ (??%%) >IH %]1111 [ %  #hd #tl #IH whd in ⊢ (??%%); >IH %] 1112 1112 qed. 1113 1113 … … 1119 1119 #id #id' #i #list_instr elim list_instr 1120 1120 [ #H normalize in H ⊢ %; >H % 1121  * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]1121  * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %] 1122 1122 qed. 1123 1123 … … 1128 1128 [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?) 1129 1129 >eq_identifier_refl % 1130  * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]1130  * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %] 1131 1131 qed. 1132 1132 … … 1146 1146 occurs_exactly_once id list_instr. 1147 1147 #id #i #list_instr elim list_instr 1148 [ %  #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]1148 [ %  #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %] 1149 1149 qed. 1150 1150 … … 1153 1153 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix. 1154 1154 #id #id' #i #prefix elim prefix 1155 [ whd in ⊢ (?% → ?) 1156 change in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) with (eq_identifier ? id' id)1155 [ whd in ⊢ (?% → ?); 1156 change in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?); with (eq_identifier ? id' id); 1157 1157 @eq_identifier_elim normalize nodelta; /2/ 1158  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?)1158  *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?); 1159 1159 cases he; normalize nodelta 1160 1160 [ #H @ (IH H) 1161  #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??)with (eq_identifier ? x id)1161  #x whd in ⊢ (? → ?(??%)); change in match (instruction_matches_identifier ??); with (eq_identifier ? x id) 1162 1162 @eq_identifier_elim #E normalize nodelta 1163 1163 [ destruct @eq_identifier_elim normalize nodelta; … … 1172 1172 (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix). 1173 1173 #id #id' #i #prefix elim prefix 1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ? _ ⇒ ?]) → ?)with (eq_identifier ???)1174 [ whd in ⊢ (?% → ?); change in ⊢ (?(match % with [_ ⇒ ? _ ⇒ ?]) → ?); with (eq_identifier ???) 1175 1175 @eq_identifier_elim #E 1176 1176 [ normalize // 1177 1177  normalize #H @⊥ @H 1178 1178 ] 1179  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?)1179  *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?); 1180 1180 cases he; normalize nodelta 1181 1181 [ #H @ (IH H) … … 1184 1184 [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf 1185 1185  #H >(does_not_occur_Some) 1186 [ #H2 whd in match (does_not_occur ??) 1187 change in match (instruction_matches_identifier ??) with (eq_identifier ???)1186 [ #H2 whd in match (does_not_occur ??); 1187 change in match (instruction_matches_identifier ??); with (eq_identifier ???) 1188 1188 >Heq >eq_identifier_refl normalize nodelta 1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) 1190 change in match (instruction_matches_identifier ??) with (eq_identifier ???)1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??); 1190 change in match (instruction_matches_identifier ??); with (eq_identifier ???) 1191 1191 >eq_identifier_refl 1192 1192 normalize nodelta @H2 … … 1198 1198 #Hor @orb_elim 1199 1199 [ <Heq2 in Hor; #Hor normalize in Hor; 1200 whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??)with (eq_identifier ???)1200 whd in match (does_not_occur ??); change in match (instruction_matches_identifier ??); with (eq_identifier ???) 1201 1201 >eq_identifier_false // normalize nodelta 1202 1202 cases (does_not_occur id' tl) in Hor; normalize nodelta // 1203  normalize nodelta whd in match (occurs_exactly_once ??) 1204 change in match (instruction_matches_identifier ??) with (eq_identifier ???)1203  normalize nodelta whd in match (occurs_exactly_once ??); 1204 change in match (instruction_matches_identifier ??); with (eq_identifier ???) 1205 1205 >eq_identifier_false // 1206 1206 ] … … 1235 1235 #i #id #instr_list elim instr_list 1236 1236 [ #n #abs whd in abs; cases abs 1237  #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ?) 1238 cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ??%%) 1237  #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ?); 1238 cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ??%%); 1239 1239 [ #H % 1240  #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ % 1240  #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %; 1241 1241 [ #_ %  #abs cases abs ]]] 1242 1242 qed. … … 1249 1249 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n. 1250 1250 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ 1251 change with (occurs_exactly_once ?? → ?) generalize in match n; n H; elim instr_list1251 change with (occurs_exactly_once ?? → ?) generalize in match n; n H; elim instr_list 1252 1252 [ #n #abs cases abs 1253  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;1253  #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta; 1254 1254 [ //  #K @IH //]] 1255 1255 qed. … … 1261 1261 = instr_list + n. 1262 1262 #i #id #instr_list elim instr_list 1263 [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %1264  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;1263 [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl % 1264  #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta; 1265 1265 [ >does_not_occur_absurd #abs cases abs  #H >plus_n_Sm applyS (IH (S n)) //]] 1266 1266 qed. … … 1275 1275 address_of_word_labels_code_mem instr_list id = 1276 1276 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 1277 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))1277 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 1278 1278 >(index_of_internal_None … H) % 1279 1279 qed. … … 1284 1284 address_of_word_labels_code_mem instr_list id = 1285 1285 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 1286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))1286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 1287 1287 >(index_of_internal_Some_miss … H) [ @refl  // ] 1288 1288 qed. … … 1292 1292 address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id 1293 1293 = bitvector_of_nat … (instr_list). 1294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)1294 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?); 1295 1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl 1296 1296 qed.
Note: See TracChangeset
for help on using the changeset viewer.