Theory CZH_Sets_IF

(* Copyright 2021 (C) Mihails Milehins *)

section‹Operations on indexed families of sets›
theory CZH_Sets_IF
  imports CZH_Sets_BRelations
begin



subsection‹Background›


text‹
This section presents results about the fundamental operations on the indexed
families of sets, such as unions and intersections of the indexed families
of sets, disjoint unions and infinite Cartesian products.

Certain elements of the content of this section were inspired by
elements of the content of cite‹"paulson_hereditarily_2013"›. 
However, as previously, many other results were ported (with amendments) from 
the main library of Isabelle/HOL.
›

abbreviation (input) imVLambda :: "V ⇒ (V ⇒ V) ⇒ V"
  where "imVLambda A f ≡ (λa∈∘A. f a) `∘ A"



subsection‹Intersection of an indexed family of sets›

syntax "_VIFINTER" :: "pttrn ⇒ V ⇒ V ⇒ V"  (‹(3⋂∘_∈∘_./ _)› [0, 0, 10] 10)

translations "⋂∘x∈∘A. f" ⇌ "CONST VInter (CONST imVLambda A (λx. f))"


text‹Rules.›

lemma vifintersectionI[intro]:
  assumes "I ≠ 0" and "⋀i. i ∈∘ I ⟹ a ∈∘ f i"  
  shows "a ∈∘ (⋂∘i∈∘I. f i)"
  using assms by (auto intro!: vsubset_antisym)

lemma vifintersectionD[dest]:
  assumes "a ∈∘ (⋂∘i∈∘I. f i)" and "i ∈∘ I"
  shows "a ∈∘ f i"
  using assms by blast

lemma vifintersectionE1[elim]:
  assumes "a ∈∘ (⋂∘i∈∘I. f i)" and "a ∈∘ f i ⟹ P" and "i ∉∘ I ⟹ P" 
  shows P
  using assms by blast

lemma vifintersectionE3[elim]:
  assumes "a ∈∘ (⋂∘i∈∘I. f i)"
  obtains "⋀i. i∈∘I ⟹ a ∈∘ f i"
  using assms by blast

lemma vifintersectionE2[elim]:
  assumes "a ∈∘ (⋂∘i∈∘I. f i)"
  obtains i where "i ∈∘ I" and "a ∈∘ f i"
  using assms by (elim vifintersectionE3) (meson assms VInterE2 app_vimageE)


text‹Set operations.›

lemma vifintersection_vempty_is[simp]: "(⋂∘i∈∘0. f i) = 0" by auto

lemma vifintersection_vsingleton_is[simp]: "(⋂∘i∈∘set{i}. f i) = f i"
  using elts_0 by blast

lemma vifintersection_vdoubleton_is[simp]: "(⋂∘i∈∘set {i, j}. f i) = f i ∩∘ f j"  
  by 
    (
      intro vsubset_antisym vsubsetI; 
      (elim vifintersectionE3 | intro vifintersectionI)
    )
    auto

lemma vifintersection_antimono1: 
  assumes "I ≠ 0" and "I ⊆∘ J"
  shows "(⋂∘j∈∘J. f j) ⊆∘ (⋂∘i∈∘I. f i)"
  using assms by blast

lemma vifintersection_antimono2: 
  assumes "I ≠ 0" and " I ⊆∘ J" and "⋀i. i ∈∘ I ⟹ f i ⊆∘ g i"
  shows "(⋂∘j∈∘J. f j) ⊆∘ (⋂∘i∈∘I. g i)"
  using assms by blast

lemma vifintersection_vintersection: 
  assumes "I ≠ 0" and "J ≠ 0"
  shows "(⋂∘i∈∘I. f i) ∩∘ (⋂∘i∈∘J. f i) = (⋂∘i∈∘I ∪∘ J. f i)"
  using assms by (auto intro!: vsubset_antisym)

lemma vifintersection_vintersection_family: 
  assumes "I ≠ 0" 
  shows "(⋂∘i∈∘I. A i) ∩∘ (⋂∘i∈∘I. B i) = (⋂∘i∈∘I. A i ∩∘ B i)"
  using assms
  by (intro vsubset_antisym vsubsetI, intro vifintersectionI | tactic‹all_tac›) 
    blast+

lemma vifintersection_vunion:
  assumes "I ≠ 0" and "J ≠ 0"
  shows "(⋂∘i∈∘I. f i) ∪∘ (⋂∘j∈∘J. g j) = (⋂∘i∈∘I. ⋂∘j∈∘J. f i ∪∘ g j)"
  using assms by (blast intro!: vsubset_antisym)

lemma vifintersection_vinsert_is[intro, simp]:
  assumes "I ≠ 0" 
  shows "(⋂∘i ∈∘ vinsert j I. f i) = f j ∩∘ (⋂∘i∈∘I. f i)"
  apply(insert assms, intro vsubset_antisym vsubsetI)
  subgoal for b by (subgoal_tac ‹b ∈∘ f j› ‹b ∈∘ (⋂∘i∈∘I. f i)›) blast+
  subgoal for b 
    by (subgoal_tac ‹b ∈∘ f j› ‹b ∈∘ (⋂∘i∈∘I. f i)›) 
      (blast intro!: vsubset_antisym)+
  done

lemma vifintersection_VPow: 
  assumes "I ≠ 0"
  shows "VPow (⋂∘i∈∘I. f i) = (⋂∘i∈∘I. VPow (f i))"
  using assms by (auto intro!: vsubset_antisym)


text‹Elementary properties.›

lemma vifintersection_constant[intro, simp]:
  assumes "I ≠ 0"
  shows "(⋂∘y∈∘I. c) = c"
  using assms by auto

lemma vifintersection_vsubset_iff: 
  assumes "I ≠ 0"
  shows "A ⊆∘ (⋂∘i∈∘I. f i) ⟷ (∀i∈∘I. A ⊆∘ f i)"
  using assms by blast

lemma vifintersection_vsubset_lower: 
  assumes "i ∈∘ I"
  shows "(⋂∘i∈∘I. f i) ⊆∘ f i"
  using assms by blast

lemma vifintersection_vsubset_greatest: 
  assumes "I ≠ 0" and "⋀i. i ∈∘ I ⟹ A ⊆∘ f i" 
  shows "A ⊆∘ (⋂∘i∈∘I. f i)"
  using assms by (intro vsubsetI vifintersectionI) auto 

lemma vifintersection_vintersection_value: 
  assumes "i ∈∘ I"
  shows "f i ∩∘ (⋂∘i∈∘I. f i) = (⋂∘i∈∘I. f i)"
  using assms by blast

lemma vifintersection_vintersection_single: 
  assumes "I ≠ 0"
  shows "B ∪∘ (⋂∘i∈∘I. A i) = (⋂∘i∈∘I. B ∪∘ A i)"
  by (insert assms, intro vsubset_antisym vsubsetI vifintersectionI) 
    blast+


text‹Connections.›

lemma vifintersection_vrange_VLambda: "(⋂∘i∈∘I. f i) = ⋂∘ (ℛ∘ (λa∈∘I. f a))"
  by (simp add: vimage_VLambda_vrange_rep)



subsection‹Union of an indexed family of sets›

syntax "_VIFUNION" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3⋃∘_∈∘_./ _)› [0, 0, 10] 10)

translations "⋃∘x∈∘A. f" ⇌ "CONST VUnion (CONST imVLambda A (λx. f))"


text‹Rules.›

lemma vifunion_iff: "b ∈∘ (⋃∘i∈∘I. f i) ⟷ (∃i∈∘I. b ∈∘ f i)" by force

lemma vifunionI[intro]: 
  assumes "i ∈∘ I" and "a ∈∘ f i" 
  shows "a ∈∘ (⋃∘i∈∘I. f i)" 
  using assms by force

lemma vifunionD[dest]: 
  assumes "a ∈∘ (⋃∘i∈∘I. f i)" 
  shows "∃i∈∘I. a ∈∘ f i" 
  using assms by auto

lemma vifunionE[elim!]: 
  assumes "a ∈∘ (⋃∘i∈∘I. f i)" and "⋀i. ⟦ i ∈∘ I; a ∈∘ f i ⟧ ⟹ R" 
  shows R
  using assms by auto


text‹Set operations.›

lemma vifunion_vempty_family[simp]: "(⋃∘i∈∘I. 0) = 0" by auto

lemma vifunion_vsingleton_is[simp]: "(⋃∘i∈∘set {i}. f i) = f i" by force

lemma vifunion_vsingleton_family[simp]: "(⋃∘i∈∘I. set {i}) = I" by force

lemma vifunion_vdoubleton: "(⋃∘i∈∘set {i, j}. f i) = f i ∪∘ f j" 
  using VLambda_vinsert vimage_vunion_left
  by (force simp: VLambda_vsingleton simp: vinsert_set_insert_eq)

lemma vifunion_mono:
  assumes "I ⊆∘ J" and "⋀i. i ∈∘ I ⟹ f i ⊆∘ g i" 
  shows "(⋃∘i∈∘I. f i) ⊆∘ (⋃∘j∈∘J. g j)"
  using assms by force

lemma vifunion_vunion_is: "(⋃∘i∈∘I. f i) ∪∘ (⋃∘j∈∘J. f j) = (⋃∘i∈∘I ∪∘ J. f i)"
  by force

lemma vifunion_vunion_family:
  "(⋃∘i∈∘I. f i) ∪∘ (⋃∘i∈∘I. g i) = (⋃∘i∈∘I. f i ∪∘ g i)"  
  by (intro vsubset_antisym vsubsetI; elim vunionE vifunionE) force+

lemma vifunion_vintersection: 
  "(⋃∘i∈∘I. f i) ∩∘ (⋃∘j∈∘J. g j) = (⋃∘i∈∘I. ⋃∘j∈∘J. f i ∩∘ g j)"
  by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vinsert_is: 
  "(⋃∘i∈∘vinsert j I. f i) = f j ∪∘ (⋃∘i∈∘I. f i)"
  by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_VPow: "(⋃∘i∈∘I. VPow (f i)) ⊆∘ VPow (⋃∘i∈∘I. f i)" by force


text‹Elementary properties.›

lemma vifunion_vempty_conv:
  "0 = (⋃∘i∈∘I. f i) ⟷ (∀i∈∘I. f i = 0)"
  "(⋃∘i∈∘I. f i) = 0 ⟷ (∀i∈∘I. f i = 0)"
  by (auto simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_constant[simp]: "(⋃∘i∈∘I. c) = (if I = 0 then 0 else c)" 
proof(intro vsubset_antisym)
  show "(if I = 0 then 0 else c) ⊆∘ (⋃∘i∈∘I. c)"
    by (cases ‹vdisjnt I I›) (auto simp: VLambda_vconst_on)
qed auto

lemma vifunion_upper:
  assumes "i ∈∘ I"
  shows "f i ⊆∘ (⋃∘i∈∘I. f i)"
  using assms by force

lemma vifunion_least: 
  assumes "⋀i. i ∈∘ I ⟹ f i ⊆∘ C"
  shows "(⋃∘i∈∘I. f i) ⊆∘ C"
  using assms by auto

lemma vifunion_absorb: 
  assumes "j ∈∘ I"
  shows "f j ∪∘ (⋃∘i∈∘I. f i) = (⋃∘i∈∘I. f i)" 
  using assms by force

lemma vifunion_vifunion_flatten: 
  "(⋃∘j∈∘(⋃∘i∈∘I. f i). g j) = (⋃∘i∈∘I. ⋃∘j∈∘f i. g j)"
  by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vsubset_iff: "((⋃∘i∈∘I. f i) ⊆∘ B) = (∀i∈∘I. f i ⊆∘ B)" by force

lemma vifunion_vsingleton_eq_vrange: "(⋃∘i∈∘I. set {f i}) = ℛ∘ (λa∈∘I. f a)"
  by force

lemma vball_vifunion[simp]: "(∀z∈∘(⋃∘i∈∘I. f i). P z) ⟷ (∀x∈∘I. ∀z∈∘f x. P z)"
  by force

lemma vbex_vifunion[simp]: "(∃z∈∘(⋃∘i∈∘I. f i). P z) ⟷ (∃x∈∘I. ∃z∈∘f x. P z)"
  by force

lemma vifunion_vintersection_index_right[simp]: "(⋃∘C∈∘B. A ∩∘ C) = A ∩∘ ⋃∘B" 
  by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_vintersection_index_left[simp]: "(⋃∘C∈∘B. C ∩∘ A) = ⋃∘B ∩∘ A" 
  by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_vunion_index[intro, simp]:
  assumes "B ≠ 0"
  shows "(⋂∘C∈∘B. A ∪∘ C) = A ∪∘ ⋂∘B"
  using assms
  by 
    (
      (intro vsubset_antisym vsubsetI); 
      (intro vifintersectionI | tactic‹all_tac›)
    ) 
    blast+

lemma vifunion_vintersection_single: "B ∩∘ (⋃∘i∈∘I. f i) = (⋃∘i∈∘I. B ∩∘ f i)" 
  by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vifunion_flip: 
  "(⋃∘b∈∘B. ⋃∘a∈∘A. f b a) = (⋃∘a∈∘A. ⋃∘b∈∘B. f b a)"
proof-
  have "x ∈∘ (⋃∘a∈∘A. ⋃∘b∈∘B. f b a)" if "x ∈∘ (⋃∘b∈∘B. ⋃∘a∈∘A. f b a)" 
    for x f A B 
  proof-
    from that obtain b where b: "b ∈∘ B" and x_b: "x ∈∘ (⋃∘a∈∘A. f b a)" 
      by fastforce
    then obtain a where a: "a ∈∘ A" and x_fba: "x ∈∘ f b a" by fastforce
    show "x ∈∘ (⋃∘a∈∘A. ⋃∘b∈∘B. f b a)"
      unfolding vifunion_iff by (auto intro: a b x_fba)
  qed
  then show ?thesis by (intro vsubset_antisym vsubsetI) auto
qed


text‹Connections.›

lemma vifunion_disjoint: "(⋃∘C ∩∘ A = 0) ⟷ (∀B∈∘C. vdisjnt B A)" 
  by (intro iffI)
    (auto intro!: vsubset_antisym simp: Sup_upper vdisjnt_vsubset_left)

lemma vdisjnt_vifunion_iff: 
  "vdisjnt A (⋃∘i∈∘I. f i) ⟷ (∀i∈∘I. vdisjnt A (f i))"
  by (force intro!: vsubset_antisym simp: vdisjnt_iff)+

lemma vifunion_VLambda: "(⋃∘i∈∘A. set {⟨i, f i⟩}) = (λa∈∘A. f a)" 
  using vifunionI by (intro vsubset_antisym vsubsetI) auto

lemma vifunion_vrange_VLambda: "(⋃∘i∈∘I. f i) = ⋃∘(ℛ∘ (λa∈∘I. f a))"
  using vimage_VLambda_vrange_rep by auto

lemma (in vsv) vsv_vrange_vsubset_vifunion_app:
  assumes "𝒟∘ r = I" and "⋀i. i ∈∘ I ⟹ r⦇i⦈ ∈∘ A i" 
  shows "ℛ∘ r ⊆∘ (⋃∘i∈∘I. A i)"
proof(intro vsubsetI)
  fix x assume "x ∈∘ ℛ∘ r"
  with assms(1) obtain i where x_def: "x = r⦇i⦈" and i: "i ∈∘ I"
    by (metis vrange_atE)
  from i assms(2)[rule_format, OF i] show "x ∈∘ (⋃∘i∈∘I. A i)"
    unfolding x_def by (intro vifunionI) auto
qed

lemma v11_vlrestriction_vifintersection: 
  assumes "I ≠ 0" and "⋀i. i ∈∘ I ⟹ v11 (f ↾l∘ (A i))" 
  shows "v11 (f ↾l∘ (⋂∘i∈∘I. A i))"
proof(intro v11I)
  show "vsv (f ↾l∘ ⋂∘ ((λa∈∘I. A a) `∘ I))"
    (*slow*)
    apply(subgoal_tac ‹⋀i. i ∈∘ I ⟹ vsv (f ↾l∘ (A i))›)
    subgoal by (insert assms(1), intro vsvI) (blast intro!: vsubset_antisym)+
    subgoal using assms by blast
    done
  show "vsv ((f ↾l∘ ⋂∘ ((λa∈∘I. A a) `∘ I))¯∘)"
  proof(intro vsvI) 
    fix a b c
    assume ab: "⟨a, b⟩ ∈∘ (f ↾l∘ ⋂∘ ((λa∈∘I. A a) `∘ I))¯∘"
      and ac: "⟨a, c⟩ ∈∘ (f ↾l∘ ⋂∘ ((λa∈∘I. A a) `∘ I))¯∘"
    from assms(2) have hyp: "⋀i. i ∈∘ I ⟹ vsv ((f ↾l∘ (A i))¯∘)" by blast
    from assms(1) obtain i where "i ∈∘ I" and "⋂∘ ((λa∈∘I. A a) `∘ I) ⊆∘ A i"
      by (auto intro!: vsubset_antisym)
    with ab ac hyp ‹i ∈∘ I› show "b = c" by auto
  qed auto
qed



subsection‹Additional simplification rules for indexed families of sets.›


text‹Union.›

lemma vifunion_simps[simp]:
  "⋀a B I. (⋃∘i∈∘I. vinsert a (B i)) = 
    (if I=0 then 0 else vinsert a (⋃∘i∈∘I. B i))"
  "⋀A B I. (⋃∘i∈∘I. A i ∪∘ B) = ((if I=0 then 0 else (⋃∘i∈∘I. A i) ∪∘ B))"
  "⋀A B I. (⋃∘i∈∘I. A ∪∘ B i) = ((if I=0 then 0 else A ∪∘ (⋃∘i∈∘I. B i)))"
  "⋀A B I. (⋃∘i∈∘I. A i ∩∘ B) = ((⋃∘i∈∘I. A i) ∩∘ B)"
  "⋀A B I. (⋃∘i∈∘I. A ∩∘ B i) = (A ∩∘ (⋃∘i∈∘I. B i))"
  "⋀A B I. (⋃∘i∈∘I. A i -∘ B) = ((⋃∘i∈∘I. A i) -∘ B)"
  "⋀A B. (⋃∘i∈∘⋃∘A. B i) = (⋃∘y∈∘A. ⋃∘i∈∘y. B i)"
  by 
    (
      force 
        simp: vrange_VLambda vimage_VLambda_vrange_rep
        intro!: vsubset_antisym
    )+

lemma vifunion_simps_ext:
  "⋀a B I. vinsert a (⋃∘i∈∘I. B i) = 
    (if I=0 then set {a} else (⋃∘i∈∘I. vinsert a (B i)))"
  "⋀A B I. (⋃∘i∈∘I. A i) ∪∘ B = (if I=0 then B else (⋃∘i∈∘I. A i ∪∘ B))"
  "⋀A B I. A ∪∘ (⋃∘i∈∘I. B i) = (if I=0 then A else (⋃∘i∈∘I. A ∪∘ B i))"
  "⋀A B I. ((⋃∘i∈∘I. A i) ∩∘ B) = (⋃∘i∈∘I. A i ∩∘ B)"
  "⋀A B I. ((⋃∘i∈∘I. A i) -∘ B) = (⋃∘i∈∘I. A i -∘ B)"
  "⋀A B. (⋃∘y∈∘A. ⋃∘i∈∘y. B i) = (⋃∘i∈∘⋃∘A. B i)"
  by (auto simp: vrange_VLambda)

lemma vifunion_vball_vbex_simps[simp]:
  "⋀A P. (∀a∈∘⋃∘A. P a) ⟷ (∀y∈∘A. ∀a∈∘y. P a)"
  "⋀A P. (∃a∈∘⋃∘A. P a) ⟷ (∃y∈∘A. ∃a∈∘y. P a)"
  using vball_vifunion vbex_vifunion by auto


text‹Intersection.›

lemma vifintersection_simps[simp]: 
  "⋀I A B. (⋂∘i∈∘I. A i ∩∘ B) = (if I = 0 then 0 else (⋂∘i∈∘I. A i) ∩∘ B)"
  "⋀I A B. (⋂∘i∈∘I. A ∩∘ B i) = (if I = 0 then 0 else A ∩∘ (⋂∘i∈∘I. B i))"
  "⋀I A B. (⋂∘i∈∘I. A i -∘ B) = (if I = 0 then 0 else (⋂∘i∈∘I. A i) -∘ B)"
  "⋀I A B. (⋂∘i∈∘I. A -∘ B i) = (if I = 0 then 0 else A -∘ (⋃∘i∈∘I. B i))"
  "⋀I a B. 
    (⋂∘i∈∘I. vinsert a (B i)) = (if I = 0 then 0 else vinsert a (⋂∘i∈∘I. B i))"
  "⋀I A B. (⋂∘i∈∘I. A i ∪∘ B) = (if I = 0 then 0 else ((⋂∘i∈∘I. A i) ∪∘ B))"
  "⋀I A B. (⋂∘i∈∘I. A ∪∘ B i) = (if I = 0 then 0 else (A ∪∘ (⋂∘i∈∘I. B i)))"
  by force+

lemma vifintersection_simps_ext:
  "⋀A B I. (⋂∘i∈∘I. A i) ∩∘ B = (if I = 0 then 0 else (⋂∘i∈∘I. A i ∩∘ B))"
  "⋀A B I. A ∩∘ (⋂∘i∈∘I. B i) = (if I = 0 then 0 else (⋂∘i∈∘I. A ∩∘ B i))"
  "⋀A B I. (⋂∘i∈∘I. A i) -∘ B = (if I = 0 then 0 else (⋂∘i∈∘I. A i -∘ B))"
  "⋀A B I. A -∘ (⋃∘i∈∘I. B i) = (if I = 0 then A else (⋂∘i∈∘I. A -∘ B i))"
  "⋀a B I. vinsert a (⋂∘i∈∘I. B i) = 
    (if I = 0 then set {a} else (⋂∘i∈∘I. vinsert a (B i)))"
  "⋀A B I. ((⋂∘i∈∘I. A i) ∪∘ B) = (if I = 0 then B else (⋂∘i∈∘I. A i ∪∘ B))"
  "⋀A B I. A ∪∘ (⋂∘i∈∘I. B i) = (if I = 0 then A else (⋂∘i∈∘I. A ∪∘ B i))"
  using vifintersection_simps by auto



subsection‹Knowledge transfer: union and intersection of indexed families›

lemma SUP_vifunion: "(SUP ξ∈elts α. A ξ) = (⋃∘ξ∈∘α. A ξ)"
  by (simp add: vimage_VLambda_vrange_rep vrange_VLambda)

lemma INF_vifintersection: "(INF ξ∈elts α. A ξ) = (⋂∘ξ∈∘α. A ξ)"
  by (simp add: vimage_VLambda_vrange_rep vrange_VLambda)

lemmas Ord_induct3'[consumes 1, case_names 0 succ Limit, induct type: V] =
  Ord_induct3[unfolded SUP_vifunion]

lemma Limit_vifunion_def[simp]:
  assumes "Limit α"
  shows "(⋃∘ξ∈∘α. ξ) = α"
  using assms unfolding SUP_vifunion[symmetric] by simp

lemmas_with[unfolded SUP_vifunion INF_vifintersection]: 
  TC = ZFC_Cardinals.TC
  and rank_Sup = ZFC_Cardinals.rank_Sup
  and TC_def = ZFC_Cardinals.TC_def
  and Ord_equality = ZFC_in_HOL.Ord_equality
  and Aleph_Limit = ZFC_Cardinals.Aleph_Limit
  and rank = ZFC_Cardinals.rank
  and Vset = ZFC_in_HOL.Vset
  and mult = Kirby.mult
  and Aleph_def = ZFC_Cardinals.Aleph_def
  and times_V_def = Kirby.times_V_def
  and mult_Limit = Kirby.mult_Limit
  and Vfrom = ZFC_in_HOL.Vfrom
  and Vfrom_def = ZFC_in_HOL.Vfrom_def
  and rank_def = ZFC_Cardinals.rank_def
  and add_Limit = Kirby.add_Limit
  and Limit_Vfrom_eq = ZFC_in_HOL.Limit_Vfrom_eq
  and VSigma_def = ZFC_Cardinals.VSigma_def
  and add_Sup_distrib_id = Kirby.add_Sup_distrib_id
  and Limit_add_Sup_distrib = Kirby.Limit_add_Sup_distrib
  and TC_mult = Kirby.TC_mult
  and add_Sup_distrib = Kirby.add_Sup_distrib



subsection‹Disjoint union›


text‹
See the main library of ‹ZFC in HOL› for further information 
and elementary properties.
›

syntax "_VSIGMA" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3∐∘_∈∘_./ _)› [0, 0, 10] 10)

translations "∐∘i∈∘I. A" ⇌ "CONST VSigma I (λi. A)"


text‹Further rules.›

lemma vdunion_def: "(∐∘i∈∘I. A i) = (⋃∘i∈∘I. ⋃∘x∈∘A i. set {⟨i, x⟩})" 
  by (auto simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vdunionI:
  assumes "ix = ⟨i, x⟩" and "i ∈∘ I" and "x ∈∘ A i"
  shows "ix ∈∘ (∐∘i∈∘I. A i)"
  using assms(2,3) unfolding assms(1) vdunion_def by (intro vifunionI) auto

lemmas vdunionD = VSigmaD1 VSigmaD2
  and vdunionE = VSigmaE


text‹Set operations.›

lemma vdunion_vsingleton: "(∐∘i∈∘set{c}. A i) = set {c} ×∘ A c" by auto

lemma vdunion_vdoubleton: 
  "(∐∘i∈∘set{a, b}. A i) = set {a} ×∘ A a ∪∘ set {b} ×∘ A b" 
  by auto


text‹Connections.›

lemma vdunion_vsum: "(∐∘i∈∘set{0, 1}. if i=0 then A else B) = A ⨄ B"
  unfolding vdunion_vdoubleton vsum_def by simp



subsection‹Canonical injection›
                                         
definition vcinjection :: "(V ⇒ V) ⇒ V ⇒ V"
  where "vcinjection A i = (λx∈∘A i. ⟨i, x⟩)"


text‹Rules.›

mk_VLambda vcinjection_def
  |vsv vcinjection_vsv[intro]|
  |vdomain vcinjection_vdomain[simp]|
  |app vcinjection_app[simp, intro]|


text‹Elementary results.›

lemma vcinjection_vrange_vsubset: 
  assumes "i ∈∘ I" 
  shows "ℛ∘ (vcinjection A i) ⊆∘ (∐∘i∈∘I. A i)"
  unfolding vcinjection_def
proof(intro vrange_VLambda_vsubset)
  fix x assume prems: "x ∈∘ A i"
  show "⟨i, x⟩ ∈∘ (∐∘i∈∘I. A i)" 
    by (intro vdunionI[where A=A, OF _ assms prems]) simp
qed

lemma vcinjection_vrange: 
  assumes "i ∈∘ I" and "⋀j. j ∈∘ I ⟹ A j ≠ 0"
  shows "ℛ∘ (vcinjection A i) = (⋃∘x∈∘A i. set {⟨i, x⟩})"
proof(intro vsubset_antisym)
  interpret vsv ‹vcinjection A i› by (rule vcinjection_vsv)
  show "ℛ∘ (vcinjection A i) ⊆∘ (⋃∘x∈∘A i. set {⟨i, x⟩})"
    unfolding vcinjection_def
  proof(intro vrange_VLambda_vsubset)
    fix x assume prems: "x ∈∘ A i"
    show "⟨i, x⟩ ∈∘ (⋃∘x∈∘A i. set {⟨i, x⟩})" 
      by (intro vifunionI, rule prems) simp
  qed
  show "(⋃∘x∈∘A i. set {⟨i, x⟩}) ⊆∘ ℛ∘ (vcinjection A i)"
  proof(rule vsubsetI)
    fix ix assume "ix ∈∘ (⋃∘x∈∘A i. set {⟨i, x⟩})"
    then obtain x where x: "x ∈∘ A i" and ix_def: "ix = ⟨i, x⟩" 
      by (elim vifunionE) auto
    with x show "ix ∈∘ ℛ∘ (vcinjection A i)"
      unfolding ix_def by (intro vsv_vimageI2') auto
  qed
qed



subsection‹Infinite Cartesian product›

definition vproduct :: "V ⇒ (V ⇒ V) ⇒ V"
  where "vproduct I A = set {f. vsv f ∧ 𝒟∘ f = I ∧ (∀i∈∘I. f⦇i⦈ ∈∘ A i)}"

syntax "_VPRODUCT" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3∏∘_∈∘_./ _)› [0, 0, 10] 10)

translations "∏∘i∈∘I. A" ⇌ "CONST vproduct I (λi. A)"

lemma small_vproduct[simp]:
  "small {f. vsv f ∧ 𝒟∘ f = I ∧ (∀i∈∘I. f⦇i⦈ ∈∘ A i)}"
  (is ‹small ?A›)
proof-
  from small_vsv[of I ‹(⋃∘i∈∘I. A i)›] have 
    "small {f. vsv f ∧ 𝒟∘ f = I ∧ ℛ∘ f ⊆∘ (⋃∘i∈∘I. A i)}"
    by simp
  moreover have "?A ⊆ {f. vsv f ∧ 𝒟∘ f = I ∧ ℛ∘ f ⊆∘ (⋃∘i∈∘I. A i)}"
  proof(intro subsetI, unfold mem_Collect_eq, elim conjE, intro conjI)
    fix f assume prems: "vsv f" "𝒟∘ f = I" "∀i∈elts I. f⦇i⦈ ∈∘ A i"
    interpret vsv f by (rule prems(1))
    show "ℛ∘ f ⊆∘ (⋃∘i∈∘I. A i)"
    proof(intro vsubsetI)
      fix y assume "y ∈∘ ℛ∘ f"
      with prems(2) obtain i where y_def: "y = f⦇i⦈" and i: "i ∈∘ I"
        by (blast dest: vrange_atD)
      from i prems(3) vifunionI show "y ∈∘ (⋃∘i∈∘I. A i)" 
        unfolding y_def by auto
    qed
  qed
  ultimately show ?thesis by (metis (lifting) smaller_than_small)
qed


text‹Rules.›

lemma vproductI[intro!]:
  assumes "vsv f" and "𝒟∘ f = I" and "∀i∈∘I. f⦇i⦈ ∈∘ A i"
  shows "f ∈∘ (∏∘i∈∘I. A i)"
  using assms small_vproduct unfolding vproduct_def by auto

lemma vproductD[dest]:
  assumes "f ∈∘ (∏∘i∈∘I. A i)"
  shows "vsv f" 
    and "𝒟∘ f = I"
    and "∀i∈∘I. f⦇i⦈ ∈∘ A i"
  using assms unfolding vproduct_def by auto

lemma vproductE[elim!]:
  assumes "f ∈∘ (∏∘i∈∘I. A i)"
  obtains "vsv f" and "𝒟∘ f = I" and "∀i∈∘I. f⦇i⦈ ∈∘ A i"
  using assms unfolding vproduct_def by auto


text‹Set operations.›

lemma vproduct_index_vempty[simp]: "(∏∘i∈∘0. A i) = set {0}"
proof-
  have "{f. vsv f ∧ 𝒟∘ f = 0 ∧ (∀i∈∘0. f⦇i⦈ ∈∘ A i)} = {0}"
    using vbrelation.vlrestriction_vdomain vsv_eqI by fastforce
  then show ?thesis unfolding vproduct_def by simp
qed

lemma vproduct_vsingletonI:
  assumes "f⦇c⦈ ∈∘ A c" and "f = set {⟨c, f⦇c⦈⟩}" 
  shows "f ∈∘ (∏∘i∈∘set{c}. A i)"
  using assms 
  apply(intro vproductI)
  subgoal by (metis rel_vsingleton.vsv_axioms)
  subgoal by (force intro!: vsubset_antisym)
  subgoal by auto
  done

lemma vproduct_vsingletonD: 
  assumes "f ∈∘ (∏∘i∈∘set{c}. A i)" 
  shows "vsv f" and "f⦇c⦈ ∈∘ A c" and "f = set {⟨c, f⦇c⦈⟩}"
proof-
  from assms show "f = set {⟨c, f⦇c⦈⟩}"
    by (elim vproductE) (metis VLambda_vsingleton  vsv.vsv_is_VLambda)
qed (use assms in auto)

lemma vproduct_vsingletonE: 
  assumes "f ∈∘ (∏∘i∈∘set{c}. A i)" 
  obtains "vsv f" and "f⦇c⦈ ∈∘ A c" and "f = set {⟨c, f⦇c⦈⟩}"
  using assms vproduct_vsingletonD that by auto

lemma vproduct_vsingleton_iff: 
  "f ∈∘ (∏∘i∈∘set{c}. A i) ⟷ f⦇c⦈ ∈∘ A c ∧ f = set {⟨c, f⦇c⦈⟩}" 
  by (rule iffI) (auto simp: vproduct_vsingletonD intro!: vproduct_vsingletonI)

lemma vproduct_vdoubletonI[intro]:
  assumes "vsv f"
    and "f⦇a⦈ ∈∘ A a" 
    and "f⦇b⦈ ∈∘ A b" 
    and "𝒟∘ f = set {a, b}"
    and "ℛ∘ f ⊆∘ A a ∪∘ A b"
  shows "f ∈∘ (∏∘i∈∘set {a, b}. A i)"
  using assms vifunion_vdoubleton by (intro vproductI) auto

lemma vproduct_vdoubletonD[dest]: 
  assumes "f ∈∘ (∏∘i∈∘set{a, b}. A i)" 
  shows "vsv f"
    and "f⦇a⦈ ∈∘ A a" 
    and "f⦇b⦈ ∈∘ A b" 
    and "𝒟∘ f = set {a, b}" 
    and "f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}"
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms vifunion_vdoubleton by fastforce
  subgoal by (metis assms VLambda_vdoubleton vproductE vsv.vsv_is_VLambda)
  done

lemma vproduct_vdoubletonE: 
  assumes "f ∈∘ (∏∘i∈∘set{a, b}. A i)" 
  obtains "vsv f"
    and "f⦇a⦈ ∈∘ A a" 
    and "f⦇b⦈ ∈∘ A b" 
    and "𝒟∘ f = set {a, b}" 
    and "f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}"
  using assms vproduct_vdoubletonD that by simp

lemma vproduct_vdoubleton_iff: 
  "f ∈∘ (∏∘i∈∘set {a, b}. A i) ⟷ 
    vsv f ∧ 
    f⦇a⦈ ∈∘ A a ∧ 
    f⦇b⦈ ∈∘ A b ∧ 
    𝒟∘ f = set {a, b} ∧ 
    f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}" 
  by (force elim!: vproduct_vdoubletonE)+


text‹Elementary properties.›

lemma vproduct_eq_vemptyI:
  assumes "i ∈∘ I" and "A i = 0"
  shows "(∏∘i∈∘I. A i) = 0"
proof(intro vsubset_antisym vsubsetI)
  fix x assume prems: "x ∈∘ (∏∘i∈∘I. A i)"
  from assms vproductD(3)[OF prems] show "x ∈∘ 0" by auto
qed auto

lemma vproduct_eq_vemptyD:
  assumes "(∏∘i∈∘I. A i) ≠ 0"
  shows "⋀i. i ∈∘ I ⟹ A i ≠ 0"
proof(rule ccontr, unfold not_not)
  fix i assume prems: "i ∈∘ I" "A i = 0"
  with vproduct_eq_vemptyI[where A=A, OF prems] assms show False by simp
qed

lemma vproduct_vrange:
  assumes "f ∈∘ (∏∘i∈∘I. A i)"
  shows "ℛ∘ f ⊆∘ (⋃∘i∈∘I. A i)"
proof(intro vsubsetI)
  fix x assume prems: "x ∈∘ ℛ∘ f"
  have vsv_f: "vsv f"
    and dom_f: "𝒟∘ f = I"
    and fi: "⋀i. i ∈∘ I ⟹ f⦇i⦈ ∈∘ A i"
    by (simp_all add: vproductD[OF assms, rule_format])
  interpret f: vsv f by (rule vsv_f)
  from prems dom_f obtain i where x_def: "x = f⦇i⦈" and i: "i ∈∘ I"
    by (auto elim: f.vrange_atE) 
  from i fi show "x ∈∘ (⋃∘i∈∘I. A i)" unfolding x_def by (intro vifunionI) auto
qed

lemma vproduct_vsubset_VPow: "(∏∘i∈∘I. A i) ⊆∘ VPow (I ×∘ (⋃∘i∈∘I. A i))"
proof(intro vsubsetI)
  fix f assume "f ∈∘ (∏∘i∈∘I. A i)"
  then have vsv: "vsv f" 
    and domain: "𝒟∘ f = I" 
    and range: "∀i∈elts I. f⦇i⦈ ∈∘ A i" 
    by auto
  interpret f: vsv f by (rule vsv)
  have "f ⊆∘ I ×∘ (⋃∘i∈∘I. A i)"
  proof(intro vsubsetI)
    fix x assume prems: "x ∈∘ f"
    then obtain a b where x_def: "x = ⟨a, b⟩" by (elim f.vbrelation_vinE)
    with prems have "a ∈∘ 𝒟∘ f" and "b ∈∘ ℛ∘ f" by auto
    with range domain prems show "x ∈∘ I ×∘ (⋃∘i∈∘I. A i)"
      by (fastforce simp: x_def)
  qed
  then show "f ∈∘ VPow (I ×∘ (⋃∘i∈∘I. A i))" by simp
qed

lemma VLambda_in_vproduct:
  assumes "⋀i. i ∈∘ I ⟹ f i ∈∘ A i"
  shows "(λi∈∘I. f i) ∈∘ (∏∘i∈∘I. A i)"
  using assms by (simp add: vproductI vsv.vsv_vrange_vsubset_vifunion_app)

lemma vproduct_cong:
  assumes "⋀i. i ∈∘ I ⟹ f i = g i"
  shows "(∏∘i∈∘I. f i) = (∏∘i∈∘I. g i)"
proof-
  have "(∏∘i∈∘I. f i) ⊆∘ (∏∘i∈∘I. g i)" if "⋀i. i ∈∘ I ⟹ f i = g i" for f g
  proof(intro vsubsetI)
    fix x assume "x ∈∘ (∏∘i∈∘I. f i)"
    note xD = vproductD[OF this]     
    interpret vsv x by (rule xD(1))
    show "x ∈∘ (∏∘i∈∘I. g i)" 
      by (metis xD(2,3) that VLambda_in_vproduct vsv_is_VLambda)
  qed
  with assms show ?thesis by (intro vsubset_antisym) auto
qed

lemma vproduct_ex_in_vproduct:
  assumes "x ∈∘ (∏∘i∈∘J. A i)" and "J ⊆∘ I" and "⋀i. i ∈∘ I ⟹ A i ≠ 0"
  obtains X where "X ∈∘ (∏∘i∈∘I. A i)" and "x = X ↾l∘ J"
proof-
  define X where "X = (λi∈∘I. if i ∈∘ J then x⦇i⦈ else (SOME x. x ∈∘ A i))" 
  have X: "X ∈∘ (∏∘i∈∘I. A i)"
    by (intro vproductI) (use assms in ‹auto simp: X_def›)
  moreover have "x = X ↾l∘ J"
  proof(rule vsv_eqI)
    from assms(1) have [simp]: "𝒟∘ x = J" by clarsimp 
    moreover from assms(2) have "𝒟∘ (X ↾l∘ J) = J" unfolding X_def by fastforce
    ultimately show "𝒟∘ x = 𝒟∘ (X ↾l∘ J)" by simp 
    show "x⦇i⦈ = (X ↾l∘ J)⦇i⦈" if "i ∈∘ 𝒟∘ x" for i
      using that assms(2) unfolding X_def by auto
  qed (use assms X in auto)
  ultimately show ?thesis using that by simp
qed

lemma vproduct_vsingleton_def: "(∏∘i∈∘set {j}. A i) = (∏∘i∈∘set {j}. A j)"
  by auto

lemma vprojection_in_VUnionI:
  assumes "A ⊆∘ (∏∘i∈∘I. F i)" and "f ∈∘ A" and "i ∈∘ I"
  shows "f⦇i⦈ ∈∘ ⋃∘(⋃∘(⋃∘A))"
proof(intro VUnionI)
  show "f ∈∘ A" by (rule assms(2))
  from assms(1,2) have "f ∈∘ (∏∘i∈∘I. F i)" by auto
  note f = vproductD[OF this, rule_format]
  interpret vsv f rewrites "𝒟∘ f = I" by (auto intro: f(1) simp: f(2))
  show "⟨i, f⦇i⦈⟩ ∈∘ f" by (meson assms(3) vsv_appE)
  show "set {i, f⦇i⦈} ∈∘ ⟨i, f⦇i⦈⟩" unfolding vpair_def by simp
qed simp


subsection‹Projection›

definition vprojection :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V"
  where "vprojection I A i = (λf∈∘(∏∘i∈∘I. A i). f⦇i⦈)"


text‹Rules.›

mk_VLambda vprojection_def
  |vsv vprojection_vsv[intro]|
  |vdomain vprojection_vdomain[simp]|
  |app vprojection_app[simp, intro]|


text‹Elementary results.›

lemma vprojection_vrange_vsubset: 
  assumes "i ∈∘ I" 
  shows "ℛ∘ (vprojection I A i) ⊆∘ A i"
  unfolding vprojection_def
proof(intro vrange_VLambda_vsubset)
  fix f assume prems: "f ∈∘ (∏∘i∈∘I. A i)"
  show "f⦇i⦈ ∈∘ A i" by (intro vproductD(3)[OF prems, rule_format] assms)
qed

lemma vprojection_vrange: 
  assumes "i ∈∘ I" and "⋀j. j ∈∘ I ⟹ A j ≠ 0"
  shows "ℛ∘ (vprojection I A i) = A i"
proof
  (
    intro 
      vsubset_antisym vprojection_vrange_vsubset vrange_VLambda_vsubset assms(1)
  )
  show "A i ⊆∘ ℛ∘ (vprojection I A i)"
  proof(intro vsubsetI)
    fix x assume prems: "x ∈∘ A i"
    obtain f 
      where f: "⋀x. x ∈∘ set {A i | i. i ∈∘ I} ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈∘ x" 
        and "vsv f"
      using that by (rule Axiom_of_Choice)
    define f' where "f' = (λj∈∘I. if j = i then x else f⦇A j⦈)"
    show "x ∈∘ ℛ∘ (vprojection I A i)"               
      unfolding vprojection_def
    proof(rule rel_VLambda.vsv_vimageI2')
      show "f' ∈∘ 𝒟∘ (λf∈∘vproduct I A. f⦇i⦈)"
        unfolding vdomain_VLambda
      proof(intro vproductI, unfold Ball_def; (intro allI conjI impI)?)
        fix j assume "j ∈∘ I"
        with prems assms(2) show "f'⦇j⦈ ∈∘ A j"
          unfolding f'_def by (cases ‹j = i›) (auto intro!: f)
      qed (simp_all add: f'_def)
      with assms(1) show "x = (λf∈∘vproduct I A. f⦇i⦈)⦇f'⦈"
        unfolding f'_def by simp
    qed
  qed
qed



subsection‹Cartesian power of a set›

definition vcpower :: "V ⇒ V ⇒ V" (infixr ‹^×› 80)
  where "A ^× n = (∏∘i∈∘n. A)"


text‹Rules.›

lemma vcpowerI[intro]:
  assumes "f ∈∘ (∏∘i∈∘n. A)"
  shows "f ∈∘ (A ^× n)" 
  using assms unfolding vcpower_def by auto

lemma vcpowerD[dest]:
  assumes "f ∈∘ (A ^× n)"
  shows "f ∈∘ (∏∘i∈∘n. A)"
  using assms unfolding vcpower_def by auto

lemma vcpowerE[elim]:
  assumes "f ∈∘ (A ^× n)" and "f ∈∘ (∏∘i∈∘n. A) ⟹ P"
  shows P
  using assms unfolding vcpower_def by auto


text‹Set operations.›

lemma vcpower_index_vempty[simp]: "A ^× 0 = set {0}"
  unfolding vcpower_def by (rule vproduct_index_vempty)

lemma vcpower_of_vempty: 
  assumes "n ≠ 0"
  shows "0 ^× n = 0"
  using assms unfolding vcpower_def vproduct_def by simp

lemma vcpower_vsubset_mono: 
  assumes "A ⊆∘ B"
  shows "A ^× n ⊆∘ B ^× n"
  using assms
  by (intro vsubsetI vcpowerI vproductI)
    (auto intro: vproductD[OF vcpowerD, rule_format])


text‹Connections.›

lemma vcpower_vdomain: 
  assumes "f ∈∘ (A ^× n)"
  shows "𝒟∘ f = n"
  using assms by auto

lemma vcpower_vrange:
  assumes "f ∈∘ (A ^× n)"
  shows "ℛ∘ f ⊆∘ A"
  using assms by (intro vsubsetI; elim vcpowerE vproductE) auto

text‹\newpage›

end