src/ZF/CardinalArith.thy
changeset 12776 249600a63ba9
parent 12667 7e6eaaa125f2
child 12820 02e2ff3e4d37
     1.1 --- a/src/ZF/CardinalArith.thy	Wed Jan 16 15:04:37 2002 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Wed Jan 16 17:52:06 2002 +0100
     1.3 @@ -102,4 +102,60 @@
     1.4       "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
     1.5  by (simp add: OUnion_def Card_0) 
     1.6  
     1.7 +lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
     1.8 +apply (unfold lesspoll_def)
     1.9 +apply (rule conjI)
    1.10 +apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
    1.11 +apply (rule notI)
    1.12 +apply (erule eqpollE)
    1.13 +apply (rule succ_lepoll_natE)
    1.14 +apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
    1.15 +                    lepoll_trans, assumption); 
    1.16 +done
    1.17 +
    1.18 +lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
    1.19 +apply (unfold lesspoll_def)
    1.20 +apply (simp add: Card_iff_initial)
    1.21 +apply (fast intro!: le_imp_lepoll ltI leI)
    1.22 +done
    1.23 +
    1.24 +lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
    1.25 +by (fast dest!: lepoll_0_is_0)
    1.26 +
    1.27 +lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
    1.28 +by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
    1.29 +
    1.30 +lemma Finite_Fin_lemma [rule_format]:
    1.31 +     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
    1.32 +apply (induct_tac "n")
    1.33 +apply (rule allI)
    1.34 +apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
    1.35 +apply (rule allI)
    1.36 +apply (rule impI)
    1.37 +apply (erule conjE)
    1.38 +apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption))
    1.39 +apply (frule Diff_sing_eqpoll, (assumption))
    1.40 +apply (erule allE)
    1.41 +apply (erule impE, fast)
    1.42 +apply (drule subsetD, (assumption))
    1.43 +apply (drule Fin.consI, (assumption))
    1.44 +apply (simp add: cons_Diff)
    1.45 +done
    1.46 +
    1.47 +lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
    1.48 +by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
    1.49 +
    1.50 +lemma lesspoll_lemma: 
    1.51 +        "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
    1.52 +apply (unfold lesspoll_def)
    1.53 +apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
    1.54 +            intro!: eqpollI elim: notE 
    1.55 +            elim!: eqpollE lepoll_trans)
    1.56 +done
    1.57 +
    1.58 +lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
    1.59 +apply (unfold Finite_def) 
    1.60 +apply (blast intro: eqpoll_trans eqpoll_sym) 
    1.61 +done
    1.62 +
    1.63  end