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