Theory CSP_law_dist

Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover

theory CSP_law_dist = CSP_law_commut + CSP_law_decompo: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_dist = CSP_law_commut + CSP_law_decompo:

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

declare not_None_eq [simp del]

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

      distribution of internal choice over ...

         1. (P1 |~| P2) [+] Q
         2. Q [+] (P1 |~| P2)
         3. (P1 |~| P2) |[X]| Q
         4. Q |[X]| (P1 |~| P2)
         5. (P1 |~| P2) -- X
         6. (P1 |~| P2) [[r]]

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

(*********************************************************
                dist law for Ext_choice (l)
 *********************************************************)

lemma domSF_Ext_choice_dist_l: 
  "[[(P1 |~| P2) [+] Q]]SF ev = [[(P1 [+] Q) |~| (P2 [+] Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Ext_choice_mem Int_choice_mem, fast)+

(* domF *)
 apply (rule eq_iffI)
 apply (rule, simp add: Ext_choice_mem Int_choice_mem
                        memF_IntF memF_UnF memT_UnT, fast)+
done

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

lemma csp_Ext_choice_dist_l: 
  "LET:fp df IN (P1 |~| P2) [+] Q =F
   LET:fp df IN (P1 [+] Q) |~| (P2 [+] Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Ext_choice_dist_l)

(*********************************************************
                dist law for Ext_choice (r)
 *********************************************************)

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

lemma csp_Ext_choice_dist_r: 
  "LET:fp df IN P [+] (Q1 |~| Q2) =F
   LET:fp df IN (P [+] Q1) |~| (P [+] Q2)"
apply (rule csp_rw_left)
apply (rule csp_commut)
apply (rule csp_rw_left)
apply (rule csp_Ext_choice_dist_l)
apply (rule csp_decompo)
apply (rule csp_commut)+
done

(*********************************************************
                dist law for Parallel (l)
 *********************************************************)

lemma domSF_Parallel_dist_l: 
  "[[(P1 |~| P2) |[X]| Q]]SF ev = [[(P1 |[X]| Q) |~| (P2 |[X]| Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Parallel_mem Int_choice_mem, fast)+

(* domF *)
 apply (rule eq_iffI)
  apply (rule, simp add: Parallel_mem Int_choice_mem)
  apply (elim disjE conjE exE)
  apply (rule disjI1)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z" in exI)
  apply (fast)
  apply (rule disjI2)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z" in exI)
  apply (fast)

  apply (rule, simp add: Parallel_mem Int_choice_mem)
  apply (elim disjE conjE exE)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z" in exI)
  apply (fast)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z" in exI)
  apply (fast)
done

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

lemma csp_Parallel_dist_l: 
  "LET:fp df IN (P1 |~| P2) |[X]| Q =F
   LET:fp df IN (P1 |[X]| Q) |~| (P2 |[X]| Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Parallel_dist_l)

(*********************************************************
                dist law for Parallel (r)
 *********************************************************)

lemma csp_Parallel_dist_r: 
  "LET:fp df IN P |[X]| (Q1 |~| Q2) =F
   LET:fp df IN (P |[X]| Q1) |~| (P |[X]| Q2)"
apply (rule csp_rw_left)
apply (rule csp_commut)
apply (rule csp_rw_left)
apply (rule csp_Parallel_dist_l)
apply (rule csp_decompo)
apply (rule csp_commut)+
done

(*********************************************************
                dist law for Hiding
 *********************************************************)

lemma domSF_Hiding_dist: 
  "[[(P1 |~| P2) -- X]]SF ev =
   [[(P1 -- X) |~| (P2 -- X)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Hiding_mem Int_choice_mem, fast)+

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

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

lemma csp_Hiding_dist: 
  "LET:fp df IN (P1 |~| P2) -- X =F
   LET:fp df IN (P1 -- X) |~| (P2 -- X)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Hiding_dist)

(*********************************************************
               dist law for Renaming
 *********************************************************)

lemma domSF_Renaming_dist: 
  "[[(P1 |~| P2) [[r]]]]SF ev =
   [[(P1 [[r]]) |~| (P2 [[r]])]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Renaming_mem Int_choice_mem, fast)+

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

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

lemma csp_Renaming_dist: 
  "LET:fp df IN (P1 |~| P2) [[r]] =F
   LET:fp df IN (P1 [[r]]) |~| (P2 [[r]])"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Renaming_dist)

(*********************************************************
         dist law for Sequential composition
 *********************************************************)

lemma domSF_Seq_compo_dist: 
  "[[(P1 |~| P2) ;; Q]]SF ev =
   [[(P1 ;; Q) |~| (P2 ;; Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Seq_compo_mem Int_choice_mem, fast)+

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

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

lemma csp_Seq_compo_dist: 
  "LET:fp df IN (P1 |~| P2) ;; Q =F
   LET:fp df IN (P1 ;; Q) |~| (P2 ;; Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Seq_compo_dist)

(*********************************************************
                     dist laws
 *********************************************************)

lemmas csp_dist = csp_Ext_choice_dist_l csp_Ext_choice_dist_r
                  csp_Parallel_dist_l   csp_Parallel_dist_r
                  csp_Hiding_dist       csp_Renaming_dist
                  csp_Seq_compo_dist

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

      distribution of internal bind over ...

         1. (! :X .. Pf) [+] Q
         2. Q [+] (! :X .. Pf)
         3. (! :X .. Pf) |[X]| Q
         4. Q |[X]| (! :X .. Pf)
         5. (! :X .. Pf) -- X
         6. (! :X .. Pf) [[r]]

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

(*********************************************************
                Rep_dist law for Ext_choice (l)
 *********************************************************)

lemma domSF_Ext_choice_Rep_dist_l: 
  "X ~= {} ==> [[(! :X .. Pf) [+] Q]]SF ev = [[! x:X .. (Pf x [+] Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
 apply (rule, simp add: Ext_choice_mem Rep_int_choice_mem
                        memF_IntF memF_UnF memT_UnT, fast)+

(* domF *)
 apply (rule eq_iffI)
 apply (rule, simp add: Ext_choice_mem Rep_int_choice_mem
                        memF_IntF memF_UnF memT_UnT, fast)+
done

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

lemma csp_Ext_choice_Rep_dist_l: 
  "X ~= {} ==> LET:fp df IN (! :X .. Pf) [+] Q =F
               LET:fp df IN ! x:X .. (Pf x [+] Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Ext_choice_Rep_dist_l)

(*********************************************************
                Rep_dist law for Ext_choice (r)
 *********************************************************)

lemma csp_Ext_choice_Rep_dist_r: 
  "X ~= {} ==> LET:fp df IN P [+] (! :X .. Qf) =F
               LET:fp df IN ! x:X .. (P [+] Qf x)"
apply (rule csp_rw_left)
apply (rule csp_commut)
apply (rule csp_rw_left)
apply (rule csp_Ext_choice_Rep_dist_l, simp)
apply (rule csp_decompo, simp)
apply (rule csp_commut)
done

(*********************************************************
                Rep_dist law for Parallel (l)
 *********************************************************)

lemma domSF_Parallel_Rep_dist_l: 
  "Y ~= {} ==> [[(! :Y .. Pf) |[X]| Q]]SF ev = [[! x:Y .. (Pf x |[X]| Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
  apply (rule, simp add: Parallel_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE)
   apply (subgoal_tac "EX a. a:Y")
   apply (elim exE)
   apply (rule disjI2)
   apply (rule_tac x="a" in exI)
   apply (simp)
   apply (rule_tac x="[]t" in exI)
   apply (rule_tac x="ta" in exI)
   apply (simp)
   apply (fast)
  (* *)
   apply (rule disjI2)
   apply (rule_tac x="a" in exI)
   apply (fast)

  apply (rule, simp add: Parallel_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE)
   apply (rule_tac x="[]t" in exI)
   apply (rule_tac x="[]t" in exI)
   apply (simp)
   apply (fast)

(* domF *)
 apply (rule eq_iffI)
  apply (rule, simp add: Parallel_mem Rep_int_choice_mem)
  apply (elim conjE exE)
   apply (rule_tac x="a" in exI, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Z" in exI)
   apply (fast)
  (* *)
  apply (rule, simp add: Parallel_mem Rep_int_choice_mem)
  apply (elim conjE exE)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Z" in exI)
   apply (fast)
done

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

lemma csp_Parallel_Rep_dist_l: 
  "Y ~= {} ==>
     LET:fp df IN (! :Y .. Pf) |[X]| Q =F
     LET:fp df IN ! x:Y .. (Pf x |[X]| Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Parallel_Rep_dist_l)

(*********************************************************
                Rep_dist law for Parallel (r)
 *********************************************************)

lemma csp_Parallel_Rep_dist_r: 
  "Y ~= {} ==>
     LET:fp df IN P |[X]| (! :Y .. Qf) =F
     LET:fp df IN ! x:Y .. (P |[X]| Qf x)"
apply (rule csp_rw_left)
apply (rule csp_commut)
apply (rule csp_rw_left)
apply (rule csp_Parallel_Rep_dist_l, simp)
apply (rule csp_decompo, simp)
apply (rule csp_commut)
done

(*********************************************************
                Rep_dist law for Hiding
 *********************************************************)

lemma domSF_Hiding_Rep_dist: 
  "[[(! :Y .. Pf) -- X]]SF ev = [[! x:Y .. (Pf x -- X)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
  apply (rule, simp add: Hiding_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE, simp, fast)

  apply (rule, simp add: Hiding_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE)
  apply (rule_tac x="[]t" in exI, simp)
  apply (rule_tac x="s" in exI, fast)

(* domF *)
 apply (rule eq_iffI)
 apply (rule, simp add: Hiding_mem Rep_int_choice_mem, fast)+
done

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

lemma csp_Hiding_Rep_dist: 
  "LET:fp df IN (! :Y .. Pf) -- X =F
   LET:fp df IN ! x:Y .. (Pf x -- X)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Hiding_Rep_dist)

(*********************************************************
                Rep_dist law for Renaming
 *********************************************************)

lemma domSF_Renaming_Rep_dist: 
  "[[(! :X .. Pf) [[r]]]]SF ev = [[! x:X .. (Pf x [[r]])]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
  apply (rule, simp add: Renaming_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE, simp, fast)
  apply (rule, simp add: Renaming_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE, simp, fast)

(* domF *)
 apply (rule eq_iffI)
 apply (rule, simp add: Renaming_mem Rep_int_choice_mem, fast)+
done

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

lemma csp_Renaming_Rep_dist: 
  "LET:fp df IN (! :X .. Pf) [[r]] =F
   LET:fp df IN ! x:X .. (Pf x [[r]])"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Renaming_Rep_dist)

(*********************************************************
          Rep_dist law for Sequential composition
 *********************************************************)

lemma domSF_Seq_compo_Rep_dist: 
  "[[(! :X .. Pf) ;; Q]]SF ev = [[! x:X .. (Pf x ;; Q)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* domT *)
 apply (rule eq_iffI)
  apply (rule, simp add: Seq_compo_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE, simp, fast, fast)
  apply (rule, simp add: Seq_compo_mem Rep_int_choice_mem)
  apply (elim disjE conjE exE)
  apply (rule disjI1)
  apply (rule_tac x="[]t" in exI, simp, fast, fast)

(* domF *)
 apply (rule eq_iffI)
 apply (rule, simp add: Seq_compo_mem Rep_int_choice_mem, fast)+
done

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

lemma csp_Seq_compo_Rep_dist: 
  "LET:fp df IN (! :X .. Pf) ;; Q =F
   LET:fp df IN ! x:X .. (Pf x ;; Q)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Seq_compo_Rep_dist)

(*********************************************************
                     Rep_dist laws
 *********************************************************)

lemmas csp_Rep_dist = csp_Ext_choice_Rep_dist_l csp_Ext_choice_Rep_dist_r
                      csp_Parallel_Rep_dist_l   csp_Parallel_Rep_dist_r
                      csp_Hiding_Rep_dist       csp_Renaming_Rep_dist
                      csp_Seq_compo_Rep_dist

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

declare not_None_eq    [simp]

end

lemma domSF_Ext_choice_dist_l: 

  [[(P1 |~| P2) [+] Q]]SF ev = [[P1 [+] Q |~| P2 [+] Q]]SF ev

lemma csp_Ext_choice_dist_l: 

  
  LET:fp df IN (P1 |~| P2) [+] Q =F 
  LET:fp df IN P1 [+] Q |~| P2 [+] Q

lemma csp_Ext_choice_dist_r: 

  
  LET:fp df IN P [+] (Q1 |~| Q2) =F 
  LET:fp df IN P [+] Q1 |~| P [+] Q2

lemma domSF_Parallel_dist_l: 

  [[(P1 |~| P2) |[X]| Q]]SF ev = [[P1 |[X]| Q |~| P2 |[X]| Q]]SF ev

lemma csp_Parallel_dist_l: 

  
  LET:fp df IN (P1 |~| P2) |[X]| Q =F 
  LET:fp df IN P1 |[X]| Q |~| P2 |[X]| Q

lemma csp_Parallel_dist_r: 

  
  LET:fp df IN P |[X]| (Q1 |~| Q2) =F 
  LET:fp df IN P |[X]| Q1 |~| P |[X]| Q2

lemma domSF_Hiding_dist: 

  [[(P1 |~| P2) -- X]]SF ev = [[P1 -- X |~| P2 -- X]]SF ev

lemma csp_Hiding_dist: 

  
  LET:fp df IN (P1 |~| P2) -- X =F 
  LET:fp df IN P1 -- X |~| P2 -- X

lemma domSF_Renaming_dist: 

  [[(P1 |~| P2) [[r]]]]SF ev = [[P1 [[r]] |~| P2 [[r]]]]SF ev

lemma csp_Renaming_dist: 

  
  LET:fp df IN (P1 |~| P2) [[r]] =F 
  LET:fp df IN P1 [[r]] |~| P2 [[r]]

lemma domSF_Seq_compo_dist: 

  [[(P1 |~| P2) ;; Q]]SF ev = [[P1 ;; Q |~| P2 ;; Q]]SF ev

lemma csp_Seq_compo_dist: 

  
  LET:fp df IN (P1 |~| P2) ;; Q =F 
  LET:fp df IN P1 ;; Q |~| P2 ;; Q

lemmas csp_dist: 

  
  LET:fp df IN (P1 |~| P2) [+] Q =F 
  LET:fp df IN P1 [+] Q |~| P2 [+] Q
  
  LET:fp df IN P [+] (Q1 |~| Q2) =F 
  LET:fp df IN P [+] Q1 |~| P [+] Q2
  
  LET:fp df IN (P1 |~| P2) |[X]| Q =F 
  LET:fp df IN P1 |[X]| Q |~| P2 |[X]| Q
  
  LET:fp df IN P |[X]| (Q1 |~| Q2) =F 
  LET:fp df IN P |[X]| Q1 |~| P |[X]| Q2
  
  LET:fp df IN (P1 |~| P2) -- X =F 
  LET:fp df IN P1 -- X |~| P2 -- X
  
  LET:fp df IN (P1 |~| P2) [[r]] =F 
  LET:fp df IN P1 [[r]] |~| P2 [[r]]
  
  LET:fp df IN (P1 |~| P2) ;; Q =F 
  LET:fp df IN P1 ;; Q |~| P2 ;; Q

lemma domSF_Ext_choice_Rep_dist_l: 

  X ≠ {} ==> [[(! :X .. Pf) [+] Q]]SF ev = [[! x:X .. Pf x [+] Q]]SF ev

lemma csp_Ext_choice_Rep_dist_l: 

  X ≠ {}
  ==> 
      LET:fp df IN (! :X .. Pf) [+] Q =F 
      LET:fp df IN ! x:X .. Pf x [+] Q

lemma csp_Ext_choice_Rep_dist_r: 

  X ≠ {}
  ==> 
      LET:fp df IN P [+] (! :X .. Qf) =F 
      LET:fp df IN ! x:X .. P [+] Qf x

lemma domSF_Parallel_Rep_dist_l: 

  Y ≠ {} ==> [[(! :Y .. Pf) |[X]| Q]]SF ev = [[! x:Y .. Pf x |[X]| Q]]SF ev

lemma csp_Parallel_Rep_dist_l: 

  Y ≠ {}
  ==> 
      LET:fp df IN (! :Y .. Pf) |[X]| Q =F 
      LET:fp df IN ! x:Y .. Pf x |[X]| Q

lemma csp_Parallel_Rep_dist_r: 

  Y ≠ {}
  ==> 
      LET:fp df IN P |[X]| (! :Y .. Qf) =F 
      LET:fp df IN ! x:Y .. P |[X]| Qf x

lemma domSF_Hiding_Rep_dist: 

  [[(! :Y .. Pf) -- X]]SF ev = [[! x:Y .. Pf x -- X]]SF ev

lemma csp_Hiding_Rep_dist: 

  
  LET:fp df IN (! :Y .. Pf) -- X =F 
  LET:fp df IN ! x:Y .. Pf x -- X

lemma domSF_Renaming_Rep_dist: 

  [[(! :X .. Pf) [[r]]]]SF ev = [[! x:X .. Pf x [[r]]]]SF ev

lemma csp_Renaming_Rep_dist: 

  
  LET:fp df IN (! :X .. Pf) [[r]] =F 
  LET:fp df IN ! x:X .. Pf x [[r]]

lemma domSF_Seq_compo_Rep_dist: 

  [[(! :X .. Pf) ;; Q]]SF ev = [[! x:X .. Pf x ;; Q]]SF ev

lemma csp_Seq_compo_Rep_dist: 

  
  LET:fp df IN (! :X .. Pf) ;; Q =F 
  LET:fp df IN ! x:X .. Pf x ;; Q

lemmas csp_Rep_dist: 

  X ≠ {}
  ==> 
      LET:fp df IN (! :X .. Pf) [+] Q =F 
      LET:fp df IN ! x:X .. Pf x [+] Q
  X ≠ {}
  ==> 
      LET:fp df IN P [+] (! :X .. Qf) =F 
      LET:fp df IN ! x:X .. P [+] Qf x
  Y ≠ {}
  ==> 
      LET:fp df IN (! :Y .. Pf) |[X]| Q =F 
      LET:fp df IN ! x:Y .. Pf x |[X]| Q
  Y ≠ {}
  ==> 
      LET:fp df IN P |[X]| (! :Y .. Qf) =F 
      LET:fp df IN ! x:Y .. P |[X]| Qf x
  
  LET:fp df IN (! :Y .. Pf) -- X =F 
  LET:fp df IN ! x:Y .. Pf x -- X
  
  LET:fp df IN (! :X .. Pf) [[r]] =F 
  LET:fp df IN ! x:X .. Pf x [[r]]
  
  LET:fp df IN (! :X .. Pf) ;; Q =F 
  LET:fp df IN ! x:X .. Pf x ;; Q