Theory CPO_set

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

theory CPO_set
imports CPO_prod
begin

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

         1. Bool is CPO
         2. ==> Sets are CPO.
         3. 
         4. 

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

(********************************************************** 
              def: bot in bool
 **********************************************************)

instance bool :: bot0
apply (intro_classes)
done

defs (overloaded)
  bool_Bot_def : "Bot == False"

(*
     For Isabelle 2007

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

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

(************************************************************
                   Bool bot ==> bot
 ************************************************************)

(*** bool Bot ***)

lemma bool_Bot:
  "ALL (X::(bool)). Bot <= X"
apply (simp add: bool_Bot_def)
apply (simp add: le_bool_def)
done

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

(*****************************
       bool bot => bot
 *****************************)

instance bool :: bot
apply (intro_classes)
by (simp add: bool_Bot)

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

(*** set Bot ***)

lemma set_Bot:
  "ALL (X::('a set)). Bot <= X"
by (simp add: prod_Bot)

(************************************************************
                      Bool : CPO
 ************************************************************)

(*** bool directed decompo ***)

lemma bool_cpo_lm:
  "directed (Bs::(bool) set) ==> Bs hasLUB"
apply (simp add: hasLUB_def)
apply (rule_tac x="(EX b:Bs. b)" in exI)
apply (simp add: isLUB_def isUB_def)
apply (simp add: le_bool_def)
by (auto)

(*****************************
          Bool : CPO
 *****************************)

instance bool :: cpo
apply (intro_classes)
by (simp add: bool_cpo_lm)

(************************************************************
                      Bool : CPO_BOT
 ************************************************************)

instance bool :: cpo_bot
by (intro_classes)

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

lemma set_cpo:
  "directed (Xs::('a set) set) ==> Xs hasLUB"
by (simp add: complete_cpo)

(* because (bool::cpo) and ("fun" :: (type,cpo) cpo) *)

(************************************************************
                      Set : CPO_bot
 ************************************************************)

lemma set_bot:
  "Bot <= (x::'a set)"
by (simp add: bottom_bot)

(* because (bool::bot) and ("fun" :: (type,bot) bot) *)

end