Theory Ext_pre_choice_cpo

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

theory Ext_pre_choice_cpo = Ext_pre_choice + 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]

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

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

         1. [[? :X -> Pf]]T : continuous
         2. [[? :X -> Pf]]F : continuous
         3. 
         4. 

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

(*** Ext_pre_choice_evalT_continuous ***)

lemma Ext_pre_choice_evalT_continuous:
 "ALL a. continuous [[Pf a]]T ==> continuous [[? :X -> Pf]]T"
apply (simp add: continuous_iff)
apply (intro allI impI)

apply (subgoal_tac "Xa ~= {}")
apply (erule exchange_forall_orderE)
apply (drule_tac x="Xa" in spec)
apply (simp add: isLUB_UnionT)

apply (rule_tac x="LUB Xa" in exI)
apply (rule conjI)
apply (rule eq_iffI)

(* <= *)
 apply (rule)
 apply (simp add: memT_UnionT)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, fast)
 apply (elim conjE exE)
 apply (simp add: memT_UnionT)
 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)

 apply (subgoal_tac "LUB Xa = x", simp)
 apply (simp add: memT_UnionT)
 apply (erule bexE)

 apply (rule_tac x="xa" in bexI)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)

(* => *)
 apply (rule)
 apply (simp add: memT_UnionT)
 apply (erule bexE)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule disjI2)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI, simp)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB Xa = xa", simp)
 apply (simp add: memT_UnionT)
 apply (rule_tac x="x" in bexI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (simp add: isLUB_LUB)

by (simp add: directed_def)

(*** Ext_pre_choice_evalF_continuous ***)

lemma Ext_pre_choice_evalF_continuous:
 "ALL a. continuous [[Pf a]]F ==> continuous [[? :X -> Pf]]F"
apply (simp add: continuous_iff)
apply (intro allI impI)

apply (subgoal_tac "Xa ~= {}")
apply (erule exchange_forall_orderE)
apply (drule_tac x="Xa" in spec)
apply (simp add: isLUB_UnionF)

apply (rule_tac x="LUB Xa" in exI)
apply (rule conjI)
apply (rule eq_iffI)

(* <= *)
 apply (rule)
 apply (simp add: memF_UnionF)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, fast)
 apply (elim conjE exE)
 apply (simp add: memF_UnionF)
 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)

 apply (subgoal_tac "LUB Xa = x", simp)
 apply (simp add: memF_UnionF)
 apply (erule bexE)

 apply (rule_tac x="xa" in bexI)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)

(* => *)
 apply (rule)
 apply (simp add: memF_UnionF)
 apply (erule bexE)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule disjI2)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI, simp)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB Xa = xa", simp)
 apply (simp add: memF_UnionF)
 apply (rule_tac x="x" in bexI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (simp add: isLUB_LUB)

by (simp add: directed_def)

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]
declare disj_not1      [simp]
declare not_None_eq    [simp]

end