Theory Trace_ren

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

theory Trace_ren = 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. 
         2. 
         3. 
         4. 

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

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

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

inductive "renx r"
intros
renx_nil: 
  "(0, []t, []t) : renx r"

renx_Tick: 
  "(0, [Tick]t, [Tick]t) : renx r"

renx_Ev: 
  "[| (n, s, t) : renx r ; (a, b) : r ; s ~= None |]
   ==> (Suc n, [Ev a]t @t s, [Ev b]t @t t) : renx r"

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

defs
  ren_tr_def : "s [[r]]tr t == (EX n. (n, 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)}"

(*************************************************************
                       renx None
 *************************************************************)

lemma renx_not_None_lm: 
  "ALL r n s t. (n, s, t) : renx r
       --> (s ~= None & t ~= None)"
apply (rule allI)
apply (rule allI)
apply (induct_tac n)
apply (intro allI impI)
apply (erule renx.elims)
apply (simp_all)

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

(*** rule ***)

lemma renx_not_None:
  "(n, s, t) : renx r ==> (s ~= None & t ~= None)"
by (simp add: renx_not_None_lm)

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

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

lemma ren_tr_nil[simp]:
  "[]t [[r]]tr []t"
apply (simp add: ren_tr_def)
apply (rule_tac x="0" in exI)
by (simp add: renx.intros)

lemma ren_tr_Tick[simp]: 
  "[Tick]t [[r]]tr [Tick]t"
apply (simp add: ren_tr_def)
apply (rule_tac x="0" in exI)
by (simp add: renx.intros)

lemma ren_tr_Ev: 
  "[| s [[r]]tr t ; (a, b) : r ; s ~= None |]
   ==> ([Ev a]t @t s) [[r]]tr ([Ev b]t @t t)"
apply (simp add: ren_tr_def)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
by (simp add: renx.intros)

(*** intro rule ***)

lemmas ren_tr_intros = ren_tr_Ev

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

lemma ren_tr_elims_lm:
 "[| s [[r]]tr t ;
     (s = []t & t = []t) --> P ;
     (s = [Tick]t & t = [Tick]t) --> P ;
     ALL a b s' t'.
        (s' [[r]]tr t' & s = [Ev a]t @t s' & t = [Ev b]t @t t' & 
         (a, b) : r & s' ~= None)
        --> P |]
  ==> P"
apply (simp add: ren_tr_def)
apply (erule exE)
apply (erule renx.elims)
apply (simp_all)

apply (drule mp)
apply (rule_tac x="b" in exI)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule_tac x="na" in exI)
by (simp_all)

(*** elim rule ***)

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

(*************************************************************
                      ren_tr None
 *************************************************************)

(*** ren_tr ***)

lemma ren_tr_not_None_lm: 
  "ALL r s t. s [[r]]tr t --> (s ~= None & t ~= None)"
apply (simp add: ren_tr_def)
apply (intro allI impI)
apply (erule exE)
by (simp add: renx_not_None)

(*** rule ***)

lemma ren_tr_not_None:
  "s [[r]]tr t ==> (s ~= None & t ~= None)"
by (simp add: ren_tr_not_None_lm)

(*** None False ***)

lemma ren_tr_None_False1[simp]: 
  "~ None [[r]]tr t"
apply (insert ren_tr_not_None[of "None" r t])
by (auto)

lemma ren_tr_None_False2[simp]: 
  "~ s [[r]]tr None"
apply (insert ren_tr_not_None[of s r "None"])
by (auto)

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

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

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

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

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

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

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

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

(*** left ***)

(* only if *)

lemma ren_tr_Ev_decompo_left_only_if: 
  "([Ev a]t @t s) [[r]]tr u 
    ==> (EX b t. u = [Ev b]t @t t & (a, b) : r & s [[r]]tr t)"
apply (case_tac "u = None", simp)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="u" in spec, simp)

 apply (erule disjE, simp)   (* []t --> contradict *)
 apply (erule disjE, simp)   (* [Tick]t --> contradict *)

 apply (erule ren_tr_elims)
by (simp_all)

(* if *)

lemma ren_tr_Ev_decompo_left_if: 
  "[| (a, b) : r ; s [[r]]tr t |]
    ==> ([Ev a]t @t s) [[r]]tr ([Ev b]t @t t)"
apply (rule ren_tr_intros)
apply (simp_all)
apply (case_tac "s = None", simp)
by (simp)

(* iff *)

lemma ren_tr_Ev_decompo_left: 
  "([Ev a]t @t s) [[r]]tr u
      = (EX b t. u = [Ev b]t @t t & (a, b) : r & s [[r]]tr t)"
apply (rule iffI)
apply (simp add: ren_tr_Ev_decompo_left_only_if)
apply (elim exE)
apply (simp add: ren_tr_Ev_decompo_left_if)
done

(*** right ***)

(* only if *)

lemma ren_tr_Ev_decompo_right_only_if: 
  "u [[r]]tr ([Ev b]t @t t)
    ==> (EX a s. u = [Ev a]t @t s & (a, b) : r & s [[r]]tr t)"
apply (case_tac "u = None", simp)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="u" in spec, simp)

 apply (erule disjE, simp)   (* []t --> contradict *)
 apply (erule disjE, simp)   (* [Tick]t --> contradict *)

 apply (erule ren_tr_elims)
 apply (simp_all)
by (case_tac "t' ~= None", simp, simp)

(* if *)

lemma ren_tr_Ev_decompo_right_if: 
  "[| (a, b) : r ; s [[r]]tr t |]
    ==> ([Ev a]t @t s) [[r]]tr ([Ev b]t @t t)"
apply (rule ren_tr_intros)
apply (simp_all)
apply (case_tac "s ~= None", simp)
by (simp)

(* iff *)

lemma ren_tr_Ev_decompo_right: 
  "u [[r]]tr ([Ev b]t @t t)
     = (EX a s. u = [Ev a]t @t s & (a, b) : r & s [[r]]tr t)"
apply (rule iffI)
apply (simp add: ren_tr_Ev_decompo_right_only_if)
apply (elim exE)
apply (simp add: ren_tr_Ev_decompo_right_if)
done

lemmas ren_tr_Ev_decompo = ren_tr_Ev_decompo_left ren_tr_Ev_decompo_right

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

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

(*** left ***)

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

lemma ren_tr_one_decompo_left: 
  "[Ev a]t [[r]]tr t = (EX b. t = [Ev b]t & (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]]tr [Ev b]t ==> (EX a. s = [Ev a]t & (a, b) : r)"
apply (insert ren_tr_Ev_decompo_right[of s r b "[]t"])
by (simp)

lemma ren_tr_one_decompo_right: 
  "s [[r]]tr [Ev b]t = (EX a. s = [Ev a]t & (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]]tr 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_Ev_decompo)
apply (elim conjE exE)
by (simp)

(*** rule ***)

lemma ren_tr_notick_left: "[| s [[r]]tr 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]]tr 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_Ev_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]]tr 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_not_None:
  "ALL r s1 s2 t1 t2.
     (s1 [[r]]tr t1 & s2 [[r]]tr t2 & (s1 @t s2 ~= None | t1 @t t2 ~= None))
       --> (s1 @t s2) [[r]]tr (t1 @t 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 (intro allI impI)
 apply (simp add: ren_tr_Ev_decompo)
 apply (elim conjE exE, simp)

 apply (drule_tac x="s2" in spec)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="t2" in spec)
 apply (simp)

 apply (rule_tac x="b" in exI)
 apply (rule_tac x="t @t t2" in exI)
 apply (simp)
done

(*** rule ***)

lemma ren_tr_appt:
  "[| s1 [[r]]tr t1 ; s2 [[r]]tr t2 ; s1 @t s2 ~= None | t1 @t t2 ~= None |]
     ==> (s1 @t s2) [[r]]tr (t1 @t t2)"
apply (case_tac "s2 = None", simp)
by (simp add: ren_tr_appt_notick_not_None)

(*--------------------*
 |   [Ev a]t @t ...   |
 *--------------------*)

lemma ren_tr_appt_Ev:
  "[| (a, b) : r ; s [[r]]tr t |]
     ==> ([Ev a]t @t s) [[r]]tr ([Ev b]t @t t)"
apply (insert ren_tr_appt[of "[Ev a]t" r "[Ev b]t" s t])
apply (case_tac "[Ev a]t @t s = None")
by (simp_all)

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

(*** left ***)

(* only if *)

lemma ren_tr_appt_decompo_left_only_if_lm: 
  "ALL r s1 s2 t. (s1 @t s2) [[r]]tr t 
    --> (EX t1 t2. t = t1 @t t2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
apply (rule allI)
apply (rule allI)
apply (induct_tac s1 rule: induct_trace)
apply (simp_all)

(* [Tick]t *)
apply (intro allI impI)
apply (case_tac "[Tick]t @t s2 = None", simp, simp) (* contradict *)

(* [Ev a] @t ... *)
apply (intro allI impI)
apply (simp add: ren_tr_Ev_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]t @t t1" in exI)
apply (rule_tac x="t2" in exI)
apply (simp)
apply (rule_tac x="b" in exI)
apply (rule_tac x="t1" in exI)
by (simp)

(* rule *)

lemma ren_tr_appt_decompo_left_only_if: 
  "(s1 @t s2) [[r]]tr t
    ==> (EX t1 t2. t = t1 @t t2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
by (simp add: ren_tr_appt_decompo_left_only_if_lm)

(* iff *)

lemma ren_tr_appt_decompo_left:
  "t ~= None 
   ==> (s1 @t s2) [[r]]tr t
      = (EX t1 t2. t = t1 @t t2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
apply (rule iffI)
apply (simp add: ren_tr_appt_decompo_left_only_if)
apply (elim conjE exE)
by (simp add: ren_tr_appt)

(*** right ***)

(* only if *)

lemma ren_tr_appt_decompo_right_only_if_lm: 
  "ALL r t1 t2 s. s [[r]]tr (t1 @t t2)
    --> (EX s1 s2. s = s1 @t s2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
apply (rule allI)
apply (rule allI)
apply (induct_tac t1 rule: induct_trace)
apply (simp_all)

(* [Tick]t *)
apply (intro allI impI)
apply (case_tac "[Tick]t @t t2 = None", simp, simp) (* contradict *)

(* [Ev a] @t ... *)
apply (intro allI impI)
apply (simp add: ren_tr_Ev_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]t @t s1" in exI)
apply (rule_tac x="s2" in exI)
apply (simp)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="s1" in exI)
by (simp)

(* rule *)

lemma ren_tr_appt_decompo_right_only_if: 
  "s [[r]]tr (t1 @t t2) 
    ==> (EX s1 s2. s = s1 @t s2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
by (simp add: ren_tr_appt_decompo_right_only_if_lm)

(* iff *)

lemma ren_tr_appt_decompo_right:
  "s ~= None
    ==> s [[r]]tr (t1 @t t2)
      = (EX s1 s2. s = s1 @t s2 & s1 [[r]]tr t1 & s2 [[r]]tr t2)"
apply (rule iffI)
apply (simp add: ren_tr_appt_decompo_right_only_if)
apply (elim conjE exE)
by (simp add: ren_tr_appt)

lemmas ren_tr_appt_decompo
     = ren_tr_appt_decompo_left ren_tr_appt_decompo_right

(*--------------------*
 |   [Ev a]t @t ...   |
 *--------------------*)

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

apply (case_tac "s = None", simp, simp)
apply (simp add: ren_tr_one_decompo)
apply (elim conjE exE, simp)

by (simp add: ren_tr_appt_Ev)

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

lemma ren_tr_last_decompo_Ev[simp]: 
  "(notick s | notick t)
    ==> (s @t [Ev a]t) [[r]]tr (t @t [Ev b]t) = (s [[r]]tr t & (a,b) : r)"
apply (insert ren_tr_appt_decompo_right[of "(s @t [Ev a]t)" r t "[Ev b]t"])
apply (case_tac "s @t [Ev a]t ~= None", simp)

 apply (rule iffI)

  (* => *)
  apply (elim conjE exE)
  apply (simp add: ren_tr_one_decompo)
  apply (elim conjE exE)
  apply (simp)
  apply (case_tac "notick s1", simp, simp)

  (* <= *)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="[Ev a]t" in exI)
  apply (simp)

(* s @t [Ev a]t = None *)
by (auto simp add: ren_tr_notick_right not_None)

lemma ren_tr_last_decompo_Tick[simp]: 
  "(notick s | notick t)
    ==> (s @t [Tick]t) [[r]]tr (t @t [Tick]t) = (s [[r]]tr t)"
apply (insert ren_tr_appt_decompo_right[of "(s @t [Tick]t)" r t "[Tick]t"])
apply (case_tac "notick s")
by (auto simp add: ren_tr_notick_right not_None)

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

(*** ren same length ***)

lemma ren_tr_lengtht:
  "ALL r s t. s [[r]]tr 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)
 apply (drule_tac x="t'" in spec)
by (simp add: ren_tr_not_None)

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

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

(* [Ev a]t @t ... *)
apply (intro allI impI)
apply (elim conjE)
apply (erule disjE, simp)

apply (simp add: ren_tr_Ev_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 @t t" in exI, simp)
apply (rule disjI2)
apply (rule_tac x="t" in exI, simp)
done

(*** rule ***)

lemma ren_tr_prefix:
  "[| prefix v u ; s [[r]]tr u |] ==> (EX t. prefix t s & t [[r]]tr 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]]tr u ;
      !! t. [| prefix t s ; t [[r]]tr v |] ==> R 
   |] ==> R"
apply (insert ren_tr_prefix[of v u s r])
by (auto)

(*************************************************************
                       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] 
declare not_None_eq [simp] 

end