Theory Hiding

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

theory Hiding = CSP_semantics:

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

(*********************************************************
                        DomT
 *********************************************************)

(*** Hiding_domT ***)

lemma Hiding_domT : 
  "{t. EX s. t = s --tr X & s :t [[P]]T ev } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="[]t" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: not_None hide_tr_prefix)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Hiding_memT ***)

lemma Hiding_memT:
  "(t :t [[P -- X]]T ev) = 
   (EX s. t = s --tr X & s :t [[P]]T ev)"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Hiding_domT[simplified memT_def])

(*********************************************************
                         DomF
 *********************************************************)

(*** Hiding_domF ***)

lemma Hiding_domF : 
  "{f. EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f [[P]]F ev} : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac t Y Z s)
apply (rule_tac x="s" in exI)
apply (simp)
by (rule memF_F2, simp, force)

lemma Hiding_memF:
  "(f :f [[P -- X]]F ev) = 
   (EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f [[P]]F ev)"
apply (simp only: evalF_def)
by (simp add: memF_def Abs_domF_inverse Hiding_domF[simplified memF_def])

lemmas Hiding_mem = Hiding_memT Hiding_memF

(*********************************************************
                         domSF
 *********************************************************)

(*** T2 ***)

lemma Hiding_T2 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_T2 ([[P -- X]]T ev, [[P -- X]]F ev)"
apply (simp add: HC_T2_def Hiding_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(*** F3 ***)

lemma Hiding_F3 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_F3 ([[P -- X]]T ev, [[P -- X]]F ev)"
apply (simp add: HC_F3_def Hiding_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rename_tac t Y Z s)
apply (rule_tac x="s" in exI, simp)

apply (simp add: domSF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="Ev ` X Un Y" in spec)
apply (drule_tac x="Z - Ev ` X" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="a" in spec)
 apply (simp)

 apply (insert event_tick_or_Ev)
 apply (drule_tac x="a" in spec)
 apply (erule disjE)
  (* Tick *)
  apply (drule_tac x="s @t [Tick]t" in spec)
  apply (simp add: not_None)
  (* Ev *)
  apply (elim conjE exE)
  apply (drule_tac x="s @t [Ev aa]t" in spec)
  apply (simp add: not_None)
  apply (subgoal_tac "aa ~: X", simp_all)
  apply (force)

apply (subgoal_tac "Ev ` X Un Y Un (Z - Ev ` X) = Ev ` X Un (Y Un Z)", simp)
by (auto)

(* T3_F4 *)

lemma Hiding_T3_F4 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_T3_F4 ([[P -- X]]T ev, [[P -- X]]F ev)"
apply (simp add: HC_T3_F4_def Hiding_mem)
apply (intro allI impI)
apply (elim conjE exE)

apply (insert hide_tr_decompo_lm)
apply (drule_tac x="X" in spec)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="[Tick]t" in spec)
apply (simp add: not_None)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (drule sym)

apply (subgoal_tac "(EX t''. t' = t'' @t [Tick]t & sett t'' <= Ev ` X)")
 apply (elim conjE exE)
 apply (case_tac "(s' @t t'') = None", simp add: appt_ass_rev del: appt_ass)
 apply (case_tac "t'' = None", simp)

 (* F4 *)
 apply (rule conjI)
  apply (rule_tac x="s' @t t''" in exI)
  apply (simp)
  apply (subgoal_tac "t'' --tr X = []t", simp)
   apply (simp add: domSF_def HC_F4_def)
   apply (elim conjE)
   apply (drule_tac x="s' @t t''" in spec)
   apply (subgoal_tac "notick t''")
    apply (simp)
   apply (simp add: notick_def)
   apply (force)
  apply (rule hide_tr_nilt_sett_if)
   apply (simp)
  apply (simp)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="sa" in exI, simp)
 apply (simp add: domSF_def HC_T3_def)
 apply (elim conjE)
 apply (drule_tac x="s' @t t''" in spec, simp)
 apply (case_tac "~ notick t''", simp, simp)

apply (rule hide_tr_Tick_sett_only_if)
apply (case_tac "t' = None")
by (simp_all)

(*** Hiding_domSF ***)

lemma Hiding_domSF :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> ([[P -- X]]T ev, [[P -- X]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Hiding_T2)
apply (simp add: Hiding_F3)
apply (simp add: Hiding_T3_F4)
done

(*********************************************************
                      mono
 *********************************************************)

(*** T ***)

lemma Hiding_evalT_mono:
  "[[P1]]T ev1 <= [[P2]]T ev2 ==> [[P1 -- X]]T ev1 <= [[P2 -- X]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Hiding_memT)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
by (simp_all)

(*** F ***)

lemma Hiding_evalF_mono:
  "[[P1]]F ev1 <= [[P2]]F ev2 ==> [[P1 -- X]]F ev1 <= [[P2 -- X]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Hiding_memF)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
by (simp_all)

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

declare disj_not1   [simp] 
declare not_None_eq [simp]

end