Theory Domain_SF_prod_cms

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

theory Domain_SF_prod_cms = Domain_SF_prod + Domain_SF_cms + RS_prod:

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

         1. 
         2. 
         3. 
         4. 

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

(**************************************************************)
(*                                                            *)
(*  It has already proven that ('i,'a) dom_SF_prod is a CMS   *)
(*  because dom_SF is a CMS and "=>" preserves CMS.           *)
(*                                                            *)
(*    instance dom_SF :: (type) cms_rs  in Domain_SF.thy      *)
(*    instance => :: (type,cms_rs) cms_rs in RS_prod.thy      *)
(*                                                            *)
(*  This can be confirmed as the following lemmas.            *)
(*                                                            *)
(**************************************************************)

lemma LimitSF_prod_Limit:
  "cauchy (SFps::(('i,'a) domSF_prod) infinite_seq) ==> SFps convergeTo Limit SFps"
by (simp add: Limit_is)
   (* see "Limit_is" in RS.thy *)

(************************************************************
             continuity lemma for refinement
 ************************************************************)

lemma continuou_rs_RefSF_prod: "continuous_rs (RefSF_prod SEp)"
apply (simp add: RefSF_prod_def)
apply (simp add: order_prod_def)

apply (insert prod_continuous_rs[of "(%i. RefSF (SEp i))"])
apply (simp add: continuous_rs_RefSF)
by (simp add: RefSF_def)

(************************************************************
         continuity lemma for (Reverse) refinement
 ************************************************************)

lemma continuou_rs_RevSF_prod: "continuous_rs (RevSF_prod SEp)"
apply (simp add: RevSF_prod_def)
apply (simp add: order_prod_def)

apply (insert prod_continuous_rs[of "(%i. RevSF (SEp i))"])
apply (simp add: continuous_rs_RevSF)
by (simp add: RevSF_def)

(************************************************************
          Metric Fixed Point Induction for refinement
 ************************************************************)

theorem cms_fixpoint_induction_ref:
  "[| constructive_rs f ; mono f ; SEp <= f SEp ; SFp = f SFp |]
   ==> (SEp::('i,'a) domSF_prod) <= SFp"
apply (insert cms_fixpoint_induction[of "RefSF_prod SEp" SEp f])
apply (simp add: continuou_rs_RefSF_prod)
apply (simp add: RefSF_prod_def)

apply (subgoal_tac "inductivefun (op <= SEp) f")
apply (insert UFP_is[of f], simp)
apply (simp add: isUFP_def)

      (* inductiveness *)
apply (simp add: inductivefun_def)
apply (intro allI impI)
apply (simp add: mono_def)
apply (drule_tac x="SEp" in spec)
apply (drule_tac x="x" in spec)
apply (simp)
done

(************************************************************
        Metric Fixed Point Induction for refinement (rev)
 ************************************************************)

theorem cms_fixpoint_induction_rev:
  "[| constructive_rs f ; mono f ; f SEp <= SEp ; SFp = f SFp |]
   ==> (SFp::('i,'a) domSF_prod) <= SEp"
apply (insert cms_fixpoint_induction[of "RevSF_prod SEp" SEp f])
apply (simp add: continuou_rs_RevSF_prod)
apply (simp add: RevSF_prod_def)

apply (subgoal_tac "inductivefun (%SFp. SFp <= SEp) f")
apply (insert UFP_is[of f], simp)
apply (simp add: isUFP_def)

      (* inductiveness *)
apply (simp add: inductivefun_def)
apply (intro allI impI)
apply (simp add: mono_def)
apply (drule_tac x="x" in spec)
apply (drule_tac x="SEp" in spec)
apply (simp)
done

end