1(* Title: HOL/HOLCF/Product_Cpo.thy 2 Author: Franz Regensburger 3*) 4 5section \<open>The cpo of cartesian products\<close> 6 7theory Product_Cpo 8 imports Adm 9begin 10 11default_sort cpo 12 13 14subsection \<open>Unit type is a pcpo\<close> 15 16instantiation unit :: discrete_cpo 17begin 18 19definition below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True" 20 21instance 22 by standard simp 23 24end 25 26instance unit :: pcpo 27 by standard simp 28 29 30subsection \<open>Product type is a partial order\<close> 31 32instantiation prod :: (below, below) below 33begin 34 35definition below_prod_def: "(\<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" 36 37instance .. 38 39end 40 41instance prod :: (po, po) po 42proof 43 fix x :: "'a \<times> 'b" 44 show "x \<sqsubseteq> x" 45 by (simp add: below_prod_def) 46next 47 fix x y :: "'a \<times> 'b" 48 assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" 49 then show "x = y" 50 unfolding below_prod_def prod_eq_iff 51 by (fast intro: below_antisym) 52next 53 fix x y z :: "'a \<times> 'b" 54 assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" 55 then show "x \<sqsubseteq> z" 56 unfolding below_prod_def 57 by (fast intro: below_trans) 58qed 59 60 61subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close> 62 63lemma prod_belowI: "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q" 64 by (simp add: below_prod_def) 65 66lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d" 67 by (simp add: below_prod_def) 68 69text \<open>Pair \<open>(_,_)\<close> is monotone in both arguments\<close> 70 71lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" 72 by (simp add: monofun_def) 73 74lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" 75 by (simp add: monofun_def) 76 77lemma monofun_pair: "x1 \<sqsubseteq> x2 \<Longrightarrow> y1 \<sqsubseteq> y2 \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" 78 by simp 79 80lemma ch2ch_Pair [simp]: "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))" 81 by (rule chainI, simp add: chainE) 82 83text \<open>\<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> are monotone\<close> 84 85lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y" 86 by (simp add: below_prod_def) 87 88lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y" 89 by (simp add: below_prod_def) 90 91lemma monofun_fst: "monofun fst" 92 by (simp add: monofun_def below_prod_def) 93 94lemma monofun_snd: "monofun snd" 95 by (simp add: monofun_def below_prod_def) 96 97lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] 98 99lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd] 100 101lemma prod_chain_cases: 102 assumes chain: "chain Y" 103 obtains A B 104 where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))" 105proof 106 from chain show "chain (\<lambda>i. fst (Y i))" 107 by (rule ch2ch_fst) 108 from chain show "chain (\<lambda>i. snd (Y i))" 109 by (rule ch2ch_snd) 110 show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" 111 by simp 112qed 113 114 115subsection \<open>Product type is a cpo\<close> 116 117lemma is_lub_Pair: "range A <<| x \<Longrightarrow> range B <<| y \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)" 118 by (simp add: is_lub_def is_ub_def below_prod_def) 119 120lemma lub_Pair: "chain A \<Longrightarrow> chain B \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)" 121 for A :: "nat \<Rightarrow> 'a::cpo" and B :: "nat \<Rightarrow> 'b::cpo" 122 by (fast intro: lub_eqI is_lub_Pair elim: thelubE) 123 124lemma is_lub_prod: 125 fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" 126 assumes "chain S" 127 shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 128 using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI) 129 130lemma lub_prod: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 131 for S :: "nat \<Rightarrow> 'a::cpo \<times> 'b::cpo" 132 by (rule is_lub_prod [THEN lub_eqI]) 133 134instance prod :: (cpo, cpo) cpo 135proof 136 fix S :: "nat \<Rightarrow> ('a \<times> 'b)" 137 assume "chain S" 138 then have "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 139 by (rule is_lub_prod) 140 then show "\<exists>x. range S <<| x" .. 141qed 142 143instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo 144proof 145 fix x y :: "'a \<times> 'b" 146 show "x \<sqsubseteq> y \<longleftrightarrow> x = y" 147 by (simp add: below_prod_def prod_eq_iff) 148qed 149 150 151subsection \<open>Product type is pointed\<close> 152 153lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" 154 by (simp add: below_prod_def) 155 156instance prod :: (pcpo, pcpo) pcpo 157 by intro_classes (fast intro: minimal_prod) 158 159lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" 160 by (rule minimal_prod [THEN bottomI, symmetric]) 161 162lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 163 by (simp add: inst_prod_pcpo) 164 165lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" 166 unfolding inst_prod_pcpo by (rule fst_conv) 167 168lemma snd_strict [simp]: "snd \<bottom> = \<bottom>" 169 unfolding inst_prod_pcpo by (rule snd_conv) 170 171lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>" 172 by simp 173 174lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>" 175 by (simp add: split_def) 176 177 178subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close> 179 180lemma cont_pair1: "cont (\<lambda>x. (x, y))" 181 apply (rule contI) 182 apply (rule is_lub_Pair) 183 apply (erule cpo_lubI) 184 apply (rule is_lub_const) 185 done 186 187lemma cont_pair2: "cont (\<lambda>y. (x, y))" 188 apply (rule contI) 189 apply (rule is_lub_Pair) 190 apply (rule is_lub_const) 191 apply (erule cpo_lubI) 192 done 193 194lemma cont_fst: "cont fst" 195 apply (rule contI) 196 apply (simp add: lub_prod) 197 apply (erule cpo_lubI [OF ch2ch_fst]) 198 done 199 200lemma cont_snd: "cont snd" 201 apply (rule contI) 202 apply (simp add: lub_prod) 203 apply (erule cpo_lubI [OF ch2ch_snd]) 204 done 205 206lemma cont2cont_Pair [simp, cont2cont]: 207 assumes f: "cont (\<lambda>x. f x)" 208 assumes g: "cont (\<lambda>x. g x)" 209 shows "cont (\<lambda>x. (f x, g x))" 210 apply (rule cont_apply [OF f cont_pair1]) 211 apply (rule cont_apply [OF g cont_pair2]) 212 apply (rule cont_const) 213 done 214 215lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst] 216 217lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd] 218 219lemma cont2cont_case_prod: 220 assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)" 221 assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)" 222 assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)" 223 assumes g: "cont (\<lambda>x. g x)" 224 shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)" 225 unfolding split_def 226 apply (rule cont_apply [OF g]) 227 apply (rule cont_apply [OF cont_fst f2]) 228 apply (rule cont_apply [OF cont_snd f3]) 229 apply (rule cont_const) 230 apply (rule f1) 231 done 232 233lemma prod_contI: 234 assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))" 235 assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))" 236 shows "cont f" 237proof - 238 have "cont (\<lambda>(x, y). f (x, y))" 239 by (intro cont2cont_case_prod f1 f2 cont2cont) 240 then show "cont f" 241 by (simp only: case_prod_eta) 242qed 243 244lemma prod_cont_iff: "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))" 245 apply safe 246 apply (erule cont_compose [OF _ cont_pair1]) 247 apply (erule cont_compose [OF _ cont_pair2]) 248 apply (simp only: prod_contI) 249 done 250 251lemma cont2cont_case_prod' [simp, cont2cont]: 252 assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))" 253 assumes g: "cont (\<lambda>x. g x)" 254 shows "cont (\<lambda>x. case_prod (f x) (g x))" 255 using assms by (simp add: cont2cont_case_prod prod_cont_iff) 256 257text \<open>The simple version (due to Joachim Breitner) is needed if 258 either element type of the pair is not a cpo.\<close> 259 260lemma cont2cont_split_simple [simp, cont2cont]: 261 assumes "\<And>a b. cont (\<lambda>x. f x a b)" 262 shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)" 263 using assms by (cases p) auto 264 265text \<open>Admissibility of predicates on product types.\<close> 266 267lemma adm_case_prod [simp]: 268 assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))" 269 shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)" 270 unfolding case_prod_beta using assms . 271 272 273subsection \<open>Compactness and chain-finiteness\<close> 274 275lemma fst_below_iff: "fst x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)" 276 for x :: "'a \<times> 'b" 277 by (simp add: below_prod_def) 278 279lemma snd_below_iff: "snd x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)" 280 for x :: "'a \<times> 'b" 281 by (simp add: below_prod_def) 282 283lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)" 284 by (rule compactI) (simp add: fst_below_iff) 285 286lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)" 287 by (rule compactI) (simp add: snd_below_iff) 288 289lemma compact_Pair: "compact x \<Longrightarrow> compact y \<Longrightarrow> compact (x, y)" 290 by (rule compactI) (simp add: below_prod_def) 291 292lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y" 293 apply (safe intro!: compact_Pair) 294 apply (drule compact_fst, simp) 295 apply (drule compact_snd, simp) 296 done 297 298instance prod :: (chfin, chfin) chfin 299 apply intro_classes 300 apply (erule compact_imp_max_in_chain) 301 apply (case_tac "\<Squnion>i. Y i", simp) 302 done 303 304end 305