Theory CSP_T_law_ufp

           (*-------------------------------------------*
            |        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_ufp = CSP_T_continuous + CSP_T_contraction + CSP_T_mono
                     + CSP_T_law_decompo:

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

         1. cms 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]

(*=======================================================*
 |                                                       |
 |                        CMS                            |
 |                                                       |
 *=======================================================*)

lemma cspT_Banach_fix:
   "(FIX! PF)(p) =T (!nat n .. ((((PF^n) (%q. AnyInitProc)) p) |. n))"
apply (simp add: FIX1_def FIX1n_def)
done

(*-----------*
 |  normal   |
 *-----------*)

lemma semT_normal_FIX1_lm_induct:
   "ALL PF p. PF : gProcFun -->
    (ALL m. n <= m -->
         distance ([[(PF ^ n) Any p]]T, [[(PF ^ m) Any p]]T)
         <= (1 / 2) ^ n)"
apply (rule induct
[of "(%n. ALL PF p. PF : gProcFun -->
     (ALL m. n <= m -->
         distance ([[(PF ^ n) Any p]]T, [[(PF ^ m) Any p]]T)
         <= (1 / 2) ^ n))" n])
apply (simp add: distance_rs_less_one)

(* step *)
apply (intro allI impI)
apply (simp only: gProcFun_implies_ProcFun iteration_in_ProcFun semTFun_f_p)
apply (simp add: iteration_in_ProcFun compo_in_ProcFun 
                 semTFun_compo_semTFun_fun)

apply (drule_tac x="PF" in spec)
apply (simp)
apply (subgoal_tac "EX m'. m = Suc m'")
apply (erule exE)
apply (erule exchange_forall_orderE)
apply (simp)
apply (simp add: iteration_in_ProcFun semTFun_compo_semTFun_fun)
apply (drule_tac x="m'" in spec)
apply (simp)
apply (simp add: iteration_in_ProcFun compo_in_ProcFun semTFun_f_p)
apply (subgoal_tac 
  "distance ([[PF ^ n]]TFun (%p. [[Any p]]T) ,
             [[PF ^ m']]TFun (%p. [[Any p]]T))
   <= (1 / 2) ^ n")
apply (rule order_trans)
apply (subgoal_tac
  "distance ([[PF]]TFun ([[PF ^ n]]TFun (%p. [[Any p]]T)) p,
             [[PF]]TFun ([[PF ^ m']]TFun (%p. [[Any p]]T)) p) * 2
<= distance ([[PF]]TFun ([[PF ^ n]]TFun (%p. [[Any p]]T)),
             [[PF]]TFun ([[PF ^ m']]TFun (%p. [[Any p]]T))) * 2")
apply (assumption)
apply (simp)
apply (rule prod_distance_rs_le)

apply (subgoal_tac "contraction_alpha [[PF]]TFun (1/2)")
apply (simp add: contraction_alpha_def)
apply (simp add: map_alpha_def)
apply (drule_tac x="([[PF ^ n]]TFun (%p. [[Any p]]T))" in spec)
apply (drule_tac x="([[PF ^ m']]TFun (%p. [[Any p]]T))" in spec)
apply (rule order_trans)
apply (assumption)
apply (simp)
apply (simp add: contraction_alpha_semTFun)

apply (simp add: prod_distance_least)
apply (insert nat_zero_or_Suc)
apply (drule_tac x="m" in spec)
apply (simp)
done

lemma semT_normal_FIX1_lm:
   "PF : gProcFun ==>
     distance ([[(PF ^ n) Any p]]T, [[(PF ^ m) Any p]]T)
     <= (1 / 2) ^ min n m"
apply (case_tac "n <= m")
 apply (simp add: min_def)
 apply (simp add: semT_normal_FIX1_lm_induct)
 apply (simp add: min_def)
 apply (subgoal_tac
   "distance ([[(PF ^ n) Any p]]T, [[(PF ^ m) Any p]]T) =
    distance ([[(PF ^ m) Any p]]T, [[(PF ^ n) Any p]]T)")
 apply (simp add: semT_normal_FIX1_lm_induct)
 apply (simp add: symmetry_ms)
done

(* normal *)

lemma semT_normal_FIX1:
   "PF : gProcFun ==> normal (%n. [[(FIX![n] PF) p]]T)"
apply (unfold normal_def)
apply (intro allI)
apply (simp add: FIX1n_def del: funpow.simps)
 apply (rule order_trans)
 apply (rule semT_normal_FIX1_lm)
 apply (simp_all)
done

(* normal p *)

lemma semT_normal_FIX1_p:
   "PF : gProcFun ==> normal (%n p. [[(FIX![n] PF) p]]T)"
apply (simp add: prod_normal_seq_iff)
apply (intro allI)
apply (simp add: proj_fun_def)
apply (simp add: comp_def)
apply (simp add: semT_normal_FIX1)
done

(*-----------*
 |   limit   |
 *-----------*)

lemma semT_FIX1_prod_Limit_lm:
  "normal (%x. traces((FIX![x] PF) p)) ==>
   traces (!nat n .. (FIX![n] PF) p |. n) = 
   Limit_domT (%x. traces ((FIX![x] PF) p))"
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE)
 apply (simp)
 apply (elim conjE exE)
 apply (simp add: Limit_domT_def)
 apply (simp (no_asm_simp) add: memT_def)
 apply (simp add: Abs_domT_inverse)
 apply (simp add: LimitT_def)

 apply (subgoal_tac
  "(t :t traces ((FIX![lengtht t] PF) p))
   = (t :t traces ((FIX![a] PF) p))")
 apply (simp)
 apply (rule normal_seq_domT)
 apply (simp_all)

 (* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (simp add: Limit_domT_def)
 apply (simp add: memT_def)
 apply (simp add: Abs_domT_inverse)
 apply (fold memT_def)
 apply (simp add: LimitT_def)
 apply (rule disjI2)
 apply (rule_tac x="(lengtht t)" in exI)
 apply (simp)
done

lemma semT_FIX1_prod_Limit:
 "PF : gProcFun ==>
  [[(FIX! PF) p]]T = (prod_Limit (%n p. [[(FIX![n] PF) p]]T)) p"
apply (simp add: prod_Limit_def)
apply (simp add: proj_fun_def)
apply (simp add: comp_def)
apply (subgoal_tac "normal (%x. [[(FIX![x] PF) p]]T)")
apply (simp add: Limit_domT_Limit_eq)
apply (simp add: FIX1_def)
apply (simp add: semT_def)
apply (simp add: semT_FIX1_prod_Limit_lm)
apply (simp add: semT_normal_FIX1)
done

(*--------------*
 |  convergeTo  |
 *--------------*)

lemma semT_FIX1_convergeTo_prod_Limit:
  "PF : gProcFun ==>
   (%n p. [[(FIX![n] PF) p]]T) convergeTo 
   (prod_Limit (%n p. [[(FIX![n] PF) p]]T))"
apply (rule prod_cms_normal_Limit)
apply (simp add: prod_normal_seq_iff)
apply (rule allI)
apply (simp add: proj_fun_def)
apply (simp add: comp_def)
apply (simp add: semT_normal_FIX1)
done

lemma semT_FIX1_convergeTo_FIX1:
  "PF : gProcFun ==>
   (%n p. [[(FIX![n] PF) p]]T) convergeTo 
    (%p. [[(FIX! PF) p]]T)"
apply (simp add: semT_FIX1_prod_Limit)
apply (simp add: semT_FIX1_convergeTo_prod_Limit)
done

(*--------------*
 |      UFP     |
 *--------------*)

lemma semT_FIX1_UFP:
  "PF : gProcFun ==> (%p. [[(FIX! PF) p]]T) = UFP [[PF]]TFun"
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (insert semT_FIX1_convergeTo_FIX1[of PF])
apply (simp add: semT_normal_FIX1_p prod_convergeTo)
apply (simp add: proj_fun_def)
apply (simp add: comp_def)
apply (drule_tac x="x" in spec)
apply (insert semT_normal_FIX1_p[of PF])
apply (simp add: FIX1n_def)
apply (simp add: semTFun_f_p iteration_in_ProcFun)
apply (simp add: semTFun_compo_n_Tf)
apply (insert Banach_thm_prod[of "[[PF]]TFun" "(%p. [[AnyInitProc]]T)"])
apply (simp add: contraction_semTFun)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (simp add: unique_convergence)
done

lemma traces_FIX1_UFP:
  "PF : gProcFun ==> (%p. traces ((FIX! PF) p)) = UFP (tracesFun PF)"
apply (simp add: semT_FIX1_UFP[simplified semT_def])
apply (simp add: semTFun_tracesFun)
done

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

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

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

lemma semT_FIX1_UFP_fixed_point:
   "PF : gProcFun
    ==> [[PF]]TFun (%p. [[(FIX! PF) p]]T) = (%p. [[(FIX! PF) p]]T)"
apply (insert semT_FIX1_isUFP[of PF], simp)
apply (simp add: isUFP_def)
done

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

lemma cspT_FIX1_isUFP:
   "PF : gProcFun ==>
   (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_FIX1_isUFP[of PF], simp)
apply (rule)

 (* FP *)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (simp add: semTFun_f_p)
 apply (simp add: isUFP_def)

 (* 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: order_prod_def)
 apply (simp add: expand_fun_eq)
done

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

lemma cspT_unwind_cms_lm:
  "PF : gProcFun
   ==> 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_FIX1_UFP_fixed_point)
done

(*** csp rule ***)

lemma cspT_unwind_cms:
  "PF : gProcFun ==> (FIX! PF) p =T PF (FIX! PF) p"
by (simp add: cspT_unwind_cms_lm)

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

(* refinement *)

lemma cspT_fp_induct_cms_ref_left_lm:
   "[| PF : gProcFun ; f p <=T Q ; ALL p. (PF f) p <=T f p |]
    ==> (FIX! PF) p <=T Q"
apply (simp add: refT_def)
apply (simp add: fold_order_prod_def)
apply (simp add: semTFun_f_p)

apply (simp add: semT_FIX1_UFP_p)
apply (insert cms_fixpoint_induction_ref
       [of "[[PF]]TFun" "(%p. [[f p]]T)" "UFP [[PF]]TFun"])
apply (simp add: contra_alpha_to_contst contraction_alpha_semTFun)
apply (simp add: mono_semTFun)
apply (simp add: contraction_semTFun UFP_fp Banach_thm_EX)
apply (simp add: order_prod_def)
apply (rotate_tac -1)
apply (drule_tac x="p" in spec)
apply (simp)
done

(*** csp rule ***)

lemma cspT_fp_induct_cms_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_cms_ref_left_lm)

(*** right ***)

lemma cspT_fp_induct_cms_right_lm:
   "[| PF : gProcFun  ; 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_FIX1_UFP_p)
apply (insert cms_fixpoint_induction_rev
       [of "[[PF]]TFun" "(%p. [[f p]]T)" "UFP [[PF]]TFun"])
apply (simp add: contra_alpha_to_contst contraction_alpha_semTFun)
apply (simp add: mono_semTFun)
apply (simp add: contraction_semTFun UFP_fp Banach_thm_EX)
apply (simp add: order_prod_def)
apply (rotate_tac -1)
apply (drule_tac x="p" in spec)
apply (simp)
done

(*** csp rule ***)

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

(* equivalence *)

lemma cspT_fp_induct_cms_eq_left_lm:
   "[| PF : gProcFun ; f p =T Q ; ALL p. (PF f) p =T f p |]
    ==> (FIX! PF) p =T Q"
apply (simp add: eqT_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semTFun_f_p)
apply (insert semT_FIX1_isUFP[of PF], simp)
apply (simp add: isUFP_def)
apply (elim conjE)
apply (drule_tac x="(%p. [[f p]]T)" in spec)
apply (simp add: expand_fun_eq)
done

(*** csp rule ***)

lemma cspT_fp_induct_cms_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_cms_eq_left_lm)

lemma cspT_fp_induct_cms_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_cms_eq_left)
apply (simp)
apply (rule cspT_sym)
apply (simp)
apply (rule cspT_sym)
apply (simp)
done

lemmas cspT_fp_induct_cms_left 
     = cspT_fp_induct_cms_ref_left cspT_fp_induct_cms_eq_left

lemmas cspT_fp_induct_cms_right 
     = cspT_fp_induct_cms_ref_right cspT_fp_induct_cms_eq_right

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

(*=======================================================*
 |                         cms                           |
 *=======================================================*)

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

lemma cspT_MU1_isUFP:
   "PX : gProcX
    ==> MUX! PX =T PX (MUX! PX) & (ALL P. P =T PX P --> P =T (MUX! PX))"
apply (simp add: MUX1_def)
apply (insert cspT_FIX1_isUFP[of "(%f p. PX (f MUp))"])
apply (simp add: gProcX_def gProcFun_def)
apply (simp add: eqT_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_cms:
  "PX : gProcX ==> MUX! PX =T PX (MUX! PX)"
apply (simp add: MUX1_def)--koko
apply (insert cspT_unwind_cms[of "(%f p. PX (f MUp))" "MUp"])
apply (simp add: gProcX_def gProcFun_def)
done

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

lemma cspT_fp_induct_MU_cms_ref_left:
   "[| PX : gProcX ; PX Q <=T Q |] ==> (MUX! PX) <=T Q"
apply (simp add: MUX1_def)
apply (rule cspT_fp_induct_cms_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_cms_ref_right:
   "[| PX : gProcX ; Q <=T PX Q |]
    ==> Q <=T (MUX! PX)"
apply (simp add: MUX1_def)
apply (rule cspT_fp_induct_cms_ref_right[of _ _"(%X. Q)"])
apply (simp add: gProcX_def)
apply (simp add: gProcFun_def)
apply (simp)
apply (simp)
done

lemma cspT_fp_induct_MU_cms_eq_left:
   "[| PX : gProcX ; PX Q =T Q |]
    ==> (MUX! PX) =T Q"
apply (simp add: MUX1_def)
apply (rule cspT_fp_induct_cms_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_cms_eq_right:
   "[| PX : gProcX ; Q =T PX Q |]
    ==> Q =T (MUX! PX)"
apply (rule cspT_sym)
apply (rule cspT_fp_induct_MU_cms_eq_left)
apply (simp)
apply (rule cspT_sym)
apply (simp)
done

lemmas cspT_fp_induct_MU_cms_left = cspT_fp_induct_MU_cms_ref_left
                                    cspT_fp_induct_MU_cms_eq_left

lemmas cspT_fp_induct_MU_cms_right = cspT_fp_induct_MU_cms_ref_right
                                     cspT_fp_induct_MU_cms_eq_right

(*=======================================================*
 |                   expand by Banach                    |
 *=======================================================*)

lemma cspT_MU_eq_cms: 
   "PX : gProcX
    ==> (MUX! PX) =T (!nat n .. ((PX ^ n) AnyInitProc) |. n)"
apply (simp add: MUX1_def)
apply (simp add: FIX1_def)
apply (simp add: FIX1n_def)
apply (rule cspT_decompo)
apply (simp)
apply (simp)
apply (induct_tac n)
apply (simp)

(* step *)
apply (simp add: cspT_semantics)
apply (simp add: traces.simps)
apply (subgoal_tac "constructive_rs (tracesFun (%f p. PX (f MUp)))") (* sub 1 *)

 apply (simp add: constructive_rs_def)
 apply (simp add: tracesFun_def)
 apply (simp add: tracesfun_def)

 apply (drule_tac x=
  "(%p. traces (((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp))" in spec)
 apply (drule_tac x="(%p. traces ((PX ^ na) AnyInitProc))" in spec)
 apply (drule_tac x="na" in spec)
 apply (simp add: prod_restriction_def)
 apply (simp add: expand_fun_eq)

 apply (subgoal_tac
   "(PX (Proc_T (traces (((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp))))
    =T (PX (((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp))")   (* sub 2 *)
 apply (subgoal_tac
   "(PX (Proc_T(traces ((PX ^ na) AnyInitProc))))
    =T (PX ((PX ^ na) AnyInitProc))")                                (* sub 3 *)
 apply (simp add: cspT_semantics)

 (* sub 3*)
 apply (rule cspT_ProcX_cong[of PX])
 apply (simp)
 apply (simp add: cspT_semantics)
 apply (simp add: traces_Proc_T)

 (* sub 2*)
 apply (rule cspT_ProcX_cong[of PX])
 apply (simp)
 apply (simp add: cspT_semantics)
 apply (simp add: traces_Proc_T)

(* sub 1 *)
apply (rule contra_alpha_to_contst)
apply (rule contraction_alpha_tracesFun)
apply (simp add: gProcX_def gProcFun_def)
done

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end