Theory CPO_set

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |                 August 2004               |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CPO_set = CPO:

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

         1. Sets are CPO.
         2. 
         3. 
         4. 

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

(********************************************************** 
              def: prod of bot
 **********************************************************)

instance set :: (type) bot0
apply (intro_classes)
done

defs (overloaded)
  set_Bot_def : "Bot == {}"

(************************************************************
                   Set bot ==> bot
 ************************************************************)

(*** set Bot ***)

lemma set_Bot:
  "ALL (X::('a set)). Bot <= X"
apply (simp add: set_Bot_def)
done

(*****************************
       Set bot => bot
 *****************************)

instance set :: (type) bot
apply (intro_classes)
by (simp add: set_Bot)

(************************************************************
                      Set : CPO
 ************************************************************)

(*** set directed decompo ***)

lemma set_cpo_lm:
  "directed (Xs::('a set) set) ==> Xs hasLUB"
apply (simp add: hasLUB_def)
apply (rule_tac x="Union Xs" in exI)
apply (simp add: isLUB_def isUB_def)
by (auto)

(*****************************
          Set : CPO
 *****************************)

instance set :: (type) cpo
apply (intro_classes)
by (simp add: set_cpo_lm)

(************************************************************
                      Set : CPO_BOT
 ************************************************************)

instance set :: (type) cpo_bot
by (intro_classes)

end