Theory Trace_hide

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

theory Trace_hide = 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. 

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


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

inductive "hidex X"
intros
hidex_None:
  "(0, None, None) : hidex X"

hidex_nil:
  "(0, []t, []t) : hidex X"

hidex_Tick:
  "(Suc 0, [Tick]t, [Tick]t) : hidex X"

hidex_in: 
  "[| (n, s, t) : hidex X ; a : X ; s ~= None |]
   ==> (Suc n, [Ev a]t @t s, t) : hidex X"

hidex_notin: 
  "[| (n, s, t) : hidex X ; a ~: X ;  s ~= None |]
   ==> (Suc n, [Ev a]t @t s, [Ev a]t @t t) : hidex X"

consts
  hide_tr  :: "'a trace => 'a set => 'a trace"
                                    ("_ --tr _" [84,85] 84)

defs
  hide_tr_def : 
    "s --tr X == THE t. (lengtht s, s, t) : hidex X"

(*************************************************************
                       hidex None
 *************************************************************)

lemma hidex_None_None_only_if: 
  "ALL X n s. (n, None, s) : hidex X --> (n = 0 & s = None)"
apply (intro allI)
apply (induct_tac n)
apply (intro allI impI)
apply (erule hidex.elims)
apply (simp, simp, simp, simp, simp)

apply (rule impI)
apply (erule hidex.elims)
by (simp_all)

(*** iff ***)

lemma hidex_None_None[simp]: 
  "(n, None, s) : hidex X = (n = 0 & s = None)"
apply (intro iffI)
apply (simp add: hidex_None_None_only_if)
by (simp add: hidex.intros)

(*************************************************************
                    hidex imples "not None"
 *************************************************************)

lemma hidex_not_None_only_if_lm: 
  "ALL X n s t. ((n, s, t) : hidex X & s ~= None) --> t ~= None"
apply (rule allI)
apply (rule allI)
apply (induct_tac n)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims)
apply (simp, simp, simp, simp, simp)

(* step case *)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims)
apply (erule rem_asmE, simp)
apply (erule rem_asmE, simp)
apply (erule rem_asmE, simp)

apply (drule_tac x="sa" in spec)
apply (drule_tac x="ta" in spec)
apply (simp)

apply (drule_tac x="sa" in spec)
apply (drule_tac x="ta" in spec)
apply (simp)
done

lemma hidex_not_None_only_if: 
  "[| (n, s, t) : hidex X ; s ~= None |] ==> t ~= None"
apply (insert hidex_not_None_only_if_lm)
apply (drule_tac x="X" in spec)
apply (drule_tac x="n" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

(*** if ***)

lemma hidex_not_None_if_lm: 
  "ALL X n s t. ((n, s, t) : hidex X & t ~= None) --> s ~= None"
apply (rule allI)
apply (rule allI)
apply (induct_tac n)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims)
apply (simp, simp, simp, simp, simp)

(* step case *)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims)
apply (erule rem_asmE, simp)
apply (erule rem_asmE, simp)
apply (erule rem_asmE, simp)

apply (drule_tac x="sa" in spec)
apply (drule_tac x="ta" in spec)
apply (simp)

apply (drule_tac x="sa" in spec)
apply (drule_tac x="ta" in spec)
apply (simp)
done

lemma hidex_not_None_if: 
  "[| (n, s, t) : hidex X ; t ~= None |] ==> s ~= None"
apply (insert hidex_not_None_if_lm)
apply (drule_tac x="X" in spec)
apply (drule_tac x="n" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
by (simp)

(*** thus ***)

lemma hidex_None_or_not_lm: 
  "ALL X n s t. (n, s, t) : hidex X 
     --> (s = None & t = None) | (s ~= None & t ~= None)"
apply (intro allI impI)
apply (case_tac "s = None & t = None", simp)
apply (simp)
apply (rule disjI2)
apply (erule disjE)
apply (simp, rule hidex_not_None_only_if, simp, simp)
apply (simp, rule hidex_not_None_if, simp, simp)
done

lemma hidex_None_or_not: 
  "(n, s, t) : hidex X 
   ==> (s = None & t = None) | (s ~= None & t ~= None)"
by (simp add: hidex_None_or_not_lm)

(*************************************************************
                       THE hidex 
 *************************************************************)

(*** exists ***)

lemma hidex_exists_not_None_lm: 
  "ALL X s. (EX t. (lengtht s, s, t) : hidex X)"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp add: hidex.intros)

apply (simp_all)
apply (rule_tac x="[]t" in exI, simp add: hidex.intros)
apply (rule_tac x="[Tick]t" in exI, simp add: hidex.intros)

apply (elim exE)
apply (case_tac "a : X")
apply (rule_tac x="t" in exI, simp add: hidex.intros)
apply (rule_tac x="[Ev a]t @t t" in exI, simp add: hidex.intros)
done

(*** exists !! ***)

lemma hidex_exists: 
  "EX t. (lengtht s, s, t) : hidex X"
by (simp add: hidex_exists_not_None_lm)

(*** unique ***)

lemma hidex_unique_lm: 
  "ALL X s t u. ((lengtht s, s, t) : hidex X & (lengtht s, s, u) : hidex X)
    --> t = u"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)

(* []t *)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims, simp_all)
apply (erule hidex.elims, simp_all)

(* [Tick]t *)
apply (intro allI impI)
apply (erule conjE)
apply (erule hidex.elims, simp_all)
apply (erule hidex.elims, simp_all)

(* step *)
apply (intro allI impI)
apply (erule conjE)
apply (case_tac "a : X")
 apply (erule hidex.elims, simp_all)
 apply (erule hidex.elims, simp_all)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="u" in spec)
 apply (elim conjE, simp)

 apply (erule hidex.elims, simp_all)
 apply (erule hidex.elims, simp_all)
 apply (drule_tac x="ta" in spec)
 apply (drule_tac x="tb" in spec)
 apply (elim conjE, simp)
done

lemma hidex_unique: 
  "[| (lengtht s, s, t) : hidex X ; (lengtht s, s, u) : hidex X |]
   ==> t = u"
apply (insert hidex_unique_lm)
apply (drule_tac x="X" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="t" in spec)
apply (drule_tac x="u" in spec)
apply (simp)
done

(*************************************************************
                       THE hidex 
 *************************************************************)

lemma hidex_to_hide_tr : 
    "(lengtht s, s, t) : hidex X = (t = s --tr X)"
apply (simp add: hide_tr_def)
apply (rule iffI)
apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: hidex_unique)

apply (simp)
apply (insert hidex_exists[of s X])
apply (erule exE)
apply (rule theI[of "(%x. (lengtht s, s, x) : hidex X)"])
apply (simp)
apply (simp add: hidex_unique)
done

lemma hide_tr_to_hidex : 
    "(s --tr X = t) = ((lengtht s, s, t) : hidex X)"
apply (simp add: hidex_to_hide_tr)
by (fast)

lemma hide_tr_to_hidex_sym : 
    "(t = s --tr X) = ((lengtht s, s, t) : hidex X)"
by (simp add: hidex_to_hide_tr)

lemmas hide_tr_iff = hide_tr_to_hidex hide_tr_to_hidex_sym

(*************************************************************
                         hide_tr
 *************************************************************)

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

lemma hide_tr_None[simp] : "None --tr X = None"
by (simp add: hide_tr_to_hidex)

lemma hide_tr_nil[simp] : "[]t --tr X = []t"
apply (simp add: hide_tr_to_hidex)
by (simp add: hidex.intros)

lemma hide_tr_Tick[simp] : "[Tick]t --tr X = [Tick]t"
apply (simp add: hide_tr_to_hidex)
by (simp add: hidex.intros)

lemma hide_tr_in_lm : 
  "[| a : X ;  t = s --tr X |]
   ==> ([Ev a]t @t s) --tr X = t"
apply (simp add: hide_tr_to_hidex_sym)
apply (case_tac "s ~= None")
apply (simp add: hide_tr_to_hidex)
apply (simp add: hidex.intros)
apply (simp add: hide_tr_to_hidex)
done

lemma hide_tr_in[simp] : 
  "a : X ==> ([Ev a]t @t s) --tr X = s --tr X"
by (simp add: hide_tr_in_lm)

lemma hide_tr_in_one[simp] : 
  "a : X ==> [Ev a]t --tr X = []t"
apply (insert hide_tr_in[of a X "[]t"])
by (simp)

lemma hide_tr_notin_lm : 
  "[| a ~: X ;  t = s --tr X |]
   ==> ([Ev a]t @t s) --tr X = [Ev a]t @t t"
apply (simp add: hide_tr_to_hidex_sym)
apply (case_tac "s ~= None")
apply (simp add: hide_tr_to_hidex)
apply (simp add: hidex.intros)
apply (simp add: hide_tr_to_hidex)
done

lemma hide_tr_notin_appt[simp] : 
  "a ~: X ==> ([Ev a]t @t s) --tr X = [Ev a]t @t (s --tr X)"
by (simp add: hide_tr_notin_lm)

lemma hide_tr_notin[simp] : 
  "a ~: X ==> [Ev a]t --tr X = [Ev a]t"
apply (insert hide_tr_notin_appt[of a X "[]t"])
by (simp)

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

lemma hide_tr_elims_lm:
  "[| s --tr X = t ;
      (( s = None & t = None ) --> P) ;
      (( s = []t & t = []t ) --> P) ;
      (( s = [Tick]t & t = [Tick]t ) --> P) ;
      ( ALL a s'.
        ((s = [Ev a]t @t s' & s' --tr X = t & a : X & s' ~= None )
         --> P)) ;
      ( ALL a s' t'.
        ((s = [Ev a]t @t s' & t = [Ev a]t @t t' & s' --tr X = t' & a ~: X & s' ~= None )
         --> P)) |]
   ==> P"
apply (simp add: hide_tr_iff)
apply (erule hidex.elims)
apply (simp_all)
apply (elim conjE, simp)
apply (elim conjE, simp)
apply (drule mp)
apply (rule_tac x="ta" in exI, simp, simp)
done

lemma hide_tr_elims:
  "[| s --tr X = t; 
      [| s = None ; t = None |] ==> P; 
      [| s = []t ; t = []t |] ==> P; 
      [| s = [Tick]t ; t = [Tick]t |] ==> P; 
   !!a s'.
      [| s = [Ev a]t @t s' ; s' --tr X = t; a : X; s' ~= None |]
      ==> P;
   !!a s' t'.
      [| s = [Ev a]t @t s' ; t = [Ev a]t @t t' ; s' --tr X = t' ; a ~: X; s' ~= None |]
      ==> P |]
   ==> P"
apply (rule hide_tr_elims_lm[of s X t])
apply (simp_all)
by (force)+

(*------------------*
 |     not None     |
 *------------------*)

lemma hide_tr_not_None_only_if: "s --tr X ~= None ==> s ~= None"
apply (simp add: hide_tr_iff)
apply (erule contrapos_nn)
by (simp)

lemma hide_tr_not_None_if: "s ~= None ==> s --tr X ~= None"
apply (simp add: hide_tr_iff)
apply (erule contrapos_nn)
apply (insert hidex_None_or_not[of "lengtht s" s "None" X])
by (simp)

lemma hide_tr_not_None[simp]: "(s --tr X ~= None) = (s ~= None)"
apply (rule iffI)
apply (rule hide_tr_not_None_only_if, simp)
by (simp add: hide_tr_not_None_if)

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

lemma hide_tr_None_None[simp]: "(s --tr X = None) = (s = None)"
apply (rule iffI)
apply (erule contrapos_pp, simp)
apply (erule contrapos_pp, simp)
done

lemma hide_tr_None_None_sym[simp]: "(None = s --tr X) = (s = None)"
apply (insert hide_tr_None_None[of s X])
by (auto simp del: hide_tr_None_None)

(*************************************************************
        a new event is not introduced by HIDE (trace)
 *************************************************************)

lemma hide_tr_in_event[simp]:
  "e : sett (s --tr X) = (e ~: Ev ` X & e : sett s)"
apply (induct_tac s rule: induct_trace)
apply (simp)
apply (simp)
apply (simp, force)

apply (simp)
apply (case_tac "a : X")
apply (simp)
apply (rule iffI, simp, force)

apply (simp add: hide_tr_not_None_if)
apply (rule iffI, force, force)
done

(*** notick ***)

lemma hide_tr_notick[simp]: "notick (s --tr X) = notick s"
apply (simp add: notick_def)
apply (rule iffI)
apply (force)
apply (simp)
done

(*************************************************************
                  appended traces in hide
 *************************************************************)

lemma hide_tr_appt_notick_lm:
  "ALL X s e t. notick s --> ((s @t t) --tr X = (s --tr X) @t (t --tr X))"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)

apply (intro allI impI, simp)
apply (case_tac "a : X")
by (simp_all)

(*** simp ***)

lemma hide_tr_appt[simp]:
  "s @t t ~= None ==> (s @t t) --tr X = (s --tr X) @t (t --tr X)"
apply (simp add: decompo_appt_not_None)
apply (elim conjE)
apply (erule disjE)
apply (simp add: hide_tr_appt_notick_lm)
by (simp)

(*************************************************************
                 decompose traces in hide
 *************************************************************)

lemma hide_tr_decompo_lm:
  "ALL X u s t.
      (u ~= None & u --tr X = s @t t)
      --> (EX s' t'. u = s' @t t' &
                     s = s' --tr X & t = t' --tr X) "
apply (rule allI)
apply (rule allI)
apply (induct_tac u rule: induct_trace)
apply (simp)
apply (simp)

apply (intro allI impI)
apply (simp)
apply (erule disjE)
apply (rule_tac x="[Tick]t" in exI)
apply (rule_tac x="[]t" in exI)
apply (simp)
apply (rule_tac x="[]t" in exI)
apply (rule_tac x="[Tick]t" in exI)
apply (simp)

apply (intro allI impI)
apply (erule conjE)
apply (erule hide_tr_elims)
apply (simp_all)

 (* a : X *)
 apply (drule_tac x="sa" in spec)
 apply (drule_tac x="t" in spec)
 apply (simp)
 apply (elim conjE exE)
 apply (simp)

 apply (rule_tac x="[Ev aa]t @t s'a" in exI)
 apply (rule_tac x="t'" in exI)
 apply (simp)

 (* a ~: X *)
 apply (case_tac "sa = None", simp add: hide_tr_not_None_if)
 apply (case_tac "t' = None", simp add: hide_tr_not_None_if)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (rotate_tac -1)
 apply (drule_tac x="sa" in spec, simp)

  (* []t *)
  apply (erule disjE)
  apply (rule_tac x="[]t" in exI, simp)

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

  (* [Ev a]t @t ... *)
  apply (elim exE)
  apply (simp)
  apply (drule_tac x="sb" in spec)
  apply (drule_tac x="t" in spec)
  apply (simp)
  apply (elim conjE exE)

  apply (rule_tac x="[Ev aa]t @t s'a" in exI)
  apply (rule_tac x="t'a" in exI)
  apply (simp)
done

(*** simp ***)

lemma hide_tr_decompo:
  "[| u ~= None ; u --tr X = s @t t |]
     ==> (EX s' t'. u = s' @t t' &
                    s = s' --tr X & t = t' --tr X) "
by (simp add: hide_tr_decompo_lm)

(*************************************************************
                  hide trace prefix_closed
 *************************************************************)

lemma hide_tr_prefix_only_if_lm:
 "ALL X s u. (s ~= None & prefix u (s --tr X)) 
    --> (EX t. u = t --tr X & prefix t s)"
apply (rule allI)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)

(* Tick *)
apply (force)

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

 apply (case_tac "a : X")
 apply (drule_tac x="u" in spec, simp)
 apply (elim conjE exE)
 apply (rule_tac x="[Ev a]t @t t" in exI, simp)
 apply (rule_tac x="t" in exI, simp)

 (* a ~: X *)
 apply (simp)

  (* u = []t *)
  apply (erule disjE)
  apply (rule_tac x="[]t" in exI, simp)

  (* u = [Ev a]t @t ... *)
  apply (elim conjE exE)
  apply (drule_tac x="v'" in spec, simp)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev a]t @t t" in exI, simp)
  apply (rule_tac x="t" in exI, simp)
done

lemma hide_tr_prefix_only_if:
 "[| s ~= None ; prefix u (s --tr X) |] 
    ==> (EX t. u = t --tr X & prefix t s)"
by (simp add: hide_tr_prefix_only_if_lm)

(*** if ***)

lemma hide_tr_prefix_if:
 "[| s ~= None ; prefix t s |] ==> prefix (t --tr X) (s --tr X)"
apply (simp add: prefix_def)
apply (erule exE)
apply (simp)
apply (rule_tac x="u --tr X" in exI)
by (simp)

lemma hide_tr_prefix:
 "s ~= None ==> prefix u (s --tr X) = (EX t. u = t --tr X & prefix t s)"
apply (rule iffI)
apply (simp add: hide_tr_prefix_only_if)
apply (erule exE)
by (simp add: hide_tr_prefix_if)

(*************************************************************
                  hide + alpha lemma
 *************************************************************)

(* rev []t *)

(* only if *)

lemma hide_tr_nilt_sett_only_if_lm:
  "ALL s. (s ~= None & s --tr X = []t) --> (sett s <= Ev ` X)"
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)
apply (intro allI impI)
apply (elim conjE exE)
apply (case_tac "a : X")
by (simp_all)

lemma hide_tr_nilt_sett_only_if:
  "[| s ~= None ; s --tr X = []t |] ==> (sett s <= Ev ` X)"
by (simp add: hide_tr_nilt_sett_only_if_lm)

(* if *)

lemma hide_tr_nilt_sett_if_lm:
  "ALL s. (s ~= None & sett s <= Ev ` X) --> s --tr X = []t"
apply (rule allI)
apply (induct_tac s rule: induct_trace)
apply (simp_all)
apply (force)
apply (intro allI impI)
apply (elim conjE)
apply (simp)
apply (case_tac "a : X")
by (auto)

lemma hide_tr_nilt_sett_if:
  "[| s ~= None ; sett s <= Ev ` X |] ==> s --tr X = []t"
by (simp add: hide_tr_nilt_sett_if_lm)

(* iff *)

lemma hide_tr_nilt_sett:
  "s ~= None ==> (s --tr X = []t) = (sett s <= Ev ` X)"
apply (rule iffI)
apply (simp add: hide_tr_nilt_sett_only_if)
apply (simp add: hide_tr_nilt_sett_if)
done

(* rev [Tick]t *)

(* only if *)

lemma hide_tr_Tick_sett_only_if_lm:
  "ALL s. (s ~= None & s --tr X = [Tick]t) 
    --> (EX s'. s = s' @t [Tick]t & sett s' <= Ev ` X)"
apply (rule allI)
apply (induct_tac s rule: rev_induct_trace)
apply (simp_all)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: not_None)

apply (erule disjE)
 apply (simp)
 apply (elim conjE exE, simp)

 apply (simp)
 apply (rule conjI)
 apply (insert event_tick_or_Ev)
 apply (drule_tac x="e" in spec)
 apply (erule disjE, simp)
 apply (erule exE)
 apply (case_tac "a : X")
 apply (simp_all add: not_None hide_tr_nilt_sett)
done

lemma hide_tr_Tick_sett_only_if:
  "[| s ~= None ; s --tr X = [Tick]t |]
    ==> (EX s'. s = s' @t [Tick]t & sett s' <= Ev ` X)"
by (simp add: hide_tr_Tick_sett_only_if_lm)

(* if *)

lemma hide_tr_Tick_sett_if:
  "[| s @t [Tick]t ~= None ; sett s <= Ev ` X |]
   ==> s --tr X = []t"
apply (case_tac "s = None", simp)
by (simp add: not_None hide_tr_nilt_sett)

(* iff *)

lemma hide_tr_Tick_sett:
  "s ~= None ==> (s --tr X = [Tick]t)
               = (EX s'. s = s' @t [Tick]t & sett s' <= Ev ` X)"
apply (rule iffI)
apply (simp add: hide_tr_Tick_sett_only_if)
apply (elim conjE exE)
apply (simp add: hide_tr_Tick_sett_if)
done

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

declare disj_not1 [simp] 
declare not_None_eq [simp] 

end