SSL Hilbert_Choice.thy Sprache: Isabelle

(*  Title:      HOL/Hilbert_Choice.thy
    Author:     Lawrence C Paulson, Tobias Nipkow
    Author:     Viorel Preoteasa (Results about complete distributive lattices)
    Copyright   2001  University of Cambridge
*)

section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>

theory Hilbert_Choice
  imports Wellfounded
  keywords "specification" :: thy_goal_defn
begin

subsection \<open>Hilbert's epsilon\<close>

axiomatization Eps :: "('a \ bool) \ 'a"
  where someI: "P x \ P (Eps P)"

syntax (epsilon)
  "_Eps" :: "pttrn \ bool \ 'a" (\(\indent=3 notation=\binder \\\\_./ _)\ [0, 10] 10)
syntax (input)
  "_Eps" :: "pttrn \ bool \ 'a" (\(\indent=3 notation=\binder @\\@ _./ _)\ [0, 10] 10)
syntax
  "_Eps" :: "pttrn \ bool \ 'a" (\(\indent=3 notation=\binder SOME\\SOME _./ _)\ [0, 10] 10)

syntax_consts "_Eps" \<rightleftharpoons> Eps

translations
  "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"

print_translation \<open>
  [(\<^const_syntax>\<open>Eps\<close>, fn ctxt => fn [Abs abs] =>
      let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
      in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>

definition inv_into :: "'a set \ ('a \ 'b) \ ('b \ 'a)" where
"inv_into A f = (\x. SOME y. y \ A \ f y = x)"

lemma inv_into_def2: "inv_into A f x = (SOME y. y \ A \ f y = x)"
by(simp add: inv_into_def)

abbreviation inv :: "('a \ 'b) \ ('b \ 'a)" where
"inv \ inv_into UNIV"

subsection \<open>Hilbert's Epsilon-operator\<close>

lemma Eps_cong:
  assumes "\x. P x = Q x"
  shows "Eps P = Eps Q"
  using ext[of P Q, OF assms] by simp

text \<open>
  Easier to use than \<open>someI\<close> if the witness comes from an
  existential formula.
\<close>
lemma someI_ex [elim?]: "\x. P x \ P (SOME x. P x)"
  by (elim exE someI)

lemma some_eq_imp:
  assumes "Eps P = a" "P b" shows "P a"
  using assms someI_ex by force

text \<open>
  Easier to use than \<open>someI\<close> because the conclusion has only one
  occurrence of \<^term>\<open>P\<close>.
\<close>
lemma someI2: "P a \ (\x. P x \ Q x) \ Q (SOME x. P x)"
  by (blast intro: someI)

text \<open>
  Easier to use than \<open>someI2\<close> if the witness comes from an
  existential formula.
\<close>
lemma someI2_ex: "\a. P a \ (\x. P x \ Q x) \ Q (SOME x. P x)"
  by (blast intro: someI2)

lemma someI2_bex: "\a\A. P a \ (\x. x \ A \ P x \ Q x) \ Q (SOME x. x \ A \ P x)"
  by (blast intro: someI2)

lemma some_equality [intro]: "P a \ (\x. P x \ x = a) \ (SOME x. P x) = a"
  by (blast intro: someI2)

lemma some1_equality: "\!x. P x \ P a \ (SOME x. P x) = a"
  by blast

lemma some_eq_ex: "P (SOME x. P x) \ (\x. P x)"
  by (blast intro: someI)

lemma some_in_eq: "(SOME x. x \ A) \ A \ A \ {}"
  unfolding ex_in_conv[symmetric] by (rule some_eq_ex)

lemma some_eq_trivial [simp]: "(SOME y. y = x) = x"
  by (rule some_equality) (rule refl)

lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
  by (iprover intro: some_equality)

subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>

lemma choice: "\x. \y. Q x y \ \f. \x. Q x (f x)"
  by (fast elim: someI)

lemma bchoice: "\x\S. \y. Q x y \ \f. \x\S. Q x (f x)"
  by (fast elim: someI)

lemma choice_iff: "(\x. \y. Q x y) \ (\f. \x. Q x (f x))"
  by (fast elim: someI)

lemma choice_iff': "(\x. P x \ (\y. Q x y)) \ (\f. \x. P x \ Q x (f x))"
  by (fast elim: someI)

lemma bchoice_iff: "(\x\S. \y. Q x y) \ (\f. \x\S. Q x (f x))"
  by (fast elim: someI)

lemma bchoice_iff': "(\x\S. P x \ (\y. Q x y)) \ (\f. \x\S. P x \ Q x (f x))"
  by (fast elim: someI)

lemma dependent_nat_choice:
  assumes 1: "\x. P 0 x"
    and 2: "\x n. P n x \ \y. P (Suc n) y \ Q n x y"
  shows "\f. \n. P n (f n) \ Q n (f n) (f (Suc n))"
proof (intro exI allI conjI)
  fix n
  define f where "f = rec_nat (SOME x. P 0 x) (\n x. SOME y. P (Suc n) y \ Q n x y)"
  then have "P 0 (f 0)" "\n. P n (f n) \ P (Suc n) (f (Suc n)) \ Q n (f n) (f (Suc n))"
    using someI_ex[OF 1] someI_ex[OF 2] by simp_all
  then show "P n (f n)" "Q n (f n) (f (Suc n))"
    by (induct n) auto
qed

lemma finite_subset_Union:
  assumes "finite A" "A \ \\"
  obtains \<F> where "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
proof -
  have "\x\A. \B\\. x\B"
    using assms by blast
  then obtain f where f: "\x. x \ A \ f x \ \ \ x \ f x"
    by (auto simp add: bchoice_iff Bex_def)
  show thesis
  proof
    show "finite (f ` A)"
      using assms by auto
  qed (use f in auto)
qed

subsection \<open>Getting an element of a nonempty set\<close>

definition some_elem :: "'a set \ 'a"
  where "some_elem A = (SOME x. x \ A)"

lemma some_elem_eq [simp]: "some_elem {x} = x"
  by (simp add: some_elem_def)

lemma some_elem_nonempty: "A \ {} \ some_elem A \ A"
  unfolding some_elem_def by (auto intro: someI)

lemma is_singleton_some_elem: "is_singleton A \ A = {some_elem A}"
  by (auto simp: is_singleton_def)

lemma some_elem_image_unique:
  assumes "A \ {}"
    and *: "\y. y \ A \ f y = a"
  shows "some_elem (f ` A) = a"
  unfolding some_elem_def
proof (rule some1_equality)
  from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
  with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
  then show "a \ f ` A" by auto
  with * show "\!x. x \ f ` A"
    by auto
qed

subsection \<open>Function Inverse\<close>

lemma inv_def: "inv f = (\y. SOME x. f x = y)"
  by (simp add: inv_into_def)

lemma inv_into_into: "x \ f ` A \ inv_into A f x \ A"
  by (simp add: inv_into_def) (fast intro: someI2)

lemma inv_identity [simp]: "inv (\a. a) = (\a. a)"
  by (simp add: inv_def)

lemma inv_id [simp]: "inv id = id"
  by (simp add: id_def)

lemma inv_into_f_f [simp]: "inj_on f A \ x \ A \ inv_into A f (f x) = x"
  by (simp add: inv_into_def inj_on_def) (blast intro: someI2)

lemma inv_f_f: "inj f \ inv f (f x) = x"
  by simp

lemma f_inv_into_f: "y \ f`A \ f (inv_into A f y) = y"
  by (simp add: inv_into_def) (fast intro: someI2)

lemma inv_into_f_eq: "inj_on f A \ x \ A \ f x = y \ inv_into A f y = x"
  by (erule subst) (fast intro: inv_into_f_f)

lemma inv_f_eq: "inj f \ f x = y \ inv f y = x"
  by (simp add:inv_into_f_eq)

lemma inj_imp_inv_eq: "inj f \ \x. f (g x) = x \ inv f = g"
  by (blast intro: inv_into_f_eq)

text \<open>But is it useful?\<close>
lemma inj_transfer:
  assumes inj: "inj f"
    and minor: "\y. y \ range f \ P (inv f y)"
  shows "P x"
proof -
  have "f x \ range f" by auto
  then have "P(inv f (f x))" by (rule minor)
  then show "P x" by (simp add: inv_into_f_f [OF inj])
qed

lemma inj_iff: "inj f \ inv f \ f = id"
  by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f)

lemma inv_o_cancel[simp]: "inj f \ inv f \ f = id"
  by (simp add: inj_iff)

lemma o_inv_o_cancel[simp]: "inj f \ g \ inv f \ f = g"
  by (simp add: comp_assoc)

lemma inv_into_image_cancel[simp]: "inj_on f A \ S \ A \ inv_into A f ` f ` S = S"
  by (fastforce simp: image_def)

lemma inj_imp_surj_inv: "inj f \ surj (inv f)"
  by (blast intro!: surjI inv_into_f_f)

lemma surj_f_inv_f: "surj f \ f (inv f y) = y"
  by (simp add: f_inv_into_f)

lemma bij_inv_eq_iff: "bij p \ x = inv p y \ p x = y"
  using surj_f_inv_f[of p] by (auto simp add: bij_def)

lemma inv_into_injective:
  assumes eq: "inv_into A f x = inv_into A f y"
    and x: "x \ f`A"
    and y: "y \ f`A"
  shows "x = y"
proof -
  from eq have "f (inv_into A f x) = f (inv_into A f y)"
    by simp
  with x y show ?thesis
    by (simp add: f_inv_into_f)
qed

lemma inj_on_inv_into: "B \ f`A \ inj_on (inv_into A f) B"
  by (blast intro: inj_onI dest: inv_into_injective injD)

lemma inj_imp_bij_betw_inv: "inj f \ bij_betw (inv f) (f ` M) M"
  by (simp add: bij_betw_def image_subsetI inj_on_inv_into)

lemma bij_betw_inv_into: "bij_betw f A B \ bij_betw (inv_into A f) B A"
  by (auto simp add: bij_betw_def inj_on_inv_into)

lemma surj_imp_inj_inv: "surj f \ inj (inv f)"
  by (simp add: inj_on_inv_into)

lemma surj_iff: "surj f \ f \ inv f = id"
  by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])

lemma surj_iff_all: "surj f \ (\x. f (inv f x) = x)"
  by (simp add: o_def surj_iff fun_eq_iff)

lemma surj_imp_inv_eq:
  assumes "surj f" and gf: "\x. g (f x) = x"
  shows "inv f = g"
proof (rule ext)
  fix x
  have "g (f (inv f x)) = inv f x"
    by (rule gf)
  then show "inv f x = g x"
    by (simp add: surj_f_inv_f \<open>surj f\<close>)
qed

lemma bij_imp_bij_inv: "bij f \ bij (inv f)"
  by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)

lemma inv_equality: "(\x. g (f x) = x) \ (\y. f (g y) = y) \ inv f = g"
  by (rule ext) (auto simp add: inv_into_def)

lemma inv_inv_eq: "bij f \ inv (inv f) = f"
  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)

text \<open>
  \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such
  that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close>
  that \<open>inv f\<close> could be any function at all, including the identity function.
  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
  (inv f) = f\<close> all fail.
\<close>

lemma inv_into_comp:
  "inj_on f (g ` A) \ inj_on g A \ x \ f ` g ` A \
    inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
  by (auto simp: f_inv_into_f inv_into_into intro: inv_into_f_eq comp_inj_on)

lemma o_inv_distrib: "bij f \ bij g \ inv (f \ g) = inv g \ inv f"
  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)

lemma image_f_inv_f: "surj f \ f ` (inv f ` A) = A"
  by (simp add: surj_f_inv_f image_comp comp_def)

lemma image_inv_f_f: "inj f \ inv f ` (f ` A) = A"
  by simp

lemma bij_image_Collect_eq:
  assumes "bij f"
  shows "f ` Collect P = {y. P (inv f y)}"
proof
  show "f ` Collect P \ {y. P (inv f y)}"
    using assms by (force simp add: bij_is_inj)
  show "{y. P (inv f y)} \ f ` Collect P"
    using assms by (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
qed

lemma bij_vimage_eq_inv_image:
  assumes "bij f"
  shows "f -` A = inv f ` A"
proof
  show "f -` A \ inv f ` A"
    using assms by (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
  show "inv f ` A \ f -` A"
    using assms by (auto simp add: bij_is_surj [THEN surj_f_inv_f])
qed

lemma inv_fn_o_fn_is_id:
  fixes f::"'a \ 'a"
  assumes "bij f"
  shows "((inv f)^^n) o (f^^n) = (\x. x)"
proof -
  have "((inv f)^^n)((f^^n) x) = x" for x n
  proof (induction n)
    case (Suc n)
    have *: "(inv f) (f y) = y" for y
      by (simp add: assms bij_is_inj)
    have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
      by (simp add: funpow_swap1)
    also have "... = (inv f^^n) ((f^^n) x)"
      using * by auto
    also have "... = x" using Suc.IH by auto
    finally show ?case by simp
  qed (auto)
  then show ?thesis unfolding o_def by blast
qed

lemma fn_o_inv_fn_is_id:
  fixes f::"'a \ 'a"
  assumes "bij f"
  shows "(f^^n) o ((inv f)^^n) = (\x. x)"
proof -
  have "(f^^n) (((inv f)^^n) x) = x" for x n
  proof (induction n)
    case (Suc n)
    have *: "f(inv f y) = y" for y
      using bij_inv_eq_iff[OF assms] by auto
    have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
      by (simp add: funpow_swap1)
    also have "... = (f^^n) ((inv f^^n) x)"
      using * by auto
    also have "... = x" using Suc.IH by auto
    finally show ?case by simp
  qed (auto)
  then show ?thesis unfolding o_def by blast
qed

lemma inv_fn:
  fixes f::"'a \ 'a"
  assumes "bij f"
  shows "inv (f^^n) = ((inv f)^^n)"
proof -
  have "inv (f^^n) x = ((inv f)^^n) x" for x
  proof (rule inv_into_f_eq)
    show "inj (f ^^ n)"
      by (simp add: inj_fn[OF bij_is_inj [OF assms]])
    show "(f ^^ n) ((inv f ^^ n) x) = x"
      using fn_o_inv_fn_is_id[OF assms, THEN fun_cong] by force
  qed auto
  then show ?thesis by auto
qed

lemma funpow_inj_finite: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
  assumes \<open>inj p\<close> \<open>finite {y. \<exists>n. y = (p ^^ n) x}\<close>
  obtains n where \<open>n > 0\<close> \<open>(p ^^ n) x = x\<close>
proof -
  have \<open>infinite (UNIV :: nat set)\<close>
    by simp
  moreover have \<open>{y. \<exists>n. y = (p ^^ n) x} = (\<lambda>n. (p ^^ n) x) ` UNIV\<close>
    by auto
  with assms have \<open>finite \<dots>\<close>
    by simp
  ultimately have "\n \ UNIV. \ finite {m \ UNIV. (p ^^ m) x = (p ^^ n) x}"
    by (rule pigeonhole_infinite)
  then obtain n where "infinite {m. (p ^^ m) x = (p ^^ n) x}" by auto
  then have "infinite ({m. (p ^^ m) x = (p ^^ n) x} - {n})" by auto
  then have "({m. (p ^^ m) x = (p ^^ n) x} - {n}) \ {}"
    by (auto simp add: subset_singleton_iff)
  then obtain m where m: "(p ^^ m) x = (p ^^ n) x" "m \ n" by auto

  { fix m n assume "(p ^^ n) x = (p ^^ m) x" "m < n"
    have "(p ^^ (n - m)) x = inv (p ^^ m) ((p ^^ m) ((p ^^ (n - m)) x))"
      using \<open>inj p\<close> by (simp add: inv_f_f)
    also have "((p ^^ m) ((p ^^ (n - m)) x)) = (p ^^ n) x"
      using \<open>m < n\<close> funpow_add [of m \<open>n - m\<close> p] by simp
    also have "inv (p ^^ m) \ = x"
      using \<open>inj p\<close>  by (simp add: \<open>(p ^^ n) x = _\<close>)
    finally have "(p ^^ (n - m)) x = x" "0 < n - m"
      using \<open>m < n\<close> by auto }
  note general = this

  show thesis
  proof (cases m n rule: linorder_cases)
    case less
    then have \<open>n - m > 0\<close> \<open>(p ^^ (n - m)) x = x\<close>
      using general [of n m] m by simp_all
    then show thesis by (blast intro: that)
  next
    case equal
    then show thesis using m by simp
  next
    case greater
    then have \<open>m - n > 0\<close> \<open>(p ^^ (m - n)) x = x\<close>
      using general [of m n] m by simp_all
    then show thesis by (blast intro: that)
  qed
qed

lemma mono_inv:
  fixes f::"'a::linorder \ 'b::linorder"
  assumes "mono f" "bij f"
  shows "mono (inv f)"
proof
  fix x y::'b assume "x \ y"
  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)
  show "inv f x \ inv f y"
  proof (rule le_cases)
    assume "a \ b"
    thus ?thesis using  \<open>bij f\<close> x y by(simp add: bij_def inv_f_f)
  next
    assume "b \ a"
    hence "f b \ f a" by(rule monoD[OF \mono f\])
    hence "y \ x" using x y by simp
    hence "x = y" using \<open>x \<le> y\<close> by auto
    thus ?thesis by simp
  qed
qed

lemma strict_mono_inv_on_range:
  fixes f :: "'a::linorder \ 'b::order"
  assumes "strict_mono f"
  shows "strict_mono_on (range f) (inv f)"
proof (clarsimp simp: strict_mono_on_def)
  fix x y
  assume "f x < f y"
  then show "inv f (f x) < inv f (f y)"
    using assms strict_mono_imp_inj_on strict_mono_less by fastforce
qed

lemma mono_bij_Inf:
  fixes f :: "'a::complete_linorder \ 'b::complete_linorder"
  assumes "mono f" "bij f"
  shows "f (Inf A) = Inf (f`A)"
proof -
  have "surj f" using \<open>bij f\<close> by (auto simp: bij_betw_def)
  have *: "(inv f) (Inf (f`A)) \ Inf ((inv f)`(f`A))"
    using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
  have "Inf (f`A) \ f (Inf ((inv f)`(f`A)))"
    using monoD[OF \<open>mono f\<close> *] by(simp add: surj_f_inv_f[OF \<open>surj f\<close>])
  also have "... = f(Inf A)"
    using assms by (simp add: bij_is_inj)
  finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
qed

lemma finite_fun_UNIVD1:
  assumes fin: "finite (UNIV :: ('a \ 'b) set)"
    and card: "card (UNIV :: 'b set) \ Suc 0"
  shows "finite (UNIV :: 'a set)"
proof -
  let ?UNIV_b = "UNIV :: 'b set"
  from fin have "finite ?UNIV_b"
    by (rule finite_fun_UNIVD2)
  with card have "card ?UNIV_b \ Suc (Suc 0)"
    by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff)
  then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))"
    by simp
  then obtain b1 b2 :: 'b where b1b2: "b1 \ b2"
    by (auto simp: card_Suc_eq)
  from fin have fin': "finite (range (\f :: 'a \ 'b. inv f b1))"
    by (rule finite_imageI)
  have "UNIV = range (\f :: 'a \ 'b. inv f b1)"
  proof (rule UNIV_eq_I)
    fix x :: 'a
    from b1b2 have "x = inv (\y. if y = x then b1 else b2) b1"
      by (simp add: inv_into_def)
    then show "x \ range (\f::'a \ 'b. inv f b1)"
      by blast
  qed
  with fin' show ?thesis
    by simp
qed

text \<open>
  Every infinite set contains a countable subset. More precisely we
  show that a set \<open>S\<close> is infinite if and only if there exists an
  injective function from the naturals into \<open>S\<close>.

  The ``only if'' direction is harder because it requires the
  construction of a sequence of pairwise different elements of an
  infinite set \<open>S\<close>. The idea is to construct a sequence of
  non-empty and infinite subsets of \<open>S\<close> obtained by successively
  removing elements of \<open>S\<close>.
\<close>

lemma infinite_countable_subset:
  assumes inf: "\ finite S"
  shows "\f::nat \ 'a. inj f \ range f \ S"
  \<comment> \<open>Courtesy of Stephan Merz\<close>
proof -
  define Sseq where "Sseq = rec_nat S (\n T. T - {SOME e. e \ T})"
  define pick where "pick n = (SOME e. e \ Sseq n)" for n
  have *: "Sseq n \ S" "\ finite (Sseq n)" for n
    by (induct n) (auto simp: Sseq_def inf)
  then have **: "\n. pick n \ Sseq n"
    unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
  with * have "range pick \ S" by auto
  moreover have "pick n \ pick (n + Suc m)" for m n
  proof -
    have "pick n \ Sseq (n + Suc m)"
      by (induct m) (auto simp add: Sseq_def pick_def)
    with ** show ?thesis by auto
  qed
  then have "inj pick"
    by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
  ultimately show ?thesis by blast
qed

lemma infinite_iff_countable_subset: "\ finite S \ (\f::nat \ 'a. inj f \ range f \ S)"
  \<comment> \<open>Courtesy of Stephan Merz\<close>
  using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto

lemma image_inv_into_cancel:
  assumes surj: "f`A = A'"
    and sub: "B' \ A'"
  shows "f `((inv_into A f)`B') = B'"
  using assms
proof (auto simp: f_inv_into_f)
  let ?f' = "inv_into A f"
  fix a'
  assume *: "a' \ B'"
  with sub have "a' \ A'" by auto
  with surj have "a' = f (?f' a')"
    by (auto simp: f_inv_into_f)
  with * show "a' \ f ` (?f' ` B')" by blast
qed

lemma inv_into_inv_into_eq:
  assumes "bij_betw f A A'"
    and a: "a \ A"
  shows "inv_into A' (inv_into A f) a = f a"
proof -
  let ?f' = "inv_into A f"
  let ?f'' = "inv_into A' ?f'"
  from assms have *: "bij_betw ?f' A' A"
    by (auto simp: bij_betw_inv_into)
  with a obtain a' where a': "a' \ A'" "?f' a' = a"
    unfolding bij_betw_def by force
  with a * have "?f'' a = a'"
    by (auto simp: f_inv_into_f bij_betw_def)
  moreover from assms a' have "f a = a'"
    by (auto simp: bij_betw_def)
  ultimately show "?f'' a = f a" by simp
qed

lemma inj_on_iff_surj:
  assumes "A \ {}"
  shows "(\f. inj_on f A \ f ` A \ A') \ (\g. g ` A' = A)"
proof safe
  fix f
  assume inj: "inj_on f A" and incl: "f ` A \ A'"
  let ?phi = "\a' a. a \ A \ f a = a'"
  let ?csi = "\a. a \ A"
  let ?g = "\a'. if a' \ f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
  have "?g ` A' = A"
  proof
    show "?g ` A' \ A"
    proof clarify
      fix a'
      assume *: "a' \ A'"
      show "?g a' \ A"
      proof (cases "a' \ f ` A")
        case True
        then obtain a where "?phi a' a" by blast
        then have "?phi a' (SOME a. ?phi a' a)"
          using someI[of "?phi a'" a] by blast
        with True show ?thesis by auto
      next
        case False
        with assms have "?csi (SOME a. ?csi a)"
          using someI_ex[of ?csi] by blast
        with False show ?thesis by auto
      qed
    qed
  next
    show "A \ ?g ` A'"
    proof -
      have "?g (f a) = a \ f a \ A'" if a: "a \ A" for a
      proof -
        let ?b = "SOME aa. ?phi (f a) aa"
        from a have "?phi (f a) a" by auto
        then have *: "?phi (f a) ?b"
          using someI[of "?phi(f a)" a] by blast
        then have "?g (f a) = ?b" using a by auto
        moreover from inj * a have "a = ?b"
          by (auto simp add: inj_on_def)
        ultimately have "?g(f a) = a" by simp
        with incl a show ?thesis by auto
      qed
      then show ?thesis by force
    qed
  qed
  then show "\g. g ` A' = A" by blast
next
  fix g
  let ?f = "inv_into A' g"
  have "inj_on ?f (g ` A')"
    by (auto simp: inj_on_inv_into)
  moreover have "?f (g a') \ A'" if a': "a' \ A'" for a'
  proof -
    let ?phi = "\ b'. b' \ A' \ g b' = g a'"
    from a' have "?phi a'" by auto
    then have "?phi (SOME b'. ?phi b')"
      using someI[of ?phi] by blast
    then show ?thesis by (auto simp: inv_into_def)
  qed
  ultimately show "\f. inj_on f (g ` A') \ f ` g ` A' \ A'"
    by auto
qed

lemma Ex_inj_on_UNION_Sigma:
  "\f. (inj_on f (\i \ I. A i) \ f ` (\i \ I. A i) \ (SIGMA i : I. A i))"
proof
  let ?phi = "\a i. i \ I \ a \ A i"
  let ?sm = "\a. SOME i. ?phi a i"
  let ?f = "\a. (?sm a, a)"
  have "inj_on ?f (\i \ I. A i)"
    by (auto simp: inj_on_def)
  moreover
  have "?sm a \ I \ a \ A(?sm a)" if "i \ I" and "a \ A i" for i a
    using that someI[of "?phi a" i] by auto
  then have "?f ` (\i \ I. A i) \ (SIGMA i : I. A i)"
    by auto
  ultimately show "inj_on ?f (\i \ I. A i) \ ?f ` (\i \ I. A i) \ (SIGMA i : I. A i)"
    by auto
qed

lemma inv_unique_comp:
  assumes fg: "f \ g = id"
    and gf: "g \ f = id"
  shows "inv f = g"
  using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)

lemma subset_image_inj:
  "S \ f ` T \ (\U. U \ T \ inj_on f U \ S = f ` U)"
proof safe
  show "\U\T. inj_on f U \ S = f ` U"
    if "S \ f ` T"
  proof -
    from that [unfolded subset_image_iff subset_iff]
    obtain g where g: "\x. x \ S \ g x \ T \ x = f (g x)"
      by (auto simp add: image_iff Bex_def choice_iff')
    show ?thesis
    proof (intro exI conjI)
      show "g ` S \ T"
        by (simp add: g image_subsetI)
      show "inj_on f (g ` S)"
        using g by (auto simp: inj_on_def)
      show "S = f ` (g ` S)"
        using g image_subset_iff by auto
    qed
  qed
qed blast

subsection \<open>Other Consequences of Hilbert's Epsilon\<close>

text \<open>Hilbert's Epsilon and the \<^term>\<open>split\<close> Operator\<close>

text \<open>Looping simprule!\<close>
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))"
  by simp

lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
  by (simp add: split_def)

lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \ y = y') = (x, y)"
  by blast

text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
lemma wf_iff_no_infinite_down_chain: "wf r \ (\f. \i. (f (Suc i), f i) \ r)"
  (is "_ \ \ ?ex")
proof
  assume "wf r"
  show "\ ?ex"
  proof
    assume ?ex
    then obtain f where f: "(f (Suc i), f i) \ r" for i
      by blast
    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
      by (auto simp: wf_eq_minimal)
    let ?Q = "{w. \i. w = f i}"
    fix n
    have "f n \ ?Q" by blast
    from minimal [OF this] obtain j where "(y, f j) \ r \ y \ ?Q" for y by blast
    with this [OF \<open>(f (Suc j), f j) \<in> r\<close>] have "f (Suc j) \<notin> ?Q" by simp
    then show False by blast
  qed
next
  assume "\ ?ex"
  then show "wf r"
  proof (rule contrapos_np)
    assume "\ wf r"
    then obtain Q x where x: "x \ Q" and rec: "z \ Q \ \y. (y, z) \ r \ y \ Q" for z
      by (auto simp add: wf_eq_minimal)
    obtain descend :: "nat \ 'a"
      where descend_0: "descend 0 = x"
        and descend_Suc: "descend (Suc n) = (SOME y. y \ Q \ (y, descend n) \ r)" for n
      by (rule that [of "rec_nat x (\_ rec. (SOME y. y \ Q \ (y, rec) \ r))"]) simp_all
    have descend_Q: "descend n \ Q" for n
    proof (induct n)
      case 0
      with x show ?case by (simp only: descend_0)
    next
      case Suc
      then show ?case by (simp only: descend_Suc) (rule someI2_ex; use rec in blast)
    qed
    have "(descend (Suc i), descend i) \ r" for i
      by (simp only: descend_Suc) (rule someI2_ex; use descend_Q rec in blast)
    then show "\f. \i. (f (Suc i), f i) \ r" by blast
  qed
qed

lemma wf_no_infinite_down_chainE:
  assumes "wf r"
  obtains k where "(f (Suc k), f k) \ r"
  using assms wf_iff_no_infinite_down_chain[of r] by blast

text \<open>A dynamically-scoped fact for TFL\<close>
lemma tfl_some: "\P x. P x \ P (Eps P)"
  by (blast intro: someI)

subsection \<open>An aside: bounded accessible part\<close>

text \<open>Finite monotone eventually stable sequences\<close>

lemma finite_mono_remains_stable_implies_strict_prefix:
  fixes f :: "nat \ 'a::order"
  assumes S: "finite (range f)" "mono f"
    and eq: "\n. f n = f (Suc n) \ f (Suc n) = f (Suc (Suc n))"
  shows "\N. (\n\N. \m\N. m < n \ f m < f n) \ (\n\N. f N = f n)"
  using assms
proof -
  have "\n. f n = f (Suc n)"
  proof (rule ccontr)
    assume "\ ?thesis"
    then have "\n. f n \ f (Suc n)" by auto
    with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)"
      by (auto simp: le_less mono_iff_le_Suc)
    with lift_Suc_mono_less_iff[of f] have *: "\n m. n < m \ f n < f m"
      by auto
    have "inj f"
    proof (intro injI)
      fix x y
      assume "f x = f y"
      then show "x = y"
        by (cases x y rule: linorder_cases) (auto dest: *)
    qed
    with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
      by (rule finite_imageD)
    then show False by simp
  qed
  then obtain n where n: "f n = f (Suc n)" ..
  define N where "N = (LEAST n. f n = f (Suc n))"
  have N: "f N = f (Suc N)"
    unfolding N_def using n by (rule LeastI)
  show ?thesis
  proof (intro exI[of _ N] conjI allI impI)
    fix n
    assume "N \ n"
    then have "\m. N \ m \ m \ n \ f m = f N"
    proof (induct rule: dec_induct)
      case base
      then show ?case by simp
    next
      case (step n)
      then show ?case
        using eq [rule_format, of "n - 1"] N
        by (cases n) (auto simp add: le_Suc_eq)
    qed
    from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
  next
    fix n m :: nat
    assume "m < n" "n \ N"
    then show "f m < f n"
    proof (induct rule: less_Suc_induct)
      case (1 i)
      then have "i < N" by simp
      then have "f i \ f (Suc i)"
        unfolding N_def by (rule not_less_Least)
      with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
    next
      case 2
      then show ?case by simp
    qed
  qed
qed

lemma finite_mono_strict_prefix_implies_finite_fixpoint:
  fixes f :: "nat \ 'a set"
  assumes S: "\i. f i \ S" "finite S"
    and ex: "\N. (\n\N. \m\N. m < n \ f m \ f n) \ (\n\N. f N = f n)"
  shows "f (card S) = (\n. f n)"
proof -
  from ex obtain N where inj: "\n m. n \ N \ m \ N \ m < n \ f m \ f n"
    and eq: "\n\N. f N = f n"
    by atomize auto
  have "i \ N \ i \ card (f i)" for i
  proof (induct i)
    case 0
    then show ?case by simp
  next
    case (Suc i)
    with inj [of "Suc i" i] have "(f i) \ (f (Suc i))" by auto
    moreover have "finite (f (Suc i))" using S by (rule finite_subset)
    ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
    with Suc inj show ?case by auto
  qed
  then have "N \ card (f N)" by simp
  also have "\ \ card S" using S by (intro card_mono)
  finally have \<section>: "f (card S) = f N" using eq by auto
  moreover have "\ (range f) \ f N"
  proof clarify
    fix x n
    assume "x \ f n"
    with eq inj [of N] show "x \ f N"
      by (cases "n < N") (auto simp: not_less)
  qed
  ultimately show ?thesis
    by auto
qed

subsection \<open>More on injections, bijections, and inverses\<close>

locale bijection =
  fixes f :: "'a \ 'a"
  assumes bij: "bij f"
begin

lemma bij_inv: "bij (inv f)"
  using bij by (rule bij_imp_bij_inv)

lemma surj [simp]: "surj f"
  using bij by (rule bij_is_surj)

lemma inj: "inj f"
  using bij by (rule bij_is_inj)

lemma surj_inv [simp]: "surj (inv f)"
  using inj by (rule inj_imp_surj_inv)

lemma inj_inv: "inj (inv f)"
  using surj by (rule surj_imp_inj_inv)

lemma eqI: "f a = f b \ a = b"
  using inj by (rule injD)

lemma eq_iff [simp]: "f a = f b \ a = b"
  by (auto intro: eqI)

lemma eq_invI: "inv f a = inv f b \ a = b"
  using inj_inv by (rule injD)

lemma eq_inv_iff [simp]: "inv f a = inv f b \ a = b"
  by (auto intro: eq_invI)

lemma inv_left [simp]: "inv f (f a) = a"
  using inj by (simp add: inv_f_eq)

lemma inv_comp_left [simp]: "inv f \ f = id"
  by (simp add: fun_eq_iff)

lemma inv_right [simp]: "f (inv f a) = a"
  using surj by (simp add: surj_f_inv_f)

lemma inv_comp_right [simp]: "f \ inv f = id"
  by (simp add: fun_eq_iff)

lemma inv_left_eq_iff [simp]: "inv f a = b \ f b = a"
  by auto

lemma inv_right_eq_iff [simp]: "b = inv f a \ f b = a"
  by auto

end

lemma infinite_imp_bij_betw:
  assumes infinite: "\ finite A"
  shows "\h. bij_betw h A (A - {a})"
proof (cases "a \ A")
  case False
  then have "A - {a} = A" by blast
  then show ?thesis
    using bij_betw_id[of A] by auto
next
  case True
  with infinite have "\ finite (A - {a})" by auto
  with infinite_iff_countable_subset[of "A - {a}"]
  obtain f :: "nat \ 'a" where "inj f" and f: "f ` UNIV \ A - {a}" by blast
  define g where "g n = (if n = 0 then a else f (Suc n))" for n
  define A' where "A' = g ` UNIV"
  have *: "\y. f y \ a" using f by blast
  have 3: "inj_on g UNIV \ g ` UNIV \ A \ a \ g ` UNIV"
    using \<open>inj f\<close> f * unfolding inj_on_def g_def
    by (auto simp add: True image_subset_iff)
  then have 4: "bij_betw g UNIV A' \ a \ A' \ A' \ A"
    using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
  then have 5: "bij_betw (inv g) A' UNIV"
    by (auto simp add: bij_betw_inv_into)
  from 3 obtain n where n: "g n = a" by auto
  have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
    by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
  define v where "v m = (if m < n then m else Suc m)" for m
  have "m < n \ m = n" if "\k. k < n \ m \ Suc k" for m
    using that [of "m-1"] by auto
  then have 7: "bij_betw v UNIV (UNIV - {n})"
    unfolding bij_betw_def inj_on_def v_def by auto
  define h' where "h' = g \<circ> v \<circ> (inv g)"
  with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
    by (auto simp add: bij_betw_trans)
  define h where "h b = (if b \ A' then h' b else b)" for b
  with 8 have "bij_betw h A' (A' - {a})"
    using bij_betw_cong[of A' h] by auto
  moreover
  have "\b \ A - A'. h b = b" by (auto simp: h_def)
  then have "bij_betw h (A - A') (A - A')"
    using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
  moreover
  from 4 have "(A' \ (A - A') = {} \ A' \ (A - A') = A) \
    ((A' - {a}) \ (A - A') = {} \ (A' - {a}) \ (A - A') = A - {a})"
    by blast
  ultimately have "bij_betw h A (A - {a})"
    using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
  then show ?thesis by blast
qed

lemma infinite_imp_bij_betw2:
  assumes "\ finite A"
  shows "\h. bij_betw h A (A \ {a})"
proof (cases "a \ A")
  case True
  then have "A \ {a} = A" by blast
  then show ?thesis using bij_betw_id[of A] by auto
next
  case False
  let ?A' = "A \ {a}"
  from False have "A = ?A' - {a}" by blast
  moreover from assms have "\ finite ?A'" by auto
  ultimately obtain f where "bij_betw f ?A' A"
    using infinite_imp_bij_betw[of ?A' a] by auto
  then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into)
  then show ?thesis by auto
qed

lemma bij_betw_inv_into_left: "bij_betw f A A' \ a \ A \ inv_into A f (f a) = a"
  unfolding bij_betw_def by clarify (rule inv_into_f_f)

lemma bij_betw_inv_into_right: "bij_betw f A A' \ a' \ A' \ f (inv_into A f a') = a'"
  unfolding bij_betw_def using f_inv_into_f by force

lemma bij_betw_inv_into_subset:
  "bij_betw f A A' \ B \ A \ f ` B = B' \ bij_betw (inv_into A f) B' B"
  by (auto simp: bij_betw_def intro: inj_on_inv_into)

subsection \<open>Specification package -- Hilbertized version\<close>

lemma exE_some: "Ex P \ c \ Eps P \ P c"
  by (simp only: someI_ex)

ML_file \<open>Tools/choice_specification.ML\<close>

subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>

context complete_distrib_lattice
begin

lemma Sup_Inf: "\ (Inf ` A) = \ (Sup ` {f ` A |f. \B\A. f B \ B})"
proof (rule order.antisym)
  show "\ (Inf ` A) \ \ (Sup ` {f ` A |f. \B\A. f B \ B})"
    using Inf_lower2 Sup_upper
    by (fastforce simp add: intro: Sup_least INF_greatest)
next
  show "\ (Sup ` {f ` A |f. \B\A. f B \ B}) \ \ (Inf ` A)"
  proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
    fix f
    assume "\Y. (\f. Y = f ` A \ (\Y\A. f Y \ Y)) \ f Y \ Y"
    then have B: "\ F . (\ Y \ A . F Y \ Y) \ \ Z \ A . f (F ` A) = F Z"
      by auto
    show "\(f ` {f ` A |f. \Y\A. f Y \ Y}) \ \(Inf ` A)"
    proof (cases "\ Z \ A . \(f ` {f ` A |f. \Y\A. f Y \ Y}) \ Inf Z")
      case True
      from this obtain Z where [simp]: "Z \ A" and A: "\(f ` {f ` A |f. \Y\A. f Y \ Y}) \ Inf Z"
        by blast
      have B: "... \ $Inf ` A)"
        by (simp add: SUP_upper)
      from A and B show ?thesis
        by simp
    next
      case False
      then have X: "\ Z . Z \ A \ \ x . x \ Z \ \ \(f ` {f ` A |f. \Y\A. f Y \ Y}) \ x"
        using Inf_greatest by blast
      define F where "F = (\ Z . SOME x . x \ Z \ \ \(f ` {f ` A |f. \Y\A. f Y \ Y}) \ x)"
      have C: "\Y. Y \ A \ F Y \ Y"
        using X by (simp add: F_def, rule someI2_ex, auto)
      have E: "\Y. Y \ A \ \ \(f ` {f ` A |f. \Y\A. f Y \ Y}) \ F Y"
        using X by (simp add: F_def, rule someI2_ex, auto)
      from C and B obtain  Z where D: "Z \ A " and Y: "f (F ` A) = F Z"
        by blast
      from E and D have W: "\ \(f ` {f ` A |f. \Y\A. f Y \ Y}) \ F Z"
        by simp
      have "\(f ` {f ` A |f. \Y\A. f Y \ Y}) \ f (F ` A)"
        using C by (blast intro: INF_lower)
      with W Y show ?thesis
        by simp
    qed
  qed
qed

lemma dual_complete_distrib_lattice:
  "class.complete_distrib_lattice Sup Inf sup ($ (>) inf \ \"
  by (simp add: class.complete_distrib_lattice.intro [OF dual_complete_lattice]
                class.complete_distrib_lattice_axioms_def Sup_Inf)

lemma sup_Inf: "a \ \B = $($ a ` B)"
proof (rule order.antisym)
  show "a \ \B \ $($ a ` B)"
    using Inf_lower sup.mono by (fastforce intro: INF_greatest)
next
  have "$($ a ` B) \ $Sup ` {{f {a}, f B} |f. f {a} = a \ f B \ B})"
    by (rule INF_greatest, auto simp add: INF_lower)
  also have "... = \(Inf ` {{a}, B})"
    by (unfold Sup_Inf, simp)
  finally show "\(($ a ` B) \ a \ \B"
    by simp
qed

lemma inf_Sup: "a \ \B = $($ a ` B)"
  using dual_complete_distrib_lattice
  by (rule complete_distrib_lattice.sup_Inf)

lemma INF_SUP: "(\y. \x. P x y) = (\f. \x. P (f x) x)"
proof (rule order.antisym)
  show "(SUP x. INF y. P (x y) y) \ (INF y. SUP x. P x y)"
    by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
next
  have "(INF y. SUP x. ((P x y))) \ Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \ ?B")
  proof (rule INF_greatest, clarsimp)
    fix y
    have "?A \ (SUP x. P x y)"
      by (rule INF_lower, simp)
    also have "... \ Sup {uu. \x. uu = P x y}"
      by (simp add: full_SetCompr_eq)
    finally show "?A \ Sup {uu. \x. uu = P x y}"
      by simp
  qed
  also have "... \ (SUP x. INF y. P (x y) y)"
  proof (subst Inf_Sup, rule SUP_least, clarsimp)
    fix f
    assume A: "\Y. (\y. Y = {uu. \x. uu = P x y}) \ f Y \ Y"

    have " \(f ` {uu. \y. uu = {uu. \x. uu = P x y}}) \
      (\<Sqinter>y. P (SOME x. f {P x y |x. True} = P x y) y)"
    proof (rule INF_greatest, clarsimp)
      fix y
        have "(INF x\{uu. \y. uu = {uu. \x. uu = P x y}}. f x) \ f {uu. \x. uu = P x y}"
          by (rule INF_lower, blast)
        also have "... \ P (SOME x. f {uu . \x. uu = P x y} = P x y) y"
          by (rule someI2_ex) (use A in auto)
        finally show "\(f ` {uu. \y. uu = {uu. \x. uu = P x y}}) \
          P (SOME x. f {uu. \<exists>x. uu = P x y} = P x y) y"
          by simp
      qed
      also have "... \ (SUP x. INF y. P (x y) y)"
        by (rule SUP_upper, simp)
      finally show "$f ` {uu. \y. uu = {uu. \x. uu = P x y}}) \ (\x. \y. P (x y) y)"
        by simp
    qed
  finally show "(INF y. SUP x. P x y) \ (SUP x. INF y. P (x y) y)"
    by simp
qed

lemma INF_SUP_set: "(\B\A. \(g ` B)) = (\B\{f ` A |f. \C\A. f C \ C}. \(g ` B))"
                    (is "_ = (\B\?F. _)")
proof (rule order.antisym)
  have "\ ((g \ f) ` A) \ \ (g ` B)" if "\B. B \ A \ f B \ B" "B \ A" for f B
    using that by (auto intro: SUP_upper2 INF_lower2)
  then show "(\x\?F. \a\x. g a) \ (\x\A. \a\x. g a)"
    by (auto intro!: SUP_least INF_greatest simp add: image_comp)
next
  show "(\x\A. \a\x. g a) \ (\x\?F. \a\x. g a)"
  proof (cases "{} \ A")
    case True
    then show ?thesis
      by (rule INF_lower2) simp_all
  next
    case False
    {fix x
      have "(\x\A. \x\x. g x) \ (\u. if x \ A then if u \ x then g u else \ else $"
      proof (cases "x \ A")
        case True
        then show ?thesis
          by (intro INF_lower2 SUP_least SUP_upper2) auto
      qed auto
    }
    then have "(\Y\A. \a\Y. g a) \ (\Y. \y. if Y \ A then if y \ Y then g y else \ else \)"
      by (rule INF_greatest)
    also have "... = (\x. \Y. if Y \ A then if x Y \ Y then g (x Y) else \ else \)"
      by (simp only: INF_SUP)
    also have "... \ (\x\?F. \a\x. g a)"
    proof (rule SUP_least)
      show "(\B. if B \ A then if x B \ B then g (x B) else \ else \)
               \<le> (\<Squnion>x\<in>?F. \<Sqinter>x\<in>x. g x)" for x
      proof -
        define G where "G \ \Y. if x Y \ Y then x Y else (SOME x. x \Y)"
        have "\Y\A. G Y \ Y"
          using False some_in_eq G_def by auto
        then have A: "G ` A \ ?F"
          by blast
        show "(\Y. if Y \ A then if x Y \ Y then g (x Y) else \ else \) \ (\x\?F. \x\x. g x)"
          by (fastforce simp: G_def intro: SUP_upper2 [OF A] INF_greatest INF_lower2)
      qed
    qed
    finally show ?thesis by simp
  qed
qed

lemma SUP_INF: "(\y. \x. P x y) = (\x. \y. P (x y) y)"
  using dual_complete_distrib_lattice
  by (rule complete_distrib_lattice.INF_SUP)

lemma SUP_INF_set: "(\x\A. \ (g ` x)) = (\x\{f ` A |f. \Y\A. f Y \ Y}. \ (g ` x))"
  using dual_complete_distrib_lattice
  by (rule complete_distrib_lattice.INF_SUP_set)

end

(*properties of the former complete_distrib_lattice*)
context complete_distrib_lattice
begin

lemma sup_INF: "a \ (\b\B. f b) = (\b\B. a \ f b)"
  by (simp add: sup_Inf image_comp)

lemma inf_SUP: "a \ (\b\B. f b) = (\b\B. a \ f b)"
  by (simp add: inf_Sup image_comp)

lemma Inf_sup: "\B \ a = (\b\B. b \ a)"
  by (simp add: sup_Inf sup_commute)

lemma Sup_inf: "\B \ a = (\b\B. b \ a)"
  by (simp add: inf_Sup inf_commute)

lemma INF_sup: "(\b\B. f b) \ a = (\b\B. f b \ a)"
  by (simp add: sup_INF sup_commute)

lemma SUP_inf: "(\b\B. f b) \ a = (\b\B. f b \ a)"
  by (simp add: inf_SUP inf_commute)

lemma Inf_sup_eq_top_iff: "(\B \ a = \) \ (\b\B. b \ a = \)"
  by (simp only: Inf_sup INF_top_conv)

lemma Sup_inf_eq_bot_iff: "(\B \ a = \) \ (\b\B. b \ a = \)"
  by (simp only: Sup_inf SUP_bot_conv)

lemma INF_sup_distrib2: "(\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)"
  by (subst INF_commute) (simp add: sup_INF INF_sup)

lemma SUP_inf_distrib2: "(\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)"
  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)

end

instantiation set :: (type) complete_distrib_lattice
begin
instance proof (standard, clarsimp)
  fix A :: "(('a set) set) set"
  fix x::'a
  assume A: "\\~~\A. \X\\~~. x \ X"~~~~
  define F where "F \ \Y. SOME X. Y \ A \ X \ Y \ x \ X"
  have "(\S \ F ` A. x \ S)"
    using A unfolding F_def by (fastforce intro: someI2_ex)
  moreover have "\Y\A. F Y \ Y"
    using A unfolding F_def by (fastforce intro: someI2_ex)
  then have "\f. F ` A = f ` A \ (\Y\A. f Y \ Y)"
    by blast
  ultimately show "\X. (\f. X = f ` A \ (\Y\A. f Y \ Y)) \ (\S\X. x \ S)"
    by auto
qed
end

instance set :: (type) complete_boolean_algebra ..

instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
begin
instance by standard (simp add: le_fun_def INF_SUP_set image_comp)
end

instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..

context complete_linorder
begin

subclass complete_distrib_lattice
proof (standard, rule ccontr)
  fix A :: "'a set set"
  let ?F = "{f ` A |f. \Y\A. f Y \ Y}"
  assume "\ \(Sup ` A) \ \(Inf ` ?F)"
  then have C: "\(Sup ` A) > \(Inf ` ?F)"
    by (simp add: not_le)
  show False
  proof (cases "\ z . \(Sup ` A) > z \ z > \(Inf ` ?F)")
    case True
    then obtain z where A: "z < \(Sup ` A)" and X: "z > \(Inf ` ?F)"
      by blast
    then have B: "\Y. Y \ A \ \k \Y . z < k"
      using local.less_Sup_iff by(force dest: less_INF_D)

    define G where "G \ \Y. SOME k . k \ Y \ z < k"
    have E: "\Y. Y \ A \ G Y \ Y"
      using B unfolding G_def by (fastforce intro: someI2_ex)
    have "z \ Inf (G ` A)"
    proof (rule INF_greatest)
      show  "\Y. Y \ A \ z \ G Y"
        using B unfolding G_def by (fastforce intro: someI2_ex)
    qed
    also have "... \ \(Inf ` ?F)"
      by (rule SUP_upper) (use E in blast)
    finally have "z \ \(Inf ` ?F)"
      by simp

    with X show ?thesis
      using local.not_less by blast
  next
    case False
    have B: "\Y. Y \ A \ \ k \Y . \(Inf ` ?F) < k"
      using C local.less_Sup_iff by(force dest: less_INF_D)
    define G where "G \ \ Y . SOME k . k \ Y \ \(Inf ` ?F) < k"
    have E: "\Y. Y \ A \ G Y \ Y"
      using B unfolding G_def by (fastforce intro: someI2_ex)
    have "\Y. Y \ A \ \(Sup ` A) \ G Y"
      using B False local.leI unfolding G_def by (fastforce intro: someI2_ex)
    then have "\(Sup ` A) \ Inf (G ` A)"
      by (simp add: local.INF_greatest)
    also have "Inf (G ` A) \ \(Inf ` ?F)"
      by (rule SUP_upper) (use E in blast)
    finally have "\(Sup ` A) \ \(Inf ` ?F)"
      by simp
    with C show ?thesis
      using not_less by blast
  qed
qed
end

end

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.