equal
deleted
inserted
replaced
43 (*** The following really belong in OrderType ***) |
43 (*** The following really belong in OrderType ***) |
44 |
44 |
45 lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0" |
45 lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0" |
46 apply (erule trans_induct3 [of j]) |
46 apply (erule trans_induct3 [of j]) |
47 apply (simp_all add: oadd_Limit) |
47 apply (simp_all add: oadd_Limit) |
48 apply (simp add: Union_empty_iff Limit_def lt_def) |
48 apply (simp add: Union_empty_iff Limit_def lt_def, blast) |
49 apply blast |
|
50 done |
49 done |
51 |
50 |
52 lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j" |
51 lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j" |
53 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) |
52 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) |
54 |
53 |
64 apply (frule Limit_has_1 [THEN ltD]) |
63 apply (frule Limit_has_1 [THEN ltD]) |
65 apply (rule increasing_LimitI) |
64 apply (rule increasing_LimitI) |
66 apply (rule Ord_0_lt) |
65 apply (rule Ord_0_lt) |
67 apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) |
66 apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) |
68 apply (force simp add: Union_empty_iff oadd_eq_0_iff |
67 apply (force simp add: Union_empty_iff oadd_eq_0_iff |
69 Limit_is_Ord [of j, THEN Ord_in_Ord]) |
68 Limit_is_Ord [of j, THEN Ord_in_Ord], auto) |
70 apply auto |
|
71 apply (rule_tac x="succ(x)" in bexI) |
69 apply (rule_tac x="succ(x)" in bexI) |
72 apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) |
70 apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) |
73 apply (simp add: Limit_def lt_def) |
71 apply (simp add: Limit_def lt_def) |
74 done |
72 done |
75 |
73 |
108 apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) |
106 apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) |
109 apply (rule notI) |
107 apply (rule notI) |
110 apply (erule eqpollE) |
108 apply (erule eqpollE) |
111 apply (rule succ_lepoll_natE) |
109 apply (rule succ_lepoll_natE) |
112 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] |
110 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] |
113 lepoll_trans, assumption); |
111 lepoll_trans, assumption) |
114 done |
112 done |
115 |
113 |
116 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K" |
114 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K" |
117 apply (unfold lesspoll_def) |
115 apply (unfold lesspoll_def) |
118 apply (simp add: Card_iff_initial) |
116 apply (simp add: Card_iff_initial) |
131 apply (rule allI) |
129 apply (rule allI) |
132 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) |
130 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) |
133 apply (rule allI) |
131 apply (rule allI) |
134 apply (rule impI) |
132 apply (rule impI) |
135 apply (erule conjE) |
133 apply (erule conjE) |
136 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption)) |
134 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) |
137 apply (frule Diff_sing_eqpoll, (assumption)) |
135 apply (frule Diff_sing_eqpoll, assumption) |
138 apply (erule allE) |
136 apply (erule allE) |
139 apply (erule impE, fast) |
137 apply (erule impE, fast) |
140 apply (drule subsetD, (assumption)) |
138 apply (drule subsetD, assumption) |
141 apply (drule Fin.consI, (assumption)) |
139 apply (drule Fin.consI, assumption) |
142 apply (simp add: cons_Diff) |
140 apply (simp add: cons_Diff) |
143 done |
141 done |
144 |
142 |
145 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)" |
143 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)" |
146 by (unfold Finite_def, blast intro: Finite_Fin_lemma) |
144 by (unfold Finite_def, blast intro: Finite_Fin_lemma) |