Changeset 392 for Csemantics
 Timestamp:
 Dec 8, 2010, 4:56:24 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIOcomplete.ma
r389 r392 780 780 nqed. 781 781 782 nlet corec show_reactive ge s 782 (* A slightly different version of the above, to work around a problem with the 783 next result. *) 784 nlet corec reactive_traceinf'' ge s 785 (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 783 786 (REACTIVE: ∀tr,s1,e1. 784 787 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 785 788 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 786 : execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?. 787 napply daemon; (* 788 nrewrite > (unroll_traceinf' (reactive_traceinf' …)); 789 (* FIXME: want to unfold and do case analysis on REACTIVE …, but can't until bug is fixed. *) 790 ncases (reactive_traceinf' ge s REACTIVE); 791 #tr tr' NE; nwhd in ⊢ (?(?%)??); nrewrite > (traceinf_traceinfp_app …); 792 napply (reacting … NE); 789 : traceinf' ≝ ?. 790 ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H; 791 @ tr ? H; 792 napply (reactive_traceinf'' ge s'); 793 ##[ napply REACTIVE; ##[ ##2: nlapply (exec_over_isteps' … STEPS); 794 #E; nrewrite > E in STEPS; 795 #STEPS; napply STEPS; ##] 796 ## 797 #tr1 s1 e1 STEPS1; 798 napply REACTIVE; 799 ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1; 800 napply (isteps_trans … STEPS STEPS1); 801 ## ##skip 802 ##] 803 ##] 804 nqed. 805 806 (* We want to prove 807 808 nlemma show_reactive : ∀ge,s. 809 ∀REACTIVE:∀tr,s1,e1. 810 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 811 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. 812 execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). 813 814 but the current matita won't unfold reactive_traceinf' so that we can do case 815 analysis on (REACTIVE …). Instead we take an "applied" version of REACTIVE that 816 we can do case analysis on, then get it into the desired form afterwards. 793 817 *) 794 nqed. 818 nlet corec show_reactive' ge s 819 (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 820 (REACTIVE: ∀tr1,s1,e1. 821 execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 822 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) 823 : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s REACTIVE0 REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?. 824 (*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*) 825 napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]); 826 ncases REACTIVE0; 827 #x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT; 828 nwhd in ⊢ (?(?%)??); 829 (*nrewrite > (traceinf_traceinfp_app …);*) 830 napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]); 831 napply (reacting … STEPS NOTSILENT); 832 (*nrewrite < (exec_over_isteps' … STEPS) in ⊢ (???%);*) 833 napply (match (exec_over_isteps' … STEPS) return λe'.λ_. 834 ?(?(reactive_traceinf'' ?? 835 (REACTIVE ??? (eq_ind_r execution e1 (λx.λ_.execution_isteps ???? e1 → ?) (λS.S) ? (exec_over_isteps' ???? e1 STEPS) STEPS)) 836 (λtr2,s2,e2,S1.REACTIVE ? s2 e2 (eq_ind_r execution e1 (λx.λ_:x=e1.execution_isteps tr2 s1 x s2 e2 → ?) (λS.isteps_trans ?????? e1 ? STEPS S) ? (exec_over_isteps' ???? e1 STEPS) S1)) 837 ))? e' 838 with [ refl ⇒ ? ]); 839 napply show_reactive'; 840 nqed. 841 842 nlemma show_reactive : ∀ge,s. 843 ∀REACTIVE:∀tr,s1,e1. 844 execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → 845 Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. 846 execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s ? REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). 847 ##[ 848 #ge s REACTIVE; 849 napply show_reactive'; 850 ## napply (REACTIVE … (isteps_none …)); 851 ##] nqed. 795 852 796 853 nlemma execution_characterisation_complete:
Note: See TracChangeset
for help on using the changeset viewer.