Theory Partitions_ZF

theory Partitions_ZF
imports Finite_ZF FiniteSeq_ZF
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written 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{Partitions\_ZF.thy}*}

theory Partitions_ZF imports Finite_ZF FiniteSeq_ZF

begin

text{*It is a common trick in proofs that we divide a set into non-overlapping
  subsets. The first case is when we split the set into 
  two nonempty disjoint sets. Here this is modeled as an ordered pair of sets
  and the set of such divisions of set $X$ is called @{text "Bisections(X)"}.
  The second variation on this theme is a set-valued function (aren't they all
  in ZF?) whose values are nonempty and mutually disjoint.
  *}

section{*Bisections*}

text{*This section is about dividing sets into two non-overlapping subsets.
  *}

text{*The set of bisections of a given set $A$ is a set of pairs of nonempty
  subsets of $A$ that do not overlap and their union is equal to $A$.*}

definition
  "Bisections(X) = {p ∈ Pow(X)×Pow(X). 
  fst(p)≠0 ∧ snd(p)≠0 ∧ fst(p)∩snd(p) = 0 ∧ fst(p)∪snd(p) = X}"

text{*Properties of bisections.*}

lemma bisec_props: assumes "⟨A,B⟩ ∈ Bisections(X)" shows
  "A≠0"  "B≠0" "A ⊆ X"  "B ⊆ X"  "A ∩ B = 0"  "A ∪ B = X"  "X ≠ 0"
  using assms Bisections_def by auto;

text{*Kind of inverse of @{text "bisec_props"}: a pair of nonempty
  disjoint sets form a bisection of their union.*}

lemma is_bisec: 
  assumes "A≠0"  "B≠0"  "A ∩ B = 0" 
  shows "⟨A,B⟩ ∈ Bisections(A∪B)" using assms Bisections_def
  by auto;


text{*Bisection of $X$ is a pair of subsets of $X$.*}

lemma bisec_is_pair: assumes "Q ∈ Bisections(X)"
  shows "Q = ⟨fst(Q), snd(Q)⟩"
  using assms Bisections_def by auto;

text{*The set of bisections of the empty set is empty.*}

lemma bisec_empty: shows "Bisections(0) = 0"
  using Bisections_def by auto;

text{*The next lemma shows what can we say about bisections of a set
  with another element added.*}

lemma bisec_add_point: 
  assumes A1: "x ∉ X" and A2: "⟨A,B⟩ ∈ Bisections(X ∪ {x})"
  shows "(A = {x} ∨ B = {x}) ∨ (⟨A - {x}, B - {x}⟩ ∈ Bisections(X))"
  proof -
    { assume "A ≠ {x}" and "B ≠ {x}"
      with A2 have "A - {x} ≠ 0" and "B - {x} ≠ 0"
	using singl_diff_empty Bisections_def
	by auto;
      moreover have "(A - {x}) ∪ (B - {x}) = X"
      proof -
	have "(A - {x}) ∪ (B - {x}) = (A ∪ B) - {x}"
	  by auto;
	also from assms have "(A ∪ B) - {x} = X"
	  using Bisections_def by auto;
	finally show ?thesis by simp;
      qed;
      moreover from A2 have "(A - {x}) ∩ (B - {x}) = 0"
	using Bisections_def by auto;
      ultimately have "⟨A - {x}, B - {x}⟩ ∈ Bisections(X)"
	using Bisections_def by auto;
    } thus ?thesis by auto;
qed;

text{*A continuation of the lemma @{text "bisec_add_point"}
  that refines the case when the pair with removed point bisects
  the original set.*}

lemma bisec_add_point_case3: 
  assumes A1: "⟨A,B⟩ ∈ Bisections(X ∪ {x})"
  and A2: "⟨A - {x}, B - {x}⟩ ∈ Bisections(X)"
  shows 
  "(⟨A, B - {x}⟩ ∈ Bisections(X) ∧ x ∈ B) ∨ 
  (⟨A - {x}, B⟩ ∈ Bisections(X) ∧ x ∈ A)"
proof -
  from A1 have "x ∈ A ∪ B"
    using Bisections_def by auto;
  hence "x∈A ∨ x∈B" by simp;
  from A1 have "A - {x} = A ∨ B - {x} = B"
    using Bisections_def by auto;
  moreover
  { assume "A - {x} = A"
    with A2 `x ∈ A ∪ B` have 
      "⟨A, B - {x}⟩ ∈ Bisections(X) ∧ x ∈ B" 
      using singl_diff_eq by simp }
  moreover
  { assume "B - {x} = B"
    with A2 `x ∈ A ∪ B` have 
      "⟨A - {x}, B⟩ ∈ Bisections(X) ∧ x ∈ A"
      using singl_diff_eq by simp }
  ultimately show ?thesis by auto;
qed;

text{*Another lemma about bisecting a set with an added point.*}

lemma point_set_bisec: 
  assumes A1: "x ∉ X" and A2: "⟨{x}, A⟩ ∈ Bisections(X ∪ {x})"
  shows "A = X" and "X ≠ 0"
proof -
  from A2 have "A ⊆ X" using Bisections_def by auto;
  moreover
  { fix a assume "a∈X"
    with A2 have "a ∈ {x} ∪ A" using Bisections_def by simp;
    with A1 `a∈X` have "a ∈ A" by auto }
  ultimately show "A = X" by auto;
  with A2 show "X ≠ 0" using Bisections_def by simp;
qed;

text{*Yet another lemma about bisecting a set with an added point,
  very similar to @{text " point_set_bisec"} with almost the same proof.*}

lemma set_point_bisec: 
  assumes A1: "x ∉ X" and A2: "⟨A, {x}⟩ ∈ Bisections(X ∪ {x})"
  shows "A = X" and "X ≠ 0"
proof -
  from A2 have "A ⊆ X" using Bisections_def by auto;
  moreover
  { fix a assume "a∈X"
    with A2 have "a ∈ A ∪ {x}" using Bisections_def by simp;
    with A1 `a∈X` have "a ∈ A" by auto }
  ultimately show "A = X" by auto;
  with A2 show "X ≠ 0" using Bisections_def by simp;
qed

text{*If a pair of sets bisects a finite set, then both 
  elements of the pair are finite.*}

lemma bisect_fin: 
  assumes A1: "A ∈ FinPow(X)" and A2: "Q ∈ Bisections(A)"
  shows "fst(Q) ∈ FinPow(X)" and "snd(Q) ∈ FinPow(X)"
proof -
  from A2 have "⟨fst(Q), snd(Q)⟩ ∈ Bisections(A)"
    using bisec_is_pair by simp;
  then have "fst(Q) ⊆ A" and "snd(Q) ⊆ A"
    using bisec_props by auto;
  with A1 show "fst(Q) ∈ FinPow(X)" and "snd(Q) ∈ FinPow(X)"
    using FinPow_def subset_Finite by auto;
qed

section{*Partitions*}

text{*This sections covers the situation when we have an arbitrary number
  of sets we want to partition into.*}

text{*We define a notion of a partition as a set valued function 
  such that the values for different arguments are disjoint.
  The name is derived from the fact that such 
  function "partitions" the union of its arguments. 
  Please let me know if you have 
  a better idea for a name for such notion. We would prefer to say
 ''is a partition'', but that reserves the letter ''a'' as a keyword(?)
  which causes problems. *}

definition
  Partition ("_ {is partition}" [90] 91) where
  "P {is partition} ≡  ∀x ∈ domain(P). 
  P`(x) ≠ 0 ∧ (∀y ∈ domain(P). x≠y --> P`(x) ∩ P`(y) = 0)"

text{*A fact about lists of mutually disjoint sets.*}

lemma list_partition: assumes A1: "n ∈ nat" and 
  A2: "a : succ(n) -> X"   "a {is partition}"
  shows "(\<Union>i∈n. a`(i)) ∩ a`(n) = 0"
proof -
  { assume "(\<Union>i∈n. a`(i)) ∩ a`(n) ≠ 0"
    then have "∃x. x ∈ (\<Union>i∈n. a`(i)) ∩ a`(n)"
      by (rule nonempty_has_element);
    then obtain x where "x ∈ (\<Union>i∈n. a`(i))" and  I: "x ∈ a`(n)"
      by auto;
    then obtain i where "i ∈ n" and "x ∈ a`(i)" by auto;
    with A2 I have False 
      using mem_imp_not_eq func1_1_L1 Partition_def
      by auto;
  } thus ?thesis by auto;
qed;

text{*We can turn every injection into a partition.*}

lemma inj_partition: 
  assumes A1: "b ∈ inj(X,Y)" 
  shows 
  "∀x ∈ X. {⟨x, {b`(x)}⟩. x ∈ X}`(x) = {b`(x)}" and
  "{⟨x, {b`(x)}⟩. x ∈ X} {is partition}"
proof -
  let ?p = "{⟨x, {b`(x)}⟩. x ∈ X}"
  { fix x assume "x ∈ X"
    from A1 have "b : X -> Y" using inj_def
      by simp;
    with `x ∈ X` have "{b`(x)} ∈ Pow(Y)"
       using apply_funtype by simp;
  } hence "∀x ∈ X. {b`(x)} ∈ Pow(Y)" by simp;
  then have "?p : X -> Pow(Y)" using ZF_fun_from_total 
    by simp;
  then have "domain(?p) = X" using func1_1_L1
    by simp;
  from `?p : X -> Pow(Y)` show I: "∀x ∈ X. ?p`(x) = {b`(x)}"
    using ZF_fun_from_tot_val0 by simp;
  { fix x assume "x ∈ X"
    with I have "?p`(x) = {b`(x)}" by simp
    hence "?p`(x) ≠ 0" by simp;
    moreover
    { fix t assume "t ∈ X" and "x ≠ t"
      with A1 `x ∈ X` have "b`(x) ≠ b`(t)" using inj_def 
	by auto;
      with I `x∈X` `t ∈ X` have "?p`(x) ∩ ?p`(t) = 0"
	by auto }
    ultimately have 
      "?p`(x) ≠ 0 ∧ (∀t ∈ X. x≠t --> ?p`(x) ∩ ?p`(t) = 0)"
      by simp;
  } with `domain(?p) = X` show "{⟨x, {b`(x)}⟩. x ∈ X} {is partition}"
    using Partition_def by simp;
qed;
      
  
    

end