Theory FinOrd_ZF

(*
    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.

*)

section ‹Finite sets and order relations›

theory FinOrd_ZF imports Finite_ZF func_ZF_1

begin

text‹This theory file contains properties of finite sets related to order 
  relations. Part of this is similar to what is done in ‹Finite_ZF_1›
  except that the development is based on the notion of finite powerset
  defined in ‹Finite_ZF› rather the one defined in standard
  Isabelle ‹Finite› theory.›

subsection‹Finite vs. bounded sets›

text‹The goal of this section is to show that finite sets are bounded and 
  have maxima and minima.›

text‹For total and transitive relations 
  nonempty finite set has a maximum.›

theorem fin_has_max: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "B ∈ FinPow(X)" and A4: "B ≠ 0"
  shows "HasAmaximum(r,B)"
proof -
  have "0=0 ∨ HasAmaximum(r,0)" by simp
  moreover have 
    "∀A ∈ FinPow(X). A=0 ∨ HasAmaximum(r,A) ⟶
    (∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x}))"
  proof -
    { fix A 
      assume "A ∈ FinPow(X)"  "A = 0 ∨ HasAmaximum(r,A)"
      have "∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x})"
      proof -
	{ fix x assume "x∈X"
	  note ‹A = 0 ∨ HasAmaximum(r,A)›
	  moreover
	  { assume "A = 0"
	    then have "A∪{x} = {x}" by simp
	    from A1 have "refl(X,r)" using total_is_refl 
	      by simp
	    with ‹x∈X› ‹A∪{x} = {x}› have "HasAmaximum(r,A∪{x})"
	      using Order_ZF_4_L8 by simp }
	  moreover
	  { assume "HasAmaximum(r,A)"
	    with A1 A2 ‹A ∈ FinPow(X)›  ‹x∈X› 
	    have "HasAmaximum(r,A∪{x})" 
	      using FinPow_def Order_ZF_4_L9 by simp }
	  ultimately  have "A ∪ {x} = 0 ∨ HasAmaximum(r,A ∪ {x})"
	    by auto
	} thus "∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x})"
	  by simp
      qed
    } thus ?thesis by simp
  qed
  moreover note A3
  ultimately have "B = 0 ∨  HasAmaximum(r,B)"
    by (rule FinPow_induct)
  with A4 show "HasAmaximum(r,B)" by simp
qed

text‹For linearly ordered nonempty finite sets the 
  maximum is in the set and indeed it is the greatest
  element of the set.›

lemma linord_max_props: assumes A1: "IsLinOrder(X,r)" and
  A2: "A ∈ FinPow(X)" "A ≠ 0"
  shows
  "Maximum(r,A) ∈ A"
  "Maximum(r,A) ∈ X"
  "∀a∈A. ⟨a,Maximum(r,A)⟩ ∈ r"
proof -
  from A1 A2 show 
    "Maximum(r,A) ∈ A" and "∀a∈A. ⟨a,Maximum(r,A)⟩ ∈ r"
    using IsLinOrder_def fin_has_max Order_ZF_4_L3
    by auto
  with A2 show "Maximum(r,A) ∈ X" using FinPow_def
    by auto
qed
  
subsection‹Order isomorphisms of finite sets›

text‹In this section we eastablish that if two linearly 
  ordered finite sets have the same number of elements,
  then they are order-isomorphic and the isomorphism
  is unique. This allows us to talk about ''enumeration''
  of a linearly ordered finite set. We define the enumeration as 
  the order isomorphism between the number of elements
  of the set (which is a natural number $n = \{0,1,..,n-1\}$)
  and the set.›

text‹A really weird corner case - empty set is order isomorphic with itself.
›

lemma empty_ord_iso: shows "ord_iso(0,r,0,R) ≠ 0"
proof -
  have "0 ≈ 0" using eqpoll_refl by simp
  then obtain f where "f ∈ bij(0,0)"
    using eqpoll_def by blast
  then show ?thesis using ord_iso_def by auto
qed

text‹Even weirder than ‹empty_ord_iso›
  The order automorphism of the empty set is unique.›

lemma empty_ord_iso_uniq: 
  assumes "f ∈ ord_iso(0,r,0,R)"  "g ∈ ord_iso(0,r,0,R)"
  shows "f = g"
proof -
  from assms have "f : 0 → 0" and "g: 0 → 0"
    using ord_iso_def bij_def surj_def by auto
    moreover have "∀x∈0. f`(x) = g`(x)" by simp
    ultimately show "f = g" by (rule func_eq)
qed

text‹The empty set is the only order automorphism of itself.›

lemma empty_ord_iso_empty: shows "ord_iso(0,r,0,R) = {0}"
proof -
  have "0 ∈ ord_iso(0,r,0,R)"
  proof -
    have "ord_iso(0,r,0,R) ≠ 0" by (rule empty_ord_iso)
    then obtain f where "f ∈ ord_iso(0,r,0,R)" by auto
    then show "0 ∈ ord_iso(0,r,0,R)" 
      using ord_iso_def bij_def surj_def fun_subset_prod
      by auto
  qed
  then show "ord_iso(0,r,0,R) = {0}" using empty_ord_iso_uniq
    by blast
qed

text‹An induction (or maybe recursion?) scheme for linearly ordered sets.
  The induction step is that we show that if the property holds
  when the set is a singleton or for a set with the maximum removed, 
  then it holds for the set. The idea is that since we can build
  any finite set by adding elements on the right, then if the property
  holds for the empty set and is invariant with respect to this operation, then
  it must hold for all finite sets.›

lemma fin_ord_induction:  
  assumes A1: "IsLinOrder(X,r)" and A2: "P(0)" and
  A3: "∀A ∈ FinPow(X). A ≠ 0 ⟶ (P(A - {Maximum(r,A)}) ⟶ P(A))"
  and A4: "B ∈ FinPow(X)" shows "P(B)"
proof -
  note A2
  moreover have "∀ A ∈ FinPow(X). A ≠ 0 ⟶ (∃a∈A. P(A-{a}) ⟶ P(A))"
  proof -
    { fix A assume "A ∈  FinPow(X)" and "A ≠ 0"
      with A1 A3 have "∃a∈A. P(A-{a}) ⟶ P(A)"
	using IsLinOrder_def fin_has_max
	  IsLinOrder_def Order_ZF_4_L3
	by blast
    } thus ?thesis by simp
  qed
  moreover note A4
  ultimately show "P(B)" by (rule FinPow_ind_rem_one)
qed

text‹A sligltly more complicated version of ‹fin_ord_induction›
  that allows to prove properties that are not true for the empty set.›

lemma fin_ord_ind:  
  assumes A1: "IsLinOrder(X,r)" and A2: "∀A ∈ FinPow(X). 
  A = 0 ∨ (A = {Maximum(r,A)} ∨ P(A - {Maximum(r,A)}) ⟶ P(A))"
  and A3: "B ∈  FinPow(X)" and A4: "B≠0"
  shows "P(B)"
proof -
  { fix A assume "A ∈  FinPow(X)" and "A ≠ 0"
    with A1 A2 have
      "∃a∈A. A = {a} ∨ P(A-{a}) ⟶ P(A)"
      using IsLinOrder_def fin_has_max
	IsLinOrder_def Order_ZF_4_L3
      by blast
  } then have "∀A ∈ FinPow(X). 
      A = 0 ∨ (∃a∈A. A = {a} ∨ P(A-{a}) ⟶ P(A))"
    by auto
  with A3 A4 show "P(B)" using  FinPow_rem_ind
    by simp
qed

text‹Yet another induction scheme. We build a linearly ordered
  set by adding elements that are greater than all elements in the
  set.›

lemma fin_ind_add_max: 
  assumes A1: "IsLinOrder(X,r)" and A2: "P(0)" and A3: "∀ A ∈ FinPow(X). 
  ( ∀ x ∈ X-A. P(A) ∧ (∀a∈A. ⟨a,x⟩ ∈ r ) ⟶ P(A ∪ {x}))"
  and A4: "B ∈ FinPow(X)"
  shows "P(B)"
proof -
  note A1 A2
  moreover have
    "∀C ∈ FinPow(X). C ≠ 0 ⟶ (P(C - {Maximum(r,C)}) ⟶ P(C))"
    proof -
      { fix C assume "C ∈ FinPow(X)" and "C ≠ 0"
	let ?x = "Maximum(r,C)"
	let ?A = "C - {?x}"
	assume "P(?A)"
	moreover from ‹C ∈ FinPow(X)› have "?A ∈ FinPow(X)"
	  using fin_rem_point_fin by simp
	moreover from A1 ‹C ∈ FinPow(X)› ‹C ≠ 0› have 
	  "?x ∈ C" and "?x ∈ X - ?A" and "∀a∈?A. ⟨a,?x⟩ ∈ r"
	  using linord_max_props by auto
	moreover note A3
	ultimately have "P(?A ∪ {?x})" by auto
	moreover from ‹?x ∈ C› have "?A ∪ {?x} = C"
	  by auto
	ultimately have "P(C)" by simp
      } thus ?thesis by simp
    qed
    moreover note A4
  ultimately show "P(B)" by (rule fin_ord_induction)
qed

text‹The only order automorphism of a linearly ordered
  finite set is the identity.›

theorem fin_ord_auto_id: assumes A1: "IsLinOrder(X,r)"
  and A2: "B ∈  FinPow(X)" and A3: "B≠0"
  shows "ord_iso(B,r,B,r) = {id(B)}"
proof -
  note A1
  moreover
  { fix A assume "A ∈  FinPow(X)" "A≠0"
    let ?M = "Maximum(r,A)"
    let ?A⇩0 = "A - {?M}"
    assume "A = {?M} ∨ ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}"
    moreover
    { assume "A = {?M}"
      have "ord_iso({?M},r,{?M},r) = {id({?M})}"
	using id_ord_auto_singleton by simp
      with ‹A = {?M}› have "ord_iso(A,r,A,r) = {id(A)}"
	by simp }
    moreover
    { assume "ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}"
      have "ord_iso(A,r,A,r) = {id(A)}"
      proof
	show "{id(A)} ⊆ ord_iso(A,r,A,r)"
	  using id_ord_iso by simp
	{ fix f assume "f ∈ ord_iso(A,r,A,r)"
	  with A1 ‹A ∈  FinPow(X)› ‹A≠0› have 
	    "restrict(f,?A⇩0) ∈ ord_iso(?A⇩0, r, A-{f`(?M)},r)"
	    using IsLinOrder_def fin_has_max ord_iso_rem_max 
	    by auto
	  with A1 ‹A ∈  FinPow(X)› ‹A≠0› ‹f ∈ ord_iso(A,r,A,r)›
	    ‹ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}›
	  have "restrict(f,?A⇩0) = id(?A⇩0)"
	    using IsLinOrder_def fin_has_max max_auto_fixpoint 
	    by auto
	  moreover from A1 ‹f ∈ ord_iso(A,r,A,r)› 
	    ‹A ∈  FinPow(X)› ‹A≠0› have
	    "f : A → A" and "?M ∈ A" and "f`(?M) = ?M"
	    using ord_iso_def bij_is_fun IsLinOrder_def 
	      fin_has_max Order_ZF_4_L3 max_auto_fixpoint
	    by auto
	  ultimately have "f = id(A)" using id_fixpoint_rem
	    by simp 
	} then show "ord_iso(A,r,A,r) ⊆ {id(A)}"
	  by auto
      qed
    }
    ultimately have "ord_iso(A,r,A,r) = {id(A)}"
      by auto
  } then have "∀A ∈  FinPow(X). A = 0 ∨ 
      (A = {Maximum(r,A)} ∨ 
      ord_iso(A-{Maximum(r,A)},r,A-{Maximum(r,A)},r) = 
      {id(A-{Maximum(r,A)})} ⟶  ord_iso(A,r,A,r) = {id(A)})"
    by auto
  moreover note A2 A3
  ultimately show "ord_iso(B,r,B,r) = {id(B)}"
    by (rule fin_ord_ind)
qed

text‹Every two finite linearly ordered sets are order 
  isomorphic. The statement is formulated to make the 
  proof by induction on the size of the set easier, 
  see ‹fin_ord_iso_ex› for an alternative formulation.
›

lemma fin_order_iso: 
  assumes A1: "IsLinOrder(X,r)"  "IsLinOrder(Y,R)" and
  A2: "n ∈ nat" 
  shows "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
  A ≈ n ∧ B ≈ n ⟶ ord_iso(A,r,B,R) ≠ 0"
proof -
  note A2
  moreover have "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
    A ≈ 0 ∧ B ≈ 0 ⟶ ord_iso(A,r,B,R) ≠ 0"
    using eqpoll_0_is_0 empty_ord_iso by blast
  moreover have "∀k ∈ nat.
    (∀A ∈ FinPow(X). ∀B ∈ FinPow(Y). 
    A ≈ k ∧ B ≈ k ⟶ ord_iso(A,r,B,R) ≠ 0) ⟶
    (∀C ∈ FinPow(X). ∀D ∈ FinPow(Y). 
    C ≈ succ(k) ∧ D ≈ succ(k) ⟶ ord_iso(C,r,D,R) ≠ 0)"
  proof -
    { fix k assume "k ∈ nat"
      assume A3: "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y). 
	A ≈ k ∧ B ≈ k ⟶ ord_iso(A,r,B,R) ≠ 0"
      have "∀C ∈ FinPow(X). ∀D ∈ FinPow(Y). 
	C ≈ succ(k) ∧ D ≈ succ(k) ⟶ ord_iso(C,r,D,R) ≠ 0"
      proof -
	{ fix C assume "C ∈ FinPow(X)"
	  fix D assume "D ∈ FinPow(Y)"
	  assume "C ≈ succ(k)"  "D ≈ succ(k)"
	  then have "C ≠ 0" and "D≠ 0"
	    using eqpoll_succ_imp_not_empty by auto
	  let ?M⇩C = "Maximum(r,C)"
	  let ?M⇩D = "Maximum(R,D)"
	  let ?C⇩0 = "C - {?M⇩C}"
	  let ?D⇩0 = "D - {?M⇩D}"
	  from ‹C ∈ FinPow(X)› have "C ⊆ X"
	    using FinPow_def by simp
	  with A1 have "IsLinOrder(C,r)"
	    using ord_linear_subset by blast
	  from ‹D ∈ FinPow(Y)› have "D ⊆ Y"
	    using FinPow_def by simp
	  with A1 have "IsLinOrder(D,R)"
	    using ord_linear_subset by blast 
	  from A1 ‹C ∈ FinPow(X)› ‹D ∈ FinPow(Y)›  
	    ‹C ≠ 0› ‹D≠ 0› have 
	    "HasAmaximum(r,C)" and "HasAmaximum(R,D)"
	    using IsLinOrder_def fin_has_max 
	    by auto
	  with A1 have "?M⇩C ∈ C" and "?M⇩D ∈ D"
	    using IsLinOrder_def Order_ZF_4_L3 by auto
	  with ‹C ≈ succ(k)›  ‹D ≈ succ(k)› have 
	    "?C⇩0  ≈ k" and "?D⇩0 ≈ k" using Diff_sing_eqpoll by auto
	  from ‹C ∈ FinPow(X)› ‹D ∈ FinPow(Y)›
	  have "?C⇩0 ∈  FinPow(X)" and "?D⇩0 ∈  FinPow(Y)"
	    using fin_rem_point_fin by auto
	  with A3 ‹?C⇩0  ≈ k› ‹?D⇩0 ≈ k› have
	    "ord_iso(?C⇩0,r,?D⇩0,R) ≠ 0" by simp
	  with ‹IsLinOrder(C,r)›  ‹IsLinOrder(D,R)› 
	    ‹HasAmaximum(r,C)› ‹HasAmaximum(R,D)›
	  have "ord_iso(C,r,D,R) ≠ 0"
	    by (rule rem_max_ord_iso)
	} thus ?thesis by simp
      qed
    } thus ?thesis by blast
  qed
  ultimately show ?thesis by (rule ind_on_nat)
qed

text‹Every two finite linearly ordered sets are order 
  isomorphic.›

lemma fin_ord_iso_ex: 
  assumes A1: "IsLinOrder(X,r)"  "IsLinOrder(Y,R)" and
  A2: "A ∈ FinPow(X)" "B ∈ FinPow(Y)" and A3: "B ≈ A"
  shows "ord_iso(A,r,B,R) ≠ 0"
proof -
  from A2 obtain n where "n ∈ nat" and "A ≈ n"
    using finpow_decomp by auto
  from  A3 ‹A ≈ n› have "B ≈ n" by (rule eqpoll_trans)
  with A1 A2 ‹A ≈ n› ‹n ∈ nat› show "ord_iso(A,r,B,R) ≠ 0"
    using fin_order_iso by simp
qed

text‹Existence and uniqueness of order isomorphism for two
  linearly ordered sets with the same number of elements.›

theorem fin_ord_iso_ex_uniq: 
  assumes A1: "IsLinOrder(X,r)"  "IsLinOrder(Y,R)" and
  A2: "A ∈ FinPow(X)" "B ∈ FinPow(Y)" and A3: "B ≈ A"
  shows "∃!f. f ∈ ord_iso(A,r,B,R)"
proof
  from assms show "∃f. f ∈ ord_iso(A,r,B,R)"
    using fin_ord_iso_ex by blast
  fix f g 
  assume A4: "f ∈ ord_iso(A,r,B,R)"  "g ∈ ord_iso(A,r,B,R)"
  then have "converse(g) ∈ ord_iso(B,R,A,r)"
    using ord_iso_sym by simp
  with ‹f ∈ ord_iso(A,r,B,R)› have 
    I: "converse(g) O f ∈  ord_iso(A,r,A,r)"
    by (rule ord_iso_trans)
  { assume "A ≠ 0"
    with A1 A2 I have "converse(g) O f = id(A)"
      using fin_ord_auto_id by auto
    with A4 have "f = g" 
      using ord_iso_def comp_inv_id_eq_bij by auto }
  moreover
  { assume "A = 0"
    then have "A ≈ 0" using eqpoll_0_iff
      by simp
    with A3 have "B ≈ 0" by (rule eqpoll_trans)
    with A4 ‹A = 0› have
      "f ∈ ord_iso(0,r,0,R)" and  "g ∈ ord_iso(0,r,0,R)"
      using eqpoll_0_iff by auto
    then have "f = g" by (rule empty_ord_iso_uniq) }
  ultimately show "f = g" 
    using ord_iso_def comp_inv_id_eq_bij
    by auto
qed



end