16697

1 
(* Title: HOLCF/Pcpodef.thy


2 
ID: $Id$


3 
Author: Brian Huffman


4 
*)


5 


6 
header {* Subtypes of pcpos *}


7 


8 
theory Pcpodef


9 
imports Adm

23152

10 
uses ("Tools/pcpodef_package.ML")

16697

11 
begin


12 


13 
subsection {* Proving a subtype is a partial order *}


14 


15 
text {*


16 
A subtype of a partial order is itself a partial order,


17 
if the ordering is defined in the standard way.


18 
*}


19 


20 
theorem typedef_po:


21 
fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord"


22 
assumes type: "type_definition Rep Abs A"


23 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


24 
shows "OFCLASS('b, po_class)"


25 
apply (intro_classes, unfold less)


26 
apply (rule refl_less)

16918

27 
apply (rule type_definition.Rep_inject [OF type, THEN iffD1])


28 
apply (erule (1) antisym_less)


29 
apply (erule (1) trans_less)

16697

30 
done


31 


32 

17812

33 
subsection {* Proving a subtype is chainfinite *}


34 


35 
lemma monofun_Rep:


36 
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


37 
shows "monofun Rep"


38 
by (rule monofunI, unfold less)


39 


40 
lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]


41 
lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]


42 


43 
theorem typedef_chfin:


44 
fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"


45 
assumes type: "type_definition Rep Abs A"


46 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


47 
shows "OFCLASS('b, chfin_class)"


48 
apply (intro_classes, clarify)


49 
apply (drule ch2ch_Rep [OF less])


50 
apply (drule chfin [rule_format])


51 
apply (unfold max_in_chain_def)


52 
apply (simp add: type_definition.Rep_inject [OF type])


53 
done


54 


55 

16697

56 
subsection {* Proving a subtype is complete *}


57 


58 
text {*


59 
A subtype of a cpo is itself a cpo if the ordering is


60 
defined in the standard way, and the defining subset


61 
is closed with respect to limits of chains. A set is


62 
closed if and only if membership in the set is an


63 
admissible predicate.


64 
*}


65 

16918

66 
lemma Abs_inverse_lub_Rep:

16697

67 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"


68 
assumes type: "type_definition Rep Abs A"


69 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


70 
and adm: "adm (\<lambda>x. x \<in> A)"

16918

71 
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"


72 
apply (rule type_definition.Abs_inverse [OF type])


73 
apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])

16697

74 
apply (rule type_definition.Rep [OF type])


75 
done


76 

16918

77 
theorem typedef_lub:

16697

78 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"


79 
assumes type: "type_definition Rep Abs A"


80 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


81 
and adm: "adm (\<lambda>x. x \<in> A)"

16918

82 
shows "chain S \<Longrightarrow> range S << Abs (\<Squnion>i. Rep (S i))"


83 
apply (frule ch2ch_Rep [OF less])

16697

84 
apply (rule is_lubI)


85 
apply (rule ub_rangeI)

16918

86 
apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])


87 
apply (erule is_ub_thelub)


88 
apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])


89 
apply (erule is_lub_thelub)


90 
apply (erule ub2ub_Rep [OF less])

16697

91 
done


92 

16918

93 
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]


94 

16697

95 
theorem typedef_cpo:


96 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"


97 
assumes type: "type_definition Rep Abs A"


98 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


99 
and adm: "adm (\<lambda>x. x \<in> A)"


100 
shows "OFCLASS('b, cpo_class)"

16918

101 
proof


102 
fix S::"nat \<Rightarrow> 'b" assume "chain S"


103 
hence "range S << Abs (\<Squnion>i. Rep (S i))"


104 
by (rule typedef_lub [OF type less adm])


105 
thus "\<exists>x. range S << x" ..


106 
qed

16697

107 


108 


109 
subsubsection {* Continuity of @{term Rep} and @{term Abs} *}


110 


111 
text {* For any subcpo, the @{term Rep} function is continuous. *}


112 


113 
theorem typedef_cont_Rep:


114 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"


115 
assumes type: "type_definition Rep Abs A"


116 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


117 
and adm: "adm (\<lambda>x. x \<in> A)"


118 
shows "cont Rep"


119 
apply (rule contI)

16918

120 
apply (simp only: typedef_thelub [OF type less adm])


121 
apply (simp only: Abs_inverse_lub_Rep [OF type less adm])

16697

122 
apply (rule thelubE [OF _ refl])

16918

123 
apply (erule ch2ch_Rep [OF less])

16697

124 
done


125 


126 
text {*


127 
For a subcpo, we can make the @{term Abs} function continuous


128 
only if we restrict its domain to the defining subset by


129 
composing it with another continuous function.


130 
*}


131 

16918

132 
theorem typedef_is_lubI:


133 
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


134 
shows "range (\<lambda>i. Rep (S i)) << Rep x \<Longrightarrow> range S << x"


135 
apply (rule is_lubI)


136 
apply (rule ub_rangeI)


137 
apply (subst less)


138 
apply (erule is_ub_lub)


139 
apply (subst less)


140 
apply (erule is_lub_lub)


141 
apply (erule ub2ub_Rep [OF less])


142 
done


143 

16697

144 
theorem typedef_cont_Abs:


145 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"


146 
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"


147 
assumes type: "type_definition Rep Abs A"


148 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"

16918

149 
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)

16697

150 
and f_in_A: "\<And>x. f x \<in> A"


151 
and cont_f: "cont f"


152 
shows "cont (\<lambda>x. Abs (f x))"


153 
apply (rule contI)

16918

154 
apply (rule typedef_is_lubI [OF less])


155 
apply (simp only: type_definition.Abs_inverse [OF type f_in_A])


156 
apply (erule cont_f [THEN contE])

16697

157 
done


158 

17833

159 
subsection {* Proving subtype elements are compact *}


160 


161 
theorem typedef_compact:


162 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"


163 
assumes type: "type_definition Rep Abs A"


164 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


165 
and adm: "adm (\<lambda>x. x \<in> A)"


166 
shows "compact (Rep k) \<Longrightarrow> compact k"


167 
proof (unfold compact_def)


168 
have cont_Rep: "cont Rep"


169 
by (rule typedef_cont_Rep [OF type less adm])


170 
assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"


171 
with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)


172 
thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)


173 
qed


174 

16697

175 
subsection {* Proving a subtype is pointed *}


176 


177 
text {*


178 
A subtype of a cpo has a least element if and only if


179 
the defining subset has a least element.


180 
*}


181 

16918

182 
theorem typedef_pcpo_generic:

16697

183 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"


184 
assumes type: "type_definition Rep Abs A"


185 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


186 
and z_in_A: "z \<in> A"


187 
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"


188 
shows "OFCLASS('b, pcpo_class)"


189 
apply (intro_classes)


190 
apply (rule_tac x="Abs z" in exI, rule allI)


191 
apply (unfold less)


192 
apply (subst type_definition.Abs_inverse [OF type z_in_A])


193 
apply (rule z_least [OF type_definition.Rep [OF type]])


194 
done


195 


196 
text {*


197 
As a special case, a subtype of a pcpo has a least element


198 
if the defining subset contains @{term \<bottom>}.


199 
*}


200 

16918

201 
theorem typedef_pcpo:

16697

202 
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"


203 
assumes type: "type_definition Rep Abs A"


204 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


205 
and UU_in_A: "\<bottom> \<in> A"


206 
shows "OFCLASS('b, pcpo_class)"

16918

207 
by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)

16697

208 


209 
subsubsection {* Strictness of @{term Rep} and @{term Abs} *}


210 


211 
text {*


212 
For a subpcpo where @{term \<bottom>} is a member of the defining


213 
subset, @{term Rep} and @{term Abs} are both strict.


214 
*}


215 


216 
theorem typedef_Abs_strict:


217 
assumes type: "type_definition Rep Abs A"


218 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


219 
and UU_in_A: "\<bottom> \<in> A"


220 
shows "Abs \<bottom> = \<bottom>"


221 
apply (rule UU_I, unfold less)


222 
apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])


223 
done


224 


225 
theorem typedef_Rep_strict:


226 
assumes type: "type_definition Rep Abs A"


227 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


228 
and UU_in_A: "\<bottom> \<in> A"


229 
shows "Rep \<bottom> = \<bottom>"


230 
apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])


231 
apply (rule type_definition.Abs_inverse [OF type UU_in_A])


232 
done


233 


234 
theorem typedef_Abs_defined:


235 
assumes type: "type_definition Rep Abs A"


236 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


237 
and UU_in_A: "\<bottom> \<in> A"


238 
shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"


239 
apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])


240 
apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)


241 
done


242 


243 
theorem typedef_Rep_defined:


244 
assumes type: "type_definition Rep Abs A"


245 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


246 
and UU_in_A: "\<bottom> \<in> A"


247 
shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"


248 
apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])


249 
apply (simp add: type_definition.Rep_inject [OF type])


250 
done


251 

19519

252 
subsection {* Proving a subtype is flat *}


253 


254 
theorem typedef_flat:


255 
fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"


256 
assumes type: "type_definition Rep Abs A"


257 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"


258 
and UU_in_A: "\<bottom> \<in> A"


259 
shows "OFCLASS('b, flat_class)"


260 
apply (intro_classes)


261 
apply (unfold less)


262 
apply (simp add: type_definition.Rep_inject [OF type, symmetric])


263 
apply (simp add: typedef_Rep_strict [OF type less UU_in_A])


264 
apply (simp add: ax_flat)


265 
done


266 

16697

267 
subsection {* HOLCF type definition package *}


268 

23152

269 
use "Tools/pcpodef_package.ML"

16697

270 


271 
end
