1(* Title: HOL/HOLCF/Pcpo.thy 2 Author: Franz Regensburger 3*) 4 5section \<open>Classes cpo and pcpo\<close> 6 7theory Pcpo 8 imports Porder 9begin 10 11subsection \<open>Complete partial orders\<close> 12 13text \<open>The class cpo of chain complete partial orders\<close> 14 15class cpo = po + 16 assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x" 17begin 18 19text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close> 20 21lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)" 22 by (fast dest: cpo elim: is_lub_lub) 23 24lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l" 25 by (blast dest: cpo intro: is_lub_lub) 26 27text \<open>Properties of the lub\<close> 28 29lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)" 30 by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) 31 32lemma is_lub_thelub: "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" 33 by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2]) 34 35lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)" 36 by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) 37 38lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" 39 by (simp add: lub_below_iff) 40 41lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)" 42 by (erule below_trans, erule is_ub_thelub) 43 44lemma lub_range_mono: "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 45 apply (erule lub_below) 46 apply (subgoal_tac "\<exists>j. X i = Y j") 47 apply clarsimp 48 apply (erule is_ub_thelub) 49 apply auto 50 done 51 52lemma lub_range_shift: "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" 53 apply (rule below_antisym) 54 apply (rule lub_range_mono) 55 apply fast 56 apply assumption 57 apply (erule chain_shift) 58 apply (rule lub_below) 59 apply assumption 60 apply (rule_tac i="i" in below_lub) 61 apply (erule chain_shift) 62 apply (erule chain_mono) 63 apply (rule le_add1) 64 done 65 66lemma maxinch_is_thelub: "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" 67 apply (rule iffI) 68 apply (fast intro!: lub_eqI lub_finch1) 69 apply (unfold max_in_chain_def) 70 apply (safe intro!: below_antisym) 71 apply (fast elim!: chain_mono) 72 apply (drule sym) 73 apply (force elim!: is_ub_thelub) 74 done 75 76text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close> 77 78lemma lub_mono: "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 79 by (fast elim: lub_below below_lub) 80 81text \<open>the = relation between two chains is preserved by their lubs\<close> 82 83lemma lub_eq: "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 84 by simp 85 86lemma ch2ch_lub: 87 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 88 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 89 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" 90 apply (rule chainI) 91 apply (rule lub_mono [OF 2 2]) 92 apply (rule chainE [OF 1]) 93 done 94 95lemma diag_lub: 96 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 97 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 98 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" 99proof (rule below_antisym) 100 have 3: "chain (\<lambda>i. Y i i)" 101 apply (rule chainI) 102 apply (rule below_trans) 103 apply (rule chainE [OF 1]) 104 apply (rule chainE [OF 2]) 105 done 106 have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" 107 by (rule ch2ch_lub [OF 1 2]) 108 show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" 109 apply (rule lub_below [OF 4]) 110 apply (rule lub_below [OF 2]) 111 apply (rule below_lub [OF 3]) 112 apply (rule below_trans) 113 apply (rule chain_mono [OF 1 max.cobounded1]) 114 apply (rule chain_mono [OF 2 max.cobounded2]) 115 done 116 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" 117 apply (rule lub_mono [OF 3 4]) 118 apply (rule is_ub_thelub [OF 2]) 119 done 120qed 121 122lemma ex_lub: 123 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 124 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 125 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)" 126 by (simp add: diag_lub 1 2) 127 128end 129 130 131subsection \<open>Pointed cpos\<close> 132 133text \<open>The class pcpo of pointed cpos\<close> 134 135class pcpo = cpo + 136 assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" 137begin 138 139definition bottom :: "'a" ("\<bottom>") 140 where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" 141 142lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" 143 unfolding bottom_def 144 apply (rule the1I2) 145 apply (rule ex_ex1I) 146 apply (rule least) 147 apply (blast intro: below_antisym) 148 apply simp 149 done 150 151end 152 153text \<open>Old "UU" syntax:\<close> 154 155syntax UU :: logic 156translations "UU" \<rightharpoonup> "CONST bottom" 157 158text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close> 159setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close> 160simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc 161 162text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close> 163 164lemma below_bottom_iff [simp]: "x \<sqsubseteq> \<bottom> \<longleftrightarrow> x = \<bottom>" 165 by (simp add: po_eq_conv) 166 167lemma eq_bottom_iff: "x = \<bottom> \<longleftrightarrow> x \<sqsubseteq> \<bottom>" 168 by simp 169 170lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" 171 by (subst eq_bottom_iff) 172 173lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" 174 by (simp only: eq_bottom_iff lub_below_iff) 175 176 177subsection \<open>Chain-finite and flat cpos\<close> 178 179text \<open>further useful classes for HOLCF domains\<close> 180 181class chfin = po + 182 assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" 183begin 184 185subclass cpo 186 apply standard 187 apply (frule chfin) 188 apply (blast intro: lub_finch1) 189 done 190 191lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y" 192 by (simp add: chfin finite_chain_def) 193 194end 195 196class flat = pcpo + 197 assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y" 198begin 199 200subclass chfin 201proof 202 fix Y 203 assume *: "chain Y" 204 show "\<exists>n. max_in_chain n Y" 205 apply (unfold max_in_chain_def) 206 apply (cases "\<forall>i. Y i = \<bottom>") 207 apply simp 208 apply simp 209 apply (erule exE) 210 apply (rule_tac x="i" in exI) 211 apply clarify 212 using * apply (blast dest: chain_mono ax_flat) 213 done 214qed 215 216lemma flat_below_iff: "x \<sqsubseteq> y \<longleftrightarrow> x = \<bottom> \<or> x = y" 217 by (safe dest!: ax_flat) 218 219lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)" 220 by (safe dest!: ax_flat) 221 222end 223 224subsection \<open>Discrete cpos\<close> 225 226class discrete_cpo = below + 227 assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" 228begin 229 230subclass po 231 by standard simp_all 232 233text \<open>In a discrete cpo, every chain is constant\<close> 234 235lemma discrete_chain_const: 236 assumes S: "chain S" 237 shows "\<exists>x. S = (\<lambda>i. x)" 238proof (intro exI ext) 239 fix i :: nat 240 from S le0 have "S 0 \<sqsubseteq> S i" by (rule chain_mono) 241 then have "S 0 = S i" by simp 242 then show "S i = S 0" by (rule sym) 243qed 244 245subclass chfin 246proof 247 fix S :: "nat \<Rightarrow> 'a" 248 assume S: "chain S" 249 then have "\<exists>x. S = (\<lambda>i. x)" 250 by (rule discrete_chain_const) 251 then have "max_in_chain 0 S" 252 by (auto simp: max_in_chain_def) 253 then show "\<exists>i. max_in_chain i S" .. 254qed 255 256end 257 258end 259