Theory CSP_F_law_dist

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_dist = CSP_F_law_basic + CSP_F_law_decompo
                      + CSP_T_law_dist:

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

      distribution over internal choice

         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]]
         7. (P1 |~| P2) ;; Q
         8. (P1 |~| P2) |. n
         9. !! x:X .. (P1 |~| P2)

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

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

lemma cspF_Ext_choice_dist_l: 
  "(P1 |~| P2) [+] Q =F
   (P1 [+] Q) |~| (P2 [+] Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_dist_l)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, fast)+
done

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

lemma cspF_Ext_choice_dist_r: 
  "P [+] (Q1 |~| Q2) =F
   (P [+] Q1) |~| (P [+] Q2)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_dist_l)
apply (rule cspF_decompo)
apply (rule cspF_commut)+
done

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

lemma cspF_Parallel_dist_l: 
  "(P1 |~| P2) |[X]| Q =F
   (P1 |[X]| Q) |~| (P2 |[X]| Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_dist_l)
apply (rule order_antisym)

  apply (rule, simp add: in_failures)
  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: in_failures)
  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

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

lemma cspF_Parallel_dist_r: 
  "P |[X]| (Q1 |~| Q2) =F
   (P |[X]| Q1) |~| (P |[X]| Q2)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_dist_l)
apply (rule cspF_decompo)
apply (rule cspF_commut)+
done

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

lemma cspF_Hiding_dist: 
  "(P1 |~| P2) -- X =F
   (P1 -- X) |~| (P2 -- X)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_dist)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

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

lemma cspF_Renaming_dist: 
  "(P1 |~| P2) [[r]] =F
   (P1 [[r]]) |~| (P2 [[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_dist)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

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

lemma cspF_Seq_compo_dist: 
  "(P1 |~| P2) ;; Q =F
   (P1 ;; Q) |~| (P2 ;; Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_dist)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, fast)+
done

(*********************************************************
               dist law for Depth_rest
 *********************************************************)

lemma cspF_Depth_rest_dist: 
  "(P1 |~| P2) |. n =F
   (P1 |. n) |~| (P2 |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_dist)
apply (rule order_antisym)
apply (rule, simp add: in_failures)
apply (rule, simp add: in_failures)
apply (fast)
done

(*********************************************************
               dist law for Rep_int_choice
 *********************************************************)

lemma cspF_Rep_int_choice_dist:
  "!! c:C .. (Pf c |~| Qf c) =F (!! c:C .. Pf c) |~| (!! c:C .. Qf c)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_dist)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

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

lemmas cspF_dist = cspF_Ext_choice_dist_l cspF_Ext_choice_dist_r
                   cspF_Parallel_dist_l   cspF_Parallel_dist_r
                   cspF_Hiding_dist       cspF_Renaming_dist
                   cspF_Seq_compo_dist    cspF_Depth_rest_dist
                   cspF_Rep_int_choice_dist

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

      distribution of internal bind over ...

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

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

(*********************************************************
                Dist law for Ext_choice (l)
 *********************************************************)

lemma cspF_Ext_choice_Dist0_l_nonempty: 
  "C ~= {} ==> (!! :C .. Pf) [+] Q =F
               !! c:C .. (Pf c [+] Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_Dist0_l_nonempty)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, fast)+
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist0_l: 
  "(!! :C .. Pf) [+] Q =F
   IF (C={}) THEN (DIV [+] Q) ELSE (!! c:C .. (Pf c [+] Q))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_decompo)
apply (simp add: cspF_Rep_int_choice_empty)
apply (simp)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Ext_choice_Dist0_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist0 law for Ext_choice (r)
 *********************************************************)

lemma cspF_Ext_choice_Dist0_r_nonempty: 
  "C ~= {} ==> P [+] (!! :C .. Qf) =F
               !! c:C .. (P [+] Qf c)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_Dist0_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist0_r: 
  "P [+] (!! :C .. Qf) =F
   IF (C={}) THEN (P [+] DIV) ELSE (!! c:C .. (P [+] Qf c))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_decompo)
apply (simp)
apply (simp add: cspF_Rep_int_choice_empty)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Ext_choice_Dist0_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist0 law for Parallel (l)
 *********************************************************)

lemma cspF_Parallel_Dist0_l_nonempty: 
  "C ~= {} ==>
     (!! :C .. Pf) |[X]| Q =F
     !! c:C .. (Pf c |[X]| Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_Dist0_l_nonempty)
apply (rule order_antisym)

(* domF *)
  apply (rule)
  apply (simp add: in_failures)
  apply (elim conjE exE bexE)
   apply (rule_tac x="c" in bexI)
   apply (rule_tac x="Y" in exI)
   apply (rule_tac x="Z" in exI)
   apply (fast)
   apply (simp)
  (* *)
  apply (rule)
  apply (simp add: in_failures)
  apply (elim conjE exE bexE)
   apply (rule_tac x="Y" in exI)
   apply (rule_tac x="Z" in exI)
   apply (fast)
done

(*** Dist ***)

lemma cspF_Parallel_Dist0_l: 
  "(!! :C .. Pf) |[X]| Q =F
   IF (C={}) THEN (DIV |[X]| Q) ELSE (!! c:C .. (Pf c |[X]| Q))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_decompo)
apply (simp)
apply (simp add: cspF_Rep_int_choice_empty)
apply (simp)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Parallel_Dist0_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist0 law for Parallel (r)
 *********************************************************)

lemma cspF_Parallel_Dist0_r_nonempty: 
  "C ~= {} ==>
     P |[X]| (!! :C .. Qf) =F
     !! c:C .. (P |[X]| Qf c)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Dist0_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Parallel_Dist0_r: 
  "P |[X]| (!! :C .. Qf) =F
   IF (C={}) THEN (P |[X]| DIV) ELSE (!! c:C .. (P |[X]| Qf c))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (simp add: cspF_Rep_int_choice_empty)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Parallel_Dist0_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist0 law for Hiding
 *********************************************************)

lemma cspF_Hiding_Dist0: 
  "(!! :C .. Pf) -- X =F
   !! c:C .. (Pf c -- X)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_Dist0)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
                Dist0 law for Renaming
 *********************************************************)

lemma cspF_Renaming_Dist0: 
  "(!! :C .. Pf) [[r]] =F
   !! c:C .. (Pf c [[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_Dist0)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
          Dist0 law for Sequential composition
 *********************************************************)

lemma cspF_Seq_compo_Dist0: 
  "(!! :C .. Pf) ;; Q =F
   !! c:C .. (Pf c ;; Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_Dist0)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures)
apply (force)
apply (rule, simp add: in_traces in_failures)
apply (force)
done

(*********************************************************
                Dist0 law for Depth_rest
 *********************************************************)

lemma cspF_Depth_rest_Dist0: 
  "(!! :C .. Pf) |. n =F
   !! c:C .. (Pf c |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_Dist0)
apply (rule order_antisym)
apply (rule, simp add: in_failures)
apply (rule, simp add: in_failures)
done

(*********************************************************
                     Dist0 laws
 *********************************************************)

lemmas cspF_Dist0 = cspF_Ext_choice_Dist0_l cspF_Ext_choice_Dist0_r
                        cspF_Parallel_Dist0_l   cspF_Parallel_Dist0_r
                        cspF_Hiding_Dist0       cspF_Renaming_Dist0
                        cspF_Seq_compo_Dist0    cspF_Depth_rest_Dist0

lemmas cspF_Dist0_nonempty = 
       cspF_Ext_choice_Dist0_l_nonempty cspF_Ext_choice_Dist0_r_nonempty
       cspF_Parallel_Dist0_l_nonempty   cspF_Parallel_Dist0_r_nonempty
       cspF_Hiding_Dist0       cspF_Renaming_Dist0
       cspF_Seq_compo_Dist0    cspF_Depth_rest_Dist0

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

      for convenience

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

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

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

lemma cspF_Ext_choice_Dist_fun_l_nonempty: 
  "[| inj f ; X ~= {} |]
   ==> (!!<f> :X .. Pf) [+] Q =F !!<f> x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0_nonempty)

lemma cspF_Ext_choice_Dist_fun_r_nonempty: 
  "[| inj f ; X ~= {} |]
   ==> P [+] (!!<f> :X .. Qf) =F !!<f> x:X .. (P [+] Qf x)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0_nonempty)

lemma cspF_Parallel_Dist_fun_l_nonempty: 
  "[| inj f ; Y ~= {} |]
   ==> (!!<f> :Y .. Pf) |[X]| Q =F !!<f> x:Y .. (Pf x |[X]| Q)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0_nonempty)

lemma cspF_Parallel_Dist_fun_r_nonempty: 
  "[| inj f ; Y ~= {} |]
   ==> P |[X]| (!!<f> :Y .. Qf) =F !!<f> x:Y .. (P |[X]| Qf x)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0_nonempty)

lemma cspF_Ext_choice_Dist_fun_l: 
  "(!!<f> :X .. Pf) [+] Q =F
   IF (X ={}) THEN (DIV [+] Q) ELSE (!!<f> x:X .. (Pf x [+] Q))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist0)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Ext_choice_Dist_fun_r: 
  "P [+] (!!<f> :X .. Qf) =F
   IF (X ={}) THEN (P [+] DIV) ELSE (!!<f> x:X .. (P [+] Qf x))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist0)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_fun_l: 
  "(!!<f> :Y .. Pf) |[X]| Q =F
   IF (Y ={}) THEN (DIV |[X]| Q) ELSE (!!<f> x:Y .. (Pf x |[X]| Q))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist0)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_fun_r: 
  "P |[X]| (!!<f> :Y .. Qf) =F
   IF (Y ={}) THEN (P |[X]| DIV) ELSE (!!<f> x:Y .. (P |[X]| Qf x))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist0)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Hiding_Dist_fun: 
  "inj f ==> (!!<f> :Y .. Pf) -- X =F !!<f> x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0)

lemma cspF_Renaming_Dist_fun: 
  "inj f ==> (!!<f> :X .. Pf) [[r]] =F !!<f> x:X .. (Pf x [[r]])"
by (simp add: Rep_int_choice_fun_def cspF_Dist0)

lemma cspF_Seq_compo_Dist_fun:
  "inj f ==> (!!<f> :X .. Pf) ;; Q =F !!<f> x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0)

lemma cspF_Depth_rest_Dist_fun: 
  "inj f ==> (!!<f> :X .. Pf) |. n =F !!<f> x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_fun_def cspF_Dist0)

(*********************************************************
                     Dist laws
 *********************************************************)

lemmas cspF_Dist_fun = cspF_Ext_choice_Dist_fun_l cspF_Ext_choice_Dist_fun_r
                           cspF_Parallel_Dist_fun_l   cspF_Parallel_Dist_fun_r
                           cspF_Hiding_Dist_fun       cspF_Renaming_Dist_fun
                           cspF_Seq_compo_Dist_fun    cspF_Depth_rest_Dist_fun

lemmas cspF_Dist_fun_nonempty = 
       cspF_Ext_choice_Dist_fun_l_nonempty cspF_Ext_choice_Dist_fun_r_nonempty
       cspF_Parallel_Dist_fun_l_nonempty   cspF_Parallel_Dist_fun_r_nonempty
       cspF_Hiding_Dist_fun       cspF_Renaming_Dist_fun
       cspF_Seq_compo_Dist_fun    cspF_Depth_rest_Dist_fun

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

      for convenience

         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]]
         7. (! :X .. Pf) |. n

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

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

lemma cspF_Ext_choice_Dist_com_l_nonempty: 
  "X ~= {}
   ==> (! :X .. Pf) [+] Q =F ! x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Ext_choice_Dist_com_r_nonempty: 
  "X ~= {}
   ==> P [+] (! :X .. Qf) =F ! x:X .. (P [+] Qf x)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Parallel_Dist_com_l_nonempty: 
  "Y ~= {}
   ==> (! :Y .. Pf) |[X]| Q =F ! x:Y .. (Pf x |[X]| Q)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Parallel_Dist_com_r_nonempty: 
  "Y ~= {}
   ==> P |[X]| (! :Y .. Qf) =F ! x:Y .. (P |[X]| Qf x)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Ext_choice_Dist_com_l: 
  "(! :X .. Pf) [+] Q =F 
   IF (X ={}) THEN (DIV [+] Q) ELSE (! x:X .. (Pf x [+] Q))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist_fun)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Ext_choice_Dist_com_r: 
  "P [+] (! :X .. Qf) =F
   IF (X ={}) THEN (P [+] DIV) ELSE (! x:X .. (P [+] Qf x))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist_fun)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_com_l: 
  "(! :Y .. Pf) |[X]| Q =F
   IF (Y ={}) THEN (DIV |[X]| Q) ELSE (! x:Y .. (Pf x |[X]| Q))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist_fun)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_com_r: 
  "P |[X]| (! :Y .. Qf) =F 
   IF (Y ={}) THEN (P |[X]| DIV) ELSE (! x:Y .. (P |[X]| Qf x))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Dist_fun)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Hiding_Dist_com: 
  "(! :Y .. Pf) -- X =F ! x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Renaming_Dist_com: 
  "(! :X .. Pf) [[r]] =F ! x:X .. (Pf x [[r]])"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Seq_compo_Dist_com:
  "(! :X .. Pf) ;; Q =F ! x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

lemma cspF_Depth_rest_Dist_com: 
  "(! :X .. Pf) |. n =F ! x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_com_def cspF_Dist_fun_nonempty)

(*********************************************************
                     Dist laws
 *********************************************************)

lemmas cspF_Dist_com = cspF_Ext_choice_Dist_com_l cspF_Ext_choice_Dist_com_r
                           cspF_Parallel_Dist_com_l   cspF_Parallel_Dist_com_r
                           cspF_Hiding_Dist_com       cspF_Renaming_Dist_com
                           cspF_Seq_compo_Dist_com    cspF_Depth_rest_Dist_com

lemmas cspF_Dist_com_nonempty = 
       cspF_Ext_choice_Dist_com_l_nonempty cspF_Ext_choice_Dist_com_r_nonempty
       cspF_Parallel_Dist_com_l_nonempty   cspF_Parallel_Dist_com_r_nonempty
       cspF_Hiding_Dist_com       cspF_Renaming_Dist_com
       cspF_Seq_compo_Dist_com    cspF_Depth_rest_Dist_com

(*** all rules ***)

lemmas cspF_Dist = cspF_Dist0 cspF_Dist_fun cspF_Dist_com

lemmas cspF_Dist_nonempty = cspF_Dist0_nonempty
                            cspF_Dist_fun_nonempty
                            cspF_Dist_com_nonempty

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

      additional distribution of internal bind over ...

         1. (!! :X .. (a -> P))
         2. (!! :Y .. (? :X -> P))

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

(*********************************************************
              Dist law for Act_prefix
 *********************************************************)

lemma cspF_Act_prefix_Dist0:
  "C ~= {} ==> 
   a -> (!! :C .. Pf) =F !! c:C .. (a -> Pf c)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Act_prefix_Dist0)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (erule disjE)
  apply (force)

  apply (elim conjE exE bexE)
  apply (rule_tac x="c" in bexI)
  apply (force)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE bexE exE)
  apply (simp)
  apply (simp)
  apply (rule_tac x="c" in bexI)
  apply (simp)
  apply (simp)
done

(*********************************************************
              Dist0 law for Ext_pre_choice
 *********************************************************)

lemma cspF_Ext_pre_choice_Dist0:
  "C ~= {} ==> 
   ? x:X -> (!! c:C .. (Pf c) x) =F !! c:C .. (? :X -> (Pf c))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_pre_choice_Dist0)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (erule disjE)
  apply (force)

  apply (elim conjE exE bexE)
  apply (rule_tac x="c" in bexI)
  apply (force)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE bexE)
  apply (simp)
  apply (simp)
  apply (rule_tac x="c" in bexI)
  apply (simp)
  apply (simp)
done

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

      for convenience

         1. (!!<f> :X .. (a -> P))
         2. (!!<f> :Y .. (? :X -> P))

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

lemma cspF_Act_prefix_Dist_fun:
  "X ~= {} ==> 
   a -> (!!<f> :X .. Pf) =F !!<f> x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_fun_def cspF_Act_prefix_Dist0)

lemma cspF_Ext_pre_choice_Dist_fun:
  "Y ~= {} ==> 
   ? x:X -> (!!<f> y:Y .. (Pf y) x) =F !!<f> y:Y .. (? :X -> (Pf y))"
by (simp add: Rep_int_choice_fun_def cspF_Ext_pre_choice_Dist0)

lemma cspF_Act_prefix_Dist_com:
  "X ~= {} ==> 
   a -> (! :X .. Pf) =F ! x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_com_def cspF_Act_prefix_Dist_fun)

lemma cspF_Ext_pre_choice_Dist_com:
  "Y ~= {} ==> 
   ? x:X -> (! y:Y .. (Pf y) x) =F ! y:Y .. (? :X -> (Pf y))"
by (simp add: Rep_int_choice_com_def cspF_Ext_pre_choice_Dist_fun)

(*** arias ***)

lemmas cspF_Act_prefix_Dist 
     = cspF_Act_prefix_Dist0
       cspF_Act_prefix_Dist_fun
       cspF_Act_prefix_Dist_com

lemmas cspF_Ext_pre_choice_Dist
     = cspF_Ext_pre_choice_Dist0
       cspF_Ext_pre_choice_Dist_fun
       cspF_Ext_pre_choice_Dist_com

(*****************************************************************
      distribution of external choice over ...
         1. (P1 [+] P2) [[r]]
         2. (P1 [+] P2) |. n
 *****************************************************************)

(*********************
     [[r]]-[+]-dist
 *********************)

lemma cspF_Renaming_Ext_dist: 
  "(P1 [+] P2) [[r]] =F
   (P1 [[r]]) [+] (P2 [[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_Ext_dist)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (force)

(* <= *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (force)
done


(*********************
     |.-[+]-dist
 *********************)

lemma cspF_Depth_rest_Ext_dist: 
  "(P1 [+] P2) |. n =F
   (P1 |. n) [+] (P2 |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_Ext_dist)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (force)

(* <= *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (force)
done

lemmas cspF_Ext_dist = cspF_Renaming_Ext_dist cspF_Depth_rest_Ext_dist

(*---------------------------------------------------------*
 |                   complex distribution                  |
 *---------------------------------------------------------*)

(*********************
     !!-input-!set
 *********************)

lemma cspF_Rep_int_choice_input_set:
  "(!! c:C .. (? :(Yf c) -> Rff c))
   =F
   (!set Y : {Yf c|c. c:C} .. (? a : Y -> (!! c:{c:C. a : Yf c} .. Rff c a)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_input_set)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_failures)
 apply (elim disjE conjE exE bexE)
 apply (simp_all)
 apply (force)
 apply (force)

(* <= *)
 apply (rule, simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
apply (rule_tac x="c" in bexI)
apply (simp)
apply (simp)
apply (rule_tac x="ca" in bexI)
apply (simp)
apply (simp)
done

(*-------------------------------*
          !!-[+]-Dist
 *-------------------------------*)

lemma cspF_Rep_int_choice_Ext_Dist:
  "ALL c:C. (Qf c = SKIP | Qf c = DIV) ==>
   (!! c:C .. (Pf c [+] Qf c)) =F
   ((!! :C .. Pf) [+] (!! :C .. Qf))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_Ext_Dist)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (elim conjE exE bexE disjE)

  apply (drule_tac x="c" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="c" in bexI)
  apply (simp add: in_traces)
  apply (simp)

  apply (simp add: in_failures)
  apply (force)

  apply (drule_tac x="c" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule_tac x="c" in bexI)
  apply (simp add: in_failures)
  apply (simp)

  apply (simp add: in_failures)
  apply (force)

  apply (drule_tac x="c" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="c" in bexI)
  apply (simp add: in_traces)
  apply (simp)

  apply (simp add: in_traces)

(* => *)
 apply (rule)
 apply (simp add: in_failures in_traces)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)

  apply (case_tac "EX c:C. Qf c = SKIP")
  apply (erule bexE)
  apply (rule_tac x="cb" in bexI)
  apply (simp add: in_failures in_traces)
   apply (case_tac "Qf ca = SKIP")
   apply (simp add: in_failures)
   apply (case_tac "Qf ca = DIV")
   apply (simp add: in_failures)
   apply (fast)
  apply (simp)

  apply (simp add: in_failures in_traces)

  apply (force)
  apply (force)
  apply (force)
  apply (force)
done

(*-------------------------------*
          !!-input-Dist
 *-------------------------------*)

(* SKIP *)

lemma cspF_Rep_int_choice_input_Dist_SKIP:
  "(!set X:Xs .. (? :X -> Pf)) [+] SKIP =F (? :(Union Xs) -> Pf) [+] SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_input_Dist)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE exE disjE bexE)
 apply (simp_all)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE exE disjE bexE)
 apply (simp_all)
 apply (force)
done

(* DIV *)

lemma cspF_Rep_int_choice_input_Dist_DIV:
  "(!set X:Xs .. (? :X -> Pf)) [+] DIV =F (? :(Union Xs) -> Pf) [+] DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_input_Dist)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE exE disjE bexE)
 apply (simp_all)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE exE disjE bexE)
 apply (simp_all)
 apply (force)
done

(* SKIP or DIV *)

lemma cspF_Rep_int_choice_input_Dist:
  "Q = SKIP | Q = DIV ==>
   (!set X:Xs .. (? :X -> Pf)) [+] Q =F (? :(Union Xs) -> Pf) [+] Q"
apply (erule disjE)
apply (simp add: cspF_Rep_int_choice_input_Dist_SKIP)
apply (simp add: cspF_Rep_int_choice_input_Dist_DIV)
done

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

end