Changeset 3550
- Timestamp:
- Apr 8, 2015, 7:53:48 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Lang_meas.ma
r3549 r3550 163 163 #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta 164 164 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct 165 | cases daemon 166 | cases daemon 165 | #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2 166 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta 167 [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 168 [1,2,3,4,6,7: 169 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 170 | #lin #io #lout #instr #_ ] 171 #_ whd in ⊢ (??%% → ?); 172 [ | 173 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 174 | cases(call_post_clean ?????); normalize nodelta 175 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 176 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 177 [| #z cases(?∧?) normalize nodelta 178 ] 179 ] 180 ] 181 | cases(call_post_clean ?????) normalize nodelta 182 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 183 [ cases (?==?) normalize nodelta ] 184 ]] 185 | cases(call_post_clean ?????) normalize nodelta 186 [| #x cases(? ∧ ?) normalize nodelta ] 187 ] 188 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 189 ] 190 #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 191 cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false'' 192 cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind 193 cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 194 #_ #_ #EQ destruct % // * #f * #lab #EQ destruct 195 | #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2 196 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta 197 [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 198 [1,2,3,4,6,7: 199 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 200 | #lin #io #lout #instr #_ ] 201 #_ whd in ⊢ (??%% → ?); 202 [ | 203 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 204 | cases(call_post_clean ?????); normalize nodelta 205 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 206 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 207 [| #z cases(?∧?) normalize nodelta 208 ] 209 ] 210 ] 211 | cases(call_post_clean ?????) normalize nodelta 212 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 213 [ cases (?==?) normalize nodelta ] 214 ]] 215 | cases(call_post_clean ?????) normalize nodelta 216 [| #x cases(? ∧ ?) normalize nodelta ] 217 ] 218 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 219 ] 220 #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 221 cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false'' 222 cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind 223 cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 224 #_ #_ #EQ destruct % // * #f * #lab #EQ destruct 167 225 | #s1 #s2 #lin #io #lout #instr #men #EQcode #EQeval #EQcodes2 #EQcont_s2 #EQ destruct #Hio * whd in match state_rel; 168 226 normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] ** 169 227 #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode inversion(code ? s1') 170 [1,2,3,4,5,6: cases daemon (* ASSURDI*) 228 [1,2,3,4,5,6: 229 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 230 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ] 231 #_ whd in ⊢ (??%% → ?); 232 [ | 233 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 234 | cases(call_post_clean ?????); normalize nodelta 235 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 236 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 237 [| #z cases(?∧?) normalize nodelta 238 ] 239 ] 240 ] 241 | cases(call_post_clean ?????) normalize nodelta 242 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 243 [| #y cases(?∧?) normalize nodelta 244 ] 245 ] 246 | cases(call_post_clean ?????) normalize nodelta 247 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 248 [ cases (?==?) normalize nodelta ] 249 ]] 250 ] 251 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 171 252 | #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta 172 253 [ #EQ destruct] #x … … 177 258 whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] ** 178 259 #H1 #a_top #a_tail normalize nodelta #Hcall **** #HH1 >EQcode inversion(code ? s1') 179 [1,2,3,4,5,7: cases daemon (* ASSURDI*) 260 [1,2,3,4,5,7: 261 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 262 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_ ] 263 #_ whd in ⊢ (??%% → ?); 264 [ | 265 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 266 | cases(call_post_clean ?????); normalize nodelta 267 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 268 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 269 [| #z cases(?∧?) normalize nodelta 270 ] 271 ] 272 ] 273 | cases(call_post_clean ?????) normalize nodelta 274 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 275 [| #y cases(?∧?) normalize nodelta 276 ] 277 ] 278 | cases(call_post_clean ?????) normalize nodelta 279 [| #x cases(? ∧ ?) normalize nodelta ] 280 ] 281 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 180 282 |*: #f' #act_p' #lbl' #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta 181 283 [ #EQ destruct] #x cases lbl' in EQcode_s1'; normalize nodelta [ #_ #EQ destruct] #lbl'' #EQcode_s1' … … 192 294 whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta [ #_ *] 193 295 ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode inversion(code … s1') 194 [1,3,4,5,6,7: cases daemon (*ASSURDI*) 296 [1,3,4,5,6,7: 297 [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 298 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ] 299 #_ whd in ⊢ (??%% → ?); 300 [ 301 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 302 | cases(call_post_clean ?????); normalize nodelta 303 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 304 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 305 [| #z cases(?∧?) normalize nodelta 306 ] 307 ] 308 ] 309 | cases(call_post_clean ?????) normalize nodelta 310 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 311 [| #y cases(?∧?) normalize nodelta 312 ] 313 ] 314 | cases(call_post_clean ?????) normalize nodelta 315 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 316 [ cases (?==?) normalize nodelta ] 317 ]] 318 | cases(call_post_clean ?????) normalize nodelta 319 [| #x cases(? ∧ ?) normalize nodelta ] 320 ] 321 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 195 322 | #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct 196 323 >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct] … … 215 342 216 343 lemma bool_true : ∀b : bool.b=true → b. * // #EQ destruct qed. 217 (* 218 axiom actionlabel_of_cost_is_not_empty : ∀l : ActionLabel. 219 is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c]. 220 *) 344 221 345 lemma labelled_action_is_correct : 222 346 ∀p,p',prog. … … 247 371 cases cost_lbl #HH2 #EQ destruct #EQget #EQ_cleaned #EQstore #EQio #EQ destruct 248 372 >EQcode_s1 in EQ_cleaned; inversion(code ? s1') 249 [2,3,4,5,6,7: cases daemon (*ASSURDI*)] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct 373 [2,3,4,5,6,7: [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 374 #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ] 375 #_ whd in ⊢ (??%% → ?); 376 [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 377 | cases(call_post_clean ?????); normalize nodelta 378 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 379 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 380 [| #z cases(?∧?) normalize nodelta 381 ] 382 ] 383 ] 384 | cases(call_post_clean ?????) normalize nodelta 385 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 386 [| #y cases(?∧?) normalize nodelta 387 ] 388 ] 389 | cases(call_post_clean ?????) normalize nodelta 390 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 391 [ cases (?==?) normalize nodelta ] 392 ]] 393 | cases(call_post_clean ?????) normalize nodelta 394 [| #x cases(? ∧ ?) normalize nodelta ] 395 ] 396 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct 250 397 %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} % 251 398 [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %] … … 256 403 whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta 257 404 [#_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1') 258 [1,2,4,5,6,7: cases daemon (*ASSURDI*)] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); 405 [1,2,4,5,6,7: [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 406 #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ] 407 #_ whd in ⊢ (??%% → ?); 408 [ | 409 | cases(call_post_clean ?????); normalize nodelta 410 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 411 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 412 [| #z cases(?∧?) normalize nodelta 413 ] 414 ] 415 ] 416 | cases(call_post_clean ?????) normalize nodelta 417 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 418 [| #y cases(?∧?) normalize nodelta 419 ] 420 ] 421 | cases(call_post_clean ?????) normalize nodelta 422 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 423 [ cases (?==?) normalize nodelta ] 424 ]] 425 | cases(call_post_clean ?????) normalize nodelta 426 [| #x cases(? ∧ ?) normalize nodelta ] 427 ] 428 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); 259 429 inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned 260 430 cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget] … … 271 441 whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *] 272 442 ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1') 273 [1,2,3,4,5,6: cases daemon (*ASSURDI*) ] 443 [1,2,3,4,5,6: [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 444 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ] 445 #_ whd in ⊢ (??%% → ?); 446 [ | 447 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 448 | cases(call_post_clean ?????); normalize nodelta 449 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 450 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 451 [| #z cases(?∧?) normalize nodelta 452 ] 453 ] 454 ] 455 | cases(call_post_clean ?????) normalize nodelta 456 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 457 [| #y cases(?∧?) normalize nodelta 458 ] 459 ] 460 | cases(call_post_clean ?????) normalize nodelta 461 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 462 [ cases (?==?) normalize nodelta ] 463 ]] 464 ] 465 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ] 274 466 #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] 275 467 * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
Note: See TracChangeset
for help on using the changeset viewer.