1(* Title: HOL/HOLCF/Cpodef.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Subtypes of pcpos\<close> 6 7theory Cpodef 8 imports Adm 9 keywords "pcpodef" "cpodef" :: thy_goal_defn 10begin 11 12subsection \<open>Proving a subtype is a partial order\<close> 13 14text \<open> 15 A subtype of a partial order is itself a partial order, 16 if the ordering is defined in the standard way. 17\<close> 18 19setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, NONE)\<close> 20 21theorem typedef_po: 22 fixes Abs :: "'a::po \<Rightarrow> 'b::type" 23 assumes type: "type_definition Rep Abs A" 24 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 25 shows "OFCLASS('b, po_class)" 26 apply (intro_classes, unfold below) 27 apply (rule below_refl) 28 apply (erule (1) below_trans) 29 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) 30 apply (erule (1) below_antisym) 31 done 32 33setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, SOME \<^typ>\<open>'a::below \<Rightarrow> 'a::below \<Rightarrow> bool\<close>)\<close> 34 35 36subsection \<open>Proving a subtype is finite\<close> 37 38lemma typedef_finite_UNIV: 39 fixes Abs :: "'a::type \<Rightarrow> 'b::type" 40 assumes type: "type_definition Rep Abs A" 41 shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)" 42proof - 43 assume "finite A" 44 then have "finite (Abs ` A)" 45 by (rule finite_imageI) 46 then show "finite (UNIV :: 'b set)" 47 by (simp only: type_definition.Abs_image [OF type]) 48qed 49 50 51subsection \<open>Proving a subtype is chain-finite\<close> 52 53lemma ch2ch_Rep: 54 assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 55 shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))" 56 unfolding chain_def below . 57 58theorem typedef_chfin: 59 fixes Abs :: "'a::chfin \<Rightarrow> 'b::po" 60 assumes type: "type_definition Rep Abs A" 61 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 62 shows "OFCLASS('b, chfin_class)" 63 apply intro_classes 64 apply (drule ch2ch_Rep [OF below]) 65 apply (drule chfin) 66 apply (unfold max_in_chain_def) 67 apply (simp add: type_definition.Rep_inject [OF type]) 68 done 69 70 71subsection \<open>Proving a subtype is complete\<close> 72 73text \<open> 74 A subtype of a cpo is itself a cpo if the ordering is 75 defined in the standard way, and the defining subset 76 is closed with respect to limits of chains. A set is 77 closed if and only if membership in the set is an 78 admissible predicate. 79\<close> 80 81lemma typedef_is_lubI: 82 assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 83 shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x" 84 by (simp add: is_lub_def is_ub_def below) 85 86lemma Abs_inverse_lub_Rep: 87 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 88 assumes type: "type_definition Rep Abs A" 89 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 90 and adm: "adm (\<lambda>x. x \<in> A)" 91 shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))" 92 apply (rule type_definition.Abs_inverse [OF type]) 93 apply (erule admD [OF adm ch2ch_Rep [OF below]]) 94 apply (rule type_definition.Rep [OF type]) 95 done 96 97theorem typedef_is_lub: 98 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 99 assumes type: "type_definition Rep Abs A" 100 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 101 and adm: "adm (\<lambda>x. x \<in> A)" 102 assumes S: "chain S" 103 shows "range S <<| Abs (\<Squnion>i. Rep (S i))" 104proof - 105 from S have "chain (\<lambda>i. Rep (S i))" 106 by (rule ch2ch_Rep [OF below]) 107 then have "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" 108 by (rule cpo_lubI) 109 then have "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))" 110 by (simp only: Abs_inverse_lub_Rep [OF type below adm S]) 111 then show "range S <<| Abs (\<Squnion>i. Rep (S i))" 112 by (rule typedef_is_lubI [OF below]) 113qed 114 115lemmas typedef_lub = typedef_is_lub [THEN lub_eqI] 116 117theorem typedef_cpo: 118 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 119 assumes type: "type_definition Rep Abs A" 120 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 121 and adm: "adm (\<lambda>x. x \<in> A)" 122 shows "OFCLASS('b, cpo_class)" 123proof 124 fix S :: "nat \<Rightarrow> 'b" 125 assume "chain S" 126 then have "range S <<| Abs (\<Squnion>i. Rep (S i))" 127 by (rule typedef_is_lub [OF type below adm]) 128 then show "\<exists>x. range S <<| x" .. 129qed 130 131 132subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close> 133 134text \<open>For any sub-cpo, the \<^term>\<open>Rep\<close> function is continuous.\<close> 135 136theorem typedef_cont_Rep: 137 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 138 assumes type: "type_definition Rep Abs A" 139 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 140 and adm: "adm (\<lambda>x. x \<in> A)" 141 shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))" 142 apply (erule cont_apply [OF _ _ cont_const]) 143 apply (rule contI) 144 apply (simp only: typedef_lub [OF type below adm]) 145 apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) 146 apply (rule cpo_lubI) 147 apply (erule ch2ch_Rep [OF below]) 148 done 149 150text \<open> 151 For a sub-cpo, we can make the \<^term>\<open>Abs\<close> function continuous 152 only if we restrict its domain to the defining subset by 153 composing it with another continuous function. 154\<close> 155 156theorem typedef_cont_Abs: 157 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 158 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" 159 assumes type: "type_definition Rep Abs A" 160 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 161 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) 162 and f_in_A: "\<And>x. f x \<in> A" 163 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" 164 unfolding cont_def is_lub_def is_ub_def ball_simps below 165 by (simp add: type_definition.Abs_inverse [OF type f_in_A]) 166 167 168subsection \<open>Proving subtype elements are compact\<close> 169 170theorem typedef_compact: 171 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 172 assumes type: "type_definition Rep Abs A" 173 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 174 and adm: "adm (\<lambda>x. x \<in> A)" 175 shows "compact (Rep k) \<Longrightarrow> compact k" 176proof (unfold compact_def) 177 have cont_Rep: "cont Rep" 178 by (rule typedef_cont_Rep [OF type below adm cont_id]) 179 assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)" 180 with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst) 181 then show "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below) 182qed 183 184 185subsection \<open>Proving a subtype is pointed\<close> 186 187text \<open> 188 A subtype of a cpo has a least element if and only if 189 the defining subset has a least element. 190\<close> 191 192theorem typedef_pcpo_generic: 193 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 194 assumes type: "type_definition Rep Abs A" 195 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 196 and z_in_A: "z \<in> A" 197 and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x" 198 shows "OFCLASS('b, pcpo_class)" 199 apply (intro_classes) 200 apply (rule_tac x="Abs z" in exI, rule allI) 201 apply (unfold below) 202 apply (subst type_definition.Abs_inverse [OF type z_in_A]) 203 apply (rule z_least [OF type_definition.Rep [OF type]]) 204 done 205 206text \<open> 207 As a special case, a subtype of a pcpo has a least element 208 if the defining subset contains \<^term>\<open>\<bottom>\<close>. 209\<close> 210 211theorem typedef_pcpo: 212 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" 213 assumes type: "type_definition Rep Abs A" 214 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 215 and bottom_in_A: "\<bottom> \<in> A" 216 shows "OFCLASS('b, pcpo_class)" 217 by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal) 218 219 220subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close> 221 222text \<open> 223 For a sub-pcpo where \<^term>\<open>\<bottom>\<close> is a member of the defining 224 subset, \<^term>\<open>Rep\<close> and \<^term>\<open>Abs\<close> are both strict. 225\<close> 226 227theorem typedef_Abs_strict: 228 assumes type: "type_definition Rep Abs A" 229 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 230 and bottom_in_A: "\<bottom> \<in> A" 231 shows "Abs \<bottom> = \<bottom>" 232 apply (rule bottomI, unfold below) 233 apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A]) 234 done 235 236theorem typedef_Rep_strict: 237 assumes type: "type_definition Rep Abs A" 238 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 239 and bottom_in_A: "\<bottom> \<in> A" 240 shows "Rep \<bottom> = \<bottom>" 241 apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) 242 apply (rule type_definition.Abs_inverse [OF type bottom_in_A]) 243 done 244 245theorem typedef_Abs_bottom_iff: 246 assumes type: "type_definition Rep Abs A" 247 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 248 and bottom_in_A: "\<bottom> \<in> A" 249 shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)" 250 apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) 251 apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A) 252 done 253 254theorem typedef_Rep_bottom_iff: 255 assumes type: "type_definition Rep Abs A" 256 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 257 and bottom_in_A: "\<bottom> \<in> A" 258 shows "(Rep x = \<bottom>) = (x = \<bottom>)" 259 apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst]) 260 apply (simp add: type_definition.Rep_inject [OF type]) 261 done 262 263 264subsection \<open>Proving a subtype is flat\<close> 265 266theorem typedef_flat: 267 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" 268 assumes type: "type_definition Rep Abs A" 269 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 270 and bottom_in_A: "\<bottom> \<in> A" 271 shows "OFCLASS('b, flat_class)" 272 apply (intro_classes) 273 apply (unfold below) 274 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) 275 apply (simp add: typedef_Rep_strict [OF type below bottom_in_A]) 276 apply (simp add: ax_flat) 277 done 278 279 280subsection \<open>HOLCF type definition package\<close> 281 282ML_file \<open>Tools/cpodef.ML\<close> 283 284end 285