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 \<open>Complete lattices\<close>

theory Complete_Lattices
  imports Fun
begin

subsection \<open>Syntactic infimum and supremum operations\<close>

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" \<rightleftharpoons> Inf and
  "_SUP1" "_SUP" \<rightleftharpoons> 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 \<open>Abstract complete lattices\<close>

text \<open>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.\<close>

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 \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower)
  with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> 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 \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper)
  with \<open>a \<le> b\<close> show "a \<le> \<Squnion>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)"
  \<comment> \<open>The last inclusion is POSITIVE!\<close>
  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 \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
  moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> 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 \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
  moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> 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 \<open>\<Sqinter>A = \<top>\<close> \<open>x \<noteq> \<top>\<close> 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 \<open>y < (\<Sqinter>i\<in>A. f i)\<close>
  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 \<open>i \<in> A\<close> by (rule SUP_upper)
  also note \<open>(\<Squnion>i\<in>A. f i) < y\<close>
  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}}) =
      \<Squnion>(Inf ` {f ` {{a, b}, {a, c}} | f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> 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 \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)

lemma mono_Sup: "(\x\A. f x) \ f (\A)"
  using \<open>mono f\<close> 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 \<open>mono f\<close>] INF_lower)

lemma mono_SUP: "(\x\I. f (A x)) \ f (\i\I. A i)"
  by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] 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 \<open>Complete lattice on \<^typ>\<open>bool\<close>\<close>

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 \<open>Complete lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>

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 \<open>Complete lattice on unary and binary predicates\<close>

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 \<open>Complete lattice on \<^typ>\<open>_ set\<close>\<close>

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 \<open>Inter\<close>

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 \<open>
  \<^medskip> A ``destruct'' rule -- every \<^term>\<open>X\<close> in \<^term>\<open>C\<close>
  contains \<^term>\<open>A\<close> as an element, but \<^prop>\<open>A \<in> X\<close> can hold when
  \<^prop>\<open>X \<in> C\<close> does not!  This rule is analogous to \<open>spec\<close>.
\<close>

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"
  \<comment> \<open>``Classical'' elimination rule -- does not require proving
    \<^prop>\<open>X \<in> C\<close>.\<close>
  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 \<open>Intersections of families\<close>

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\\<^bsub>_\<^esub>)/ _)\ [0, 10] 10)
  "_INTER"      :: "pttrn \ 'a set \ 'b set \ 'b set" (\(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)\ [0, 0, 10] 10)

syntax_consts
  "_INTER1" "_INTER" \<rightleftharpoons> 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"
  \<comment> \<open>"Classical" elimination -- by the Excluded Middle on \<^prop>\<open>a\<in>A\<close>.\<close>
  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)"
  \<comment> \<open>The last inclusion is POSITIVE!\<close>
  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 \<open>Union\<close>

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"
  \<comment> \<open>The order of the premises presupposes that \<^term>\<open>C\<close> is rigid;
    \<^term>\<open>A\<close> may be flexible.\<close>
  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 \<open>fastforce+\<close>)

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 \<open>Unions of families\<close>

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

syntax
  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_./ _)\<close> [0, 10] 10)
  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)

syntax (latex output)
  "_UNION1"     :: "pttrns => 'b set => 'b set"           (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)\<close> [0, 0, 10] 10)

syntax_consts
  "_UNION1" "_UNION" \<rightleftharpoons> Union

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

text \<open>
  Note the difference between ordinary syntax of indexed
  unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>)
  and their \LaTeX\ rendition: \<^term>\<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>.
\<close>

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)"
  \<comment> \<open>The order of the premises presupposes that \<^term>\<open>A\<close> is rigid;
    \<^term>\<open>b\<close> may be flexible.\<close>
  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) \
    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>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})"
  \<comment> \<open>NOT suitable for rewriting\<close>
  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 \<open>Distributive laws\<close>

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 *)
  \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
  \<comment> \<open>Union of a family of unions\<close>
  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)"
  \<comment> \<open>Halmos, Naive Set Theory, page 35.\<close>
  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 \<open>Injections and bijections\<close>

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 \<open>Complement\<close>

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 \<open>Miniscoping and maxiscoping\<close>

text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close>

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 \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close>

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 \<open>Finally\<close>

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
  \<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>

end

quality98%

¤ Dauer der Verarbeitung: 0.23 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.