Theory Trace_ren

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               November 2004               |
            |                   July 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Trace_ren
imports Prefix
begin

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

declare disj_not1 [simp del]

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

         1. 
         2. 
         3. 
         4. 

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

(*************************************************************
               functions used for defining [[ ]]
 *************************************************************)

consts
  renx :: "('a * 'b) set => ('a trace * 'b trace) set"

inductive "renx r"
intros
renx_nil: 
  "(<>, <>) : renx r"

renx_Tick: 
  "(<Tick>, <Tick>) : renx r"

renx_Ev: 
  "[| (s, t) : renx r ; (a, b) : r |]
   ==> (<Ev a> ^^ s, <Ev b> ^^ t) : renx r"

consts
  ren_tr :: "'a trace => ('a * 'b) set => 'b trace => bool"
                                    ("(_ [[_]]* _)" [1000,0,1000] 1000)

defs
  ren_tr_def : "s [[r]]* t == (( s, t) : renx r)"

consts
  ren_inv :: "('a * 'b) set => 'b event set => 'a event set"
                                    ("([[_]]inv _)" [0,1000] 1000)

defs
  ren_inv_def: 
   "[[r]]inv X == 
      {ea. EX eb : X. ea = Tick & eb = Tick |
                      (EX a b. (a,b):r & ea = Ev a & eb = Ev b)}"

(*************************************************************
                 ren_tr intros and elims
 *************************************************************)

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

lemma ren_tr_nil[simp]:
  "<> [[r]]* <>"
apply (simp add: ren_tr_def)
by (simp add: renx.intros)

lemma ren_tr_Tick[simp]: 
  "<Tick> [[r]]* <Tick>"
apply (simp add: ren_tr_def)
by (simp add: renx.intros)

lemma ren_tr_Ev: 
  "[| s [[r]]* t ; (a, b) : r |]
   ==> (<Ev a> ^^ s) [[r]]* (<Ev b> ^^ t)"
apply (simp add: ren_tr_def)
by (simp add: renx.intros)

(*** intro rule ***)

lemmas ren_tr_intros = ren_tr_Ev

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

lemma ren_tr_elims_lm:
 "[| s [[r]]* t ;
     (s = <> & t = <>) --> P ;
     (s = <Tick> & t = <Tick>) --> P ;
     ALL a b s' t'.
        (s' [[r]]* t' & s = <Ev a> ^^ s' & t = <Ev b> ^^ t' & 
         (a, b) : r )
        --> P |]
  ==> P"
apply (simp add: ren_tr_def)
apply (erule renx.elims)
apply (simp_all)
done

(*** elim rule ***)

lemma ren_tr_elims:
 "[| s [[r]]* t ;
     [| s = <>; t = <> |] ==> P ;
     [| s = <Tick>; t = <Tick> |] ==> P ;
     !!a b s' t'.
        [| s' [[r]]* t' ; s = <Ev a> ^^ s' ; t = <Ev b> ^^ t' ;
            (a, b) : r |]
        ==> P |]
  ==> P"
apply (rule ren_tr_elims_lm[of s r t])
by (auto)

(*************************************************************
                 ren_tr decomposition
 *************************************************************)

(*-------------------*
 |     ren nil       |
 *-------------------*)

lemma ren_tr_nil1[simp]: "(<> [[r]]* s) = (s = <>)"
apply (rule iffI)
by (erule ren_tr_elims, simp_all)

lemma ren_tr_nil2[simp]: "(s [[r]]* <>) = (s = <>)"
apply (rule iffI)
by (erule ren_tr_elims, simp_all)

(*-------------------*
 |     ren Tick      |
 *-------------------*)

lemma ren_tr_Tick1[simp]: "(<Tick> [[r]]* s) = (s = <Tick>)"
apply (rule iffI)
by (erule ren_tr_elims, simp_all)

lemma ren_tr_Tick2[simp]: "(s [[r]]* <Tick>) = (s = <Tick>)"
apply (rule iffI)
by (erule ren_tr_elims, simp_all)

(*-------------------*
 |     ren Ev        |
 *-------------------*)

(*** left ***)

(* only if *)

lemma ren_tr_decompo_left_only_if: 
  "(<Ev a> ^^ s) [[r]]* u 
    ==> (EX b t. u = <Ev b> ^^ t & (a, b) : r & s [[r]]* t)"
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="u" in spec)

apply (erule disjE, simp)   (* <> --> contradict *)
apply (erule disjE, simp)   (* <Tick> --> contradict *)

apply (erule ren_tr_elims)
by (simp_all)

(* if *)

lemma ren_tr_decompo_left_if: 
  "[| (a, b) : r ; s [[r]]* t |]
    ==> (<Ev a> ^^ s) [[r]]* (<Ev b> ^^ t)"
apply (rule ren_tr_intros)
by (simp_all)

(* iff *)

lemma ren_tr_decompo_left: 
  "(<Ev a> ^^ s) [[r]]* u
      = (EX b t. u = <Ev b> ^^ t & (a, b) : r & s [[r]]* t)"
apply (rule iffI)
apply (simp add: ren_tr_decompo_left_only_if)
apply (elim exE)
apply (simp add: ren_tr_decompo_left_if)
done

(*** right ***)

(* only if *)

lemma ren_tr_decompo_right_only_if: 
  "u [[r]]* (<Ev b> ^^ t)
    ==> (EX a s. u = <Ev a> ^^ s & (a, b) : r & s [[r]]* t)"
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="u" in spec)

 apply (erule disjE, simp)   (* <> --> contradict *)
 apply (erule disjE, simp)   (* <Tick> --> contradict *)

 apply (erule ren_tr_elims)
by (simp_all)

(* if *)

lemma ren_tr_decompo_right_if: 
  "[| (a, b) : r ; s [[r]]* t |]
    ==> (<Ev a> ^^ s) [[r]]* (<Ev b> ^^ t)"
apply (rule ren_tr_intros)
by (simp_all)

(* iff *)

lemma ren_tr_decompo_right: 
  "u [[r]]* (<Ev b> ^^ t)
     = (EX a s. u = <Ev a> ^^ s & (a, b) : r & s [[r]]* t)"
apply (rule iffI)
apply (simp add: ren_tr_decompo_right_only_if)
apply (elim exE)
apply (simp add: ren_tr_decompo_right_if)
done

lemmas ren_tr_decompo = ren_tr_decompo_left ren_tr_decompo_right

(*-------------------*
 |     ren one       |
 *-------------------*)

lemma ren_tr_one[simp]: 
  "(a, b) : r ==> <Ev a> [[r]]* <Ev b>"
apply (insert ren_tr_Ev[of "<>" r "<>" a b])
by (simp)

(*** left ***)

lemma ren_tr_one_decompo_left_only_if: 
  "<Ev a> [[r]]* t ==> (EX b. t = <Ev b> & (a, b) : r)"
apply (insert ren_tr_decompo_left[of a "<>" r t])
by (simp)

lemma ren_tr_one_decompo_left: 
  "<Ev a> [[r]]* t = (EX b. t = <Ev b> & (a, b) : r)"
apply (rule iffI)
apply (simp add: ren_tr_one_decompo_left_only_if)
by (auto)

(*** right ***)

lemma ren_tr_one_decompo_right_only_if: 
  "s [[r]]* <Ev b> ==> (EX a. s = <Ev a> & (a, b) : r)"
apply (insert ren_tr_decompo_right[of s r b "<>"])
by (simp)

lemma ren_tr_one_decompo_right: 
  "s [[r]]* <Ev b> = (EX a. s = <Ev a> & (a, b) : r)"
apply (rule iffI)
apply (simp add: ren_tr_one_decompo_right_only_if)
by (auto)

lemmas ren_tr_one_decompo = ren_tr_one_decompo_left ren_tr_one_decompo_right

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

(*** left ***)

lemma ren_tr_noTick_left_lm: "ALL r s t. (s [[r]]* t & noTick s) --> noTick t"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)

apply (intro allI impI)
apply (simp add: ren_tr_decompo)
apply (elim conjE exE)
by (simp)

(*** rule ***)

lemma ren_tr_noTick_left: "[| s [[r]]* t ; noTick s |] ==> noTick t"
apply (insert ren_tr_noTick_left_lm)
apply (drule_tac x="r" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

(*** right ***)

lemma ren_tr_noTick_right_lm: "ALL r s t. (s [[r]]* t & noTick t) --> noTick s"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)
apply (simp add: disj_not1)

apply (intro allI impI)
apply (simp add: ren_tr_decompo)
apply (elim conjE exE)
apply (drule mp)
apply (rule_tac x="ta" in exI)
by (simp_all)

(*** rule ***)

lemma ren_tr_noTick_right: "[| s [[r]]* t ; noTick t |] ==> noTick s"
apply (insert ren_tr_noTick_right_lm)
apply (drule_tac x="r" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

(*************************************************************
                 ren_tr appending
 *************************************************************)

(*** noTick not None ***)

lemma ren_tr_appt_noTick_lm:
  "ALL r s1 s2 t1 t2.
     (s1 [[r]]* t1 & s2 [[r]]* t2 & (noTick s1 & noTick t1))
       --> (s1 ^^ s2) [[r]]* (t1 ^^ t2)"
apply (rule allI)
apply (rule allI)
apply (induct_tac s1 rule: induct_trace)
 apply (simp_all)

 apply (intro allI impI)
 apply (elim conjE)
 apply (erule ren_tr_elims)
 apply (simp_all)

 apply (simp add: appt_assoc)
 apply (simp add: ren_tr_decompo)
done

(*** rule ***)

lemma ren_tr_appt:
  "[| s1 [[r]]* t1 ; s2 [[r]]* t2 ; noTick s1 | noTick t1 | s2 = <> | t2 = <> |]
     ==> (s1 ^^ s2) [[r]]* (t1 ^^ t2)"
apply (elim disjE)
apply (simp add: ren_tr_appt_noTick_lm ren_tr_noTick_left)
apply (simp add: ren_tr_appt_noTick_lm ren_tr_noTick_right)
by (simp_all)

(*--------------------*
 |   <Ev a> ^^ ...   |
 *--------------------*)

lemma ren_tr_appt_Ev:
  "[| (a, b) : r ; s [[r]]* t |]
     ==> (<Ev a> ^^ s) [[r]]* (<Ev b> ^^ t)"
apply (insert ren_tr_appt[of "<Ev a>" r "<Ev b>" s t])
by (simp_all)

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

(*** left ***)

(* only if *)

lemma ren_tr_appt_decompo_left_only_if_lm: 
  "ALL r s1 s2 t. ((s1 ^^ s2) [[r]]* t & (noTick s1 | s2 = <>))
    --> (EX t1 t2. t = t1 ^^ t2 & s1 [[r]]* t1 & s2 [[r]]* t2 
                 & (noTick t1 | t2 = <>))"
apply (rule allI)
apply (rule allI)
apply (induct_tac s1 rule: induct_trace)
apply (simp_all)

(* [Ev a] ^^ ... *)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: appt_assoc)
apply (simp add: ren_tr_decompo_left)
apply (elim conjE exE)
apply (drule_tac x="s2" in spec)
apply (drule_tac x="ta" in spec)
apply (simp)
apply (elim conjE exE)
apply (rule_tac x="<Ev b> ^^ t1" in exI)
apply (rule_tac x="t2" in exI)
apply (simp add: appt_assoc)
done

(* rule *)

lemma ren_tr_appt_decompo_left_only_if: 
  "[| (s1 ^^ s2) [[r]]* t ; noTick s1 | s2 = <> |]
    ==> (EX t1 t2. t = t1 ^^ t2 & s1 [[r]]* t1 & s2 [[r]]* t2 
                 & (noTick t1 | t2 = <>))"
by (simp add: ren_tr_appt_decompo_left_only_if_lm)

(* iff *)

lemma ren_tr_appt_decompo_left:
  "noTick s1 | s2 = <>
   ==> (s1 ^^ s2) [[r]]* t
      = (EX t1 t2. t = t1 ^^ t2 & s1 [[r]]* t1 & s2 [[r]]* t2 
                 & (noTick t1 | t2 = <>))"
apply (rule iffI)
apply (simp add: ren_tr_appt_decompo_left_only_if)
apply (elim conjE exE)
apply (auto simp add: ren_tr_appt)
done

(*** right ***)

(* only if *)

lemma ren_tr_appt_decompo_right_only_if_lm: 
  "ALL r t1 t2 s. (s [[r]]* (t1 ^^ t2) & (noTick t1 | t2 = <>))
    --> (EX s1 s2. s = s1 ^^ s2 & s1 [[r]]* t1 & s2 [[r]]* t2 
                 & (noTick s1 | s2 = <>))"
apply (rule allI)
apply (rule allI)
apply (induct_tac t1 rule: induct_trace)
apply (simp_all)

(* [Ev a] ^^ ... *)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: appt_assoc)
apply (simp add: ren_tr_decompo_right)
apply (elim conjE exE)
apply (drule_tac x="t2" in spec)
apply (drule_tac x="sb" in spec)
apply (simp)
apply (elim conjE exE)
apply (rule_tac x="<Ev aa> ^^ s1" in exI)
apply (rule_tac x="s2" in exI)
apply (simp add: appt_assoc)
done

(* rule *)

lemma ren_tr_appt_decompo_right_only_if: 
  "[| s [[r]]* (t1 ^^ t2) ; noTick t1 | t2 = <> |]
    ==> (EX s1 s2. s = s1 ^^ s2 & s1 [[r]]* t1 & s2 [[r]]* t2
                 & (noTick s1 | s2 = <>))"
by (simp add: ren_tr_appt_decompo_right_only_if_lm)

(* iff *)

lemma ren_tr_appt_decompo_right:
  "noTick t1 | t2 = <>
    ==> s [[r]]* (t1 ^^ t2)
      = (EX s1 s2. s = s1 ^^ s2 & s1 [[r]]* t1 & s2 [[r]]* t2
                 & (noTick s1 | s2 = <>))"
apply (rule iffI)
apply (simp add: ren_tr_appt_decompo_right_only_if)
apply (elim conjE exE)
by (auto simp add: ren_tr_appt)

lemmas ren_tr_appt_decompo
     = ren_tr_appt_decompo_left ren_tr_appt_decompo_right

(*--------------------*
 |   <Ev a> ^^ ...   |
 *--------------------*)

lemma ren_tr_head_decompo[simp]: 
  "(<Ev a> ^^ s) [[r]]* (<Ev b> ^^ t) = ((a, b) : r & s [[r]]* t)"
apply (insert ren_tr_appt_decompo_right[of  "<Ev b>" t "<Ev a> ^^ s" r])
apply (rule iffI)

apply (simp add: ren_tr_one_decompo)
apply (elim conjE exE, simp)
by (simp add: ren_tr_appt_Ev)

(*--------------------*
 |    ... ^^ [e]t     |
 *--------------------*)

lemma ren_tr_last_decompo_Ev[simp]: 
  "[| noTick s ; noTick t |]
    ==> (s ^^ <Ev a>) [[r]]* (t ^^ <Ev b>) = (s [[r]]* t & (a,b) : r)"
apply (insert ren_tr_appt_decompo_right[of t "<Ev b>" "(s ^^ <Ev a>)" r])
 apply (rule iffI)

  (* => *)
  apply (simp add: ren_tr_one_decompo)
  apply (elim conjE exE)
  apply (simp)

  (* <= *)
  apply (simp)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="<Ev a>" in exI)
  apply (simp)
done

lemma ren_tr_last_decompo_Tick[simp]: 
  "[| noTick s ; noTick t |]
    ==> (s ^^ <Tick>) [[r]]* (t ^^ <Tick>) = (s [[r]]* t)"
apply (insert ren_tr_appt_decompo_right[of t "<Tick>" "(s ^^ <Tick>)" r])
by (auto simp add: ren_tr_noTick_right)

(*************************************************************
                 ren_tr lengtht
 *************************************************************)

(*** ren same length ***)

lemma ren_tr_lengtht:
  "ALL r s t. s [[r]]* t --> lengtht s = lengtht t"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)

 apply (simp_all)
 apply (intro allI impI)
 apply (erule ren_tr_elims)
 apply (simp_all)
done

(*************************************************************
                    ren_tr prefix
 *************************************************************)

lemma ren_tr_prefix_lm:
  "ALL r u v s. prefix v u & s [[r]]* u
     --> (EX t. prefix t s & t [[r]]* v)"
apply (rule allI)
apply (rule allI)
apply (induct_tac u rule: induct_trace)
apply (simp_all)

(* <Ev a> ^^ ... *)
apply (intro allI impI)
apply (elim conjE)
apply (erule disjE, simp)

apply (simp add: ren_tr_decompo)
apply (elim conjE exE, simp)

apply (drule_tac x="v'" in spec)
apply (drule_tac x="sb" in spec, simp)
apply (elim conjE exE)

apply (rule_tac x="<Ev aa> ^^ t" in exI, simp)
done

(*** rule ***)

lemma ren_tr_prefix:
  "[| prefix v u ; s [[r]]* u |] ==> (EX t. prefix t s & t [[r]]* v)"
apply (insert ren_tr_prefix_lm)
apply (drule_tac x="r" in spec)
apply (drule_tac x="u" in spec)
apply (drule_tac x="v" in spec)
apply (drule_tac x="s" in spec)
by (simp)

(*** erule ***)

lemma ren_tr_prefixE:
  "[| prefix v u ; s [[r]]* u ;
      !! t. [| prefix t s ; t [[r]]* v |] ==> R 
   |] ==> R"
apply (insert ren_tr_prefix[of v u s r])
by (auto)

(*************************************************************
                    inj --> unique
 *************************************************************)

lemma ren_tr_inj_unique_ALL:
  "ALL s1 s2. (inj f &
          s1 [[{b. EX a. b = (a, f a)}]]* t &
          s2 [[{b. EX a. b = (a, f a)}]]* t )
       --> s1 = s2"
apply (induct_tac t rule: induct_trace)
apply (simp_all)
apply (intro allI impI)
apply (elim conjE)
apply (simp add: ren_tr_decompo_right)
apply (elim conjE exE)
apply (simp)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="sb" in spec)
apply (simp)
apply (simp add: inj_on_def)
done

lemma ren_tr_inj_unique:
  "[| inj f ;
          s1 [[{b. EX a. b = (a, f a)}]]* t ;
          s2 [[{b. EX a. b = (a, f a)}]]* t |]
   ==> s1 = s2"
apply (insert ren_tr_inj_unique_ALL[of f t])
apply (simp)
done

(*************************************************************
                       inverse R
 *************************************************************)

lemma ren_inv_sub_Evset[simp]: "[[r]]inv Evset <= Evset"
by (auto simp add: ren_inv_def Evset_def)

lemma ren_inv_sub:
  "X <= Y ==> [[r]]inv X <= [[r]]inv Y"
by (auto simp add: ren_inv_def)

lemma ren_inv_Un[simp]:
  "[[r]]inv(X Un Y) = [[r]]inv X Un [[r]]inv Y"
by (auto simp add: ren_inv_def)

(*** [[r]]inv preserves "no Tick" ***)

lemma ren_inv_no_Tick[simp]: "([[r]]inv X <= Evset) = (X <= Evset)"
by (auto simp add: ren_inv_def Evset_def)

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

declare disj_not1 [simp] 

end