1(* Title: HOL/Complete_Partial_Order.thy 2 Author: Brian Huffman, Portland State University 3 Author: Alexander Krauss, TU Muenchen 4*) 5 6section \<open>Chain-complete partial orders and their fixpoints\<close> 7 8theory Complete_Partial_Order 9 imports Product_Type 10begin 11 12subsection \<open>Monotone functions\<close> 13 14text \<open>Dictionary-passing version of \<^const>\<open>Orderings.mono\<close>.\<close> 15 16definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 17 where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))" 18 19lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f" 20 unfolding monotone_def by iprover 21 22lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)" 23 unfolding monotone_def by iprover 24 25 26subsection \<open>Chains\<close> 27 28text \<open> 29 A chain is a totally-ordered set. Chains are parameterized over 30 the order for maximal flexibility, since type classes are not enough. 31\<close> 32 33definition chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 34 where "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)" 35 36lemma chainI: 37 assumes "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> ord x y \<or> ord y x" 38 shows "chain ord S" 39 using assms unfolding chain_def by fast 40 41lemma chainD: 42 assumes "chain ord S" and "x \<in> S" and "y \<in> S" 43 shows "ord x y \<or> ord y x" 44 using assms unfolding chain_def by fast 45 46lemma chainE: 47 assumes "chain ord S" and "x \<in> S" and "y \<in> S" 48 obtains "ord x y" | "ord y x" 49 using assms unfolding chain_def by fast 50 51lemma chain_empty: "chain ord {}" 52 by (simp add: chain_def) 53 54lemma chain_equality: "chain (=) A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)" 55 by (auto simp add: chain_def) 56 57lemma chain_subset: "chain ord A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> chain ord B" 58 by (rule chainI) (blast dest: chainD) 59 60lemma chain_imageI: 61 assumes chain: "chain le_a Y" 62 and mono: "\<And>x y. x \<in> Y \<Longrightarrow> y \<in> Y \<Longrightarrow> le_a x y \<Longrightarrow> le_b (f x) (f y)" 63 shows "chain le_b (f ` Y)" 64 by (blast intro: chainI dest: chainD[OF chain] mono) 65 66 67subsection \<open>Chain-complete partial orders\<close> 68 69text \<open> 70 A \<open>ccpo\<close> has a least upper bound for any chain. In particular, the 71 empty set is a chain, so every \<open>ccpo\<close> must have a bottom element. 72\<close> 73 74class ccpo = order + Sup + 75 assumes ccpo_Sup_upper: "chain (\<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A" 76 assumes ccpo_Sup_least: "chain (\<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z" 77begin 78 79lemma chain_singleton: "Complete_Partial_Order.chain (\<le>) {x}" 80 by (rule chainI) simp 81 82lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x" 83 by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton) 84 85 86subsection \<open>Transfinite iteration of a function\<close> 87 88context notes [[inductive_internals]] 89begin 90 91inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set" 92 for f :: "'a \<Rightarrow> 'a" 93 where 94 step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f" 95 | Sup: "chain (\<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f" 96 97end 98 99lemma iterates_le_f: "x \<in> iterates f \<Longrightarrow> monotone (\<le>) (\<le>) f \<Longrightarrow> x \<le> f x" 100 by (induct x rule: iterates.induct) 101 (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+ 102 103lemma chain_iterates: 104 assumes f: "monotone (\<le>) (\<le>) f" 105 shows "chain (\<le>) (iterates f)" (is "chain _ ?C") 106proof (rule chainI) 107 fix x y 108 assume "x \<in> ?C" "y \<in> ?C" 109 then show "x \<le> y \<or> y \<le> x" 110 proof (induct x arbitrary: y rule: iterates.induct) 111 fix x y 112 assume y: "y \<in> ?C" 113 and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x" 114 from y show "f x \<le> y \<or> y \<le> f x" 115 proof (induct y rule: iterates.induct) 116 case (step y) 117 with IH f show ?case by (auto dest: monotoneD) 118 next 119 case (Sup M) 120 then have chM: "chain (\<le>) M" 121 and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto 122 show "f x \<le> Sup M \<or> Sup M \<le> f x" 123 proof (cases "\<exists>z\<in>M. f x \<le> z") 124 case True 125 then have "f x \<le> Sup M" 126 apply rule 127 apply (erule order_trans) 128 apply (rule ccpo_Sup_upper[OF chM]) 129 apply assumption 130 done 131 then show ?thesis .. 132 next 133 case False 134 with IH' show ?thesis 135 by (auto intro: ccpo_Sup_least[OF chM]) 136 qed 137 qed 138 next 139 case (Sup M y) 140 show ?case 141 proof (cases "\<exists>x\<in>M. y \<le> x") 142 case True 143 then have "y \<le> Sup M" 144 apply rule 145 apply (erule order_trans) 146 apply (rule ccpo_Sup_upper[OF Sup(1)]) 147 apply assumption 148 done 149 then show ?thesis .. 150 next 151 case False with Sup 152 show ?thesis by (auto intro: ccpo_Sup_least) 153 qed 154 qed 155qed 156 157lemma bot_in_iterates: "Sup {} \<in> iterates f" 158 by (auto intro: iterates.Sup simp add: chain_empty) 159 160 161subsection \<open>Fixpoint combinator\<close> 162 163definition fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" 164 where "fixp f = Sup (iterates f)" 165 166lemma iterates_fixp: 167 assumes f: "monotone (\<le>) (\<le>) f" 168 shows "fixp f \<in> iterates f" 169 unfolding fixp_def 170 by (simp add: iterates.Sup chain_iterates f) 171 172lemma fixp_unfold: 173 assumes f: "monotone (\<le>) (\<le>) f" 174 shows "fixp f = f (fixp f)" 175proof (rule antisym) 176 show "fixp f \<le> f (fixp f)" 177 by (intro iterates_le_f iterates_fixp f) 178 have "f (fixp f) \<le> Sup (iterates f)" 179 by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp) 180 then show "f (fixp f) \<le> fixp f" 181 by (simp only: fixp_def) 182qed 183 184lemma fixp_lowerbound: 185 assumes f: "monotone (\<le>) (\<le>) f" 186 and z: "f z \<le> z" 187 shows "fixp f \<le> z" 188 unfolding fixp_def 189proof (rule ccpo_Sup_least[OF chain_iterates[OF f]]) 190 fix x 191 assume "x \<in> iterates f" 192 then show "x \<le> z" 193 proof (induct x rule: iterates.induct) 194 case (step x) 195 from f \<open>x \<le> z\<close> have "f x \<le> f z" by (rule monotoneD) 196 also note z 197 finally show "f x \<le> z" . 198 next 199 case (Sup M) 200 then show ?case 201 by (auto intro: ccpo_Sup_least) 202 qed 203qed 204 205end 206 207 208subsection \<open>Fixpoint induction\<close> 209 210setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close> 211 212definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 213 where "admissible lub ord P \<longleftrightarrow> (\<forall>A. chain ord A \<longrightarrow> A \<noteq> {} \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))" 214 215lemma admissibleI: 216 assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)" 217 shows "ccpo.admissible lub ord P" 218 using assms unfolding ccpo.admissible_def by fast 219 220lemma admissibleD: 221 assumes "ccpo.admissible lub ord P" 222 assumes "chain ord A" 223 assumes "A \<noteq> {}" 224 assumes "\<And>x. x \<in> A \<Longrightarrow> P x" 225 shows "P (lub A)" 226 using assms by (auto simp: ccpo.admissible_def) 227 228setup \<open>Sign.map_naming Name_Space.parent_path\<close> 229 230lemma (in ccpo) fixp_induct: 231 assumes adm: "ccpo.admissible Sup (\<le>) P" 232 assumes mono: "monotone (\<le>) (\<le>) f" 233 assumes bot: "P (Sup {})" 234 assumes step: "\<And>x. P x \<Longrightarrow> P (f x)" 235 shows "P (fixp f)" 236 unfolding fixp_def 237 using adm chain_iterates[OF mono] 238proof (rule ccpo.admissibleD) 239 show "iterates f \<noteq> {}" 240 using bot_in_iterates by auto 241next 242 fix x 243 assume "x \<in> iterates f" 244 then show "P x" 245 proof (induct rule: iterates.induct) 246 case prems: (step x) 247 from this(2) show ?case by (rule step) 248 next 249 case (Sup M) 250 then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm) 251 qed 252qed 253 254lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)" 255 unfolding ccpo.admissible_def by simp 256 257(*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)" 258unfolding ccpo.admissible_def chain_def by simp 259*) 260lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)" 261 by (auto intro: ccpo.admissibleI) 262 263lemma admissible_conj: 264 assumes "ccpo.admissible lub ord (\<lambda>x. P x)" 265 assumes "ccpo.admissible lub ord (\<lambda>x. Q x)" 266 shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)" 267 using assms unfolding ccpo.admissible_def by simp 268 269lemma admissible_all: 270 assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)" 271 shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)" 272 using assms unfolding ccpo.admissible_def by fast 273 274lemma admissible_ball: 275 assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)" 276 shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)" 277 using assms unfolding ccpo.admissible_def by fast 278 279lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}" 280 unfolding chain_def by fast 281 282context ccpo 283begin 284 285lemma admissible_disj: 286 fixes P Q :: "'a \<Rightarrow> bool" 287 assumes P: "ccpo.admissible Sup (\<le>) (\<lambda>x. P x)" 288 assumes Q: "ccpo.admissible Sup (\<le>) (\<lambda>x. Q x)" 289 shows "ccpo.admissible Sup (\<le>) (\<lambda>x. P x \<or> Q x)" 290proof (rule ccpo.admissibleI) 291 fix A :: "'a set" 292 assume chain: "chain (\<le>) A" 293 assume A: "A \<noteq> {}" and P_Q: "\<forall>x\<in>A. P x \<or> Q x" 294 have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)" 295 (is "?P \<or> ?Q" is "?P1 \<and> ?P2 \<or> _") 296 proof (rule disjCI) 297 assume "\<not> ?Q" 298 then consider "\<forall>x\<in>A. \<not> Q x" | a where "a \<in> A" "\<forall>y\<in>A. a \<le> y \<longrightarrow> \<not> Q y" 299 by blast 300 then show ?P 301 proof cases 302 case 1 303 with P_Q have "\<forall>x\<in>A. P x" by blast 304 with A show ?P by blast 305 next 306 case 2 307 note a = \<open>a \<in> A\<close> 308 show ?P 309 proof 310 from P_Q 2 have *: "\<forall>y\<in>A. a \<le> y \<longrightarrow> P y" by blast 311 with a have "P a" by blast 312 with a show ?P1 by blast 313 show ?P2 314 proof 315 fix x 316 assume x: "x \<in> A" 317 with chain a show "\<exists>y\<in>A. x \<le> y \<and> P y" 318 proof (rule chainE) 319 assume le: "a \<le> x" 320 with * a x have "P x" by blast 321 with x le show ?thesis by blast 322 next 323 assume "a \<ge> x" 324 with a \<open>P a\<close> show ?thesis by blast 325 qed 326 qed 327 qed 328 qed 329 qed 330 moreover 331 have "Sup A = Sup {x \<in> A. P x}" if "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y" for P 332 proof (rule antisym) 333 have chain_P: "chain (\<le>) {x \<in> A. P x}" 334 by (rule chain_compr [OF chain]) 335 show "Sup A \<le> Sup {x \<in> A. P x}" 336 apply (rule ccpo_Sup_least [OF chain]) 337 apply (drule that [rule_format]) 338 apply clarify 339 apply (erule order_trans) 340 apply (simp add: ccpo_Sup_upper [OF chain_P]) 341 done 342 show "Sup {x \<in> A. P x} \<le> Sup A" 343 apply (rule ccpo_Sup_least [OF chain_P]) 344 apply clarify 345 apply (simp add: ccpo_Sup_upper [OF chain]) 346 done 347 qed 348 ultimately 349 consider "\<exists>x. x \<in> A \<and> P x" "Sup A = Sup {x \<in> A. P x}" 350 | "\<exists>x. x \<in> A \<and> Q x" "Sup A = Sup {x \<in> A. Q x}" 351 by blast 352 then show "P (Sup A) \<or> Q (Sup A)" 353 apply cases 354 apply simp_all 355 apply (rule disjI1) 356 apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp) 357 apply (rule disjI2) 358 apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp) 359 done 360qed 361 362end 363 364instance complete_lattice \<subseteq> ccpo 365 by standard (fast intro: Sup_upper Sup_least)+ 366 367lemma lfp_eq_fixp: 368 assumes mono: "mono f" 369 shows "lfp f = fixp f" 370proof (rule antisym) 371 from mono have f': "monotone (\<le>) (\<le>) f" 372 unfolding mono_def monotone_def . 373 show "lfp f \<le> fixp f" 374 by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl) 375 show "fixp f \<le> lfp f" 376 by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono]) 377qed 378 379hide_const (open) iterates fixp 380 381end 382