Theory Domain_SF_prod_cpo

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

theory Domain_SF_prod_cpo = Domain_SF_cpo + Domain_SF_prod + CPO_prod:

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

         1. ('i,'a) dom_SF_prod is a CPO.
         2. 
         3. 
         4. 

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

(**************************************************************)
(*                                                            *)
(*  It has already proven that ('i,'a) dom_SF_prod is a CPO   *)
(*  because dom_SF is a CPO and "=>" preserves CPO.           *)
(*                                                            *)
(*  instance dom_SF :: (type) cpo_bot in Domain_SF_cpo.thy    *)
(*  instance fun :: (type,cpo_bot) cpo_bot in CPO_prod.thy    *)
(*                                                            *)
(**************************************************************)

(*----------------------------------------------------------*
 |                                                          |
 |         Fixed point induction for refinement             |
 |                                                          |
 *----------------------------------------------------------*)

(************************************************************
         admissibility lemma for refinement for cpo
 ************************************************************)

lemma RevSF_prod_admissible: "admissible (RevSF_prod SEp)"
apply (simp add: RevSF_prod_def)
apply (simp add: admissible_def)
by (auto simp add: LUB_least complete_cpo)

(*** Bot ***)

lemma RevSF_prod_Bot: "RevSF_prod SEp Bot"
by (simp add: RevSF_prod_def bottom_bot)

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

theorem cpo_fixpoint_induction_rev:
  "[| continuous f ; f SEp <= SEp |] 
   ==> LFP f <= (SEp::('i,'a) domSF_prod)"
apply (insert cpo_fixpoint_induction[of "(RevSF_prod SEp)" f])
apply (simp add: RevSF_prod_admissible RevSF_prod_Bot)
apply (subgoal_tac "inductivefun (RevSF_prod SEp) f")
apply (simp add: RevSF_prod_def)

      (* inductiveness *)
apply (simp add: inductivefun_def RevSF_prod_def)
apply (intro allI impI)
apply (insert continuous_mono[of f])
apply (simp add: mono_def)
apply (drule_tac x="x" in spec)
apply (drule_tac x="SEp" in spec)
by (simp)

(*** EX version ***)

theorem cpo_fixpoint_induction_rev_EX:
  "[| continuous f ; f SEp <= SEp ; SFp isLFP f |]
   ==> SFp <= (SEp::('i,'a) domSF_prod)"
apply (insert cpo_fixpoint_induction_rev[of f SEp])
by (auto simp add: isLFP_LFP)

end