Theory ZF1

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

    Copyright (C) 2005, 2006  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.

*)

header {*\isaheader{ZF1.thy}*}
theory ZF1 imports pair 

begin

section{*Lemmas in Zermelo-Fraenkel set theory*}

text{*Here we put lemmas from the set theory that we could not find in 
the standard Isabelle distribution.*}

text{*If all sets of a nonempty collection are the same, then its union 
  is the same.*}

lemma ZF1_1_L1: assumes "C≠0" and "∀y∈C. b(y) = A" 
  shows "(\<Union>y∈C. b(y)) = A" using prems by blast;
  
text{*The union af all values of a constant meta-function belongs to 
the same set as the constant.*}

lemma ZF1_1_L2: assumes A1:"C≠0" and A2: "∀x∈C. b(x) ∈ A" 
  and A3: "∀x y. x∈C ∧ y∈C --> b(x) = b(y)"
  shows "(\<Union>x∈C. b(x))∈A"
proof -;
  from A1 obtain x where D1:"x∈C" by auto;
  with A3 have "∀y∈C. b(y) = b(x)" by blast;
  with A1 have "(\<Union>y∈C. b(y)) = b(x)" 
    using ZF1_1_L1 by simp;
  with D1 A2 show ?thesis by simp;
qed;

text{*A purely technical lemma that shows what it means that something
  belongs to a subset of cartesian product defined by separation. Seems 
  there is no way to avoid that ugly lambda notation.
  *}

lemma ZF1_1_L3: assumes A1: "x∈X"  "y∈Y" and A2: "z = a(x,y)"
  shows "z ∈ {a(x,y).⟨x,y⟩ ∈ X×Y}"
proof;
  from A2 show "z = (λ ⟨x,y⟩. a(x, y))(<x,y>)" by simp;
  from A1 show "<x,y> ∈ X×Y" by simp;
qed;

text{*If two meta-functions are the same on a cartesian product,
  then the subsets defined by them are the same. I am surprised blast
  can not handle this.*}

lemma ZF1_1_L4: assumes A1: "∀x∈X.∀y∈Y. 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}";
    then obtain x y where T1: "z = a(x,y)" "x∈X" "y∈Y"
      by auto;
    with A1 have "z = b(x,y)" "x∈X" "y∈Y" by simp;
    then show  "z ∈ {b(x,y).⟨x,y⟩ ∈ X×Y}"
      using ZF1_1_L3 by simp;
  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}";
    then obtain x y where T1: "z = b(x,y)" "x∈X" "y∈Y"
      by auto;
    with A1 have "z = a(x,y)" "x∈X" "y∈Y" by simp;
    then show "z ∈ {a(x,y).⟨x,y⟩ ∈ X×Y}"
      using ZF1_1_L3 by simp;
  qed;
qed;

text{*If two meta-functions are the same on a cartesian product,
  then the subsets defined by them are the same. I am surprised blast
  can not handle this. This is similar to @{text "ZF1_1_L4"}, except that
  the set definition varies over @{text "p∈X×Y"} rather than 
  @{text "<x,y>∈X×Y"}.*}

lemma ZF1_1_L4A: assumes A1: "∀x∈X.∀y∈Y. 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). p∈X×Y}"
    then obtain p where D1: "z=a(p)" "p∈X×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 "?p∈X×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;

text{*If two meta-functions are the same on a set, then they define the same
  set by separation.*}
(* for some more complicated a,b we can not use simp too show that *)
lemma ZF1_1_L4B: assumes "∀x∈X. a(x) = b(x)"
  shows "{a(x). x∈X} = {b(x). x∈X}"
  using prems by simp;

text{*A set defined by a constant meta-function is a singleton.*}

lemma ZF1_1_L5: assumes "X≠0" and "∀x∈X. b(x) = c"
  shows "{b(x). x∈X} = {c}" using prems by blast;

text{* Most of the time, @{text "auto"} does this job, but there are strange 
  cases when the next lemma is needed. *}

lemma subset_with_property: assumes "Y = {x∈X. b(x)}"
  shows "Y ⊆ X" 
  using prems by auto;

text{*We can choose an element from a nonempty set.*}

lemma nonempty_has_element: assumes "X≠0" shows "∃x. x∈X"
  using prems by auto;

text{*For 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$.*}

constdefs
  "ProductCollection(T,S) ≡ \<Union>U∈T.{U×V. V∈S}"

text{*The untion of the product collection of collections $S,T$* is the 
  cartesian product of $\bigcup S$ and  $\bigcup T$. *}

lemma ZF1_1_L6: shows "\<Union> ProductCollection(S,T) = \<Union>S × \<Union>T"
  using ProductCollection_def by auto;

text{*An intersection of subsets is a subset.*}

lemma ZF1_1_L7: assumes A1: "I≠0" and A2: "∀i∈I. P(i) ⊆ X"
  shows "( \<Inter>i∈I. P(i) ) ⊆ X"
proof -
  from A1 obtain i0 where "i0 ∈ I" by auto;
  with A2 have "( \<Inter>i∈I. P(i) ) ⊆ P(i0)" and "P(i0) ⊆ X"
    by auto;
  thus "( \<Inter>i∈I. P(i) ) ⊆ X" by auto;
qed;

end