(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2005-2008 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 equalities

begin

text{*Standard Isabelle distribution contains lots of facts about basic set

theory. This theory file adds some more.*}

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 one collection is contained in another, then we can say the same

abot their unions.*}

lemma collection_contain: assumes "A⊆B" shows "\<Union>A ⊆ \<Union>B"

proof

fix x assume "x ∈ \<Union>A"

then obtain X where "x∈X" and "X∈A" by auto

with assms show "x ∈ \<Union>B" by auto

qed

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 assms 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{*If 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: "∀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}"

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

text{*If two meta-functions are the same on a cartesian product,

then the subsets defined by them are the same.

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{*A 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×V≠0" "U×V ⊆ X×Y" shows "U⊆X" and "V⊆Y"

using assms by auto

text{*A 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 ⊆ {t∈X. ⟨t,y⟩ ∈ A}" and "V ⊆ {t∈Y. ⟨x,t⟩ ∈ A}"

using assms by auto

text{*If two meta-functions are the same on a set, then they define the same

set by separation.*}

lemma ZF1_1_L4B: assumes "∀x∈X. a(x) = b(x)"

shows "{a(x). x∈X} = {b(x). x∈X}"

using assms 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 assms 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 assms by auto

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

lemma nonempty_has_element: assumes "X≠0" shows "∃x. x∈X"

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; *)

text{*In Isabelle/ZF the intersection of an empty family is

empty. This is exactly lemma @{text "Inter_0"} from Isabelle's

@{text "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 "\<Inter>0 = 0" by (rule Inter_0);

text{*If an intersection of a collection is not empty, then the collection is

not empty. We are (ab)using the fact the the intesection of empty collection

is defined to be empty.*}

lemma inter_nempty_nempty: assumes "\<Inter>A ≠ 0" shows "A≠0"

using assms 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$.*}

definition

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

text{*The union 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 i⇩_{0}where "i⇩_{0}∈ I" by auto

with A2 have "( \<Inter>i∈I. P(i) ) ⊆ P(i⇩_{0})" and "P(i⇩_{0}) ⊆ X"

by auto

thus "( \<Inter>i∈I. P(i) ) ⊆ X" by auto

qed

text{*Isabelle/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 "\<Union> {x} = x" by auto

text{*Some properties of singletons.*}

lemma ZF1_1_L9: assumes A1: "∃! x. x∈A ∧ φ(x)"

shows

"∃a. {x∈A. φ(x)} = {a}"

"\<Union> {x∈A. φ(x)} ∈ A"

"φ(\<Union> {x∈A. φ(x)})"

proof -

from A1 show "∃a. {x∈A. φ(x)} = {a}" by auto

then obtain a where I: "{x∈A. φ(x)} = {a}" by auto

then have "\<Union> {x∈A. φ(x)} = a" by auto

moreover

from I have "a ∈ {x∈A. φ(x)}" by simp

hence "a∈A" and "φ(a)" by auto

ultimately show "\<Union> {x∈A. φ(x)} ∈ A" and "φ(\<Union> {x∈A. φ(x)})"

by auto

qed

text{*A simple version of @{text " ZF1_1_L9"}. *}

corollary sigleton_extract: assumes "∃! x. x∈A"

shows "(\<Union> A) ∈ A"

proof -

from assms have "∃! x. x∈A ∧ True" by simp;

then have "\<Union> {x∈A. True} ∈ A" by (rule ZF1_1_L9);

thus "(\<Union> A) ∈ A" by simp;

qed;

text{*A criterion for when a set defined by comprehension is a singleton.*}

lemma singleton_comprehension:

assumes A1: "y∈X" and A2: "∀x∈X. ∀y∈X. P(x) = P(y)"

shows "(\<Union>{P(x). x∈X}) = P(y)"

proof -

let ?A = "{P(x). x∈X}"

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 "(\<Union>?A) ∈ ?A" by (rule sigleton_extract);

then obtain x where "x ∈ X" and "(\<Union>?A) = P(x)"

by auto;

from A1 A2 `x ∈ X` have "P(x) = P(y)"

by blast;

with `(\<Union>?A) = P(x)` show "(\<Union>?A) = P(y)" by simp;

qed;

text{*Adding an element of a set to that set does not change the set.*}

lemma set_elem_add: assumes "x∈X" shows "X ∪ {x} = X" using assms

by auto

text{*Here 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}"

text{*A lemma on a union of a restriction of a collection

to a set.*}

lemma union_restrict:

shows "\<Union>(M {restricted to} X) = (\<Union>M) ∩ X"

using RestrictedTo_def by auto;

text{*Next 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: "∀U∈C. ∃A∈B. U = \<Union>A"

shows "\<Union>\<Union> {\<Union>{A∈B. U = \<Union>A}. U∈C} = \<Union>C"

proof

show "\<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A}) ⊆ \<Union>C" by blast

show "\<Union>C ⊆ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})"

proof

fix x assume "x ∈ \<Union>C"

show "x ∈ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})"

proof -

from `x ∈ \<Union>C` obtain U where "U∈C ∧ x∈U" by auto

with A1 obtain A where "A∈B ∧ U = \<Union>A" by auto

from `U∈C ∧ x∈U` `A∈B ∧ U = \<Union>A` show "x∈ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})"

by auto

qed

qed

qed

text{*Standard Isabelle uses a notion of @{text "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;

text{*If a difference between a set and a sigleton is empty, then

the set is empty or it is equal to the sigleton.*}

lemma singl_diff_empty: assumes "A - {x} = 0"

shows "A = 0 ∨ A = {x}"

using assms by auto;

text{*If a difference between a set and a sigleton 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;

text{*A basic property of sets defined by comprehension.

This is one side of standard Isabelle's @{text "separation"}

that is in the simp set but somehow not always used by simp. *}

lemma comprehension: assumes "a ∈ {x∈X. p(x)}"

shows "a∈X" and "p(a)" using assms by auto

end