100 |
100 |
101 lemma Card_OUN [simp,intro,TC]: |
101 lemma Card_OUN [simp,intro,TC]: |
102 "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))" |
102 "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))" |
103 by (simp add: OUnion_def Card_0) |
103 by (simp add: OUnion_def Card_0) |
104 |
104 |
|
105 lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat" |
|
106 apply (unfold lesspoll_def) |
|
107 apply (rule conjI) |
|
108 apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) |
|
109 apply (rule notI) |
|
110 apply (erule eqpollE) |
|
111 apply (rule succ_lepoll_natE) |
|
112 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] |
|
113 lepoll_trans, assumption); |
|
114 done |
|
115 |
|
116 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K" |
|
117 apply (unfold lesspoll_def) |
|
118 apply (simp add: Card_iff_initial) |
|
119 apply (fast intro!: le_imp_lepoll ltI leI) |
|
120 done |
|
121 |
|
122 lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0" |
|
123 by (fast dest!: lepoll_0_is_0) |
|
124 |
|
125 lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0" |
|
126 by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) |
|
127 |
|
128 lemma Finite_Fin_lemma [rule_format]: |
|
129 "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)" |
|
130 apply (induct_tac "n") |
|
131 apply (rule allI) |
|
132 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) |
|
133 apply (rule allI) |
|
134 apply (rule impI) |
|
135 apply (erule conjE) |
|
136 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption)) |
|
137 apply (frule Diff_sing_eqpoll, (assumption)) |
|
138 apply (erule allE) |
|
139 apply (erule impE, fast) |
|
140 apply (drule subsetD, (assumption)) |
|
141 apply (drule Fin.consI, (assumption)) |
|
142 apply (simp add: cons_Diff) |
|
143 done |
|
144 |
|
145 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)" |
|
146 by (unfold Finite_def, blast intro: Finite_Fin_lemma) |
|
147 |
|
148 lemma lesspoll_lemma: |
|
149 "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0" |
|
150 apply (unfold lesspoll_def) |
|
151 apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] |
|
152 intro!: eqpollI elim: notE |
|
153 elim!: eqpollE lepoll_trans) |
|
154 done |
|
155 |
|
156 lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)" |
|
157 apply (unfold Finite_def) |
|
158 apply (blast intro: eqpoll_trans eqpoll_sym) |
|
159 done |
|
160 |
105 end |
161 end |