1.1 --- a/src/HOLCF/Cpodef.thy Sat Nov 27 14:34:54 2010 -0800
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,285 +0,0 @@
1.4 -(* Title: HOLCF/Pcpodef.thy
1.5 - Author: Brian Huffman
1.6 -*)
1.7 -
1.8 -header {* Subtypes of pcpos *}
1.9 -
1.10 -theory Cpodef
1.11 -imports Adm
1.12 -uses ("Tools/cpodef.ML")
1.13 -begin
1.14 -
1.15 -subsection {* Proving a subtype is a partial order *}
1.16 -
1.17 -text {*
1.18 - A subtype of a partial order is itself a partial order,
1.19 - if the ordering is defined in the standard way.
1.20 -*}
1.21 -
1.22 -setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
1.23 -
1.24 -theorem typedef_po:
1.25 - fixes Abs :: "'a::po \<Rightarrow> 'b::type"
1.26 - assumes type: "type_definition Rep Abs A"
1.27 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.28 - shows "OFCLASS('b, po_class)"
1.29 - apply (intro_classes, unfold below)
1.30 - apply (rule below_refl)
1.31 - apply (erule (1) below_trans)
1.32 - apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
1.33 - apply (erule (1) below_antisym)
1.34 -done
1.35 -
1.36 -setup {* Sign.add_const_constraint (@{const_name Porder.below},
1.37 - SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
1.38 -
1.39 -subsection {* Proving a subtype is finite *}
1.40 -
1.41 -lemma typedef_finite_UNIV:
1.42 - fixes Abs :: "'a::type \<Rightarrow> 'b::type"
1.43 - assumes type: "type_definition Rep Abs A"
1.44 - shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
1.45 -proof -
1.46 - assume "finite A"
1.47 - hence "finite (Abs ` A)" by (rule finite_imageI)
1.48 - thus "finite (UNIV :: 'b set)"
1.49 - by (simp only: type_definition.Abs_image [OF type])
1.50 -qed
1.51 -
1.52 -subsection {* Proving a subtype is chain-finite *}
1.53 -
1.54 -lemma ch2ch_Rep:
1.55 - assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.56 - shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
1.57 -unfolding chain_def below .
1.58 -
1.59 -theorem typedef_chfin:
1.60 - fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
1.61 - assumes type: "type_definition Rep Abs A"
1.62 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.63 - shows "OFCLASS('b, chfin_class)"
1.64 - apply intro_classes
1.65 - apply (drule ch2ch_Rep [OF below])
1.66 - apply (drule chfin)
1.67 - apply (unfold max_in_chain_def)
1.68 - apply (simp add: type_definition.Rep_inject [OF type])
1.69 -done
1.70 -
1.71 -subsection {* Proving a subtype is complete *}
1.72 -
1.73 -text {*
1.74 - A subtype of a cpo is itself a cpo if the ordering is
1.75 - defined in the standard way, and the defining subset
1.76 - is closed with respect to limits of chains. A set is
1.77 - closed if and only if membership in the set is an
1.78 - admissible predicate.
1.79 -*}
1.80 -
1.81 -lemma typedef_is_lubI:
1.82 - assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.83 - shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
1.84 -unfolding is_lub_def is_ub_def below by simp
1.85 -
1.86 -lemma Abs_inverse_lub_Rep:
1.87 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
1.88 - assumes type: "type_definition Rep Abs A"
1.89 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.90 - and adm: "adm (\<lambda>x. x \<in> A)"
1.91 - shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
1.92 - apply (rule type_definition.Abs_inverse [OF type])
1.93 - apply (erule admD [OF adm ch2ch_Rep [OF below]])
1.94 - apply (rule type_definition.Rep [OF type])
1.95 -done
1.96 -
1.97 -theorem typedef_is_lub:
1.98 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
1.99 - assumes type: "type_definition Rep Abs A"
1.100 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.101 - and adm: "adm (\<lambda>x. x \<in> A)"
1.102 - shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
1.103 -proof -
1.104 - assume S: "chain S"
1.105 - hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
1.106 - hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
1.107 - hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
1.108 - by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
1.109 - thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
1.110 - by (rule typedef_is_lubI [OF below])
1.111 -qed
1.112 -
1.113 -lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
1.114 -
1.115 -theorem typedef_cpo:
1.116 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
1.117 - assumes type: "type_definition Rep Abs A"
1.118 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.119 - and adm: "adm (\<lambda>x. x \<in> A)"
1.120 - shows "OFCLASS('b, cpo_class)"
1.121 -proof
1.122 - fix S::"nat \<Rightarrow> 'b" assume "chain S"
1.123 - hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
1.124 - by (rule typedef_is_lub [OF type below adm])
1.125 - thus "\<exists>x. range S <<| x" ..
1.126 -qed
1.127 -
1.128 -subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
1.129 -
1.130 -text {* For any sub-cpo, the @{term Rep} function is continuous. *}
1.131 -
1.132 -theorem typedef_cont_Rep:
1.133 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
1.134 - assumes type: "type_definition Rep Abs A"
1.135 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.136 - and adm: "adm (\<lambda>x. x \<in> A)"
1.137 - shows "cont Rep"
1.138 - apply (rule contI)
1.139 - apply (simp only: typedef_lub [OF type below adm])
1.140 - apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
1.141 - apply (rule cpo_lubI)
1.142 - apply (erule ch2ch_Rep [OF below])
1.143 -done
1.144 -
1.145 -text {*
1.146 - For a sub-cpo, we can make the @{term Abs} function continuous
1.147 - only if we restrict its domain to the defining subset by
1.148 - composing it with another continuous function.
1.149 -*}
1.150 -
1.151 -theorem typedef_cont_Abs:
1.152 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
1.153 - fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
1.154 - assumes type: "type_definition Rep Abs A"
1.155 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.156 - and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
1.157 - and f_in_A: "\<And>x. f x \<in> A"
1.158 - shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
1.159 -unfolding cont_def is_lub_def is_ub_def ball_simps below
1.160 -by (simp add: type_definition.Abs_inverse [OF type f_in_A])
1.161 -
1.162 -subsection {* Proving subtype elements are compact *}
1.163 -
1.164 -theorem typedef_compact:
1.165 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
1.166 - assumes type: "type_definition Rep Abs A"
1.167 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.168 - and adm: "adm (\<lambda>x. x \<in> A)"
1.169 - shows "compact (Rep k) \<Longrightarrow> compact k"
1.170 -proof (unfold compact_def)
1.171 - have cont_Rep: "cont Rep"
1.172 - by (rule typedef_cont_Rep [OF type below adm])
1.173 - assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
1.174 - with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
1.175 - thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
1.176 -qed
1.177 -
1.178 -subsection {* Proving a subtype is pointed *}
1.179 -
1.180 -text {*
1.181 - A subtype of a cpo has a least element if and only if
1.182 - the defining subset has a least element.
1.183 -*}
1.184 -
1.185 -theorem typedef_pcpo_generic:
1.186 - fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
1.187 - assumes type: "type_definition Rep Abs A"
1.188 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.189 - and z_in_A: "z \<in> A"
1.190 - and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
1.191 - shows "OFCLASS('b, pcpo_class)"
1.192 - apply (intro_classes)
1.193 - apply (rule_tac x="Abs z" in exI, rule allI)
1.194 - apply (unfold below)
1.195 - apply (subst type_definition.Abs_inverse [OF type z_in_A])
1.196 - apply (rule z_least [OF type_definition.Rep [OF type]])
1.197 -done
1.198 -
1.199 -text {*
1.200 - As a special case, a subtype of a pcpo has a least element
1.201 - if the defining subset contains @{term \<bottom>}.
1.202 -*}
1.203 -
1.204 -theorem typedef_pcpo:
1.205 - fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
1.206 - assumes type: "type_definition Rep Abs A"
1.207 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.208 - and UU_in_A: "\<bottom> \<in> A"
1.209 - shows "OFCLASS('b, pcpo_class)"
1.210 -by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
1.211 -
1.212 -subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
1.213 -
1.214 -text {*
1.215 - For a sub-pcpo where @{term \<bottom>} is a member of the defining
1.216 - subset, @{term Rep} and @{term Abs} are both strict.
1.217 -*}
1.218 -
1.219 -theorem typedef_Abs_strict:
1.220 - assumes type: "type_definition Rep Abs A"
1.221 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.222 - and UU_in_A: "\<bottom> \<in> A"
1.223 - shows "Abs \<bottom> = \<bottom>"
1.224 - apply (rule UU_I, unfold below)
1.225 - apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
1.226 -done
1.227 -
1.228 -theorem typedef_Rep_strict:
1.229 - assumes type: "type_definition Rep Abs A"
1.230 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.231 - and UU_in_A: "\<bottom> \<in> A"
1.232 - shows "Rep \<bottom> = \<bottom>"
1.233 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
1.234 - apply (rule type_definition.Abs_inverse [OF type UU_in_A])
1.235 -done
1.236 -
1.237 -theorem typedef_Abs_bottom_iff:
1.238 - assumes type: "type_definition Rep Abs A"
1.239 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.240 - and UU_in_A: "\<bottom> \<in> A"
1.241 - shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
1.242 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
1.243 - apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
1.244 -done
1.245 -
1.246 -theorem typedef_Rep_bottom_iff:
1.247 - assumes type: "type_definition Rep Abs A"
1.248 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.249 - and UU_in_A: "\<bottom> \<in> A"
1.250 - shows "(Rep x = \<bottom>) = (x = \<bottom>)"
1.251 - apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
1.252 - apply (simp add: type_definition.Rep_inject [OF type])
1.253 -done
1.254 -
1.255 -theorem typedef_Abs_defined:
1.256 - assumes type: "type_definition Rep Abs A"
1.257 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.258 - and UU_in_A: "\<bottom> \<in> A"
1.259 - shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
1.260 -by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
1.261 -
1.262 -theorem typedef_Rep_defined:
1.263 - assumes type: "type_definition Rep Abs A"
1.264 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.265 - and UU_in_A: "\<bottom> \<in> A"
1.266 - shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
1.267 -by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
1.268 -
1.269 -subsection {* Proving a subtype is flat *}
1.270 -
1.271 -theorem typedef_flat:
1.272 - fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
1.273 - assumes type: "type_definition Rep Abs A"
1.274 - and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
1.275 - and UU_in_A: "\<bottom> \<in> A"
1.276 - shows "OFCLASS('b, flat_class)"
1.277 - apply (intro_classes)
1.278 - apply (unfold below)
1.279 - apply (simp add: type_definition.Rep_inject [OF type, symmetric])
1.280 - apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
1.281 - apply (simp add: ax_flat)
1.282 -done
1.283 -
1.284 -subsection {* HOLCF type definition package *}
1.285 -
1.286 -use "Tools/cpodef.ML"
1.287 -
1.288 -end