Theory CSP_F_law_fp

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_law_fp
imports CSP_T_law_fp CSP_F_law_ufp
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               February 2005               |
            |                   June 2005 (modified)    |
            |              September 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_fp
imports CSP_T_law_fp CSP_F_law_ufp
begin

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

         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                            |
 |                                                       |
 *=======================================================*)

(*-------------*
 |  existency  |
 *-------------*)

lemma semF_hasLFP_cpo: 
 "Pf = PNfun ==> [[Pf]]Ffun hasLFP"
apply (rule Tarski_thm_EX)
apply (rule continuous_semFfun)
done

lemma semF_LFP_cpo:
  "[| Pf = PNfun ;
      FPmode = CPOmode | FPmode = MIXmode |]
  ==> [[$p]]F = LFP [[Pf]]Ffun p"
apply (simp add: semF_def)
apply (simp add: semFf_Proc_name)
apply (simp add: MF_def)
apply (simp add: semFfix_def)
apply (force)
done

lemma semF_LFP_fun_cpo:
  "[| Pf = PNfun ;
      FPmode = CPOmode | FPmode = MIXmode |]
  ==> (%p. [[$p]]F) = LFP [[Pf]]Ffun"
apply (simp (no_asm) add: expand_fun_eq)
apply (simp add: semF_LFP_cpo)
done

(*---------*
 |    MF   |
 *---------*)

lemma MF_fixed_point_cpo:
      "[| (Pf::'p=>('p,'a) proc) = PNfun; FPmode = CPOmode | FPmode = MIXmode |]
        ==> [[Pf]]Ffun (MF::'p => 'a domF) = (MF::'p => 'a domF)"
apply (simp add: MF_def)
apply (simp add: semFfix_def)
apply (erule disjE)
apply (simp_all)
apply (rule LFP_fp)
apply (simp add: semF_hasLFP_cpo)
apply (rule LFP_fp)
apply (simp add: semF_hasLFP_cpo)
done

(*-------------*
 |  greatest   |
 *-------------*)

lemma ALL_cspF_greatest_cpo:
  "[| Pf = PNfun ;
       FPmode = CPOmode ;
       ALL p. (Pf p) << f =F f p |] ==> ALL p. f p <=F $p"
apply (simp add: eqF_def refF_def)
apply (fold semF_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (fold order_prod_def)
apply (insert semF_LFP_fun_cpo[of "Pf"])
apply (simp)

apply (rule LFP_least)
apply (simp add: semF_hasLFP_cpo)

apply (simp add: semF_subst)
apply (simp add: semFfun_def)
done

lemma cspF_greatest_cpo:
  "[| Pf = PNfun ;
       FPmode = CPOmode ;
       ALL p. (Pf p) << f =F f p |] ==> f p <=F $p"
by (simp add: ALL_cspF_greatest_cpo)

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

lemma ALL_cspF_unwind_cpo:
   "[| Pf = PNfun ;
       FPmode = CPOmode | FPmode = MIXmode |]
     ==> ALL p. ($p =F Pf p)"
apply (simp add: eqF_def)
apply (simp add: semFf_Proc_name)
apply (simp add: MF_def)
apply (simp add: semFfix_def)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semFf_semFfun)
apply (simp add: LFP_fp semF_hasLFP_cpo)
apply (force)
done

(*  csp law  *)

lemma cspF_unwind_cpo:
   "[| Pf = PNfun ;
       FPmode = CPOmode | FPmode = MIXmode |]
     ==> $p =F Pf p"
by (simp add: ALL_cspF_unwind_cpo)

(*-------------------------------------------------------*
 |                                                       |
 |    fixed point inducntion (CSP-Prover intro rule)     |
 |                                                       |
 *-------------------------------------------------------*)

(*** right ***)

lemma cspF_fp_induct_cpo_ref_right_ALL:
   "[| Pf = PNfun ;
       FPmode = CPOmode | FPmode = MIXmode ;
       Q <=F f p;
       ALL p. f p <=F (Pf p)<<f |]
    ==> Q <=F $p"
apply (simp add: refF_semF)
apply (insert cpo_fixpoint_induction_rev
       [of "[[Pf]]Ffun" "(%p. [[f p]]F)"])
apply (simp add: LFP_fp semF_hasLFP_cpo)
apply (simp add: fold_order_prod_def)
apply (simp add: semF_subst_semFfun)

apply (simp add: continuous_semFfun)
apply (simp add: order_prod_def)
apply (drule_tac x="p" in spec)+

apply (simp add: semF_LFP_cpo)
done

(*  csp law  *)

lemma cspF_fp_induct_cpo_ref_right:
   "[| Pf = PNfun ;
       FPmode = CPOmode | FPmode = MIXmode ;
       Q <=F f p;
       !! p. f p <=F (Pf p)<<f |]
    ==> Q <=F $p"
by (simp add: cspF_fp_induct_cpo_ref_right_ALL)

lemmas cspF_fp_induct_cpo_right 
     = cspF_fp_induct_cpo_ref_right

(*=======================================================*
 |                                                       |
 |                    LFP <--> UFP                       |
 |                                                       |
 |                       MIXmode                         |
 |                                                       |
 *=======================================================*)

lemma semF_guarded_LFP_UFP:
  "[| Pf = PNfun ; guardedfun Pf |]
   ==> LFP [[Pf]]Ffun = UFP [[Pf]]Ffun"
by (simp add: semF_hasUFP_cms hasUFP_LFP_UFP)

(*----------- refinement -----------*)

(*** left ***)

lemma cspF_fp_induct_mix_ref_left_ALL:
   "[| Pf = PNfun ;
       guardedfun Pf ;
       FPmode = MIXmode ;
       f p <=F Q ;
       ALL p. (Pf p)<<f <=F f p |]
    ==> $p <=F Q"
apply (simp add: refF_semF)
apply (insert cms_fixpoint_induction_ref
       [of "[[Pf]]Ffun" "(%p. [[f p]]F)" "UFP [[Pf]]Ffun"])
apply (simp add: semF_guarded_LFP_UFP[THEN sym])
apply (simp add: LFP_fp semF_hasLFP_cpo)

apply (simp add: fold_order_prod_def)
apply (simp add: semF_subst_semFfun)
apply (simp add: mono_semFfun)
apply (simp add: contra_alpha_to_contst contraction_alpha_semFfun)
apply (simp add: order_prod_def)
apply (drule_tac x="p" in spec)+
apply (simp add: semF_LFP_cpo)
done

(*  csp law  *)

lemma cspF_fp_induct_mix_ref_left:
   "[| Pf = PNfun ;
       guardedfun Pf ;
       FPmode = MIXmode ;
       f p <=F Q ;
       !! p. (Pf p)<<f <=F f p |]
    ==> $p <=F Q"
by (simp add: cspF_fp_induct_mix_ref_left_ALL)

(*----------- equality -----------*)

(*** left ***)

lemma cspF_fp_induct_mix_eq_left_ALL:
   "[| Pf = PNfun ;
       guardedfun Pf ;
       FPmode = MIXmode ;
       f p =F Q ;
       ALL p. (Pf p)<<f =F f p |]
    ==> $p =F Q"
apply (simp add: eqF_semF)
apply (simp add: expand_fun_eq[THEN sym])
apply (simp add: semF_subst_semFfun)
apply (insert semF_LFP_fun_cpo[of Pf])
apply (simp add: semF_guarded_LFP_UFP)
apply (subgoal_tac "(%p. [[$p]]F) = (%p. [[f p]]F)")
apply (simp add: expand_fun_eq)

apply (rule hasUFP_unique_solution[of "[[Pf]]Ffun"])
apply (simp_all add: semF_hasUFP_cms)
apply (simp add: UFP_fp semF_hasUFP_cms)
done

(*  csp law  *)

lemma cspF_fp_induct_mix_eq_left:
   "[| Pf = PNfun ;
       guardedfun Pf ;
       FPmode = MIXmode ;
       f p =F Q ;
       !! p. (Pf p)<<f =F f p |]
    ==> $p =F Q"
by (simp add: cspF_fp_induct_mix_eq_left_ALL)

lemma cspF_fp_induct_mix_eq_right:
   "[| Pf = PNfun ;
       guardedfun Pf ;
       FPmode = MIXmode ;
       Q =F f p;
       !! p. f p =F (Pf p)<<f |]
    ==> Q =F $p"
apply (rule cspF_sym)
apply (rule cspF_fp_induct_mix_eq_left[of Pf f p Q])
apply (simp_all)
apply (rule cspF_sym)
apply (simp)
apply (rule cspF_sym)
apply (simp)
done

lemmas cspF_fp_induct_mix_left 
     = cspF_fp_induct_mix_ref_left cspF_fp_induct_mix_eq_left

lemmas cspF_fp_induct_mix_right 
     = cspF_fp_induct_cpo_ref_right cspF_fp_induct_mix_eq_right

(*=======================================================*
 |                                                       |
 |            mixing CPOmode and CMSmode                 |
 |                                                       |
 *=======================================================*)

lemma cspF_unwind:
   "[| Pf = PNfun ;
       FPmode = CPOmode
     | FPmode = CMSmode & guardedfun Pf
     | FPmode = MIXmode |]
     ==> $p =F Pf p"
apply (erule disjE)
apply (simp add: cspF_unwind_cpo)
apply (erule disjE)
apply (simp add: cspF_unwind_cms)
apply (simp add: cspF_unwind_cpo)
done

lemma cspF_fp_induct_ref_right:
   "[| Pf = PNfun ;
       FPmode = CPOmode
     | FPmode = CMSmode & guardedfun Pf
     | FPmode = MIXmode ;
       Q <=F f p;
       !! p. f p <=F (Pf p)<<f |]
    ==> Q <=F $p"
apply (erule disjE)
apply (simp add: cspF_fp_induct_cpo_right)
apply (erule disjE)
apply (simp add: cspF_fp_induct_cms_right)
apply (simp add: cspF_fp_induct_cpo_right)
done

lemma cspF_fp_induct_ref_left:
   "[| Pf = PNfun ;
       FPmode = CMSmode 
     | FPmode = MIXmode ;
       guardedfun Pf ;
       f p <=F Q ;
       !! p. (Pf p)<<f <=F f p |]
    ==> $p <=F Q"
apply (erule disjE)
apply (simp add: cspF_fp_induct_cms_left)
apply (simp add: cspF_fp_induct_mix_left)
done

lemma cspF_fp_induct_eq_left:
   "[| Pf = PNfun ;
       FPmode = CMSmode 
     | FPmode = MIXmode ;
       guardedfun Pf ;
       f p =F Q ;
       !! p. (Pf p)<<f =F f p |]
    ==> $p =F Q"
apply (erule disjE)
apply (simp add: cspF_fp_induct_cms_left)
apply (simp add: cspF_fp_induct_mix_left)
done

lemma cspF_fp_induct_eq_right:
   "[| Pf = PNfun ;
       FPmode = CMSmode 
     | FPmode = MIXmode ;
       guardedfun Pf ;
       Q =F f p;
       !! p. f p =F (Pf p)<<f |]
    ==> Q =F $p"
apply (erule disjE)
apply (simp add: cspF_fp_induct_cms_right)
apply (simp add: cspF_fp_induct_mix_right)
done

(*** cpo and cms ***)

lemmas cspF_fp_induct_right = cspF_fp_induct_ref_right cspF_fp_induct_eq_right
lemmas cspF_fp_induct_left = cspF_fp_induct_ref_left cspF_fp_induct_eq_left

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end

lemma semF_hasLFP_cpo: 

  Pf = PNfun ==> [[Pf]]Ffun hasLFP

lemma semF_LFP_cpo: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode |]
  ==> [[$p]]F = LFP [[Pf]]Ffun p

lemma semF_LFP_fun_cpo: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode |]
  ==> (%p. [[$p]]F) = LFP [[Pf]]Ffun

lemma MF_fixed_point_cpo: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode |] ==> [[Pf]]Ffun MF = MF

lemma ALL_cspF_greatest_cpo: 

  [| Pf = PNfun; FPmode = CPOmode; ∀p. (Pf p) << f =F f p |] ==> ∀p. f p <=F $p

lemma cspF_greatest_cpo: 

  [| Pf = PNfun; FPmode = CPOmode; ∀p. (Pf p) << f =F f p |] ==> f p <=F $p

lemma ALL_cspF_unwind_cpo: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode |] ==> ∀p. $p =F Pf p

lemma cspF_unwind_cpo: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode |] ==> $p =F Pf p

lemma cspF_fp_induct_cpo_ref_right_ALL: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     ∀p. f p <=F (Pf p) << f |]
  ==> Q <=F $p

lemma cspF_fp_induct_cpo_ref_right: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p

lemmas cspF_fp_induct_cpo_right: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p

lemmas cspF_fp_induct_cpo_right: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p

lemma semF_guarded_LFP_UFP: 

  [| Pf = PNfun; guardedfun Pf |] ==> LFP [[Pf]]Ffun = UFP [[Pf]]Ffun

lemma cspF_fp_induct_mix_ref_left_ALL: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p <=F Q;
     ∀p. (Pf p) << f <=F f p |]
  ==> $p <=F Q

lemma cspF_fp_induct_mix_ref_left: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q

lemma cspF_fp_induct_mix_eq_left_ALL: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p =F Q;
     ∀p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemma cspF_fp_induct_mix_eq_left: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemma cspF_fp_induct_mix_eq_right: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemmas cspF_fp_induct_mix_left: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q
  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemmas cspF_fp_induct_mix_left: 

  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q
  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemmas cspF_fp_induct_mix_right: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p
  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemmas cspF_fp_induct_mix_right: 

  [| Pf = PNfun; FPmode = CPOmode ∨ FPmode = MIXmode; Q <=F f p;
     !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p
  [| Pf = PNfun; guardedfun Pf; FPmode = MIXmode; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemma cspF_unwind: 

  [| Pf = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf ∨ FPmode = MIXmode |]
  ==> $p =F Pf p

lemma cspF_fp_induct_ref_right: 

  [| Pf = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf ∨ FPmode = MIXmode;
     Q <=F f p; !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p

lemma cspF_fp_induct_ref_left: 

  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q

lemma cspF_fp_induct_eq_left: 

  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemma cspF_fp_induct_eq_right: 

  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemmas cspF_fp_induct_right: 

  [| Pf = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf ∨ FPmode = MIXmode;
     Q <=F f p; !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p
  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemmas cspF_fp_induct_right: 

  [| Pf = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf ∨ FPmode = MIXmode;
     Q <=F f p; !!p. f p <=F (Pf p) << f |]
  ==> Q <=F $p
  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; Q =F f p;
     !!p. f p =F (Pf p) << f |]
  ==> Q =F $p

lemmas cspF_fp_induct_left: 

  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q
  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q

lemmas cspF_fp_induct_left: 

  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p <=F Q;
     !!p. (Pf p) << f <=F f p |]
  ==> $p <=F Q
  [| Pf = PNfun; FPmode = CMSmode ∨ FPmode = MIXmode; guardedfun Pf; f p =F Q;
     !!p. (Pf p) << f =F f p |]
  ==> $p =F Q