Theory Finite_ZF_1

(*
    This file is a part of IsarMathLib - 
    a library of formalized mathematics 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{Finite\_ZF.thy}*}

theory Finite_ZF_1 imports Finite1 Order_ZF 

begin

text{*This theory file contains properties of finite sets related to order 
  relations.*}

section{*Finite vs. bounded sets*}

text{*The goal of this section is to show that finite sets are bounded and 
  have maxima and minima.*}

text{*Finite set has a maximum - induction step.*}

lemma Finite_ZF_1_1_L1: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "A∈Fin(X)" and A4: "x∈X" and A5: "A=0 ∨ HasAmaximum(r,A)"
  shows "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})"
proof (cases "A=0");
  assume "A=0" then have T1: "A∪{x} = {x}" by simp;
  from A1 have "refl(X,r)" using total_is_refl by simp;
  with T1 A4 show "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})" 
    using Order_ZF_4_L8 by simp;
next assume "A≠0" 
  with A1 A2 A3 A4 A5 show "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})" 
    using FinD Order_ZF_4_L9 by simp;
qed;

text{*For total and transitive relations finite set has a maximum.*}

theorem Finite_ZF_1_1_T1A: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "B∈Fin(X)"
  shows "B=0 ∨ HasAmaximum(r,B)"
proof -
  have "0=0 ∨ HasAmaximum(r,0)" by simp;
  moreover from A3 have "B∈Fin(X)" .;
  moreover from A1 A2 have "∀A∈Fin(X). ∀x∈X. 
    x∉A ∧ (A=0 ∨ HasAmaximum(r,A)) --> (A∪{x}=0 ∨ HasAmaximum(r,A∪{x}))"
    using Finite_ZF_1_1_L1 by simp;
  ultimately show  "B=0 ∨ HasAmaximum(r,B)" by (rule Finite1_L16B);
qed;

text{*Finite set has a minimum - induction step.*}

lemma Finite_ZF_1_1_L2: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "A∈Fin(X)" and A4: "x∈X" and A5: "A=0 ∨ HasAminimum(r,A)"
  shows "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})"
proof (cases "A=0");
  assume "A=0" then have T1: "A∪{x} = {x}" by simp;
  from A1 have "refl(X,r)" using total_is_refl by simp;
  with T1 A4 show "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})" 
    using Order_ZF_4_L8 by simp;
next assume "A≠0" 
  with A1 A2 A3 A4 A5 show "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})" 
    using FinD Order_ZF_4_L10 by simp;
qed;

text{*For total and transitive relations finite set has a minimum.*}

theorem Finite_ZF_1_1_T1B: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "B ∈ Fin(X)"
  shows "B=0 ∨ HasAminimum(r,B)"
proof -
  have "0=0 ∨ HasAminimum(r,0)" by simp;
  moreover from A3 have "B∈Fin(X)" .;
  moreover from A1 A2 have "∀A∈Fin(X). ∀x∈X. 
    x∉A ∧ (A=0 ∨ HasAminimum(r,A)) --> (A∪{x}=0 ∨ HasAminimum(r,A∪{x}))"
    using Finite_ZF_1_1_L2 by simp;
  ultimately show  "B=0 ∨ HasAminimum(r,B)" by (rule Finite1_L16B);
qed

text{*For transitive and total relations finite sets are bounded.*}

theorem Finite_ZF_1_T1: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"  
  and A3: "B∈Fin(X)"
  shows "IsBounded(B,r)"
proof -;
  from A1 A2 A3 have "B=0 ∨ HasAminimum(r,B)" "B=0 ∨ HasAmaximum(r,B)"
    using Finite_ZF_1_1_T1A Finite_ZF_1_1_T1B by auto;
  then have 
    "B = 0 ∨ IsBoundedBelow(B,r)" "B = 0 ∨ IsBoundedAbove(B,r)"
    using Order_ZF_4_L7 Order_ZF_4_L8A by auto;
  then show "IsBounded(B,r)" using 
    IsBounded_def IsBoundedBelow_def IsBoundedAbove_def
    by simp;
qed;

text{*For linearly ordered finite sets maximum and minimum have desired 
  properties. The reason we need linear order is that we need the order
  to be total and transitive for the finite sets to have a maximum and minimum
  and then we also need antisymmetry for the maximum and minimum to be unique.
  *}

theorem Finite_ZF_1_T2:
  assumes A1: "IsLinOrder(X,r)" and A2: "A ∈ Fin(X)" and A3: "A≠0"
  shows 
  "Maximum(r,A) ∈ A" 
  "Minimum(r,A) ∈ A"
  "∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r" 
  "∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"
proof -;
  from A1 have T1: "r {is total on} X" "trans(r)" "antisym(r)"
    using IsLinOrder_def by auto;
  moreover from T1 A2 A3 have "HasAmaximum(r,A)" 
    using Finite_ZF_1_1_T1A by auto;
  moreover from T1 A2 A3 have "HasAminimum(r,A)"
    using Finite_ZF_1_1_T1B by auto
  ultimately show 
    "Maximum(r,A) ∈ A" 
    "Minimum(r,A) ∈ A"
    "∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r" "∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"
    using Order_ZF_4_L3 Order_ZF_4_L4 by auto;
qed;

text{*A special case of @{text "Finite_ZF_1_T2"} when the set has three
  elements.*}

corollary Finite_ZF_1_L2A: 
  assumes A1: "IsLinOrder(X,r)" and A2: "a∈X"  "b∈X"  "c∈X"
  shows 
  "Maximum(r,{a,b,c}) ∈ {a,b,c}" 
  "Minimum(r,{a,b,c}) ∈ {a,b,c}"
  "Maximum(r,{a,b,c}) ∈ X" 
  "Minimum(r,{a,b,c}) ∈ X"
  "⟨a,Maximum(r,{a,b,c})⟩ ∈ r"
  "⟨b,Maximum(r,{a,b,c})⟩ ∈ r"
  "⟨c,Maximum(r,{a,b,c})⟩ ∈ r"
proof -
  from A2 have I: "{a,b,c} ∈ Fin(X)"  "{a,b,c} ≠ 0"
    by auto;
  with A1 show II: "Maximum(r,{a,b,c}) ∈ {a,b,c}" 
    by (rule Finite_ZF_1_T2);
  moreover from A1 I show III: "Minimum(r,{a,b,c}) ∈ {a,b,c}"
    by (rule Finite_ZF_1_T2);
  moreover from A2 have "{a,b,c} ⊆ X"
    by auto;
  ultimately show  
    "Maximum(r,{a,b,c}) ∈ X" 
    "Minimum(r,{a,b,c}) ∈ X"
    by auto;
  from A1 I have "∀x∈{a,b,c}. ⟨x,Maximum(r,{a,b,c})⟩ ∈ r"
    by (rule Finite_ZF_1_T2);
  then show 
    "⟨a,Maximum(r,{a,b,c})⟩ ∈ r"
    "⟨b,Maximum(r,{a,b,c})⟩ ∈ r"
    "⟨c,Maximum(r,{a,b,c})⟩ ∈ r"
    by auto;
qed;


text{*If for every element of $X$ we can find one in $A$ 
  that is greater, then the $A$ can not be finite. Works for relations
  that are total, transitive and antisymmetric.*}

lemma Finite_ZF_1_1_L3: 
  assumes A1: "r {is total on} X" 
  and A2: "trans(r)" and A3: "antisym(r)"
  and A4: "r ⊆ X×X" and A5: "X≠0" 
  and A6: "∀x∈X. ∃a∈A. x≠a ∧ ⟨x,a⟩ ∈ r"
  shows "A ∉ Fin(X)"
proof -
  from prems have "¬IsBounded(A,r)"
    using Order_ZF_3_L14 IsBounded_def
    by simp;
  with A1 A2 show "A ∉ Fin(X)"
    using Finite_ZF_1_T1 by auto;
qed;

end;