Theory CSP_T_law_dist

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

theory CSP_T_law_dist = CSP_T_law_basic:

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

      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 cspT_Ext_choice_dist_l: 
  "(P1 |~| P2) [+] Q =T
   (P1 [+] Q) |~| (P2 [+] Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemma cspT_Ext_choice_dist_r: 
  "P [+] (Q1 |~| Q2) =T
   (P [+] Q1) |~| (P [+] Q2)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_Ext_choice_dist_l)
apply (rule cspT_decompo)
apply (rule cspT_commut)+
done

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

lemma cspT_Parallel_dist_l: 
  "(P1 |~| P2) |[X]| Q =T
   (P1 |[X]| Q) |~| (P2 |[X]| Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemma cspT_Parallel_dist_r: 
  "P |[X]| (Q1 |~| Q2) =T
   (P |[X]| Q1) |~| (P |[X]| Q2)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_Parallel_dist_l)
apply (rule cspT_decompo)
apply (rule cspT_commut)+
done

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

lemma cspT_Hiding_dist: 
  "(P1 |~| P2) -- X =T
   (P1 -- X) |~| (P2 -- X)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemma cspT_Renaming_dist: 
  "(P1 |~| P2) [[r]] =T
   (P1 [[r]]) |~| (P2 [[r]])"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemma cspT_Seq_compo_dist: 
  "(P1 |~| P2) ;; Q =T
   (P1 ;; Q) |~| (P2 ;; Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemma cspT_Depth_rest_dist: 
  "(P1 |~| P2) |. n =T
   (P1 |. n) |~| (P2 |. n)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)
apply (rule, simp add: in_traces)
apply (force)
done

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

lemma cspT_Rep_int_choice_dist:
  "!! c:C .. (Pf c |~| Qf c) =T (!! c:C .. Pf c) |~| (!! c:C .. Qf c)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

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

lemmas cspT_dist = cspT_Ext_choice_dist_l cspT_Ext_choice_dist_r
                   cspT_Parallel_dist_l   cspT_Parallel_dist_r
                   cspT_Hiding_dist       cspT_Renaming_dist
                   cspT_Seq_compo_dist    cspT_Depth_rest_dist
                   cspT_Rep_int_choice_dist

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

      distribution over replicated internal choice

         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

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

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

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

(*** Dist ***)

lemma cspT_Ext_choice_Dist0_l: 
  "(!! :C .. Pf) [+] Q =T
   IF (C={}) THEN (DIV [+] Q) ELSE (!! c:C .. (Pf c [+] Q))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_decompo)
apply (simp add: cspT_Rep_int_choice_empty)
apply (simp)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_Ext_choice_Dist0_l_nonempty)
apply (simp)
done

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

lemma cspT_Ext_choice_Dist0_r_nonempty: 
  "C ~= {} ==> P [+] (!! :C .. Qf) =T
               !! c:C .. (P [+] Qf c)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_Ext_choice_Dist0_l_nonempty, simp)
apply (rule cspT_decompo, simp)
apply (rule cspT_commut)
done

(*** Dist ***)

lemma cspT_Ext_choice_Dist0_r: 
  "P [+] (!! :C .. Qf) =T
   IF (C={}) THEN (P [+] DIV) ELSE (!! c:C .. (P [+] Qf c))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_decompo)
apply (simp)
apply (simp add: cspT_Rep_int_choice_empty)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_Ext_choice_Dist0_r_nonempty)
apply (simp)
done

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

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

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
  apply (subgoal_tac "EX c. c:C")
  apply (elim exE)
  apply (rule disjI2)
  apply (rule_tac x="c" in bexI)
  apply (simp)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="ta" in exI)
  apply (simp)
  apply (simp)
  apply (fast)
  (* *)
  apply (rule disjI2)
  apply (rule_tac x="c" in bexI)
  apply (fast)
  apply (simp)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)
  apply (fast)
done

(*** Dist ***)

lemma cspT_Parallel_Dist0_l: 
  "(!! :C .. Pf) |[X]| Q =T
   IF (C={}) THEN (DIV |[X]| Q) ELSE (!! c:C .. (Pf c |[X]| Q))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_decompo)
apply (simp)
apply (simp add: cspT_Rep_int_choice_empty)
apply (simp)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_Parallel_Dist0_l_nonempty)
apply (simp)
done

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

lemma cspT_Parallel_Dist0_r_nonempty: 
  "C ~= {} ==>
     P |[X]| (!! :C .. Qf) =T
     !! c:C .. (P |[X]| Qf c)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_Parallel_Dist0_l_nonempty, simp)
apply (rule cspT_decompo, simp)
apply (rule cspT_commut)
done

(*** Dist ***)

lemma cspT_Parallel_Dist0_r: 
  "P |[X]| (!! :C .. Qf) =T
   IF (C={}) THEN (P |[X]| DIV) ELSE (!! c:C .. (P |[X]| Qf c))"
apply (case_tac "C={}")
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_decompo)
apply (simp)
apply (simp)
apply (simp add: cspT_Rep_int_choice_empty)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (rule cspT_Parallel_Dist0_r_nonempty)
apply (simp)
done

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

lemma cspT_Hiding_Dist0: 
  "(!! :C .. Pf) -- X =T
   !! c:C .. (Pf c -- X)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE, simp, fast)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (rule_tac x="<>" in exI, simp)
 apply (rule_tac x="s" in exI, fast)
done

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

lemma cspT_Renaming_Dist0: 
  "(!! :C .. Pf) [[r]] =T
   !! c:C .. (Pf c [[r]])"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE, simp, fast)
 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE, simp, fast)
done

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

lemma cspT_Seq_compo_Dist0: 
  "(!! :C .. Pf) ;; Q =T
   !! c:C .. (Pf c ;; Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (simp)
 apply (fast)
 apply (force)
 apply (rule disjI2)
 apply (rule_tac x="c" in bexI)
 apply (force)
 apply (simp)

 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (rule disjI1)
 apply (rule_tac x="<>" in exI, simp)
 apply (fast)
 apply (fast)
done

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

lemma cspT_Depth_rest_Dist0: 
  "(!! :C .. Pf) |. n =T
   !! c:C .. (Pf c |. n)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

 apply (rule, simp add: in_traces)
 apply (rule, simp add: in_traces)
 apply (force)
done

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

lemmas cspT_Dist0 = cspT_Ext_choice_Dist0_l cspT_Ext_choice_Dist0_r
                        cspT_Parallel_Dist0_l   cspT_Parallel_Dist0_r
                        cspT_Hiding_Dist0       cspT_Renaming_Dist0
                        cspT_Seq_compo_Dist0    cspT_Depth_rest_Dist0

lemmas cspT_Dist0_nonempty = 
       cspT_Ext_choice_Dist0_l_nonempty cspT_Ext_choice_Dist0_r_nonempty
       cspT_Parallel_Dist0_l_nonempty   cspT_Parallel_Dist0_r_nonempty
       cspT_Hiding_Dist0       cspT_Renaming_Dist0
       cspT_Seq_compo_Dist0    cspT_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 cspT_Ext_choice_Dist_fun_l_nonempty: 
  "[| inj f ; X ~= {} |]
   ==> (!!<f> :X .. Pf) [+] Q =T !!<f> x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_fun_def cspT_Dist0_nonempty)

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

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

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

lemma cspT_Ext_choice_Dist_fun_l: 
  "(!!<f> :X .. Pf) [+] Q =T 
   IF (X ={}) THEN (DIV [+] Q) ELSE (!!<f> x:X .. (Pf x [+] Q))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist0)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Ext_choice_Dist_fun_r: 
  "P [+] (!!<f> :X .. Qf) =T
   IF (X ={}) THEN (P [+] DIV) ELSE (!!<f> x:X .. (P [+] Qf x))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist0)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Parallel_Dist_fun_l: 
  "(!!<f> :Y .. Pf) |[X]| Q =T
   IF (Y ={}) THEN (DIV |[X]| Q) ELSE (!!<f> x:Y .. (Pf x |[X]| Q))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist0)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Parallel_Dist_fun_r: 
  "P |[X]| (!!<f> :Y .. Qf) =T 
   IF (Y ={}) THEN (P |[X]| DIV) ELSE (!!<f> x:Y .. (P |[X]| Qf x))"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist0)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Hiding_Dist_fun: 
  "(!!<f> :Y .. Pf) -- X =T !!<f> x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_fun_def cspT_Dist0)

lemma cspT_Renaming_Dist_fun: 
  "(!!<f> :X .. Pf) [[r]] =T !!<f> x:X .. (Pf x [[r]])"
by (simp add: Rep_int_choice_fun_def cspT_Dist0)

lemma cspT_Seq_compo_Dist_fun:
  "(!!<f> :X .. Pf) ;; Q =T !!<f> x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_fun_def cspT_Dist0)

lemma cspT_Depth_rest_Dist_fun: 
  "(!!<f> :X .. Pf) |. n =T !!<f> x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_fun_def cspT_Dist0)

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

lemmas cspT_Dist_fun = cspT_Ext_choice_Dist_fun_l cspT_Ext_choice_Dist_fun_r
                           cspT_Parallel_Dist_fun_l   cspT_Parallel_Dist_fun_r
                           cspT_Hiding_Dist_fun       cspT_Renaming_Dist_fun
                           cspT_Seq_compo_Dist_fun    cspT_Depth_rest_Dist_fun

lemmas cspT_Dist_fun_nonempty = 
       cspT_Ext_choice_Dist_fun_l_nonempty cspT_Ext_choice_Dist_fun_r_nonempty
       cspT_Parallel_Dist_fun_l_nonempty   cspT_Parallel_Dist_fun_r_nonempty
       cspT_Hiding_Dist_fun       cspT_Renaming_Dist_fun
       cspT_Seq_compo_Dist_fun    cspT_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 cspT_Ext_choice_Dist_com_l_nonempty: 
  "X ~= {}
   ==> (! :X .. Pf) [+] Q =T ! x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

lemma cspT_Ext_choice_Dist_com_r_nonempty: 
  "X ~= {}
   ==> P [+] (! :X .. Qf) =T ! x:X .. (P [+] Qf x)"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

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

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

lemma cspT_Ext_choice_Dist_com_l: 
  "(! :X .. Pf) [+] Q =T 
   IF (X ={}) THEN (DIV [+] Q) ELSE (! x:X .. (Pf x [+] Q))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist_fun)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Ext_choice_Dist_com_r: 
  "P [+] (! :X .. Qf) =T
   IF (X ={}) THEN (P [+] DIV) ELSE (! x:X .. (P [+] Qf x))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist_fun)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Parallel_Dist_com_l: 
  "(! :Y .. Pf) |[X]| Q =T
   IF (Y ={}) THEN (DIV |[X]| Q) ELSE (! x:Y .. (Pf x |[X]| Q))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist_fun)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Parallel_Dist_com_r: 
  "P |[X]| (! :Y .. Qf) =T 
   IF (Y ={}) THEN (P |[X]| DIV) ELSE (! x:Y .. (P |[X]| Qf x))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspT_rw_left)
apply (rule cspT_Dist_fun)
apply (rule cspT_decompo)
apply (auto)
done

lemma cspT_Hiding_Dist_com: 
  "(! :Y .. Pf) -- X =T ! x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

lemma cspT_Renaming_Dist_com: 
  "(! :X .. Pf) [[r]] =T ! x:X .. (Pf x [[r]])"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

lemma cspT_Seq_compo_Dist_com:
  "(! :X .. Pf) ;; Q =T ! x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

lemma cspT_Depth_rest_Dist_com: 
  "(! :X .. Pf) |. n =T ! x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_com_def cspT_Dist_fun_nonempty)

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

lemmas cspT_Dist_com = cspT_Ext_choice_Dist_com_l cspT_Ext_choice_Dist_com_r
                           cspT_Parallel_Dist_com_l   cspT_Parallel_Dist_com_r
                           cspT_Hiding_Dist_com       cspT_Renaming_Dist_com
                           cspT_Seq_compo_Dist_com    cspT_Depth_rest_Dist_com

lemmas cspT_Dist_com_nonempty = 
       cspT_Ext_choice_Dist_com_l_nonempty cspT_Ext_choice_Dist_com_r_nonempty
       cspT_Parallel_Dist_com_l_nonempty   cspT_Parallel_Dist_com_r_nonempty
       cspT_Hiding_Dist_com       cspT_Renaming_Dist_com
       cspT_Seq_compo_Dist_com    cspT_Depth_rest_Dist_com

(*** all rules ***)

lemmas cspT_Dist = cspT_Dist0 cspT_Dist_fun cspT_Dist_com

lemmas cspT_Dist_nonempty = cspT_Dist0_nonempty
                            cspT_Dist_fun_nonempty
                            cspT_Dist_com_nonempty

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

      additional distribution over replicated internal choice

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

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

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

lemma cspT_Act_prefix_Dist0:
  "C ~= {} ==> 
   a -> (!! :C .. Pf) =T !! c:C .. (a -> Pf c)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (simp_all)
 apply (force)
 apply (force)

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

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

lemma cspT_Ext_pre_choice_Dist0:
  "C ~= {} ==> 
   ? x:X -> (!! c:C .. (Pf c) x) =T !! c:C .. (? :X -> (Pf c))"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (simp_all)
 apply (force)
 apply (force)

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

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

      for convenience

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

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

lemma cspT_Act_prefix_Dist_fun:
  "X ~= {} ==> 
   a -> (!!<f> :X .. Pf) =T !!<f> x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_fun_def cspT_Act_prefix_Dist0)

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

lemma cspT_Act_prefix_Dist_com:
  "X ~= {} ==> 
   a -> (! :X .. Pf) =T ! x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_com_def cspT_Act_prefix_Dist_fun)

lemma cspT_Ext_pre_choice_Dist_com:
  "Y ~= {} ==> 
   ? x:X -> (! y:Y .. (Pf y) x) =T ! y:Y .. (? :X -> (Pf y))"
by (simp add: Rep_int_choice_com_def cspT_Ext_pre_choice_Dist_fun)

(*** arias ***)

lemmas cspT_Act_prefix_Dist 
     = cspT_Act_prefix_Dist0
       cspT_Act_prefix_Dist_fun
       cspT_Act_prefix_Dist_com

lemmas cspT_Ext_pre_choice_Dist
     = cspT_Ext_pre_choice_Dist0
       cspT_Ext_pre_choice_Dist_fun
       cspT_Ext_pre_choice_Dist_com

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

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

lemma cspT_Renaming_Ext_dist:
  "(P1 [+] P2) [[r]] =T
   (P1 [[r]]) [+] (P2 [[r]])"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

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

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

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

lemmas cspT_Ext_dist = cspT_Renaming_Ext_dist cspT_Depth_rest_Ext_dist

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

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

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

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

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

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

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

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
 apply (force)
 apply (drule_tac x="c" in bspec)
 apply (simp)
 apply (erule disjE)
 apply (simp_all add: in_traces)
 apply (erule disjE)
 apply (simp_all)
 apply (rule disjI2)
 apply (rule_tac x="c" in bexI)
 apply (simp_all add: in_traces)

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

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

lemma cspT_Rep_int_choice_input:
  "!set X:Xs .. (? :X -> Pf) =T (? :(Union Xs) -> Pf)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

lemma cspT_Rep_int_choice_input_Dist:
  "(!set X:Xs .. (? :X -> Pf)) [+] Q =T (? :(Union Xs) -> Pf) [+] Q"
apply (rule cspT_decompo)
apply (rule cspT_Rep_int_choice_input)
apply (rule cspT_reflex)
done

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

end