Changeset 378 for Csemantics
 Timestamp:
 Dec 6, 2010, 11:49:57 AM (9 years ago)
 Location:
 Csemantics
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIO.ma
r366 r378 1329 1329 execution_isteps tr' s e s' e' → 1330 1330 k i = e_step tr s e → 1331 (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog*)1331 (* (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)*) 1332 1332 execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'. 1333 1334 nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3. 1335 execution_isteps tr1 s1 e1 s2 e2 → 1336 execution_isteps tr2 s2 e2 s3 e3 → 1337 execution_isteps (tr1⧺tr2) s1 e1 s3 e3. 1338 #tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1; 1339 ##[ #s e; //; 1340 ## #e e' tr tr' s1' s2' s3' H1 H2 H3; 1341 nrewrite > (Eapp_assoc …); 1342 napply isteps_one; 1343 napply H2; napply H3; 1344 ## #e e' o k i s1' s2' s3' tr tr' H1 H2 H3 H4; 1345 nrewrite > (Eapp_assoc …); 1346 napply (isteps_interact … H2); /2/; 1347 ##] nqed. 1333 1348 1334 1349 nlemma exec_e_step: ∀ge,x,tr,s,e. … … 1353 1368 ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; 1354 1369 napply refl; 1370 ## #EXEC; nwhd in EXEC:(??%?); ndestruct 1371 ##] nqed. 1372 1373 nlemma exec_e_step_inv2: ∀ge,x,tr,s,e. 1374 exec_inf_aux ge x = e_step tr s e → 1375 ¬∃r.final_state s r. 1376 #ge x tr s e; 1377 nrewrite > (exec_inf_aux_unfold …); ncases x; 1378 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct 1379 ## #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?); 1380 ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; 1381 napply FINAL; 1355 1382 ## #EXEC; nwhd in EXEC:(??%?); ndestruct 1356 1383 ##] nqed. … … 1395 1422 ## #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC'); 1396 1423 ##] 1397 ## #e e' o k i s s' s0 tr tr' H1 H2 H3IH;1424 ## #e e' o k i s s' s0 tr tr' H1 H2 IH; 1398 1425 nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?); 1399 1426 ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; … … 1411 1438 ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?); 1412 1439 ncases (is_final_state s); 1413 ##[ #X; ncases X; #r FINAL'; napply False_ind; napply (absurd ?? H3); 1440 ##[ #X; ncases X; #r FINAL'; napply False_ind; 1441 ncases (exec_e_step_inv2 … H2); #H; napply H; 1414 1442 @ r; napply FINAL' ##] 1415 1443 #FINAL'; nwhd in ⊢ (??%?); … … 1431 1459 ninductive execution_terminates : trace → state → execution → state → Prop ≝ 1432 1460  terminates : ∀s,s',tr,tr',r,e,m. 1433 execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m). 1461 execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m) 1462 (* We should only be able to get to here if main is an external function, which is silly. *) 1463  annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i. 1464 execution_isteps tr s e s' (e_interact o k) → 1465 k i = e_stop tr' r m → 1466 execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m). 1434 1467 1435 1468 ncoinductive execution_diverging : execution → Prop ≝ … … 1510 1543 ##] nqed. 1511 1544 1545 nlemma e_stop_inv: ∀ge,x,tr,r,m. 1546 exec_inf_aux ge x = e_stop tr r m → 1547 x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉. 1548 #ge x tr r m; 1549 nrewrite > (exec_inf_aux_unfold …); ncases x; 1550 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct; 1551 ## #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s'); 1552 ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?); 1553 ndestruct (EXEC); napply refl; 1554 ## #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC); 1555 ##] 1556 ## #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC); 1557 ##] nqed. 1558 1512 1559 nlemma terminates_sound: ∀ge,tr,s,s',e. 1513 1560 execution_terminates tr s e s' → … … 1515 1562 ∃r. star (mk_transrel … step) ge s tr s' ∧ final_state s' r. 1516 1563 #ge tr0 s0 s0' e0 H; ncases H; 1517 #s s' tr tr' r e m ESTEPS EXEC; @r; @; //; 1518 ncases (several_steps … ESTEPS EXEC); #STARs' EXECs'; 1519 napply (star_right … STARs'); 1520 ##[ ##2: napply (final_step ge tr' r m s'); 1521 napply (exec_e_step … EXECs'); 1522 ## ##skip 1523 ## napply refl 1564 ##[ #s s' tr tr' r e m ESTEPS EXEC; @r; @; //; 1565 ncases (several_steps … ESTEPS EXEC); #STARs' EXECs'; 1566 napply (star_right … STARs'); 1567 ##[ ##2: napply (final_step ge tr' r m s'); 1568 napply (exec_e_step … EXECs'); 1569 ## ##skip 1570 ## napply refl 1571 ##] 1572 ## #s s' tr tr' r e m o k i ESTEPS EXECK EXEC; @r; @; //; 1573 ncases (several_steps … ESTEPS EXEC); #STARs' EXECs'; 1574 napply (star_right … STARs'); 1575 ##[ ##2: nlapply (exec_step_sound ge s'); 1576 nlapply (exec_e_step … EXECs'); 1577 ncases (exec_step ge s'); 1578 ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …); #EXECs''; 1579 nwhd in EXECs'':(??%?) ⊢ (% → ?); 1580 ncut (o' = o); ##[ ndestruct (EXECs''); // ##] #E1; 1581 nrewrite > E1 in k' EXECs'' ⊢ %; #k' EXECs''; 1582 ncut (k = λv.exec_inf_aux ge (k' v)); ##[ ndestruct (EXECs''); // ##] #E2; 1583 nrewrite > E2 in ESTEPS EXECK EXECs' EXECs''; 1584 #ESTEPS EXECK EXECs' EXECs'' STEP; nlapply (STEP i); 1585 nrewrite > (e_stop_inv … EXECK); nwhd in ⊢ (% → ?); 1586 //; 1587 ## #z; ncases z; #tr'' s''; nrewrite > (exec_inf_aux_unfold …); 1588 nwhd in ⊢ (??%? → ?); ncases (is_final_state s''); 1589 #H EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC) 1590 ## nrewrite > (exec_inf_aux_unfold …); 1591 #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC) 1592 ##] 1593 ## ##skip 1594 ## napply refl 1595 ##] 1524 1596 ##] nqed. 1525 1597 
Csemantics/CexecIOcomplete.ma
r366 r378 512 512 ##] 513 513 ##] nqed. 514 515 ninductive execution_characterisation : execution → Type ≝ 516  ec_terminates: ∀s,s',e,tr. 517 execution_terminates tr s e s' → 518 execution_characterisation (e_step E0 s e) 519  ec_diverges: ∀s,e,tr. 520 execution_diverges tr e → 521 execution_characterisation (e_step E0 s e) 522  ec_reacts: ∀s,e,tr. 523 execution_reacts tr s e → 524 execution_characterisation (e_step E0 s e) 525  ec_wrong: ∀e,s,s',tr. 526 execution_goes_wrong tr s e s' → 527 execution_characterisation (e_step E0 s e). 528 529 (* bit of a hack to avoid inability to reduce term in match *) 530 ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝ 531 λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k  _ ⇒ True ]. 532 533 nlemma err_does_not_interact: ∀A,B,P,e1,e2. 534 (∀x:B.interact_prop A P (e2 x)) → 535 interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2). 536 #A B P e1 e2 H; 537 ncases e1; //; nqed. 538 539 nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2. 540 (∀x,y.interact_prop A P (e2 x y)) → 541 interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2). 542 #A B C P e1 e2 H; 543 ncases e1; ##[ #z; ncases z; ##] //; nqed. 544 545 nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2. 546 (∀x.interact_prop A P (e2 x)) → 547 interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2). 548 #A B P Q e1 e2 H; 549 ncases e1; //; nqed. 550 551 nlemma opt_does_not_interact: ∀A,B,P,e1,e2. 552 (∀x:B.interact_prop A P (e2 x)) → 553 interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2). 554 #A B P e1 e2 H; 555 ncases e1; //; nqed. 556 557 nlemma exec_step_interaction: 558 ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s). 559 #ge s; ncases s; 560 ##[ #f st kk e m; ncases st; 561 ##[ ##11,14: #a ## ##2,4,6,7,12,13,15: #a b ## ##3,5: #a b c ## ##8: #a b c d ##] 562 ##[ ##4,6,8,9: napply I ##] 563 nwhd in ⊢ (???%); 564 ##[ ncases a; ##[ ncases (fn_return f); //; ## #e; nwhd nodelta in ⊢ (???%); 565 napply err_sig_does_not_interact; #x; napply err2_does_not_interact; // ##] 566 ## ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ## #z; ncases z; #x y; napply I ##] 567 ## napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I 568 ## ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I 569 ## napply err2_does_not_interact; #x1 x2; ncases x1; //; 570 ## napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply err_does_not_interact; #x6; ncases a; 571 ##[ napply I; ## #x7; napply err2_does_not_interact; #x8 x9; napply I ##] 572 ## ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I 573 ## napply I ##] 574 ## ncases kk; ##[ ##1,8: ncases (fn_return f); //; ## ##2,3,5,6,7: //; 575 ## #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##] 576 ## ncases kk; //; 577 ## ncases kk; ##[ ##4: #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I 578 ## ##*: // ##] 579 ##] 580 ## #f args kk m; ncases f; 581 ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f')); 582 #x; ncases x; ##[ *; ## #z; ncases z; #x1 x2 H; 583 napply err_sig_does_not_interact; //; ##] 584 (* This is the only case that actually matters! *) 585 ## #fn argtys rty; nwhd in ⊢ (???%); 586 napply err_sig_does_not_interact; #x1; 587 nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl; 588 ## @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##] 589 ##] 590 ## #v kk m; nwhd in ⊢ (???%); ncases kk; 591 ##[ ##8: #x1 x2 x3 x4; ncases x1; 592 ##[ nwhd in ⊢ (???%); ncases v; // ## #x5; nwhd in ⊢ (???%); ncases x5; 593 #x6 x7; napply opt_does_not_interact; // ##] 594 ## ##*: // ##] 595 ##] nqed. 596 597 598 (* Some classical logic (roughly like a fragment of Coq's library) *) 599 nlemma classical_doubleneg: 600 ∀classic:(∀P:Prop.P ∨ ¬P). 601 ∀P:Prop. ¬ (¬ P) → P. 602 #classic P; *; #H; 603 ncases (classic P); 604 ##[ // ## #H'; napply False_ind; /2/; ##] 605 nqed. 606 607 nlemma classical_not_all_not_ex: 608 ∀classic:(∀P:Prop.P ∨ ¬P). 609 ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x. 610 #classic A P; *; #H; 611 napply (classical_doubleneg classic); @; *; #H'; 612 napply H; #x; @; #H''; napply H'; @x; napply H''; 613 nqed. 614 615 nlemma classical_not_all_ex_not: 616 ∀classic:(∀P:Prop.P ∨ ¬P). 617 ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x. 618 #classic A P; *; #H; 619 napply (classical_not_all_not_ex classic A (λx.¬ P x)); 620 @; #H'; napply H; #x; napply (classical_doubleneg classic); 621 napply H'; 622 nqed. 623 624 nlemma not_imply_elim: 625 ∀classic:(∀P:Prop.P ∨ ¬P). 626 ∀P,Q:Prop. ¬ (P → Q) → P. 627 #classic P Q; *; #H; 628 napply (classical_doubleneg classic); @; *; #H'; 629 napply H; #H''; napply False_ind; napply H'; napply H''; 630 nqed. 631 632 nlemma not_imply_elim2: 633 ∀P,Q:Prop. ¬ (P → Q) → ¬ Q. 634 #P Q; *; #H; @; #H'; 635 napply H; #_; napply H'; 636 nqed. 637 638 nlemma imply_to_and: 639 ∀classic:(∀P:Prop.P ∨ ¬P). 640 ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q. 641 #classic P Q H; @; 642 ##[ napply (not_imply_elim classic P Q H); 643 ## napply (not_imply_elim2 P Q H); 644 ##] nqed. 645 646 ninductive execution_not_over : execution → Prop ≝ 647  eno_step: ∀tr,s,e. execution_not_over (e_step tr s e) 648  eno_interact: ∀o,k,tr,s,e,i. 649 k i = e_step tr s e → 650 execution_not_over (e_interact o k). 651 652 nlemma eno_stop: ∀tr,r,m. execution_not_over (e_stop tr r m) → False. 653 #tr0 r0 m0 H; ninversion H; 654 ##[ #tr s e E; ndestruct 655 ## #o k tr s e i K E; ndestruct 656 ##] nqed. 657 658 nlemma eno_wrong: execution_not_over e_wrong → False. 659 #H; ninversion H; 660 ##[ #tr s e E; ndestruct 661 ## #o k tr s e i K E; ndestruct 662 ##] nqed. 663 664 nlet corec show_divergence s e 665 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → 666 execution_not_over e1) 667 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0) 668 (CONTINUES:∀tr2,s2,o,k. execution_isteps tr2 s e s2 (e_interact o k) → ∃i.∃tr3.∃s3.∃e3. k i = e_step tr3 s3 e3 ∧ tr3 ≠ E0) 669 : execution_diverging e ≝ ?. 670 nlapply (NONTERMINATING E0 s e ?); //; 671 ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %; 672 ##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO); 673 ## #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?); 674 ##[ nrewrite < (E0_right tr) in ⊢ (?%????); 675 napply isteps_one; napply isteps_none; 676 ## #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*) 677 #NONTERMINATING CONTINUES; #_; @; 678 napply (show_divergence s'); 679 ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1); 680 nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one; 681 napply S; 682 ## #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2); 683 nchange in ⊢ (?%????) with (Eapp E0 tr2); 684 napply isteps_one; napply S; 685 ## #tr2 s2 o k S; napply (CONTINUES tr2 s2 o k); 686 nchange in ⊢ (?%????) with (Eapp E0 tr2); 687 napply isteps_one; napply S; 688 ##] 689 ##] 690 ## #_; #_; #_; #ENO; nelim (eno_wrong … ENO); 691 ## #o k UNREACTIVE NONTERMINATING CONTINUES; #_; 692 nlapply (CONTINUES E0 s o k ?); 693 ##[ napply isteps_none; 694 ## *; #i; *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT; 695 napply False_ind; napply (absurd ?? NOTSILENT); 696 napply (UNREACTIVE … s' e'); 697 nrewrite < (E0_right tr') in ⊢ (?%????); 698 napply (isteps_interact … EXEC); //; 699 ##] 700 ##] nqed. 701 702 nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'. 703 execution_isteps tr s e s' e' → 704 e = (exec_inf_aux ge (exec_step ge s)) → 705 exec_inf_aux ge (exec_step ge s') = e'. 706 #ge tr0 s0 s0' e0 e0'; 707 #ISTEPS; nelim ISTEPS; 708 ##[ #s e E; nrewrite > E; napply refl; 709 ## #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E; 710 napply IH; napply sym_eq; napply exec_e_step; 711 ##[ ##3: napply sym_eq; napply E ##] 712 ## #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E; 713 napply IH; 714 ncases (exec_step ge s3) in E; 715 ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?); 716 #E'; nwhd in E':(???%); ndestruct (E'); 717 napply sym_eq; napply exec_e_step; 718 ##[ ##3: napply EXECK; ##] 719 ## #z; ncases z; #tr' s'; 720 nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?); 721 nwhd in ⊢ (???% → ?); ncases (is_final_state s'); 722 #F E'; nwhd in E':(???%); ndestruct (E'); 723 ## nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?); 724 #E'; nwhd in E':(???%); ndestruct (E'); 725 ##] 726 ##] nqed. 727 728 nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. 729 exec_inf_aux ge (exec_step ge s) = e_interact o k → 730 k i = e_step tr s' e → 731 tr ≠ E0. 732 #ge o k i tr s s' e; nrewrite > (exec_inf_aux_unfold …); 733 nlapply (exec_step_interaction ge s); 734 ncases (exec_step ge s); 735 ##[ #o' k' ; nwhd in ⊢ (% → ??%? → ?); #H E K; ndestruct (E); 736 nlapply (H i); *; #tr'; *; #s''; *; #K' TR; 737 nrewrite > K' in K; nrewrite > (exec_inf_aux_unfold …); 738 nwhd in ⊢ (??%? → ?); 739 ncases (is_final_state s''); 740 ##[ #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E); 741 ## #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E); 742 napply TR 743 ##] 744 ## #x; ncases x; #tr' s'' H; nwhd in ⊢ (??%? → ?); 745 ncases (is_final_state s''); #F E; nwhd in E:(??%?); ndestruct (E); 746 ## #_; #E; nwhd in E:(??%?); ndestruct (E); 747 ##] nqed. 748 749 nlemma execution_characterisation_complete: 750 ∀classic:(∀P:Prop.P ∨ ¬P). 751 ∀ge,s. ¬ (∃r. final_state s r) → 752 execution_characterisation (exec_inf_aux ge (Value ??? 〈E0,s〉)). 753 #classic ge s; *; #NOTFINAL; 754 nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (?%); 755 ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##] 756 #NOTFINAL'; nwhd in ⊢ (?%); 757 ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 758 execution_not_over e1)); 759 ##[ #NONTERMINATING; 760 ncases (classic (∃tr,s1,e1. execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 ∧ 761 ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0)); 762 ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE; 763 napply (ec_diverges … tr); 764 napply (diverges_diverging … INITIAL); 765 napply (show_divergence s1); 766 ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2); 767 napply (isteps_trans … INITIAL S); 768 ## #tr2 s2 e2 S; napply (UNREACTIVE … S); 769 ## #tr2 s2 o; ncases o; #o_id o_args o_typ; ncases o_typ; #k S; 770 nlapply (exec_over_isteps … INITIAL (refl ??)); #EXEC1; 771 nlapply (exec_over_isteps … S (sym_eq … EXEC1)); 772 nlapply (NONTERMINATING (Eapp tr tr2) s2 (e_interact (mk_io_out o_id o_args ?) k) ?); 773 ##[ ##1,3: napply (isteps_trans … INITIAL S); ##] 774 #NOTOVER; ninversion NOTOVER; 775 ##[ ##1,3: #tr' s' e' E; ndestruct (E); 776 ## ##*: #o' k' tr' s' e' i' KR E; ndestruct (E); 777 #EXEC; 778 @ i'; @ tr'; @s'; @e'; @;//; napply (interaction_is_not_silent … EXEC KR); 779 ##] 780 ##] 781 782 (* FINISH *) 783 ## *; #REACTIVE; 784 (* napply ec_reacts;*) 785 (* FINISH *) 786 ##] 787 788 ## #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING); 789 *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2); 790 *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3); 791 *; #e NNT4; nelim (imply_to_and classic … NNT4); 792 ncases e; 793 ##[ #tr' r m; #STEPS NOSTEP; 794 napply (ec_terminates s (Returnstate (Vint r) Kstop m) ? (Eapp tr tr')); @; 795 ##[ napply s' 796 ## napply STEPS 797 ##] 798 ## #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0; 799 napply NOSTEP; // 800 ## #STEPS NOSTEP; 801 napply (ec_wrong ? s s' tr); @; //; 802 (* The following is stupidly complicated for an impossible case. 803 It ought to be simplified. *) 804 ## #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP; 805 ##[ nletin i ≝ (repr 0) ## nletin i ≝ Fzero ##] 806 nlapply (refl ? (k i)); 807 ncases (k i) in ⊢ (???% → ?); 808 ##[ ##1,5: #tr' r m K; 809 napply (ec_terminates s ???); 810 ##[ ##3,6: napply (annoying_corner_case_terminates … STEPS K); 811 ## ##*: ##skip 812 ##] 813 ## ##2,6: #tr' s'' e' K; napply False_rect_Type0; 814 napply (absurd ?? NOSTEP); 815 napply (eno_interact … K); 816 ## ##3,7: #K; 817 nlapply (exec_step_interaction ge s'); 818 nlapply (exec_over_isteps … STEPS (refl ??)); 819 nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s'); 820 ##[ ##1,4: #o k E H; nwhd in E:(??%?) H; 821 ndestruct (E); 822 nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K; 823 nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?); 824 ncases (is_final_state s'); #F E; nwhd in E:(??%?); 825 ndestruct (E); 826 ## ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?); 827 ncases (is_final_state s); #F E; nwhd in E:(??%?); 828 ndestruct (E); 829 ## ##3,6: #E; nwhd in E:(??%?); ndestruct (E); 830 ##] 831 ## ##4,8: #o0 k0 K; 832 nlapply (exec_step_interaction ge s'); 833 nlapply (exec_over_isteps … STEPS (refl ??)); 834 nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s'); 835 ##[ ##1,4: #o k E H; nwhd in E:(??%?) H; 836 ndestruct (E); 837 nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K; 838 nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?); 839 ncases (is_final_state s'); #F E; nwhd in E:(??%?); 840 ndestruct (E); 841 ## ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?); 842 ncases (is_final_state s); #F E; nwhd in E:(??%?); 843 ndestruct (E); 844 ## ##3,6: #E; nwhd in E:(??%?); ndestruct (E); 845 ##] 846 ##] 847 ##] 848 ##] 849 850 851 ndefinition behaviour_of_execution: 852 execution_characterisation → program_behavior ≝ 853 λexec.match exec with 854 [ ec_terminates s s' e tr H ⇒ Terminates tr ? 855  ec_diverges e tr H ⇒ Diverges tr 856  ec_reacts s e tr H ⇒ Reacts tr 857  ec_wrong e s s' tr H ⇒ Goes_wrong tr 858 ]. 859
Note: See TracChangeset
for help on using the changeset viewer.