1(* Title: HOL/Hilbert_Choice.thy 2 Author: Lawrence C Paulson, Tobias Nipkow 3 Author: Viorel Preoteasa (Results about complete distributive lattices) 4 Copyright 2001 University of Cambridge 5*) 6 7section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close> 8 9theory Hilbert_Choice 10 imports Wellfounded 11 keywords "specification" :: thy_goal_defn 12begin 13 14subsection \<open>Hilbert's epsilon\<close> 15 16axiomatization Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 17 where someI: "P x \<Longrightarrow> P (Eps P)" 18 19syntax (epsilon) 20 "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3\<some>_./ _)" [0, 10] 10) 21syntax (input) 22 "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3@ _./ _)" [0, 10] 10) 23syntax 24 "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10) 25translations 26 "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)" 27 28print_translation \<open> 29 [(\<^const_syntax>\<open>Eps\<close>, fn _ => fn [Abs abs] => 30 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 31 in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)] 32\<close> \<comment> \<open>to avoid eta-contraction of body\<close> 33 34definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where 35"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)" 36 37lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)" 38by(simp add: inv_into_def) 39 40abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where 41"inv \<equiv> inv_into UNIV" 42 43 44subsection \<open>Hilbert's Epsilon-operator\<close> 45 46lemma Eps_cong: 47 assumes "\<And>x. P x = Q x" 48 shows "Eps P = Eps Q" 49 using ext[of P Q, OF assms] by simp 50 51text \<open> 52 Easier to apply than \<open>someI\<close> if the witness comes from an 53 existential formula. 54\<close> 55lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)" 56 apply (erule exE) 57 apply (erule someI) 58 done 59 60lemma some_eq_imp: 61 assumes "Eps P = a" "P b" shows "P a" 62 using assms someI_ex by force 63 64text \<open> 65 Easier to apply than \<open>someI\<close> because the conclusion has only one 66 occurrence of \<^term>\<open>P\<close>. 67\<close> 68lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)" 69 by (blast intro: someI) 70 71text \<open> 72 Easier to apply than \<open>someI2\<close> if the witness comes from an 73 existential formula. 74\<close> 75lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)" 76 by (blast intro: someI2) 77 78lemma someI2_bex: "\<exists>a\<in>A. P a \<Longrightarrow> (\<And>x. x \<in> A \<and> P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. x \<in> A \<and> P x)" 79 by (blast intro: someI2) 80 81lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a" 82 by (blast intro: someI2) 83 84lemma some1_equality: "\<exists>!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a" 85 by blast 86 87lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)" 88 by (blast intro: someI) 89 90lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}" 91 unfolding ex_in_conv[symmetric] by (rule some_eq_ex) 92 93lemma some_eq_trivial [simp]: "(SOME y. y = x) = x" 94 by (rule some_equality) (rule refl) 95 96lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x" 97 apply (rule some_equality) 98 apply (rule refl) 99 apply (erule sym) 100 done 101 102 103subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close> 104 105lemma choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)" 106 by (fast elim: someI) 107 108lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)" 109 by (fast elim: someI) 110 111lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))" 112 by (fast elim: someI) 113 114lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))" 115 by (fast elim: someI) 116 117lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))" 118 by (fast elim: someI) 119 120lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))" 121 by (fast elim: someI) 122 123lemma dependent_nat_choice: 124 assumes 1: "\<exists>x. P 0 x" 125 and 2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y" 126 shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))" 127proof (intro exI allI conjI) 128 fix n 129 define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)" 130 then have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))" 131 using someI_ex[OF 1] someI_ex[OF 2] by simp_all 132 then show "P n (f n)" "Q n (f n) (f (Suc n))" 133 by (induct n) auto 134qed 135 136lemma finite_subset_Union: 137 assumes "finite A" "A \<subseteq> \<Union>\<B>" 138 obtains \<F> where "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>" 139proof - 140 have "\<forall>x\<in>A. \<exists>B\<in>\<B>. x\<in>B" 141 using assms by blast 142 then obtain f where f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<B> \<and> x \<in> f x" 143 by (auto simp add: bchoice_iff Bex_def) 144 show thesis 145 proof 146 show "finite (f ` A)" 147 using assms by auto 148 qed (use f in auto) 149qed 150 151 152subsection \<open>Function Inverse\<close> 153 154lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)" 155 by (simp add: inv_into_def) 156 157lemma inv_into_into: "x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A" 158 by (simp add: inv_into_def) (fast intro: someI2) 159 160lemma inv_identity [simp]: "inv (\<lambda>a. a) = (\<lambda>a. a)" 161 by (simp add: inv_def) 162 163lemma inv_id [simp]: "inv id = id" 164 by (simp add: id_def) 165 166lemma inv_into_f_f [simp]: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> inv_into A f (f x) = x" 167 by (simp add: inv_into_def inj_on_def) (blast intro: someI2) 168 169lemma inv_f_f: "inj f \<Longrightarrow> inv f (f x) = x" 170 by simp 171 172lemma f_inv_into_f: "y \<in> f`A \<Longrightarrow> f (inv_into A f y) = y" 173 by (simp add: inv_into_def) (fast intro: someI2) 174 175lemma inv_into_f_eq: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> f x = y \<Longrightarrow> inv_into A f y = x" 176 by (erule subst) (fast intro: inv_into_f_f) 177 178lemma inv_f_eq: "inj f \<Longrightarrow> f x = y \<Longrightarrow> inv f y = x" 179 by (simp add:inv_into_f_eq) 180 181lemma inj_imp_inv_eq: "inj f \<Longrightarrow> \<forall>x. f (g x) = x \<Longrightarrow> inv f = g" 182 by (blast intro: inv_into_f_eq) 183 184text \<open>But is it useful?\<close> 185lemma inj_transfer: 186 assumes inj: "inj f" 187 and minor: "\<And>y. y \<in> range f \<Longrightarrow> P (inv f y)" 188 shows "P x" 189proof - 190 have "f x \<in> range f" by auto 191 then have "P(inv f (f x))" by (rule minor) 192 then show "P x" by (simp add: inv_into_f_f [OF inj]) 193qed 194 195lemma inj_iff: "inj f \<longleftrightarrow> inv f \<circ> f = id" 196 by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f) 197 198lemma inv_o_cancel[simp]: "inj f \<Longrightarrow> inv f \<circ> f = id" 199 by (simp add: inj_iff) 200 201lemma o_inv_o_cancel[simp]: "inj f \<Longrightarrow> g \<circ> inv f \<circ> f = g" 202 by (simp add: comp_assoc) 203 204lemma inv_into_image_cancel[simp]: "inj_on f A \<Longrightarrow> S \<subseteq> A \<Longrightarrow> inv_into A f ` f ` S = S" 205 by (fastforce simp: image_def) 206 207lemma inj_imp_surj_inv: "inj f \<Longrightarrow> surj (inv f)" 208 by (blast intro!: surjI inv_into_f_f) 209 210lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y" 211 by (simp add: f_inv_into_f) 212 213lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" 214 using surj_f_inv_f[of p] by (auto simp add: bij_def) 215 216lemma inv_into_injective: 217 assumes eq: "inv_into A f x = inv_into A f y" 218 and x: "x \<in> f`A" 219 and y: "y \<in> f`A" 220 shows "x = y" 221proof - 222 from eq have "f (inv_into A f x) = f (inv_into A f y)" 223 by simp 224 with x y show ?thesis 225 by (simp add: f_inv_into_f) 226qed 227 228lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B" 229 by (blast intro: inj_onI dest: inv_into_injective injD) 230 231lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A" 232 by (auto simp add: bij_betw_def inj_on_inv_into) 233 234lemma surj_imp_inj_inv: "surj f \<Longrightarrow> inj (inv f)" 235 by (simp add: inj_on_inv_into) 236 237lemma surj_iff: "surj f \<longleftrightarrow> f \<circ> inv f = id" 238 by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a]) 239 240lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)" 241 by (simp add: o_def surj_iff fun_eq_iff) 242 243lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g" 244 apply (rule ext) 245 apply (drule_tac x = "inv f x" in spec) 246 apply (simp add: surj_f_inv_f) 247 done 248 249lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)" 250 by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv) 251 252lemma inv_equality: "(\<And>x. g (f x) = x) \<Longrightarrow> (\<And>y. f (g y) = y) \<Longrightarrow> inv f = g" 253 by (rule ext) (auto simp add: inv_into_def) 254 255lemma inv_inv_eq: "bij f \<Longrightarrow> inv (inv f) = f" 256 by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f) 257 258text \<open> 259 \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such 260 that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close> 261 that \<open>inv f\<close> could be any function at all, including the identity function. 262 If \<open>inv f = id\<close> then \<open>inv f\<close> is a bijection, but \<open>inj f\<close>, \<open>surj f\<close> and \<open>inv 263 (inv f) = f\<close> all fail. 264\<close> 265 266lemma inv_into_comp: 267 "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow> 268 inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x" 269 apply (rule inv_into_f_eq) 270 apply (fast intro: comp_inj_on) 271 apply (simp add: inv_into_into) 272 apply (simp add: f_inv_into_f inv_into_into) 273 done 274 275lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f" 276 by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f) 277 278lemma image_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A" 279 by (simp add: surj_f_inv_f image_comp comp_def) 280 281lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A" 282 by simp 283 284lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}" 285 apply auto 286 apply (force simp add: bij_is_inj) 287 apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric]) 288 done 289 290lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A" 291 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f]) 292 apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric]) 293 done 294 295lemma inv_fn_o_fn_is_id: 296 fixes f::"'a \<Rightarrow> 'a" 297 assumes "bij f" 298 shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)" 299proof - 300 have "((inv f)^^n)((f^^n) x) = x" for x n 301 proof (induction n) 302 case (Suc n) 303 have *: "(inv f) (f y) = y" for y 304 by (simp add: assms bij_is_inj) 305 have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))" 306 by (simp add: funpow_swap1) 307 also have "... = (inv f^^n) ((f^^n) x)" 308 using * by auto 309 also have "... = x" using Suc.IH by auto 310 finally show ?case by simp 311 qed (auto) 312 then show ?thesis unfolding o_def by blast 313qed 314 315lemma fn_o_inv_fn_is_id: 316 fixes f::"'a \<Rightarrow> 'a" 317 assumes "bij f" 318 shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)" 319proof - 320 have "(f^^n) (((inv f)^^n) x) = x" for x n 321 proof (induction n) 322 case (Suc n) 323 have *: "f(inv f y) = y" for y 324 using bij_inv_eq_iff[OF assms] by auto 325 have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))" 326 by (simp add: funpow_swap1) 327 also have "... = (f^^n) ((inv f^^n) x)" 328 using * by auto 329 also have "... = x" using Suc.IH by auto 330 finally show ?case by simp 331 qed (auto) 332 then show ?thesis unfolding o_def by blast 333qed 334 335lemma inv_fn: 336 fixes f::"'a \<Rightarrow> 'a" 337 assumes "bij f" 338 shows "inv (f^^n) = ((inv f)^^n)" 339proof - 340 have "inv (f^^n) x = ((inv f)^^n) x" for x 341 apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]]) 342 using fn_o_inv_fn_is_id[OF assms, of n, THEN fun_cong] by (simp) 343 then show ?thesis by auto 344qed 345 346lemma mono_inv: 347 fixes f::"'a::linorder \<Rightarrow> 'b::linorder" 348 assumes "mono f" "bij f" 349 shows "mono (inv f)" 350proof 351 fix x y::'b assume "x \<le> y" 352 from \<open>bij f\<close> obtain a b where x: "x = f a" and y: "y = f b" by(fastforce simp: bij_def surj_def) 353 show "inv f x \<le> inv f y" 354 proof (rule le_cases) 355 assume "a \<le> b" 356 thus ?thesis using \<open>bij f\<close> x y by(simp add: bij_def inv_f_f) 357 next 358 assume "b \<le> a" 359 hence "f b \<le> f a" by(rule monoD[OF \<open>mono f\<close>]) 360 hence "y \<le> x" using x y by simp 361 hence "x = y" using \<open>x \<le> y\<close> by auto 362 thus ?thesis by simp 363 qed 364qed 365 366lemma mono_bij_Inf: 367 fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder" 368 assumes "mono f" "bij f" 369 shows "f (Inf A) = Inf (f`A)" 370proof - 371 have "surj f" using \<open>bij f\<close> by (auto simp: bij_betw_def) 372 have *: "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))" 373 using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp 374 have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))" 375 using monoD[OF \<open>mono f\<close> *] by(simp add: surj_f_inv_f[OF \<open>surj f\<close>]) 376 also have "... = f(Inf A)" 377 using assms by (simp add: bij_is_inj) 378 finally show ?thesis using mono_Inf[OF assms(1), of A] by auto 379qed 380 381lemma finite_fun_UNIVD1: 382 assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)" 383 and card: "card (UNIV :: 'b set) \<noteq> Suc 0" 384 shows "finite (UNIV :: 'a set)" 385proof - 386 let ?UNIV_b = "UNIV :: 'b set" 387 from fin have "finite ?UNIV_b" 388 by (rule finite_fun_UNIVD2) 389 with card have "card ?UNIV_b \<ge> Suc (Suc 0)" 390 by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff) 391 then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))" 392 by simp 393 then obtain b1 b2 :: 'b where b1b2: "b1 \<noteq> b2" 394 by (auto simp: card_Suc_eq) 395 from fin have fin': "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" 396 by (rule finite_imageI) 397 have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)" 398 proof (rule UNIV_eq_I) 399 fix x :: 'a 400 from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" 401 by (simp add: inv_into_def) 402 then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)" 403 by blast 404 qed 405 with fin' show ?thesis 406 by simp 407qed 408 409text \<open> 410 Every infinite set contains a countable subset. More precisely we 411 show that a set \<open>S\<close> is infinite if and only if there exists an 412 injective function from the naturals into \<open>S\<close>. 413 414 The ``only if'' direction is harder because it requires the 415 construction of a sequence of pairwise different elements of an 416 infinite set \<open>S\<close>. The idea is to construct a sequence of 417 non-empty and infinite subsets of \<open>S\<close> obtained by successively 418 removing elements of \<open>S\<close>. 419\<close> 420 421lemma infinite_countable_subset: 422 assumes inf: "\<not> finite S" 423 shows "\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S" 424 \<comment> \<open>Courtesy of Stephan Merz\<close> 425proof - 426 define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})" 427 define pick where "pick n = (SOME e. e \<in> Sseq n)" for n 428 have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n 429 by (induct n) (auto simp: Sseq_def inf) 430 then have **: "\<And>n. pick n \<in> Sseq n" 431 unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex) 432 with * have "range pick \<subseteq> S" by auto 433 moreover have "pick n \<noteq> pick (n + Suc m)" for m n 434 proof - 435 have "pick n \<notin> Sseq (n + Suc m)" 436 by (induct m) (auto simp add: Sseq_def pick_def) 437 with ** show ?thesis by auto 438 qed 439 then have "inj pick" 440 by (intro linorder_injI) (auto simp add: less_iff_Suc_add) 441 ultimately show ?thesis by blast 442qed 443 444lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S)" 445 \<comment> \<open>Courtesy of Stephan Merz\<close> 446 using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto 447 448lemma image_inv_into_cancel: 449 assumes surj: "f`A = A'" 450 and sub: "B' \<subseteq> A'" 451 shows "f `((inv_into A f)`B') = B'" 452 using assms 453proof (auto simp: f_inv_into_f) 454 let ?f' = "inv_into A f" 455 fix a' 456 assume *: "a' \<in> B'" 457 with sub have "a' \<in> A'" by auto 458 with surj have "a' = f (?f' a')" 459 by (auto simp: f_inv_into_f) 460 with * show "a' \<in> f ` (?f' ` B')" by blast 461qed 462 463lemma inv_into_inv_into_eq: 464 assumes "bij_betw f A A'" 465 and a: "a \<in> A" 466 shows "inv_into A' (inv_into A f) a = f a" 467proof - 468 let ?f' = "inv_into A f" 469 let ?f'' = "inv_into A' ?f'" 470 from assms have *: "bij_betw ?f' A' A" 471 by (auto simp: bij_betw_inv_into) 472 with a obtain a' where a': "a' \<in> A'" "?f' a' = a" 473 unfolding bij_betw_def by force 474 with a * have "?f'' a = a'" 475 by (auto simp: f_inv_into_f bij_betw_def) 476 moreover from assms a' have "f a = a'" 477 by (auto simp: bij_betw_def) 478 ultimately show "?f'' a = f a" by simp 479qed 480 481lemma inj_on_iff_surj: 482 assumes "A \<noteq> {}" 483 shows "(\<exists>f. inj_on f A \<and> f ` A \<subseteq> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)" 484proof safe 485 fix f 486 assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'" 487 let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'" 488 let ?csi = "\<lambda>a. a \<in> A" 489 let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)" 490 have "?g ` A' = A" 491 proof 492 show "?g ` A' \<subseteq> A" 493 proof clarify 494 fix a' 495 assume *: "a' \<in> A'" 496 show "?g a' \<in> A" 497 proof (cases "a' \<in> f ` A") 498 case True 499 then obtain a where "?phi a' a" by blast 500 then have "?phi a' (SOME a. ?phi a' a)" 501 using someI[of "?phi a'" a] by blast 502 with True show ?thesis by auto 503 next 504 case False 505 with assms have "?csi (SOME a. ?csi a)" 506 using someI_ex[of ?csi] by blast 507 with False show ?thesis by auto 508 qed 509 qed 510 next 511 show "A \<subseteq> ?g ` A'" 512 proof - 513 have "?g (f a) = a \<and> f a \<in> A'" if a: "a \<in> A" for a 514 proof - 515 let ?b = "SOME aa. ?phi (f a) aa" 516 from a have "?phi (f a) a" by auto 517 then have *: "?phi (f a) ?b" 518 using someI[of "?phi(f a)" a] by blast 519 then have "?g (f a) = ?b" using a by auto 520 moreover from inj * a have "a = ?b" 521 by (auto simp add: inj_on_def) 522 ultimately have "?g(f a) = a" by simp 523 with incl a show ?thesis by auto 524 qed 525 then show ?thesis by force 526 qed 527 qed 528 then show "\<exists>g. g ` A' = A" by blast 529next 530 fix g 531 let ?f = "inv_into A' g" 532 have "inj_on ?f (g ` A')" 533 by (auto simp: inj_on_inv_into) 534 moreover have "?f (g a') \<in> A'" if a': "a' \<in> A'" for a' 535 proof - 536 let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'" 537 from a' have "?phi a'" by auto 538 then have "?phi (SOME b'. ?phi b')" 539 using someI[of ?phi] by blast 540 then show ?thesis by (auto simp: inv_into_def) 541 qed 542 ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" 543 by auto 544qed 545 546lemma Ex_inj_on_UNION_Sigma: 547 "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i))" 548proof 549 let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i" 550 let ?sm = "\<lambda>a. SOME i. ?phi a i" 551 let ?f = "\<lambda>a. (?sm a, a)" 552 have "inj_on ?f (\<Union>i \<in> I. A i)" 553 by (auto simp: inj_on_def) 554 moreover 555 have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a 556 using that someI[of "?phi a" i] by auto 557 then have "?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)" 558 by auto 559 ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)" 560 by auto 561qed 562 563lemma inv_unique_comp: 564 assumes fg: "f \<circ> g = id" 565 and gf: "g \<circ> f = id" 566 shows "inv f = g" 567 using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) 568 569lemma subset_image_inj: 570 "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)" 571proof safe 572 show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U" 573 if "S \<subseteq> f ` T" 574 proof - 575 from that [unfolded subset_image_iff subset_iff] 576 obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)" 577 by (auto simp add: image_iff Bex_def choice_iff') 578 show ?thesis 579 proof (intro exI conjI) 580 show "g ` S \<subseteq> T" 581 by (simp add: g image_subsetI) 582 show "inj_on f (g ` S)" 583 using g by (auto simp: inj_on_def) 584 show "S = f ` (g ` S)" 585 using g image_subset_iff by auto 586 qed 587 qed 588qed blast 589 590 591subsection \<open>Other Consequences of Hilbert's Epsilon\<close> 592 593text \<open>Hilbert's Epsilon and the \<^term>\<open>split\<close> Operator\<close> 594 595text \<open>Looping simprule!\<close> 596lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))" 597 by simp 598 599lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))" 600 by (simp add: split_def) 601 602lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \<and> y = y') = (x, y)" 603 by blast 604 605 606text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close> 607lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> r)" 608 (is "_ \<longleftrightarrow> \<not> ?ex") 609proof 610 assume "wf r" 611 show "\<not> ?ex" 612 proof 613 assume ?ex 614 then obtain f where f: "(f (Suc i), f i) \<in> r" for i 615 by blast 616 from \<open>wf r\<close> have minimal: "x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" for x Q 617 by (auto simp: wf_eq_minimal) 618 let ?Q = "{w. \<exists>i. w = f i}" 619 fix n 620 have "f n \<in> ?Q" by blast 621 from minimal [OF this] obtain j where "(y, f j) \<in> r \<Longrightarrow> y \<notin> ?Q" for y by blast 622 with this [OF \<open>(f (Suc j), f j) \<in> r\<close>] have "f (Suc j) \<notin> ?Q" by simp 623 then show False by blast 624 qed 625next 626 assume "\<not> ?ex" 627 then show "wf r" 628 proof (rule contrapos_np) 629 assume "\<not> wf r" 630 then obtain Q x where x: "x \<in> Q" and rec: "z \<in> Q \<Longrightarrow> \<exists>y. (y, z) \<in> r \<and> y \<in> Q" for z 631 by (auto simp add: wf_eq_minimal) 632 obtain descend :: "nat \<Rightarrow> 'a" 633 where descend_0: "descend 0 = x" 634 and descend_Suc: "descend (Suc n) = (SOME y. y \<in> Q \<and> (y, descend n) \<in> r)" for n 635 by (rule that [of "rec_nat x (\<lambda>_ rec. (SOME y. y \<in> Q \<and> (y, rec) \<in> r))"]) simp_all 636 have descend_Q: "descend n \<in> Q" for n 637 proof (induct n) 638 case 0 639 with x show ?case by (simp only: descend_0) 640 next 641 case Suc 642 then show ?case by (simp only: descend_Suc) (rule someI2_ex; use rec in blast) 643 qed 644 have "(descend (Suc i), descend i) \<in> r" for i 645 by (simp only: descend_Suc) (rule someI2_ex; use descend_Q rec in blast) 646 then show "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r" by blast 647 qed 648qed 649 650lemma wf_no_infinite_down_chainE: 651 assumes "wf r" 652 obtains k where "(f (Suc k), f k) \<notin> r" 653 using assms wf_iff_no_infinite_down_chain[of r] by blast 654 655 656text \<open>A dynamically-scoped fact for TFL\<close> 657lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)" 658 by (blast intro: someI) 659 660 661subsection \<open>An aside: bounded accessible part\<close> 662 663text \<open>Finite monotone eventually stable sequences\<close> 664 665lemma finite_mono_remains_stable_implies_strict_prefix: 666 fixes f :: "nat \<Rightarrow> 'a::order" 667 assumes S: "finite (range f)" "mono f" 668 and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))" 669 shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)" 670 using assms 671proof - 672 have "\<exists>n. f n = f (Suc n)" 673 proof (rule ccontr) 674 assume "\<not> ?thesis" 675 then have "\<And>n. f n \<noteq> f (Suc n)" by auto 676 with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)" 677 by (auto simp: le_less mono_iff_le_Suc) 678 with lift_Suc_mono_less_iff[of f] have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" 679 by auto 680 have "inj f" 681 proof (intro injI) 682 fix x y 683 assume "f x = f y" 684 then show "x = y" 685 by (cases x y rule: linorder_cases) (auto dest: *) 686 qed 687 with \<open>finite (range f)\<close> have "finite (UNIV::nat set)" 688 by (rule finite_imageD) 689 then show False by simp 690 qed 691 then obtain n where n: "f n = f (Suc n)" .. 692 define N where "N = (LEAST n. f n = f (Suc n))" 693 have N: "f N = f (Suc N)" 694 unfolding N_def using n by (rule LeastI) 695 show ?thesis 696 proof (intro exI[of _ N] conjI allI impI) 697 fix n 698 assume "N \<le> n" 699 then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N" 700 proof (induct rule: dec_induct) 701 case base 702 then show ?case by simp 703 next 704 case (step n) 705 then show ?case 706 using eq [rule_format, of "n - 1"] N 707 by (cases n) (auto simp add: le_Suc_eq) 708 qed 709 from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto 710 next 711 fix n m :: nat 712 assume "m < n" "n \<le> N" 713 then show "f m < f n" 714 proof (induct rule: less_Suc_induct) 715 case (1 i) 716 then have "i < N" by simp 717 then have "f i \<noteq> f (Suc i)" 718 unfolding N_def by (rule not_less_Least) 719 with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le) 720 next 721 case 2 722 then show ?case by simp 723 qed 724 qed 725qed 726 727lemma finite_mono_strict_prefix_implies_finite_fixpoint: 728 fixes f :: "nat \<Rightarrow> 'a set" 729 assumes S: "\<And>i. f i \<subseteq> S" "finite S" 730 and ex: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)" 731 shows "f (card S) = (\<Union>n. f n)" 732proof - 733 from ex obtain N where inj: "\<And>n m. n \<le> N \<Longrightarrow> m \<le> N \<Longrightarrow> m < n \<Longrightarrow> f m \<subset> f n" 734 and eq: "\<forall>n\<ge>N. f N = f n" 735 by atomize auto 736 have "i \<le> N \<Longrightarrow> i \<le> card (f i)" for i 737 proof (induct i) 738 case 0 739 then show ?case by simp 740 next 741 case (Suc i) 742 with inj [of "Suc i" i] have "(f i) \<subset> (f (Suc i))" by auto 743 moreover have "finite (f (Suc i))" using S by (rule finite_subset) 744 ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono) 745 with Suc inj show ?case by auto 746 qed 747 then have "N \<le> card (f N)" by simp 748 also have "\<dots> \<le> card S" using S by (intro card_mono) 749 finally have "f (card S) = f N" using eq by auto 750 then show ?thesis 751 using eq inj [of N] 752 apply auto 753 apply (case_tac "n < N") 754 apply (auto simp: not_less) 755 done 756qed 757 758 759subsection \<open>More on injections, bijections, and inverses\<close> 760 761locale bijection = 762 fixes f :: "'a \<Rightarrow> 'a" 763 assumes bij: "bij f" 764begin 765 766lemma bij_inv: "bij (inv f)" 767 using bij by (rule bij_imp_bij_inv) 768 769lemma surj [simp]: "surj f" 770 using bij by (rule bij_is_surj) 771 772lemma inj: "inj f" 773 using bij by (rule bij_is_inj) 774 775lemma surj_inv [simp]: "surj (inv f)" 776 using inj by (rule inj_imp_surj_inv) 777 778lemma inj_inv: "inj (inv f)" 779 using surj by (rule surj_imp_inj_inv) 780 781lemma eqI: "f a = f b \<Longrightarrow> a = b" 782 using inj by (rule injD) 783 784lemma eq_iff [simp]: "f a = f b \<longleftrightarrow> a = b" 785 by (auto intro: eqI) 786 787lemma eq_invI: "inv f a = inv f b \<Longrightarrow> a = b" 788 using inj_inv by (rule injD) 789 790lemma eq_inv_iff [simp]: "inv f a = inv f b \<longleftrightarrow> a = b" 791 by (auto intro: eq_invI) 792 793lemma inv_left [simp]: "inv f (f a) = a" 794 using inj by (simp add: inv_f_eq) 795 796lemma inv_comp_left [simp]: "inv f \<circ> f = id" 797 by (simp add: fun_eq_iff) 798 799lemma inv_right [simp]: "f (inv f a) = a" 800 using surj by (simp add: surj_f_inv_f) 801 802lemma inv_comp_right [simp]: "f \<circ> inv f = id" 803 by (simp add: fun_eq_iff) 804 805lemma inv_left_eq_iff [simp]: "inv f a = b \<longleftrightarrow> f b = a" 806 by auto 807 808lemma inv_right_eq_iff [simp]: "b = inv f a \<longleftrightarrow> f b = a" 809 by auto 810 811end 812 813lemma infinite_imp_bij_betw: 814 assumes infinite: "\<not> finite A" 815 shows "\<exists>h. bij_betw h A (A - {a})" 816proof (cases "a \<in> A") 817 case False 818 then have "A - {a} = A" by blast 819 then show ?thesis 820 using bij_betw_id[of A] by auto 821next 822 case True 823 with infinite have "\<not> finite (A - {a})" by auto 824 with infinite_iff_countable_subset[of "A - {a}"] 825 obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast 826 define g where "g n = (if n = 0 then a else f (Suc n))" for n 827 define A' where "A' = g ` UNIV" 828 have *: "\<forall>y. f y \<noteq> a" using 2 by blast 829 have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV" 830 apply (auto simp add: True g_def [abs_def]) 831 apply (unfold inj_on_def) 832 apply (intro ballI impI) 833 apply (case_tac "x = 0") 834 apply (auto simp add: 2) 835 proof - 836 fix y 837 assume "a = (if y = 0 then a else f (Suc y))" 838 then show "y = 0" by (cases "y = 0") (use * in auto) 839 next 840 fix x y 841 assume "f (Suc x) = (if y = 0 then a else f (Suc y))" 842 with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def) 843 next 844 fix n 845 from 2 show "f (Suc n) \<in> A" by blast 846 qed 847 then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A" 848 using inj_on_imp_bij_betw[of g] by (auto simp: A'_def) 849 then have 5: "bij_betw (inv g) A' UNIV" 850 by (auto simp add: bij_betw_inv_into) 851 from 3 obtain n where n: "g n = a" by auto 852 have 6: "bij_betw g (UNIV - {n}) (A' - {a})" 853 by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>) 854 define v where "v m = (if m < n then m else Suc m)" for m 855 have 7: "bij_betw v UNIV (UNIV - {n})" 856 proof (unfold bij_betw_def inj_on_def, intro conjI, clarify) 857 fix m1 m2 858 assume "v m1 = v m2" 859 then show "m1 = m2" 860 apply (cases "m1 < n") 861 apply (cases "m2 < n") 862 apply (auto simp: inj_on_def v_def [abs_def]) 863 apply (cases "m2 < n") 864 apply auto 865 done 866 next 867 show "v ` UNIV = UNIV - {n}" 868 proof (auto simp: v_def [abs_def]) 869 fix m 870 assume "m \<noteq> n" 871 assume *: "m \<notin> Suc ` {m'. \<not> m' < n}" 872 have False if "n \<le> m" 873 proof - 874 from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto 875 from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" .. 876 with ** have "n \<le> m'" by auto 877 with m' * show ?thesis by auto 878 qed 879 then show "m < n" by force 880 qed 881 qed 882 define h' where "h' = g \<circ> v \<circ> (inv g)" 883 with 5 6 7 have 8: "bij_betw h' A' (A' - {a})" 884 by (auto simp add: bij_betw_trans) 885 define h where "h b = (if b \<in> A' then h' b else b)" for b 886 then have "\<forall>b \<in> A'. h b = h' b" by simp 887 with 8 have "bij_betw h A' (A' - {a})" 888 using bij_betw_cong[of A' h] by auto 889 moreover 890 have "\<forall>b \<in> A - A'. h b = b" by (auto simp: h_def) 891 then have "bij_betw h (A - A') (A - A')" 892 using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto 893 moreover 894 from 4 have "(A' \<inter> (A - A') = {} \<and> A' \<union> (A - A') = A) \<and> 895 ((A' - {a}) \<inter> (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})" 896 by blast 897 ultimately have "bij_betw h A (A - {a})" 898 using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp 899 then show ?thesis by blast 900qed 901 902lemma infinite_imp_bij_betw2: 903 assumes "\<not> finite A" 904 shows "\<exists>h. bij_betw h A (A \<union> {a})" 905proof (cases "a \<in> A") 906 case True 907 then have "A \<union> {a} = A" by blast 908 then show ?thesis using bij_betw_id[of A] by auto 909next 910 case False 911 let ?A' = "A \<union> {a}" 912 from False have "A = ?A' - {a}" by blast 913 moreover from assms have "\<not> finite ?A'" by auto 914 ultimately obtain f where "bij_betw f ?A' A" 915 using infinite_imp_bij_betw[of ?A' a] by auto 916 then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into) 917 then show ?thesis by auto 918qed 919 920lemma bij_betw_inv_into_left: "bij_betw f A A' \<Longrightarrow> a \<in> A \<Longrightarrow> inv_into A f (f a) = a" 921 unfolding bij_betw_def by clarify (rule inv_into_f_f) 922 923lemma bij_betw_inv_into_right: "bij_betw f A A' \<Longrightarrow> a' \<in> A' \<Longrightarrow> f (inv_into A f a') = a'" 924 unfolding bij_betw_def using f_inv_into_f by force 925 926lemma bij_betw_inv_into_subset: 927 "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw (inv_into A f) B' B" 928 by (auto simp: bij_betw_def intro: inj_on_inv_into) 929 930 931subsection \<open>Specification package -- Hilbertized version\<close> 932 933lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c" 934 by (simp only: someI_ex) 935 936ML_file \<open>Tools/choice_specification.ML\<close> 937 938subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close> 939 940context complete_distrib_lattice 941begin 942 943lemma Sup_Inf: "\<Squnion> (Inf ` A) = \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})" 944proof (rule antisym) 945 show "\<Squnion> (Inf ` A) \<le> \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})" 946 apply (rule Sup_least, rule INF_greatest) 947 using Inf_lower2 Sup_upper by auto 948next 949 show "\<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B}) \<le> \<Squnion> (Inf ` A)" 950 proof (simp add: Inf_Sup, rule SUP_least, simp, safe) 951 fix f 952 assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y" 953 from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z" 954 by auto 955 show "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)" 956 proof (cases "\<exists> Z \<in> A . \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z") 957 case True 958 from this obtain Z where [simp]: "Z \<in> A" and A: "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z" 959 by blast 960 have B: "... \<le> \<Squnion>(Inf ` A)" 961 by (simp add: SUP_upper) 962 from A and B show ?thesis 963 by simp 964 next 965 case False 966 from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x" 967 using Inf_greatest by blast 968 define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x)" 969 have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" 970 using X by (simp add: F_def, rule someI2_ex, auto) 971 have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y" 972 using X by (simp add: F_def, rule someI2_ex, auto) 973 from C and B obtain Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z" 974 by blast 975 from E and D have W: "\<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Z" 976 by simp 977 have "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> f (F ` A)" 978 apply (rule INF_lower) 979 using C by blast 980 from this and W and Y show ?thesis 981 by simp 982 qed 983 qed 984qed 985 986lemma dual_complete_distrib_lattice: 987 "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>" 988 apply (rule class.complete_distrib_lattice.intro) 989 apply (fact dual_complete_lattice) 990 by (simp add: class.complete_distrib_lattice_axioms_def Sup_Inf) 991 992lemma sup_Inf: "a \<squnion> \<Sqinter>B = \<Sqinter>((\<squnion>) a ` B)" 993proof (rule antisym) 994 show "a \<squnion> \<Sqinter>B \<le> \<Sqinter>((\<squnion>) a ` B)" 995 apply (rule INF_greatest) 996 using Inf_lower sup.mono by fastforce 997next 998 have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})" 999 by (rule INF_greatest, auto simp add: INF_lower) 1000 also have "... = \<Squnion>(Inf ` {{a}, B})" 1001 by (unfold Sup_Inf, simp) 1002 finally show "\<Sqinter>((\<squnion>) a ` B) \<le> a \<squnion> \<Sqinter>B" 1003 by simp 1004qed 1005 1006lemma inf_Sup: "a \<sqinter> \<Squnion>B = \<Squnion>((\<sqinter>) a ` B)" 1007 using dual_complete_distrib_lattice 1008 by (rule complete_distrib_lattice.sup_Inf) 1009 1010lemma INF_SUP: "(\<Sqinter>y. \<Squnion>x. P x y) = (\<Squnion>f. \<Sqinter>x. P (f x) x)" 1011proof (rule antisym) 1012 show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)" 1013 by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast) 1014next 1015 have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B") 1016 proof (rule INF_greatest, clarsimp) 1017 fix y 1018 have "?A \<le> (SUP x. P x y)" 1019 by (rule INF_lower, simp) 1020 also have "... \<le> Sup {uu. \<exists>x. uu = P x y}" 1021 by (simp add: full_SetCompr_eq) 1022 finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}" 1023 by simp 1024 qed 1025 also have "... \<le> (SUP x. INF y. P (x y) y)" 1026 proof (subst Inf_Sup, rule SUP_least, clarsimp) 1027 fix f 1028 assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y" 1029 1030 have " \<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le> 1031 (\<Sqinter>y. P (SOME x. f {P x y |x. True} = P x y) y)" 1032 proof (rule INF_greatest, clarsimp) 1033 fix y 1034 have "(INF x\<in>{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}" 1035 by (rule INF_lower, blast) 1036 also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y" 1037 apply (rule someI2_ex) 1038 using A by auto 1039 finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le> 1040 P (SOME x. f {uu. \<exists>x. uu = P x y} = P x y) y" 1041 by simp 1042 qed 1043 also have "... \<le> (SUP x. INF y. P (x y) y)" 1044 by (rule SUP_upper, simp) 1045 finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le> (\<Squnion>x. \<Sqinter>y. P (x y) y)" 1046 by simp 1047 qed 1048 finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)" 1049 by simp 1050qed 1051 1052lemma INF_SUP_set: "(\<Sqinter>B\<in>A. \<Squnion>(g ` B)) = (\<Squnion>B\<in>{f ` A |f. \<forall>C\<in>A. f C \<in> C}. \<Sqinter>(g ` B))" 1053proof (rule antisym) 1054 have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" and "B \<in> A" 1055 for f and B 1056 using that by (auto intro: SUP_upper2 INF_lower2) 1057 then show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)" 1058 by (auto intro!: SUP_least INF_greatest simp add: image_comp) 1059next 1060 show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)" 1061 proof (cases "{} \<in> A") 1062 case True 1063 then show ?thesis 1064 by (rule INF_lower2) simp_all 1065 next 1066 case False 1067 have *: "\<And>f B. B \<in> A \<Longrightarrow> f B \<in> B \<Longrightarrow> 1068 (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (f B)" 1069 by (rule INF_lower2, auto) 1070 have **: "\<And>f B. B \<in> A \<Longrightarrow> f B \<notin> B \<Longrightarrow> 1071 (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> B)" 1072 by (rule INF_lower2, auto) 1073 have ****: "\<And>f B. B \<in> A \<Longrightarrow> 1074 (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) 1075 \<le> (if f B \<in> B then g (f B) else g (SOME x. x \<in> B))" 1076 by (rule INF_lower2) auto 1077 have ***: "\<And>x. (\<Sqinter>B. if B \<in> A then if x B \<in> B then g (x B) else \<bottom> else \<top>) 1078 \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)" 1079 proof - 1080 fix x 1081 define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))" 1082 have B: "(\<forall>Y\<in>A. F Y \<in> Y)" 1083 using False some_in_eq F_def by auto 1084 have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}" 1085 using B by blast 1086 show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)" 1087 using A apply (rule SUP_upper2) 1088 apply (rule INF_greatest) 1089 using * ** 1090 apply (auto simp add: F_def) 1091 done 1092 qed 1093 1094 {fix x 1095 have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)" 1096 proof (cases "x \<in> A") 1097 case True 1098 then show ?thesis 1099 apply (rule INF_lower2) 1100 apply (rule SUP_least) 1101 apply (rule SUP_upper2) 1102 apply auto 1103 done 1104 next 1105 case False 1106 then show ?thesis by simp 1107 qed 1108 } 1109 from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)" 1110 by (rule INF_greatest) 1111 also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)" 1112 by (simp only: INF_SUP) 1113 also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)" 1114 apply (rule SUP_least) 1115 using *** apply simp 1116 done 1117 finally show ?thesis by simp 1118 qed 1119qed 1120 1121lemma SUP_INF: "(\<Squnion>y. \<Sqinter>x. P x y) = (\<Sqinter>x. \<Squnion>y. P (x y) y)" 1122 using dual_complete_distrib_lattice 1123 by (rule complete_distrib_lattice.INF_SUP) 1124 1125lemma SUP_INF_set: "(\<Squnion>x\<in>A. \<Sqinter> (g ` x)) = (\<Sqinter>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Squnion> (g ` x))" 1126 using dual_complete_distrib_lattice 1127 by (rule complete_distrib_lattice.INF_SUP_set) 1128 1129end 1130 1131(*properties of the former complete_distrib_lattice*) 1132context complete_distrib_lattice 1133begin 1134 1135lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" 1136 by (simp add: sup_Inf image_comp) 1137 1138lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" 1139 by (simp add: inf_Sup image_comp) 1140 1141lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)" 1142 by (simp add: sup_Inf sup_commute) 1143 1144lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)" 1145 by (simp add: inf_Sup inf_commute) 1146 1147lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)" 1148 by (simp add: sup_INF sup_commute) 1149 1150lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)" 1151 by (simp add: inf_SUP inf_commute) 1152 1153lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)" 1154 by (simp only: Inf_sup INF_top_conv) 1155 1156lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)" 1157 by (simp only: Sup_inf SUP_bot_conv) 1158 1159lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)" 1160 by (subst INF_commute) (simp add: sup_INF INF_sup) 1161 1162lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)" 1163 by (subst SUP_commute) (simp add: inf_SUP SUP_inf) 1164 1165end 1166 1167context complete_boolean_algebra 1168begin 1169 1170lemma dual_complete_boolean_algebra: 1171 "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus" 1172 by (rule class.complete_boolean_algebra.intro, 1173 rule dual_complete_distrib_lattice, 1174 rule dual_boolean_algebra) 1175end 1176 1177 1178 1179instantiation set :: (type) complete_distrib_lattice 1180begin 1181instance proof (standard, clarsimp) 1182 fix A :: "(('a set) set) set" 1183 fix x::'a 1184 define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))" 1185 assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X" 1186 1187 from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)" 1188 apply (safe, simp add: F_def) 1189 by (rule someI2_ex, auto) 1190 1191 have C: "(\<forall>Y\<in>A. F Y \<in> Y)" 1192 apply (simp add: F_def, safe) 1193 apply (rule someI2_ex) 1194 using A by auto 1195 1196 have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))" 1197 using C by blast 1198 1199 from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)" 1200 by auto 1201qed 1202end 1203 1204instance set :: (type) complete_boolean_algebra .. 1205 1206instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice 1207begin 1208instance by standard (simp add: le_fun_def INF_SUP_set image_comp) 1209end 1210 1211instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. 1212 1213context complete_linorder 1214begin 1215 1216subclass complete_distrib_lattice 1217proof (standard, rule ccontr) 1218 fix A 1219 assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1220 then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1221 by (simp add: not_le) 1222 show False 1223 proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})") 1224 case True 1225 from this obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1226 by blast 1227 1228 from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y" 1229 by (simp add: less_INF_D) 1230 1231 from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k" 1232 using local.less_Sup_iff by blast 1233 1234 define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)" 1235 1236 have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y" 1237 using B apply (simp add: F_def) 1238 by (rule someI2_ex, auto) 1239 1240 1241 have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" 1242 using B apply (simp add: F_def) 1243 by (rule someI2_ex, auto) 1244 1245 have "z \<le> Inf (F ` A)" 1246 by (simp add: D local.INF_greatest local.order.strict_implies_order) 1247 1248 also have "... \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1249 apply (rule SUP_upper, safe) 1250 using E by blast 1251 finally have "z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1252 by simp 1253 1254 from X and this show ?thesis 1255 using local.not_less by blast 1256 next 1257 case False 1258 from this have A: "\<And> z . \<Sqinter>(Sup ` A) \<le> z \<or> z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1259 using local.le_less_linear by blast 1260 1261 from C have "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < Sup Y" 1262 by (simp add: less_INF_D) 1263 1264 from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k" 1265 using local.less_Sup_iff by blast 1266 1267 define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k)" 1268 1269 have D: "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < F Y" 1270 using B apply (simp add: F_def) 1271 by (rule someI2_ex, auto) 1272 1273 have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" 1274 using B apply (simp add: F_def) 1275 by (rule someI2_ex, auto) 1276 1277 have "\<And> Y . Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> F Y" 1278 using D False local.leI by blast 1279 1280 from this have "\<Sqinter>(Sup ` A) \<le> Inf (F ` A)" 1281 by (simp add: local.INF_greatest) 1282 1283 also have "Inf (F ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1284 apply (rule SUP_upper, safe) 1285 using E by blast 1286 1287 finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 1288 by simp 1289 1290 from C and this show ?thesis 1291 using not_less by blast 1292 qed 1293 qed 1294end 1295 1296 1297 1298end 1299