Theory CSP_F_law_ufp

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

theory CSP_F_law_ufp = CSP_F_continuous + CSP_F_contraction + CSP_F_mono
                     + CSP_F_law_decompo + CSP_T_law_ufp:

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

         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 cspF_Banach_fix:
   "(FIX! PF)(p) =F (!nat n .. ((((PF^n) (%q. AnyInitProc)) p) |. n))"
apply (simp add: FIX1_def FIX1n_def)
done

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

lemma semF_normal_FIX1_lm_induct:
   "ALL PF p. PF : gProcFun -->
    (ALL m. n <= m -->
         distance ([[(PF ^ n) Any p]]F, [[(PF ^ m) Any p]]F)
         <= (1 / 2) ^ n)"
apply (rule induct
[of "(%n. ALL PF p. PF : gProcFun -->
     (ALL m. n <= m -->
         distance ([[(PF ^ n) Any p]]F, [[(PF ^ m) Any p]]F)
         <= (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 semFFun_f_p)
apply (simp add: iteration_in_ProcFun compo_in_ProcFun 
                 semFFun_compo_semFFun_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 semFFun_compo_semFFun_fun)
apply (drule_tac x="m'" in spec)
apply (simp)
apply (simp add: iteration_in_ProcFun compo_in_ProcFun semFFun_f_p)
apply (subgoal_tac 
  "distance ([[PF ^ n]]FFun (%p. [[Any p]]F) ,
             [[PF ^ m']]FFun (%p. [[Any p]]F))
   <= (1 / 2) ^ n")
apply (rule order_trans)
apply (subgoal_tac
  "distance ([[PF]]FFun ([[PF ^ n]]FFun (%p. [[Any p]]F)) p,
             [[PF]]FFun ([[PF ^ m']]FFun (%p. [[Any p]]F)) p) * 2
<= distance ([[PF]]FFun ([[PF ^ n]]FFun (%p. [[Any p]]F)),
             [[PF]]FFun ([[PF ^ m']]FFun (%p. [[Any p]]F))) * 2")
apply (assumption)
apply (simp)
apply (rule prod_distance_rs_le)

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

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

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

(* normal *)

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

(* normal p *)

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

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

lemma semF_FIX1_prod_Limit_lm:
  "normal (%x. failures ((FIX![x] PF) p)) ==>
   failures (!nat n .. (FIX![n] PF) p |. n) =
   Limit_setF (%x. failures ((FIX![x] PF) p))"
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE)

 apply (simp add: Limit_setF_def)
 apply (simp (no_asm_simp) add: memF_def)
 apply (simp add: Abs_setF_inverse)
 apply (simp add: LimitF_def)

 apply (erule disjE)

  apply (rule disjI1)
  apply (subgoal_tac
   "((s, X) :f failures ((FIX![Suc (lengtht s)] PF) p))
    = ((s, X) :f failures ((FIX![a] PF) p))")
  apply (simp)
  apply (rule normal_seq_setF_less)
  apply (simp_all)

 (* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (simp add: Limit_setF_def)
 apply (simp add: memF_def)
 apply (simp add: Abs_setF_inverse)
 apply (fold memF_def)
 apply (simp add: LimitF_def)
 apply (erule disjE)

  apply (rule_tac x="Suc (lengtht s)" in exI)
  apply (simp)

  apply (rule_tac x="(lengtht s)" in exI)
  apply (simp)
done

lemma semF_FIX1_prod_Limit:
 "PF : gProcFun ==>
  [[(FIX! PF) p]]F = (prod_Limit (%n p. [[(FIX![n] PF) p]]F)) 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]]F)")
apply (simp add: Limit_domF_Limit_eq)
apply (simp add: FIX1_def)

apply (simp add: semF_def)
apply (simp add: pairF_def)
apply (simp add: Limit_domF_def)
apply (simp add: LimitTF_in Abs_domF_inject)
apply (simp add: LimitTF_def)

apply (simp add: normal_domF LimitTF_iff)
apply (simp add: comp_def)
apply (simp add: Abs_domF_inverse)
apply (fold pairF_def)
apply (simp add: pairF)

apply (simp add: pair_normal_seq_compo_iff)
apply (simp add: comp_def)
apply (erule conjE)

apply (simp add: semT_FIX1_prod_Limit_lm)
apply (simp add: semF_FIX1_prod_Limit_lm)

apply (simp add: semF_normal_FIX1)
done

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

lemma semF_FIX1_convergeTo_prod_Limit:
  "PF : gProcFun ==>
   (%n p. [[(FIX![n] PF) p]]F) convergeTo 
   (prod_Limit (%n p. [[(FIX![n] PF) p]]F))"
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: semF_normal_FIX1)
done

lemma semF_FIX1_convergeTo_FIX1:
  "PF : gProcFun ==>
   (%n p. [[(FIX![n] PF) p]]F) convergeTo 
    (%p. [[(FIX! PF) p]]F)"
apply (simp add: semF_FIX1_prod_Limit)
apply (simp add: semF_FIX1_convergeTo_prod_Limit)
done

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

lemma semF_FIX1_UFP:
  "PF : gProcFun
   ==> (%p. [[(FIX! PF) p]]F) = UFP [[PF]]FFun"
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (insert semF_FIX1_convergeTo_FIX1[of PF])
apply (simp add: semF_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 semF_normal_FIX1_p[of PF])
apply (simp add: FIX1n_def)
apply (simp add: semFFun_f_p iteration_in_ProcFun)
apply (simp add: semFFun_compo_n_SFf)
apply (insert Banach_thm_prod[of "[[PF]]FFun" "(%p. [[AnyInitProc]]F)"])
apply (simp add: contraction_semFFun)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (simp add: unique_convergence)
done

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

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

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

lemma semF_FIX1_UFP_fixed_point:
   "PF : gProcFun 
    ==> [[PF]]FFun (%p. [[(FIX! PF) p]]F) = (%p. [[(FIX! PF) p]]F)"
apply (insert semF_FIX1_isUFP[of PF], simp)
apply (simp add: isUFP_def)
done

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

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

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

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

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

(*** csp rule ***)

lemma cspF_unwind_cms:
  "PF : gProcFun
   ==> (FIX! PF) p =F PF (FIX! PF) p"
by (simp add: cspF_unwind_cms_lm)

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

(* refinement *)

lemma cspF_fp_induct_cms_ref_left_lm:
   "[| PF : gProcFun  ;
       f p <=F Q ; ALL p. (PF f) p <=F f p |]
    ==> (FIX! PF) p <=F Q"
apply (simp add: refF_def)
apply (simp add: fold_order_prod_def)
apply (simp add: semFFun_f_p)

apply (simp add: semF_FIX1_UFP_p)
apply (insert cms_fixpoint_induction_ref
       [of "[[PF]]FFun" "(%p. [[f p]]F)" "UFP [[PF]]FFun"])
apply (simp add: contra_alpha_to_contst contraction_alpha_semFFun)
apply (simp add: mono_semFFun)
apply (simp add: contraction_semFFun 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 cspF_fp_induct_cms_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_cms_ref_left_lm)

(*** reverse ***)

lemma cspF_fp_induct_cms_ref_right_lm:
   "[| PF : gProcFun  ;
    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_FIX1_UFP_p)
apply (insert cms_fixpoint_induction_rev
       [of "[[PF]]FFun" "(%p. [[f p]]F)" "UFP [[PF]]FFun"])
apply (simp add: contra_alpha_to_contst contraction_alpha_semFFun)
apply (simp add: mono_semFFun)
apply (simp add: contraction_semFFun 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 cspF_fp_induct_cms_ref_right:
   "[| PF : gProcFun  ;
    Q <=F f p ; !!p. f p <=F (PF f) p |]
    ==> Q <=F (FIX! PF) p"
by (simp add: cspF_fp_induct_cms_ref_right_lm)

(* equivalence *)

lemma cspF_fp_induct_cms_eq_left_lm:
   "[| PF : gProcFun  ;
       f p =F Q ; ALL p. (PF f) p =F f p |]
    ==> (FIX! PF) p =F Q"
apply (simp add: eqF_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semFFun_f_p)
apply (insert semF_FIX1_isUFP[of PF], simp)
apply (simp add: isUFP_def)
apply (elim conjE)
apply (drule_tac x="(%p. [[f p]]F)" in spec)
apply (simp add: expand_fun_eq)
done

(*** csp rule ***)

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

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

lemmas cspF_fp_induct_cms_left 
     = cspF_fp_induct_cms_ref_left cspF_fp_induct_cms_eq_left

lemmas cspF_fp_induct_cms_right 
     = cspF_fp_induct_cms_ref_right cspF_fp_induct_cms_eq_right

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

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

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

lemma cspF_MU1_isUFP:
   "PX : gProcX
    ==> MUX! PX =F PX (MUX! PX) & (ALL P. P =F PX P --> P =F (MUX! PX))"
apply (simp add: MUX1_def)
apply (insert cspF_FIX1_isUFP[of "(%f p. PX (f MUp))"])
apply (simp add: gProcX_def gProcFun_def)
apply (simp add: eqF_prod_def)
apply (intro allI impI)
apply (elim conjE)
apply (drule_tac x="(%f. P)" in spec)
apply (simp)
done

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

lemma cspF_unwind_MU_cms:
  "PX : gProcX
    ==> MUX! PX =F PX (MUX! PX)"
apply (simp add: cspF_MU1_isUFP)
done

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

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

lemma cspF_fp_induct_MU_cms_eq_left:
   "[| PX : gProcX ; PX Q =F Q |]
    ==> (MUX! PX) =F Q"
apply (simp add: MUX1_def)
apply (rule cspF_fp_induct_cms_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_cms_eq_right:
   "[| PX : gProcX ; Q =F PX Q |]
    ==> Q =F (MUX! PX)"
apply (rule cspF_sym)
apply (rule cspF_fp_induct_MU_cms_eq_left)
apply (simp)
apply (rule cspF_sym)
apply (simp)
done

lemmas cspF_fp_induct_MU_cms_left = cspF_fp_induct_MU_cms_ref_left
                                    cspF_fp_induct_MU_cms_eq_left

lemmas cspF_fp_induct_MU_cms_right = cspF_fp_induct_MU_cms_ref_right
                                     cspF_fp_induct_MU_cms_eq_right

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

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

(* step *)
apply (simp add: eqF_def)
apply (simp add: semF_Depth_rest)
apply (subgoal_tac "constructive_rs ([[%f p. PX (f MUp)]]FFun)") (* sub 1 *)

 apply (simp add: constructive_rs_def)
 apply (simp add: semFFun_def)
 apply (simp add: semFfun_def)

 apply (drule_tac x=
  "(%p. [[((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp]]F)" in spec)
 apply (drule_tac x=
  "(%p. [[(PX ^ na) AnyInitProc]]F)" 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_F([[((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp]]F)))
    =F (PX (((%f n. PX (f MUp)) ^ na) (%q. AnyInitProc) MUp))")  (* sub 2 *)
 apply (subgoal_tac
   "(PX (Proc_F([[(PX ^ na) AnyInitProc]]F)))
    =F (PX ((PX ^ na) AnyInitProc))")                                 (* sub 3 *)
 apply (simp add: eqF_def)

 (* sub 3*)
 apply (rule cspF_ProcX_cong[of PX])
 apply (simp)
 apply (simp add: eqF_def)
 apply (simp add: semF_Proc_F)

 (* sub 2*)
 apply (rule cspF_ProcX_cong[of PX])
 apply (simp)
 apply (simp add: eqF_def)
 apply (simp add: semF_Proc_F)

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

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end