Theory Renaming

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

theory Renaming = 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
 *********************************************************)

(*** Renaming_domT ***)

lemma Renaming_domT : "{t. EX s. s [[r]]tr t & 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 (erule ren_tr_prefixE, simp)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Renaming_memT ***)

lemma Renaming_memT:
  "(t :t [[P [[r]]]]T ev) = 
   (EX s. s [[r]]tr t & s :t [[P]]T ev)"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Renaming_domT[simplified memT_def])

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

(*** Renaming_domF ***)

lemma Renaming_domF : 
  "{f. EX s t X. f = (t,X) & s [[r]]tr t & 
                 (s, [[r]]inv X) :f [[P]]F ev } : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp)
apply (rule memF_F2, simp)
apply (rule ren_inv_sub, simp)
done

lemma Renaming_memF:
  "(f :f [[P [[r]]]]F ev) = 
   (EX s t X. f = (t,X) & s [[r]]tr t & (s, [[r]]inv X) :f [[P]]F ev)"
apply (simp add: evalF_def)
by (simp add: memF_def Abs_domF_inverse Renaming_domF[simplified memF_def])

lemmas Renaming_mem = Renaming_memT Renaming_memF

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

(*** T2 ***)

lemma Renaming_T2 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_T2 ([[P [[r]]]]T ev, [[P [[r]]]]F ev)"
apply (simp add: HC_T2_def Renaming_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 Renaming_F3 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_F3 ([[P [[r]]]]T ev, [[P [[r]]]]F ev)"
apply (simp add: HC_F3_def Renaming_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI, simp)

apply (simp add: domSF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="[[r]]inv X" in spec)
apply (drule_tac x="[[r]]inv Y" in spec)

apply (drule mp)
 apply (simp add: ren_tr_notick_right)
 apply (intro allI impI)
 apply (simp add: ren_inv_def)
 apply (erule bexE)
 apply (fold ren_inv_def)
 apply (drule_tac x="eb" in spec, simp)

  (* Tick *)
  apply (erule disjE)
  apply (drule_tac x=" sa @t [a]t" in spec)
  apply (simp)
  (* Ev *)
  apply (elim conjE exE)
  apply (drule_tac x=" sa @t [Ev aa]t" in spec)
  apply (simp)
by (simp)

(* T3_F4 *)

lemma Renaming_T3_F4 :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> HC_T3_F4 ([[P [[r]]]]T ev, [[P [[r]]]]F ev)"
apply (simp add: HC_T3_F4_def Renaming_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (case_tac "sa = None", simp)
apply (simp add: ren_tr_appt_decompo)
apply (elim conjE exE)
apply (case_tac "~ notick s1", simp)
apply (simp)

 (* F4 *)
 apply (rule conjI)
 apply (rule_tac x="s1" in exI, simp)
 apply (simp add: domSF_def HC_F4_def)
 apply (elim conjE)
 apply (drule_tac x="s1" in spec, simp)
 apply (rule memF_F2, simp, simp)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="s1 @t [Tick]t" in exI, simp)
 apply (simp add: domSF_def HC_T3_def)
done

(*** Renaming_domSF ***)

lemma Renaming_domSF :
  "([[P]]T ev, [[P]]F ev) : domSF
     ==> ([[P [[r]]]]T ev, [[P [[r]]]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Renaming_T2)
apply (simp add: Renaming_F3)
apply (simp add: Renaming_T3_F4)
done

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

(*** T ***)

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

(*** F ***)

lemma Renaming_evalF_mono:
  "[[P1]]F ev1 <= [[P2]]F ev2 ==> [[P1 [[r]]]]F ev1 <= [[P2 [[r]]]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Renaming_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