Theory Cardinal

(*  Title:      ZF/Cardinal.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

sectionCardinal Numbers Without the Axiom of Choice

theory Cardinal imports OrderType Finite Nat Sum begin

definition
  (*least ordinal operator*)
   Least    :: "(io)  i"    (binder μ  10)  where
     "Least(P)  THE i. Ord(i)  P(i)  (j. j<i  ¬P(j))"

definition
  eqpoll   :: "[i,i]  o"     (infixl  50)  where
    "A  B  f. f  bij(A,B)"

definition
  lepoll   :: "[i,i]  o"     (infixl  50)  where
    "A  B  f. f  inj(A,B)"

definition
  lesspoll :: "[i,i]  o"     (infixl  50)  where
    "A  B  A  B  ¬(A  B)"

definition
  cardinal :: "ii"           (|_|)  where
    "|A|  (μ i. i  A)"

definition
  Finite   :: "io"  where
    "Finite(A)  nnat. A  n"

definition
  Card     :: "io"  where
    "Card(i)  (i = |i|)"


subsectionThe Schroeder-Bernstein Theorem
textSee Davey and Priestly, page 106

(** Lemma: Banach's Decomposition Theorem **)

lemma decomp_bnd_mono: "bnd_mono(X, λW. X - g``(Y - f``W))"
by (rule bnd_monoI, blast+)

lemma Banach_last_equation:
    "g  Y->X
      g``(Y - f`` lfp(X, λW. X - g``(Y - f``W))) =
         X - lfp(X, λW. X - g``(Y - f``W))"
apply (rule_tac P = "λu. v = X-u" for v
       in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
apply (simp add: double_complement  fun_is_rel [THEN image_subset])
done

lemma decomposition:
     "f  X->Y;  g  Y->X 
      XA XB YA YB. (XA  XB = 0)  (XA  XB = X) 
                      (YA  YB = 0)  (YA  YB = Y) 
                      f``XA=YA  g``YB=XB"
apply (intro exI conjI)
apply (rule_tac [6] Banach_last_equation)
apply (rule_tac [5] refl)
apply (assumption |
       rule  Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
done

lemma schroeder_bernstein:
    "f  inj(X,Y);  g  inj(Y,X)  h. h  bij(X,Y)"
apply (insert decomposition [of f X Y g])
apply (simp add: inj_is_fun)
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
(* The instantiation of exI to @{term"restrict(f,XA) ∪ converse(restrict(g,YB))"}
   is forced by the context⋀*)
done


(** Equipollence is an equivalence relation **)

lemma bij_imp_eqpoll: "f  bij(A,B)  A  B"
  unfolding eqpoll_def
apply (erule exI)
done

(*A ≈ A*)
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]

lemma eqpoll_sym: "X  Y  Y  X"
  unfolding eqpoll_def
apply (blast intro: bij_converse_bij)
done

lemma eqpoll_trans [trans]:
    "X  Y;  Y  Z  X  Z"
  unfolding eqpoll_def
apply (blast intro: comp_bij)
done

(** Le-pollence is a partial ordering **)

lemma subset_imp_lepoll: "X<=Y  X  Y"
  unfolding lepoll_def
apply (rule exI)
apply (erule id_subset_inj)
done

lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]

lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]

lemma eqpoll_imp_lepoll: "X  Y  X  Y"
by (unfold eqpoll_def bij_def lepoll_def, blast)

lemma lepoll_trans [trans]: "X  Y;  Y  Z  X  Z"
  unfolding lepoll_def
apply (blast intro: comp_inj)
done

lemma eq_lepoll_trans [trans]: "X  Y;  Y  Z  X  Z"
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)

lemma lepoll_eq_trans [trans]: "X  Y;  Y  Z  X  Z"
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)

(*Asymmetry law*)
lemma eqpollI: "X  Y;  Y  X  X  Y"
  unfolding lepoll_def eqpoll_def
apply (elim exE)
apply (rule schroeder_bernstein, assumption+)
done

lemma eqpollE:
    "X  Y; X  Y; Y  X  P  P"
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)

lemma eqpoll_iff: "X  Y  X  Y  Y  X"
by (blast intro: eqpollI elim!: eqpollE)

lemma lepoll_0_is_0: "A  0  A = 0"
  unfolding lepoll_def inj_def
apply (blast dest: apply_type)
done

(*@{term"0 ≲ Y"}*)
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]

lemma lepoll_0_iff: "A  0  A=0"
by (blast intro: lepoll_0_is_0 lepoll_refl)

lemma Un_lepoll_Un:
    "A  B; C  D; B  D = 0  A  C  B  D"
  unfolding lepoll_def
apply (blast intro: inj_disjoint_Un)
done

(*A ≈ 0 ⟹ A=0*)
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]

lemma eqpoll_0_iff: "A  0  A=0"
by (blast intro: eqpoll_0_is_0 eqpoll_refl)

lemma eqpoll_disjoint_Un:
    "A  B;  C  D;  A  C = 0;  B  D = 0
      A  C  B  D"
  unfolding eqpoll_def
apply (blast intro: bij_disjoint_Un)
done


subsectionlesspoll: contributions by Krzysztof Grabczewski

lemma lesspoll_not_refl: "¬ (i  i)"
by (simp add: lesspoll_def)

lemma lesspoll_irrefl [elim!]: "i  i  P"
by (simp add: lesspoll_def)

lemma lesspoll_imp_lepoll: "A  B  A  B"
by (unfold lesspoll_def, blast)

lemma lepoll_well_ord: "A  B; well_ord(B,r)  s. well_ord(A,s)"
  unfolding lepoll_def
apply (blast intro: well_ord_rvimage)
done

lemma lepoll_iff_leqpoll: "A  B  A  B | A  B"
  unfolding lesspoll_def
apply (blast intro!: eqpollI elim!: eqpollE)
done

lemma inj_not_surj_succ:
  assumes fi: "f  inj(A, succ(m))" and fns: "f  surj(A, succ(m))" 
  shows "f. f  inj(A,m)"
proof -
  from fi [THEN inj_is_fun] fns 
  obtain y where y: "y  succ(m)" "x. xA  f ` x  y"
    by (auto simp add: surj_def)
  show ?thesis
    proof 
      show "(λzA. if f`z = m then y else f`z)  inj(A, m)" using y fi
        by (simp add: inj_def) 
           (auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype)
      qed
qed

(** Variations on transitivity **)

lemma lesspoll_trans [trans]:
      "X  Y; Y  Z  X  Z"
  unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done

lemma lesspoll_trans1 [trans]:
      "X  Y; Y  Z  X  Z"
  unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done

lemma lesspoll_trans2 [trans]:
      "X  Y; Y  Z  X  Z"
  unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done

lemma eq_lesspoll_trans [trans]:
      "X  Y; Y  Z  X  Z"
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)

lemma lesspoll_eq_trans [trans]:
      "X  Y; Y  Z  X  Z"
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)


(** μ -- the least number operator [from HOL/Univ.ML] **)

lemma Least_equality:
    "P(i);  Ord(i);  x. x<i  ¬P(x)  (μ x. P(x)) = i"
  unfolding Least_def
apply (rule the_equality, blast)
apply (elim conjE)
apply (erule Ord_linear_lt, assumption, blast+)
done

lemma LeastI: 
  assumes P: "P(i)" and i: "Ord(i)" shows "P(μ x. P(x))"
proof -
  { from i have "P(i)  P(μ x. P(x))"
      proof (induct i rule: trans_induct)
        case (step i) 
        show ?case
          proof (cases "P(μ a. P(a))")
            case True thus ?thesis .
          next
            case False
            hence "x. x  i  ¬P(x)" using step
              by blast
            hence "(μ a. P(a)) = i" using step
              by (blast intro: Least_equality ltD) 
            thus ?thesis using step.prems
              by simp 
          qed
      qed
  }
  thus ?thesis using P .
qed

textThe proof is almost identical to the one above!
lemma Least_le: 
  assumes P: "P(i)" and i: "Ord(i)" shows "(μ x. P(x))  i"
proof -
  { from i have "P(i)  (μ x. P(x))  i"
      proof (induct i rule: trans_induct)
        case (step i) 
        show ?case
          proof (cases "(μ a. P(a))  i")
            case True thus ?thesis .
          next
            case False
            hence "x. x  i  ¬ (μ a. P(a))  i" using step
              by blast
            hence "(μ a. P(a)) = i" using step
              by (blast elim: ltE intro: ltI Least_equality lt_trans1)
            thus ?thesis using step
              by simp 
          qed
      qed
  }
  thus ?thesis using P .
qed

(*μ really is the smallest*)
lemma less_LeastE: "P(i);  i < (μ x. P(x))  Q"
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
apply (simp add: lt_Ord)
done

(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
lemma LeastI2:
    "P(i);  Ord(i);  j. P(j)  Q(j)  Q(μ j. P(j))"
by (blast intro: LeastI )

(*If there is no such P then μ is vacuously 0*)
lemma Least_0:
    "¬ (i. Ord(i)  P(i))  (μ x. P(x)) = 0"
  unfolding Least_def
apply (rule the_0, blast)
done

lemma Ord_Least [intro,simp,TC]: "Ord(μ x. P(x))"
proof (cases "i. Ord(i)  P(i)")
  case True 
  then obtain i where "P(i)" "Ord(i)"  by auto
  hence " (μ x. P(x))  i"  by (rule Least_le) 
  thus ?thesis
    by (elim ltE)
next
  case False
  hence "(μ x. P(x)) = 0"  by (rule Least_0)
  thus ?thesis
    by auto
qed


subsectionBasic Properties of Cardinals

(*Not needed for simplification, but helpful below*)
lemma Least_cong: "(y. P(y)  Q(y))  (μ x. P(x)) = (μ x. Q(x))"
by simp

(*Need AC to get @{term"X ≲ Y ⟹ |X| ≤ |Y|"};  see well_ord_lepoll_imp_cardinal_le
  Converse also requires AC, but see well_ord_cardinal_eqE*)
lemma cardinal_cong: "X  Y  |X| = |Y|"
  unfolding eqpoll_def cardinal_def
apply (rule Least_cong)
apply (blast intro: comp_bij bij_converse_bij)
done

(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
lemma well_ord_cardinal_eqpoll:
  assumes r: "well_ord(A,r)" shows "|A|  A"
proof (unfold cardinal_def)
  show "(μ i. i  A)  A"
    by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 
qed

(* @{term"Ord(A) ⟹ |A| ≈ A"} *)
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]

lemma Ord_cardinal_idem: "Ord(A)  ||A|| = |A|"
 by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])

lemma well_ord_cardinal_eqE:
  assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|"
shows "X  Y"
proof -
  have "X  |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym)
  also have "... = |Y|" by (rule eq)
  also have "...  Y" by (rule well_ord_cardinal_eqpoll [OF woY])
  finally show ?thesis .
qed

lemma well_ord_cardinal_eqpoll_iff:
     "well_ord(X,r);  well_ord(Y,s)  |X| = |Y|  X  Y"
by (blast intro: cardinal_cong well_ord_cardinal_eqE)


(** Observations from Kunen, page 28 **)

lemma Ord_cardinal_le: "Ord(i)  |i|  i"
  unfolding cardinal_def
apply (erule eqpoll_refl [THEN Least_le])
done

lemma Card_cardinal_eq: "Card(K)  |K| = K"
  unfolding Card_def
apply (erule sym)
done

(* Could replace the  @{term"¬(j ≈ i)"}  by  @{term"¬(i ≼ j)"}. *)
lemma CardI: "Ord(i);  j. j<i  ¬(j  i)  Card(i)"
  unfolding Card_def cardinal_def
apply (subst Least_equality)
apply (blast intro: eqpoll_refl)+
done

lemma Card_is_Ord: "Card(i)  Ord(i)"
  unfolding Card_def cardinal_def
apply (erule ssubst)
apply (rule Ord_Least)
done

lemma Card_cardinal_le: "Card(K)  K  |K|"
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
done

lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
  unfolding cardinal_def
apply (rule Ord_Least)
done

textThe cardinals are the initial ordinals.
lemma Card_iff_initial: "Card(K)  Ord(K)  (j. j<K  ¬ j  K)"
proof -
  { fix j
    assume K: "Card(K)" "j  K"
    assume "j < K"
    also have "... = (μ i. i  K)" using K
      by (simp add: Card_def cardinal_def)
    finally have "j < (μ i. i  K)" .
    hence "False" using K
      by (best dest: less_LeastE) 
  }
  then show ?thesis
    by (blast intro: CardI Card_is_Ord) 
qed

lemma lt_Card_imp_lesspoll: "Card(a); i<a  i  a"
  unfolding lesspoll_def
apply (drule Card_iff_initial [THEN iffD1])
apply (blast intro!: leI [THEN le_imp_lepoll])
done

lemma Card_0: "Card(0)"
apply (rule Ord_0 [THEN CardI])
apply (blast elim!: ltE)
done

lemma Card_Un: "Card(K);  Card(L)  Card(K  L)"
apply (rule Ord_linear_le [of K L])
apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
                     subset_Un_iff2 [THEN iffD1])
done

(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)

lemma Card_cardinal [iff]: "Card(|A|)"
proof (unfold cardinal_def)
  show "Card(μ i. i  A)"
    proof (cases "i. Ord (i)  i  A")
      case False thus ?thesis           ― ‹degenerate case
        by (simp add: Least_0 Card_0)
    next
      case True                         ― ‹real case: termA is isomorphic to some ordinal
      then obtain i where i: "Ord(i)" "i  A" by blast
      show ?thesis
        proof (rule CardI [OF Ord_Least], rule notI)
          fix j
          assume j: "j < (μ i. i  A)"
          assume "j  (μ i. i  A)"
          also have "...  A" using i by (auto intro: LeastI)
          finally have "j  A" .
          thus False
            by (rule less_LeastE [OF _ j])
        qed
    qed
qed

(*Kunen's Lemma 10.5*)
lemma cardinal_eq_lemma:
  assumes i:"|i|  j" and j: "j  i" shows "|j| = |i|"
proof (rule eqpollI [THEN cardinal_cong])
  show "j  i" by (rule le_imp_lepoll [OF j])
next
  have Oi: "Ord(i)" using j by (rule le_Ord2)
  hence "i  |i|"
    by (blast intro: Ord_cardinal_eqpoll eqpoll_sym)
  also have "...  j"
    by (blast intro: le_imp_lepoll i)
  finally show "i  j" .
qed

lemma cardinal_mono:
  assumes ij: "i  j" shows "|i|  |j|"
using Ord_cardinal [of i] Ord_cardinal [of j]
proof (cases rule: Ord_linear_le)
  case le thus ?thesis .
next
  case ge
  have i: "Ord(i)" using ij
    by (simp add: lt_Ord)
  have ci: "|i|  j"
    by (blast intro: Ord_cardinal_le ij le_trans i)
  have "|i| = ||i||"
    by (auto simp add: Ord_cardinal_idem i)
  also have "... = |j|"
    by (rule cardinal_eq_lemma [OF ge ci])
  finally have "|i| = |j|" .
  thus ?thesis by simp
qed

textSince we have term|succ(nat)|  |nat|, the converse of cardinal_mono› fails!
lemma cardinal_lt_imp_lt: "|i| < |j|;  Ord(i);  Ord(j)  i < j"
apply (rule Ord_linear2 [of i j], assumption+)
apply (erule lt_trans2 [THEN lt_irrefl])
apply (erule cardinal_mono)
done

lemma Card_lt_imp_lt: "|i| < K;  Ord(i);  Card(K)  i < K"
  by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)

lemma Card_lt_iff: "Ord(i);  Card(K)  (|i| < K)  (i < K)"
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])

lemma Card_le_iff: "Ord(i);  Card(K)  (K  |i|)  (K  i)"
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])

(*Can use AC or finiteness to discharge first premise*)
lemma well_ord_lepoll_imp_cardinal_le:
  assumes wB: "well_ord(B,r)" and AB: "A  B"
  shows "|A|  |B|"
using Ord_cardinal [of A] Ord_cardinal [of B]
proof (cases rule: Ord_linear_le)
  case le thus ?thesis .
next
  case ge
  from lepoll_well_ord [OF AB wB]
  obtain s where s: "well_ord(A, s)" by blast
  have "B   |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
  also have "...  |A|" by (rule le_imp_lepoll [OF ge])
  also have "...  A" by (rule well_ord_cardinal_eqpoll [OF s])
  finally have "B  A" .
  hence "A  B" by (blast intro: eqpollI AB)
  hence "|A| = |B|" by (rule cardinal_cong)
  thus ?thesis by simp
qed

lemma lepoll_cardinal_le: "A  i; Ord(i)  |A|  i"
apply (rule le_trans)
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption)
apply (erule Ord_cardinal_le)
done

lemma lepoll_Ord_imp_eqpoll: "A  i; Ord(i)  |A|  A"
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)

lemma lesspoll_imp_eqpoll: "A  i; Ord(i)  |A|  A"
  unfolding lesspoll_def
apply (blast intro: lepoll_Ord_imp_eqpoll)
done

lemma cardinal_subset_Ord: "A<=i; Ord(i)  |A|  i"
apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
apply (auto simp add: lt_def)
apply (blast intro: Ord_trans)
done

subsectionThe finite cardinals

lemma cons_lepoll_consD:
 "cons(u,A)  cons(v,B);  uA;  vB  A  B"
apply (unfold lepoll_def inj_def, safe)
apply (rule_tac x = "λxA. if f`x=v then f`u else f`x" in exI)
apply (rule CollectI)
(*Proving it's in the function space A->B*)
apply (rule if_type [THEN lam_type])
apply (blast dest: apply_funtype)
apply (blast elim!: mem_irrefl dest: apply_funtype)
(*Proving it's injective*)
apply (simp (no_asm_simp))
apply blast
done

lemma cons_eqpoll_consD: "cons(u,A)  cons(v,B);  uA;  vB  A  B"
apply (simp add: eqpoll_iff)
apply (blast intro: cons_lepoll_consD)
done

(*Lemma suggested by Mike Fourman*)
lemma succ_lepoll_succD: "succ(m)  succ(n)  m  n"
  unfolding succ_def
apply (erule cons_lepoll_consD)
apply (rule mem_not_refl)+
done


lemma nat_lepoll_imp_le:
     "m  nat  n  nat  m  n  m  n"
proof (induct m arbitrary: n rule: nat_induct)
  case 0 thus ?case by (blast intro!: nat_0_le)
next
  case (succ m)
  show ?case  using n  nat
    proof (cases rule: natE)
      case 0 thus ?thesis using succ
        by (simp add: lepoll_def inj_def)
    next
      case (succ n') thus ?thesis using succ.hyps  succ(m)  n
        by (blast intro!: succ_leI dest!: succ_lepoll_succD)
    qed
qed

lemma nat_eqpoll_iff: "m  nat; n  nat  m  n  m = n"
apply (rule iffI)
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
apply (simp add: eqpoll_refl)
done

(*The object of all this work: every natural number is a (finite) cardinal*)
lemma nat_into_Card:
  assumes n: "n  nat" shows "Card(n)"
proof (unfold Card_def cardinal_def, rule sym)
  have "Ord(n)" using n  by auto
  moreover
  { fix i
    assume "i < n" "i  n"
    hence False using n
      by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff])
  }
  ultimately show "(μ i. i  n) = n" by (auto intro!: Least_equality) 
qed

lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]


(*Part of Kunen's Lemma 10.6*)
lemma succ_lepoll_natE: "succ(n)  n;  n  nat  P"
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)

lemma nat_lepoll_imp_ex_eqpoll_n:
     "n  nat;  nat  X  Y. Y  X  n  Y"
  unfolding lepoll_def eqpoll_def
apply (fast del: subsetI subsetCE
            intro!: subset_SIs
            dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
            elim!: restrict_bij
                   inj_is_fun [THEN fun_is_rel, THEN image_subset])
done


(** ≲, ≺ and natural numbers **)

lemma lepoll_succ: "i  succ(i)"
  by (blast intro: subset_imp_lepoll)

lemma lepoll_imp_lesspoll_succ:
  assumes A: "A  m" and m: "m  nat"
  shows "A  succ(m)"
proof -
  { assume "A  succ(m)"
    hence "succ(m)  A" by (rule eqpoll_sym)
    also have "...  m" by (rule A)
    finally have "succ(m)  m" .
    hence False by (rule succ_lepoll_natE) (rule m) }
  moreover have "A  succ(m)" by (blast intro: lepoll_trans A lepoll_succ)
  ultimately show ?thesis by (auto simp add: lesspoll_def)
qed

lemma lesspoll_succ_imp_lepoll:
     "A  succ(m); m  nat  A  m"
  unfolding lesspoll_def lepoll_def eqpoll_def bij_def
apply (auto dest: inj_not_surj_succ)
done

lemma lesspoll_succ_iff: "m  nat  A  succ(m)  A  m"
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)

lemma lepoll_succ_disj: "A  succ(m);  m  nat  A  m | A  succ(m)"
apply (rule disjCI)
apply (rule lesspoll_succ_imp_lepoll)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: lesspoll_def)
done

lemma lesspoll_cardinal_lt: "A  i; Ord(i)  |A| < i"
apply (unfold lesspoll_def, clarify)
apply (frule lepoll_cardinal_le, assumption)
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
             dest: lepoll_well_ord  elim!: leE)
done


subsectionThe first infinite cardinal: Omega, or nat

(*This implies Kunen's Lemma 10.6*)
lemma lt_not_lepoll:
  assumes n: "n<i" "n  nat" shows "¬ i  n"
proof -
  { assume i: "i  n"
    have "succ(n)  i" using n
      by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll])
    also have "...  n" by (rule i)
    finally have "succ(n)  n" .
    hence False  by (rule succ_lepoll_natE) (rule n) }
  thus ?thesis by auto
qed

textA slightly weaker version of nat_eqpoll_iff›
lemma Ord_nat_eqpoll_iff:
  assumes i: "Ord(i)" and n: "n  nat" shows "i  n  i=n"
using i nat_into_Ord [OF n]
proof (cases rule: Ord_linear_lt)
  case lt
  hence  "i  nat" by (rule lt_nat_in_nat) (rule n)
  thus ?thesis by (simp add: nat_eqpoll_iff n)
next
  case eq
  thus ?thesis by (simp add: eqpoll_refl)
next
  case gt
  hence  "¬ i  n" using n  by (rule lt_not_lepoll)
  hence  "¬ i  n" using n  by (blast intro: eqpoll_imp_lepoll)
  moreover have "i  n" using n<i by auto
  ultimately show ?thesis by blast
qed

lemma Card_nat: "Card(nat)"
proof -
  { fix i
    assume i: "i < nat" "i  nat"
    hence "¬ nat  i"
      by (simp add: lt_def lt_not_lepoll)
    hence False using i
      by (simp add: eqpoll_iff)
  }
  hence "(μ i. i  nat) = nat" by (blast intro: Least_equality eqpoll_refl)
  thus ?thesis
    by (auto simp add: Card_def cardinal_def)
qed

(*Allows showing that |i| is a limit cardinal*)
lemma nat_le_cardinal: "nat  i  nat  |i|"
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
apply (erule cardinal_mono)
done

lemma n_lesspoll_nat: "n  nat  n  nat"
  by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)


subsectionTowards Cardinal Arithmetic
(** Congruence laws for successor, cardinal addition and multiplication **)

(*Congruence law for  cons  under equipollence*)
lemma cons_lepoll_cong:
    "A  B;  b  B  cons(a,A)  cons(b,B)"
apply (unfold lepoll_def, safe)
apply (rule_tac x = "λycons (a,A) . if y=a then b else f`y" in exI)
apply (rule_tac d = "λz. if z  B then converse (f) `z else a" in lam_injective)
apply (safe elim!: consE')
   apply simp_all
apply (blast intro: inj_is_fun [THEN apply_type])+
done

lemma cons_eqpoll_cong:
     "A  B;  a  A;  b  B  cons(a,A)  cons(b,B)"
by (simp add: eqpoll_iff cons_lepoll_cong)

lemma cons_lepoll_cons_iff:
     "a  A;  b  B  cons(a,A)  cons(b,B)    A  B"
by (blast intro: cons_lepoll_cong cons_lepoll_consD)

lemma cons_eqpoll_cons_iff:
     "a  A;  b  B  cons(a,A)  cons(b,B)    A  B"
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)

lemma singleton_eqpoll_1: "{a}  1"
  unfolding succ_def
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
done

lemma cardinal_singleton: "|{a}| = 1"
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
done

lemma not_0_is_lepoll_1: "A  0  1  A"
apply (erule not_emptyE)
apply (rule_tac a = "cons (x, A-{x}) " in subst)
apply (rule_tac [2] a = "cons(0,0)" and P= "λy. y  cons (x, A-{x})" in subst)
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
done

(*Congruence law for  succ  under equipollence*)
lemma succ_eqpoll_cong: "A  B  succ(A)  succ(B)"
  unfolding succ_def
apply (simp add: cons_eqpoll_cong mem_not_refl)
done

(*Congruence law for + under equipollence*)
lemma sum_eqpoll_cong: "A  C;  B  D  A+B  C+D"
  unfolding eqpoll_def
apply (blast intro!: sum_bij)
done

(*Congruence law for * under equipollence*)
lemma prod_eqpoll_cong:
    "A  C;  B  D  A*B  C*D"
  unfolding eqpoll_def
apply (blast intro!: prod_bij)
done

lemma inj_disjoint_eqpoll:
    "f  inj(A,B);  A  B = 0  A  (B - range(f))  B"
  unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "λx. if x  A then f`x else x"
            and d = "λy. if y  range (f) then converse (f) `y else y"
       in lam_bijective)
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
apply (safe elim!: UnE')
   apply (simp_all add: inj_is_fun [THEN apply_rangeI])
apply (blast intro: inj_converse_fun [THEN apply_type])+
done


subsectionLemmas by Krzysztof Grabczewski

(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)

textIf termA has at most termn+1 elements and terma  A
      then termA-{a} has at most termn.
lemma Diff_sing_lepoll:
      "a  A;  A  succ(n)  A - {a}  n"
  unfolding succ_def
apply (rule cons_lepoll_consD)
apply (rule_tac [3] mem_not_refl)
apply (erule cons_Diff [THEN ssubst], safe)
done

textIf termA has at least termn+1 elements then termA-{a} has at least termn.
lemma lepoll_Diff_sing:
  assumes A: "succ(n)  A" shows "n  A - {a}"
proof -
  have "cons(n,n)  A" using A
    by (unfold succ_def)
  also have "...  cons(a, A-{a})"
    by (blast intro: subset_imp_lepoll)
  finally have "cons(n,n)  cons(a, A-{a})" .
  thus ?thesis
    by (blast intro: cons_lepoll_consD mem_irrefl)
qed

lemma Diff_sing_eqpoll: "a  A; A  succ(n)  A - {a}  n"
by (blast intro!: eqpollI
          elim!: eqpollE
          intro: Diff_sing_lepoll lepoll_Diff_sing)

lemma lepoll_1_is_sing: "A  1; a  A  A = {a}"
apply (frule Diff_sing_lepoll, assumption)
apply (drule lepoll_0_is_0)
apply (blast elim: equalityE)
done

lemma Un_lepoll_sum: "A  B  A+B"
  unfolding lepoll_def
apply (rule_tac x = "λxA  B. if xA then Inl (x) else Inr (x)" in exI)
apply (rule_tac d = "λz. snd (z)" in lam_injective)
apply force
apply (simp add: Inl_def Inr_def)
done

lemma well_ord_Un:
     "well_ord(X,R); well_ord(Y,S)  T. well_ord(X  Y, T)"
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
    assumption)

(*Krzysztof Grabczewski*)
lemma disj_Un_eqpoll_sum: "A  B = 0  A  B  A + B"
  unfolding eqpoll_def
apply (rule_tac x = "λaA  B. if a  A then Inl (a) else Inr (a)" in exI)
apply (rule_tac d = "λz. case (λx. x, λx. x, z)" in lam_bijective)
apply auto
done


subsection Finite and infinite sets

lemma eqpoll_imp_Finite_iff: "A  B  Finite(A)  Finite(B)"
  unfolding Finite_def
apply (blast intro: eqpoll_trans eqpoll_sym)
done

lemma Finite_0 [simp]: "Finite(0)"
  unfolding Finite_def
apply (blast intro!: eqpoll_refl nat_0I)
done

lemma Finite_cons: "Finite(x)  Finite(cons(y,x))"
  unfolding Finite_def
apply (case_tac "y ∈ x")
apply (simp add: cons_absorb)
apply (erule bexE)
apply (rule bexI)
apply (erule_tac [2] nat_succI)
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
done

lemma Finite_succ: "Finite(x)  Finite(succ(x))"
  unfolding succ_def
apply (erule Finite_cons)
done

lemma lepoll_nat_imp_Finite:
  assumes A: "A  n" and n: "n  nat" shows "Finite(A)"
proof -
  have "A  n  Finite(A)" using n
    proof (induct n)
      case 0
      hence "A = 0" by (rule lepoll_0_is_0) 
      thus ?case by simp
    next
      case (succ n)
      hence "A  n  A  succ(n)" by (blast dest: lepoll_succ_disj)
      thus ?case using succ by (auto simp add: Finite_def) 
    qed
  thus ?thesis using A .
qed

lemma lesspoll_nat_is_Finite:
     "A  nat  Finite(A)"
  unfolding Finite_def
apply (blast dest: ltD lesspoll_cardinal_lt
                   lesspoll_imp_eqpoll [THEN eqpoll_sym])
done

lemma lepoll_Finite:
  assumes Y: "Y  X" and X: "Finite(X)" shows "Finite(Y)"
proof -
  obtain n where n: "n  nat" "X  n" using X
    by (auto simp add: Finite_def)
  have "Y  X"         by (rule Y)
  also have "...  n"  by (rule n)
  finally have "Y  n" .
  thus ?thesis using n by (simp add: lepoll_nat_imp_Finite)
qed

lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]

lemma Finite_cons_iff [iff]: "Finite(cons(y,x))  Finite(x)"
by (blast intro: Finite_cons subset_Finite)

lemma Finite_succ_iff [iff]: "Finite(succ(x))  Finite(x)"
by (simp add: succ_def)

lemma Finite_Int: "Finite(A) | Finite(B)  Finite(A  B)"
by (blast intro: subset_Finite)

lemmas Finite_Diff = Diff_subset [THEN subset_Finite]

lemma nat_le_infinite_Ord:
      "Ord(i);  ¬ Finite(i)  nat  i"
  unfolding Finite_def
apply (erule Ord_nat [THEN [2] Ord_linear2])
prefer 2 apply assumption
apply (blast intro!: eqpoll_refl elim!: ltE)
done

lemma Finite_imp_well_ord:
    "Finite(A)  r. well_ord(A,r)"
  unfolding Finite_def eqpoll_def
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
done

lemma succ_lepoll_imp_not_empty: "succ(x)  y  y  0"
by (fast dest!: lepoll_0_is_0)

lemma eqpoll_succ_imp_not_empty: "x  succ(n)  x  0"
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])

lemma Finite_Fin_lemma [rule_format]:
     "n  nat  A. (An  A  X)  A  Fin(X)"
apply (induct_tac n)
apply (rule allI)
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
apply (rule allI)
apply (rule impI)
apply (erule conjE)
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
apply (frule Diff_sing_eqpoll, assumption)
apply (erule allE)
apply (erule impE, fast)
apply (drule subsetD, assumption)
apply (drule Fin.consI, assumption)
apply (simp add: cons_Diff)
done

lemma Finite_Fin: "Finite(A); A  X  A  Fin(X)"
by (unfold Finite_def, blast intro: Finite_Fin_lemma)

lemma Fin_lemma [rule_format]: "n  nat  A. A  n  A  Fin(A)"
apply (induct_tac n)
apply (simp add: eqpoll_0_iff, clarify)
apply (subgoal_tac "u. u  A")
apply (erule exE)
apply (rule Diff_sing_eqpoll [elim_format])
prefer 2 apply assumption
apply assumption
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
apply (rule Fin.consI, blast)
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
(*Now for the lemma assumed above*)
  unfolding eqpoll_def
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
done

lemma Finite_into_Fin: "Finite(A)  A  Fin(A)"
  unfolding Finite_def
apply (blast intro: Fin_lemma)
done

lemma Fin_into_Finite: "A  Fin(U)  Finite(A)"
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)

lemma Finite_Fin_iff: "Finite(A)  A  Fin(A)"
by (blast intro: Finite_into_Fin Fin_into_Finite)

lemma Finite_Un: "Finite(A); Finite(B)  Finite(A  B)"
by (blast intro!: Fin_into_Finite Fin_UnI
          dest!: Finite_into_Fin
          intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
                 Un_upper2 [THEN Fin_mono, THEN subsetD])

lemma Finite_Un_iff [simp]: "Finite(A  B)  (Finite(A)  Finite(B))"
by (blast intro: subset_Finite Finite_Un)

textThe converse must hold too.
lemma Finite_Union: "yX. Finite(y);  Finite(X)  Finite((X))"
apply (simp add: Finite_Fin_iff)
apply (rule Fin_UnionI)
apply (erule Fin_induct, simp)
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
done

(* Induction principle for Finite(A), by Sidi Ehmety *)
lemma Finite_induct [case_names 0 cons, induct set: Finite]:
"Finite(A); P(0);
    x B.   Finite(B); x  B; P(B)  P(cons(x, B))
  P(A)"
apply (erule Finite_into_Fin [THEN Fin_induct])
apply (blast intro: Fin_into_Finite)+
done

(*Sidi Ehmety.  The contrapositive says ¬Finite(A) ⟹ ¬Finite(A-{a}) *)
lemma Diff_sing_Finite: "Finite(A - {a})  Finite(A)"
  unfolding Finite_def
apply (case_tac "a ∈ A")
apply (subgoal_tac [2] "A-{a}=A", auto)
apply (rule_tac x = "succ (n) " in bexI)
apply (subgoal_tac "cons (a, A - {a}) = A  cons (n, n) = succ (n) ")
apply (drule_tac a = a and b = n in cons_eqpoll_cong)
apply (auto dest: mem_irrefl)
done

(*Sidi Ehmety.  And the contrapositive of this says
   ⟦¬Finite(A); Finite(B)⟧ ⟹ ¬Finite(A-B) *)
lemma Diff_Finite [rule_format]: "Finite(B)  Finite(A-B)  Finite(A)"
apply (erule Finite_induct, auto)
apply (case_tac "x ∈ A")
 apply (subgoal_tac [2] "A-cons (x, B) = A - B")
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
apply (drule Diff_sing_Finite, auto)
done

lemma Finite_RepFun: "Finite(A)  Finite(RepFun(A,f))"
by (erule Finite_induct, simp_all)

lemma Finite_RepFun_iff_lemma [rule_format]:
     "Finite(x); x y. f(x)=f(y)  x=y
       A. x = RepFun(A,f)  Finite(A)"
apply (erule Finite_induct)
 apply clarify
 apply (case_tac "A=0", simp)
 apply (blast del: allE, clarify)
apply (subgoal_tac "zA. x = f(z)")
 prefer 2 apply (blast del: allE elim: equalityE, clarify)
apply (subgoal_tac "B = {f(u) . u  A - {z}}")
 apply (blast intro: Diff_sing_Finite)
apply (thin_tac "A. P(A)  Finite(A)" for P)
apply (rule equalityI)
 apply (blast intro: elim: equalityE)
apply (blast intro: elim: equalityCE)
done

textI don't know why, but if the premise is expressed using meta-connectives
then  the simplifier cannot prove it automatically in conditional rewriting.
lemma Finite_RepFun_iff:
     "(x y. f(x)=f(y)  x=y)  Finite(RepFun(A,f))  Finite(A)"
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])

lemma Finite_Pow: "Finite(A)  Finite(Pow(A))"
apply (erule Finite_induct)
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
done

lemma Finite_Pow_imp_Finite: "Finite(Pow(A))  Finite(A)"
apply (subgoal_tac "Finite({{x} . x  A})")
 apply (simp add: Finite_RepFun_iff )
apply (blast intro: subset_Finite)
done

lemma Finite_Pow_iff [iff]: "Finite(Pow(A))  Finite(A)"
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)

lemma Finite_cardinal_iff:
  assumes i: "Ord(i)" shows "Finite(|i|)  Finite(i)"
  by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+


(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
  set is well-ordered.  Proofs simplified by lcp. *)

lemma nat_wf_on_converse_Memrel: "n  nat  wf[n](converse(Memrel(n)))"
proof (induct n rule: nat_induct)
  case 0 thus ?case by (blast intro: wf_onI)
next
  case (succ x)
  hence wfx: "Z. Z = 0  (zZ. y. z  y  z  x  y  x  z  x  y  Z)"
    by (simp add: wf_on_def wf_def)  ― ‹not easy to erase the duplicate termz  x!
  show ?case
    proof (rule wf_onI)
      fix Z u
      assume Z: "u  Z" "zZ. yZ. y, z  converse(Memrel(succ(x)))"
      show False 
        proof (cases "x  Z")
          case True thus False using Z
            by (blast elim: mem_irrefl mem_asym)
          next
          case False thus False using wfx [of Z] Z
            by blast
        qed
    qed
qed

lemma nat_well_ord_converse_Memrel: "n  nat  well_ord(n,converse(Memrel(n)))"
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
done

lemma well_ord_converse:
     "well_ord(A,r);
        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))
       well_ord(A,converse(r))"
apply (rule well_ord_Int_iff [THEN iffD1])
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
apply (simp add: rvimage_converse converse_Int converse_prod
                 ordertype_ord_iso [THEN ord_iso_rvimage_eq])
done

lemma ordertype_eq_n:
  assumes r: "well_ord(A,r)" and A: "A  n" and n: "n  nat"
  shows "ordertype(A,r) = n"
proof -
  have "ordertype(A,r)  A"
    by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r)
  also have "...  n" by (rule A)
  finally have "ordertype(A,r)  n" .
  thus ?thesis
    by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r)
qed

lemma Finite_well_ord_converse:
    "Finite(A);  well_ord(A,r)  well_ord(A,converse(r))"
  unfolding Finite_def
apply (rule well_ord_converse, assumption)
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
done

lemma nat_into_Finite: "n  nat  Finite(n)"
  by (auto simp add: Finite_def intro: eqpoll_refl) 

lemma nat_not_Finite: "¬ Finite(nat)"
proof -
  { fix n
    assume n: "n  nat" "nat  n"
    have "n  nat"    by (rule n)
    also have "... = n" using n
      by (simp add: Ord_nat_eqpoll_iff Ord_nat)
    finally have "n  n" .
    hence False
      by (blast elim: mem_irrefl)
  }
  thus ?thesis
    by (auto simp add: Finite_def)
qed

end