Theory CSP_law_fp_cpo

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               February 2005               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_fp_cpo = CSP_proc_cpo:

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

         1. cpo fixed point theory in CSP-Prover
         2.
         3.
         4. 

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

(*******************************
         check rev (Lfp)
 *******************************)

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

defs
  CHECKcpo_def : 
    "CHECKcpo R1 =>F R2 BY f12 ==
                    (LET:Lfp (LetD R2) IN (InP R2)
                 <=F LET:Lfp (LetD R2) IN (Rewrite (InP R1) By f12)) &
            (ALL C. LET:Lfp (LetD R2) IN (f12 C)
                <=F LET:Lfp (LetD R2) IN (Rewrite (LetD R1 C) By f12))"

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

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

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

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


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

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

lemma csp_unwind_cpo:
  "LET:Lfp df IN <C> =F LET:Lfp df IN df C"
apply (simp add: eqF_def)
apply (subgoal_tac "[[df]]DF hasLFP")
 apply (simp add: Proc_name_evalSF)
 apply (simp add: evalSF_evalDF)
 apply (insert LFP_is[of "[[df]]DF"], simp)
 apply (simp add: isLFP_def)
apply (simp add: evalDF_Tarski_thm)
done

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

lemma csp_check_fp_induct_cpo:
  "CHECKcpo (LET:Lfp df1 IN P1) =>F (LET:Lfp df2 IN P2) BY f12
          ==> LET:Lfp df2 IN P2 <=F LET:Lfp df1 IN P1"
apply (simp add: CHECKcpo_def)
apply (elim conjE)
apply (simp add: refF_def)
apply (simp add: RewriteBy_compo)
apply (simp add: evalSF_evalDF)

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

 apply (insert LFP_is[of "[[df1]]DF"], simp)
 apply (simp add: isLFP_def)

 apply (rule cpo_fixpoint_induction_rev[of "[[df1]]DF"])
 apply (simp_all add: evalDF_continuous)
apply (simp add: evalDF_Tarski_thm)
done

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

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

lemma csp_check_cpo:
  "[| (LET:Lfp (LetD R2) IN (InP R2) <=F 
       LET:Lfp (LetD R2) IN (Rewrite (InP R1) By f12)) ;
      !!C. LET:Lfp (LetD R2) IN (f12 C) <=F 
           LET:Lfp (LetD R2) IN (Rewrite (LetD R1 C) By f12) |]
    ==> CHECKcpo R1 =>F R2 BY f12"
by (simp add: CHECKcpo_def)

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

(*** reverse refinement : Lfp ***)

lemma csp_fp_induct_cpo:
  "[|      LET:Lfp df1 IN P1 <=F LET:Lfp df1 IN (Rewrite P2 By f21) ;
      !!C. LET:Lfp df1 IN (f21 C) <=F LET:Lfp df1 IN (Rewrite (df2 C) By f21) |]
    ==> LET:Lfp df1 IN P1 <=F LET:Lfp df2 IN P2"
apply (rule csp_check_fp_induct_cpo[of _ _ _ _ f21])
by (simp add: csp_check_cpo)

end