Theory CZH_Sets_Sets

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Further set algebra and other miscellaneous results›
theory CZH_Sets_Sets
imports CZH_Sets_Introduction
begin

subsection‹Background›

text‹
This section presents further set algebra and various elementary properties
of sets.

Many of the results that are presented in this section
were carried over (with amendments) from the theories \<^text>‹Set›
and \<^text>‹Complete_Lattices› in the main library.
›

declare elts_sup_iff[simp del]

subsection‹Further notation›

subsubsection‹Set membership›

abbreviation vmember :: "V ⇒ V ⇒ bool" ("(_/ ∈⇩∘ _)" [51, 51] 50)
where "vmember x A ≡ (x ∈ elts A)"
notation vmember ("'(∈⇩∘')")
and vmember ("(_/ ∈⇩∘ _)" [51, 51] 50)

abbreviation not_vmember :: "V ⇒ V ⇒ bool" ("(_/ ∉⇩∘ _)" [51, 51] 50)
where "not_vmember x A ≡ (x ∉ elts A)"
notation
not_vmember ("'(∉⇩∘')") and
not_vmember ("(_/ ∉⇩∘ _)" [51, 51] 50)

subsubsection‹Subsets›

abbreviation vsubset :: "V ⇒ V ⇒ bool"
where "vsubset ≡ less"
abbreviation vsubset_eq :: "V ⇒ V ⇒ bool"
where "vsubset_eq ≡ less_eq"

notation vsubset ("'(⊂⇩∘')")
and vsubset ("(_/ ⊂⇩∘ _)" [51, 51] 50)
and vsubset_eq ("'(⊆⇩∘')")
and vsubset_eq ("(_/ ⊆⇩∘ _)" [51, 51] 50)

subsubsection‹Ball›

syntax
"_VBall" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∀(_/∈⇩∘_)./ _)" [0, 0, 10] 10)
"_VBex" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∃(_/∈⇩∘_)./ _)" [0, 0, 10] 10)
"_VBex1" :: "pttrn ⇒ V ⇒ bool ⇒ bool" ("(3∃!(_/∈⇩∘_)./ _)" [0, 0, 10] 10)

translations
"∀x∈⇩∘A. P" ⇌ "CONST Ball (CONST elts A) (λx. P)"
"∃x∈⇩∘A. P" ⇌ "CONST Bex (CONST elts A) (λx. P)"
"∃!x∈⇩∘A. P" ⇀ "∃!x. x ∈⇩∘ A ∧ P"

subsubsection‹‹VLambda››

text‹The following notation was adapted from \<^cite>‹"paulson_hereditarily_2013"›.›

syntax "_vlam" :: "[pttrn, V, V] ⇒ V" (‹(3λ_∈⇩∘_./ _)› 10)
translations "λx∈⇩∘A. f" ⇌ "CONST VLambda A (λx. f)"

subsubsection‹Intersection and union›

abbreviation vintersection :: "V ⇒ V ⇒ V" (infixl "∩⇩∘" 70)
where "(∩⇩∘) ≡ (⊓)"
notation vintersection (infixl "∩⇩∘" 70)

abbreviation vunion :: "V ⇒ V ⇒ V"  (infixl "∪⇩∘" 65)
where "vunion ≡ sup"
notation vunion (infixl "∪⇩∘" 65)

abbreviation VInter :: "V ⇒ V" (‹⋂⇩∘›)
where "⋂⇩∘ A ≡ ⨅ (elts A)"
notation VInter (‹⋂⇩∘›)

abbreviation VUnion :: "V ⇒ V" (‹⋃⇩∘›)
where "⋃⇩∘A ≡ ⨆ (elts A)"
notation VUnion (‹⋃⇩∘›)

subsubsection‹Miscellaneous›

notation app (‹_⦇_⦈› [999, 50] 999)
notation vtimes (infixr "×⇩∘" 80)

subsection‹Elementary results.›

lemma vempty_nin[simp]: "a ∉⇩∘ 0" by simp

lemma vemptyE:
assumes "A ≠ 0"
obtains x where "x ∈⇩∘ A"

lemma in_set_CollectI:
assumes "P x" and "small {x. P x}"
shows "x ∈⇩∘ set {x. P x}"
using assms by simp

lemma small_setcompr2:
assumes "small {f x y | x y. P x y}" and "a ∈⇩∘ set {f x y | x y. P x y}"
obtains x' y' where "a = f x' y'" and "P x' y'"
using assms by auto

lemma in_small_setI:
assumes "small A" and "x ∈ A"
shows "x ∈⇩∘ set A"
using assms by simp

lemma in_small_setD:
assumes "x ∈⇩∘ set A" and "small A"
shows "x ∈ A"
using assms by simp

lemma in_small_setE:
assumes "a ∈⇩∘ set A" and "small A"
obtains "a ∈ A"
using assms by auto

lemma small_set_vsubset:
assumes "small A" and "A ⊆ elts B"
shows "set A ⊆⇩∘ B"
using assms by auto

lemma some_in_set_if_set_neq_vempty[simp]:
assumes "A ≠ 0"
shows "(SOME x. x ∈⇩∘ A) ∈⇩∘ A"
by (meson assms someI_ex vemptyE)

lemma small_vsubset_set[intro, simp]:
assumes "small B" and "A ⊆ B"
shows "set A ⊆⇩∘ set B"
using assms by (auto simp: subset_iff_less_eq_V)

lemma vset_neq_1:
assumes "b ∉⇩∘ A" and "a ∈⇩∘ A"
shows "b ≠ a"
using assms by auto

lemma vset_neq_2:
assumes "b ∈⇩∘ A" and "a ∉⇩∘ A"
shows "b ≠ a"
using assms by auto

lemma nin_vinsertI:
assumes "a ≠ b" and "a ∉⇩∘ A"
shows "a ∉⇩∘ vinsert b A"
using assms by clarsimp

lemma vsubset_if_subset:
assumes "elts A ⊆ elts B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma small_set_comprehension[simp]: "small {A i | i. i ∈⇩∘ I}"
proof(rule smaller_than_small)
show "small (A ` elts I)" by auto
qed auto

subsection‹‹VBall››

lemma vball_cong:
assumes "A = B" and "⋀x. x ∈⇩∘ B ⟹ P x ⟷ Q x"
shows "(∀x∈⇩∘A. P x) ⟷ (∀x∈⇩∘B. Q x)"

lemma vball_cong_simp[cong]:
assumes "A = B" and "⋀x. x ∈⇩∘ B =simp=> P x ⟷ Q x "
shows "(∀x∈⇩∘A. P x) ⟷ (∀x∈⇩∘B. Q x)"
using assms by (simp add: simp_implies_def)

subsection‹‹VBex››

lemma vbex_cong:
assumes "A = B" and  "⋀x. x ∈⇩∘ B ⟹ P x ⟷ Q x"
shows "(∃x∈⇩∘A. P x) ⟷ (∃x∈⇩∘B. Q x)"
using assms by (simp cong: conj_cong)

lemma vbex_cong_simp[cong]:
assumes "A = B" and "⋀x. x ∈⇩∘ B =simp=> P x ⟷ Q x "
shows "(∃x∈⇩∘A. P x) ⟷ (∃x∈⇩∘B. Q x)"
using assms by (simp add:  simp_implies_def)

subsection‹Subset›

text‹Rules.›

lemma vsubset_antisym:
assumes "A ⊆⇩∘ B" and "B ⊆⇩∘ A"
shows "A = B"
using assms by simp

lemma vsubsetI:
assumes "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vpsubsetI:
assumes "A ⊆⇩∘ B" and "x ∉⇩∘ A" and "x ∈⇩∘ B"
shows "A ⊂⇩∘ B"
using assms unfolding less_V_def by auto

lemma vsubsetD:
assumes "A ⊆⇩∘ B"
shows "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B"
using assms by auto

lemma vsubsetE:
assumes "A ⊆⇩∘ B" and "(⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B) ⟹ P"
shows P
using assms by auto

lemma vpsubsetE:
assumes "A ⊂⇩∘ B"
obtains x where "A ⊆⇩∘ B" and "x ∉⇩∘ A" and "x ∈⇩∘ B"
using assms unfolding less_V_def by (meson V_equalityI vsubsetE)

lemma vsubset_iff: "A ⊆⇩∘ B ⟷ (∀t. t ∈⇩∘ A ⟶ t ∈⇩∘ B)" by blast

text‹Elementary properties.›

lemma vsubset_eq: "A ⊆⇩∘ B ⟷ (∀x∈⇩∘A. x ∈⇩∘ B)" by auto

lemma vsubset_transitive[intro]:
assumes "A ⊆⇩∘ B" and "B ⊆⇩∘ C"
shows "A ⊆⇩∘ C"
using assms by simp

lemma vsubset_reflexive: "A ⊆⇩∘ A" by simp

text‹Set operations.›

lemma vsubset_vempty: "0 ⊆⇩∘ A" by simp

lemma vsubset_vsingleton_left: "set {a} ⊆⇩∘ A ⟷ a ∈⇩∘ A" by auto

lemmas vsubset_vsingleton_leftD[dest] = vsubset_vsingleton_left[THEN iffD1]
and vsubset_vsingleton_leftI[intro] = vsubset_vsingleton_left[THEN iffD2]

lemma vsubset_vsingleton_right: "A ⊆⇩∘ set {a} ⟷ A = set {a} ∨ A = 0"
by (auto intro!: vsubset_antisym)

lemmas vsubset_vsingleton_rightD[dest] = vsubset_vsingleton_right[THEN iffD1]
and vsubset_vsingleton_rightI[intro] = vsubset_vsingleton_right[THEN iffD2]

lemma vsubset_vdoubleton_leftD[dest]:
assumes "set {a, b} ⊆⇩∘ A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A"
using assms by auto

lemma vsubset_vdoubleton_leftI[intro]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "set {a, b} ⊆⇩∘ A"
using assms by auto

lemma vsubset_vinsert_leftD[dest]:
assumes "vinsert a A ⊆⇩∘ B"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vsubset_vinsert_leftI[intro]:
assumes "A ⊆⇩∘ B" and "a ∈⇩∘ B"
shows "vinsert a A ⊆⇩∘ B"
using assms by auto

lemma vsubset_vinsert_vinsertI[intro]:
assumes "A ⊆⇩∘ vinsert b B"
shows "vinsert b A ⊆⇩∘ vinsert b B"
using assms by auto

lemma vsubset_vinsert_rightI[intro]:
assumes "A ⊆⇩∘ B"
shows "A ⊆⇩∘ vinsert b B"
using assms by auto

lemmas vsubset_VPow = VPow_le_VPow_iff

lemmas vsubset_VPowD = vsubset_VPow[THEN iffD1]
and vsubset_VPowI = vsubset_VPow[THEN iffD2]

text‹Special properties.›

assumes "A ⊆⇩∘ B" and "c ∉⇩∘ B"
shows "c ∉⇩∘ A"
using assms by auto

subsection‹Equality›

text‹Rules.›

lemma vequalityD1:
assumes "A = B"
shows "A ⊆⇩∘ B"
using assms by simp

lemma vequalityD2:
assumes "A = B"
shows "B ⊆⇩∘ A"
using assms by simp

lemma vequalityE:
assumes "A = B" and "⟦ A ⊆⇩∘ B; B ⊆⇩∘ A ⟧ ⟹ P"
shows P
using assms by simp

lemma vequalityCE[elim]:
assumes "A = B" and "⟦ c ∈⇩∘ A; c ∈⇩∘ B ⟧ ⟹ P" and "⟦ c ∉⇩∘ A; c ∉⇩∘ B ⟧ ⟹ P"
shows P
using assms by auto

subsection‹Binary intersection›

lemma vintersection_def: "A ∩⇩∘ B = set {x. x ∈⇩∘ A ∧ x ∈⇩∘ B}"
by (metis Int_def inf_V_def)

lemma small_vintersection_set[simp]: "small {x. x ∈⇩∘ A ∧ x ∈⇩∘ B}"
by (rule down[of _ A]) auto

text‹Rules.›

lemma vintersection_iff[simp]: "x ∈⇩∘ A ∩⇩∘ B ⟷ x ∈⇩∘ A ∧ x ∈⇩∘ B"
unfolding vintersection_def by simp

lemma vintersectionI[intro!]:
assumes "x ∈⇩∘ A" and "x ∈⇩∘ B"
shows "x ∈⇩∘ A ∩⇩∘ B"
using assms by simp

lemma vintersectionD1[dest]:
assumes "x ∈⇩∘ A ∩⇩∘ B"
shows "x ∈⇩∘ A"
using assms by simp

lemma vintersectionD2[dest]:
assumes "x ∈⇩∘ A ∩⇩∘ B"
shows "x ∈⇩∘ B"
using assms by simp

lemma vintersectionE[elim!]:
assumes "x ∈⇩∘ A ∩⇩∘ B" and "x ∈⇩∘ A ⟹ x ∈⇩∘ B ⟹ P"
shows P
using assms by simp

text‹Elementary properties.›

lemma vintersection_intersection: "A ∩⇩∘ B = set (elts A ∩ elts B)"
unfolding inf_V_def by simp

lemma vintersection_assoc: "A ∩⇩∘ (B ∩⇩∘ C) = (A ∩⇩∘ B) ∩⇩∘ C" by auto

lemma vintersection_commute: "A ∩⇩∘ B = B ∩⇩∘ A" by auto

text‹Previous set operations.›

lemma vsubset_vintersection_right: "A ⊆⇩∘ (B ∩⇩∘ C) = (A ⊆⇩∘ B ∧ A ⊆⇩∘ C)"
by clarsimp

lemma vsubset_vintersection_rightD[dest]:
assumes "A ⊆⇩∘ (B ∩⇩∘ C)"
shows "A ⊆⇩∘ B" and "A ⊆⇩∘ C"
using assms by auto

lemma vsubset_vintersection_rightI[intro]:
assumes "A ⊆⇩∘ B" and "A ⊆⇩∘ C"
shows "A ⊆⇩∘ (B ∩⇩∘ C)"
using assms by auto

text‹Set operations.›

lemma vintersection_vempty: "0 ⊆⇩∘ A" by simp

lemma vintersection_vsingleton: "a ∈⇩∘ set {a}" by simp

lemma vintersection_vdoubleton: "a ∈⇩∘ set {a, b}" and "b ∈⇩∘ set {a, b}"
by simp_all

lemma vintersection_VPow[simp]: "VPow (A ∩⇩∘ B) = VPow A ∩⇩∘ VPow B" by auto

text‹Special properties.›

lemma vintersection_function_mono:
assumes "mono f"
shows "f (A ∩⇩∘ B) ⊆⇩∘ f A ∩⇩∘ f B"
using assms by (fact mono_inf)

subsection‹Binary union›

lemma small_vunion_set: "small {x. x ∈⇩∘ A ∨ x ∈⇩∘ B}"
by (rule down[of _ ‹A ∪⇩∘ B›]) (auto simp: elts_sup_iff)

text‹Rules.›

lemma vunion_def: "A ∪⇩∘ B = set {x. x ∈⇩∘ A ∨ x ∈⇩∘ B}"
unfolding Un_def sup_V_def by simp

lemma vunion_iff[simp]: "x ∈⇩∘ A ∪⇩∘ B ⟷ x ∈⇩∘ A ∨ x ∈⇩∘ B"

lemma vunionI1:
assumes "a ∈⇩∘ A"
shows "a ∈⇩∘ A ∪⇩∘ B"
using assms by simp

lemma vunionI2:
assumes "a ∈⇩∘ B"
shows "a ∈⇩∘ A ∪⇩∘ B"
using assms by simp

lemma vunionCI[intro!]:
assumes "x ∉⇩∘ B ⟹ x ∈⇩∘ A"
shows "x ∈⇩∘ A ∪⇩∘ B"
using assms by clarsimp

lemma vunionE[elim!]:
assumes "x ∈⇩∘ A ∪⇩∘ B" and "x ∈⇩∘ A ⟹ P" and "x ∈⇩∘ B ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma vunion_union: "A ∪⇩∘ B = set (elts A ∪ elts B)" by auto

lemma vunion_assoc: "A ∪⇩∘ (B ∪⇩∘ C) = (A ∪⇩∘ B) ∪⇩∘ C" by auto

lemma vunion_commute: "A ∪⇩∘ B = B ∪⇩∘ A" by auto

text‹Previous set operations.›

lemma vsubset_vunion_left: "(A ∪⇩∘ B) ⊆⇩∘ C ⟷ (A ⊆⇩∘ C ∧ B ⊆⇩∘ C)" by simp

lemma vsubset_vunion_leftD[dest]:
assumes "(A ∪⇩∘ B) ⊆⇩∘ C"
shows "A ⊆⇩∘ C" and "B ⊆⇩∘ C"
using assms by auto

lemma vsubset_vunion_leftI[intro]:
assumes "A ⊆⇩∘ C" and "B ⊆⇩∘ C"
shows "(A ∪⇩∘ B) ⊆⇩∘ C"
using assms by auto

lemma vintersection_vunion_left: "(A ∪⇩∘ B) ∩⇩∘ C = (A ∩⇩∘ C) ∪⇩∘ (B ∩⇩∘ C)"
by auto

lemma vintersection_vunion_right: "A ∩⇩∘ (B ∪⇩∘ C) = (A ∩⇩∘ B) ∪⇩∘ (A ∩⇩∘ C)"
by auto

text‹Set operations.›

lemmas vunion_vempty_left = sup_V_0_left
and vunion_vempty_right = sup_V_0_right

lemma vunion_vsingleton[simp]: "set {a} ∪⇩∘ A = vinsert a A" by auto

lemma vunion_vdoubleton[simp]: "set {a, b} ∪⇩∘ A = vinsert a (vinsert b A)"
by auto

lemma vunion_vinsert_comm_left:
"(vinsert a A) ∪⇩∘ B = A ∪⇩∘ (vinsert a B)"
by auto

lemma vunion_vinsert_comm_right:
"A ∪⇩∘ (vinsert a B) = (vinsert a A) ∪⇩∘ B"
by auto

lemma vinsert_def: "vinsert y B = set {x. x = y} ∪⇩∘ B" by auto

lemma vunion_vinsert_left: "(vinsert a A) ∪⇩∘ B = vinsert a (A ∪⇩∘ B)" by auto

lemma vunion_vinsert_right: "A ∪⇩∘ (vinsert a B) = vinsert a (A ∪⇩∘ B)" by auto

text‹Special properties.›

lemma vunion_fun_mono:
assumes "mono f"
shows "f A ∪⇩∘ f B ⊆⇩∘ f (A ∪⇩∘ B)"
using assms by (fact mono_sup)

subsection‹Set difference›

definition vdiff :: "V ⇒ V ⇒ V" (infixl ‹-⇩∘› 65)
where "A -⇩∘ B = set {x. x ∈⇩∘ A ∧ x ∉⇩∘ B}"
notation vdiff (infixl "-⇩∘" 65)

lemma small_set_vdiff[simp]: "small {x. x ∈⇩∘ A ∧ x ∉⇩∘ B}"
by (rule down[of _ A]) simp

text‹Rules.›

lemma vdiff_iff[simp]: "x ∈⇩∘ A -⇩∘ B ⟷ x ∈⇩∘ A ∧ x ∉⇩∘ B"
unfolding vdiff_def by simp

lemma vdiffI[intro!]:
assumes "x ∈⇩∘ A" and "x ∉⇩∘ B"
shows "x ∈⇩∘ A -⇩∘ B"
using assms by simp

lemma vdiffD1:
assumes "x ∈⇩∘ A -⇩∘ B"
shows "x ∈⇩∘ A"
using assms by simp

lemma vdiffD2:
assumes "x ∈⇩∘ A -⇩∘ B" and "x ∈⇩∘ B"
shows P
using assms by simp

lemma vdiffE[elim!]:
assumes "x ∈⇩∘ A -⇩∘ B" and "⟦ x ∈⇩∘ A; x ∉⇩∘ B ⟧ ⟹ P"
shows P
using assms by simp

text‹Previous set operations.›

lemma vsubset_vdiff:
assumes "A ⊆⇩∘ B -⇩∘ C"
shows "A ⊆⇩∘ B"
using assms by auto

lemma vinsert_vdiff_nin[simp]:
assumes "a ∉⇩∘ B"
shows "vinsert a (A -⇩∘ B) = vinsert a A -⇩∘ B"
using assms by auto

text‹Set operations.›

lemma vdiff_vempty_left[simp]: "0 -⇩∘ A = 0" by auto

lemma vdiff_vempty_right[simp]: "A -⇩∘ 0 = A" by auto

lemma vdiff_vsingleton_vinsert[simp]: "set {a} -⇩∘ vinsert a A = 0" by auto

lemma vdiff_vsingleton_in[simp]:
assumes "a ∈⇩∘ A"
shows "set {a} -⇩∘ A = 0"
using assms by auto

lemma vdiff_vsingleton_nin[simp]:
assumes "a ∉⇩∘ A"
shows "set {a} -⇩∘ A = set {a}"
using assms by auto

lemma vdiff_vinsert_vsingleton[simp]: "vinsert a A -⇩∘ set {a} = A -⇩∘ set {a}"
by auto

lemma vdiff_vsingleton[simp]:
assumes "a ∉⇩∘ A"
shows "A -⇩∘ set {a} = A"
using assms by auto

lemma vdiff_vsubset:
assumes "A ⊆⇩∘ B" and "D ⊆⇩∘ C"
shows "A -⇩∘ C ⊆⇩∘ B -⇩∘ D"
using assms by auto

lemma vdiff_vinsert_left_in[simp]:
assumes "a ∈⇩∘ B"
shows "(vinsert a A) -⇩∘ B = A -⇩∘ B"
using assms by auto

lemma vdiff_vinsert_left_nin:
assumes "a ∉⇩∘ B"
shows "(vinsert a A) -⇩∘ B = vinsert a (A -⇩∘ B)"
using assms by auto

lemma vdiff_vinsert_right_in: "A -⇩∘ (vinsert a B) = A -⇩∘ B -⇩∘ set {a}" by auto

lemma vdiff_vinsert_right_nin[simp]:
assumes "a ∉⇩∘ A"
shows "A -⇩∘ (vinsert a B) = A -⇩∘ B"
using assms by auto

lemma vdiff_vintersection_left: "(A ∩⇩∘ B) -⇩∘ C = (A -⇩∘ C) ∩⇩∘ (B -⇩∘ C)" by auto

lemma vdiff_vunion_left: "(A ∪⇩∘ B) -⇩∘ C = (A -⇩∘ C) ∪⇩∘ (B -⇩∘ C)" by auto

text‹Special properties.›

lemma complement_vsubset: "I -⇩∘ J ⊆⇩∘ I" by auto

lemma vintersection_complement: "(I -⇩∘ J) ∩⇩∘ J = 0" by auto

lemma vunion_complement:
assumes "J ⊆⇩∘ I"
shows "I -⇩∘ J ∪⇩∘ J = I"
using assms by auto

subsection‹Augmenting a set with an element›

lemma vinsert_compr: "vinsert y A = set {x. x = y ∨ x ∈⇩∘ A}"
unfolding vunion_def vinsert_def by simp_all

text‹Rules.›

lemma vinsert_iff[simp]: "x ∈⇩∘ vinsert y A ⟷ x = y ∨ x ∈⇩∘ A" by simp

lemma vinsertI1: "x ∈⇩∘ vinsert x A" by simp

lemma vinsertI2:
assumes "x ∈⇩∘ A"
shows "x ∈⇩∘ vinsert y A"
using assms by simp

lemma vinsertE1[elim!]:
assumes "x ∈⇩∘ vinsert y A" and "x = y ⟹ P" and "x ∈⇩∘ A ⟹ P"
shows P
using assms unfolding vinsert_def by auto

lemma vinsertCI[intro!]:
assumes "x ∉⇩∘ A ⟹ x = y"
shows "x ∈⇩∘ vinsert y A"
using assms by clarsimp

text‹Elementary properties.›

lemma vinsert_insert: "vinsert a A = set (insert a (elts A))" by auto

lemma vinsert_commute: "vinsert a (vinsert b C) = vinsert b (vinsert a C)"
by auto

lemma vinsert_ident:
assumes "x ∉⇩∘ A" and "x ∉⇩∘ B"
shows "vinsert x A = vinsert x B ⟷ A = B"
using assms by force

lemmas vinsert_identD[dest] = vinsert_ident[THEN iffD1, rotated 2]
and vinsert_identI[intro] = vinsert_ident[THEN iffD2]

text‹Set operations.›

lemma vinsert_vempty: "vinsert a 0 = set {a}" by auto

lemma vinsert_vsingleton: "vinsert a (set {b}) = set {a, b}" by auto

lemma vinsert_vdoubleton: "vinsert a (set {b, c}) = set {a, b, c}" by auto

lemma vinsert_vinsert: "vinsert a (vinsert b C) = set {a, b} ∪⇩∘ C" by auto

lemma vinsert_vunion_left: "vinsert a (A ∪⇩∘ B) = vinsert a A ∪⇩∘ B" by auto

lemma vinsert_vunion_right: "vinsert a (A ∪⇩∘ B) = A ∪⇩∘ vinsert a B" by auto

lemma vinsert_vintersection: "vinsert a (A ∩⇩∘ B) = vinsert a A ∩⇩∘ vinsert a B"
by auto

text‹Special properties.›

lemma vinsert_set_insert_empty_anyI:
assumes "P (vinsert a 0)"
shows "P (set (insert a {}))"
using assms by (simp add: vinsert_def)

lemma vinsert_set_insert_anyI:
assumes "small B" and "P (vinsert a (set (insert b B)))"
shows "P (set (insert a (insert b B)))"
using assms by (simp add: ZFC_in_HOL.vinsert_def)

lemma vinsert_set_insert_eq:
assumes "small B"
shows "set (insert a (insert b B)) = vinsert a (set (insert b B))"
using assms by (simp add: ZFC_in_HOL.vinsert_def)

lemma vsubset_vinsert:
"A ⊆⇩∘ vinsert x B ⟷ (if x ∈⇩∘ A then A -⇩∘ set {x} ⊆⇩∘ B else A ⊆⇩∘ B)"
by auto

lemma vinsert_obtain_ne:
assumes "A ≠ 0"
obtains a A' where "A = vinsert a A'" and "a ∉⇩∘ A'"
proof-
from assms mem_not_refl obtain a where "a ∈⇩∘ A"
by (auto intro!: vsubset_antisym)
with ‹a ∈⇩∘ A› have "A = vinsert a (A -⇩∘ set {a})" by auto
then show ?thesis using that by auto
qed

subsection‹Power set›

text‹Rules.›

lemma VPowI:
assumes "A ⊆⇩∘ B"
shows "A ∈⇩∘ VPow B"
using assms by simp

lemma VPowD:
assumes "A ∈⇩∘ VPow B"
shows "A ⊆⇩∘ B"
using assms by (simp add: Pow_def)

lemma VPowE[elim]:
assumes "A ∈⇩∘ VPow B" and "A ⊆⇩∘ B ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma VPow_bottom: "0 ∈⇩∘ VPow B" by simp

lemma VPow_top: "A ∈⇩∘ VPow A" by simp

text‹Set operations.›

lemma VPow_vempty[simp]: "VPow 0 = set {0}" by auto

lemma VPow_vsingleton[simp]: "VPow (set {a}) = set {0, set {a}}"
by (rule vsubset_antisym; rule vsubsetI) auto

lemma VPow_not_vempty: "VPow A ≠ 0" by auto

lemma VPow_mono:
assumes "A ⊆⇩∘ B"
shows "VPow A ⊆⇩∘ VPow B"
using assms by simp

lemma VPow_vunion_subset: "VPow A ∪⇩∘ VPow B ⊆⇩∘ VPow (A ∪⇩∘ B)" by simp

subsection‹Singletons, using insert›

text‹Rules.›

lemma vsingletonI[intro!]: "x ∈⇩∘ set {x}" by auto

lemma vsingletonD[dest!]:
assumes "y ∈⇩∘ set {x}"
shows "y = x"
using assms by auto

lemma vsingleton_iff: "y ∈⇩∘ set {x} ⟷ y = x" by simp

text‹Previous set operations.›

lemma VPow_vdoubleton[simp]:
"VPow (set {a, b}) = set {0, set {a}, set {b}, set {a, b}}"
by (intro vsubset_antisym vsubsetI)
(auto intro!: vsubset_antisym simp: vinsert_set_insert_eq)

lemma vsubset_vinsertI:
assumes "A -⇩∘ set {x} ⊆⇩∘ B"
shows "A ⊆⇩∘ vinsert x B"
using assms by auto

text‹Special properties.›

lemma vsingleton_inject:
assumes "set {x} = set {y}"
shows "x = y"
using assms by simp

lemma vsingleton_insert_inj_eq[iff]:
"set {y} = vinsert x A ⟷ x = y ∧ A ⊆⇩∘ set {y}"
by auto

lemma vsingleton_insert_inj_eq'[iff]:
"vinsert x A = set {y} ⟷ x = y ∧ A ⊆⇩∘ set {y}"
by auto

lemma vsubset_vsingletonD:
assumes "A ⊆⇩∘ set {x}"
shows "A = 0 ∨ A = set {x}"
using assms by auto

lemma vsubset_vsingleton_iff: "a ⊆⇩∘ set {x} ⟷ a = 0 ∨ a = set {x}" by auto

lemma vsubset_vdiff_vinsert: "A ⊆⇩∘ B -⇩∘ vinsert x C ⟷ A ⊆⇩∘ B -⇩∘ C ∧ x ∉⇩∘ A"
by auto

lemma vunion_vsingleton_iff:
"A ∪⇩∘ B = set {x} ⟷
A = 0 ∧ B = set {x} ∨ A = set {x} ∧ B = 0 ∨ A = set {x} ∧ B = set {x}"
by
(
metis
vsubset_vsingletonD inf_sup_ord(4) sup.idem sup_V_0_right sup_commute
)

lemma vsingleton_Un_iff:
"set {x} = A ∪⇩∘ B ⟷
A = 0 ∧ B = set {x} ∨ A = set {x} ∧ B = 0 ∨ A = set {x} ∧ B = set {x}"
by (metis vunion_vsingleton_iff sup_V_0_left sup_V_0_right sup_idem)

lemma VPow_vsingleton_iff[simp]: "VPow X = set {Y} ⟷ X = 0 ∧ Y = 0"
by (auto intro!: vsubset_antisym)

subsection‹Intersection of elements›

lemma small_VInter[simp]:
assumes "A ≠ 0"
shows "small {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}"
by (metis (no_types, lifting) assms down eq0_iff mem_Collect_eq subsetI)

lemma VInter_def: "⋂⇩∘ A = (if A = 0 then 0 else set {a. ∀x ∈⇩∘ A. a ∈⇩∘ x})"
proof(cases ‹A = 0›)
case True show ?thesis unfolding True Inf_V_def by simp
next
case False
from False have "(⋂ (elts ` elts A)) = {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}" by auto
with False show ?thesis unfolding Inf_V_def by auto
qed

text‹Rules.›

lemma VInter_iff[simp]:
assumes [simp]: "A ≠ 0"
shows "a ∈⇩∘ ⋂⇩∘ A ⟷ (∀x∈⇩∘A. a ∈⇩∘ x)"
unfolding VInter_def by auto

lemma VInterI[intro]:
assumes "A ≠ 0" and "⋀x. x ∈⇩∘ A ⟹ a ∈⇩∘ x"
shows "a ∈⇩∘ ⋂⇩∘ A"
using assms by auto

lemma VInter0I[intro]:
assumes "A = 0"
shows "⋂⇩∘ A = 0"
using assms unfolding VInter_def by simp

lemma VInterD[dest]:
assumes "a ∈⇩∘ ⋂⇩∘ A" and "x ∈⇩∘ A"
shows "a ∈⇩∘ x"
using assms by (cases ‹A = 0›) auto

lemma VInterE1[elim]:
assumes "a ∈⇩∘ ⋂⇩∘ A" and "x ∉⇩∘ A ⟹ R" and "a ∈⇩∘ x ⟹ R"
shows R
using assms elts_0 unfolding Inter_eq by blast

lemma VInterE2[elim]:
assumes "a ∈⇩∘ ⋂⇩∘ A"
obtains x where "a ∈⇩∘ x" and "x ∈⇩∘ A"
proof(cases ‹A = 0›)
show "(⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ thesis) ⟹ A = 0 ⟹ thesis"
using assms unfolding Inf_V_def by auto
show "(⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ thesis) ⟹ A ≠ 0 ⟹ thesis"
using assms by (meson assms VInterE1 that trad_foundation)
qed

lemma VInterE3: (*not elim*)
assumes "a ∈⇩∘ ⋂⇩∘ A" and "(⋀y. y ∈⇩∘ A ⟹ a ∈⇩∘ y) ⟹ P"
shows P
using assms by auto

text‹Elementary properties.›

lemma VInter_Inter: "⋂⇩∘ A = set (⋂ (elts ` (elts A)))"

lemma VInter_eq:
assumes [simp]: "A ≠ 0"
shows "⋂⇩∘ A = set {a. ∀x ∈⇩∘ A. a ∈⇩∘ x}"
unfolding VInter_def by auto

text‹Set operations.›

lemma VInter_vempty[simp]: "⋂⇩∘ 0 = 0" using VInter0I by auto

lemma VInf_vempty[simp]: "⨅{} = (0::V)" by (simp add: Inf_V_def)

lemma VInter_vdoubleton: "⋂⇩∘ (set {a, b}) = a ∩⇩∘ b"
proof(intro vsubset_antisym vsubsetI)
show "x ∈⇩∘ ⋂⇩∘ (set {a, b}) ⟹ x ∈⇩∘ a ∩⇩∘ b" for x by (elim VInterE3) auto
show "x ∈⇩∘ a ∩⇩∘ b ⟹ x ∈⇩∘ ⋂⇩∘ (set {a, b})" for x by (intro VInterI) force+
qed

lemma VInter_antimono:
assumes "B ≠ 0" and "B ⊆⇩∘ A"
shows "⋂⇩∘ A ⊆⇩∘ ⋂⇩∘ B"
using assms by blast

lemma VInter_vsubset:
assumes "⋀x. x ∈⇩∘ A ⟹ x ⊆⇩∘ B" and "A ≠ 0"
shows "⋂⇩∘ A ⊆⇩∘ B"
using assms by auto

lemma VInter_vinsert:
assumes "A ≠ 0"
shows "⋂⇩∘ (vinsert a A) = a ∩⇩∘ ⋂⇩∘ A"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vunion:
assumes "A ≠ 0" and "B ≠ 0"
shows "⋂⇩∘(A ∪⇩∘ B) = ⋂⇩∘A ∩⇩∘ ⋂⇩∘B"
using assms by (blast intro!: vsubset_antisym)

lemma VInter_vintersection:
assumes "A ∩⇩∘ B ≠ 0"
shows "⋂⇩∘ A ∪⇩∘ ⋂⇩∘ B ⊆⇩∘ ⋂⇩∘ (A ∩⇩∘ B)"
using assms by auto

lemma VInter_VPow: "⋂⇩∘ (VPow A) ⊆⇩∘ VPow (⋂⇩∘ A)" by auto

text‹Elementary properties.›

lemma VInter_lower:
assumes "x ∈⇩∘ A"
shows "⋂⇩∘ A ⊆⇩∘ x"
using assms by auto

lemma VInter_greatest:
assumes "A ≠ 0" and "⋀x. x ∈⇩∘ A ⟹ B ⊆⇩∘ x"
shows "B ⊆⇩∘ ⋂⇩∘ A"
using assms by auto

subsection‹Union of elements›

lemma Union_eq_VUnion: "⋃(elts ` elts A) = {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}" by auto

lemma small_VUnion[simp]: "small {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}"
by (fold Union_eq_VUnion) simp

lemma VUnion_def: "⋃⇩∘A = set {a. ∃x ∈⇩∘ A. a ∈⇩∘ x}"
unfolding Sup_V_def by auto

text‹Rules.›

lemma VUnion_iff[simp]: "A ∈⇩∘ ⋃⇩∘C ⟷ (∃x∈⇩∘C. A ∈⇩∘ x)" by auto

lemma VUnionI[intro]:
assumes "x ∈⇩∘ A" and "a ∈⇩∘ x"
shows "a ∈⇩∘ ⋃⇩∘A"
using assms by auto

lemma VUnionE[elim!]:
assumes "a ∈⇩∘ ⋃⇩∘A" and "⋀x. a ∈⇩∘ x ⟹ x ∈⇩∘ A ⟹ R"
shows R
using assms by clarsimp

text‹Elementary properties.›

lemma VUnion_Union: "⋃⇩∘A = set (⋃ (elts ` (elts A)))"

text‹Set operations.›

lemma VUnion_vempty[simp]: "⋃⇩∘0 = 0" by simp

lemma VUnion_vsingleton[simp]: "⋃⇩∘(set {a}) = a" by simp

lemma VUnion_vdoubleton[simp]: "⋃⇩∘(set {a, b}) = a ∪⇩∘ b" by auto

lemma VUnion_mono:
assumes "A ⊆⇩∘ B"
shows "⋃⇩∘A ⊆⇩∘ ⋃⇩∘B"
using assms by auto

lemma VUnion_vinsert: "⋃⇩∘(vinsert x A) = x ∪⇩∘ ⋃⇩∘A" by auto

lemma VUnion_vintersection: "⋃⇩∘(A ∩⇩∘ B) ⊆⇩∘ ⋃⇩∘A ∩⇩∘ ⋃⇩∘B" by auto

lemma VUnion_vunion[simp]: "⋃⇩∘(A ∪⇩∘ B) = ⋃⇩∘A ∪⇩∘ ⋃⇩∘B" by auto

lemma VUnion_VPow[simp]: "⋃⇩∘(VPow A) = A" by auto

text‹Special properties.›

lemma VUnion_vempty_conv_left: "0 = ⋃⇩∘A ⟷ (∀x∈⇩∘A. x = 0)" by auto

lemma VUnion_vempty_conv_right: "⋃⇩∘A = 0 ⟷ (∀x∈⇩∘A. x = 0)" by auto

lemma vsubset_VPow_VUnion: "A ⊆⇩∘ VPow (⋃⇩∘A)" by auto

lemma VUnion_vsubsetI:
assumes "⋀x. x ∈⇩∘ A ⟹ ∃y. y ∈⇩∘ B ∧ x ⊆⇩∘ y"
shows "⋃⇩∘A ⊆⇩∘ ⋃⇩∘B"
using assms by auto

lemma VUnion_upper:
assumes "x ∈⇩∘ A"
shows "x ⊆⇩∘ ⋃⇩∘A"
using assms by auto

lemma VUnion_least:
assumes "⋀x. x ∈⇩∘ A ⟹ x ⊆⇩∘ B"
shows "⋃⇩∘A ⊆⇩∘ B"
using assms by (fact Sup_least)

subsection‹Pairs›

subsubsection‹Further results›

lemma small_elts_of_set[simp, intro]:
assumes "small x"
shows "elts (set x) = x"

lemma small_vpair[intro, simp]:
assumes "small {a. P a}"
shows "small {⟨a, b⟩ | a. P a}"
by (subgoal_tac ‹{⟨a, b⟩ | a. P a} = (λa. ⟨a, b⟩) ` {a. P a}›)
(auto simp: assms)

subsubsection‹‹vpairs››

definition vpairs :: "V ⇒ V" where
"vpairs r = set {x. x ∈⇩∘ r ∧ (∃a b. x = ⟨a, b⟩)}"

lemma small_vpairs[simp]: "small {⟨a, b⟩ | a b. ⟨a, b⟩ ∈⇩∘ r}"
by (rule down[of _ r]) clarsimp

text‹Rules.›

lemma vpairsI[intro]:
assumes "x ∈⇩∘ r" and "x = ⟨a, b⟩"
shows "x ∈⇩∘ vpairs r"
using assms unfolding vpairs_def by auto

lemma vpairsD[dest]:
assumes "x ∈⇩∘ vpairs r"
shows "x ∈⇩∘ r" and "∃a b. x = ⟨a, b⟩"
using assms unfolding vpairs_def by auto

lemma vpairsE[elim]:
assumes "x ∈⇩∘ vpairs r"
obtains a b where "x = ⟨a, b⟩" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vpairs_def by auto

lemma vpairs_iff: "x ∈⇩∘ vpairs r ⟷ x ∈⇩∘ r ∧ (∃a b. x = ⟨a, b⟩)" by auto

text‹Elementary properties.›

lemma vpairs_iff_elts: "⟨a, b⟩ ∈⇩∘ vpairs r ⟷ ⟨a, b⟩ ∈⇩∘ r" by auto

lemma vpairs_iff_pairs: "⟨a, b⟩ ∈⇩∘ vpairs r ⟷ (a, b) ∈ pairs r"

text‹Set operations.›

lemma vpairs_vempty[simp]: "vpairs 0 = 0" by auto

lemma vpairs_vsingleton[simp]: "vpairs (set {⟨a, b⟩}) = set {⟨a, b⟩}" by auto

lemma vpairs_vinsert: "vpairs (vinsert ⟨a, b⟩ A) = set {⟨a, b⟩} ∪⇩∘ vpairs A"
by auto

lemma vpairs_mono:
assumes "r ⊆⇩∘ s"
shows "vpairs r ⊆⇩∘ vpairs s"
using assms by blast

lemma vpairs_vunion: "vpairs (A ∪⇩∘ B) = vpairs A ∪⇩∘ vpairs B" by auto

lemma vpairs_vintersection: "vpairs (A ∩⇩∘ B) = vpairs A ∩⇩∘ vpairs B" by auto

lemma vpairs_vdiff: "vpairs (A -⇩∘ B) = vpairs A -⇩∘ vpairs B" by auto

text‹Special properties.›

lemma vpairs_ex_vfst:
assumes "x ∈⇩∘ vpairs r"
shows "∃b. ⟨vfst x, b⟩ ∈⇩∘ r"
using assms by force

lemma vpairs_ex_vsnd:
assumes "y ∈⇩∘ vpairs r"
shows "∃a. ⟨a, vsnd y⟩ ∈⇩∘ r"
using assms by force

subsection‹Cartesian products›

text‹
The following lemma is based on Theorem 6.2 from
\<^cite>‹"takeuti_introduction_1971"›.
›

lemma vtimes_vsubset_VPowVPow: "A ×⇩∘ B ⊆⇩∘ VPow (VPow (A ∪⇩∘ B))"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ A ×⇩∘ B"
then obtain a b where x_def: "x = ⟨a, b⟩" and "a ∈⇩∘ A" and "b ∈⇩∘ B" by clarsimp
then show "x ∈⇩∘ VPow (VPow (A ∪⇩∘ B))"
unfolding x_def vpair_def by auto
qed

subsection‹Pairwise›

definition vpairwise :: "(V ⇒ V ⇒ bool) ⇒ V ⇒ bool"
where "vpairwise R S ⟷ (∀x∈⇩∘S. ∀y∈⇩∘S. x ≠ y ⟶ R x y)"

text‹Rules.›

lemma vpairwiseI[intro?]:
assumes "⋀x y. x ∈⇩∘ S ⟹ y ∈⇩∘ S ⟹ x ≠ y ⟹ R x y"
shows "vpairwise R S"
using assms by (simp add: vpairwise_def)

lemma vpairwiseD[dest]:
assumes "vpairwise R S" and "x ∈⇩∘ S" and "y ∈⇩∘ S" and "x ≠ y"
shows "R x y" and "R y x"
using assms unfolding vpairwise_def by auto

text‹Elementary properties.›

lemma vpairwise_trivial[simp]: "vpairwise (λi j. j ≠ i) I"
by (auto simp: vpairwise_def)

text‹Set operations.›

lemma vpairwise_vempty[simp]: "vpairwise P 0" by (force intro: vpairwiseI)

lemma vpairwise_vsingleton[simp]: "vpairwise P (set {A})"

lemma vpairwise_vinsert:
"vpairwise r (vinsert x s) ⟷
(∀y. y ∈⇩∘ s ∧ y ≠ x ⟶ r x y ∧ r y x) ∧ vpairwise r s"
by (intro iffI conjI allI impI; (elim conjE | tactic‹all_tac›))
(auto simp: vpairwise_def)

lemma vpairwise_vsubset:
assumes "vpairwise P S" and "T ⊆⇩∘ S"
shows "vpairwise P T"
using assms by (metis less_eq_V_def subset_eq vpairwiseD(2) vpairwiseI)

lemma vpairwise_mono:
assumes "vpairwise P A" and "⋀x y. P x y ⟹ Q x y" and "B ⊆⇩∘ A"
shows "vpairwise Q B"
using assms by (simp add: less_eq_V_def subset_eq vpairwiseD(2) vpairwiseI)

subsection‹Disjoint sets›

abbreviation vdisjnt :: "V ⇒ V ⇒ bool"
where "vdisjnt A B ≡ A ∩⇩∘ B = 0"

text‹Elementary properties.›

lemma vdisjnt_sym:
assumes "vdisjnt A B"
shows "vdisjnt B A"
using assms by blast

lemma vdisjnt_iff: "vdisjnt A B ⟷ (∀x. ~ (x ∈⇩∘ A ∧ x ∈⇩∘ B))" by auto

text‹Set operations.›

lemma vdisjnt_vempty1[simp]: "vdisjnt 0 A"
and vdisjnt_vempty2[simp]: "vdisjnt A 0"
by auto

lemma vdisjnt_singleton0[simp]: "vdisjnt (set {a}) (set {b}) ⟷ a ≠ b"
and vdisjnt_singleton1[simp]: "vdisjnt (set {a}) A ⟷ a ∉⇩∘ A"
and vdisjnt_singleton2[simp]: "vdisjnt A (set {a}) ⟷ a ∉⇩∘ A"
by force+

lemma vdisjnt_vinsert_left: "vdisjnt (vinsert a X) Y ⟷ a ∉⇩∘ Y ∧ vdisjnt X Y"
by (metis vdisjnt_iff vdisjnt_sym vinsertE1 vinsertI2 vinsert_iff)

lemma vdisjnt_vinsert_right: "vdisjnt Y (vinsert a X) ⟷ a ∉⇩∘ Y ∧ vdisjnt Y X"
using vdisjnt_sym vdisjnt_vinsert_left by meson

lemma vdisjnt_vsubset_left:
assumes "vdisjnt X Y" and "Z ⊆⇩∘ X"
shows "vdisjnt Z Y"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_vsubset_right:
assumes "vdisjnt X Y" and "Z ⊆⇩∘ Y"
shows "vdisjnt X Z"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_vunion_left: "vdisjnt (A ∪⇩∘ B) C ⟷ vdisjnt A C ∧ vdisjnt B C"
by auto

lemma vdisjnt_vunion_right: "vdisjnt C (A ∪⇩∘ B) ⟷ vdisjnt C A ∧ vdisjnt C B"
by auto

text‹Special properties.›

lemma vdisjnt_vemptyI[intro]:
assumes "⋀x. x ∈⇩∘ A ⟹ x ∈⇩∘ B ⟹ False"
shows "vdisjnt A B"
using assms by (auto intro!: vsubset_antisym)

lemma vdisjnt_self_iff_vempty[simp]: "vdisjnt S S ⟷ S = 0" by auto

lemma vdisjntI:
assumes "⋀x y. x ∈⇩∘ A ⟹ y ∈⇩∘ B ⟹ x ≠ y"
shows "vdisjnt A B"
using assms by auto

lemma vdisjnt_nin_right:
assumes "vdisjnt A B" and "a ∈⇩∘ A"
shows "a ∉⇩∘ B"
using assms by auto

lemma vdisjnt_nin_left:
assumes "vdisjnt B A" and "a ∈⇩∘ A"
shows "a ∉⇩∘ B"
using assms by auto

text‹\newpage›

end```