Theory Act_prefix

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

theory Act_prefix = CSP_semantics:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  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
 *********************************************************)

(*** Act_prefix_domT ***)

lemma Act_prefix_domT: 
  "{t. t = []t | (EX s. t = [Ev a]t @t s & 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)

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

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

apply (elim conjE exE, simp)
apply (erule disjE, simp)    (* None --> contradict *)
apply (erule disjE, simp)    (* []t *)

apply (elim conjE exE, simp)
apply (rule_tac x="v'" in exI, simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Act_prefix_memT ***)

lemma Act_prefix_memT: 
  "(t :t [[a -> P]]T ev) = (t = []t | (EX s. t = [Ev a]t @t s & s :t [[P]]T ev))"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Act_prefix_domT[simplified memT_def])

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

(*** Act_prefix_domF ***)

lemma Act_prefix_domF: 
  "{f. (EX X.   f = ([]t,X) & Ev a ~: X) |
       (EX s X. f = ([Ev a]t @t s, X) & (s,X) :f [[P]]F ev) } : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule_tac x="sa" in exI, simp)
apply (rule memF_F2, simp_all)
done

(*** Act_prefix_memT ***)

lemma Act_prefix_memF: 
  "(f :f [[a -> P]]F ev) = ((EX X.   f = ([]t,X) & Ev a ~: X) |
                            (EX s X. f = ([Ev a]t @t s, X) & (s,X) :f [[P]]F ev))"
apply (simp add: evalF_def)
by (simp add: memF_def Abs_domF_inverse Act_prefix_domF[simplified memF_def])

lemmas Act_prefix_mem = Act_prefix_memT Act_prefix_memF

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

(* T2 *)

lemma Act_prefix_T2 :
  "([[P]]T ev, [[P]]F ev) : domSF ==> HC_T2 ([[a -> P]]T ev, [[a -> P]]F ev)"
apply (simp add: HC_T2_def Act_prefix_mem)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rule_tac x="sa" in exI, simp)

apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(* F3 *)

lemma Act_prefix_F3 :
  "([[P]]T ev, [[P]]F ev) : domSF ==> HC_F3 ([[a -> P]]T ev, [[a -> P]]F ev)"
apply (simp add: HC_F3_def Act_prefix_mem)
apply (intro allI impI)

apply (elim conjE disjE, simp)
apply (case_tac "Ev a ~: Y", simp)  (* show "Ev a : Y --> contradict" *)
apply (drule_tac x="Ev a" in spec, simp)
apply (drule_tac x="[]t" in spec, simp)

apply (elim conjE exE, simp)
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="X" in spec)
apply (drule_tac x="Y" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="aa" in spec, simp)
 apply (drule_tac x="sa @t [aa]t" in spec, simp)
by (simp)

(* T3_F4 *)

lemma Act_prefix_T3_F4 : 
  "([[P]]T ev, [[P]]F ev) : domSF ==> HC_T3_F4 ([[a -> P]]T ev, [[a -> P]]F ev)"
apply (simp add: HC_T3_F4_def Act_prefix_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)
apply (simp add: not_None)

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

apply (elim conjE exE)      (* s = [Ev a]t @t sb *)
apply (simp add: not_None)

apply (simp add: domSF_iff HC_T3_F4_def)
apply (elim conjE exE)
apply (drule_tac x="sb" in spec)
by (simp)

(*** Act_prefix_domSF ***)

lemma Act_prefix_domSF : 
  "([[P]]T ev, [[P]]F ev) : domSF ==> ([[a -> P]]T ev, [[a -> P]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Act_prefix_T2)
apply (simp add: Act_prefix_F3)
apply (simp add: Act_prefix_T3_F4)
done

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

(*** T ***)

lemma Act_prefix_evalT_mono:
  "[[P]]T ev1 <= [[Q]]T ev2 ==> [[a -> P]]T ev1 <= [[a -> Q]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Act_prefix_memT)
apply (erule disjE, simp)

apply (elim conjE exE)
apply (drule_tac x="s" in spec)
apply (simp)
apply (rule_tac x="s" in exI)
by (simp)

(*** F ***)

lemma Act_prefix_evalF_mono:
  "[[P]]F ev1 <= [[Q]]F ev2 ==> [[a -> P]]F ev1 <= [[a -> Q]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Act_prefix_memF)
apply (erule disjE, simp)

apply (elim conjE exE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="X" in spec)
apply (simp)
apply (rule_tac x="sa" in exI)
by (simp)

(****************** to add them again ******************)

declare disj_not1   [simp]
declare not_None_eq [simp]

end