Theory CSP_T_law_fp

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

theory CSP_T_law_fp = CSP_T_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 cspT_Tarski_fix:
   "(FIX PF)(p) =T (!nat n .. (((PF^n) (%q. DIV)) p))"
apply (simp add: FIX_def FIXn_def)
done

lemmas cspT_FIX_eq = cspT_Banach_fix cspT_Tarski_fix

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

lemma traces_prod_Bot: "(%p. traces DIV) = Bot"
apply (simp add: prod_Bot_def)
apply (simp add: expand_fun_eq)
apply (simp add: traces_def)
apply (simp add: bottom_domT_def)
done

lemma semT_prod_Bot: "(%p. [[DIV]]T) = Bot"
by (simp add: semT_def traces_prod_Bot)

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

lemma traces_FIX:
    "PF : ProcFun ==>
     traces ((FIX PF) p)
     = UnionT {u. EX n. u = ((tracesFun PF) ^ n) Bot p}"
apply (simp add: FIX_def FIXn_def)
apply (subgoal_tac "{u. EX n. u = ((tracesFun PF) ^ n) Bot p} ~= {}")
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule_tac x="traces ((PF ^ a) (%q. DIV) p)" in exI)
 apply (simp)
 apply (rule_tac x="a" in exI)
 apply (simp add: tracesFun_compo_n_Tf[THEN sym])
 apply (simp add: iteration_in_ProcFun tracesFun_f_p)
 apply (simp add: traces_prod_Bot)

 (* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (rule disjI2)
 apply (elim conjE exE)
 apply (simp)
 apply (rule_tac x="na" in exI)
 apply (simp add: tracesFun_compo_n_Tf[THEN sym])
 apply (simp add: iteration_in_ProcFun tracesFun_f_p)
 apply (simp add: traces_prod_Bot)
by (auto)

(*** [[ ]]T ***)

lemma semT_FIX:
    "PF : ProcFun ==>
     [[(FIX PF) p]]T
     = UnionT {u. EX n. u = ([[PF]]TFun ^ n) Bot p}"
apply (simp add: semT_to_traces)
apply (simp add: traces_FIX)
done

(*** FIX is LUB ***)

lemma semT_FIX_isLUB:
   "PF : ProcFun ==>
    (%p. [[(FIX PF) p]]T) isLUB {x. EX n. x = ([[PF]]TFun ^ 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: semT_FIX)
apply (subgoal_tac 
     "{y. EX x. (EX n. x = ([[PF]]TFun ^ n) Bot) & y = x i} =
      {u. EX n. u = ([[PF]]TFun ^ n) Bot i}")
apply (simp)
apply (rule UnionT_isLUB)
apply (auto)
done

lemma semT_FIX_LUB:
   "PF : ProcFun ==>
    (%p. [[(FIX PF) p]]T) = LUB {x. EX n. x = ([[PF]]TFun ^ n) Bot}"
apply (rule sym)
apply (rule isLUB_LUB)
apply (simp add: semT_FIX_isLUB)
done

lemma semT_FIX_LFP:
   "PF : ProcFun ==> (%p. [[(FIX PF) p]]T) = LFP [[PF]]TFun"
apply (simp add: semT_FIX_LUB)
apply (simp add: Tarski_thm_LFP_LUB continuous_semTFun)
done

lemma semT_FIX_LFP_p:
   "PF : ProcFun ==> [[(FIX PF) p]]T = LFP [[PF]]TFun p"
apply (insert semT_FIX_LFP[of PF])
apply (simp add: expand_fun_eq)
done

lemma semT_FIX_isLFP:
   "PF : ProcFun ==> (%p. [[(FIX PF) p]]T) isLFP [[PF]]TFun"
apply (simp add: semT_FIX_LFP)
apply (simp add: LFP_is Tarski_thm_EX continuous_semTFun)
done

lemma semT_FIX_LFP_fixed_point:
   "PF : ProcFun
    ==> [[PF]]TFun (%p. [[(FIX PF) p]]T) = (%p. [[(FIX PF) p]]T)"
apply (insert semT_FIX_isLFP[of PF], simp)
apply (simp add: isLFP_def)
done

lemma semT_FIX_LFP_least:
   "PF : ProcFun ==> 
    ALL Tf. [[PF]]TFun Tf = Tf --> (%p. [[(FIX PF) p]]T) <= Tf"
apply (insert semT_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 cspT_FIX_isGFP:
  "PF : ProcFun ==> 
   (FIX PF) =T' (PF (FIX PF)) & (ALL f. f =T' PF f --> f <=T' (FIX PF))"
apply (simp add: refT_prod_def eqT_prod_def)
apply (simp add: refT_def eqT_def)
apply (insert semT_FIX_isLFP[of PF], simp)
apply (rule)

 (* FP *)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (simp add: semTFun_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: semTFun_f_p)
 apply (simp add: isLFP_def)
 apply (erule conjE)
 apply (drule_tac x="(%p. [[f p]]T)" in spec)
 apply (simp add: order_prod_def)
done

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

lemma cspT_unwind_cpo_lm:
  "PF : ProcFun ==> ALL p. (FIX PF) p =T PF (FIX PF) p"
apply (simp add: eqT_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semTFun_f_p)
apply (simp add: semT_FIX_LFP_fixed_point)
done

(*** csp rule ***)

lemma cspT_unwind_cpo:
  "PF : ProcFun ==> (FIX PF) p =T PF (FIX PF) p"
by (simp add: cspT_unwind_cpo_lm)

lemmas cspT_unwind = cspT_unwind_cpo cspT_unwind_cms

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

lemma cspT_fp_induct_cpo_lm:
   "[| PF : ProcFun ; Q <=T f p ; ALL p. f p <=T (PF f) p |]
    ==> Q <=T (FIX PF) p"
apply (simp add: refT_def)
apply (simp add: fold_order_prod_def)
apply (simp add: semTFun_f_p)
apply (simp add: semT_FIX_LFP_p)
apply (insert cpo_fixpoint_induction_rev
       [of "[[PF]]TFun" "(%p. [[f p]]T)"])
apply (simp add: continuous_semTFun)
apply (simp add: order_prod_def)
apply (rotate_tac -1)
apply (drule_tac x="p" in spec)
apply (auto)
done

(*** csp rule ***)

lemma cspT_fp_induct_cpo:
   "[| PF : ProcFun ; Q <=T f p ; !!p. f p <=T (PF f) p |]
    ==> Q <=T (FIX PF) p"
by (simp add: cspT_fp_induct_cpo_lm)

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

lemma semT_FIX_UFP:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]T) = UFP [[PF]]TFun"
apply (subgoal_tac "[[PF]]TFun hasUFP")
apply (insert semT_FIX_isLFP[of PF], simp)
apply (subgoal_tac "UFP [[PF]]TFun isUFP [[PF]]TFun")
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]]T)" in spec)
apply (simp)
apply (simp add: UFP_is)
apply (simp add: contraction_semTFun Banach_thm_EX)
done

lemma traces_FIX_UFP:
   "PF : gProcFun ==>
    (%p. traces((FIX PF) p)) = UFP (tracesFun PF)"
apply (insert semT_FIX_UFP[of PF])
apply (simp add: semT_to_traces)
done

lemma semT_FIX_UFP_p:
   "PF : gProcFun ==>
    [[(FIX PF) p]]T = UFP [[PF]]TFun p"
apply (insert semT_FIX_UFP[of PF])
apply (simp add: expand_fun_eq)
done

lemma semT_FIX_isUFP:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]T) isUFP [[PF]]TFun"
apply (simp add: semT_FIX_UFP)
apply (simp add: contraction_semTFun Banach_thm_EX UFP_is)
done

lemma semT_FIX_UFP_unique:
   "PF : gProcFun ==>
    ALL Tf. [[PF]]TFun Tf = Tf --> (%p. [[(FIX PF) p]]T) = Tf"
apply (insert semT_FIX_isUFP[of PF], simp)
apply (simp add: isUFP_def)
done

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

lemma semT_FIX_FIX1:
   "PF : gProcFun ==>
    (%p. [[(FIX PF) p]]T) = (%p. [[(FIX! PF) p]]T)"
apply (simp add: semT_FIX_UFP)
apply (simp add: semT_FIX1_UFP)
done

lemma semT_FIX_FIX1_p:
   "PF : gProcFun ==>
    [[(FIX PF) p]]T = [[(FIX! PF) p]]T"
apply (simp add: semT_FIX_UFP_p)
apply (simp add: semT_FIX1_UFP_p)
done

lemma cspT_FIX_FIX1:
   "PF : gProcFun ==>
    (FIX PF) p =T (FIX! PF) p"
apply (simp add: eqT_def)
apply (simp add: semT_FIX_FIX1_p)
done

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

lemma cspT_FIX_isUFP:
   "PF : gProcFun ==>
   (FIX PF) =T' (PF (FIX PF)) & (ALL f. f =T' PF f --> f =T' (FIX PF))"
apply (simp add: cspT_FIX_isGFP)
apply (simp add: eqT_prod_def)
apply (simp add: eqT_def)
apply (insert semT_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: semTFun_f_p)
 apply (simp add: isUFP_def)
 apply (erule conjE)
 apply (drule_tac x="(%p. [[f p]]T)" in spec)
 apply (simp add: expand_fun_eq)
done

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

(* refinement *)

lemma cspT_fp_induct_cpo_ref_left_lm:
   "[| PF : gProcFun  ;
       f p <=T Q ; ALL p. (PF f) p <=T f p |]
    ==> (FIX PF) p <=T Q"
apply (rule cspT_rw_left)
apply (rule cspT_FIX_FIX1)
apply (simp_all)
apply (simp add: cspT_fp_induct_cms_ref_left_lm)
done

(*** csp rule ***)

lemma cspT_fp_induct_cpo_ref_left:
   "[| PF : gProcFun  ;
       f p <=T Q ; !! p. (PF f) p <=T f p |]
    ==> (FIX PF) p <=T Q"
by (simp add: cspT_fp_induct_cpo_ref_left_lm)

(* equivalence *)

lemma cspT_fp_induct_cpo_eq_left_lm:
   "[| PF : gProcFun  ;
       f p =T Q ; ALL p. (PF f) p =T f p |]
    ==> (FIX PF) p =T Q"
apply (rule cspT_rw_left)
apply (rule cspT_FIX_FIX1)
apply (simp_all)
apply (simp add: cspT_fp_induct_cms_eq_left_lm)
done

(*** csp rule ***)

lemma cspT_fp_induct_cpo_eq_left:
   "[| PF : gProcFun ;
       f p =T Q ; !! p. (PF f) p =T f p |]
    ==> (FIX PF) p =T Q"
by (simp add: cspT_fp_induct_cpo_eq_left_lm)


lemma cspT_fp_induct_cpo_eq_right:
   "[| PF : gProcFun ; 
       Q =T f p ; !! p. f p =T (PF f) p |]
    ==> Q =T (FIX PF) p"
apply (rule cspT_sym)
apply (rule cspT_fp_induct_cpo_eq_left)
apply (simp)
apply (rule cspT_sym)
apply (simp)
apply (rule cspT_sym)
apply (simp)
done

lemmas cspT_fp_induct_cpo_right = 
       cspT_fp_induct_cpo cspT_fp_induct_cpo_eq_right

lemmas cspT_fp_induct_cpo_left = 
       cspT_fp_induct_cpo_ref_left cspT_fp_induct_cpo_eq_left

(*** cpo and cms ***)

lemmas cspT_fp_induct_right = cspT_fp_induct_cpo_right cspT_fp_induct_cms_right
lemmas cspT_fp_induct_left = cspT_fp_induct_cpo_left cspT_fp_induct_cms_left

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

lemma traces_FIXn_plus_sub_lm:
 "PF : ProcFun ==>
  ALL n m p. traces ((FIX[n] PF) p) <= traces ((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_traces)

apply (rule allI)
apply (simp add: FIXn_def)
apply (drule_tac x="m" in spec)
apply (simp add: tracesFun_f_p)
apply (fold order_prod_def)
apply (simp add: mono_tracesFun[simplified mono_def])
done

lemma traces_FIXn_plus_sub: 
   "PF : ProcFun ==> traces ((FIX[n] PF) p) <= traces ((FIX[n+m] PF) p)"
by (simp add: traces_FIXn_plus_sub_lm)

lemma semT_FIXn_plus_sub:
 "PF : ProcFun ==> [[(FIX[n] PF) p]]T <= [[(FIX[n+m] PF) p]]T"
apply (simp add: semT_to_traces)
apply (simp add: traces_FIXn_plus_sub)
done

lemma in_traces_FIXn_plus_sub: 
  "[| PF : ProcFun ; t :t traces ((FIX[n] PF) p) |] ==> t :t traces ((FIX[n+m] PF) p)"
apply (insert traces_FIXn_plus_sub[of PF n p m])
by (auto)

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

lemma cspT_FIX_plus_eq: 
     "PF : ProcFun ==>
      ALL f p. (FIX PF) p =T (!nat n .. ((FIX[n + f n] PF) p))"
apply (simp add: FIX_def)
apply (simp add: eqT_def)
apply (intro allI)
apply (simp add: semT_def)
apply (rule order_antisym)

 apply (rule)
 apply (simp add: in_traces)
 apply (rule disjI2)
 apply (elim conjE exE disjE, simp)
 apply (rule_tac x="a" in exI)
 apply (simp add: in_traces_FIXn_plus_sub)

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

lemma cspT_FIX_plus_eq_fun: 
     "PF : ProcFun ==>
      ALL f p. (%p. (FIX PF) p) =T' (%p. (!nat n .. ((FIX[n + f n] PF) p)))"
apply (simp add: eqT_prod_def)
apply (simp add: cspT_FIX_plus_eq)
done

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

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

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

lemma cspT_MU_isGFP:
  "PX : ProcX
    ==> MUX PX =T PX (MUX PX) & (ALL P. P =T PX P --> P <=T (MUX PX))"
apply (simp add: MUX_def)
apply (insert cspT_FIX_isGFP[of "(%f p. PX (f MUp))"])
apply (simp add: ProcX_def ProcFun_def)
apply (simp add: eqT_prod_def refT_prod_def)
apply (intro allI impI)
apply (elim conjE)
apply (drule_tac x="(%p. P)" in spec)
apply (simp)
done

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

lemma cspT_unwind_MU_cpo:
  "PX : ProcX ==> MUX PX =T PX (MUX PX)"
apply (simp add: MUX_def)
apply (insert cspT_unwind[of "(%f p. PX (f MUp))" "MUp"])
apply (simp add: ProcX_def)
apply (simp add: ProcFun_def)
done

lemmas cspT_unwind_MU = cspT_unwind_MU_cms cspT_unwind_MU_cpo

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

lemma cspT_fp_induct_MU_cpo:
   "[| PX : ProcX ; Q <=T PX Q |] ==> Q <=T (MUX PX)"
apply (simp add: MUX_def)
apply (rule cspT_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 cspT_fp_induct_MU_cpo_ref_left:
   "[| PX : gProcX ; PX Q <=T Q |]
    ==> (MUX PX) <=T Q"
apply (simp add: MUX_def)
apply (rule cspT_fp_induct_cpo_ref_left[of _ "(%X. Q)"])
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
apply (simp)
apply (simp)
done

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

lemma cspT_fp_induct_MU_cpo_eq_right:
   "[| PX : gProcX ; Q =T PX Q |]
    ==> Q =T (MUX PX)"
apply (rule cspT_sym)
apply (rule cspT_fp_induct_MU_cpo_eq_left)
apply (simp)
apply (rule cspT_sym)
apply (simp)
done

lemmas cspT_fp_induct_MU_cpo_right
     = cspT_fp_induct_MU_cpo cspT_fp_induct_MU_cpo_eq_right

lemmas cspT_fp_induct_MU_cpo_left
     = cspT_fp_induct_MU_cpo_ref_left cspT_fp_induct_MU_cpo_eq_left

(*** cpo and cms ***)

lemmas cspT_fp_induct_MU_right = cspT_fp_induct_MU_cpo_right
                                 cspT_fp_induct_MU_cms_right

lemmas cspT_fp_induct_MU_left = cspT_fp_induct_MU_cpo_left
                                cspT_fp_induct_MU_cms_left

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

lemma cspT_MU_MU1:
   "PX : gProcX ==> (MUX PX) =T (MUX! PX)"
apply (simp add: MUX_def)
apply (simp add: MUX1_def)
apply (rule cspT_FIX_FIX1)
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
done

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

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

lemma cspT_MU_plus_eq: 
     "PX : ProcX ==>
      ALL f. (MUX PX) =T (!nat n .. (PX ^ (n + f n)) DIV)"
apply (insert cspT_FIX_plus_eq[of "(%f p. PX (f 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: cspT_MU_plus_eq_lm)
done

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

lemmas cspT_MU_eq = cspT_MU_eq_cms cspT_MU_eq_cpo

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end