Theory CSP_F_law_fp

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

theory CSP_F_law_fp = CSP_T_law_fp + CSP_F_law_ufp:

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

         1. cpo fixed point theory in CSP-Prover
         2. 
         3.
         4. 

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

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

(*=======================================================*
 |                                                       |
 |                        CPO                            |
 |                                                       |
 *=======================================================*)

lemma cspF_Tarski_fix:
   "(FIX PF)(p) =F (!nat n .. (((PF^n) (%q. DIV)) p))"
apply (simp add: FIX_def FIXn_def)
done

lemmas cspF_FIX_eq = cspF_Banach_fix cspF_Tarski_fix

(*-----------*
 |    Bot    |
 *-----------*)

lemma failures_prod_Bot: "(%p. failures DIV) = Bot"
apply (simp add: prod_Bot_def)
apply (simp add: expand_fun_eq)
apply (simp add: failures_def)
apply (simp add: bottom_setF_def)
done

lemma traces_failures_prod_Bot: "(%p. (traces DIV ,, failures DIV)) = Bot"
apply (simp add: prod_Bot_def)
apply (simp add: expand_fun_eq)
apply (simp add: bottom_domF_def)
apply (simp add: traces_def failures_def)
done

lemma semF_prod_Bot: "(%p. [[DIV]]F) = Bot"
apply (simp add: semF_def)
apply (simp add: traces_failures_prod_Bot)
done

(*-----------*
 |   FIX P   |
 *-----------*)

lemma semF_FIX_LUB_domF_T:
   "fst ` Rep_domF ` 
   {y. EX x. (EX n. x = ([[P]]FFun ^ n) Bot) & y = x p}
 = {t. EX n. t = (fstF ((([[P]]FFun ^ n) Bot) p))}"
by (auto simp add: fstF_def)

lemma semF_FIX_LUB_domF_F:
   "Union (Rep_setF ` snd ` Rep_domF ` 
           {y. EX x. (EX n. x = ([[P]]FFun ^ n) Bot) & y = x p})
    = {f. EX n. f :f (sndF ((([[P]]FFun ^ n) Bot) p))}"
by (auto simp add: Union_image_eq memF_def sndF_def)

lemma semF_FIX: 
    "PF : ProcFun ==>
     [[(FIX PF) p]]F
     = LUB_domF {y. EX x. (EX n. x = ([[PF]]FFun ^ n) Bot) & y = x p}"
apply (simp add: semF_def)
apply (simp add: pairF_def)
apply (simp add: LUB_domF_def)
apply (subgoal_tac "EX x n. x = ([[P]]FFun ^ n) Bot")
apply (subgoal_tac 
 "{y. EX x. (EX n. x = ([[PF]]FFun ^ n) Bot) & y = x p} ~= {}")
apply (simp add: Abs_domF_inject LUB_TF_in_Rep)
apply (simp add: LUB_TF_def)
apply (simp add: semF_FIX_LUB_domF_T)
apply (simp add: UnionF_def semF_FIX_LUB_domF_F)
apply (rule) 

 (* T *)
 apply (simp add: traces_FIX)
 apply (simp add: semFFun_compo_n[THEN sym])
 apply (simp add: iteration_in_ProcFun pairF_semF)
 apply (simp add: iteration_in_ProcFun tracesFun_compo_n_Tf)

 (* F *)
 apply (simp add: FIX_def FIXn_def)
 apply (rule order_antisym)

  (* <= *)
  apply (rule)
  apply (simp add: in_failures)
  apply (elim conjE exE)
  apply (rule_tac x="a" in exI)
  apply (simp add: semFFun_compo_n[THEN sym])
  apply (simp add: iteration_in_ProcFun failuresFun_f_p)
  apply (simp add: iteration_in_ProcFun pairF_semF)
  apply (simp add: traces_failures_prod_Bot)

  (* => *)
  apply (rule)
  apply (simp add: semFFun_compo_n[THEN sym])
  apply (simp add: in_failures)
  apply (elim conjE exE)
  apply (rule_tac x="n" in exI)
  apply (simp add: iteration_in_ProcFun failuresFun_f_p)
  apply (simp add: iteration_in_ProcFun pairF_semF)
  apply (simp add: traces_failures_prod_Bot)

by (auto)

(*** FIX is LUB ***)

lemma semF_FIX_isLUB:
   "PF : ProcFun ==>
    (%p. [[(FIX PF) p]]F) isLUB {x. EX n. x = ([[PF]]FFun ^ n) Bot}"
apply (simp add: prod_LUB_decompo)
apply (intro allI)
apply (simp add: proj_fun_def)
apply (simp add: image_def)
apply (simp add: semF_FIX)
apply (subgoal_tac 
     "{y. EX x. (EX n. x = ([[PF]]FFun ^ n) Bot) & y = x i} =
      {u. EX n. u = ([[PF]]FFun ^ n) Bot i}")
apply (simp)
apply (rule LUB_domF_isLUB)
apply (auto)
done

lemma semF_FIX_LUB:
   "PF : ProcFun ==>
    (%p. [[(FIX PF) p]]F) = LUB {x. EX n. x = ([[PF]]FFun ^ n) Bot}"
apply (rule sym)
apply (rule isLUB_LUB)
apply (simp add: semF_FIX_isLUB)
done

lemma semF_FIX_LFP:
   "PF : ProcFun ==> (%p. [[(FIX PF) p]]F) = LFP [[PF]]FFun"
apply (simp add: semF_FIX_LUB)
apply (simp add: Tarski_thm_LFP_LUB continuous_semFFun)
done

lemma semF_FIX_LFP_p:
   "PF : ProcFun ==> [[(FIX PF) p]]F = LFP [[PF]]FFun p"
apply (insert semF_FIX_LFP[of PF])
apply (simp add: expand_fun_eq)
done

lemma semF_FIX_isLFP:
   "PF : ProcFun ==> (%p. [[(FIX PF) p]]F) isLFP [[PF]]FFun"
apply (simp add: semF_FIX_LFP)
apply (simp add: LFP_is Tarski_thm_EX continuous_semFFun)
done

lemma semF_FIX_LFP_fixed_point:
   "PF : ProcFun
    ==> [[PF]]FFun (%p. [[(FIX PF) p]]F) = (%p. [[(FIX PF) p]]F)"
apply (insert semF_FIX_isLFP[of PF], simp)
apply (simp add: isLFP_def)
done

lemma semF_FIX_LFP_least:
   "PF : ProcFun ==> 
    ALL SFf. [[PF]]FFun SFf = SFf --> (%p. [[(FIX PF) p]]F) <= SFf"
apply (insert semF_FIX_isLFP[of PF], simp)
apply (simp add: isLFP_def)
done

(*---------------------------------------------------------------------*
 |   FIX is the greatest fixed point of process-expression-functions   |
 |   (semantically least fixed point)                                  |
 *---------------------------------------------------------------------*)

lemma cspF_FIX_isGFP:
  "PF : ProcFun ==> 
   (FIX PF) =F' (PF (FIX PF)) & (ALL f. f =F' PF f --> f <=F' (FIX PF))"
apply (simp add: refF_prod_def eqF_prod_def)
apply (simp add: refF_def eqF_def)
apply (insert semF_FIX_isLFP[of PF], simp)
apply (rule)

 (* FP *)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (simp add: semFFun_f_p)
 apply (simp add: isLFP_def)

 (* LFP *)
 apply (intro allI impI)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (drule sym)
 apply (simp add: expand_fun_eq)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (simp add: semFFun_f_p)
 apply (simp add: isLFP_def)
 apply (erule conjE)
 apply (drule_tac x="(%p. [[f p]]F)" in spec)
 apply (simp add: order_prod_def)
done

(*-------------------------------------------------------*
 |                                                       |
 |           Fixpoint unwind (CSP-Prover rule)           |
 |                                                       |
 *-------------------------------------------------------*)

lemma cspF_unwind_cpo_lm:
  "PF : ProcFun ==> ALL p. (FIX PF) p =F PF (FIX PF) p"
apply (simp add: eqF_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semFFun_f_p)
apply (simp add: semF_FIX_LFP_fixed_point)
done

(*** csp rule ***)

lemma cspF_unwind_cpo:
  "PF : ProcFun ==> (FIX PF) p =F PF (FIX PF) p"
by (simp add: cspF_unwind_cpo_lm)

lemmas cspF_unwind = cspF_unwind_cpo cspF_unwind_cms

(*-------------------------------------------------------*
 |                                                       |
 |        Check fixpoint  (CSP-Prover intro rule)        |
 |                                                       |
 *-------------------------------------------------------*)

lemma cspF_fp_induct_cpo_lm:
   "[| PF : ProcFun ; Q <=F f p ; ALL p. f p <=F (PF f) p |]
    ==> Q <=F (FIX PF) p"
apply (simp add: refF_def)
apply (simp add: fold_order_prod_def)
apply (simp add: semFFun_f_p)
apply (simp add: semF_FIX_LFP_p)
apply (insert cpo_fixpoint_induction_rev
       [of "[[PF]]FFun" "(%p. [[f p]]F)"])
apply (simp add: continuous_semFFun)
apply (simp add: order_prod_def)
apply (rotate_tac -1)
apply (drule_tac x="p" in spec)
apply (auto)
done

(*** csp rule ***)

lemma cspF_fp_induct_cpo:
   "[| PF : ProcFun ; Q <=F f p ; !!p. f p <=F (PF f) p |]
    ==> Q <=F (FIX PF) p"
by (simp add: cspF_fp_induct_cpo_lm)

(*=======================================================*
 |                                                       |
 |                           UFP                         |
 |                                                       |
 *=======================================================*)

lemma semF_FIX_UFP:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]F) = UFP [[PF]]FFun"
apply (subgoal_tac "[[PF]]FFun hasUFP")
apply (insert semF_FIX_isLFP[of PF], simp)
apply (subgoal_tac "UFP [[PF]]FFun isUFP [[PF]]FFun")
apply (simp add: isUFP_def)
apply (simp add: isLFP_def)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (drule_tac x="(%p. [[(FIX PF) p]]F)" in spec)
apply (simp)
apply (simp add: UFP_is)
apply (simp add: contraction_semFFun Banach_thm_EX)
done

lemma semF_FIX_UFP_p:
   "PF : gProcFun ==>
    [[(FIX PF) p]]F = UFP [[PF]]FFun p"
apply (insert semF_FIX_UFP[of PF])
apply (simp add: expand_fun_eq)
done

lemma semF_FIX_isUFP:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]F) isUFP [[PF]]FFun"
apply (simp add: semF_FIX_UFP)
apply (simp add: contraction_semFFun Banach_thm_EX UFP_is)
done

lemma semF_FIX_UFP_unique:
   "PF : gProcFun ==>
    ALL SFf. [[PF]]FFun SFf = SFf --> (%p. [[(FIX PF) p]]F) = SFf"
apply (insert semF_FIX_isUFP[of PF], simp)
apply (simp add: isUFP_def)
done

(*=======================================================*
 |                                                       |
 |                   FIX <==> FIX1                       |
 |                                                       |
 *=======================================================*)

lemma semF_FIX_FIX1:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]F) = (%p. [[(FIX! PF) p]]F)"
apply (simp add: semF_FIX_UFP)
apply (simp add: semF_FIX1_UFP)
done

lemma semF_FIX_FIX1_p:
   "PF : gProcFun ==>
    [[(FIX PF) p]]F = [[(FIX! PF) p]]F"
apply (simp add: semF_FIX_UFP_p)
apply (simp add: semF_FIX1_UFP_p)
done

lemma cspF_FIX_FIX1:
   "PF : gProcFun ==>
    (FIX PF) p =F (FIX! PF) p"
apply (simp add: eqF_def)
apply (simp add: semF_FIX_FIX1_p)
done

(*------------------------------------------------------------------*
 |   FIX is the unique fixed point of process-expression-functions  |
 *------------------------------------------------------------------*)

lemma cspF_FIX_isUFP:
   "PF : gProcFun ==>
   (FIX PF) =F' (PF (FIX PF)) & (ALL f. f =F' PF f --> f =F' (FIX PF))"
apply (simp add: cspF_FIX_isGFP)

apply (simp add: eqF_prod_def)
apply (simp add: eqF_def)
apply (insert semF_FIX_isUFP[of PF], simp)

 (* UFP *)
 apply (intro allI impI)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (drule sym)
 apply (simp add: expand_fun_eq)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (simp add: semFFun_f_p)
 apply (simp add: isUFP_def)
 apply (erule conjE)
 apply (drule_tac x="(%p. [[f p]]F)" in spec)
 apply (simp add: expand_fun_eq)
done

(*-------------------------------------------------------*
 |                                                       |
 |        Check fixpoint  (CSP-Prover intro rule)        |
 |                                                       |
 *-------------------------------------------------------*)

(* refinement *)

lemma cspF_fp_induct_cpo_ref_left_lm:
   "[| PF : gProcFun  ;
       f p <=F Q ; ALL p. (PF f) p <=F f p |]
    ==> (FIX PF) p <=F Q"
apply (rule cspF_rw_left)
apply (rule cspF_FIX_FIX1)
apply (simp_all)
apply (simp add: cspF_fp_induct_cms_ref_left_lm)
done

(*** csp rule ***)

lemma cspF_fp_induct_cpo_ref_left:
   "[| PF : gProcFun  ;
       f p <=F Q ; !! p. (PF f) p <=F f p |]
    ==> (FIX PF) p <=F Q"
by (simp add: cspF_fp_induct_cpo_ref_left_lm)

(* equivalence *)

lemma cspF_fp_induct_cpo_eq_left_lm:
   "[| PF : gProcFun  ;
       f p =F Q ; ALL p. (PF f) p =F f p |]
    ==> (FIX PF) p =F Q"
apply (rule cspF_rw_left)
apply (rule cspF_FIX_FIX1)
apply (simp_all)
apply (simp add: cspF_fp_induct_cms_eq_left_lm)
done

(*** csp rule ***)

lemma cspF_fp_induct_cpo_eq_left:
   "[| PF : gProcFun ;
       f p =F Q ; !! p. (PF f) p =F f p |]
    ==> (FIX PF) p =F Q"
by (simp add: cspF_fp_induct_cpo_eq_left_lm)

lemma cspF_fp_induct_cpo_eq_right:
   "[| PF : gProcFun ; 
       Q =F f p ; !! p. f p =F (PF f) p |]
    ==> Q =F (FIX PF) p"
apply (rule cspF_sym)
apply (rule cspF_fp_induct_cpo_eq_left)
apply (simp)
apply (rule cspF_sym)
apply (simp)
apply (rule cspF_sym)
apply (simp)
done

lemmas cspF_fp_induct_cpo_right = 
       cspF_fp_induct_cpo cspF_fp_induct_cpo_eq_right

lemmas cspF_fp_induct_cpo_left = 
       cspF_fp_induct_cpo_ref_left cspF_fp_induct_cpo_eq_left

(*** cpo and cms ***)

lemmas cspF_fp_induct_right = cspF_fp_induct_cpo_right cspF_fp_induct_cms_right
lemmas cspF_fp_induct_left = cspF_fp_induct_cpo_left cspF_fp_induct_cms_left

(*-------------------------------------------------------*
 |                                                       |
 |         FIX expansion (CSP-Prover intro rule)         |
 |                                                       |
 *-------------------------------------------------------*)

lemma failures_FIXn_plus_sub_lm:
 "PF : ProcFun ==>
  ALL n m p. failures ((FIX[n] PF) p) <= failures ((FIX[n+m] PF) p)"
apply (rule)
apply (induct_tac n)
apply (simp add: FIXn_def)
apply (intro allI)
apply (rule)
apply (simp add: in_failures)

apply (rule allI)
apply (simp add: FIXn_def)
apply (drule_tac x="m" in spec)
apply (simp add: failuresFun_f_p)
apply (fold order_prod_def)
apply (subgoal_tac
  "(%p. (traces   ((PF ^ na) (%q. DIV) p) ,, 
          failures ((PF ^ na) (%q. DIV) p))) <=
   (%p. (traces   ((PF ^ (na + m)) (%q. DIV) p) ,,
          failures ((PF ^ (na + m)) (%q. DIV) p)))")
apply (simp add: mono_failuresFun[simplified mono_def])

apply (simp add: order_prod_def)
apply (intro allI)
apply (simp add: subdomF_decompo)
apply (insert traces_FIXn_plus_sub_lm[of PF])
apply (simp add: FIXn_def)
done

lemma failures_FIXn_plus_sub: 
   "PF : ProcFun ==> failures ((FIX[n] PF) p) <= failures ((FIX[n+m] PF) p)"
by (simp add: failures_FIXn_plus_sub_lm)

lemma semF_FIXn_plus_sub:
 "PF : ProcFun ==> [[(FIX[n] PF) p]]F <= [[(FIX[n+m] PF) p]]F"
apply (simp add: semF_decompo)
apply (simp add: subdomF_decompo)
apply (simp add: traces_FIXn_plus_sub)
apply (simp add: failures_FIXn_plus_sub)
done

lemma in_failures_FIXn_plus_sub: 
  "[| PF : ProcFun ; (s,X) :f failures ((FIX[n] PF) p) |]
   ==> (s,X) :f failures ((FIX[n+m] PF) p)"
apply (insert failures_FIXn_plus_sub[of PF n p m])
by (auto)

(*-----------------------------------------------------*
 |  sometimes FIX[n + f n] is useful more than FIX[n]  |
 *-----------------------------------------------------*)

lemma cspF_FIX_plus_eq: 
     "PF : ProcFun ==>
      ALL f p. (FIX PF) p =F (!nat n .. ((FIX[n + f n] PF) p))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_FIX_plus_eq)

apply (simp add: FIX_def)
apply (intro allI)
apply (rule order_antisym)

 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE)
 apply (rule_tac x="a" in exI)
 apply (simp add: in_failures_FIXn_plus_sub)

 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE)
 apply (rule_tac x="a + f a" in exI)
 apply (simp)
done

lemma cspF_FIX_plus_eq_fun: 
     "PF : ProcFun ==>
      ALL f p. (%p. (FIX PF) p) =F' (%p. (!nat n .. ((FIX[n + f n] PF) p)))"
apply (simp add: eqF_prod_def)
apply (simp add: cspF_FIX_plus_eq)
done

(*=======================================================*
 |                                                       |
 |                Single recursion MU                    |
 |                                                       |
 *=======================================================*)

(*=======================================================*
 |                         cpo                           |
 *=======================================================*)

(*---------------------------------------------------------------------*
 |   MU is the greatest fixed point of process-expression-functions    |
 |   (semantically least fixed point)                                  |
 *---------------------------------------------------------------------*)

lemma cspF_MU_isGFP:
  "PX : ProcX
    ==> MUX PX =F PX (MUX PX) & (ALL P. P =F PX P --> P <=F (MUX PX))"
apply (simp add: MUX_def)
apply (insert cspF_FIX_isGFP[of "(%x n. PX (x MUp))"])
apply (simp add: ProcX_def ProcFun_def)
apply (simp add: eqF_prod_def refF_prod_def)
apply (intro allI impI)
apply (elim conjE)
apply (drule_tac x="(%n. P)" in spec)
apply (simp)
done

(*-------------------------------------------------------*
 |            unwinding (CSP-Prover intro rule)          |
 *-------------------------------------------------------*)

lemma cspF_unwind_MU_cpo:
  "PX : ProcX ==> MUX PX =F PX (MUX PX)"
apply (simp add: cspF_MU_isGFP)
done

lemmas cspF_unwind_MU = cspF_unwind_MU_cms cspF_unwind_MU_cpo

(*-------------------------------------------------------*
 |        Check fixpoint  (CSP-Prover intro rule)        |
 *-------------------------------------------------------*)

lemma cspF_fp_induct_MU_cpo:
   "[| PX : ProcX ; Q <=F PX Q |] ==> Q <=F (MUX PX)"
apply (simp add: MUX_def)
apply (rule cspF_fp_induct_cpo[of _ _ "(%X. Q)"])
apply (simp add: ProcX_def)
apply (simp add: ProcFun_def)
apply (simp)
apply (simp)
done

(*=======================================================*
 |                      unique                           |
 *=======================================================*)

(*-------------------------------------------------------*
 |        Check fixpoint  (CSP-Prover intro rule)        |
 *-------------------------------------------------------*)

lemma cspF_fp_induct_MU_cpo_ref_left:
   "[| PX : gProcX ; PX Q <=F Q |]
    ==> (MUX PX) <=F Q"
apply (simp add: MUX_def)
apply (rule cspF_fp_induct_cpo_ref_left[of _ "(%X. Q)"])
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
apply (simp)
apply (simp)
done

lemma cspF_fp_induct_MU_cpo_eq_left:
   "[| PX : gProcX ; PX Q =F Q |]
    ==> (MUX PX) =F Q"
apply (simp add: MUX_def)
apply (rule cspF_fp_induct_cpo_eq_left[of _ "(%X. Q)"])
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
apply (simp)
apply (simp)
done

lemma cspF_fp_induct_MU_cpo_eq_right:
   "[| PX : gProcX ; Q =F PX Q |]
    ==> Q =F (MUX PX)"
apply (rule cspF_sym)
apply (rule cspF_fp_induct_MU_cpo_eq_left)
apply (simp)
apply (rule cspF_sym)
apply (simp)
done

lemmas cspF_fp_induct_MU_cpo_right
     = cspF_fp_induct_MU_cpo cspF_fp_induct_MU_cpo_eq_right

lemmas cspF_fp_induct_MU_cpo_left
     = cspF_fp_induct_MU_cpo_ref_left cspF_fp_induct_MU_cpo_eq_left


(*** cpo and cms ***)

lemmas cspF_fp_induct_MU_right = cspF_fp_induct_MU_cpo_right
                                 cspF_fp_induct_MU_cms_right

lemmas cspF_fp_induct_MU_left = cspF_fp_induct_MU_cpo_left
                                cspF_fp_induct_MU_cms_left

(*=======================================================*
 |                   MUX <==> MUX1                       |
 *=======================================================*)

lemma cspF_MU_MU1:
   "PX : gProcX ==> (MUX PX) =F (MUX! PX)"
apply (simp add: MUX_def)
apply (simp add: MUX1_def)
apply (rule cspF_FIX_FIX1)
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
done

(*=======================================================*
 |                   expand by Tariski                   |
 *=======================================================*)

lemma cspF_MU_plus_eq_lm: 
     "((%x p. (PX::'a proc => 'a proc) (x MUp)) ^ n) (%q. DIV) MUp = (PX ^ n) DIV"
apply (induct_tac n)
apply (simp_all)
done

lemma cspF_MU_plus_eq: 
     "PX : ProcX ==>
      ALL f. (MUX PX) =F (!nat n .. (PX ^ (n + f n)) DIV)"
apply (insert cspF_FIX_plus_eq[of "(%x p. PX (x MUp))"])
apply (simp add: ProcX_def)
apply (simp add: ProcFun_def)
apply (rule allI)
apply (drule_tac x="f" in spec)
apply (simp add: MUX_def)
apply (drule_tac x="MUp" in spec)
apply (simp add: FIXn_def)
apply (simp add: cspF_MU_plus_eq_lm)
done

lemma cspF_MU_eq_cpo:  
     "PX : ProcX ==>
      (MUX PX) =F (!nat n .. (PX ^ n) DIV)"
apply (insert cspF_MU_plus_eq[of PX])
apply (simp)
apply (drule_tac x="(%n. (0::nat))" in spec)
apply (simp)
done

lemmas cspF_MU_eq = cspF_MU_eq_cms cspF_MU_eq_cpo

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end