Quelle  Complete_Lattices.thy   Sprache: Isabelle

(*  Title:      HOL/Complete_Lattices.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Florian Haftmann
    Author:     Viorel Preoteasa (Complete Distributive Lattices)     
*)

section ‹Complete lattices›

theory Complete_Lattices
  imports Fun
begin

subsection ‹Syntactic infimum and supremum operations›

class Inf =
  fixes Inf :: "'a set \ 'a"  (‹(‹open_block notation=‹prefix ⊓››⊓ _)› [900] 900)

class Sup =
  fixes Sup :: "'a set \ 'a"  (‹(‹open_block notation=‹prefix ⊔››⊔ _)› [900] 900)

syntax
  "_INF1"     :: "pttrns \ 'b \ 'b"           (‹(‹indent=3 notation=‹binder INF››INF _./ _)› [0, 10] 10)
  "_INF"      :: "pttrn \ 'a set \ 'b \ 'b"  (‹(‹indent=3 notation=‹binder INF››INF _∈_./ _)› [0, 0, 10] 10)
  "_SUP1"     :: "pttrns \ 'b \ 'b"           (‹(‹indent=3 notation=‹binder SUP››SUP _./ _)› [0, 10] 10)
  "_SUP"      :: "pttrn \ 'a set \ 'b \ 'b"  (‹(‹indent=3 notation=‹binder SUP››SUP _∈_./ _)› [0, 0, 10] 10)

syntax
  "_INF1"     :: "pttrns \ 'b \ 'b"           (‹(‹indent=3 notation=‹binder ⊓››⊓_./ _)› [0, 10] 10)
  "_INF"      :: "pttrn \ 'a set \ 'b \ 'b"  (‹(‹indent=3 notation=‹binder ⊓››⊓_∈_./ _)› [0, 0, 10] 10)
  "_SUP1"     :: "pttrns \ 'b \ 'b"           (‹(‹indent=3 notation=‹binder ⊔››⊔_./ _)› [0, 10] 10)
  "_SUP"      :: "pttrn \ 'a set \ 'b \ 'b"  (‹(‹indent=3 notation=‹binder ⊔››⊔_∈_./ _)› [0, 0, 10] 10)

syntax_consts
  "_INF1" "_INF" ⇌ Inf and
  "_SUP1" "_SUP" ⇌ Sup

translations
  "\x y. f"   ⇌ "\x. \y. f"
  "\x. f"     ⇌ "\(CONST range (\x. f))"
  "\x\A. f"   ⇌ "CONST Inf ((\x. f) ` A)"
  "\x y. f"   ⇌ "\x. \y. f"
  "\x. f"     ⇌ "\(CONST range (\x. f))"
  "\x\A. f"   ⇌ "CONST Sup ((\x. f) ` A)"

context Inf
begin

lemma INF_image: "\ (g ` f ` A) = \ ((g \ f) ` A)"
  by (simp add: image_comp)

lemma INF_identity_eq [simp]: "(\x\A. x) = \A"
  by simp

lemma INF_id_eq [simp]: "\(id ` A) = \A"
  by simp

lemma INF_cong: "A = B \ (\x. x \ B \ C x = D x) \ \(C ` A) = \(D ` B)"
  by (simp add: image_def)

lemma INF_cong_simp:
  "A = B \ (\x. x \ B =simp=> C x = D x) \ \(C ` A) = \(D ` B)"
  unfolding simp_implies_def by (fact INF_cong)

end

context Sup
begin

lemma SUP_image: "\ (g ` f ` A) = \ ((g \ f) ` A)"
by(fact Inf.INF_image)

lemma SUP_identity_eq [simp]: "(\x\A. x) = \A"
by(fact Inf.INF_identity_eq)

lemma SUP_id_eq [simp]: "\(id ` A) = \A"
by(fact Inf.INF_id_eq)

lemma SUP_cong: "A = B \ (\x. x \ B \ C x = D x) \ \(C ` A) = \(D ` B)"
by (fact Inf.INF_cong)

lemma SUP_cong_simp:
  "A = B \ (\x. x \ B =simp=> C x = D x) \ \(C ` A) = \(D ` B)"
by (fact Inf.INF_cong_simp)

end


subsection ‹Abstract complete lattices›

text ‹A complete lattice always has a bottom and a top,
so we include them into the following type class,
along with assumptions that define bottom and top
in terms of infimum and supremum.›

class complete_lattice = lattice + Inf + Sup + bot + top +
  assumes Inf_lower: "x \ A \ \A \ x"
    and Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A"
    and Sup_upper: "x \ A \ x \ \A"
    and Sup_least: "(\x. x \ A \ x \ z) \ \A \ z"
    and Inf_empty [simp]: "\{} = \"
    and Sup_empty [simp]: "\{} = \"
begin

subclass bounded_lattice
proof
  fix a
  show "\ \ a"
    by (auto intro: Sup_least simp only: Sup_empty [symmetric])
  show "a \ \"
    by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
qed

lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (\) (>) inf \ \"
  by (auto intro!: class.complete_lattice.intro dual_lattice)
    (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+)

end

context complete_lattice
begin

lemma Sup_eqI:
  "(\y. y \ A \ y \ x) \ (\y. (\z. z \ A \ z \ y) \ x \ y) \ \A = x"
  by (blast intro: order.antisym Sup_least Sup_upper)

lemma Inf_eqI:
  "(\i. i \ A \ x \ i) \ (\y. (\i. i \ A \ y \ i) \ y \ x) \ \A = x"
  by (blast intro: order.antisym Inf_greatest Inf_lower)

lemma SUP_eqI:
  "(\i. i \ A \ f i \ x) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x"
  using Sup_eqI [of "f ` A" x] by auto

lemma INF_eqI:
  "(\i. i \ A \ x \ f i) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x"
  using Inf_eqI [of "f ` A" x] by auto

lemma INF_lower: "i \ A \ (\i\A. f i) \ f i"
  using Inf_lower [of _ "f ` A"] by simp

lemma INF_greatest: "(\i. i \ A \ u \ f i) \ u \ (\i\A. f i)"
  using Inf_greatest [of "f ` A"] by auto

lemma SUP_upper: "i \ A \ f i \ (\i\A. f i)"
  using Sup_upper [of _ "f ` A"] by simp

lemma SUP_least: "(\i. i \ A \ f i \ u) \ (\i\A. f i) \ u"
  using Sup_least [of "f ` A"] by auto

lemma Inf_lower2: "u \ A \ u \ v \ \A \ v"
  using Inf_lower [of u A] by auto

lemma INF_lower2: "i \ A \ f i \ u \ (\i\A. f i) \ u"
  using INF_lower [of i A f] by auto

lemma Sup_upper2: "u \ A \ v \ u \ v \ \A"
  using Sup_upper [of u A] by auto

lemma SUP_upper2: "i \ A \ u \ f i \ u \ (\i\A. f i)"
  using SUP_upper [of i A f] by auto

lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)"
  by (auto intro: Inf_greatest dest: Inf_lower)

lemma le_INF_iff: "u \ (\i\A. f i) \ (\i\A. u \ f i)"
  using le_Inf_iff [of _ "f ` A"] by simp

lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)"
  by (auto intro: Sup_least dest: Sup_upper)

lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i\A. f i \ u)"
  using Sup_le_iff [of "f ` A"] by simp

lemma Inf_insert [simp]: "\(insert a A) = a \ \A"
  by (auto intro: le_infI le_infI1 le_infI2 order.antisym Inf_greatest Inf_lower)

lemma INF_insert: "(\x\insert a A. f x) = f a \ \(f ` A)"
  by simp

lemma Sup_insert [simp]: "\(insert a A) = a \ \A"
  by (auto intro: le_supI le_supI1 le_supI2 order.antisym Sup_least Sup_upper)

lemma SUP_insert: "(\x\insert a A. f x) = f a \ \(f ` A)"
  by simp

lemma INF_empty: "(\x\{}. f x) = \"
  by simp

lemma SUP_empty: "(\x\{}. f x) = \"
  by simp

lemma Inf_UNIV [simp]: "\UNIV = \"
  by (auto intro!: order.antisym Inf_lower)

lemma Sup_UNIV [simp]: "\UNIV = \"
  by (auto intro!: order.antisym Sup_upper)

lemma Inf_eq_Sup: "\A = \{b. \a \ A. b \ a}"
  by (auto intro: order.antisym Inf_lower Inf_greatest Sup_upper Sup_least)

lemma Sup_eq_Inf:  "\A = \{b. \a \ A. a \ b}"
  by (auto intro: order.antisym Inf_lower Inf_greatest Sup_upper Sup_least)

lemma Inf_superset_mono: "B \ A \ \A \ \B"
  by (auto intro: Inf_greatest Inf_lower)

lemma Sup_subset_mono: "A \ B \ \A \ \B"
  by (auto intro: Sup_least Sup_upper)

lemma Inf_mono:
  assumes "\b. b \ B \ \a\A. a \ b"
  shows "\A \ \B"
proof (rule Inf_greatest)
  fix b assume "b \ B"
  with assms obtain a where "a \ A" and "a \ b" by blast
  from ‹a ∈ A› have "\A \ a" by (rule Inf_lower)
  with ‹a ≤ b› show "\A \ b" by auto
qed

lemma INF_mono: "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)"
  using Inf_mono [of "g ` B" "f ` A"] by auto

lemma INF_mono': "(\x. f x \ g x) \ (\x\A. f x) \ (\x\A. g x)"
  by (rule INF_mono) auto

lemma Sup_mono:
  assumes "\a. a \ A \ \b\B. a \ b"
  shows "\A \ \B"
proof (rule Sup_least)
  fix a assume "a \ A"
  with assms obtain b where "b \ B" and "a \ b" by blast
  from ‹b ∈ B› have "b \ \B" by (rule Sup_upper)
  with ‹a ≤ b› show "a \ \B" by auto
qed

lemma SUP_mono: "(\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)"
  using Sup_mono [of "f ` A" "g ` B"] by auto

lemma SUP_mono': "(\x. f x \ g x) \ (\x\A. f x) \ (\x\A. g x)"
  by (rule SUP_mono) auto

lemma INF_superset_mono: "B \ A \ (\x. x \ B \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)"
  🍋 ‹The last inclusion is POSITIVE!›
  by (blast intro: INF_mono dest: subsetD)

lemma SUP_subset_mono: "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)"
  by (blast intro: SUP_mono dest: subsetD)

lemma Inf_less_eq:
  assumes "\v. v \ A \ v \ u"
    and "A \ {}"
  shows "\A \ u"
proof -
  from ‹A ≠ {}› obtain v where "v \ A" by blast
  moreover from ‹v ∈ A› assms(1) have "v \ u" by blast
  ultimately show ?thesis by (rule Inf_lower2)
qed

lemma less_eq_Sup:
  assumes "\v. v \ A \ u \ v"
    and "A \ {}"
  shows "u \ \A"
proof -
  from ‹A ≠ {}› obtain v where "v \ A" by blast
  moreover from ‹v ∈ A› assms(1) have "u \ v" by blast
  ultimately show ?thesis by (rule Sup_upper2)
qed

lemma INF_eq:
  assumes "\i. i \ A \ \j\B. f i \ g j"
    and "\j. j \ B \ \i\A. g j \ f i"
  shows "\(f ` A) = \(g ` B)"
  by (intro order.antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+

lemma SUP_eq:
  assumes "\i. i \ A \ \j\B. f i \ g j"
    and "\j. j \ B \ \i\A. g j \ f i"
  shows "\(f ` A) = \(g ` B)"
  by (intro order.antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+

lemma less_eq_Inf_inter: "\A \ \B \ \(A \ B)"
  by (auto intro: Inf_greatest Inf_lower)

lemma Sup_inter_less_eq: "\(A \ B) \ \A \ \B "
  by (auto intro: Sup_least Sup_upper)

lemma Inf_union_distrib: "\(A \ B) = \A \ \B"
  by (rule order.antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)

lemma INF_union: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
  by (auto intro!: order.antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)

lemma Sup_union_distrib: "\(A \ B) = \A \ \B"
  by (rule order.antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)

lemma SUP_union: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
  by (auto intro!: order.antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)

lemma INF_inf_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)"
  by (rule order.antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)

lemma SUP_sup_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)"
  (is "?L = ?R")
proof (rule order.antisym)
  show "?L \ ?R"
    by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
  show "?R \ ?L"
    by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
qed

lemma Inf_top_conv [simp]:
  "\A = \ \ (\x\A. x = \)"
  "\ = \A \ (\x\A. x = \)"
proof -
  show "\A = \ \ (\x\A. x = \)"
  proof
    assume "\x\A. x = \"
    then have "A = {} \ A = {\}" by auto
    then show "\A = \" by auto
  next
    assume "\A = \"
    show "\x\A. x = \"
    proof (rule ccontr)
      assume "\ (\x\A. x = \)"
      then obtain x where "x \ A" and "x \ \" by blast
      then obtain B where "A = insert x B" by blast
      with ‹⊓A = ⊤› ‹x ≠ ⊤› show False by simp
    qed
  qed
  then show "\ = \A \ (\x\A. x = \)" by auto
qed

lemma INF_top_conv [simp]:
  "(\x\A. B x) = \ \ (\x\A. B x = \)"
  "\ = (\x\A. B x) \ (\x\A. B x = \)"
  using Inf_top_conv [of "B ` A"] by simp_all

lemma Sup_bot_conv [simp]:
  "\A = \ \ (\x\A. x = \)"
  "\ = \A \ (\x\A. x = \)"
  using dual_complete_lattice
  by (rule complete_lattice.Inf_top_conv)+

lemma SUP_bot_conv [simp]:
  "(\x\A. B x) = \ \ (\x\A. B x = \)"
  "\ = (\x\A. B x) \ (\x\A. B x = \)"
  using Sup_bot_conv [of "B ` A"] by simp_all

lemma INF_constant: "(\y\A. c) = (if A = {} then \ else c)"
  by (auto intro: order.antisym INF_lower INF_greatest)

lemma SUP_constant: "(\y\A. c) = (if A = {} then \ else c)"
  by (auto intro: order.antisym SUP_upper SUP_least)

lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f"
  by (simp add: INF_constant)

lemma SUP_const [simp]: "A \ {} \ (\i\A. f) = f"
  by (simp add: SUP_constant)

lemma INF_top [simp]: "(\x\A. \) = \"
  by (cases "A = {}") simp_all

lemma SUP_bot [simp]: "(\x\A. \) = \"
  by (cases "A = {}") simp_all

lemma INF_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"
  by (iprover intro: INF_lower INF_greatest order_trans order.antisym)

lemma SUP_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"
  by (iprover intro: SUP_upper SUP_least order_trans order.antisym)

lemma INF_absorb:
  assumes "k \ I"
  shows "A k \ (\i\I. A i) = (\i\I. A i)"
proof -
  from assms obtain J where "I = insert k J" by blast
  then show ?thesis by simp
qed

lemma SUP_absorb:
  assumes "k \ I"
  shows "A k \ (\i\I. A i) = (\i\I. A i)"
proof -
  from assms obtain J where "I = insert k J" by blast
  then show ?thesis by simp
qed

lemma INF_inf_const1: "I \ {} \ (\i\I. inf x (f i)) = inf x (\i\I. f i)"
  by (intro order.antisym INF_greatest inf_mono order_refl INF_lower)
     (auto intro: INF_lower2 le_infI2 intro!: INF_mono)

lemma INF_inf_const2: "I \ {} \ (\i\I. inf (f i) x) = inf (\i\I. f i) x"
  using INF_inf_const1[of I x f] by (simp add: inf_commute)

lemma less_INF_D:
  assumes "y < (\i\A. f i)" "i \ A"
  shows "y < f i"
proof -
  note ‹y < (⊓i∈A. f i)›
  also have "(\i\A. f i) \ f i" using ‹i ∈ A›
    by (rule INF_lower)
  finally show "y < f i" .
qed

lemma SUP_lessD:
  assumes "(\i\A. f i) < y" "i \ A"
  shows "f i < y"
proof -
  have "f i \ (\i\A. f i)"
    using ‹i ∈ A› by (rule SUP_upper)
  also note ‹(⊔i∈A. f i) < y›
  finally show "f i < y" .
qed

lemma INF_UNIV_bool_expand: "(\b. A b) = A True \ A False"
  by (simp add: UNIV_bool inf_commute)

lemma SUP_UNIV_bool_expand: "(\b. A b) = A True \ A False"
  by (simp add: UNIV_bool sup_commute)

lemma Inf_le_Sup: "A \ {} \ Inf A \ Sup A"
  by (blast intro: Sup_upper2 Inf_lower ex_in_conv)

lemma INF_le_SUP: "A \ {} \ \(f ` A) \ \(f ` A)"
  using Inf_le_Sup [of "f ` A"] by simp

lemma INF_eq_const: "I \ {} \ (\i. i \ I \ f i = x) \ \(f ` I) = x"
  by (auto intro: INF_eqI)

lemma SUP_eq_const: "I \ {} \ (\i. i \ I \ f i = x) \ \(f ` I) = x"
  by (auto intro: SUP_eqI)

lemma INF_eq_iff: "I \ {} \ (\i. i \ I \ f i \ c) \ \(f ` I) = c \ (\i\I. f i = c)"
  by (auto intro: INF_eq_const INF_lower order.antisym)

lemma SUP_eq_iff: "I \ {} \ (\i. i \ I \ c \ f i) \ \(f ` I) = c \ (\i\I. f i = c)"
  by (auto intro: SUP_eq_const SUP_upper order.antisym)

end

context complete_lattice
begin
lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)}) \ Inf (Sup ` A)"
  by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper)
end 

class complete_distrib_lattice = complete_lattice +
  assumes Inf_Sup_le: "Inf (Sup ` A) \ Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)})"
begin
  
lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\ Y \ A . f Y \ Y)})"
  by (rule order.antisym, rule Inf_Sup_le, rule Sup_Inf_le)

subclass distrib_lattice
proof
  fix a b c
  show "a \ b \ c = (a \ b) \ (a \ c)"
  proof (rule order.antisym, simp_all, safe)
    show "b \ c \ a \ b"
      by (rule le_infI1, simp)
    show "b \ c \ a \ c"
      by (rule le_infI2, simp)
    have [simp]: "a \ c \ a \ b \ c"
      by (rule le_infI1, simp)
    have [simp]: "b \ a \ a \ b \ c"
      by (rule le_infI2, simp)
    have "\(Sup ` {{a, b}, {a, c}}) =
      ⊔(Inf ` {f ` {{a, b}, {a, c}} | f. ∀Y∈{{a, b}, {a, c}}. f Y ∈ Y})"
      by (rule Inf_Sup)
    from this show "(a \ b) \ (a \ c) \ a \ b \ c"
      apply simp
      by (rule SUP_least, safe, simp_all)
  qed
qed
end

context complete_lattice
begin
context
  fixes f :: "'a \ 'b::complete_lattice"
  assumes "mono f"
begin

lemma mono_Inf: "f (\A) \ (\x\A. f x)"
  using ‹mono f› by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)

lemma mono_Sup: "(\x\A. f x) \ f (\A)"
  using ‹mono f› by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)

lemma mono_INF: "f (\i\I. A i) \ (\x\I. f (A x))"
  by (intro complete_lattice_class.INF_greatest monoD[OF ‹mono f›] INF_lower)

lemma mono_SUP: "(\x\I. f (A x)) \ f (\i\I. A i)"
  by (intro complete_lattice_class.SUP_least monoD[OF ‹mono f›] SUP_upper)

end

end

class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice
begin

lemma uminus_Inf: "- (\A) = \(uminus ` A)"
proof (rule order.antisym)
  show "- \A \ \(uminus ` A)"
    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
  show "\(uminus ` A) \ - \A"
    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
qed

lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)"
  by (simp add: uminus_Inf image_image)

lemma uminus_Sup: "- (\A) = \(uminus ` A)"
proof -
  have "\A = - \(uminus ` A)"
    by (simp add: image_image uminus_INF)
  then show ?thesis by simp
qed

lemma uminus_SUP: "- (\x\A. B x) = (\x\A. - B x)"
  by (simp add: uminus_Sup image_image)

end

class complete_linorder = linorder + complete_lattice
begin

lemma dual_complete_linorder:
  "class.complete_linorder Sup Inf sup (\) (>) inf \ \"
  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)

lemma complete_linorder_inf_min: "inf = min"
  by (auto intro: order.antisym simp add: min_def fun_eq_iff)

lemma complete_linorder_sup_max: "sup = max"
  by (auto intro: order.antisym simp add: max_def fun_eq_iff)

lemma Inf_less_iff: "\S < a \ (\x\S. x < a)"
  by (simp add: not_le [symmetric] le_Inf_iff)

lemma INF_less_iff: "(\i\A. f i) < a \ (\x\A. f x < a)"
  by (simp add: Inf_less_iff [of "f ` A"])

lemma less_Sup_iff: "a < \S \ (\x\S. a < x)"
  by (simp add: not_le [symmetric] Sup_le_iff)

lemma less_SUP_iff: "a < (\i\A. f i) \ (\x\A. a < f x)"
  by (simp add: less_Sup_iff [of _ "f ` A"])

lemma Sup_eq_top_iff [simp]: "\A = \ \ (\x<\. \i\A. x < i)"
proof
  assume *: "\A = \"
  show "(\x<\. \i\A. x < i)"
    unfolding * [symmetric]
  proof (intro allI impI)
    fix x
    assume "x < \A"
    then show "\i\A. x < i"
      by (simp add: less_Sup_iff)
  qed
next
  assume *: "\x<\. \i\A. x < i"
  show "\A = \"
  proof (rule ccontr)
    assume "\A \ \"
    with top_greatest [of "\A"] have "\A < \"
      unfolding le_less by auto
    with * have "\A < \A"
      unfolding less_Sup_iff by auto
    then show False by auto
  qed
qed

lemma SUP_eq_top_iff [simp]: "(\i\A. f i) = \ \ (\x<\. \i\A. x < f i)"
  using Sup_eq_top_iff [of "f ` A"] by simp

lemma Inf_eq_bot_iff [simp]: "\A = \ \ (\x>\. \i\A. i < x)"
  using dual_complete_linorder
  by (rule complete_linorder.Sup_eq_top_iff)

lemma INF_eq_bot_iff [simp]: "(\i\A. f i) = \ \ (\x>\. \i\A. f i < x)"
  using Inf_eq_bot_iff [of "f ` A"] by simp

lemma Inf_le_iff: "\A \ x \ (\y>x. \a\A. y > a)"
proof safe
  fix y
  assume "x \ \A" "y > x"
  then have "y > \A" by auto
  then show "\a\A. y > a"
    unfolding Inf_less_iff .
qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Inf_lower)

lemma INF_le_iff: "\(f ` A) \ x \ (\y>x. \i\A. y > f i)"
  using Inf_le_iff [of "f ` A"] by simp

lemma le_Sup_iff: "x \ \A \ (\ya\A. y < a)"
proof safe
  fix y
  assume "x \ \A" "y < x"
  then have "y < \A" by auto
  then show "\a\A. y < a"
    unfolding less_Sup_iff .
qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Sup_upper)

lemma le_SUP_iff: "x \ \(f ` A) \ (\yi\A. y < f i)"
  using le_Sup_iff [of _ "f ` A"] by simp

end

subsection ‹Complete lattice on 🍋‹bool››

instantiation bool :: complete_lattice
begin

definition [simp, code]: "\A \ False \ A"

definition [simp, code]: "\A \ True \ A"

instance
  by standard (auto intro: bool_induct)

end

lemma not_False_in_image_Ball [simp]: "False \ P ` A \ Ball A P"
  by auto

lemma True_in_image_Bex [simp]: "True \ P ` A \ Bex A P"
  by auto

lemma INF_bool_eq [simp]: "(\A f. \(f ` A)) = Ball"
  by (simp add: fun_eq_iff)

lemma SUP_bool_eq [simp]: "(\A f. \(f ` A)) = Bex"
  by (simp add: fun_eq_iff)

instance bool :: complete_boolean_algebra
  by (standard, fastforce)

subsection ‹Complete lattice on 🍋‹_ ==> _››

instantiation "fun" :: (type, Inf) Inf
begin

definition "\A = (\x. \f\A. f x)"

lemma Inf_apply [simp, code]: "(\A) x = (\f\A. f x)"
  by (simp add: Inf_fun_def)

instance ..

end

instantiation "fun" :: (type, Sup) Sup
begin

definition "\A = (\x. \f\A. f x)"

lemma Sup_apply [simp, code]: "(\A) x = (\f\A. f x)"
  by (simp add: Sup_fun_def)

instance ..

end

instantiation "fun" :: (type, complete_lattice) complete_lattice
begin

instance
  by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)

end

lemma INF_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)"
  by (simp add: image_comp)

lemma SUP_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)"
  by (simp add: image_comp)

subsection ‹Complete lattice on unary and binary predicates›

lemma Inf1_I: "(\P. P \ A \ P a) \ (\A) a"
  by auto

lemma INF1_I: "(\x. x \ A \ B x b) \ (\x\A. B x) b"
  by simp

lemma INF2_I: "(\x. x \ A \ B x b c) \ (\x\A. B x) b c"
  by simp

lemma Inf2_I: "(\r. r \ A \ r a b) \ (\A) a b"
  by auto

lemma Inf1_D: "(\A) a \ P \ A \ P a"
  by auto

lemma INF1_D: "(\x\A. B x) b \ a \ A \ B a b"
  by simp

lemma Inf2_D: "(\A) a b \ r \ A \ r a b"
  by auto

lemma INF2_D: "(\x\A. B x) b c \ a \ A \ B a b c"
  by simp

lemma Inf1_E:
  assumes "(\A) a"
  obtains "P a" | "P \ A"
  using assms by auto

lemma INF1_E:
  assumes "(\x\A. B x) b"
  obtains "B a b" | "a \ A"
  using assms by auto

lemma Inf2_E:
  assumes "(\A) a b"
  obtains "r a b" | "r \ A"
  using assms by auto

lemma INF2_E:
  assumes "(\x\A. B x) b c"
  obtains "B a b c" | "a \ A"
  using assms by auto

lemma Sup1_I: "P \ A \ P a \ (\A) a"
  by auto

lemma SUP1_I: "a \ A \ B a b \ (\x\A. B x) b"
  by auto

lemma Sup2_I: "r \ A \ r a b \ (\A) a b"
  by auto

lemma SUP2_I: "a \ A \ B a b c \ (\x\A. B x) b c"
  by auto

lemma Sup1_E:
  assumes "(\A) a"
  obtains P where "P \ A" and "P a"
  using assms by auto

lemma SUP1_E:
  assumes "(\x\A. B x) b"
  obtains x where "x \ A" and "B x b"
  using assms by auto

lemma Sup2_E:
  assumes "(\A) a b"
  obtains r where "r \ A" "r a b"
  using assms by auto

lemma SUP2_E:
  assumes "(\x\A. B x) b c"
  obtains x where "x \ A" "B x b c"
  using assms by auto


subsection ‹Complete lattice on 🍋‹_ set››

instantiation "set" :: (type) complete_lattice
begin

definition "\A = {x. \((\B. x \ B) ` A)}"

definition "\A = {x. \((\B. x \ B) ` A)}"

instance
  by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)

end

subsubsection ‹Inter›

abbreviation Inter :: "'a set set \ 'a set"  (‹∩›)
  where "\S \ \S"

lemma Inter_eq: "\A = {x. \B \ A. x \ B}"
proof (rule set_eqI)
  fix x
  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"
    by auto
  then show "x \ \A \ x \ {x. \B \ A. x \ B}"
    by (simp add: Inf_set_def image_def)
qed

lemma Inter_iff [simp]: "A \ \C \ (\X\C. A \ X)"
  by (unfold Inter_eq) blast

lemma InterI [intro!]: "(\X. X \ C \ A \ X) \ A \ \C"
  by (simp add: Inter_eq)

text ‹
  🚫 A ``destruct'' rule -- every 🍋‹X› in 🍋‹C›
  contains 🍋‹A› as an element, but 🍋‹A ∈ X› can hold when
  🍋‹X ∈ C› does not!  This rule is analogous to ‹spec›.
›

lemma InterD [elim, Pure.elim]: "A \ \C \ X \ C \ A \ X"
  by auto

lemma InterE [elim]: "A \ \C \ (X \ C \ R) \ (A \ X \ R) \ R"
  🍋 ‹``Classical'' elimination rule -- does not require proving
    🍋‹X ∈ C›.›
  unfolding Inter_eq by blast

lemma Inter_lower: "B \ A \ \A \ B"
  by (fact Inf_lower)

lemma Inter_subset: "(\X. X \ A \ X \ B) \ A \ {} \ \A \ B"
  by (fact Inf_less_eq)

lemma Inter_greatest: "(\X. X \ A \ C \ X) \ C \ \A"
  by (fact Inf_greatest)

lemma Inter_empty: "\{} = UNIV"
  by (fact Inf_empty) (* already simp *)

lemma Inter_UNIV: "\UNIV = {}"
  by (fact Inf_UNIV) (* already simp *)

lemma Inter_insert: "\(insert a B) = a \ \B"
  by (fact Inf_insert) (* already simp *)

lemma Inter_Un_subset: "\A \ \B \ \(A \ B)"
  by (fact less_eq_Inf_inter)

lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"
  by (fact Inf_union_distrib)

lemma Inter_UNIV_conv [simp]:
  "\A = UNIV \ (\x\A. x = UNIV)"
  "UNIV = \A \ (\x\A. x = UNIV)"
  by (fact Inf_top_conv)+

lemma Inter_anti_mono: "B \ A \ \A \ \B"
  by (fact Inf_superset_mono)


subsubsection ‹Intersections of families›

syntax (ASCII)
  "_INTER1"     :: "pttrns \ 'b set \ 'b set"           (‹(‹indent=3 notation=‹binder INT››INT _./ _)› [0, 10] 10)
  "_INTER"      :: "pttrn \ 'a set \ 'b set \ 'b set"  (‹(‹indent=3 notation=‹binder INT››INT _:_./ _)› [0, 0, 10] 10)

syntax
  "_INTER1"     :: "pttrns \ 'b set \ 'b set"           (‹(‹indent=3 notation=‹binder ∩››∩_./ _)› [0, 10] 10)
  "_INTER"      :: "pttrn \ 'a set \ 'b set \ 'b set"  (‹(‹indent=3 notation=‹binder ∩››∩_∈_./ _)› [0, 0, 10] 10)

syntax (latex output)
  "_INTER1"     :: "pttrns \ 'b set \ 'b set"           (‹(3∩(‹unbreakable›🚫_🚫)/ _)› [0, 10] 10)
  "_INTER"      :: "pttrn \ 'a set \ 'b set \ 'b set"  (‹(3∩(‹unbreakable›🚫_∈_🚫)/ _)› [0, 0, 10] 10)

syntax_consts
  "_INTER1" "_INTER" ⇌ Inter

translations
  "\x y. f"  ⇌ "\x. \y. f"
  "\x. f"    ⇌ "\(CONST range (\x. f))"
  "\x\A. f"  ⇌ "CONST Inter ((\x. f) ` A)"

lemma INTER_eq: "(\x\A. B x) = {y. \x\A. y \ B x}"
  by (auto intro!: INF_eqI)

lemma INT_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"
  using Inter_iff [of _ "B ` A"] by simp

lemma INT_I [intro!]: "(\x. x \ A \ b \ B x) \ b \ (\x\A. B x)"
  by auto

lemma INT_D [elim, Pure.elim]: "b \ (\x\A. B x) \ a \ A \ b \ B a"
  by auto

lemma INT_E [elim]: "b \ (\x\A. B x) \ (b \ B a \ R) \ (a \ A \ R) \ R"
  🍋 ‹"Classical" elimination -- by the Excluded Middle on 🍋‹a∈A›.›
  by auto

lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"
  by blast

lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"
  by blast

lemma INT_lower: "a \ A \ (\x\A. B x) \ B a"
  by (fact INF_lower)

lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)"
  by (fact INF_greatest)

lemma INT_empty: "(\x\{}. B x) = UNIV"
  by (fact INF_empty)

lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"
  by (fact INF_absorb)

lemma INT_subset_iff: "B \ (\i\I. A i) \ (\i\I. B \ A i)"
  by (fact le_INF_iff)

lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ \ (B ` A)"
  by (fact INF_insert)

lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"
  by (fact INF_union)

lemma INT_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"
  by blast

lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"
  by (fact INF_constant)

lemma INTER_UNIV_conv:
  "(UNIV = (\x\A. B x)) = (\x\A. B x = UNIV)"
  "((\x\A. B x) = UNIV) = (\x\A. B x = UNIV)"
  by (fact INF_top_conv)+ (* already simp *)

lemma INT_bool_eq: "(\b. A b) = A True \ A False"
  by (fact INF_UNIV_bool_expand)

lemma INT_anti_mono: "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\B. f x) \ (\x\A. g x)"
  🍋 ‹The last inclusion is POSITIVE!›
  by (fact INF_superset_mono)

lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"
  by blast

lemma vimage_INT: "f -` (\x\A. B x) = (\x\A. f -` B x)"
  by blast


subsubsection ‹Union›

abbreviation Union :: "'a set set \ 'a set"  (‹∪›)
  where "\S \ \S"

lemma Union_eq: "\A = {x. \B \ A. x \ B}"
proof (rule set_eqI)
  fix x
  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"
    by auto
  then show "x \ \A \ x \ {x. \B\A. x \ B}"
    by (simp add: Sup_set_def image_def)
qed

lemma Union_iff [simp]: "A \ \C \ (\X\C. A\X)"
  by (unfold Union_eq) blast

lemma UnionI [intro]: "X \ C \ A \ X \ A \ \C"
  🍋 ‹The order of the premises presupposes that 🍋‹C› is rigid;
    🍋‹A› may be flexible.›
  by auto

lemma UnionE [elim!]: "A \ \C \ (\X. A \ X \ X \ C \ R) \ R"
  by auto

lemma Union_upper: "B \ A \ B \ \A"
  by (fact Sup_upper)

lemma Union_least: "(\X. X \ A \ X \ C) \ \A \ C"
  by (fact Sup_least)

lemma Union_empty: "\{} = {}"
  by (fact Sup_empty) (* already simp *)

lemma Union_UNIV: "\UNIV = UNIV"
  by (fact Sup_UNIV) (* already simp *)

lemma Union_insert: "\(insert a B) = a \ \B"
  by (fact Sup_insert) (* already simp *)

lemma Union_Un_distrib [simp]: "\(A \ B) = \A \ \B"
  by (fact Sup_union_distrib)

lemma Union_Int_subset: "\(A \ B) \ \A \ \B"
  by (fact Sup_inter_less_eq)

lemma Union_empty_conv: "(\A = {}) \ (\x\A. x = {})"
  by (fact Sup_bot_conv) (* already simp *)

lemma empty_Union_conv: "({} = \A) \ (\x\A. x = {})"
  by (fact Sup_bot_conv) (* already simp *)

lemma subset_Pow_Union: "A \ Pow (\A)"
  by blast

lemma Union_Pow_eq [simp]: "\(Pow A) = A"
  by blast

lemma Union_mono: "A \ B \ \A \ \B"
  by (fact Sup_subset_mono)

lemma Union_subsetI: "(\x. x \ A \ \y. y \ B \ x \ y) \ \A \ \B"
  by blast

lemma disjnt_inj_on_iff:
 "\inj_on f (\\); X \ \; Y \ \\ \ disjnt (f ` X) (f ` Y) \ disjnt X Y"
  unfolding disjnt_def
  by safe (use inj_on_eq_iff in ‹fastforce+›)

lemma disjnt_Union1 [simp]: "disjnt (\\) B \ (\A \ \. disjnt A B)"
  by (auto simp: disjnt_def)

lemma disjnt_Union2 [simp]: "disjnt B (\\) \ (\A \ \. disjnt B A)"
  by (auto simp: disjnt_def)


subsubsection ‹Unions of families›

syntax (ASCII)
  "_UNION1"     :: "pttrns => 'b set => 'b set"           (‹(‹indent=3 notation=‹binder UN››UN _./ _)› [0, 10] 10)
  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (‹(‹indent=3 notation=‹binder UN››UN _:_./ _)› [0, 0, 10] 10)

syntax
  "_UNION1"     :: "pttrns => 'b set => 'b set"           (‹(‹indent=3 notation=‹binder ∪››∪_./ _)› [0, 10] 10)
  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (‹(‹indent=3 notation=‹binder ∪››∪_∈_./ _)› [0, 0, 10] 10)

syntax (latex output)
  "_UNION1"     :: "pttrns => 'b set => 'b set"           (‹(3∪(‹unbreakable›🚫_🚫)/ _)› [0, 10] 10)
  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (‹(3∪(‹unbreakable›🚫_∈_🚫)/ _)› [0, 0, 10] 10)

syntax_consts
  "_UNION1" "_UNION" ⇌ Union

translations
  "\x y. f"   ⇌ "\x. \y. f"
  "\x. f"     ⇌ "\(CONST range (\x. f))"
  "\x\A. f"   ⇌ "CONST Union ((\x. f) ` A)"

text ‹
  Note the difference between ordinary syntax of indexed
  unions and intersections (e.g.\ ‹∪a🚫1∈A🚫1. B›)
  and their \LaTeX\ rendition: 🍋‹∪a🚫1∈A🚫1. B›.
›

lemma disjoint_UN_iff: "disjnt A (\i\I. B i) \ (\i\I. disjnt A (B i))"
  by (auto simp: disjnt_def)

lemma UNION_eq: "(\x\A. B x) = {y. \x\A. y \ B x}"
  by (auto intro!: SUP_eqI)

lemma bind_UNION [code]: "Set.bind A f = \(f ` A)"
  by (simp add: bind_def UNION_eq)

lemma member_bind [simp]: "x \ Set.bind A f \ x \ \(f ` A)"
  by (simp add: bind_UNION)

lemma Union_SetCompr_eq: "\{f x| x. P x} = {a. \x. P x \ a \ f x}"
  by blast

lemma UN_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"
  using Union_iff [of _ "B ` A"] by simp

lemma UN_I [intro]: "a \ A \ b \ B a \ b \ (\x\A. B x)"
  🍋 ‹The order of the premises presupposes that 🍋‹A› is rigid;
    🍋‹b› may be flexible.›
  by auto

lemma UN_E [elim!]: "b \ (\x\A. B x) \ (\x. x\A \ b \ B x \ R) \ R"
  by auto

lemma UN_upper: "a \ A \ B a \ (\x\A. B x)"
  by (fact SUP_upper)

lemma UN_least: "(\x. x \ A \ B x \ C) \ (\x\A. B x) \ C"
  by (fact SUP_least)

lemma Collect_bex_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"
  by blast

lemma UN_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"
  by blast

lemma UN_empty: "(\x\{}. B x) = {}"
  by (fact SUP_empty)

lemma UN_empty2: "(\x\A. {}) = {}"
  by (fact SUP_bot) (* already simp *)

lemma UN_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"
  by (fact SUP_absorb)

lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ \(B ` A)"
  by (fact SUP_insert)

lemma UN_Un [simp]: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"
  by (fact SUP_union)

lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"
  by blast

lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"
  by (fact SUP_le_iff)

lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"
  by (fact SUP_constant)

lemma UNION_singleton_eq_range: "(\x\A. {f x}) = f ` A"
  by blast

lemma image_Union: "f ` \S = (\x\S. f ` x)"
  by blast

lemma UNION_empty_conv:
  "{} = (\x\A. B x) \ (\x\A. B x = {})"
  "(\x\A. B x) = {} \ (\x\A. B x = {})"
  by (fact SUP_bot_conv)+ (* already simp *)

lemma Collect_ex_eq: "{x. \y. P x y} = (\y. {x. P x y})"
  by blast

lemma ball_UN: "(\z \ \(B ` A). P z) \ (\x\A. \z \ B x. P z)"
  by blast

lemma bex_UN: "(\z \ \(B ` A). P z) \ (\x\A. \z\B x. P z)"
  by blast

lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"
  by safe (auto simp add: if_split_mem2)

lemma UN_bool_eq: "(\b. A b) = (A True \ A False)"
  by (fact SUP_UNIV_bool_expand)

lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"
  by blast

lemma UN_mono:
  "A \ B \ (\x. x \ A \ f x \ g x) \
    (∪x∈A. f x) ⊆ (∪x∈B. g x)"
  by (fact SUP_subset_mono)

lemma vimage_Union: "f -` (\A) = (\X\A. f -` X)"
  by blast

lemma vimage_UN: "f -` (\x\A. B x) = (\x\A. f -` B x)"
  by blast

lemma vimage_eq_UN: "f -` B = (\y\B. f -` {y})"
  🍋 ‹NOT suitable for rewriting›
  by blast

lemma image_UN: "f ` \(B ` A) = (\x\A. f ` B x)"
  by blast

lemma UN_singleton [simp]: "(\x\A. {x}) = A"
  by blast

lemma inj_on_image: "inj_on f (\A) \ inj_on ((`) f) A"
  unfolding inj_on_def by blast


subsubsection ‹Distributive laws›

lemma Int_Union: "A \ \B = (\C\B. A \ C)"
  by blast

lemma Un_Inter: "A \ \B = (\C\B. A \ C)"
  by blast

lemma Int_Union2: "\B \ A = (\C\B. C \ A)"
  by blast

lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"
  by (rule sym) (rule INF_inf_distrib)

lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"
  by (rule sym) (rule SUP_sup_distrib)

lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)"  (* FIXME drop *)
  by (simp add: INT_Int_distrib)

lemma Int_Inter_eq: "A \ \\ = (if \={} then A else (\B\\. A \ B))"
                    "\\ \ A = (if \={} then A else (\B\\. B \ A))"
  by auto

lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)"  (* FIXME drop *)
  🍋 ‹Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:›
  🍋 ‹Union of a family of unions›
  by (simp add: UN_Un_distrib)

lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"
  by blast

lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"
  🍋 ‹Halmos, Naive Set Theory, page 35.›
  by blast

lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"
  by blast

lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"
  by blast

lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})"
  by blast

lemma SUP_UNION: "(\x\(\y\A. g y). f x) = (\y\A. \x\g y. f x :: _ :: complete_lattice)"
  by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+


subsection ‹Injections and bijections›

lemma inj_on_Inter: "S \ {} \ (\A. A \ S \ inj_on f A) \ inj_on f (\S)"
  unfolding inj_on_def by blast

lemma inj_on_INTER: "I \ {} \ (\i. i \ I \ inj_on f (A i)) \ inj_on f (\i \ I. A i)"
  unfolding inj_on_def by safe simp

lemma inj_on_UNION_chain:
  assumes chain: "\i j. i \ I \ j \ I \ A i \ A j \ A j \ A i"
    and inj: "\i. i \ I \ inj_on f (A i)"
  shows "inj_on f (\i \ I. A i)"
proof -
  have "x = y"
    if *: "i \ I" "j \ I"
    and **: "x \ A i" "y \ A j"
    and ***: "f x = f y"
    for i j x y
    using chain [OF *]
  proof
    assume "A i \ A j"
    with ** have "x \ A j" by auto
    with inj * ** *** show ?thesis
      by (auto simp add: inj_on_def)
  next
    assume "A j \ A i"
    with ** have "y \ A i" by auto
    with inj * ** *** show ?thesis
      by (auto simp add: inj_on_def)
  qed
  then show ?thesis
    by (unfold inj_on_def UNION_eq) auto
qed

lemma bij_betw_UNION_chain:
  assumes chain: "\i j. i \ I \ j \ I \ A i \ A j \ A j \ A i"
    and bij: "\i. i \ I \ bij_betw f (A i) (A' i)"
  shows "bij_betw f (\i \ I. A i) (\i \ I. A' i)"
  unfolding bij_betw_def
proof safe
  have "\i. i \ I \ inj_on f (A i)"
    using bij bij_betw_def[of f] by auto
  then show "inj_on f (\(A ` I))"
    using chain inj_on_UNION_chain[of I A f] by auto
next
  fix i x
  assume *: "i \ I" "x \ A i"
  with bij have "f x \ A' i"
    by (auto simp: bij_betw_def)
  with * show "f x \ \(A' ` I)" by blast
next
  fix i x'
  assume *: "i \ I" "x' \ A' i"
  with bij have "\x \ A i. x' = f x"
    unfolding bij_betw_def by blast
  with * have "\j \ I. \x \ A j. x' = f x"
    by blast
  then show "x' \ f ` \(A ` I)"
    by blast
qed

(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
lemma image_INT: "inj_on f C \ \x\A. B x \ C \ j \ A \ f ` (\(B ` A)) = (\x\A. f ` B x)"
  by (auto simp add: inj_on_def) blast

lemma bij_image_INT: "bij f \ f ` (\(B ` A)) = (\x\A. f ` B x)"
  by (auto simp: bij_def inj_def surj_def) blast

lemma UNION_fun_upd: "\(A(i := B) ` J) = \(A ` (J - {i})) \ (if i \ J then B else {})"
  by (auto simp add: set_eq_iff)

lemma bij_betw_Pow:
  assumes "bij_betw f A B"
  shows "bij_betw (image f) (Pow A) (Pow B)"
proof -
  from assms have "inj_on f A"
    by (rule bij_betw_imp_inj_on)
  then have "inj_on f (\(Pow A))"
    by simp
  then have "inj_on (image f) (Pow A)"
    by (rule inj_on_image)
  then have "bij_betw (image f) (Pow A) (image f ` Pow A)"
    by (rule inj_on_imp_bij_betw)
  moreover from assms have "f ` A = B"
    by (rule bij_betw_imp_surj_on)
  then have "image f ` Pow A = Pow B"
    by (rule image_Pow_surj)
  ultimately show ?thesis by simp
qed


subsubsection ‹Complement›

lemma Compl_INT [simp]: "- (\x\A. B x) = (\x\A. -B x)"
  by blast

lemma Compl_UN [simp]: "- (\x\A. B x) = (\x\A. -B x)"
  by blast

subsubsection ‹Miniscoping and maxiscoping›

text ‹🚫 Miniscoping: pushing in quantifiers and big Unions and Intersections.›

lemma UN_simps [simp]:
  "\a B C. (\x\C. insert a (B x)) = (if C={} then {} else insert a (\x\C. B x))"
  "\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))"
  "\A B C. (\x\C. A \ B x) = ((if C={} then {} else A \ (\x\C. B x)))"
  "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)"
  "\A B C. (\x\C. A \ B x) = (A \(\x\C. B x))"
  "\A B C. (\x\C. A x - B) = ((\x\C. A x) - B)"
  "\A B C. (\x\C. A - B x) = (A - (\x\C. B x))"
  "\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"
  "\A B C. (\z\(\(B ` A)). C z) = (\x\A. \z\B x. C z)"
  "\A B f. (\x\f`A. B x) = (\a\A. B (f a))"
  by auto

lemma INT_simps [simp]:
  "\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \ B)"
  "\A B C. (\x\C. A \ B x) = (if C={} then UNIV else A \(\x\C. B x))"
  "\A B C. (\x\C. A x - B) = (if C={} then UNIV else (\x\C. A x) - B)"
  "\A B C. (\x\C. A - B x) = (if C={} then UNIV else A - (\x\C. B x))"
  "\a B C. (\x\C. insert a (B x)) = insert a (\x\C. B x)"
  "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)"
  "\A B C. (\x\C. A \ B x) = (A \ (\x\C. B x))"
  "\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"
  "\A B C. (\z\(\(B ` A)). C z) = (\x\A. \z\B x. C z)"
  "\A B f. (\x\f`A. B x) = (\a\A. B (f a))"
  by auto

lemma UN_ball_bex_simps [simp]:
  "\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"
  "\A B P. (\x\(\(B ` A)). P x) = (\a\A. \x\ B a. P x)"
  "\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"
  "\A B P. (\x\(\(B ` A)). P x) \ (\a\A. \x\B a. P x)"
  by auto


text ‹🚫 Maxiscoping: pulling out big Unions and Intersections.›

lemma UN_extend_simps:
  "\a B C. insert a (\x\C. B x) = (if C={} then {a} else (\x\C. insert a (B x)))"
  "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"
  "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"
  "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"
  "\A B C. (A \ (\x\C. B x)) = (\x\C. A \ B x)"
  "\A B C. ((\x\C. A x) - B) = (\x\C. A x - B)"
  "\A B C. (A - (\x\C. B x)) = (\x\C. A - B x)"
  "\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"
  "\A B C. (\x\A. \z\B x. C z) = (\z\(\(B ` A)). C z)"
  "\A B f. (\a\A. B (f a)) = (\x\f`A. B x)"
  by auto

lemma INT_extend_simps:
  "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"
  "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"
  "\A B C. (\x\C. A x) - B = (if C={} then UNIV - B else (\x\C. A x - B))"
  "\A B C. A - (\x\C. B x) = (if C={} then A else (\x\C. A - B x))"
  "\a B C. insert a (\x\C. B x) = (\x\C. insert a (B x))"
  "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"
  "\A B C. A \ (\x\C. B x) = (\x\C. A \ B x)"
  "\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"
  "\A B C. (\x\A. \z\B x. C z) = (\z\(\(B ` A)). C z)"
  "\A B f. (\a\A. B (f a)) = (\x\f`A. B x)"
  by auto

text ‹Finally›

lemmas mem_simps =
  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
  🍋 ‹Each of these has ALREADY been added ‹[simp]› above.›

end