Theory CSP_law_commut

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

theory CSP_law_commut = CSP_proc:

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*****************************************************************

         1. Commutativity
         2.
         3. 
         4. 

 *****************************************************************)

(*********************************************************
                      Ext choice
 *********************************************************)

lemma domSF_Ext_choice_commut:
  "[[P [+] Q]]SF ev = [[Q [+] P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)
apply (rule eq_iffI)
apply (rule, simp add: Ext_choice_mem, fast)+

apply (rule eq_iffI)
apply (rule, simp add: Ext_choice_mem UnT_commut IntF_commut UnF_commut)+
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Ext_choice_commut:
  "LET:fp df IN P [+] Q =F LET:fp df IN Q [+] P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Ext_choice_commut)

(*********************************************************
                      Int choice
 *********************************************************)

lemma domSF_Int_choice_commut:
  "[[P |~| Q]]SF ev = [[Q |~| P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)
apply (rule eq_iffI)
apply (rule, simp add: Int_choice_mem, fast)+

apply (rule eq_iffI)
apply (rule, simp add: Int_choice_mem, fast)+
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Int_choice_commut:
  "LET:fp df IN P |~| Q =F LET:fp df IN Q |~| P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Int_choice_commut)

(*********************************************************
                      Parallel
 *********************************************************)

lemma domSF_Parallel_commut:
  "[[P |[X]| Q]]SF ev = [[Q |[X]| P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)
apply (rule eq_iffI)

apply (rule, simp add: Parallel_mem)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (rule_tac x="s" in exI)
apply (simp add: par_tr_sym)

apply (rule, simp add: Parallel_mem)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (rule_tac x="s" in exI)
apply (simp add: par_tr_sym)

apply (rule eq_iffI)

apply (rule, simp add: Parallel_mem)
apply (elim conjE exE)
apply (rule_tac x="Z" in exI)
apply (rule_tac x="Y" in exI, simp)
apply (rule conjI, fast)
apply (rule_tac x="t" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: par_tr_sym)

apply (rule, simp add: Parallel_mem)
apply (elim conjE exE)
apply (rule_tac x="Z" in exI)
apply (rule_tac x="Y" in exI, simp)
apply (rule conjI, fast)
apply (rule_tac x="t" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: par_tr_sym)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Parallel_commut:
  "LET:fp df IN P |[X]| Q =F LET:fp df IN Q |[X]| P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Parallel_commut)

(*------------------*
 |      csp law     |
 *------------------*)

lemmas csp_commut = csp_Ext_choice_commut csp_Int_choice_commut csp_Parallel_commut

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

declare not_None_eq    [simp]

end