149 |
149 |
150 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" |
150 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" |
151 by (rule Rep_convex_pd [simplified]) |
151 by (rule Rep_convex_pd [simplified]) |
152 |
152 |
153 lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys" |
153 lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys" |
154 unfolding less_convex_pd_def less_set_def . |
154 unfolding less_convex_pd_def less_set_eq . |
155 |
155 |
156 |
156 |
157 subsection {* Principal ideals *} |
157 subsection {* Principal ideals *} |
158 |
158 |
159 definition |
159 definition |
177 apply (rule finite_range_approx_pd) |
177 apply (rule finite_range_approx_pd) |
178 apply (rule ex_approx_pd_eq) |
178 apply (rule ex_approx_pd_eq) |
179 apply (rule ideal_Rep_convex_pd) |
179 apply (rule ideal_Rep_convex_pd) |
180 apply (rule cont_Rep_convex_pd) |
180 apply (rule cont_Rep_convex_pd) |
181 apply (rule Rep_convex_principal) |
181 apply (rule Rep_convex_principal) |
182 apply (simp only: less_convex_pd_def less_set_def) |
182 apply (simp only: less_convex_pd_def less_set_eq) |
183 done |
183 done |
184 |
184 |
185 lemma convex_principal_less_iff [simp]: |
185 lemma convex_principal_less_iff [simp]: |
186 "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)" |
186 "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)" |
187 unfolding less_convex_pd_def Rep_convex_principal less_set_def |
187 unfolding less_convex_pd_def Rep_convex_principal less_set_eq |
188 by (fast intro: convex_le_refl elim: convex_le_trans) |
188 by (fast intro: convex_le_refl elim: convex_le_trans) |
189 |
189 |
190 lemma convex_principal_mono: |
190 lemma convex_principal_mono: |
191 "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u" |
191 "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u" |
192 by (rule convex_principal_less_iff [THEN iffD2]) |
192 by (rule convex_principal_less_iff [THEN iffD2]) |