Theory Trace_par

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

theory Trace_par = Prefix:

(*  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]

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

         1. s |[X]|list t  : lists  --> list set
         2. s |[X]|tr t   : traces --> trace set
         3. 
         4. 

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

consts
  parx :: "'a set => (nat * 'a trace * 'a trace * 'a trace) set"

inductive "parx X"
intros
parx_nil_nil: 
  "(0, []t, []t, []t) : parx X"

parx_Tick_Tick: 
  "(0, [Tick]t, [Tick]t, [Tick]t) : parx X"

parx_Ev_nil: 
  "[| (n, u, s, []t) : parx X ; a ~: X |]
   ==> (Suc n, [Ev a]t @t u, [Ev a]t @t s, []t) : parx X"

parx_nil_Ev: 
  "[| (n, u, []t, t) : parx X ; a ~: X |]
   ==> (Suc n, [Ev a]t @t u, []t, [Ev a]t @t t) : parx X"

parx_Ev_sync: 
  "[| (n, u, s, t) : parx X ; a : X |]
   ==> (Suc n, [Ev a]t @t u, [Ev a]t @t s, [Ev a]t @t t) : parx X"

parx_Ev_left: 
  "[| (n, u, s, t) : parx X ; a ~: X |]
   ==> (Suc n, [Ev a]t @t u, [Ev a]t @t s, t) : parx X"

parx_Ev_right: 
  "[| (n, u, s, t) : parx X ; a ~: X |]
   ==> (Suc n, [Ev a]t @t u, s, [Ev a]t @t t) : parx X"

consts
  par_tr :: "'a trace => 'a set => 'a trace => 'a trace set"
                                        ("(_ |[_]|tr _)" [76,0,77] 76)

defs
  par_tr_def : "s |[X]|tr t == {u. EX n. (n, u, s, t) : parx X}"

lemma par_tr_defE: "[| u : s |[X]|tr t ; EX n. (n, u, s, t) : parx X ==> R |] ==> R"
by (simp add: par_tr_def)

(*************************************************************
                       parx imples "not None"
 *************************************************************)

lemma parx_not_None_imp: 
  "ALL X n u s t. (n, u, s, t) : parx X --> (u ~= None & s ~= None & t ~= None)"
apply (rule allI)
apply (rule allI)
apply (induct_tac n)
apply (intro allI impI)
apply (erule parx.elims)
apply (simp_all)

(* step case *)
apply (intro allI impI)
apply (erule parx.elims)
by (simp_all)

(*** rule ***)

lemma parx_not_None: 
  "(n, u, s, t) : parx X ==> (u ~= None & s ~= None & t ~= None)"
by (simp add: parx_not_None_imp)

(*** par_tr ***)

lemma par_tr_not_None_imp: 
  "ALL X u s t. u : s |[X]|tr t --> (u ~= None & s ~= None & t ~= None)"
apply (simp add: par_tr_def)
apply (intro allI impI)
apply (erule exE)
by (simp add: parx_not_None)

(*** rule ***)

lemma par_tr_not_None: 
  "u : s |[X]|tr t ==> (u ~= None & s ~= None & t ~= None)"
by (simp add: par_tr_not_None_imp)

(*** None False ***)

lemma par_tr_None_False1[simp]: 
  "None : s |[X]|tr t = False"
apply (case_tac "~ None : s |[X]|tr t", simp)
apply (insert par_tr_not_None[of "None" s X t])
by (simp)

lemma par_tr_None_False2[simp]: 
  "u : None |[X]|tr t = False"
apply (case_tac "~ u : None |[X]|tr t", simp)
apply (insert par_tr_not_None[of u "None" X t])
by (simp)

lemma par_tr_None_False3[simp]: 
  "u : s |[X]|tr None = False"
apply (case_tac "~ u : s |[X]|tr None", simp)
apply (insert par_tr_not_None[of u s X "None"])
by (simp)

(*************************************************************
                 par_tr intros and elims
 *************************************************************)

(*-------------------*
 |      intros       |
 *-------------------*)

lemma par_tr_nil_nil: 
  "[]t : []t |[X]|tr []t"
apply (simp add: par_tr_def)
apply (rule_tac x="0" in exI)
by (simp add: parx.intros)

lemma par_tr_Tick_Tick: 
  "[Tick]t : [Tick]t |[X]|tr [Tick]t"
apply (simp add: par_tr_def)
apply (rule_tac x="0" in exI)
by (simp add: parx.intros)

lemma par_tr_Ev_nil: 
  "[| u : s |[X]|tr []t ; a ~: X |]
   ==> [Ev a]t @t u : ([Ev a]t @t s) |[X]|tr []t"
apply (simp add: par_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: parx.intros)

lemma par_tr_nil_Ev: 
  "[| u : []t |[X]|tr t ; a ~: X |]
   ==> [Ev a]t @t u : []t |[X]|tr ([Ev a]t @t t)"
apply (simp add: par_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: parx.intros)

lemma par_tr_Ev_sync: 
  "[| u : s |[X]|tr t ; a : X |]
   ==> [Ev a]t @t u : ([Ev a]t @t s) |[X]|tr ([Ev a]t @t t)"
apply (simp add: par_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: parx.intros)

lemma par_tr_Ev_left: 
  "[| u : s |[X]|tr t ; a ~: X |]
   ==> [Ev a]t @t u : ([Ev a]t @t s) |[X]|tr t"
apply (simp add: par_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: parx.intros)

lemma par_tr_Ev_right: 
  "[| u : s |[X]|tr t ; a ~: X |]
   ==> [Ev a]t @t u : s |[X]|tr ([Ev a]t @t t)"
apply (simp add: par_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: parx.intros)

(*** intro rule ***)

lemmas par_tr_intros =
       par_tr_nil_nil
       par_tr_Tick_Tick
       par_tr_Ev_nil
       par_tr_nil_Ev
       par_tr_Ev_sync
       par_tr_Ev_left
       par_tr_Ev_right

(*-------------------*
 |       elims       |
 *-------------------*)

lemma par_tr_elims_lm:
 "[| u : s |[X]|tr t ;
     u ~= None ;
     s ~= None ;
     t ~= None ;
     (u = []t & s = []t & t = []t) --> P ;
     (u = [Tick]t & s = [Tick]t & t = [Tick]t) --> P ;
     ALL a s' u'.
        (u = [Ev a]t @t u' & s = [Ev a]t @t s' & t = []t &
           u' : s' |[X]|tr []t & a ~: X)
        --> P;
     ALL a t' u'.
        (u = [Ev a]t @t u' & s = []t & t = [Ev a]t @t t' & 
           u' : []t |[X]|tr t' & a ~: X)
        --> P;
     ALL a s' t' u'.
        (u = [Ev a]t @t u' & s = [Ev a]t @t s' & t = [Ev a]t @t t' &
           u' : s' |[X]|tr t' & a : X)
        --> P;
     ALL a s' u'.
        (u = [Ev a]t @t u' & s = [Ev a]t @t s' &
           u' : s' |[X]|tr t & a ~: X)
        --> P;
     ALL a t' u'.
        (u = [Ev a]t @t u' & t = [Ev a]t @t t' & 
           u' : s |[X]|tr t' & a ~: X)
        --> P |]
  ==> P"
apply (simp add: par_tr_def)
apply (erule exE)
apply (erule parx.elims)
apply (simp)
apply (simp)

apply (simp)
apply (drule mp)
apply (rule_tac x="na" in exI, simp, simp)

apply (simp)
apply (drule mp)
apply (rule_tac x="na" in exI, simp, simp)

apply (simp)
apply (drule mp)
apply (rule_tac x="na" in exI, simp, simp)

apply (simp)
apply (drule mp)
apply (rule_tac x="na" in exI, simp, simp)

apply (simp)
apply (rotate_tac 4)
apply (drule mp)
apply (rule_tac x="na" in exI, simp, simp)
done

(*** elim rule ***)

lemma par_tr_elims:
 "[| u : s |[X]|tr t ;
     [| u = []t; s = []t; t = []t |] ==> P ;
     [| u = [Tick]t; s = [Tick]t; t = [Tick]t |] ==> P ;
     !!a s' u'.
        [| u = [Ev a]t @t u'; s = [Ev a]t @t s'; t = []t ; 
           u' : s' |[X]|tr []t; a ~: X |]
        ==> P;
     !!a t' u'.
        [| u = [Ev a]t @t u' ; s = []t ; t = [Ev a]t @t t' ; 
           u' : []t |[X]|tr t'; a ~: X |]
        ==> P;
     !!a s' t' u'.
        [| u = [Ev a]t @t u' ; s = [Ev a]t @t s' ; t = [Ev a]t @t t' ;
           u' : s' |[X]|tr t'; a : X |]
        ==> P;
     !!a s' u'.
        [| u = [Ev a]t @t u' ; s = [Ev a]t @t s' ; 
           u' : s' |[X]|tr t; a ~: X |]
        ==> P;
     !!a t' u'.
        [| u = [Ev a]t @t u' ; t = [Ev a]t @t t' ; 
           u' : s |[X]|tr t'; a ~: X |]
        ==> P |]
  ==> P"
apply (insert par_tr_not_None_imp)
apply (drule_tac x="X" in spec)
apply (drule_tac x="u" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
apply (rule par_tr_elims_lm[of u s X t])
by (simp_all)

(*************************************************************
                 par_tr decomposition
 *************************************************************)

(*-------------------*
 |     par nil       |
 *-------------------*)

(*** par_tr ***)

lemma par_tr_nil_only_if:
  "[]t : s |[X]|tr t ==> s = []t & t = []t"
apply (erule par_tr_elims)
by (simp_all)

(*** iff ***)

lemma par_tr_nil1[simp]:
  "([]t : s |[X]|tr t) = (s = []t & t = []t)"
apply (rule iffI)
apply (simp add: par_tr_nil_only_if)
by (simp add: par_tr_intros)

lemma par_tr_nil2[simp]:
  "(u : []t |[X]|tr []t) = (u = []t)"
apply (rule iffI)
apply (erule par_tr_elims)
by (simp_all)

(*-------------------*
 |     par Tick      |
 *-------------------*)

(*** only if ***)

lemma par_tr_Tick_only_if:
  "[Tick]t : s |[X]|tr t ==> s = [Tick]t & t = [Tick]t"
apply (erule par_tr_elims)
by (simp_all)

(*** iff ***)

lemma par_tr_Tick1[simp]:
  "[Tick]t : s |[X]|tr t = (s = [Tick]t & t = [Tick]t)"
apply (rule iffI)
apply (simp add: par_tr_Tick_only_if)
by (simp add: par_tr_intros)

lemma par_tr_Tick2[simp]:
  "(u : [Tick]t |[X]|tr [Tick]t) = (u = [Tick]t)"
apply (rule iffI)
apply (erule par_tr_elims)
by (simp_all)

(*-----------------*
 |     par Ev      |
 *-----------------*)

(*** only if ***)

lemma par_tr_Ev_only_if:
 "[Ev a]t : s |[X]|tr t
   ==> ((a  : X & s = [Ev a]t & t = [Ev a]t) |
        (a ~: X & s = [Ev a]t & t = []t) |
        (a ~: X & s = []t     & t = [Ev a]t ))"
apply (erule par_tr_elims)
by (simp_all)

(*** if ***)

lemma par_tr_Ev_if:
 "((a  : X & s = [Ev a]t & t = [Ev a]t) |
   (a ~: X & s = [Ev a]t & t = []t) |
   (a ~: X & s = []t     & t = [Ev a]t ))
   ==> [Ev a]t : s |[X]|tr t"
apply (erule disjE)
apply (insert par_tr_Ev_sync[of "[]t" "[]t" X "[]t" a], simp)
apply (erule disjE)
apply (insert par_tr_Ev_left[of "[]t" "[]t" X "[]t" a], simp)
apply (insert par_tr_Ev_right[of "[]t" "[]t" X "[]t" a], simp)
done

lemma par_tr_Ev:
 "[Ev a]t : s |[X]|tr t
   = ((a  : X & s = [Ev a]t & t = [Ev a]t) |
      (a ~: X & s = [Ev a]t & t = []t) |
      (a ~: X & s = []t     & t = [Ev a]t ))"
apply (rule iffI)
apply (simp add: par_tr_Ev_only_if)
apply (simp add: par_tr_Ev_if)
done

(*--------------------------------------------*
 |                 par one                    |
 *--------------------------------------------*)

lemma par_tr_one:
 "[e]t : s |[X]|tr t
   = ((e = Tick & s = [Tick]t & t = [Tick]t) |
     (EX a. e = Ev a &
       ((a  : X & s = [Ev a]t & t = [Ev a]t) |
        (a ~: X & s = [Ev a]t & t = []t) |
        (a ~: X & s = []t     & t = [Ev a]t ))))"
apply (insert event_tick_or_Ev)
apply (drule_tac x="e" in spec)
apply (erule disjE)
apply (simp)

apply (erule exE)
apply (simp add: par_tr_Ev)
done

(*--------------------------------------------*
 |                par head                    |
 *--------------------------------------------*)

(*** only if ***)

lemma par_tr_head_only_if:
 "[Ev a]t @t u : s |[X]|tr t
   ==> (a  : X & (EX s' t'. u : s' |[X]|tr t'
               & s = [Ev a]t @t s' & t = [Ev a]t @t t')) |
       (a ~: X & (EX s'.    u : s' |[X]|tr t & s = [Ev a]t @t s')) |
       (a ~: X & (EX t'.    u : s |[X]|tr t' & t = [Ev a]t @t t'))"
apply (erule par_tr_elims)
by (simp_all add: par_tr_not_None)

(*** if ***)

lemma par_tr_head_if:
 "(a  : X & (EX s' t'. u : s' |[X]|tr t'
               & s = [Ev a]t @t s' & t = [Ev a]t @t t')) |
       (a ~: X & (EX s'.    u : s' |[X]|tr t & s = [Ev a]t @t s')) |
       (a ~: X & (EX t'.    u : s |[X]|tr t' & t = [Ev a]t @t t'))
  ==> [Ev a]t @t u : s |[X]|tr t"

 (*** sync ***)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (simp add: par_tr_intros)

 (*** left ***)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (simp add: par_tr_intros)

 (*** right ***)
 apply (elim conjE exE)
 apply (simp add: par_tr_intros)
done

(*** iff ***)

lemma par_tr_head:
 "[Ev a]t @t u : s |[X]|tr t
   = ((a  : X & (EX s' t'. u : s' |[X]|tr t'
              & s = [Ev a]t @t s' & t = [Ev a]t @t t')) |
      (a ~: X & (EX s'.    u : s' |[X]|tr t & s = [Ev a]t @t s')) |
      (a ~: X & (EX t'.    u : s |[X]|tr t' & t = [Ev a]t @t t')))"
apply (rule iffI)
apply (simp add: par_tr_head_only_if)
apply (simp add: par_tr_head_if)
done

(*--------------------------------------------*
 |                par last                    |
 *--------------------------------------------*)

(*** only if ***)

lemma par_tr_last_only_if_lm:
 "ALL X u s t e.
    (u @t [e]t : s |[X]|tr t & notick u)
   --> (((e  : Ev ` X | e = Tick) &
            (EX s' t'. u : s' |[X]|tr t' & s = s' @t [e]t & t = t' @t [e]t
                       & notick s' & notick t')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX s'.    u : s' |[X]|tr t & s = s' @t [e]t & notick s')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX t'.    u : s |[X]|tr t' & t = t' @t [e]t & notick t')))" 
apply (rule allI)
apply (rule allI)
apply (induct_tac u rule: induct_trace)

(* base *)
 (* None *)
 apply (simp)

 (* []t *)
 apply (intro allI impI)
 apply (simp add: par_tr_one)
 apply (erule disjE, simp)
 apply (erule exE, force)

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

 (* [Ev a]t @t ua *)
 apply (intro allI impI)
 apply (elim conjE)
 apply (simp add: par_tr_head)

  (* head sync *)
  apply (erule disjE)
  apply (elim conjE exE)

  apply (drule_tac x="s'" in spec)
  apply (drule_tac x="t'" in spec)
  apply (drule_tac x="e" in spec)
  apply (simp)

   (* last sync *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="[Ev a]t @t s'a" in exI)
   apply (rule_tac x="[Ev a]t @t t'a" in exI)
   apply (simp)
   apply (rule_tac x="s'a" in exI)
   apply (rule_tac x="t'a" in exI)
   apply (simp)

   (* last left *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="[Ev a]t @t s'a" in exI, simp)
   apply (rule_tac x="s'a" in exI)
   apply (rule_tac x="t'" in exI)
   apply (simp)

   (* last right *)
   apply (simp)
   apply (elim conjE exE)
   apply (rule disjI2)
   apply (rule_tac x="[Ev a]t @t t'a" in exI, simp)
   apply (rule_tac x="s'" in exI)
   apply (rule_tac x="t'a" in exI)
   apply (simp)

  (* head left *)
  apply (erule disjE)
  apply (elim conjE exE)

  apply (drule_tac x="s'" in spec)
  apply (drule_tac x="t" in spec)
  apply (drule_tac x="e" in spec)
  apply (simp)

   (* last sync *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="[Ev a]t @t s'a" in exI)
   apply (rule_tac x="t'" in exI)
   apply (simp)
   apply (rule disjI1)
   apply (rule_tac x="s'a" in exI, simp)

   (* last left *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="[Ev a]t @t s'a" in exI, simp)
   apply (rule disjI1)
   apply (rule_tac x="s'a" in exI, simp)

   (* last right *)
   apply (simp)
   apply (elim conjE exE)
   apply (rule disjI2)
   apply (rule_tac x="t'" in exI, simp)
   apply (rule disjI1)
   apply (rule_tac x="s'" in exI, simp)

  (* head right *)
  apply (elim conjE exE)

  apply (drule_tac x="sa" in spec)
  apply (drule_tac x="t'" in spec)
  apply (drule_tac x="e" in spec)
  apply (simp)

   (* last sync *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="s'" in exI)
   apply (rule_tac x="[Ev a]t @t t'a" in exI)
   apply (simp)
   apply (rule disjI2)
   apply (rule_tac x="t'a" in exI, simp)

   (* last left *)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="s'" in exI, simp)
   apply (rule disjI2)
   apply (rule_tac x="t'" in exI, simp)

   (* last right *)
   apply (simp)
   apply (elim conjE exE)
   apply (rule disjI2)
   apply (rule_tac x="[Ev a]t @t t'a" in exI, simp)
   apply (rule disjI2)
   apply (rule_tac x="t'a" in exI, simp)
done

(*** rule ***)

lemma par_tr_last_only_if:
 "u @t [e]t : s |[X]|tr t
   ==> (((e  : Ev ` X | e = Tick) &
            (EX s' t'. u : s' |[X]|tr t' & s = s' @t [e]t & t = t' @t [e]t
                       & notick s' & notick t')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX s'.    u : s' |[X]|tr t & s = s' @t [e]t & notick s')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX t'.    u : s |[X]|tr t' & t = t' @t [e]t & notick t')))" 
apply (case_tac "u @t [e]t = None", simp)
apply (simp add: decompo_appt_not_None)
by (simp add: par_tr_last_only_if_lm)

(*** if ***)

lemma par_tr_last_if_lm:
 "ALL X u s t e.
   (((e  : Ev ` X | e = Tick) &
            (EX s' t'. u : s' |[X]|tr t' & s = s' @t [e]t & t = t' @t [e]t
                       & notick s' & notick t')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX s'.    u : s' |[X]|tr t & s = s' @t [e]t & notick s')) |
        (e ~: Ev ` X & e ~= Tick & 
            (EX t'.    u : s |[X]|tr t' & t = t' @t [e]t & notick t')))
   --> u @t [e]t : s |[X]|tr t"
apply (rule allI)
apply (rule allI)
apply (induct_tac u rule: induct_trace)

(* base *)
 (* None *)
 apply (simp)

 (* []t *)
 apply (intro allI impI)
 apply (simp add: par_tr_one)
 apply (erule disjE)
 apply (elim conjE)
 apply (erule disjE, force, force)
 apply (erule disjE)
 apply (simp add: not_tick_to_Ev)
 apply (elim conjE exE)
 apply (simp, force)
 apply (simp add: not_tick_to_Ev)
 apply (elim conjE exE)
 apply (simp, force)

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

 (* [Ev a]t @t ua *)
 apply (intro allI impI)

  (* last sync *)
  apply (erule disjE)
  apply (elim conjE exE)
  apply (erule par_tr_elims)
  apply (simp_all add: par_tr_intros)

  (* last left *)
  apply (erule disjE)
  apply (elim conjE exE)
  apply (erule par_tr_elims)
  apply (simp_all add: par_tr_intros)

  (* last right *)
  apply (elim conjE exE)
  apply (erule par_tr_elims)
  apply (simp_all add: par_tr_intros)
done

(*** rule ***)

lemma par_tr_last_if:
 "[|((e  : Ev ` X | e = Tick) &
          (EX s' t'. u : s' |[X]|tr t' & s = s' @t [e]t & t = t' @t [e]t
                      & notick s' & notick t')) |
     (e ~: Ev ` X & e ~= Tick & 
          (EX s'.    u : s' |[X]|tr t & s = s' @t [e]t & notick s')) |
     (e ~: Ev ` X & e ~= Tick & 
          (EX t'.    u : s |[X]|tr t' & t = t' @t [e]t & notick t')) |]
   ==> u @t [e]t : s |[X]|tr t"
by (simp add: par_tr_last_if_lm)

(*** iff ***)

lemma par_tr_last:
 "u @t [e]t : s |[X]|tr t
   = (((e  : Ev ` X | e = Tick) &
            (EX s' t'. u : s' |[X]|tr t' & s = s' @t [e]t & t = t' @t [e]t
                       & notick s' & notick t')) |
       (e ~: Ev ` X & e ~= Tick & 
            (EX s'.    u : s' |[X]|tr t & s = s' @t [e]t & notick s')) |
       (e ~: Ev ` X & e ~= Tick & 
            (EX t'.    u : s |[X]|tr t' & t = t' @t [e]t & notick t')))" 
apply (rule iffI)
apply (simp add: par_tr_last_only_if)
apply (simp add: par_tr_last_if)
done

(*************************************************************
                     symmetricity  
 *************************************************************)

lemma par_tr_sym_only_if_lm:
  "ALL u s t. u : (s |[X]|tr t) --> u : (t |[X]|tr s)"
apply (rule allI)
apply (induct_tac u rule: induct_trace)
apply (simp_all)

apply (intro allI impI)
apply (erule par_tr_elims)

 (* []t *)
 apply (simp)

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

 (* Ev_nil *)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="[]t" in spec)
 apply (simp add: par_tr_intros)

 (* nil_Ev *)
 apply (drule_tac x="[]t" in spec)
 apply (drule_tac x="t'" in spec)
 apply (simp add: par_tr_intros)

 (* sync *)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t'" in spec)
 apply (simp add: par_tr_intros)

 (* left *)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t" in spec)
 apply (simp add: par_tr_intros)

 (* right *)
 apply (drule_tac x="sa" in spec)
 apply (drule_tac x="t'" in spec)
 apply (simp add: par_tr_intros)
done

lemma par_tr_sym_only_if:
  "u : (s |[X]|tr t) ==> u : (t |[X]|tr s)"
apply (insert par_tr_sym_only_if_lm[of X])
apply (drule_tac x="u" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
apply (simp)
done

lemma par_tr_sym: "s |[X]|tr t = t |[X]|tr s"
apply (auto)
apply (rule par_tr_sym_only_if, simp_all)
apply (rule par_tr_sym_only_if, simp_all)
done

(*************************************************************
                     prefix_closed
 *************************************************************)

lemma par_tr_prefix_lm:
 "ALL X v u s t. prefix v u & u : s |[X]|tr t
     --> (EX s' t'. v : s' |[X]|tr t' & 
                        prefix s' s & prefix t' t)"
apply (rule allI)
apply (rule allI)
apply (induct_tac v rule: induct_trace)
apply (simp_all add: disj_not1)

apply (intro allI impI)
apply (case_tac "u = None", simp)
apply (simp add: prefix_def)
apply (elim conjE exE)
apply (simp)

apply (intro allI impI)
apply (case_tac "u = None", simp)
apply (elim conjE exE)
apply (simp add: par_tr_head)

 (* sync *)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (drule_tac x="u'" in spec)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t'" in spec)
 apply (force)

 (* left *)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (drule_tac x="u'" in spec)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t" in spec)
 apply (force)

 (* right *)
 apply (elim conjE exE)
 apply (drule_tac x="u'" in spec)
 apply (drule_tac x="sa" in spec)
 apply (drule_tac x="t'" in spec)
 apply (force)
done

(*** rule ***)

lemma par_tr_prefix:
 "[| prefix v u ; u : s |[X]|tr t |]
  ==> (EX s' t'. v : s' |[X]|tr t' & prefix s' s & prefix t' t)"
apply (insert par_tr_prefix_lm)
apply (drule_tac x="X" in spec)
apply (drule_tac x="v" in spec)
apply (drule_tac x="u" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

lemma par_tr_prefixE:
 "[| prefix v u ; u : s |[X]|tr t ;
     !! s' t'. [| v : s' |[X]|tr t' ; prefix s' s ; prefix t' t |] ==> R
  |] ==> R"
apply (insert par_tr_prefix[of v u s X t])
by (auto)

(*************************************************************
                  parallel lemmas etc.
 *************************************************************)

(*******************************
          par_tr lenght 
 *******************************)

lemma par_tr_lengtht_lm:
 "ALL X u s t. u : s |[X]|tr t
         --> lengtht s <= lengtht u & lengtht t <= lengtht u"
apply (rule allI)
apply (rule allI)
apply (induct_tac u rule: induct_trace)
apply (simp_all)

apply (intro allI impI)
apply (simp add: par_tr_head)

 (* sync *)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t'" in spec)
 apply (simp add: par_tr_not_None)

 (* left *)
 apply (erule disjE)
 apply (elim conjE exE)
 apply (drule_tac x="s'" in spec)
 apply (drule_tac x="t" in spec)
 apply (simp add: par_tr_not_None)
 apply (force)

 (* right *)
 apply (elim conjE exE)
 apply (drule_tac x="sa" in spec)
 apply (drule_tac x="t'" in spec)
 apply (simp add: par_tr_not_None)
 apply (force)
done

(*** rule ***)

lemma par_tr_lengtht:
 "u : s |[X]|tr t ==> lengtht s <= lengtht u & lengtht t <= lengtht u"
by (simp add: par_tr_lengtht_lm)

(*** ruleE ***)

lemma par_tr_lengthtE:
 "[| u : s |[X]|tr t ; 
     [| lengtht s <= lengtht u ; lengtht t <= lengtht u|] ==> R |] ==> R"
by (simp add: par_tr_lengtht)

(**************************************************
                    para
 **************************************************)

lemma par_tr_nil_Ev_rev:
  "u : []t |[X]|tr ([Ev a]t @t t)
   ==> a ~: X & (EX v. u = [Ev a]t @t v & v : []t |[X]|tr t)"
apply (erule par_tr_elims)
by (simp_all add: par_tr_intros par_tr_not_None)

lemma par_tr_Tick_Ev_rev:
  "u : [Tick]t |[X]|tr ([Ev a]t @t t)
   ==> a ~: X & (EX v. u = [Ev a]t @t v & v : [Tick]t |[X]|tr t)"
apply (erule par_tr_elims)
by (simp_all add: par_tr_intros par_tr_not_None)

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

lemma par_tr_notick_lm: 
  "ALL u s t. (notick u & u : s |[X]|tr t) --> notick s & notick t"
apply (rule allI)
apply (induct_tac u rule: rev_induct_trace)
apply (simp_all) 
apply (intro allI impI)
apply (simp add: par_tr_last)
apply (elim conjE disjE exE)
apply (drule_tac x="s'" in spec)
apply (drule_tac x="t'" in spec)
apply (simp)
apply (drule_tac x="s'" in spec)
apply (drule_tac x="t'" in spec)
apply (simp)
apply (drule_tac x="s'" in spec)
apply (drule_tac x="t" in spec)
apply (simp)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="t'" in spec)
apply (simp)
done

lemma par_tr_notick_left: 
  "[| notick u; u : s |[X]|tr t |] ==> notick s"
apply (insert par_tr_notick_lm[of X])
apply (drule_tac x="u" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

lemma par_tr_notick_right: 
  "[| notick u; u : s |[X]|tr t |] ==> notick t"
apply (insert par_tr_notick_lm[of X])
apply (drule_tac x="u" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

lemmas par_tr_notick = par_tr_notick_left par_tr_notick_right

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

declare disj_not1   [simp] 
declare not_None_eq [simp]

end