Changeset 379
 Timestamp:
 Dec 6, 2010, 4:03:36 PM (9 years ago)
 Location:
 Csemantics
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIOcomplete.ma
r378 r379 513 513 ##] nqed. 514 514 515 ninductive execution_characterisation : execution → Type≝515 ninductive execution_characterisation : execution → Prop ≝ 516 516  ec_terminates: ∀s,s',e,tr. 517 517 execution_terminates tr s e s' → … … 622 622 nqed. 623 623 624 nlemma not_ex_all_not: 625 ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x. 626 #A P; *; #H x; @; #H'; 627 napply H; @ x; napply H'; 628 nqed. 629 624 630 nlemma not_imply_elim: 625 631 ∀classic:(∀P:Prop.P ∨ ¬P). … … 643 649 ## napply (not_imply_elim2 P Q H); 644 650 ##] nqed. 651 652 nlemma not_and_to_imply: 653 ∀classic:(∀P:Prop.P ∨ ¬P). 654 ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q. 655 #classic P Q; *; #H H'; 656 @; #H''; napply H; @; //; 657 nqed. 645 658 646 659 ninductive execution_not_over : execution → Prop ≝ … … 726 739 ##] nqed. 727 740 741 nlemma exec_over_isteps': ∀ge,tr,s,s',e'. 742 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' → 743 exec_inf_aux ge (exec_step ge s') = e'. 744 #ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H; 745 napply (exec_over_isteps … H (refl ??)); 746 nqed. 747 728 748 nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. 729 749 exec_inf_aux ge (exec_step ge s) = e_interact o k → … … 747 767 ##] nqed. 748 768 769 nlet corec reactive_traceinf' ge s 770 (REACTIVE: ∀tr,s1,e1. 771 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 772 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 773 : traceinf' ≝ ?. 774 nlapply (REACTIVE E0 s (exec_inf_aux ge (exec_step ge s)) ?); 775 ##[ napply isteps_none 776 ## *; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H; 777 @ tr ? H; 778 napply (reactive_traceinf' ge s'); 779 #tr1 s1 e1 STEPS1; 780 napply REACTIVE; 781 ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1; 782 napply (isteps_trans … STEPS STEPS1); 783 ## ##skip 784 ##] 785 ##] 786 nqed. 787 788 nlet corec show_reactive ge s 789 (REACTIVE: ∀tr,s1,e1. 790 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 791 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 792 : execution_reacts (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?. 793 napply daemon; (* 794 nrewrite > (unroll_traceinf' (reactive_traceinf' …)); 795 (* FIXME: want to unfold and do case analysis on REACTIVE …, but can't until bug is fixed. *) 796 ncases (reactive_traceinf' ge s REACTIVE); 797 #tr tr' NE; nwhd in ⊢ (?(?%)??); nrewrite > (traceinf_traceinfp_app …); 798 napply (reacting … NE); 799 *) 800 nqed. 801 749 802 nlemma execution_characterisation_complete: 750 803 ∀classic:(∀P:Prop.P ∨ ¬P). 804 ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x). 751 805 ∀ge,s. ¬ (∃r. final_state s r) → 752 806 execution_characterisation (exec_inf_aux ge (Value ??? 〈E0,s〉)). 753 #classic ge s; *; #NOTFINAL;807 #classic constructive_indefinite_description ge s; *; #NOTFINAL; 754 808 nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (?%); 755 809 ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##] … … 780 834 ##] 781 835 782 (* FINISH *) 783 ## *; #REACTIVE; 784 (* napply ec_reacts;*) 785 (* FINISH *) 836 ## *; #NOTUNREACTIVE; 837 ncut (∀tr,s1,e1.execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 838 ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0); 839 ##[ #tr s1 e1 STEPS; 840 napply (classical_doubleneg classic); @; #NOREACTION; 841 napply NOTUNREACTIVE; 842 @ tr; @s1; @e1; @; //; 843 #tr2 s2 e2 STEPS2; 844 nlapply (not_ex_all_not … NOREACTION); #NR1; 845 nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2; 846 napply (classical_doubleneg classic); 847 napply NR2; //; 848 ## #REACTIVE; 849 napply ec_reacts; 850 ##[ ##2: napply (show_reactive ge s …); 851 #tr s1 e1 STEPS; 852 napply constructive_indefinite_description; 853 napply (REACTIVE … tr s1 e1 STEPS); 854 ## ##skip 855 ##] 856 ##] 786 857 ##] 787 858 … … 847 918 ##] 848 919 ##] 849 850 851 ndefinition behaviour_of_execution: 852 execution_characterisation → program_behavior ≝853 λe xec.match exec with920 nqed. 921 922 ndefinition behaviour_of_execution: ∀e. 923 execution_characterisation e → program_behavior ≝ 924 λe,exec.match exec with 854 925 [ ec_terminates s s' e tr H ⇒ Terminates tr ? 855  ec_diverges e tr H ⇒ Diverges tr926  ec_diverges _ e tr H ⇒ Diverges tr 856 927  ec_reacts s e tr H ⇒ Reacts tr 857 928  ec_wrong e s s' tr H ⇒ Goes_wrong tr 
Csemantics/Events.ma
r175 r379 131 131 repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. 132 132 *) 133 134 (* Ported from CompCert 1.7.1 >>> *) 135 136 (* * An alternate presentation of infinite traces as 137 infinite concatenations of nonempty finite traces. *) 138 139 ncoinductive traceinf': Type ≝ 140  Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'. 141 142 ndefinition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝ 143 λt,T. 144 match t return λt0.t0 ≠ E0 → ? with 145 [ nil ⇒ ? 146  cons e t' ⇒ λ_. 147 (match t' return λt0. t' = t0 → ? with 148 [ nil ⇒ λ_.〈e, T〉 149  cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉 150 ]) (refl ? t') 151 ]. 152 ##[ *; #NE; napply False_rect_Type0; napply NE; napply refl; 153 ## @; #E'; nrewrite > E' in E; #E; nwhd in E:(??%%); ndestruct (E); 154 ##] nqed. 155 156 nlet corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝ 157 match T' with 158 [ Econsinf' t T'' NOTEMPTY ⇒ 159 match split_traceinf' t T'' NOTEMPTY with [ mk_pair e tl ⇒ 160 Econsinf e (traceinf_of_traceinf' tl) ] 161 ]. 162 163 nremark unroll_traceinf': 164 ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ]. 165 #T; ncases T; //; nqed. 166 167 nremark unroll_traceinf: 168 ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ]. 169 #T; ncases T; //; 170 nqed. 171 172 nlemma traceinf_traceinfp_app: 173 ∀t,T,NE. 174 traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T. 175 #t; nelim t; 176 ##[ #T NE; ncases NE; #NE'; napply False_ind; napply NE'; napply refl; 177 ## #h t'; ncases t'; ##[ ##2: #h' t''; ##] #IH T NE; 178 nrewrite > (unroll_traceinf (traceinf_of_traceinf' ?)); 179 nwhd in ⊢ (??%?); //; nrewrite > (IH …); napply refl; 180 ##] nqed. 181 182 (* <<< *) 183 133 184 (* * The predicate [event_match ef vargs t vres] expresses that 134 185 the event [t] is generated when invoking external function [ef]
Note: See TracChangeset
for help on using the changeset viewer.