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)

syntax_consts
  "_VBall" ⇌ Ball and
  "_VBex" ⇌ Bex and
  "_VBex1" ⇌ Ex1

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)
syntax_consts "_vlam" ⇌ VLambda
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" 
  using assms trad_foundation by auto

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)"
  by (simp add: assms)

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.›

lemma vsubset_contraD:
  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" 
  by (simp add: elts_sup_iff)

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)))"
  by (simp add: Inf_V_def ext)

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)))"
  by (simp add: Inf_V_def ext)


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"
  by (simp add: assms)

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"
  by (simp add: vpairs_iff_elts pairs_iff_elts)


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})"
  by (simp add: vpairwise_def)

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