Changeset 977
 Timestamp:
 Jun 16, 2011, 12:12:59 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r975 r977 1074 1074 qed. 1075 1075 1076 lemma index_of_internal_Some_hit: ∀i,id. 1077 ∀instr_list,n. 1078 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) → 1079 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n 1080 = instr_list + n. 1081 #i #id #instr_list elim instr_list 1082 [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl % 1083  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta; 1084 [ >does_not_occur_absurd #abs cases abs  #H applyS (IH (S n)) //]] 1085 qed. 1086 1076 1087 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list. 1077 1088 occurs_exactly_once id (instr_list@[〈None …,i〉]) → … … 1089 1100 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 1090 1101 >(index_of_internal_Some_miss … H) // 1102 qed. 1103 1104 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list. 1105 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) → 1106 address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id 1107 = bitvector_of_nat … (instr_list). 1108 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?) 1109 >(index_of_internal_Some_hit … H) // 1091 1110 qed. 1092 1111 … … 1120 1139 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 1121 1140 let 〈pc',costs〉 ≝ pc_costs in 1141 ppc' = length … pre ∧ 1122 1142 tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧ 1123 1143 ∀id. occurs_exactly_once id pre → … … 1149 1169 let 〈pc, costs〉 ≝ pc_costs in 1150 1170 〈labels, costs〉. 1151 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ // 1152  whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 1153 cases construct in p4 #PC #CODE #JMEQ % 1154 [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ)) 1171 [3: whd % [%] // #id normalize in ⊢ (% → ?) #abs @⊥ // 1172  whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * #IH0 #IH1 #IH2 1173 cases construct in p4 #PC #CODE #JMEQ % [%] 1174 [ >length_append <IH0 normalize; // 1175  @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ)) 1155 1176  #id normalize nodelta; labels1; cases label; normalize nodelta 1156 1177 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 // 1157 1178  #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 1158 1179 generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %) 1159 [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit 1160 1180 [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 1181 <IH0 1161 1182  #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/] 1162 1183 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]] 1163  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * ;#IH1 #IH21184  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 1164 1185 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ] 1165 1186 qed.
Note: See TracChangeset
for help on using the changeset viewer.