Theory DIV_cpo

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

theory DIV_cpo = DIV + Domain_SF_prod_cpo:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

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

         1. [[DIV]]T : continuous
         2. [[DIV]]F : continuous
         3. 
         4. 

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

(*** DIV_evalT_continuous ***)

lemma DIV_evalT_continuous: "continuous [[DIV]]T"
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 (elim exE)
apply (rule_tac x="x" in exI, simp)
apply (simp add: evalT_def)
by (simp add: image_def isLUB_def isUB_def)

(*** DIV_evalF_continuous ***)

lemma DIV_evalF_continuous: "continuous [[DIV]]F"
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 (elim exE)
apply (rule_tac x="x" in exI, simp)
apply (simp add: evalF_def)
by (auto simp add: isLUB_def isUB_def directed_def)

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

declare disj_not1      [simp]
declare not_None_eq    [simp]

end