Theory ZF1

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2005-2023  Slawomir Kolodynski

    This program is free software Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ZF set theory basics

theory ZF1 imports ZF.Perm

begin

textThe standard Isabelle distribution contains lots of facts about basic set
  theory. This theory file adds some more.

subsectionLemmas in Zermelo-Fraenkel set theory

textHere we put lemmas from the set theory that we could not find in 
  the standard Isabelle distribution or just so that they are easier to find.

textA set cannot be a member of itself. This is exactly lemma mem_not_refl›
  from Isabelle/ZF upair.thy›, we put it here for easy reference. 

lemma mem_self: shows "xx" by (rule mem_not_refl)

textIf one collection is contained in another, then we can say the same
  about their unions.

lemma collection_contain: assumes "AB" shows "A  B"
proof
  fix x assume "x  A"
  then obtain X where "xX" and "XA" by auto
  with assms show "x  B" by auto
qed

textIf all sets of a nonempty collection are the same, then its union 
  is the same.

lemma ZF1_1_L1: assumes "C0" and "yC. b(y) = A" 
  shows "(yC. b(y)) = A" using assms by blast
  
textThe union af all values of a constant meta-function belongs to 
the same set as the constant.

lemma ZF1_1_L2: assumes A1:"C0" and A2: "xC. b(x)  A" 
  and A3: "x y. xC  yC  b(x) = b(y)"
  shows "(xC. b(x))A"
proof -
  from A1 obtain x where D1: "xC" by auto
  with A3 have "yC. b(y) = b(x)" by blast
  with A1 have "(yC. b(y)) = b(x)" 
    using ZF1_1_L1 by simp
  with D1 A2 show ?thesis by simp
qed

textIf two meta-functions are the same on a cartesian product,
  then the subsets defined by them are the same. I am surprised Isabelle
  can not handle this automatically.

lemma ZF1_1_L4: assumes A1: "xX.yY. a(x,y) = b(x,y)"
  shows "{a(x,y). x,y  X×Y} = {b(x,y). x,y  X×Y}"
proof
  show "{a(x, y). x,y  X × Y}  {b(x, y). x,y  X × Y}"
  proof
    fix z assume "z  {a(x, y) . x,y  X × Y}"
    with A1 show  "z  {b(x,y).x,y  X×Y}" by auto   
  qed
  show "{b(x, y). x,y  X × Y}  {a(x, y). x,y  X × Y}"
  proof
    fix z assume "z  {b(x, y). x,y  X × Y}"
    with A1 show "z  {a(x,y).x,y  X×Y}" by auto
  qed
qed

textIf two meta-functions are the same on a cartesian product,
  then the subsets defined by them are the same. 
  This is similar to ZF1_1_L4›, except that
  the set definition varies over p∈X×Y› rather than 
  ⟨ x,y⟩∈X×Y›.

lemma ZF1_1_L4A: assumes A1: "xX.yY. a( x,y) = b(x,y)"
  shows "{a(p). p  X×Y} = {b(x,y). x,y  X×Y}"
proof
  { fix z assume "z  {a(p). pX×Y}"
    then obtain p where D1: "z=a(p)" "pX×Y" by auto
    let ?x = "fst(p)" let ?y = "snd(p)"
    from A1 D1 have "z  {b(x,y). x,y  X×Y}" by auto
  } then show "{a(p). p  X×Y}  {b(x,y). x,y  X×Y}" by blast
next 
  { fix z assume "z  {b(x,y). x,y  X×Y}"
    then obtain x y where D1: "x,y  X×Y" "z=b(x,y)" by auto
    let ?p = " x,y" 
    from A1 D1 have "?pX×Y" "z = a(?p)" by auto
    then have "z  {a(p). p  X×Y}" by auto
  } then show "{b(x,y). x,y  X×Y}  {a(p). p  X×Y}" by blast
qed

textA lemma about inclusion in cartesian products. Included here to remember
  that we need the $U\times V \neq \emptyset$ assumption.

lemma prod_subset: assumes "U×V0" "U×V  X×Y" shows "UX" and "VY"
  using assms by auto

textA technical lemma about sections in cartesian products.

lemma section_proj: assumes "A  X×Y" and "U×V  A" and "x  U"  "y  V"
  shows "U  {tX. t,y  A}" and "V  {tY. x,t  A}"
  using assms by auto

textIf two meta-functions are the same on a set, then they define the same
  set by separation.

lemma ZF1_1_L4B: assumes "xX. a(x) = b(x)"
  shows "{a(x). xX} = {b(x). xX}"
  using assms by simp

textA set defined by a constant meta-function is a singleton.

lemma ZF1_1_L5: assumes "X0" and "xX. b(x) = c"
  shows "{b(x). xX} = {c}" using assms by blast

textMost of the time, auto› does this job, but there are strange 
  cases when the next lemma is needed.

lemma subset_with_property: assumes "Y = {xX. b(x)}"
  shows "Y  X" 
  using assms by auto

textWe can choose an element from a nonempty set.

lemma nonempty_has_element: assumes "X0" shows "x. xX"
  using assms by auto

(*text{*If after removing an element from a set we get an empty set,
  then this set must be a singleton.*}

lemma rem_point_empty: assumes "a∈A" and "A-{a} = 0"
  shows "A = {a}" using assms by auto; *)

textIn Isabelle/ZF the intersection of an empty family is 
  empty. This is exactly lemma Inter_0› from Isabelle's
  equalities› theory. We repeat this lemma here as it is very
  difficult to find. This is one reason we need comments before every 
  theorem: so that we can search for keywords.

lemma inter_empty_empty: shows "0 = 0" by (rule Inter_0)

textIf an intersection of a collection is not empty, then the collection is
  not empty. We are (ab)using the fact the the intersection of empty collection 
  is defined to be empty.

lemma inter_nempty_nempty: assumes "A  0" shows "A0"
  using assms by auto

textFor two collections $S,T$ of sets we define the product collection
  as the collections of cartesian products $A\times B$, where $A\in S, B\in T$.

definition
  "ProductCollection(T,S)  UT.{U×V. VS}"

textThe union of the product collection of collections $S,T$ is the 
  cartesian product of $\bigcup S$ and  $\bigcup T$.

lemma ZF1_1_L6: shows " ProductCollection(S,T) = S × T"
  using ProductCollection_def by auto

textAn intersection of subsets is a subset.

lemma ZF1_1_L7: assumes A1: "I0" and A2: "iI. P(i)  X"
  shows "( iI. P(i) )  X"
proof -
  from A1 obtain i0 where "i0  I" by auto
  with A2 have "( iI. P(i) )  P(i0)" and "P(i0)  X"
    by auto
  thus "( iI. P(i) )  X" by auto
qed

textIsabelle/ZF has a "THE" construct that allows to define an element
  if there is only one such that is satisfies given predicate.
  In pure ZF we can express something similar using the indentity proven below.

lemma ZF1_1_L8: shows " {x} = x" by auto

textSome properties of singletons.

lemma ZF1_1_L9: assumes A1: "∃! x. xA  φ(x)"
  shows 
  "a. {xA. φ(x)} = {a}"
  " {xA. φ(x)}  A"
  "φ( {xA. φ(x)})"
proof -
  from A1 show "a. {xA. φ(x)} = {a}" by auto
  then obtain a where I: "{xA. φ(x)} = {a}" by auto
  then have " {xA. φ(x)} = a" by auto
  moreover
  from I have "a  {xA. φ(x)}" by simp
  hence "aA" and "φ(a)" by auto
  ultimately show " {xA. φ(x)}  A" and "φ( {xA. φ(x)})"
    by auto
qed

textA simple version of  ZF1_1_L9›.

corollary singleton_extract: assumes  "∃! x. xA"
  shows "( A)  A"
proof -
  from assms have "∃! x. xA  True" by simp
  then have " {xA. True}  A" by (rule ZF1_1_L9)
  thus "( A)  A" by simp
qed

textA criterion for when a set defined by comprehension is a singleton.

lemma singleton_comprehension: 
  assumes A1: "yX" and A2: "xX. yX. P(x) = P(y)"
  shows "({P(x). xX}) = P(y)"
proof - 
  let ?A = "{P(x). xX}"
  have "∃! c. c  ?A"
  proof
    from A1 show "c. c  ?A" by auto
  next
    fix a b assume "a  ?A" and "b  ?A"
    then obtain x t where 
      "x  X" "a = P(x)" and "t  X" "b = P(t)"
      by auto
    with A2 show "a=b" by blast
  qed
  then have "(?A)  ?A" by (rule singleton_extract)
  then obtain x where "x  X" and "(?A) = P(x)"
    by auto
  from A1 A2 x  X have "P(x) = P(y)"
    by blast
  with (?A) = P(x) show "(?A) = P(y)" by simp
qed

textAdding an element of a set to that set does not change the set.

lemma set_elem_add: assumes "xX" shows "X  {x} = X" using assms 
  by auto

textHere we define a restriction of a collection of sets to a given set. 
  In romantic math this is typically denoted $X\cap M$ and means 
  $\{X\cap A : A\in M \} $. Note there is also restrict$(f,A)$ 
  defined for relations in ZF.thy.

definition
  RestrictedTo (infixl "{restricted to}" 70) where
  "M {restricted to} X  {X  A . A  M}"

textA lemma on a union of a restriction of a collection
  to a set.

lemma union_restrict: 
  shows "(M {restricted to} X) = (M)  X"
  using RestrictedTo_def by auto

textNext we show a technical identity that is used to prove sufficiency 
  of some condition for a collection of sets to be a base for a topology.

lemma ZF1_1_L10: assumes A1: "UC. AB. U = A" 
  shows " {{AB. U = A}. UC} = C"
proof
  show "(UC. {A  B . U = A})  C" by blast
  show "C  (UC. {A  B . U = A})"
  proof
    fix x assume "x  C" 
    show "x  (UC. {A  B . U = A})"
    proof -
      from x  C obtain U where "UC  xU" by auto
      with A1 obtain A where "AB  U = A" by auto
      from UC  xU AB  U = A show "x (UC. {A  B . U = A})" 
	by auto
    qed
  qed
qed

textStandard Isabelle uses a notion of cons(A,a)› that can be thought 
  of as $A\cup \{a\}$.

lemma consdef: shows "cons(a,A) = A  {a}"
  using cons_def by auto

textIf a difference between a set and a singleton is empty, then
  the set is empty or it is equal to the singleton.

lemma singl_diff_empty: assumes "A - {x} = 0"
  shows "A = 0  A = {x}"
  using assms by auto

textIf a difference between a set and a singleton is the set, 
  then the only element of the singleton is not in the set.

lemma singl_diff_eq: assumes A1: "A - {x} = A"
  shows "x  A"
proof -
  have "x  A - {x}" by auto
  with A1 show "x  A" by simp
qed

textSimple substitution in membership, has to be used by rule
  in very rare cases.

lemma eq_mem: assumes "xA" and "y=x" shows "yA" 
  using assms by simp

textA basic property of sets defined by comprehension.

lemma comprehension: assumes "a  {xX. p(x)}"
  shows "aX" and "p(a)" using assms by auto

textA basic property of a set defined by another type of comprehension.

lemma comprehension_repl: assumes "y  {p(x). xX}"
  shows "xX. y = p(x)" using assms by auto

textThe inverse of the comprehension› lemma.

lemma mem_cond_in_set: assumes "φ(c)" and "cX"
  shows "c  {xX. φ(x)}" using assms by blast

textThe image of a set by a greater relation is greater. 

lemma image_rel_mono: assumes "rs" shows "r``(A)  s``(A)" 
  using assms by auto 

text A technical lemma about relations: if $x$ is in its image by a relation $U$
  and that image is contained in some set $C$, then the image of the singleton
  $\{ x\}$ by the relation $U \cup C\times C$ equals $C$. 

lemma image_greater_rel: 
  assumes  "x  U``{x}"  and "U``{x}  C"
  shows "(U  C×C)``{x} = C"
  using assms image_Un_left by blast 

textReformulation of the definition of composition of two relations: 

lemma rel_compdef: 
  shows "x,z  r O s    (y. x,y  s  y,z  r)" 
  unfolding comp_def by auto

textDomain and range of the relation of the form $\bigcup \{U\times U : U\in P\}$
  is $\bigcup P$: 

lemma domain_range_sym: shows "domain({U×U. UP}) = P" and "range({U×U. UP}) = P" 
  by auto

textAn identity for the square (in the sense of composition) of a symmetric relation.

lemma symm_sq_prod_image: assumes "converse(r) = r" 
  shows "r O r = {(r``{x})×(r``{x}). x  domain(r)}"
proof
  { fix p assume "p  r O r"
    then obtain y z where "y,z = p" by auto
    with p  r O r obtain x where "y,x  r" and "x,z  r"
      using rel_compdef by auto
    from y,x  r have "x,y  converse(r)" by simp
    with assms x,z  r y,z = p have "xdomain(r). p  (r``{x})×(r``{x})"
      by auto
  } thus "r O r  ({(r``{x})×(r``{x}). x  domain(r)})"
    by blast
  { fix x assume "x  domain(r)"
    have "(r``{x})×(r``{x})  r O r"
    proof -
      { fix p assume "p  (r``{x})×(r``{x})"
        then obtain y z where "y,z = p" "y  r``{x}" "z  r``{x}"
          by auto
        from y  r``{x} have "x,y  r" by auto
        then have "y,x  converse(r)" by simp
        with assms z  r``{x} y,z = p have "p  r O r" by auto
      } thus ?thesis  by auto
    qed
  } thus "({(r``{x})×(r``{x}). x  domain(r)})  r O r" 
    by blast
qed 

textA reflexive relation is contained in the union of products of its singleton images. 

lemma refl_union_singl_image: 
  assumes "A  X×X" and "id(X)A" shows "A  {A``{x}×A``{x}. x  X}" 
proof -
  { fix p assume "pA"
    with assms(1) obtain x y where "xX" "yX" and "p=x,y" by auto
    with assms(2) pA have "xX. p  A``{x}×A``{x}" by auto
  } thus ?thesis by auto
qed

textIf the cartesian product of the images of $x$ and $y$ by a 
  symmetric relation $W$ has a nonempty intersection with $R$
  then $x$ is in relation $W\circ (R\circ W)$ with $y$. 

lemma sym_rel_comp: 
  assumes "W=converse(W)" and "(W``{x})×(W``{y})  R  0"
  shows "x,y  (W O (R O W))" 
proof -
  from assms(2) obtain s t where "sW``{x}" "tW``{y}" and "s,tR"
    by blast
  then have "x,s  W" and "y,t  W" by auto
  from x,s  W s,t  R have "x,t  R O W" by auto
  from y,t  W have "t,y  converse(W)" by blast
  with assms(1) x,t  R O W show ?thesis by auto
qed

text It's hard to believe but there are cases where we have to reference this rule. 

lemma set_mem_eq: assumes "xA" "A=B" shows "xB" using assms by simp

textGiven some family $\mathcal{A}$ of subsets of $X$ we can define the family of supersets of
  $\mathcal{A}$. 

definition
  "Supersets(X,𝒜)  {BPow(X). A𝒜. AB}"

textThe family itself is in its supersets. 

lemma superset_gen: assumes "AX" "A𝒜" shows "A  Supersets(X,𝒜)"
  using assms unfolding Supersets_def by auto 

textThis can be done by the auto method, but sometimes takes a long time. 

lemma witness_exists: assumes "xX" and "φ(x)" shows "xX. φ(x)"
  using assms by auto

textAnother lemma that concludes existence of some set.

lemma witness_exists1: assumes "xX" "φ(x)" "ψ(x)"
  shows "xX. φ(x)  ψ(x)"
  using assms by auto

textThe next lemma has to be used as a rule in some rare cases. 

lemma exists_in_set: assumes "x. xA  φ(x)" shows "xA. φ(x)"
  using assms by simp

textIf $x$ belongs to a set where a property holds, then the property holds
  for $x$. This has to be used as rule in rare cases. 

lemma property_holds: assumes "tX. φ(t)" and "xX"
  shows "φ(x)" using assms by simp

textSet comprehensions defined by equal expressions are the equal. 
  The second assertion is actually about functions, which are sets of pairs 
  as illustrated in lemma fun_is_set_of_pairs› in func1.thy›  

lemma set_comp_eq: assumes "xX. p(x) = q(x)" 
  shows "{p(x). xX} = {q(x). xX}" and "{x,p(x). xX} = {x,q(x). xX}"
  using assms by auto

textIf every element of a non-empty set $X\subseteq Y$ satisfies a condition
  then the set of elements of $Y$ that satisfy the condition is non-empty.

lemma non_empty_cond: assumes "X0" "XY" and "xX. P(x)"
  shows "{xY. P(x)}  0" using assms by auto 

textIf $z$ is a pair, then the cartesian product of the singletons of its 
  elements is the same as the singleton $\{ z\}$. 

lemma pair_prod: assumes "z = x,y" shows "{x}×{y} = {z}"
  using assms by blast

textIn Isabelle/ZF the set difference is written with a minus sign $A-B$
  because the standard backslash character is reserved for other purposes. 
  The next abbreviation declares that we want the set difference character $A\setminus B$
  to be synonymous with the minus sign. 

abbreviation set_difference (infixl "" 65) where "AB  A-B"

textIn ZF set theory the zero of natural numbers is the same as the empty set.
  In the next abbreviation we declare that we want $0$ and $\emptyset$ to be synonyms
  so that we can use $\emptyset$ instead of $0$ when appropriate. 

abbreviation empty_set ("") where "  0" 

end