equal
deleted
inserted
replaced
184 unfolding approx_upper_pd_def |
184 unfolding approx_upper_pd_def |
185 by (rule upper_pd.completion_approx_eq_principal) |
185 by (rule upper_pd.completion_approx_eq_principal) |
186 |
186 |
187 lemma compact_imp_upper_principal: |
187 lemma compact_imp_upper_principal: |
188 "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t" |
188 "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t" |
189 apply (drule bifinite_compact_eq_approx) |
189 by (rule upper_pd.compact_imp_principal) |
190 apply (erule exE) |
|
191 apply (erule subst) |
|
192 apply (cut_tac n=i and xs=xs in approx_eq_upper_principal) |
|
193 apply fast |
|
194 done |
|
195 |
190 |
196 lemma upper_principal_induct: |
191 lemma upper_principal_induct: |
197 "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs" |
192 "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs" |
198 by (rule upper_pd.principal_induct) |
193 by (rule upper_pd.principal_induct) |
199 |
194 |