equal
deleted
inserted
replaced
40 lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x" |
40 lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x" |
41 apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp) |
41 apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp) |
42 apply (rule is_ub_thelub, simp) |
42 apply (rule is_ub_thelub, simp) |
43 done |
43 done |
44 |
44 |
45 lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>" |
45 lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>" |
46 by (rule UU_I, rule approx_less) |
46 by (rule UU_I, rule approx_less) |
47 |
47 |
48 lemma approx_approx1: |
48 lemma approx_approx1: |
49 "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x" |
49 "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x" |
50 apply (rule antisym_less) |
50 apply (rule antisym_less) |
111 hence "approx n\<cdot>x \<sqsubseteq> Y j" |
111 hence "approx n\<cdot>x \<sqsubseteq> Y j" |
112 using approx_less by (rule trans_less) |
112 using approx_less by (rule trans_less) |
113 thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" .. |
113 thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" .. |
114 qed |
114 qed |
115 |
115 |
116 lemma bifinite_compact_eq_approx: |
116 lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" |
117 assumes x: "compact x" |
117 by (rule admD2) simp_all |
118 shows "\<exists>i. approx i\<cdot>x = x" |
|
119 proof - |
|
120 have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp |
|
121 have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp |
|
122 obtain i where i: "x \<sqsubseteq> approx i\<cdot>x" |
|
123 using compactD2 [OF x chain less] .. |
|
124 with approx_less have "approx i\<cdot>x = x" |
|
125 by (rule antisym_less) |
|
126 thus "\<exists>i. approx i\<cdot>x = x" .. |
|
127 qed |
|
128 |
118 |
129 lemma bifinite_compact_iff: |
119 lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)" |
130 "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)" |
|
131 apply (rule iffI) |
120 apply (rule iffI) |
132 apply (erule bifinite_compact_eq_approx) |
121 apply (erule profinite_compact_eq_approx) |
133 apply (erule exE) |
122 apply (erule exE) |
134 apply (erule subst) |
123 apply (erule subst) |
135 apply (rule compact_approx) |
124 apply (rule compact_approx) |
136 done |
125 done |
137 |
126 |
142 have "P (\<Squnion>n. approx n\<cdot>x)" |
131 have "P (\<Squnion>n. approx n\<cdot>x)" |
143 by (rule admD [OF adm], simp, simp add: P) |
132 by (rule admD [OF adm], simp, simp add: P) |
144 thus "P x" by simp |
133 thus "P x" by simp |
145 qed |
134 qed |
146 |
135 |
147 lemma bifinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y" |
136 lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y" |
148 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp) |
137 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp) |
149 apply (rule lub_mono, simp, simp, simp) |
138 apply (rule lub_mono, simp, simp, simp) |
150 done |
139 done |
151 |
140 |
152 subsection {* Instance for continuous function space *} |
141 subsection {* Instance for continuous function space *} |