Theory CSP_law_fp_cms

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_fp_cms = CSP_proc_cms:

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

         1. fixed point theory in Csp-Prover
         2.
         3.
         4. 

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

(*******************************
        nohide and guard
 *******************************)

lemma LET_IN_nohide_guard_lm:
      "(ALL C. (nohide ((LetD R) C))) & (ALL C. (guard ((LetD R) C)))
       --> R =F LET:Ufp (LetD R) IN (InP R)"
apply (induct_tac R)
apply (simp_all)
apply (intro allI impI)
apply (simp add: eqF_def)
apply (subgoal_tac "[[fun]]DF hasUFP")
apply (induct_tac fp_type)
apply (simp_all add: hasUFP_LFP_UFP)
apply (simp add: evalDF_Banach_thm)
done

lemma LET_IN_nohide_guard:
      "[| ALL C. (nohide ((LetD R) C)) ; ALL C. (guard ((LetD R) C)) |]
       ==> R =F LET:Ufp (LetD R) IN (InP R)"
by (simp add: LET_IN_nohide_guard_lm)

(*------------------*
 |      csp law     |
 *------------------*)

lemma LET_IN_cpo_cms:
      "[| ALL C. (nohide (df C)) ; ALL C. (guard (df C)) |]
       ==> LET:Lfp df IN P =F LET:Ufp df IN P"
apply (rule LET_IN_nohide_guard[of "LET:Lfp df IN P", simplified])
by (simp_all)

lemma LET_IN_cpo_cms_eq_left:
      "[| ALL C. (nohide (df C)) ; ALL C. (guard (df C)) |]
       ==> (LET:Lfp df IN P =F R) = (LET:Ufp df IN P =F R)"
apply (insert LET_IN_cpo_cms[of df P])
by (simp add: eqF_def)

lemma LET_IN_cpo_cms_eq_right:
      "[| ALL C. (nohide (df C)) ; ALL C. (guard (df C)) |]
       ==> (R =F LET:Lfp df IN P) = (R =F LET:Ufp df IN P)"
apply (insert LET_IN_cpo_cms[of df P])
by (simp add: eqF_def)

lemmas LET_IN_cpo_cms_eq = LET_IN_cpo_cms_eq_left LET_IN_cpo_cms_eq_right

lemma LET_IN_cpo_cms_ref_left:
      "[| ALL C. (nohide (df C)) ; ALL C. (guard (df C)) |]
       ==> (LET:Lfp df IN P <=F R) = (LET:Ufp df IN P <=F R)"
apply (insert LET_IN_cpo_cms[of df P])
by (simp add: eqF_def refF_def)

lemma LET_IN_cpo_cms_ref_right:
      "[| ALL C. (nohide (df C)) ; ALL C. (guard (df C)) |]
       ==> (R <=F LET:Lfp df IN P) = (R <=F LET:Ufp df IN P)"
apply (insert LET_IN_cpo_cms[of df P])
by (simp add: eqF_def refF_def)

lemmas LET_IN_cpo_cms_ref = LET_IN_cpo_cms_ref_left LET_IN_cpo_cms_ref_right

(*******************************
            check eq
 *******************************)

consts
  CHECKeq :: "('n,'a) procRC => ('m,'a) procRC =>
                 ('n => ('m,'a) proc) => bool"
                    ("/(2CHECK /_ )/(2=F /_ )/(2BY /_)" [50,50,50] 50)

defs
  CHECKeq_def : 
    "CHECK R1 =F R2 BY f12 ==
                    (ALL C. (nohide ((LetD R1) C))) &
                    (ALL C. (guard  ((LetD R1) C))) &
                    (ALL C. (nohide ((LetD R2) C))) &
                    (ALL C. (guard  ((LetD R2) C))) &
                    (LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12) 
                  =F LET:Ufp (LetD R2) IN (InP R2)) &
            (ALL C. LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12)
                 =F LET:Ufp (LetD R2) IN (f12 C))"

(*******************************
           check ref
 *******************************)

consts
  CHECKref :: "('n,'a) procRC => ('m,'a) procRC => 
                 ('n => ('m,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2<=F /_ )/(2BY /_)" [50,50,50] 50)

defs
  CHECKref_def : 
    "CHECK R1 <=F R2 BY f12 ==
                    (ALL C. (nohide ((LetD R1) C))) &
                    (ALL C. (guard  ((LetD R1) C))) &
                    (ALL C. (nohide ((LetD R2) C))) &
                    (ALL C. (guard  ((LetD R2) C))) &
                    (LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12)
                 <=F LET:Ufp (LetD R2) IN (InP R2))&
            (ALL C. LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12)
                <=F LET:Ufp (LetD R2) IN (f12 C))"

(*******************************
           check ref
 *******************************)

consts
  CHECKrev :: "('m,'a) procRC => ('n,'a) procRC => 
                 ('m => ('n,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2=>F /_ )/(2BY /_)" [50,50,50] 50)

defs
  CHECKrev_def : 
    "CHECK R1 =>F R2 BY f12 ==
                    (ALL C. (nohide ((LetD R1) C))) &
                    (ALL C. (guard  ((LetD R1) C))) &
                    (ALL C. (nohide ((LetD R2) C))) &
                    (ALL C. (guard  ((LetD R2) C))) &
                    (LET:Ufp (LetD R2) IN (InP R2)
                 <=F LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12)) &
            (ALL C. LET:Ufp (LetD R2) IN (f12 C)
                <=F LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12))"

(*------------------------------------*
 |              X-Symbols             |
 *------------------------------------*)

syntax (output)
  "_CHECKrefX" :: "('n,'a) procRC => ('m,'a) procRC => 
                   ('n => ('m,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2<=F /_ )/(2BY /_)" [50,50,50] 50)
  "_CHECKrevX" :: "('n,'a) procRC => ('m,'a) procRC => 
                   ('m => ('n,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2=>F /_ )/(2BY /_)" [50,50,50] 50)

syntax (xsymbols)
  "_CHECKrefX" :: "('n,'a) procRC => ('m,'a) procRC => 
                   ('n => ('m,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2\<sqsubseteq>F /_ )/(2BY /_)" [50,50,50] 50)
  "_CHECKrevX" :: "('n,'a) procRC => ('m,'a) procRC => 
                   ('m => ('n,'a) proc) => bool"
                   ("/(2CHECK /_ )/(2\<sqsupseteq>F /_ )/(2BY /_)" [50,50,50] 50)

translations
  "CHECK R1 \<sqsubseteq>F R2 BY f" == "CHECK R1 <=F R2 BY f"
  "CHECK R1 \<sqsupseteq>F R2 BY f" == "CHECK R1 =>F R2 BY f"

(*********************************************************
                        Lemmas
 *********************************************************)

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

lemma csp_unwind_Ufp:
  "[| !! C. nohide (df C) ; !! C. guard  (df C) |]
         ==> LET:Ufp df IN <C> =F LET:Ufp df IN df C"
apply (simp add: eqF_def)
apply (subgoal_tac "[[df]]DF hasUFP")
 apply (simp add: Proc_name_evalSF)
 apply (simp add: evalSF_evalDF)
 apply (insert UFP_is[of "[[df]]DF"], simp)
 apply (simp add: isUFP_def)
apply (simp add: evalDF_Banach_thm)
done

lemma csp_unwind:
  "[| !! C. nohide (df C) ; !! C. guard  (df C) |]
         ==> LET:fp df IN <C> =F LET:fp df IN df C"
apply (induct_tac fp)
apply (simp add: csp_unwind_Ufp)
apply (simp add: LET_IN_cpo_cms_eq)
apply (simp add: csp_unwind_Ufp)
done

(*----------------------------------------------------------*
 |                                                          |
 | Fixed point induction with check (CSP-Prover intro rule) |
 |                                                          |
 *----------------------------------------------------------*)

(*********************************************************
                 Fixpoint (equaity check)
 *********************************************************)

lemma csp_check_fp_induct_eq_Ufp:
  "CHECK (LET:Ufp df1 IN P1) =F (LET:Ufp df2 IN P2) BY f12 
       ==> LET:Ufp df1 IN P1 =F LET:Ufp df2 IN P2"
apply (simp add: CHECKeq_def)
apply (elim conjE)
apply (simp add: eqF_def)
apply (simp add: RewriteBy_compo)
apply (simp add: evalSF_evalDF)

apply (subgoal_tac "[[df1]]DF hasUFP & [[df2]]DF hasUFP")
 apply (drule sym, simp)
 apply (subgoal_tac "[[f12]]DF (UFP [[df2]]DF) = UFP [[df1]]DF", simp)
 apply (simp add: expand_fun_eq[THEN sym])
 apply (insert UFP_is[of "[[df1]]DF"], simp)
 apply (simp add: isUFP_def)
 apply (elim conjE)
 apply (drule_tac x="[[f12]]DF (UFP [[df2]]DF)" in spec)
 apply (simp)
apply (simp add: evalDF_Banach_thm)
done

lemma csp_check_fp_induct_eq:
  "CHECK (LET:Ufp df1 IN P1) =F (LET:Ufp df2 IN P2) BY f12 
       ==> LET:fp df1 IN P1 =F LET:fp df2 IN P2"
apply (insert csp_check_fp_induct_eq_Ufp[of df1 P1 df2 P2 f12])
apply (induct_tac fp)
apply (simp)
apply (simp add: LET_IN_cpo_cms_eq CHECKeq_def)
done

(*********************************************************
                 Fixpoint (refinment check)
                    f12 : df1 --> df2
 *********************************************************)

lemma csp_check_fp_induct_ref_Ufp:
  "CHECK (LET:Ufp df1 IN P1) <=F (LET:Ufp df2 IN P2) BY f12
       ==> LET:Ufp df1 IN P1 <=F LET:Ufp df2 IN P2"
apply (simp add: CHECKref_def)
apply (elim conjE)
apply (simp add: refF_def)
apply (simp add: RewriteBy_compo)
apply (simp add: evalSF_evalDF)

apply (subgoal_tac "[[df1]]DF hasUFP & [[df2]]DF hasUFP")
 apply (subgoal_tac "[[P1]]SF ([[f12]]DF (UFP [[df2]]DF)) 
                  <= [[P1]]SF (UFP [[df1]]DF)", simp)
 apply (subgoal_tac "[[f12]]DF (UFP [[df2]]DF) <= UFP [[df1]]DF")
 apply (simp add: evalSF_mono)
 apply (fold order_prod_def)

 apply (insert UFP_is[of "[[df1]]DF"], simp)
 apply (simp add: isUFP_def)

 apply (rule cms_fixpoint_induction_ref[of "[[df1]]DF"])
 apply (simp_all add: evalDF_contraction_half contra_alpha_to_contst
                      evalDF_mono_fun)
apply (simp add: evalDF_Banach_thm)
done

lemma csp_check_fp_induct_ref:
  "CHECK (LET:Ufp df1 IN P1) <=F (LET:Ufp df2 IN P2) BY f12
       ==> LET:fp df1 IN P1 <=F LET:fp df2 IN P2"
apply (insert csp_check_fp_induct_ref_Ufp[of df1 P1 df2 P2 f12])
apply (induct_tac fp)
apply (simp)
apply (simp add: LET_IN_cpo_cms_ref CHECKref_def)
done

(*********************************************************
             Fixpoint (reverse refinment check)
                    f12 : df1 --> df2
 *********************************************************)

lemma csp_check_fp_induct_rev_Ufp:
  "CHECK (LET:Ufp df1 IN P1) =>F (LET:Ufp df2 IN P2) BY f12
       ==> LET:Ufp df2 IN P2 <=F LET:Ufp df1 IN P1"
apply (simp add: CHECKrev_def)
apply (elim conjE)
apply (simp add: refF_def)
apply (simp add: RewriteBy_compo)
apply (simp add: evalSF_evalDF)

apply (subgoal_tac "[[df1]]DF hasUFP & [[df2]]DF hasUFP")
 apply (subgoal_tac "[[P1]]SF (UFP [[df1]]DF)
                  <= [[P1]]SF ([[f12]]DF (UFP [[df2]]DF))", simp)
 apply (subgoal_tac "UFP [[df1]]DF <= [[f12]]DF (UFP [[df2]]DF)")
 apply (simp add: evalSF_mono)
 apply (fold order_prod_def)

 apply (insert UFP_is[of "[[df1]]DF"], simp)
 apply (simp add: isUFP_def)

 apply (rule cms_fixpoint_induction_rev[of "[[df1]]DF"])
 apply (simp_all add: evalDF_contraction_half contra_alpha_to_contst
                      evalDF_mono_fun)
apply (simp add: evalDF_Banach_thm)
done

lemma csp_check_fp_induct_rev:
  "CHECK (LET:Ufp df1 IN P1) =>F (LET:Ufp df2 IN P2) BY f12
       ==> LET:fp df2 IN P2 <=F LET:fp df1 IN P1"
apply (insert csp_check_fp_induct_rev_Ufp[of df1 P1 df2 P2 f12])
apply (induct_tac fp)
apply (simp)
apply (simp add: LET_IN_cpo_cms_ref CHECKrev_def)
done

lemmas csp_check_fp_induct = csp_check_fp_induct_eq csp_check_fp_induct_ref

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

(*** unfold fixpoint for equality ***)

lemma csp_check_eq:
  "[| !!C. nohide ((LetD R1) C) ; !!C. guard ((LetD R1) C) ;
      !!C. nohide ((LetD R2) C) ; !!C. guard ((LetD R2) C) ;
      (LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12) =F 
       LET:Ufp (LetD R2) IN (InP R2)) ;
      !!C. LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12) =F
           LET:Ufp (LetD R2) IN (f12 C) |]
    ==> CHECK R1 =F R2 BY f12"
by (simp add: CHECKeq_def)

(*** unfold fixpoint for refinement ***)

lemma csp_check_ref:
  "[| !!C. nohide ((LetD R1) C) ; !!C. guard ((LetD R1) C) ;
      !!C. nohide ((LetD R2) C) ; !!C. guard ((LetD R2) C) ;
      (LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12) <=F 
       LET:Ufp (LetD R2) IN (InP R2)) ;
      !!C. LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12) <=F
           LET:Ufp (LetD R2) IN (f12 C) |]
    ==> CHECK R1 <=F R2 BY f12"
by (simp add: CHECKref_def)

(*** unfold fixpoint for reverse refinement ***)

lemma csp_check_rev:
  "[| !!C. nohide ((LetD R1) C) ; !!C. guard ((LetD R1) C) ;
      !!C. nohide ((LetD R2) C) ; !!C. guard ((LetD R2) C) ;
     (LET:Ufp (LetD R2) IN (InP R2) <=F 
      LET:Ufp (LetD R2) IN (Rewrite (InP R1) By f12)) ;
      !!C. LET:Ufp (LetD R2) IN (f12 C) <=F 
           LET:Ufp (LetD R2) IN (Rewrite (LetD R1 C) By f12) |]
    ==> CHECK R1 =>F R2 BY f12"
by (simp add: CHECKrev_def)

lemmas csp_check = csp_check_eq csp_check_ref csp_check_rev

(*-------------------------------------------------------*
 |                                                       |
 |     Fixed point induction (CSP-Prover intro rule)     |
 |                                                       |
 *-------------------------------------------------------*)

(*** equal ***)

lemma csp_fp_induct_eq:
  "[| !!C. nohide (df1 C) ; !!C. guard (df1 C) ;
      !!C. nohide (df2 C) ; !!C. guard (df2 C) ;
           LET:Ufp df2 IN (Rewrite P1 By f12) =F LET:Ufp df2 IN P2 ;
      !!C. LET:Ufp df2 IN (Rewrite (df1 C) By f12) =F LET:Ufp df2 IN (f12 C) |]
    ==> LET:fp df1 IN P1 =F LET:fp df2 IN P2"
apply (rule csp_check_fp_induct_eq[of _ _ _ _f12])
by (simp add: csp_check_eq)

(*** refinement ***)

lemma csp_fp_induct_ref:
  "[| !!C. nohide (df1 C) ; !!C. guard (df1 C) ;
      !!C. nohide (df2 C) ; !!C. guard (df2 C) ;
           LET:Ufp df2 IN (Rewrite P1 By f12) <=F LET:Ufp df2 IN P2 ;
      !!C. LET:Ufp df2 IN (Rewrite (df1 C) By f12) <=F LET:Ufp df2 IN (f12 C) |]
    ==> LET:fp df1 IN P1 <=F LET:fp df2 IN P2"
apply (rule csp_check_fp_induct_ref[of _ _ _ _ f12])
by (simp add: csp_check_ref)

(*** reverse refinement ***)

lemma csp_fp_induct_rev:
  "[| !!C. nohide (df1 C) ; !!C. guard (df1 C) ;
      !!C. nohide (df2 C) ; !!C. guard (df2 C) ;
           LET:Ufp df1 IN P1 <=F LET:Ufp df1 IN (Rewrite P2 By f21) ;
      !!C. LET:Ufp df1 IN (f21 C) <=F LET:Ufp df1 IN (Rewrite (df2 C) By f21) |]
    ==> LET:fp df1 IN P1 <=F LET:fp df2 IN P2"
apply (rule csp_check_fp_induct_rev[of _ _ _ _ f21])
by (simp add: csp_check_rev)

lemmas csp_fp_induct_cms = csp_fp_induct_eq csp_fp_induct_ref

end