Theory Rep_int_choice

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

theory Rep_int_choice = 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]

(*********************************************************
                        Dom_T
 *********************************************************)

(*** Rep_int_choice_domT ***)

lemma Rep_int_choice_domT: 
  "{t. t = []t | (EX a. t :t [[Pf a]]T ev & a : X) } : 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)
apply (rule disjI2)
apply (rule_tac x="a" in exI, simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Rep_int_choice_memT ***)

lemma Rep_int_choice_memT: 
  "(t :t [[! :X .. Pf]]T ev) = 
   (t = []t | (EX a. t :t [[Pf a]]T ev & a : X))"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Rep_int_choice_domT[simplified memT_def])

(*********************************************************
                        Dom_F
 *********************************************************)

(*** Rep_int_choice_domF ***)

lemma Rep_int_choice_domF: 
  "{f. EX a. f :f [[Pf a]]F ev & a : X } : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="a" in exI, simp)
apply (rule memF_F2, simp_all)
done

(*** Rep_int_choice_memT ***)

lemma Rep_int_choice_memF: 
  "(f :f [[! :X .. Pf]]F ev) = 
   (EX a. f :f [[Pf a]]F ev & a : X)"
apply (simp add: evalF_def)
by (simp add: memF_def Abs_domF_inverse Rep_int_choice_domF[simplified memF_def])

lemmas Rep_int_choice_mem = Rep_int_choice_memT Rep_int_choice_memF

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

(* T2 *)

lemma Rep_int_choice_T2 :
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_T2 ([[! :X .. Pf]]T ev, [[! :X .. Pf]]F ev)"
apply (simp add: HC_T2_def Rep_int_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule disjI2)
apply (drule_tac x="a" in spec)
apply (rule_tac x="a" in exI)
apply (simp add: domSF_def HC_T2_def)
by (auto)

(* F3 *)

lemma Rep_int_choice_F3 :
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_F3 ([[! :X .. Pf]]T ev, [[! :X .. Pf]]F ev)"
apply (simp add: HC_F3_def Rep_int_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (drule_tac x="a" in spec)
apply (rule_tac x="a" 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="Xa" 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="a" in spec, simp)
by (simp)

(* T3_F4 *)

lemma Rep_int_choice_T3_F4 : 
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_T3_F4 ([[! :X .. Pf]]T ev, [[! :X .. Pf]]F ev)"
apply (simp add: HC_T3_F4_def Rep_int_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (drule_tac x="a" in spec)

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

(*** Rep_int_choice_domSF ***)

lemma Rep_int_choice_domSF : 
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> ([[! :X .. Pf]]T ev, [[! :X .. Pf]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Rep_int_choice_T2)
apply (simp add: Rep_int_choice_F3)
apply (simp add: Rep_int_choice_T3_F4)
done

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

(*** T ***)

lemma Rep_int_choice_evalT_mono:
  "ALL a:X. [[Pf a]]T ev1 <= [[Qf a]]T ev2
   ==> [[! :X .. Pf]]T ev1 <= [[! :X .. Qf]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Rep_int_choice_memT)
apply (erule disjE, simp)

apply (elim conjE exE)
apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="t" in spec, simp)
apply (rule disjI2)
apply (rule_tac x="a" in exI)
by (simp)

(*** F ***)

lemma Rep_int_choice_evalF_mono:
  "ALL a:X. [[Pf a]]F ev1 <= [[Qf a]]F ev2
   ==> [[! :X .. Pf]]F ev1 <= [[! :X .. Qf]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Rep_int_choice_memF)

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

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end