Theory Int_choice

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

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

(*** Int_choice_memT ***)

lemma Int_choice_memT: 
  "(t :t [[P |~| Q]]T ev) = (t :t [[P]]T ev | t :t [[Q]]T ev)"
by (simp add: evalT_def memT_UnT)

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

(*** Int_choice_memF ***)

lemma Int_choice_memF: 
  "(f :f [[P |~| Q]]F ev) = (f :f [[P]]F ev | f :f [[Q]]F ev)"
by (simp add: evalF_def memF_UnF)

lemmas Int_choice_mem = Int_choice_memT Int_choice_memF

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

(* T2 *)

lemma Int_choice_T2 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T2 ([[P |~| Q]]T ev, [[P |~| Q]]F ev)"
apply (simp add: HC_T2_def Int_choice_mem)
apply (simp add: domSF_def HC_T2_def)
by (auto)

(* F3 *)

lemma Int_choice_F3 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_F3 ([[P |~| Q]]T ev, [[P |~| Q]]F ev)"
apply (simp add: HC_F3_def Int_choice_mem)
apply (simp add: domSF_def HC_F3_def)
by (auto)

(* T3_F4 *)

lemma Int_choice_T3_F4 : 
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T3_F4 ([[P |~| Q]]T ev, [[P |~| Q]]F ev)"
apply (simp add: HC_T3_F4_def Int_choice_mem)
apply (simp add: domSF_iff HC_T3_F4_def)
by (auto)

(*** Int_choice_domSF ***)

lemma Int_choice_domSF : 
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> ([[P |~| Q]]T ev, [[P |~| Q]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Int_choice_T2)
apply (simp add: Int_choice_F3)
apply (simp add: Int_choice_T3_F4)
done

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

(*** T ***)

lemma Int_choice_evalT_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; [[Q1]]T ev1 <= [[Q2]]T ev2 |]
   ==> [[P1 |~| Q1]]T ev1 <= [[P2 |~| Q2]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Int_choice_memT)
apply (erule disjE)
by (simp_all)

(*** F ***)

lemma Int_choice_evalF_mono:
  "[| [[P1]]F ev1 <= [[P2]]F ev2 ; [[Q1]]F ev1 <= [[Q2]]F ev2 |]
   ==> [[P1 |~| Q1]]F ev1 <= [[P2 |~| Q2]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Int_choice_memF)
apply (erule disjE)
by (simp_all)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end