Changeset 3390 for LTS/Traces.ma

Timestamp:

Oct 10, 2013, 2:53:31 PM (7 years ago)

Author:

piccolo

Message:

Patched simulation proof, changed definition of silent trace

File:

• LTS/Traces.ma (modified) (4 diffs)

LTS/Traces.ma

@@ -198 +198 @@
 | silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
 | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
-                ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other → pre_silent_trace … tl → 
+                ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl → 
                 pre_silent_trace … (t_ind … prf … tl).
 
@@ -208 +208 @@
 [ #st' #EQ1 #EQ2 destruct #EQ destruct]
 #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
-#EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct
+#EQ destruct #_ #Hclass' @IH [ assumption ] assumption
 qed.
 
@@ -217 +217 @@
 definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
 raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
-(is_trace_non_empty … t → as_classify … st1 = cl_other).
+(is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
+well_formed_trace … t.
 
 lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
 ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
-#S #st1 #st2 #t elim t -t
+#S #st1 #st2 #t * //
+qed.
+(* elim t -t
 [ #st #_ %]
 #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
@@ -228 +231 @@
 #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
 % [ assumption | #_ assumption]
-qed.
+qed.*)
 
 inductive pre_measurable_trace (S : abstract_status) :