Quelle Cardinal_aux.thy Sprache: Isabelle

(*  Title:      ZF/AC/Cardinal_aux.thy
    Author:     Krzysztof Grabczewski

Auxiliary lemmas concerning cardinalities.
*)

theory Cardinal_aux imports AC_Equiv begin

lemma Diff_lepoll: "\A \ succ(m); B \ A; B\0\ \ A-B \ m"
apply (rule not_emptyE, assumption)
apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll])
done

(* ********************************************************************** *)
(* Lemmas involving ordinals and cardinalities used in the proofs         *)
(* concerning AC16 and DC                                                 *)
(* ********************************************************************** *)

(* j=|A| *)
lemma lepoll_imp_ex_le_eqpoll:
     "\A \ i; Ord(i)\ \ \j. j \ i \ A \ j"
by (blast intro!: lepoll_cardinal_le well_ord_Memrel
                  well_ord_cardinal_eqpoll [THEN eqpoll_sym]
          dest: lepoll_well_ord)

(* j=|A| *)
lemma lesspoll_imp_ex_lt_eqpoll:
     "\A \ i; Ord(i)\ \ \j. j A \ j"
by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)

lemma Un_eqpoll_Inf_Ord:
  assumes A: "A \ i" and B: "B \ i" and NFI: "\ Finite(i)" and i: "Ord(i)"
  shows "A \ B \ i"
proof (rule eqpollI)
  have AB: "A \ B" using A B by (blast intro: eqpoll_sym eqpoll_trans)
  have "2 \ nat"
    by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat])
  also have "... \ i"
    by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+
  also have "... \ A" by (blast intro: eqpoll_sym A)
  finally have "2 \ A" .
  have ICI: "InfCard(|i|)"
    by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i)
  have "A \ B \ A + B" by (rule Un_lepoll_sum)
  also have "... \ A \ B"
    by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] \<open>2 \<lesssim> A\<close>])
  also have "... \ i \ i"
    by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B)
  also have "... \ i"
    by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i)
  finally show "A \ B \ i" .
next
  have "i \ A" by (blast intro: A eqpoll_sym)
  also have "... \ A \ B" by (blast intro: subset_imp_lepoll)
  finally show "i \ A \ B" .
qed

schematic_goal paired_bij: "?f \ bij({{y,z}. y \ x}, x)"
apply (rule RepFun_bijective)
apply (simp add: doubleton_eq_iff, blast)
done

lemma paired_eqpoll: "{{y,z}. y \ x} \ x"
by (unfold eqpoll_def, fast intro!: paired_bij)

lemma ex_eqpoll_disjoint: "\B. B \ A \ B \ C = 0"
by (fast intro!: paired_eqpoll equals0I elim: mem_asym)

(*Finally we reach this result.  Surely there's a simpler proof?*)
lemma Un_lepoll_Inf_Ord:
     "\A \ i; B \ i; \Finite(i); Ord(i)\ \ A \ B \ i"
apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
apply (erule conjE)
apply (drule lepoll_trans)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+))
apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll)
done

lemma Least_in_Ord: "\P(i); i \ j; Ord(j)\ \ (\ i. P(i)) \ j"
apply (erule Least_le [THEN leE])
apply (erule Ord_in_Ord, assumption)
apply (erule ltE)
apply (fast dest: OrdmemD)
apply (erule subst_elem, assumption)
done

lemma Diff_first_lepoll:
     "\well_ord(x,r); y \ x; y \ succ(n); n \ nat\
      \<Longrightarrow> y - {THE b. first(b,y,r)} \<lesssim> n"
apply (case_tac "y=0", simp add: empty_lepollI)
apply (fast intro!: Diff_sing_lepoll the_first_in)
done

lemma UN_subset_split:
     "(\x \ X. P(x)) \ (\x \ X. P(x)-Q(x)) \ (\x \ X. Q(x))"
by blast

lemma UN_sing_lepoll: "Ord(a) \ (\x \ a. {P(x)}) \ a"
  unfolding lepoll_def
apply (rule_tac x = "\z \ (\x \ a. {P (x) }) . (\ i. P (i) =z) " in exI)
apply (rule_tac d = "\z. P (z) " in lam_injective)
apply (fast intro!: Least_in_Ord)
apply (fast intro: LeastI elim!: Ord_in_Ord)
done

lemma UN_fun_lepoll_lemma [rule_format]:
     "\well_ord(T, R); \Finite(a); Ord(a); n \ nat\
      \<Longrightarrow> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n \<and> f`b \<subseteq> T) \<longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a"
apply (induct_tac "n")
apply (rule allI)
apply (rule impI)
apply (rule_tac b = "\b \ a. f`b" in subst)
apply (rule_tac [2] empty_lepollI)
apply (rule equals0I [symmetric], clarify)
apply (fast dest: lepoll_0_is_0 [THEN subst])
apply (rule allI)
apply (rule impI)
apply (erule_tac x = "\x \ a. f`x - {THE b. first (b,f`x,R) }" in allE)
apply (erule impE, simp)
apply (fast intro!: Diff_first_lepoll, simp)
apply (rule UN_subset_split [THEN subset_imp_lepoll, THEN lepoll_trans])
apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll)
done

lemma UN_fun_lepoll:
     "\\b \ a. f`b \ n \ f`b \ T; well_ord(T, R);
         \<not>Finite(a); Ord(a); n \<in> nat\<rbrakk> \<Longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a"
by (blast intro: UN_fun_lepoll_lemma)

lemma UN_lepoll:
     "\\b \ a. F(b) \ n \ F(b) \ T; well_ord(T, R);
         \<not>Finite(a); Ord(a); n \<in> nat\<rbrakk>
      \<Longrightarrow> (\<Union>b \<in> a. F(b)) \<lesssim> a"
apply (rule rev_mp)
apply (rule_tac f="\b \ a. F (b)" in UN_fun_lepoll)
apply auto
done

lemma UN_eq_UN_Diffs:
     "Ord(a) \ (\b \ a. F(b)) = (\b \ a. F(b) - (\c \ b. F(c)))"
apply (rule equalityI)
prefer 2 apply fast
apply (rule subsetI)
apply (erule UN_E)
apply (rule UN_I)
apply (rule_tac P = "\z. x \ F (z) " in Least_in_Ord, (assumption+))
apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify)
apply (erule_tac P = "\z. x \ F (z) " and i = c in less_LeastE)
apply (blast intro: Ord_Least ltI)
done

lemma lepoll_imp_eqpoll_subset:
     "a \ X \ \Y. Y \ X \ a \ Y"
apply (unfold lepoll_def eqpoll_def, clarify)
apply (blast intro: restrict_bij
             dest: inj_is_fun [THEN fun_is_rel, THEN image_subset])
done

(* ********************************************************************** *)
(* Diff_lesspoll_eqpoll_Card                                              *)
(* ********************************************************************** *)

lemma Diff_lesspoll_eqpoll_Card_lemma:
     "\A\a; \Finite(a); Card(a); B \ a; A-B \ a\ \ P"
apply (elim lesspoll_imp_ex_lt_eqpoll [THEN exE] Card_is_Ord conjE)
apply (frule_tac j=xa in Un_upper1_le [OF lt_Ord lt_Ord], assumption)
apply (frule_tac j=xa in Un_upper2_le [OF lt_Ord lt_Ord], assumption)
apply (drule Un_least_lt, assumption)
apply (drule eqpoll_imp_lepoll [THEN lepoll_trans],
       rule le_imp_lepoll, assumption)+
apply (case_tac "Finite(x \ xa)")
txt\<open>finite case\<close>
apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+)
apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
apply (fast dest: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_Finite])
txt\<open>infinite case\<close>
apply (drule Un_lepoll_Inf_Ord, (assumption+))
apply (blast intro: le_Ord2)
apply (drule lesspoll_trans1
             [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans]
                 lt_Card_imp_lesspoll], assumption+)
apply (simp add: lesspoll_def)
done

lemma Diff_lesspoll_eqpoll_Card:
     "\A \ a; \Finite(a); Card(a); B \ a\ \ A - B \ a"
apply (rule ccontr)
apply (rule Diff_lesspoll_eqpoll_Card_lemma, (assumption+))
apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2]
                    subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (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.