Theory Proc_name_cpo

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

theory Proc_name_cpo = Proc_name + Domain_SF_prod_cpo:

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

         1. [[<C>]]SF : continuous
         2.
         3. 
         4. 

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

(*** Proc_name_evalSF_continuous ***)

lemma Proc_name_evalSF_continuous: "continuous [[<C>]]SF"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (insert complete_cpo_lm)
apply (drule_tac x="X" in spec, simp)
apply (simp add: hasLUB_def)
apply (erule exE)
apply (rule_tac x="x" in exI, simp)

apply (simp add: prod_LUB_decompo)
apply (drule_tac x="C" in spec)
apply (simp add: proj_fun_def)
apply (simp add: Proc_name_evalSF)
apply (subgoal_tac "[[<C>]]SF ` X = (%x. x C) ` X", simp)
by (auto simp add: image_iff Proc_name_evalSF)

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

end