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