156 by (rule lower_pd_minimal [THEN UU_I, symmetric]) |
156 by (rule lower_pd_minimal [THEN UU_I, symmetric]) |
157 |
157 |
158 |
158 |
159 subsection {* Approximation *} |
159 subsection {* Approximation *} |
160 |
160 |
161 instance lower_pd :: (profinite) approx .. |
161 instantiation lower_pd :: (profinite) profinite |
162 |
162 begin |
163 defs (overloaded) |
163 |
164 approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx" |
164 definition |
165 |
165 approx_lower_pd_def: "approx = lower_pd.completion_approx" |
166 instance lower_pd :: (profinite) profinite |
166 |
|
167 instance |
167 apply (intro_classes, unfold approx_lower_pd_def) |
168 apply (intro_classes, unfold approx_lower_pd_def) |
168 apply (simp add: lower_pd.chain_completion_approx) |
169 apply (simp add: lower_pd.chain_completion_approx) |
169 apply (rule lower_pd.lub_completion_approx) |
170 apply (rule lower_pd.lub_completion_approx) |
170 apply (rule lower_pd.completion_approx_idem) |
171 apply (rule lower_pd.completion_approx_idem) |
171 apply (rule lower_pd.finite_fixes_completion_approx) |
172 apply (rule lower_pd.finite_fixes_completion_approx) |
172 done |
173 done |
|
174 |
|
175 end |
173 |
176 |
174 instance lower_pd :: (bifinite) bifinite .. |
177 instance lower_pd :: (bifinite) bifinite .. |
175 |
178 |
176 lemma approx_lower_principal [simp]: |
179 lemma approx_lower_principal [simp]: |
177 "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)" |
180 "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)" |