Theory Trace

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               November 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Trace = Infra:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite (notick | t = []t)                 *)
(*                                                                     *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(***********************************************************

    Type Definitions
      'a event      : type of events      a,b,...
      'a trace      : type of traces      s,t,...

 ***********************************************************)

datatype 'a event = Ev 'a | Tick

consts
  Evset     :: "'a event set"
  EvsetTick :: "'a event set"

defs
  Evset_def     : "Evset     == {a. a ~= Tick}"
  EvsetTick_def : "EvsetTick == UNIV"

(* EvsetTick seems to be useless, but it sometimes *)
(* makes proofs to be readable.                    *)

(*------------------------------------*
 |              X-Symbols             |
 *------------------------------------*)

syntax (output)
  "_TickX" :: "'a event" ("Tick")

syntax (xsymbols)
  "_TickX" :: "'a event" ("\<surd>")

translations
  "\<surd>"   == "Tick"

(*******************************
    Evset contains all (Ev a)
 *******************************)

lemma Un_Evset[simp] : "Ev ` X Un Evset = Evset"
by (auto simp add: Evset_def)

(*******************************
         Tick or Ev a
 *******************************)

lemma event_tick_or_Ev: "ALL e. e = Tick | (EX a. e = Ev a)"
apply (intro allI)
by (induct_tac e, auto)

lemma not_tick_to_Ev: "(e ~= Tick) = (EX a. e = Ev a)"
apply (auto)
apply (insert event_tick_or_Ev)
apply (drule_tac x="e" in spec)
by (simp)

lemma in_Ev_set : "(e : Ev ` X) = (EX a. (e = Ev a & a : X))"
by (auto)

lemma notin_Ev_set : "(e ~: Ev ` X) = (e = Tick | (EX a. (e = Ev a & a ~: X)))"
apply (insert event_tick_or_Ev)
apply (drule_tac x="e" in spec)
by (auto)

(*******************************
             inj
 *******************************)

lemma inj_Ev: "inj Ev"
apply (simp add: inj_on_def)
done

(***********************************************************
                    Definition of traces
 ***********************************************************)

(* "typedef" requires defined types are not empty as follows: *)

typedef 'a Some_trace = "{ss::('a event list). Tick ~: set (butlast ss)}"
apply (rule_tac x ="[]" in exI)
apply (simp)
done

declare Rep_Some_trace         [simp]

types 'a trace = "'a Some_trace option"

(*****************************************************************
            directly convert from list to trace
 *****************************************************************)

consts
  Abs_trace :: "'a event list => 'a trace"
  Rep_trace :: "'a trace => 'a event list"

defs
  Abs_trace_def : 
    "Abs_trace s == if s : Some_trace then Some (Abs_Some_trace s) else None"

  Rep_trace_def : 
    "Rep_trace s == Rep_Some_trace (the s)"

(***********************************************************)
(*                  operators over traces                  *)
(*                                                         *)
(*    memo    (infixr "@t" 65) = ("_ @t _" [66,65] 65)     *)
(*                                                         *)
(***********************************************************)

consts
  nilt    :: "'a trace"                                ("[]t")
  sett    :: "'a trace => 'a event set"
  lengtht :: "'a trace => nat"
  notick  :: "'a trace => bool"
  apprep  :: "'a trace => 'a trace => 'a event list"  (infixr "@rep" 65)
  appt    :: "'a trace => 'a trace => 'a trace"        (infixr "@t" 65)

  hdt      :: "'a trace => 'a event"
  tlt      :: "'a trace => 'a trace"
  lastt    :: "'a trace => 'a event"
  butlastt :: "'a trace => 'a trace"

defs
  nilt_def   : "[]t       == Abs_trace []"
  sett_def   : "sett s    == if (s = None) then {} else set (Rep_trace s)"
  lengtht_def: "lengtht s == if (s = None) then 0 else length (Rep_trace s)"
  notick_def : "notick s  == (s ~= None) & (Tick ~: sett s)"
  apprep_def : "s @rep t  == Rep_trace s @ Rep_trace t"
  appt_def   : "s @t t    == if (s = None | t = None) then None
                             else Abs_trace (s @rep t)"

  hdt_def      : "hdt s      == hd (Rep_trace s)"
  tlt_def      : "tlt s      == if s = None then None
                                else Abs_trace (tl (Rep_trace s))"
  lastt_def    : "lastt s    == last (Rep_trace s)"
  butlastt_def : "butlastt s == if s = None then None
                                else Abs_trace (butlast (Rep_trace s))"

syntax
  "@trace"   :: "args => 'a trace"                       ("[(_)]t")

translations
  "[s]t"      == "Abs_trace [s]"

(***********************************************************
                       option
 ***********************************************************)

lemma trace_None_or_Some_or_None: "ALL s. s = None | (EX ss. s = Some ss)"
by (auto)

(***********************************************************
                          lemmas
 ***********************************************************)

(***************************************
         trace Rep and Abs lemmas
 ***************************************)

lemma Abs_trace_None:
   "s ~: Some_trace ==> Abs_trace s = None"
by (simp add: Abs_trace_def)

lemma Abs_trace_Some:
   "s : Some_trace ==> Abs_trace s = Some (Abs_Some_trace s)"
by (simp add: Abs_trace_def)

lemma Abs_trace_None_notin_Some_trace: 
   "(Abs_trace s = None) = (s ~: Some_trace)"
by (auto simp add: Abs_trace_def)

lemma Abs_trace_not_None_in_Some_trace: 
   "(Abs_trace s ~= None) = (s : Some_trace)"
by (auto simp add: Abs_trace_def)

(*** basic ***)

lemma Rep_trace[simp]: "Rep_trace t : Some_trace"
by (simp add: Rep_trace_def)

lemma Abs_trace_inverse:
  "t : Some_trace ==> Rep_trace (Abs_trace t) = t"
apply (simp add: Abs_trace_def Rep_trace_def)
by (simp add: Abs_Some_trace_inverse)

lemma Rep_trace_inverse:
  "t ~= None ==> Abs_trace (Rep_trace t) = t"
apply (simp add: Abs_trace_def Rep_trace_def)
by (auto simp add: Rep_Some_trace_inverse)

lemma Abs_trace_inject:
  "[| s : Some_trace ; t : Some_trace |] 
     ==> (Abs_trace s = Abs_trace t) = (s = t)"
apply (simp add: Abs_trace_def)
by (simp add: Abs_Some_trace_inject)

lemma Rep_trace_inject:
  "[| s ~= None ; t ~= None |] 
     ==> (Rep_trace s = Rep_trace t) = (s = t)"
apply (simp add: Rep_trace_def)
by (auto simp add: Rep_Some_trace_inject)

(*** Abs-Rep ***)

lemma Abs_trace_Rep_trace_inverse_Some_left: 
  "[| t : Some_trace ; Abs_trace t = Some s |] ==> t = Rep_trace (Some s)"
apply (simp add: Abs_trace_def Rep_trace_def)
by (auto simp add: Abs_Some_trace_inverse Rep_Some_trace_inverse)

lemma Abs_trace_Rep_trace_inverse_Some_right: 
  "[| t : Some_trace ; Some s = Abs_trace t |] ==> t = Rep_trace (Some s)"
apply (simp add: Abs_trace_def Rep_trace_def)
by (auto simp add: Abs_Some_trace_inverse Rep_Some_trace_inverse)

lemmas Abs_trace_Rep_trace_inverse_Some =
       Abs_trace_Rep_trace_inverse_Some_left Abs_trace_Rep_trace_inverse_Some_right

lemma Abs_trace_Rep_trace_inverse_left: 
  "[| t : Some_trace ; s ~= None |] ==> ((Abs_trace t = s) = (t = Rep_trace s))"
by (auto simp add: Abs_trace_Rep_trace_inverse_Some Rep_trace_inverse)

lemma Abs_trace_Rep_trace_inverse_right: 
  "[| t : Some_trace ; s ~= None |] ==> ((s = Abs_trace t) = (t = Rep_trace s))"
by (auto simp add: Abs_trace_Rep_trace_inverse_Some
                   Abs_trace_inverse Rep_trace_inverse)

lemmas Abs_trace_Rep_trace_inverse =
       Abs_trace_Rep_trace_inverse_left Abs_trace_Rep_trace_inverse_right

(*** Rep-Abs ***)

lemma Rep_trace_Abs_trace_inverse_left_only_if: 
  "[| t ~= None ; Rep_trace t = s |] ==> t = Abs_trace s"
by (auto simp add: Rep_trace_inverse)

lemma Rep_trace_Abs_trace_inverse_right_only_if: 
  "[| t ~= None ; s = Rep_trace t |] ==> t = Abs_trace s"
by (auto simp add: Rep_trace_inverse)

lemmas Rep_trace_Abs_trace_inverse_only_if =
           Rep_trace_Abs_trace_inverse_left_only_if
           Rep_trace_Abs_trace_inverse_right_only_if

(*** Abs image ***)

lemma Abs_trace_inverse_in_only_if: 
  "[| ALL s:X. s : Some_trace ; t : Abs_trace ` X |] ==> Rep_trace t : X"
apply (simp add: image_def, erule bexE)
apply (drule_tac x="x" in bspec, simp)
by (simp add: Abs_trace_inverse)

lemma Abs_trace_inverse_in_if: 
  "[| t ~= None ; Rep_trace t : X |] ==> t : Abs_trace ` X"
apply (simp add: image_def)
apply (rule_tac x="Rep_trace t" in bexI)
by (simp_all add: Rep_trace_inverse)

lemma Abs_trace_inverse_in:
  "[| ALL s:X. s : Some_trace ; t ~= None |]
       ==> (t : Abs_trace ` X) = (Rep_trace t : X)"
apply (rule iffI)
apply (simp add: Abs_trace_inverse_in_only_if)
by (simp add: Abs_trace_inverse_in_if)

(*******************************
         check in Some_trace
 *******************************)

lemma nil_in_Some_trace[simp] : "[] : Some_trace"
by (simp add: Some_trace_def)

lemma tick_in_Some_trace[simp] : "[Tick]:Some_trace"
by (simp add: Some_trace_def)

lemma event_in_Some_trace[simp] : "[a] : Some_trace"
by (simp add: Some_trace_def)

lemma notic_in_Some_trace[simp] : "Tick ~: set s ==> s : Some_trace"
by (simp add: Some_trace_def notin_set_butlast)

(*--------------------------*
 |        decompo app       |
 *--------------------------*)

(*** decompo traces only if ***)

lemma decompo_app_in_Some_trace_only_if1 : "s @ t : Some_trace ==> s : Some_trace"
apply (simp add: Some_trace_def)
apply (simp add: notin_butlast_decompo)
apply (erule disjE)
by (simp_all add: notin_set_butlast)

lemma decompo_app_in_Some_trace_only_if2 : "s @ t : Some_trace ==> t : Some_trace"
apply (simp add: Some_trace_def)
apply (simp add: notin_butlast_decompo)
by (auto)

lemma decompo_app_in_Some_trace_only_if : 
  "s @ t : Some_trace ==> (s : Some_trace & t = []) | (Tick ~: set s & t : Some_trace)"
apply (insert list_last_nil_or_unnil)
apply (drule_tac x="t" in spec)
apply (erule disjE)

 (* t = [] *)
 apply (simp)

 (* t = sa @ [a] *)
 apply (elim exE)
 apply (rule disjI2)
 apply (rule conjI)

 apply (simp add: Some_trace_def)
 apply (simp add: notin_butlast_decompo)

 apply (rule decompo_app_in_Some_trace_only_if2[of s])
 apply (simp)
done

(*** decompo Some_traces if ***)

lemma decompo_app_in_Some_trace_if : 
  "[| Tick ~: set s ; t : Some_trace |] ==> s @ t : Some_trace"
by (simp add: Some_trace_def notin_butlast_decompo)

(****** decompo Some_traces iff ******)

lemma decompo_app_in_Some_trace : 
  "s @ t : Some_trace = ((s : Some_trace & t = []) | (Tick ~: set s & t : Some_trace))"
apply (rule iffI)
apply (simp add: decompo_app_in_Some_trace_only_if)
apply (erule disjE)
by (simp_all add: decompo_app_in_Some_trace_if)

(*--------------------------*
 |       decompo cons       |
 *--------------------------*)

(*** decompo Some_traces if ***)

lemma decompo_head_in_Some_trace_if:
  "[| a ~= Tick ; t : Some_trace |] ==> a # t : Some_trace"
apply (insert decompo_app_in_Some_trace_if[of "[a]" t])
by (auto)

lemma decompo_head_in_Some_trace : 
  "a # t : Some_trace =  (t = [] | (a ~= Tick & t : Some_trace))"
apply (insert decompo_app_in_Some_trace[of "[a]"])
by (auto)

lemma decompo_last_in_Some_trace_if : 
  "Tick ~: set s ==> s @ [a] : Some_trace"
apply (insert decompo_app_in_Some_trace_if[of s "[a]"])
by (auto)

lemma decompo_last_in_Some_trace : 
  "s @ [a] : Some_trace = (Tick ~: set s)"
apply (insert decompo_app_in_Some_trace[of s "[a]"])
by (simp)

(*--------------------------*
 |        app not in        |
 *--------------------------*)

lemma app_None_notin_Some_trace_left:
   "s ~: Some_trace ==> t @ s ~: Some_trace"
apply (auto simp add: Some_trace_def)
apply (simp add: in_butlast_decompo)
apply (case_tac "s = []")
by (simp_all)

lemma app_None_notin_Some_trace_right:
   "s ~: Some_trace ==> s @ t ~: Some_trace"
apply (auto simp add: Some_trace_def)
apply (simp add: in_butlast_decompo)
apply (rule disjI1)
by (rule in_set_butlast, simp)

lemmas app_None_notin_Some_trace = 
       app_None_notin_Some_trace_left app_None_notin_Some_trace_right

(*******************************
            Tick
 *******************************)

lemma Tick_is_last : "Tick#s : Some_trace ==> s = []"
apply (case_tac "s = []")
by (auto simp add: Some_trace_def)

(*******************************
           not None
 *******************************)

lemma nil_not_None1[simp]: "[]t ~= None"
by (simp add: nilt_def Abs_trace_def)

lemma nil_not_None2[simp]: "None ~= []t"
by (simp add: nilt_def Abs_trace_def)

lemma event_not_None1[simp]: "[a]t ~= None"
by (simp add: Abs_trace_def)

lemma event_not_None2[simp]: "None ~= [a]t"
by (simp add: Abs_trace_def)

lemma list_not_None1[simp]: "t : Some_trace ==> Abs_trace t ~= None"
by (simp add: Abs_trace_def)

lemma list_not_None2[simp]: "t : Some_trace ==> None ~= Abs_trace t"
by (simp add: Abs_trace_def)

(*******************************
             Nil
 *******************************)

lemma one_neq_nil[simp]: "[a]t ~= []t"
by (simp add: nilt_def Abs_trace_inject)

lemma one_neq_nil_sym[simp]: "[]t ~= [a]t"
by (simp add: nilt_def Abs_trace_inject)

(*******************************
           notick
 *******************************)

(*** notick Ev ***)

lemma notick_Ev[simp]: "notick [Ev a]t"
apply (simp add: notick_def sett_def)
by (simp add: Abs_trace_inverse)

lemma notick_EvI: "(EX a. e = Ev a) ==> notick [e]t"
apply (simp add: notick_def sett_def)
by (auto simp add: Abs_trace_inverse)

(*** notick nil ***)

lemma notick_nil[simp]: "notick []t"
apply (simp add: notick_def nilt_def sett_def)
by (simp add: Abs_trace_inverse) 

(*** notick not None ***)
lemma notick_not_None[simp]: "~ notick None"
by (simp_all add: notick_def)

(*** notick not None ***)
lemma if_notick_not_None: "notick t ==> t ~= None"
by (simp_all add: notick_def)

(*** not notick Tick ***)
lemma not_notick_Tick[simp]: "~ notick [Tick]t"
apply (simp_all add: notick_def)
by (simp add: sett_def Abs_trace_inverse)

(*******************************
            Event
 *******************************)

lemma Event_eq[simp] : "([e1]t = [e2]t) = (e1 = e2)"
by (simp add: Abs_trace_inject)

(***********************************************************
                   @rep in trace
 ***********************************************************)

(*-----------------------------*
 |          s @rep t           |
 *-----------------------------*)

(*** only if ***)

lemma decompo_apprep_in_Some_trace_only_if:
  "[| s ~= None ; t ~= None ; (s @rep t) : Some_trace |] ==> (notick s | t = []t)"
apply (simp add: apprep_def decompo_app_in_Some_trace)
apply (simp add: nilt_def notick_def sett_def)
by (auto simp add: Rep_trace_Abs_trace_inverse_only_if)

(*** if ***)

lemma decompo_apprep_in_Some_trace_if:
  "(notick s | t = []t) ==> s @rep t : Some_trace"
apply (simp add: apprep_def decompo_app_in_Some_trace nilt_def)
apply (auto simp add: Abs_trace_inverse)
by (auto simp add: notick_def sett_def)

(*** iff ***)

lemma decompo_apprep_in_Some_trace:
  "[| s ~= None ; t ~= None |]
     ==> ((s @rep t) : Some_trace) = (notick s | t = []t)"
apply (rule iffI)
apply (simp add: decompo_apprep_in_Some_trace_only_if)
by (simp add: decompo_apprep_in_Some_trace_if)

(*** rule ***)

lemma decompo_apprep_in_Some_traceI:
  "s @rep t : Some_trace ==> (s = None | t = None | notick s | t = []t)"
apply (case_tac "s ~= None & t ~= None")
by (auto simp add: decompo_apprep_in_Some_trace_only_if)

lemma decompo_apprep_notin_Some_traceI:
  "s @rep t ~: Some_trace ==> (~ notick s & t ~= []t)"
apply (erule contrapos_np)
by (simp add: decompo_apprep_in_Some_trace_if)

(*** erule ***)

lemma decompo_apprep_in_Some_traceE:
  "[| s @rep t : Some_trace ; 
      s = None | t = None | notick s | t = []t ==> R |] ==> R"
by (simp add: decompo_apprep_in_Some_traceI)

lemma decompo_apprep_notin_Some_traceE:
  "[| s @rep t ~: Some_trace ;
      [| ~ notick s ; t ~= []t |] ==> R |] ==> R"
by (simp add: decompo_apprep_notin_Some_traceI)

(***********************************************************
                  lemmas for s @t t 
 ***********************************************************)

(*-----------------------------*
 | Abs_trace distribution on @ |
 *-----------------------------*)

lemma Abs_trace_app_dist[simp]:
  "Abs_trace s @t Abs_trace t = Abs_trace (s @ t)"
apply (simp add: appt_def)
apply (rule conjI)
apply (simp add: Abs_trace_None_notin_Some_trace)
apply (simp add: Abs_trace_None app_None_notin_Some_trace)

apply (rule conjI)
apply (simp add: Abs_trace_None_notin_Some_trace)
apply (simp add: Abs_trace_None app_None_notin_Some_trace)

apply (intro impI)
apply (elim conjE exE)
apply (simp add: apprep_def)
 apply (case_tac "s : Some_trace")
 apply (case_tac "t : Some_trace")
 apply (simp add: Abs_trace_inverse)
 by (simp_all add: not_None_eq Abs_trace_None)

(*                     test                          *)
(* lemma "[a,b]t @t [c,d,e]t = [a,b,c,d,e]t" by simp *)

(***********************************************************
                    s @t t <==> s @rep t
 ***********************************************************)

(*--------------------------*
 |       def or undef       |
 *--------------------------*)

lemma appt_apprep_defined:
  "[| notick s | t = []t ; s ~= None ; t ~= None |]
     ==> s @t t = Some (Abs_Some_trace (s @rep t))"
apply (simp add: appt_def Abs_trace_def)
by (simp add: decompo_apprep_in_Some_trace)

(*--------------------------*
 |       decompo cons       |
 *--------------------------*)

lemma appt_apprep_cons:
  "s ~= None ==> [a]t @t s = Abs_trace (a # Rep_trace s)"
apply (simp add: appt_def apprep_def)
by (simp add: Abs_trace_inverse)

(*--------------------------*
 |       decompo last       |
 *--------------------------*)

lemma appt_apprep_last:
  "notick t ==> t @t [e]t = Abs_trace (Rep_trace t @ [e])"
apply (simp add: appt_def apprep_def if_notick_not_None)
by (simp add: Abs_trace_inverse)

lemma appt_Some_last:
  "notick s ==> s @t [a]t = Some (Abs_Some_trace (Rep_trace s @ [a]))"
apply (simp add: appt_apprep_last)
apply (simp add: notick_def sett_def)
by (auto simp add: Abs_trace_def decompo_last_in_Some_trace_if)

lemma appt_None_last:
  "~ notick s ==> s @t [a]t = None"
apply (simp add: appt_def)
apply (intro impI)
apply (case_tac "s @rep [a]t ~: Some_trace")
apply (simp add: Abs_trace_None)
by (simp add: decompo_apprep_in_Some_trace)

lemma appt_None_last_contrapos:
  "s @t [a]t ~= None ==> notick s"
apply (erule contrapos_np)
by (simp add: appt_None_last)

(***********************************************************
                  lemmas for s @t t 
 ***********************************************************)

lemma appt_nil_left[simp]: "[]t @t s = s"
apply (case_tac "s ~= None")
apply (simp add: appt_def apprep_def)
apply (simp add: nilt_def)
apply (simp add: Abs_trace_inverse Rep_trace_inverse)
by (simp add: appt_def)

lemma appt_nil_right[simp]: "s @t []t = s"
apply (case_tac "s ~= None")
apply (simp add: appt_def apprep_def)
apply (simp add: nilt_def)
apply (simp add: Abs_trace_inverse Rep_trace_inverse)
by (simp add: appt_def)

lemma event_app_not_nil_left[simp]: "[e]t @t s ~= []t"
apply (simp add: appt_def)
apply (case_tac "[e]t @rep s : Some_trace")
apply (simp add: nilt_def)
apply (simp add: Abs_trace_inject)
apply (simp add: apprep_def Abs_trace_inverse)

by (simp add: Abs_trace_None)

lemma event_app_not_nil_right[simp]: "s @t [e]t ~= []t"
apply (simp add: appt_def)
apply (case_tac "s @rep [e]t : Some_trace")
apply (simp add: nilt_def)
apply (simp add: Abs_trace_inject)
apply (simp add: apprep_def Abs_trace_inverse)

by (simp add: Abs_trace_None)

(***********************************************************
                 induction for traces
 ***********************************************************)

(*** induction ***)

lemma induct_event_list:
  "s : Some_trace &
   P []t & P [Tick]t &
   (ALL s a. (P (Abs_trace s) & Abs_trace s ~= None) --> P ([Ev a]t @t (Abs_trace s)))
    --> P (Abs_trace s)"
apply (simp only: Abs_trace_not_None_in_Some_trace)
apply (induct_tac s)

(* base case *)
apply (simp add: nilt_def)

(* step case *)
apply (intro impI)
apply (simp add: decompo_head_in_Some_trace)

apply (insert event_tick_or_Ev)
apply (drule_tac x="a" in spec)
by (auto)

(*** rule ***)

lemma induct_trace:
  "[| P None ; P []t ; P [Tick]t ; 
      !! (s::'a trace) a. [| P s ; s ~= None |] ==> P ([Ev a]t @t s) |]
    ==> P (s)"
apply (insert induct_event_list[of "Rep_trace s" P])
apply (case_tac "s = None")
by (simp_all add: Rep_trace_inverse del: Abs_trace_app_dist)

(*------------------------------------------------------*
 |  use this induction rule "induct_trace" as follows:  |
 |                                                      |
 |      lemma test_induction: "test (s::'a trace)"      |
 |      apply (induct_tac s rule: induct_trace)         |
 |                                                      |
 *------------------------------------------------------*)

(*** reverse induction ***)

lemma rev_induct_event_list_lm1:
  "notick (Abs_trace s) = (Tick ~: set s & s : Some_trace)"
apply (simp add: notick_def sett_def)
apply (simp only: Abs_trace_not_None_in_Some_trace)
by (auto simp add: Abs_trace_inverse)

lemma rev_induct_event_list:
  "s : Some_trace &
   P []t & 
   (ALL s e. (P (Abs_trace s) & notick (Abs_trace s))
    --> P ((Abs_trace s) @t [e]t))
    --> P (Abs_trace s)"
apply (simp only: rev_induct_event_list_lm1)
apply (induct_tac s rule: rev_induct)

(* base case *)
apply (simp add: nilt_def)

(* step case *)
by (simp add: decompo_last_in_Some_trace)

(*** rule ***)

lemma rev_induct_trace:
  "[| P None ; P []t ; 
      !! (s::'a trace) e. [| P s ; notick s |] ==> P (s @t [e]t) |]
    ==> P (s)"
apply (insert rev_induct_event_list[of "Rep_trace s" P])
apply (case_tac "s = None")
by (simp_all add: Rep_trace_inverse del: Abs_trace_app_dist)

(*----------------------------------------------------------*
 |  use this induction rule "rev_induct_trace" as follows:  |
 |                                                          |
 |      lemma test_induction: "test (s::'a trace)"          |
 |      apply (induct_tac s rule: rev_induct_trace)         |
 |                                                          |
 *----------------------------------------------------------*)

(***********************************************************
                   convenient lemmas
 ***********************************************************)

lemma appt_ass_lm1 : "(s @ t) @ u ~: S ==> s @ (t @ u) ~: S"
by (simp)

(*--------------------------*
 |   associativity of @t    |
 *--------------------------*)

lemma appt_ass[simp] : "(s @t t) @t u = s @t (t @t u)"
apply (simp add: appt_def)
apply (auto)

(* None = ... *)
 apply (rule sym)
 apply (simp add: Abs_trace_None_notin_Some_trace)
 apply (rotate_tac 1, drule sym)
 apply (simp add: apprep_def)

  apply (case_tac "(Rep_trace (Some yb) @ Rep_trace (Some y)) : Some_trace")
  apply (simp add: Abs_trace_inverse)
  apply (rule appt_ass_lm1)
  apply (rule app_None_notin_Some_trace_right)
  apply (simp)

  (* not case *)
  apply (simp add: Abs_trace_None)

(* ... = None *)
 apply (simp add: Abs_trace_None_notin_Some_trace)
 apply (drule sym)
 apply (simp add: apprep_def)

  apply (case_tac "(Rep_trace (Some ya) @ Rep_trace (Some yc)) : Some_trace")
  apply (simp add: Abs_trace_inverse)
  apply (rule app_None_notin_Some_trace_left)
  apply (simp)

  (* not case *)
  apply (simp add: Abs_trace_None)

(* ... = ... *)
 apply (drule sym)
 apply (drule sym)
 apply (simp add: apprep_def)
  apply (case_tac "(Rep_trace (Some ya) @ Rep_trace (Some yc)) : Some_trace")
  apply (case_tac "(Rep_trace (Some yc) @ Rep_trace (Some y)) : Some_trace")
  apply (simp_all add: Abs_trace_inverse Abs_trace_None)
done

lemma appt_ass_rev : "s @t (t @t u) = (s @t t) @t u"
by (simp)

(*** nil ***)

lemma appt_nil[simp]: "(s @t t = []t) = (s = []t & t = []t)"
apply (rule iffI)
apply (simp_all)

apply (simp add: appt_def)
apply (case_tac "s = None | t = None")
apply (simp_all)
apply (case_tac "s @rep t : Some_trace")
 apply (simp add: nilt_def)
 apply (simp add: Abs_trace_inject)
 apply (simp add: apprep_def)
 apply (simp add: Rep_trace_Abs_trace_inverse_only_if)

 apply (simp add: Abs_trace_None)
done

lemma appt_nil_sym[simp]: "([]t = s @t t) = (s = []t & t = []t)"
apply (auto)
by (drule sym, simp)+

(*---------------------------*
 |   decompo appt not None   |
 *---------------------------*)

(*** only if ***)

lemma decompo_appt_not_None_rep_only_if:
  "s @t t ~= None ==> (s ~= None & t ~= None & s @rep t : Some_trace)"
apply (simp add: appt_def)
apply (case_tac "s = None | t = None")
apply (simp)
apply (case_tac "s @rep t : Some_trace")
by (simp_all add: Abs_trace_None)

(*** if ***)

lemma decompo_appt_not_None_rep_if:
  "(s ~= None & t ~= None & s @rep t : Some_trace) ==> s @t t ~= None"
by (simp add: appt_def Abs_trace_def)

(*** iff ***)

lemma decompo_appt_not_None_rep:
  "(s @t t ~= None) = (s ~= None & t ~= None & s @rep t : Some_trace)"
apply (rule iffI)
apply (rule decompo_appt_not_None_rep_only_if, simp)
by (simp add: decompo_appt_not_None_rep_if)

(*** notick or nil ***)

(*** only if ***)

lemma decompo_appt_not_None_only_if:
  "s @t t ~= None ==> (s ~= None & t ~= None & (notick s | t = []t))"
apply (insert decompo_appt_not_None_rep_only_if[of s t])
by (auto simp add: decompo_apprep_in_Some_trace)

(*** if ***)

lemma decompo_appt_not_None_if:
  "(s ~= None & t ~= None & (notick s | t = []t)) ==> s @t t ~= None"
apply (insert decompo_appt_not_None_rep_if[of s t])
by (auto simp add: decompo_apprep_in_Some_trace)

(*** iff ***)

lemma decompo_appt_not_None1:
  "(s @t t ~= None) = (s ~= None & t ~= None & (notick s | t = []t))"
apply (rule iffI)
apply (rule decompo_appt_not_None_only_if, simp)
by (simp add: decompo_appt_not_None_if)

lemma decompo_appt_not_None2:
  "(None ~= s @t t) = (s ~= None & t ~= None & (notick s | t = []t))"
apply (insert decompo_appt_not_None1[of s t])
apply (drule sym)
by (auto)

lemmas decompo_appt_not_None = decompo_appt_not_None1 decompo_appt_not_None2

(*---------------------------*
 |     decompo appt None     |
 *---------------------------*)

lemma decompo_appt_None1:
  "(s @t t = None) = (s = None | t = None | (~ notick s & t ~= []t))"
apply (rule iffI)
apply (erule contrapos_pp)
apply (simp add: decompo_appt_not_None)
apply (erule contrapos_pp)
apply (simp add: decompo_appt_not_None)
done

lemma decompo_appt_None2:
  "(None = s @t t) = (s = None | t = None | (~ notick s & t ~= []t))"
apply (insert decompo_appt_None1[of s t])
apply (drule sym)
by (auto)

lemmas decompo_appt_None = decompo_appt_None1 decompo_appt_None2

(*---------------------------*
 |          appt None        |
 *---------------------------*)

(*** appt None ***)

lemma appt_None_left[simp]: "None @t s = None"
by (simp add: appt_def Abs_trace_def)

lemma appt_None_right[simp]: "s @t None = None"
by (simp add: appt_def Abs_trace_def)

lemma appt_None_Ev[simp]: "([Ev a]t @t s = None) = (s = None)"
by (simp add: appt_def decompo_apprep_in_Some_trace_if)

lemma appt_None_Ev_sym[simp]: "(None = [Ev a]t @t s) = (s = None)"
by (simp add: appt_def decompo_apprep_in_Some_trace_if)

(*---------------------------*
 |      appt None or not     |
 *---------------------------*)

lemma appt_last_not_None_left: "notick s ==> s @t [e]t ~= None"
by (simp add: appt_Some_last)

lemma appt_last_not_None_right: "notick s ==> None ~= s @t [e]t"
by (simp add: appt_Some_last)

lemmas appt_last_not_None = appt_last_not_None_left appt_last_not_None_right

lemma appt_last_None[simp]: "~ notick s ==> s @t [e]t = None"
by (simp add: decompo_appt_None)

lemma appt_notick_None: "[| notick s ; t ~= None |] ==> s @t t ~= None"
apply (simp add: appt_def)
apply (case_tac "s ~= None", simp)
apply (simp add: decompo_apprep_in_Some_trace_if Abs_trace_inverse)
by (simp)

lemma appt_head_not_None: "s ~= None ==> [Ev a]t @t s ~= None"
by (simp add: appt_def decompo_apprep_in_Some_trace_if)

lemmas appt_not_None = appt_last_not_None appt_notick_None appt_head_not_None

(*--------------------------*
 |         length           |
 *--------------------------*)

(*** 0 ***)
lemma lengtht_nil_zero[simp]: "lengtht ([]t) = 0"
apply (simp add: nilt_def lengtht_def)
by (simp add: Abs_trace_inverse)

lemma lengtht_None_zero[simp]: "lengtht (None) = 0"
by (simp add: lengtht_def)

(*** 1 ***)
lemma lengtht_one_event[simp]: "lengtht ([e]t) = Suc 0"
apply (simp add: lengtht_def)
by (simp add: Abs_trace_inverse)

(*** length + 1 ***)

lemma lengtht_app_event_Suc_last[simp]:
  "notick s ==> lengtht (s @t [a]t) = Suc (lengtht s)"
apply (simp add: appt_def lengtht_def)
apply (simp add: Abs_trace_inverse decompo_apprep_in_Some_trace_if)
apply (simp add: apprep_def)
apply (simp add: Abs_trace_inverse)
by (simp add: notick_def)

lemma lengtht_app_event_Suc_head[simp]:
  "[| s ~= None ; s ~= []t |] ==> lengtht ([Ev a]t @t s) = Suc (lengtht s)"
apply (simp add: appt_def lengtht_def)
apply (simp add: Abs_trace_inverse decompo_apprep_in_Some_trace_if)
apply (simp add: apprep_def)
by (simp add: Abs_trace_inverse)

(*** app length ***)

lemma lengtht_app_decompo1[simp]:
  "[| s ~= None ; t ~= None ; notick s |] 
      ==> lengtht (s @t t) = lengtht s + lengtht t"
apply (simp add: appt_def lengtht_def)
apply (simp add: Abs_trace_inverse decompo_apprep_in_Some_trace_if)
by (simp add: apprep_def)

lemma lengtht_app_decompo2[simp]:
  "s @t t ~= None 
      ==> lengtht (s @t t) = lengtht s + lengtht t"
apply (case_tac "t = []t", simp)
by (simp add: decompo_appt_not_None)

(*---------------------------*
 |           sett            |
 *---------------------------*)

(*** None ***)

lemma sett_None[simp]: "sett None = {}"
by (simp add: sett_def)

(*** nil ***)

lemma sett_nil[simp]: "sett []t = {}"
apply (simp add: sett_def)
by (simp add: nilt_def Abs_trace_inverse)

(*** one ***)

lemma sett_one[simp]: "sett [e]t = {e}"
apply (simp add: sett_def)
by (simp add: Abs_trace_inverse)

(*** appt ***)

lemma sett_appt[simp]:
  "s @t t ~= None ==> sett (s @t t) = sett s Un sett t"
apply (simp add: decompo_appt_not_None_rep)
apply (simp add: sett_def appt_def)
apply (simp add: Abs_trace_inverse)
by (simp add: apprep_def)

(*---------------------------*
 |     decompo appt Tick     |
 *---------------------------*)

(*** only if ***)

lemma decompo_appt_notick_only_if:
  "notick (s @t t) ==> (notick s & notick t)"
apply (simp add: notick_def)
apply (elim conjE)
by (simp add: decompo_appt_not_None_rep)

(*** if ***)

lemma decompo_appt_notick_if:
  "[| notick s ; notick t |] ==> notick (s @t t)"
apply (simp add: notick_def)
apply (elim conjE)

apply (case_tac "s @rep t : Some_trace")
 apply (simp add: decompo_appt_not_None_rep)
 apply (erule decompo_apprep_notin_Some_traceE)
 apply (simp add: notick_def)
done

(*** iff ***)

lemma decompo_appt_notick[simp]:
  "notick (s @t t) = (notick s & notick t)"
apply (rule iffI)
apply (rule decompo_appt_notick_only_if, simp)
by (simp add: decompo_appt_notick_if)

(*---------------------------*
 |   a trace is ... or ...   |
 *---------------------------*)

(*** trace --> nil or Tick or etc ***)

lemma trace_nil_or_Tick_or_Ev: 
  "ALL t. t ~= None --> ((t = []t) | (t = [Tick]t) | (EX a s. t=[Ev a]t @t s))"
apply (intro allI)
apply (induct_tac t rule: induct_trace)
by (auto)

(*** trace --> nil or unnil ***)

lemma trace_nil_or_unnil: 
  "ALL t. t ~= None --> ((t = []t) | (EX a s. t=[a]t @t s))"
apply (intro allI)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="t" in spec)
apply (intro impI, simp)

apply (erule disjE, simp)

apply (erule disjE)
apply (rule disjI2)
apply (rule_tac x="Tick" in exI)
apply (rule_tac x="[]t" in exI)
apply (simp)

apply (rule disjI2)
apply (elim exE)
apply (rule_tac x="Ev a" in exI)
apply (rule_tac x="s" in exI)
by (simp)

(*** trace --> nil or unnil (last) ***)

lemma trace_last_nil_or_unnil: 
  "ALL t. t ~= None --> ((t = []t) | (EX s a. notick s & t = s @t [a]t))"
apply (intro allI)
apply (induct_tac t rule: rev_induct_trace)
by (auto)

(*** trace --> notick or tick (last) ***)

lemma trace_last_notick_or_tick: 
  "ALL t. t ~= None --> (notick t | (EX s. notick s & t = s @t [Tick]t))"
apply (intro allI impI)
apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="t" in spec, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (insert event_tick_or_Ev)
 apply (drule_tac x="a" in spec)
  apply (erule disjE, simp)        (* Tick *)
  apply (rule_tac x="s" in exI, simp)
  apply (elim exE, simp)
done

(*---------------------------*
 |     head must be last     |
 *---------------------------*)

lemma appt_Tick_nil_only_if: "[Tick]t @t s ~= None ==> s = []t"
apply (simp add: appt_def)
apply (case_tac "s = None", simp, simp)
apply (case_tac "[Tick]t @rep s ~: Some_trace")
apply (simp add: Abs_trace_None)
apply (case_tac "s = []t", simp)
by (simp add: decompo_apprep_in_Some_trace)

lemma appt_Tick_nil[simp]: "([Tick]t @t s ~= None) = (s = []t)"
apply (rule iffI)
by (simp_all add: appt_Tick_nil_only_if)

lemma appt_Tick_nil_contrapos[simp]: "([Tick]t @t s = None) = (s ~= []t)"
apply (rule iffI)
apply (case_tac "s ~= []t", simp, simp)
by (case_tac "[Tick]t @t s = None", simp, simp)

lemma appt_unnil_Tick_None: "s ~= []t ==> [Tick]t @t s = None"
by (simp)

lemma appt_Tick_unnil: "s ~= []t ==> [Tick]t @t s = None"
by (simp)

(*---------------------------*
 |    same head and last     |
 *---------------------------*)

(*** same head ***)

lemma appt_same_head_only_if: 
  "[| (s ~= None | t ~= None) ; [Ev a]t @t s = [Ev b]t @t t |]
      ==> a = b & s = t"
apply (case_tac "s ~= None & t ~= None")
apply (simp add: appt_apprep_cons)
apply (simp add: Abs_trace_inject decompo_head_in_Some_trace_if)
apply (simp add: Rep_trace_inject)

apply (erule disjE)
apply (case_tac "t = None", simp, simp)
apply (case_tac "s = None", simp, simp)
done

lemma appt_same_head[simp]: 
  "(s ~= None | t ~= None)
      ==> ([Ev a]t @t s = [Ev b]t @t t) = (a = b & s = t)"
apply (rule iffI)
apply (rule appt_same_head_only_if)
by (simp_all)

(*** same last ***)

lemma appt_same_last_only_if: 
  "[| (notick s | notick t) ; s @t [a]t = t @t [b]t |]
      ==> s = t & a = b"
apply (case_tac "notick s & notick t")
apply (simp add: appt_apprep_last)
apply (simp add: notick_def sett_def)
apply (elim conjE)
apply (simp add: Abs_trace_inject decompo_last_in_Some_trace_if)
apply (simp add: Rep_trace_inject)
by (auto simp: appt_Some_last appt_None_last)

lemma appt_same_last[simp]: 
  "(notick s | notick t) ==> (s @t [a]t = t @t [b]t) = (s = t & a = b)"
apply (rule iffI)
apply (rule appt_same_last_only_if)
by (simp_all)

(*---------------------------*
 |     appt decompo one      |
 *---------------------------*)

lemma appt_decompo_one_only_if:
  "s @t t = [a]t ==> (s = [a]t & t = []t) | (s = []t & t = [a]t)"
apply (simp add: appt_def)
apply (case_tac "s = None | t = None", simp)
apply (case_tac "s @rep t ~: Some_trace", simp add: Abs_trace_None)
apply (simp add: Abs_trace_inject)
apply (simp add: apprep_def list_app_decompo_one)
by (auto simp add: Abs_trace_Rep_trace_inverse nilt_def)

lemma appt_decompo_one[simp]:
  "(s @t t = [a]t) = ((s = [a]t & t = []t) | (s = []t & t = [a]t))"
apply (rule iffI)
apply (simp add: appt_decompo_one_only_if)
by (auto)

lemma appt_decompo_one_sym[simp]:
  "([a]t = s @t t) = ((s = [a]t & t = []t) | (s = []t & t = [a]t))"
apply (rule iffI)
apply (drule sym, simp)
by (rule sym, simp)

(*---------------------------*
 |     same_head + Tick      |
 *---------------------------*)

lemma appt_same_head_Tick_left: 
  "t ~= None
      ==> ([e]t @t s = [Ev a]t @t t) = (e = Ev a & s = t)"
apply (insert event_tick_or_Ev)
apply (drule_tac x="e" in spec)
apply (erule disjE)
apply (simp)
apply (case_tac "[Tick]t @t s ~= [Ev a]t @t t", simp)
apply (simp)
apply (case_tac "s = []t", simp)
apply (simp add: appt_Tick_unnil)

apply (erule exE)
by (simp)

lemma appt_same_head_Tick_right: 
  "t ~= None
      ==> ([Ev a]t @t t = [e]t @t s) = (e = Ev a & s = t)"
apply (insert appt_same_head_Tick_left[of t e s a])
apply (simp)
apply (drule sym)
apply (rule iffI)
by (simp_all)

lemmas appt_same_head_Tick[simp] 
     = appt_same_head_Tick_left appt_same_head_Tick_right

(******************************************************************
                        head and tail
 ******************************************************************)

(*** tl : Some_trace ***)

lemma tlt_Some_trace:
  "[| s : Some_trace ; s ~= [] |] ==> tl s : Some_trace"
apply (simp add: Some_trace_def)
apply (insert list_nil_or_unnil)
apply (drule_tac x="s" in spec)

apply (erule disjE, simp)
apply (elim exE, simp)
by (case_tac "sa = []", simp, simp)

(*** tlt None ***)

lemma tlt_not_None:
  "[| s ~= None ; s ~= []t |] ==> tlt s ~= None"
apply (simp add: tlt_def)
apply (insert tlt_Some_trace[of "Rep_trace s"])
apply (simp add: nilt_def)
apply (case_tac "Rep_trace s = []")
apply (simp add: Rep_trace_Abs_trace_inverse_only_if)
by (simp)

lemma tlt_not_None_contrapos:
  "[| tlt s = None ; s ~= []t |] ==> s = None"
apply (erule contrapos_pp)
by (simp add: tlt_not_None)

lemma tlt_None[simp]: "tlt None = None"
by (simp add: tlt_def)

(*** head !! ***)

lemma hdt_appt[simp]: "s ~= None ==> hdt ([Ev a]t @t s) = Ev a"
apply (simp add: appt_def)
apply (simp add: hdt_def)
apply (simp add: decompo_apprep_in_Some_trace_if Abs_trace_inverse)
apply (simp add: apprep_def)
by (simp add: Abs_trace_inverse)

(* one *)

lemma hdt_one[simp]: "hdt [a]t = a"
apply (simp add: hdt_def)
by (simp add: Abs_trace_inverse)

(*** tail !! ***)

lemma tlt_appt[simp]: "tlt ([Ev a]t @t s) = s"
apply (simp add: appt_def)
apply (simp add: tlt_def)
apply (simp add: decompo_apprep_in_Some_trace_if Abs_trace_inverse)
apply (simp add: apprep_def)
by (simp add: Abs_trace_inverse Rep_trace_inverse)

(* one *)

lemma tlt_one[simp]: "tlt [a]t = []t"
apply (simp add: tlt_def)
by (simp add: Abs_trace_inverse nilt_def)

(*** head + tail ***)

lemma hdt_appt_tail[simp]: "s ~= []t ==> [hdt s]t @t (tlt s) = s"
apply (case_tac "s = None", simp)

apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)
apply (simp)
apply (erule disjE, simp)
by (elim exE, simp)

(******************************************************************
                        butlast & last
 ******************************************************************)

(*** butlast : Some_trace ***)

lemma butlast_Some_trace:
  "[| s : Some_trace ; s ~= [] |] ==> butlast s : Some_trace"
by (simp add: Some_trace_def notin_set_butlast)

lemma butlast_Some_trace_Rep:
  "s ~= []t ==> butlast (Rep_trace s) : Some_trace"
apply (insert Rep_trace[of s])
apply (case_tac "Rep_trace s ~= []")
apply (simp add: Some_trace_def)
apply (simp add: notin_set_butlast)
by (simp)

(*** tlt None ***)

lemma batlastt_not_None:
  "[| s ~= None ; s ~= []t |] ==> butlastt s ~= None"
apply (simp add: butlastt_def)
apply (simp add: nilt_def)
apply (case_tac "butlast (Rep_trace s) : Some_trace")
apply (simp add: Abs_trace_def)
apply (insert Rep_trace[of s])
apply (simp add: Some_trace_def notin_set_butlast)
done

lemma batlastt_not_None_contrapos:
  "[| butlastt s = None ; s ~= []t |] ==> s = None"
apply (erule contrapos_pp)
by (simp add: batlastt_not_None)

lemma batlastt_None[simp]: "butlastt None = None"
by (simp add: butlastt_def)

(*** last !! ***)

lemma lastt_appt[simp]: "notick s ==> lastt (s @t [e]t) = e"
apply (simp add: appt_def)
apply (simp add: lastt_def if_notick_not_None)
apply (simp add: decompo_apprep_in_Some_trace_if Abs_trace_inverse)
by (simp add: apprep_def Abs_trace_inverse)

(* one *)

lemma lastt_one[simp]: "lastt [a]t = a"
apply (simp add: lastt_def)
by (simp add: Abs_trace_inverse)

(*** butlast !! ***)

lemma butlastt_appt[simp]: "notick s ==> butlastt (s @t [e]t) = s"
apply (simp add: appt_def)
apply (simp add: butlastt_def decompo_apprep_in_Some_trace_if)
apply (simp add: Abs_trace_inverse decompo_apprep_in_Some_trace_if)
apply (simp add: apprep_def Abs_trace_inverse)
by (simp add: Rep_trace_inverse)

(* one *)

lemma butlastt_one[simp]: "butlastt [a]t = []t"
apply (simp add: butlastt_def)
by (simp add: Abs_trace_inverse nilt_def)

(*** butlast + last ***)

lemma butlastt_appt_lastt[simp]: "s ~= []t ==> (butlastt s) @t [lastt s]t = s"
apply (case_tac "s = None", simp)

apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="s" in spec)
apply (simp)
apply (elim conjE exE)
by (simp)

(******************************************************************
                        notick + alpha
 ******************************************************************)

(* tick in *)

lemma not_notick_unnil[simp]: "~ notick s ==> s ~= []t"
by (case_tac "s ~= []t", simp_all)

(* notick butlastt *)

lemma notick_butlast: "[| s ~= None ; s ~= []t |] ==> notick (butlastt s)"
apply (simp add: butlastt_def)
apply (simp add: notick_def sett_def)
apply (simp add: butlast_Some_trace_Rep Abs_trace_inverse)
apply (insert Rep_trace[of s])
by (simp add: Some_trace_def)

(* tick and butlastt *)

lemma tick_decompo: "ALL s. ~ notick s --> s = ((butlastt s) @t [Tick]t)"
apply (intro allI impI)
apply (case_tac "s = None", simp)

apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="s" in spec)
apply (simp)

apply (elim conjE exE)
by (simp add: notick_def)

(******************************************************************
                         lengtht plus
 ******************************************************************)

(*** lengtht zero ***)

lemma lengtht_zero: "(lengtht s = 0) = (s = []t | s = None)"
apply (induct_tac s rule: induct_trace)
by (simp_all)

(*** lengtht one ***)

lemma lengtht_one: "(lengtht s = Suc 0) = (EX e. s = [e]t)"
apply (induct_tac s rule: induct_trace)
apply (simp_all)
by (simp add: lengtht_zero)

(******************************************************************
                            not None
 ******************************************************************)

lemmas not_None = if_notick_not_None appt_not_None
                  tlt_not_None batlastt_not_None

(******************************************************************
                          in Some_trace
 ******************************************************************)

lemmas in_Some_trace = decompo_apprep_in_Some_trace_if
                       decompo_app_in_Some_trace_if
                       decompo_head_in_Some_trace_if
                       decompo_last_in_Some_trace_if
                       tlt_Some_trace
                       butlast_Some_trace

(******************************************************************
                         convenient lemmas
 ******************************************************************)

(*-------------------*
 |  for Seq_compo T1 |
 *-------------------*)

lemma appt_decompo_lm: 
  "ALL s1 s2 t1 t2.
   s1 @t s2 ~= None
       --> (s1 @t s2 = t1 @t t2) 
           = ((EX u. s1 @t u = t1 & s2 = u @t t2) |
              (EX u. s1 = t1 @t u & u @t s2 = t2))"
apply (rule allI)
apply (induct_tac s1 rule: induct_trace)
apply (simp_all)
apply (force)
apply (force)
apply (intro allI impI)
apply (drule_tac x="s2" in spec, simp)

apply (rule iffI)
 (* => *)
 apply (case_tac "t1 = None", simp)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="t1" in spec, simp)
 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim exE, simp)     (* t1 = [Ev aa]t @t sa *)
 apply (drule_tac x="sa" in spec)
 apply (drule_tac x="t2" in spec)
 apply (simp)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule disjI2)
 apply (rule_tac x="u" in exI)
 apply (fast)

 (* <= *)
 apply (elim disjE conjE exE)
 apply (simp del: appt_ass add: appt_ass_rev)
 apply (simp del: appt_ass add: appt_ass_rev)
 apply (simp)
done

lemma appt_decompo: 
  "s1 @t s2 ~= None
   ==> (s1 @t s2 = t1 @t t2) 
       = ((EX u. s1 @t u = t1 & s2 = u @t t2) |
          (EX u. s1 = t1 @t u & u @t s2 = t2))"
by (simp add: appt_decompo_lm)

(*-------------------*
 |  for Seq_compo T2 |
 *-------------------*)

lemma notick_or_last_Tick: 
  "ALL s. s ~= None --> notick s | (EX t. s = t @t [Tick]t)"
apply (rule allI)
apply (induct_tac s rule: rev_induct_trace)
apply (simp_all)
apply (intro impI)
apply (insert event_tick_or_Ev)
apply (drule_tac x="e" in spec)
by (auto)

(****************** to add it again ******************)

declare disj_not1 [simp] 
declare not_None_eq [simp] 

end