Theory Finite_ZF

theory Finite_ZF
imports ZF1 Nat_ZF_IML
(* 
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 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{Finite\_ZF.thy}*}

theory Finite_ZF imports ZF1 Nat_ZF_IML Cardinal

begin

text{*Standard Isabelle Finite.thy contains a very useful
notion of finite powerset: the set of finite subsets of a given set.
The definition, however, is specific to Isabelle and based on the notion
of "datatype", obviously not something that belongs to ZF set theory.
This theory file devolopes the notion of finite powerset similarly as
in Finite.thy, but based on standard library's
Cardinal.thy. This theory file is intended to
replace IsarMathLib's @{text "Finite1"} and @{text "Finite_ZF_1"} theories
that are currently derived from the "datatype" approach.
*}


section{*Definition and basic properties of finite powerset*}

text{*The goal of this section is to prove an induction theorem about
finite powersets: if the empty set has some property and this property is
preserved by adding a single element of a set,
then this property is true for all finite subsets of this set. *}



text{*We defined the finite powerset @{text "FinPow(X)"} as those elements
of the powerset that are finite.*}


definition
"FinPow(X) ≡ {A ∈ Pow(X). Finite(A)}"

text{*The cardinality of an element of finite powerset is a natural number.*}

lemma card_fin_is_nat: assumes "A ∈ FinPow(X)"
shows "|A| ∈ nat" and "A ≈ |A|"
using assms FinPow_def Finite_def cardinal_cong nat_into_Card
Card_cardinal_eq by auto;

text{*A reformulation of @{text "card_fin_is_nat"}: for a finit
set $A$ there is a bijection between $|A|$ and $A$.*}


lemma fin_bij_card: assumes A1: "A ∈ FinPow(X)"
shows "∃b. b ∈ bij(|A|, A)"
proof -
from A1 have "|A| ≈ A" using card_fin_is_nat eqpoll_sym
by blast;
then show ?thesis using eqpoll_def by auto
qed;

text{*If a set has the same number of elements as $n \in \mathbb{N}$,
then its cardinality is $n$. Recall that in set theory a natural number
$n$ is a set that has $n$ elements.*}


lemma card_card: assumes "A ≈ n" and "n ∈ nat"
shows "|A| = n"
using assms cardinal_cong nat_into_Card Card_cardinal_eq
by auto;

text{*If we add a point to a finite set, the cardinality
increases by one. To understand the second assertion
$| A \cup \{ a\}| = |A| \cup \{ |A|\} $ recall that
the cardinality $|A|$ of $A$ is a natural number
and for natural numbers we have $n+1 = n \cup \{ n\}$.
*}


lemma card_fin_add_one: assumes A1: "A ∈ FinPow(X)" and A2: "a ∈ X-A"
shows
"|A ∪ {a}| = succ( |A| )"
"|A ∪ {a}| = |A| ∪ {|A|}"
proof -
from A1 A2 have "cons(a,A) ≈ cons( |A|, |A| )"
using card_fin_is_nat mem_not_refl cons_eqpoll_cong
by auto;
moreover have "cons(a,A) = A ∪ {a}" by (rule consdef);
moreover have "cons( |A|, |A| ) = |A| ∪ {|A|}"
by (rule consdef);
ultimately have "A∪{a} ≈ succ( |A| )" using succ_explained
by simp;
with A1 show
"|A ∪ {a}| = succ( |A| )" and "|A ∪ {a}| = |A| ∪ {|A|}"
using card_fin_is_nat card_card by auto;
qed

text{*We can decompose the finite powerset into collection of
sets of the same natural cardinalities.*}


lemma finpow_decomp:
shows "FinPow(X) = (\<Union>n ∈ nat. {A ∈ Pow(X). A ≈ n})"
using Finite_def FinPow_def by auto

text{*Finite powerset is the union of sets of cardinality
bounded by natural numbers.*}


lemma finpow_union_card_nat:
shows "FinPow(X) = (\<Union>n ∈ nat. {A ∈ Pow(X). A \<lesssim> n})"
proof -
have "FinPow(X) ⊆ (\<Union>n ∈ nat. {A ∈ Pow(X). A \<lesssim> n})"
using finpow_decomp FinPow_def eqpoll_imp_lepoll
by auto
moreover have
"(\<Union>n ∈ nat. {A ∈ Pow(X). A \<lesssim> n}) ⊆ FinPow(X)"
using lepoll_nat_imp_Finite FinPow_def by auto
ultimately show ?thesis by auto
qed;

text{*A different form of @{text "finpow_union_card_nat"} (see above) -
a subset that has not more elements than a given natural number
is in the finite powerset.*}


lemma lepoll_nat_in_finpow:
assumes "n ∈ nat" "A ⊆ X" "A \<lesssim> n"
shows "A ∈ FinPow(X)"
using assms finpow_union_card_nat by auto;

text{*Natural numbers are finite subsets of the set of natural numbers.*}

lemma nat_finpow_nat: assumes "n ∈ nat" shows "n ∈ FinPow(nat)"
using assms nat_into_Finite nat_subset_nat FinPow_def
by simp;

text{*A finite subset is a finite subset of itself.*}

lemma fin_finpow_self: assumes "A ∈ FinPow(X)" shows "A ∈ FinPow(A)"
using assms FinPow_def by auto;

text{*If we remove an element and put it back we get the set back.
*}


lemma rem_add_eq: assumes "a∈A" shows "(A-{a}) ∪ {a} = A"
using assms by auto

text{*Induction for finite powerset. This is smilar to the
standard Isabelle's @{text "Fin_induct"}. *}


theorem FinPow_induct: assumes A1: "P(0)" and
A2: "∀A ∈ FinPow(X). P(A) --> (∀a∈X. P(A ∪ {a}))" and
A3: "B ∈ FinPow(X)"
shows "P(B)"
proof -
{ fix n assume "n ∈ nat"
moreover from A1 have I: "∀B∈Pow(X). B \<lesssim> 0 --> P(B)"
using lepoll_0_is_0 by auto
moreover have "∀ k ∈ nat.
(∀B ∈ Pow(X). (B \<lesssim> k --> P(B))) -->
(∀B ∈ Pow(X). (B \<lesssim> succ(k) --> P(B)))"

proof -
{ fix k assume A4: "k ∈ nat"
assume A5: "∀ B ∈ Pow(X). (B \<lesssim> k --> P(B))"
fix B assume A6: "B ∈ Pow(X)" "B \<lesssim> succ(k)"
have "P(B)"
proof -
have "B = 0 --> P(B)"
proof -
{ assume "B = 0"
then have "B \<lesssim> 0" using lepoll_0_iff
by simp
with I A6 have "P(B)" by simp
} thus "B = 0 --> P(B)" by simp
qed
moreover have "B≠0 --> P(B)"
proof -
{ assume "B ≠ 0"
then obtain a where II: "a∈B" by auto
let ?A = "B - {a}"
from A6 II have "?A ⊆ X" and "?A \<lesssim> k"
using Diff_sing_lepoll by auto
with A4 A5 have "?A ∈ FinPow(X)" and "P(?A)"
using lepoll_nat_in_finpow finpow_decomp
by auto
with A2 A6 II have " P(?A ∪ {a})"
by auto
moreover from II have "?A ∪ {a} = B"
by auto
ultimately have "P(B)" by simp
} thus "B≠0 --> P(B)" by simp
qed
ultimately show "P(B)" by auto
qed
} thus ?thesis by blast
qed
ultimately have "∀B ∈ Pow(X). (B \<lesssim> n --> P(B))"
by (rule ind_on_nat)
} then have "∀n ∈ nat. ∀B ∈ Pow(X). (B \<lesssim> n --> P(B))"
by auto
with A3 show "P(B)" using finpow_union_card_nat
by auto
qed

text{*A subset of a finites subset is a finite subset.*}

lemma subset_finpow: assumes "A ∈ FinPow(X)" and "B ⊆ A"
shows "B ∈ FinPow(X)"
using assms FinPow_def subset_Finite by auto;

text{*If we subtract anything from a finite set,
the resulting set is finite.*}


lemma diff_finpow:
assumes "A ∈ FinPow(X)" shows "A-B ∈ FinPow(X)"
using assms subset_finpow by blast;

text{*If we remove a point from a finites subset,
we get a finite subset.*}


corollary fin_rem_point_fin: assumes "A ∈ FinPow(X)"
shows "A - {a} ∈ FinPow(X)"
using assms diff_finpow by simp;

text{*Cardinality of a nonempty finite set is a successsor
of some natural number.*}


lemma card_non_empty_succ:
assumes A1: "A ∈ FinPow(X)" and A2: "A ≠ 0"
shows "∃n ∈ nat. |A| = succ(n)"
proof -
from A2 obtain a where "a ∈ A" by auto;
let ?B = "A - {a}"
from A1 `a ∈ A` have
"?B ∈ FinPow(X)" and "a ∈ X - ?B"
using FinPow_def fin_rem_point_fin by auto;
then have "|?B ∪ {a}| = succ( |?B| )"
using card_fin_add_one by auto;
moreover from `a ∈ A` `?B ∈ FinPow(X)` have
"A = ?B ∪ {a}" and "|?B| ∈ nat"
using card_fin_is_nat by auto;
ultimately show "∃n ∈ nat. |A| = succ(n)" by auto;
qed;

text{*Nonempty set has non-zero cardinality. This is probably
true without the assumption that the set is finite, but
I couldn't derive it from standard Isabelle theorems.
*}


lemma card_non_empty_non_zero:
assumes "A ∈ FinPow(X)" and "A ≠ 0"
shows "|A| ≠ 0"
proof -
from assms obtain n where "|A| = succ(n)"
using card_non_empty_succ by auto;
then show "|A| ≠ 0" using succ_not_0
by simp;
qed;

text{*Another variation on the induction theme:
If we can show something holds for the empty set and
if it holds for all finite sets with
at most $k$ elements then it holds for all
finite sets with at most $k+1$
elements, the it holds for all finite sets.*}


theorem FinPow_card_ind: assumes A1: "P(0)" and
A2: "∀k∈nat.
(∀A ∈ FinPow(X). A \<lesssim> k --> P(A)) -->
(∀A ∈ FinPow(X). A \<lesssim> succ(k) --> P(A))"

and A3: "A ∈ FinPow(X)" shows "P(A)"
proof -
from A3 have "|A| ∈ nat" and "A ∈ FinPow(X)" and "A \<lesssim> |A|"
using card_fin_is_nat eqpoll_imp_lepoll by auto;
moreover have "∀n ∈ nat. (∀A ∈ FinPow(X).
A \<lesssim> n --> P(A))"

proof;
fix n assume "n ∈ nat"
moreover from A1 have "∀A ∈ FinPow(X). A \<lesssim> 0 --> P(A)"
using lepoll_0_is_0 by auto;
moreover note A2
ultimately show
"∀A ∈ FinPow(X). A \<lesssim> n --> P(A)"
by (rule ind_on_nat);
qed;
ultimately show "P(A)" by simp;
qed;

text{*Another type of induction (or, maybe recursion).
The induction step we try to find a point in the set that
if we remove it, the fact that the property holds for the
smaller set implies that the property holds for the whole set.
*}


lemma FinPow_ind_rem_one: assumes A1: "P(0)" and
A2: "∀ A ∈ FinPow(X). A ≠ 0 --> (∃a∈A. P(A-{a}) --> P(A))"
and A3: "B ∈ FinPow(X)"
shows "P(B)"
proof -
note A1
moreover have "∀k∈nat.
(∀B ∈ FinPow(X). B \<lesssim> k --> P(B)) -->
(∀C ∈ FinPow(X). C \<lesssim> succ(k) --> P(C))"

proof -
{ fix k assume "k ∈ nat"
assume A4: "∀B ∈ FinPow(X). B \<lesssim> k --> P(B)"
have "∀C ∈ FinPow(X). C \<lesssim> succ(k) --> P(C)"
proof -
{ fix C assume "C ∈ FinPow(X)"
assume "C \<lesssim> succ(k)"
note A1
moreover
{ assume "C ≠ 0"
with A2 `C ∈ FinPow(X)` obtain a where
"a∈C" and "P(C-{a}) --> P(C)"
by auto;
with A4 `C ∈ FinPow(X)` `C \<lesssim> succ(k)`
have "P(C)" using Diff_sing_lepoll fin_rem_point_fin
by simp }
ultimately have "P(C)" by auto
} thus ?thesis by simp;
qed;
} thus ?thesis by blast;
qed;
moreover note A3
ultimately show "P(B)" by (rule FinPow_card_ind)
qed;

text{* Yet another induction theorem. This is similar, but
slightly more complicated than @{text "FinPow_ind_rem_one"}.
The difference is in the treatment of the empty set to allow
to show properties that are not true for empty set.
*}


lemma FinPow_rem_ind: assumes A1: "∀A ∈ FinPow(X).
A = 0 ∨ (∃a∈A. A = {a} ∨ P(A-{a}) --> P(A))"

and A2: "A ∈ FinPow(X)" and A3: "A≠0"
shows "P(A)"
proof -
have "0 = 0 ∨ P(0)" by simp;
moreover have
"∀k∈nat.
(∀B ∈ FinPow(X). B \<lesssim> k --> (B=0 ∨ P(B))) -->
(∀A ∈ FinPow(X). A \<lesssim> succ(k) --> (A=0 ∨ P(A)))"

proof -
{ fix k assume "k ∈ nat"
assume A4: "∀B ∈ FinPow(X). B \<lesssim> k --> (B=0 ∨ P(B))"
have "∀A ∈ FinPow(X). A \<lesssim> succ(k) --> (A=0 ∨ P(A))"
proof -
{ fix A assume "A ∈ FinPow(X)"
assume "A \<lesssim> succ(k)" "A≠0"
from A1 `A ∈ FinPow(X)` `A≠0` obtain a
where "a∈A" and "A = {a} ∨ P(A-{a}) --> P(A)"
by auto;
let ?B = "A-{a}"
from A4 `A ∈ FinPow(X)` `A \<lesssim> succ(k)` `a∈A`
have "?B = 0 ∨ P(?B)"
using Diff_sing_lepoll fin_rem_point_fin
by simp;
with `a∈A` `A = {a} ∨ P(A-{a}) --> P(A)`
have "P(A)" by auto;
} thus ?thesis by auto;
qed;
} thus ?thesis by blast
qed;
moreover note A2
ultimately have "A=0 ∨ P(A)" by (rule FinPow_card_ind);
with A3 show "P(A)" by simp;
qed;

text{*If a family of sets is closed with respect to taking intersections
of two sets then it is closed with respect to taking intersections
of any nonempty finite collection.*}


lemma inter_two_inter_fin:
assumes A1: "∀V∈T. ∀W∈T. V ∩ W ∈ T" and
A2: "N ≠ 0" and A3: "N ∈ FinPow(T)"
shows "(\<Inter>N ∈ T)"
proof -
have "0 = 0 ∨ (\<Inter>0 ∈ T)" by simp
moreover have "∀M ∈ FinPow(T). (M = 0 ∨ \<Inter>M ∈ T) -->
(∀W ∈ T. M∪{W} = 0 ∨ \<Inter>(M ∪ {W}) ∈ T)"

proof -
{ fix M assume "M ∈ FinPow(T)"
assume A4: "M = 0 ∨ \<Inter>M ∈ T"
{ assume "M = 0"
hence "∀W ∈ T. M∪{W} = 0 ∨ \<Inter>(M ∪ {W}) ∈ T"
by auto }
moreover
{ assume "M ≠ 0"
with A4 have "\<Inter>M ∈ T" by simp
{ fix W assume "W ∈ T"
from `M ≠ 0` have "\<Inter>(M ∪ {W}) = (\<Inter>M) ∩ W"
by auto
with A1 `\<Inter>M ∈ T` `W ∈ T` have "\<Inter>(M ∪ {W}) ∈ T"
by simp
} hence "∀W ∈ T. M∪{W} = 0 ∨ \<Inter>(M ∪ {W}) ∈ T"
by simp }
ultimately have "∀W ∈ T. M∪{W} = 0 ∨ \<Inter>(M ∪ {W}) ∈ T"
by blast
} thus ?thesis by simp
qed
moreover note `N ∈ FinPow(T)`
ultimately have "N = 0 ∨ (\<Inter>N ∈ T)"
by (rule FinPow_induct)
with A2 show "(\<Inter>N ∈ T)" by simp
qed

text{*If a family of sets contains the empty set and
is closed with respect to taking unions
of two sets then it is closed with respect to taking unions
of any finite collection.*}


lemma union_two_union_fin:
assumes A1: "0 ∈ C" and A2: "∀A∈C. ∀B∈C. A∪B ∈ C" and
A3: "N ∈ FinPow(C)"
shows "\<Union>N ∈ C"
proof -
from `0 ∈ C` have "\<Union>0 ∈ C" by simp
moreover have "∀M ∈ FinPow(C). \<Union>M ∈ C --> (∀A∈C. \<Union>(M ∪ {A}) ∈ C)"
proof -
{ fix M assume "M ∈ FinPow(C)"
assume "\<Union>M ∈ C"
fix A assume "A∈C"
have "\<Union>(M ∪ {A}) = (\<Union>M) ∪ A" by auto
with A2 `\<Union>M ∈ C` `A∈C` have "\<Union>(M ∪ {A}) ∈ C"
by simp
} thus ?thesis by simp
qed
moreover note `N ∈ FinPow(C)`
ultimately show "\<Union>N ∈ C" by (rule FinPow_induct)
qed

text{*Empty set is in finite power set.*}

lemma empty_in_finpow: shows "0 ∈ FinPow(X)"
using FinPow_def by simp

text{*Singleton is in the finite powerset.*}

lemma singleton_in_finpow: assumes "x ∈ X"
shows "{x} ∈ FinPow(X)" using assms FinPow_def by simp

text{*Union of two finite subsets is a finite subset.*}

lemma union_finpow: assumes "A ∈ FinPow(X)" and "B ∈ FinPow(X)"
shows "A ∪ B ∈ FinPow(X)"
using assms FinPow_def by auto

text{*Union of finite number of finite sets is finite.*}

lemma fin_union_finpow: assumes "M ∈ FinPow(FinPow(X))"
shows "\<Union>M ∈ FinPow(X)"
using assms empty_in_finpow union_finpow union_two_union_fin
by simp;

(*text{*A subset of a finites subset is a finite subset.*}

lemma subset_finpow: assumes "A ∈ FinPow(X)" and "B ⊆ A"
shows "B ∈ FinPow(X)"
using assms FinPow_def subset_Finite by auto;*)

text{*If a set is finite after removing one element, then it is finite.*}

lemma rem_point_fin_fin:
assumes A1: "x ∈ X" and A2: "A - {x} ∈ FinPow(X)"
shows "A ∈ FinPow(X)"
proof -
from assms have "(A - {x}) ∪ {x} ∈ FinPow(X)"
using singleton_in_finpow union_finpow by simp;
moreover have "A ⊆ (A - {x}) ∪ {x}" by auto;
ultimately show "A ∈ FinPow(X)"
using FinPow_def subset_Finite by auto;
qed;

text{*An image of a finite set is finite.*}

lemma fin_image_fin: assumes "∀V∈B. K(V)∈C" and "N ∈ FinPow(B)"
shows "{K(V). V∈N} ∈ FinPow(C)"
proof -
have "{K(V). V∈0} ∈ FinPow(C)" using FinPow_def
by auto
moreover have "∀A ∈ FinPow(B).
{K(V). V∈A} ∈ FinPow(C) --> (∀a∈B. {K(V). V ∈ (A ∪ {a})} ∈ FinPow(C))"

proof -
{ fix A assume "A ∈ FinPow(B)"
assume "{K(V). V∈A} ∈ FinPow(C)"
fix a assume "a∈B"
have "{K(V). V ∈ (A ∪ {a})} ∈ FinPow(C)"
proof -
have "{K(V). V ∈ (A ∪ {a})} = {K(V). V∈A} ∪ {K(a)}"
by auto
moreover note `{K(V). V∈A} ∈ FinPow(C)`
moreover from `∀V∈B. K(V) ∈ C` `a∈B` have "{K(a)} ∈ FinPow(C)"
using singleton_in_finpow by simp
ultimately show ?thesis using union_finpow by simp
qed
} thus ?thesis by simp
qed
moreover note `N ∈ FinPow(B)`
ultimately show "{K(V). V∈N} ∈ FinPow(C)"
by (rule FinPow_induct)
qed

text{*Union of a finite indexed family of finite sets is finite.*}

lemma union_fin_list_fin:
assumes A1: "n ∈ nat" and A2: "∀k ∈ n. N(k) ∈ FinPow(X)"
shows
"{N(k). k ∈ n} ∈ FinPow(FinPow(X))" and "(\<Union>k ∈ n. N(k)) ∈ FinPow(X)"
proof -;
from A1 have "n ∈ FinPow(n)"
using nat_finpow_nat fin_finpow_self by auto
with A2 show "{N(k). k ∈ n} ∈ FinPow(FinPow(X))"
by (rule fin_image_fin);
then show "(\<Union>k ∈ n. N(k)) ∈ FinPow(X)"
using fin_union_finpow by simp;
qed;

end