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)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_dist
imports CSP_F_law_basic CSP_F_law_decompo CSP_T_law_dist
begin

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

      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[M,M]
   (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[M,M]
   (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[M,M]
   (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[M,M]
   (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[M,M]
   (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[M,M]
   (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[M,M]
   (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[M,M]
   (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_nat_dist:
  "!nat n:N .. (Pf n |~| Qf n) =F[M,M] (!nat n:N .. Pf n) |~| (!nat n:N .. Qf n)"
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

lemma cspF_Rep_int_choice_set_dist:
  "!set X:Xs .. (Pf X |~| Qf X) =F[M,M] (!set X:Xs .. Pf X) |~| (!set X:Xs .. Qf X)"
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

lemma cspF_Rep_int_choice_com_dist:
  "! a:X .. (Pf a |~| Qf a) =F[M,M] (! a:X .. Pf a) |~| (! a:X .. Qf a)"
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

lemma cspF_Rep_int_choice_f_dist:
  "inj f ==>
   !<f> a:X .. (Pf a |~| Qf a) =F[M,M] (!<f> a:X .. Pf a) |~| (!<f> a:X .. Qf a)"
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

lemmas cspF_Rep_int_choice_dist =
       cspF_Rep_int_choice_nat_dist
       cspF_Rep_int_choice_set_dist
       cspF_Rep_int_choice_com_dist
       cspF_Rep_int_choice_f_dist

(*********************************************************
                     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. (!nat :N .. Pf) [+] Q
         2. Q [+] (!nat :N .. Pf)
         3. (!nat :N .. Pf) |[X]| Q
         4. Q |[X]| (!nat :N .. Pf)
         5. (!nat :N .. Pf) -- X
         6. (!nat :N .. Pf) [[r]]
         7. (!nat :N .. Pf) |. n

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

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

lemma cspF_Ext_choice_Dist_nat_l_nonempty: 
  "N ~= {} ==> (!nat :N .. Pf) [+] Q =F[M,M]
               !nat n:N .. (Pf n [+] Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Dist_nonempty)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, fast)+
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist_nat_l: 
  "(!nat :N .. Pf) [+] Q =F[M,M]
   IF (N={}) THEN (DIV [+] Q) ELSE (!nat n:N .. (Pf n [+] Q))"
apply (case_tac "N={}")
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_Dist_nat_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist_nat law for Ext_choice (r)
 *********************************************************)

lemma cspF_Ext_choice_Dist_nat_r_nonempty: 
  "N ~= {} ==> P [+] (!nat :N .. Qf) =F[M,M]
               !nat n:N .. (P [+] Qf n)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_Dist_nat_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist_nat_r: 
  "P [+] (!nat :N .. Qf) =F[M,M]
   IF (N={}) THEN (P [+] DIV) ELSE (!nat n:N .. (P [+] Qf n))"
apply (case_tac "N={}")
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_Dist_nat_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist_nat law for Parallel (l)
 *********************************************************)

lemma cspF_Parallel_Dist_nat_l_nonempty: 
  "N ~= {} ==>
     (!nat :N .. Pf) |[X]| Q =F[M,M]
     !nat n:N .. (Pf n |[X]| Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_Dist_nat_l_nonempty)
apply (rule order_antisym)

(* domF *)
  apply (rule)
  apply (simp add: in_failures)
  apply (elim conjE exE bexE)
   apply (rule_tac x="n" 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_Dist_nat_l: 
  "(!nat :N .. Pf) |[X]| Q =F[M,M]
   IF (N={}) THEN (DIV |[X]| Q) ELSE (!nat n:N .. (Pf n |[X]| Q))"
apply (case_tac "N={}")
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_Dist_nat_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist_nat law for Parallel (r)
 *********************************************************)

lemma cspF_Parallel_Dist_nat_r_nonempty: 
  "N ~= {} ==>
     P |[X]| (!nat :N .. Qf) =F[M,M]
     !nat n:N .. (P |[X]| Qf n)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Dist_nat_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Parallel_Dist_nat_r: 
  "P |[X]| (!nat :N .. Qf) =F[M,M]
   IF (N={}) THEN (P |[X]| DIV) ELSE (!nat n:N .. (P |[X]| Qf n))"
apply (case_tac "N={}")
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_Dist_nat_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist_nat law for Hiding
 *********************************************************)

lemma cspF_Hiding_Dist_nat: 
  "(!nat :N .. Pf) -- X =F[M,M]
   !nat n:N .. (Pf n -- X)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_Dist_nat)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
                Dist_nat law for Renaming
 *********************************************************)

lemma cspF_Renaming_Dist_nat: 
  "(!nat :N .. Pf) [[r]] =F[M,M]
   !nat n:N .. (Pf n [[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_Dist_nat)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
          Dist_nat law for Sequential composition
 *********************************************************)

lemma cspF_Seq_compo_Dist_nat: 
  "(!nat :N .. Pf) ;; Q =F[M,M]
   !nat n:N .. (Pf n ;; Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_Dist_nat)
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

(*********************************************************
                Dist_nat law for Depth_rest
 *********************************************************)

lemma cspF_Depth_rest_Dist_nat: 
  "(!nat :N .. Pf) |. m =F[M,M]
   !nat n:N .. (Pf n |. m)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_Dist_nat)
apply (rule order_antisym)
apply (rule, simp add: in_failures)
apply (rule, simp add: in_failures)
done

(*********************************************************
                     Dist_nat laws
 *********************************************************)

lemmas cspF_Dist_nat = cspF_Ext_choice_Dist_nat_l cspF_Ext_choice_Dist_nat_r
                        cspF_Parallel_Dist_nat_l   cspF_Parallel_Dist_nat_r
                        cspF_Hiding_Dist_nat       cspF_Renaming_Dist_nat
                        cspF_Seq_compo_Dist_nat    cspF_Depth_rest_Dist_nat

lemmas cspF_Dist_nat_nonempty = 
       cspF_Ext_choice_Dist_nat_l_nonempty cspF_Ext_choice_Dist_nat_r_nonempty
       cspF_Parallel_Dist_nat_l_nonempty   cspF_Parallel_Dist_nat_r_nonempty
       cspF_Hiding_Dist_nat       cspF_Renaming_Dist_nat
       cspF_Seq_compo_Dist_nat    cspF_Depth_rest_Dist_nat

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

      distribution of internal bind over ...

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

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

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

lemma cspF_Ext_choice_Dist_set_l_nonempty: 
  "Xs ~= {} ==> (!set :Xs .. Pf) [+] Q =F[M,M]
               !set X:Xs .. (Pf X [+] Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Dist_nonempty)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, fast)+
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist_set_l: 
  "(!set :Xs .. Pf) [+] Q =F[M,M]
   IF (Xs={}) THEN (DIV [+] Q) ELSE (!set X:Xs .. (Pf X [+] Q))"
apply (case_tac "Xs={}")
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_Dist_set_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist_set law for Ext_choice (r)
 *********************************************************)

lemma cspF_Ext_choice_Dist_set_r_nonempty: 
  "Xs ~= {} ==> P [+] (!set :Xs .. Qf) =F[M,M]
               !set X:Xs .. (P [+] Qf X)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_Dist_set_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Ext_choice_Dist_set_r: 
  "P [+] (!set :Xs .. Qf) =F[M,M]
   IF (Xs={}) THEN (P [+] DIV) ELSE (!set X:Xs .. (P [+] Qf X))"
apply (case_tac "Xs={}")
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_Dist_set_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist_set law for Parallel (l)
 *********************************************************)

lemma cspF_Parallel_Dist_set_l_nonempty: 
  "Xs ~= {} ==>
     (!set :Xs .. Pf) |[Y]| Q =F[M,M]
     !set X:Xs .. (Pf X |[Y]| Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_Dist_set_l_nonempty)
apply (rule order_antisym)

(* domF *)
  apply (rule)
  apply (simp add: in_failures)
  apply (elim conjE exE bexE)
   apply (rule_tac x="Xa" in bexI)
   apply (rule_tac x="Ya" 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="Ya" in exI)
   apply (rule_tac x="Z" in exI)
   apply (fast)
done

(*** Dist ***)

lemma cspF_Parallel_Dist_set_l: 
  "(!set :Xs .. Pf) |[Y]| Q =F[M,M]
   IF (Xs={}) THEN (DIV |[Y]| Q) ELSE (!set X:Xs .. (Pf X |[Y]| Q))"
apply (case_tac "Xs={}")
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_Dist_set_l_nonempty)
apply (simp)
done

(*********************************************************
                Dist_set law for Parallel (r)
 *********************************************************)

lemma cspF_Parallel_Dist_set_r_nonempty: 
  "Xs ~= {} ==>
     P |[Y]| (!set :Xs .. Qf) =F[M,M]
     !set X:Xs .. (P |[Y]| Qf X)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Dist_set_l_nonempty, simp)
apply (rule cspF_decompo, simp)
apply (rule cspF_commut)
done

(*** Dist ***)

lemma cspF_Parallel_Dist_set_r: 
  "P |[Y]| (!set :Xs .. Qf) =F[M,M]
   IF (Xs={}) THEN (P |[Y]| DIV) ELSE (!set X:Xs .. (P |[Y]| Qf X))"
apply (case_tac "Xs={}")
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_Dist_set_r_nonempty)
apply (simp)
done

(*********************************************************
                Dist_set law for Hiding
 *********************************************************)

lemma cspF_Hiding_Dist_set: 
  "(!set :Xs .. Pf) -- Y =F[M,M]
   !set X:Xs .. (Pf X -- Y)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_Dist_set)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
                Dist_set law for Renaming
 *********************************************************)

lemma cspF_Renaming_Dist_set: 
  "(!set :Xs .. Pf) [[r]] =F[M,M]
   !set X:Xs .. (Pf X [[r]])"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_Dist_set)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

(*********************************************************
          Dist_set law for Sequential composition
 *********************************************************)

lemma cspF_Seq_compo_Dist_set: 
  "(!set :Xs .. Pf) ;; Q =F[M,M]
   !set X:Xs .. (Pf X ;; Q)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_Dist_set)
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

(*********************************************************
                Dist_set law for Depth_rest
 *********************************************************)

lemma cspF_Depth_rest_Dist_set: 
  "(!set :Xs .. Pf) |. m =F[M,M]
   !set X:Xs .. (Pf X |. m)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_Dist_set)
apply (rule order_antisym)
apply (rule, simp add: in_failures)
apply (rule, simp add: in_failures)
done

(*********************************************************
                     Dist_set laws
 *********************************************************)

lemmas cspF_Dist_set = cspF_Ext_choice_Dist_set_l cspF_Ext_choice_Dist_set_r
                        cspF_Parallel_Dist_set_l   cspF_Parallel_Dist_set_r
                        cspF_Hiding_Dist_set       cspF_Renaming_Dist_set
                        cspF_Seq_compo_Dist_set    cspF_Depth_rest_Dist_set

lemmas cspF_Dist_set_nonempty = 
       cspF_Ext_choice_Dist_set_l_nonempty cspF_Ext_choice_Dist_set_r_nonempty
       cspF_Parallel_Dist_set_l_nonempty   cspF_Parallel_Dist_set_r_nonempty
       cspF_Hiding_Dist_set       cspF_Renaming_Dist_set
       cspF_Seq_compo_Dist_set    cspF_Depth_rest_Dist_set

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

      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[M,M] ! x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_com_def cspF_Dist_set_nonempty)

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

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

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

lemma cspF_Ext_choice_Dist_com_l: 
  "(! :X .. Pf) [+] Q =F[M,M] 
   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_set)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Ext_choice_Dist_com_r: 
  "P [+] (! :X .. Qf) =F[M,M]
   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_set)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_com_l: 
  "(! :Y .. Pf) |[X]| Q =F[M,M]
   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_set)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Parallel_Dist_com_r: 
  "P |[X]| (! :Y .. Qf) =F[M,M] 
   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_set)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Hiding_Dist_com: 
  "(! :Y .. Pf) -- X =F[M,M] ! x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_com_def cspF_Dist_set_nonempty)

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

lemma cspF_Seq_compo_Dist_com:
  "(! :X .. Pf) ;; Q =F[M,M] ! x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_com_def cspF_Dist_set_nonempty)

lemma cspF_Depth_rest_Dist_com: 
  "(! :X .. Pf) |. n =F[M,M] ! x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_com_def cspF_Dist_set_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


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

      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_f_l_nonempty: 
  "[| inj f ; X ~= {} |]
   ==> (!<f> :X .. Pf) [+] Q =F[M,M] !<f> x:X .. (Pf x [+] Q)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com_nonempty)

lemma cspF_Ext_choice_Dist_f_r_nonempty: 
  "[| inj f ; X ~= {} |]
   ==> P [+] (!<f> :X .. Qf) =F[M,M] !<f> x:X .. (P [+] Qf x)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com_nonempty)

lemma cspF_Parallel_Dist_f_l_nonempty: 
  "[| inj f ; Y ~= {} |]
   ==> (!<f> :Y .. Pf) |[X]| Q =F[M,M] !<f> x:Y .. (Pf x |[X]| Q)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com_nonempty)

lemma cspF_Parallel_Dist_f_r_nonempty: 
  "[| inj f ; Y ~= {} |]
   ==> P |[X]| (!<f> :Y .. Qf) =F[M,M] !<f> x:Y .. (P |[X]| Qf x)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com_nonempty)

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

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

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

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

lemma cspF_Hiding_Dist_f: 
  "(!<f> :Y .. Pf) -- X =F[M,M] !<f> x:Y .. (Pf x -- X)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com)

lemma cspF_Renaming_Dist_f: 
  "(!<f> :X .. Pf) [[r]] =F[M,M] !<f> x:X .. (Pf x [[r]])"
by (simp add: Rep_int_choice_f_def cspF_Dist_com)

lemma cspF_Seq_compo_Dist_f:
  "(!<f> :X .. Pf) ;; Q =F[M,M] !<f> x:X .. (Pf x ;; Q)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com)

lemma cspF_Depth_rest_Dist_f: 
  "(!<f> :X .. Pf) |. n =F[M,M] !<f> x:X .. (Pf x |. n)"
by (simp add: Rep_int_choice_f_def cspF_Dist_com)

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

lemmas cspF_Dist_f = cspF_Ext_choice_Dist_f_l cspF_Ext_choice_Dist_f_r
                           cspF_Parallel_Dist_f_l   cspF_Parallel_Dist_f_r
                           cspF_Hiding_Dist_f       cspF_Renaming_Dist_f
                           cspF_Seq_compo_Dist_f    cspF_Depth_rest_Dist_f

lemmas cspF_Dist_f_nonempty = 
       cspF_Ext_choice_Dist_f_l_nonempty cspF_Ext_choice_Dist_f_r_nonempty
       cspF_Parallel_Dist_f_l_nonempty   cspF_Parallel_Dist_f_r_nonempty
       cspF_Hiding_Dist_f       cspF_Renaming_Dist_f
       cspF_Seq_compo_Dist_f    cspF_Depth_rest_Dist_f

(*** all rules ***)

lemmas cspF_Dist = cspF_Dist_nat cspF_Dist_set cspF_Dist_com cspF_Dist_f

lemmas cspF_Dist_nonempty = cspF_Dist_nat_nonempty
                            cspF_Dist_set_nonempty
                            cspF_Dist_com_nonempty
                            cspF_Dist_f_nonempty

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

      additional distribution of internal bind over ...

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

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

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

lemma cspF_Act_prefix_Dist_nat:
  "N ~= {} ==> 
   a -> (!nat :N .. Pf) =F[M,M] !nat n:N .. (a -> Pf n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Act_prefix_Dist_nat)
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="n" 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="n" in bexI)
  apply (simp)
  apply (simp)
done

(*********************************************************
              Dist_nat law for Ext_pre_choice
 *********************************************************)

lemma cspF_Ext_pre_choice_Dist_nat:
  "N ~= {} ==> 
   ? x:X -> (!nat n:N .. (Pf n) x) =F[M,M] !nat n:N .. (? :X -> (Pf n))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_pre_choice_Dist_nat)
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="n" 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="n" in bexI)
  apply (simp)
  apply (simp)
done

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

      additional distribution of internal bind over ...

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

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

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

lemma cspF_Act_prefix_Dist_set:
  "Xs ~= {} ==> 
   a -> (!set :Xs .. Pf) =F[M,M] !set X:Xs .. (a -> Pf X)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Act_prefix_Dist_set)
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="Xa" 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="Xa" in bexI)
  apply (simp)
  apply (simp)
done

(*********************************************************
              Dist_nat law for Ext_pre_choice
 *********************************************************)

lemma cspF_Ext_pre_choice_Dist_set:
  "Ys ~= {} ==> 
   ? x:X -> (!set Y:Ys .. (Pf Y) x) =F[M,M] !set Y:Ys .. (? :X -> (Pf Y))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_pre_choice_Dist_set)
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="Xaa" 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="Xaa" in bexI)
  apply (simp)
  apply (simp)
done

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

      for convenience

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

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

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

lemma cspF_Act_prefix_Dist_com:
  "X ~= {} ==> 
   a -> (! :X .. Pf) =F[M,M] ! x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_com_def cspF_Act_prefix_Dist_set)

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

lemma cspF_Act_prefix_Dist_f:
  "X ~= {} ==> 
   a -> (!<f> :X .. Pf) =F[M,M] !<f> x:X .. (a -> Pf x)"
by (simp add: Rep_int_choice_f_def cspF_Act_prefix_Dist_com)

lemma cspF_Ext_pre_choice_Dist_f:
  "Y ~= {} ==> 
   ? x:X -> (!<f> y:Y .. (Pf y) x) =F[M,M] !<f> y:Y .. (? :X -> (Pf y))"
by (simp add: Rep_int_choice_f_def cspF_Ext_pre_choice_Dist_com)

(*** arias ***)

lemmas cspF_Act_prefix_Dist 
     = cspF_Act_prefix_Dist_nat
       cspF_Act_prefix_Dist_set
       cspF_Act_prefix_Dist_com
       cspF_Act_prefix_Dist_f

lemmas cspF_Ext_pre_choice_Dist
     = cspF_Ext_pre_choice_Dist_nat
       cspF_Ext_pre_choice_Dist_set
       cspF_Ext_pre_choice_Dist_com
       cspF_Ext_pre_choice_Dist_f

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

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

lemma cspF_Renaming_Ext_dist: 
  "(P1 [+] P2) [[r]] =F[M,M]
   (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[M,M]
   (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_nat_input_set:
  "(!nat n:N .. (? :(Yf n) -> Rff n))
   =F[M,M]
   (!set Y : {Yf n|n. n:N} .. (? a : Y -> (!nat n:{n:N. a : Yf n} .. Rff n 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="n" in bexI)
apply (simp)
apply (simp)
apply (rule_tac x="na" in bexI)
apply (simp)
apply (simp)
done

lemma cspF_Rep_int_choice_set_input_set:
  "(!set X:Xs .. (? :(Yf X) -> Rff X))
   =F[M,M]
   (!set Y : {Yf X|X. X:Xs} .. (? a : Y -> (!set X:{X:Xs. a : Yf X} .. Rff X 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="Xb" in bexI)
apply (simp)
apply (simp)
apply (rule_tac x="Xc" in bexI)
apply (simp)
apply (simp)
done

lemmas cspF_Rep_int_choice_input_set =
       cspF_Rep_int_choice_nat_input_set
       cspF_Rep_int_choice_set_input_set

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

lemma cspF_Rep_int_choice_Ext_Dist_nat:
  "ALL n:N. (Qf n = SKIP | Qf n = DIV) ==>
   (!nat n:N .. (Pf n [+] Qf n)) =F[M,M]
   ((!nat :N .. Pf) [+] (!nat :N .. 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="n" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="n" in bexI)
  apply (simp add: in_traces)
  apply (simp)

  apply (simp add: in_failures)
  apply (force)

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

  apply (simp add: in_failures)
  apply (force)

  apply (drule_tac x="n" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="n" 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 n:N. Qf n = SKIP")
  apply (erule bexE)
  apply (rule_tac x="nb" in bexI)
  apply (simp add: in_failures in_traces)
   apply (case_tac "Qf na = SKIP")
   apply (simp add: in_failures)
   apply (case_tac "Qf na = 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

lemma cspF_Rep_int_choice_Ext_Dist_set:
  "ALL X:Xs. (Qf X = SKIP | Qf X = DIV) ==>
   (!set X:Xs .. (Pf X [+] Qf X)) =F[M,M]
   ((!set :Xs .. Pf) [+] (!set :Xs .. Qf))"
(* by the same proof *)
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="Xa" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="Xa" in bexI)
  apply (simp add: in_traces)
  apply (simp)

  apply (simp add: in_failures)
  apply (force)

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

  apply (simp add: in_failures)
  apply (force)

  apply (drule_tac x="Xa" in bspec, simp)
  apply (erule disjE)
  apply (simp add: in_failures)
  apply (rule disjI2)
  apply (rule disjI2)
  apply (rule_tac x="Xa" 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 X:Xs. Qf X = SKIP")
  apply (erule bexE)
  apply (rule_tac x="Xc" in bexI)
  apply (simp add: in_failures in_traces)
   apply (case_tac "Qf Xb = SKIP")
   apply (simp add: in_failures)
   apply (case_tac "Qf Xb = 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

lemma cspF_Rep_int_choice_Ext_Dist_com:
  "ALL a:X. (Qf a = SKIP | Qf a = DIV) ==>
   (! a:X .. (Pf a [+] Qf a)) =F[M,M]
   ((! :X .. Pf) [+] (! :X .. Qf))"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_Ext_Dist_set)
by (auto)

lemma cspF_Rep_int_choice_Ext_Dist_f:
  "[| inj f ; ALL a:X. (Qf a = SKIP | Qf a = DIV) |] ==>
   (!<f> a:X .. (Pf a [+] Qf a)) =F[M,M]
   ((!<f> :X .. Pf) [+] (!<f> :X .. Qf))"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice_Ext_Dist_com)
by (auto)

lemmas cspF_Rep_int_choice_Ext_Dist =
       cspF_Rep_int_choice_Ext_Dist_nat
       cspF_Rep_int_choice_Ext_Dist_set
       cspF_Rep_int_choice_Ext_Dist_com
       cspF_Rep_int_choice_Ext_Dist_f

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

(* SKIP *)

lemma cspF_Rep_int_choice_input_Dist_SKIP:
  "(!set X:Xs .. (? :X -> Pf)) [+] SKIP =F[M,M] (? :(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[M,M] (? :(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[M,M] (? :(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

(*-------------------------------*
          !!-Ext-choice-SKIP
 *-------------------------------*)

(*** nat ***)

lemma cspF_Rep_int_choice_nat_Ext_choice:
  "Q = SKIP | Q = DIV ==>
  (!nat n:N .. (? :(Xf n) -> Pf n)) [+] Q
    =F[M,M] (? x:Union {Xf n|n. n:N} -> (!nat n:{n:N. x: Xf n}  .. Pf n x)) [+] Q"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Rep_int_choice_input_set)
apply (rule cspF_reflex)

apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_input_Dist)
apply (simp)
apply (simp)
done

(*** set ***)

lemma cspF_Rep_int_choice_set_Ext_choice:
  "Q = SKIP | Q = DIV ==>
  (!set X:Xs .. (? :(Xf X) -> Pf X)) [+] Q
    =F[M,M] (? x:Union {Xf X|X. X:Xs} -> (!set X:{X:Xs. x: Xf X}  .. Pf X x)) [+] Q"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Rep_int_choice_input_set)
apply (rule cspF_reflex)

apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_input_Dist)
apply (simp)
apply (simp)
done

lemmas cspF_Rep_int_choice_Ext_choice =
       cspF_Rep_int_choice_nat_Ext_choice
       cspF_Rep_int_choice_set_Ext_choice

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

end