SSL Cardinal.thy Sprache: Isabelle

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

section\<open>Cardinal Numbers Without the Axiom of Choice\<close>

theory Cardinal imports OrderType Finite Nat Sum begin

definition
  (*least ordinal operator*)
   Least    :: "(i\o) \ i" (binder \\ \ 10) where
     "Least(P) \ THE i. Ord(i) \ P(i) \ (\j. j \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 :: "i\i" (\(\open_block notation=\mixfix cardinal\\|_|)\)
  where "|A| \ (\ i. i \ A)"

definition
  Finite   :: "i\o" where
    "Finite(A) \ \n\nat. A \ n"

definition
  Card     :: "i\o" where
    "Card(i) \ (i = |i|)"

subsection\<open>The Schroeder-Bernstein Theorem\<close>
text\<open>See Davey and Priestly, page 106\<close>

(** 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
     \<Longrightarrow> g``(Y - f`` lfp(X, \<lambda>W. X - g``(Y - f``W))) =
         X - lfp(X, \<lambda>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\ \
      \<exists>XA XB YA YB. (XA \<inter> XB = 0) \<and> (XA \<union> XB = X) \<and>
                      (YA \<inter> YB = 0) \<and> (YA \<union> YB = Y) \<and>
                      f``XA=YA \<and> 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) \<union> converse(restrict(g,YB))"}
   is forced by the context\<And>*)
done

(** Equipollence is an equivalence relation **)

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

(*A \<approx> 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 \<lesssim> 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 \<approx> 0 \<Longrightarrow> 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\
     \<Longrightarrow> A \<union> C \<approx> B \<union> D"
  unfolding eqpoll_def
apply (blast intro: bij_disjoint_Un)
done

subsection\<open>lesspoll: contributions by Krzysztof Grabczewski\<close>

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. x\A \ f ` x \ y"
    by (auto simp add: surj_def)
  show ?thesis
    proof
      show "(\z\A. 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)

(** \<mu> -- the least number operator [from HOL/Univ.ML] **)

lemma Least_equality:
    "\P(i); Ord(i); \x. x \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

text\<open>The proof is almost identical to the one above!\<close>
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

(*\<mu> 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 \<mu> 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

subsection\<open>Basic Properties of Cardinals\<close>

(*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 \<lesssim> Y \<Longrightarrow> |X| \<le> |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) \<Longrightarrow> |A| \<approx> 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"\<not>(j \<approx> i)"}  by  @{term"\<not>(i \<preceq> j)"}. *)
lemma CardI: "\Ord(i); \j. j \(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

text\<open>The cardinals are the initial ordinals.\<close>
lemma Card_iff_initial: "Card(K) \ Ord(K) \ (\j. j \ 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 \ 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           \<comment> \<open>degenerate case\<close>
        by (simp add: Least_0 Card_0)
    next
      case True                         \<comment> \<open>real case: \<^term>\<open>A\<close> is isomorphic to some ordinal\<close>
      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

text\<open>Since we have \<^term>\<open>|succ(nat)| \<le> |nat|\<close>, the converse of \<open>cardinal_mono\<close> fails!\<close>
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

subsection\<open>The finite cardinals\<close>

lemma cons_lepoll_consD:
"\cons(u,A) \ cons(v,B); u\A; v\B\ \ A \ B"
apply (unfold lepoll_def inj_def, safe)
apply (rule_tac x = "\x\A. 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); u\A; v\B\ \ 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 \<open>n \<in> nat\<close>
    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

(** \<lesssim>, \<prec> 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

subsection\<open>The first infinite cardinal: Omega, or nat\<close>

(*This implies Kunen's Lemma 10.6*)
lemma lt_not_lepoll:
  assumes n: "n "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

text\<open>A slightly weaker version of \<open>nat_eqpoll_iff\<close>\<close>
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 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)

subsection\<open>Towards Cardinal Arithmetic\<close>
(** 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 = "\y\cons (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

subsection\<open>Lemmas by Krzysztof Grabczewski\<close>

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

text\<open>If \<^term>\<open>A\<close> has at most \<^term>\<open>n+1\<close> elements and \<^term>\<open>a \<in> A\<close>
      then \<^term>\<open>A-{a}\<close> has at most \<^term>\<open>n\<close>.\<close>
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

text\<open>If \<^term>\<open>A\<close> has at least \<^term>\<open>n+1\<close> elements then \<^term>\<open>A-{a}\<close> has at least \<^term>\<open>n\<close>.\<close>
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 = "\x\A \ B. if x\A 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 = "\a\A \ 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 \<open>Finite and infinite sets\<close>

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. (A\n \ 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)

text\<open>The converse must hold too.\<close>
lemma Finite_Union: "\\y\X. 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);
    \<And>x B.   \<lbrakk>Finite(B); x \<notin> B; P(B)\<rbrakk> \<Longrightarrow> P(cons(x, B))\<rbrakk>
\<Longrightarrow> P(A)"
apply (erule Finite_into_Fin [THEN Fin_induct])
apply (blast intro: Fin_into_Finite)+
done

(*Sidi Ehmety.  The contrapositive says \<not>Finite(A) \<Longrightarrow> \<not>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
   \<lbrakk>\<not>Finite(A); Finite(B)\<rbrakk> \<Longrightarrow> \<not>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\
      \<Longrightarrow> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)"
apply (erule Finite_induct)
apply clarify
apply (case_tac "A=0", simp)
apply (blast del: allE, clarify)
apply (subgoal_tac "\z\A. 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

text\<open>I don't know why, but if the premise is expressed using meta-connectives
then  the simplifier cannot prove it automatically in conditional rewriting.\<close>
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 \ (\z\Z. \y. z \ y \ z \ x \ y \ x \ z \ x \ y \ Z)"
    by (simp add: wf_on_def wf_def)  \<comment> \<open>not easy to erase the duplicate \<^term>\<open>z \<in> x\<close>!\<close>
  show ?case
    proof (rule wf_onI)
      fix Z u
      assume Z: "u \ Z" "\z\Z. \y\Z. \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))))\<rbrakk>
      \<Longrightarrow> 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

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.22Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.