author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 35901  12f09bf2c77f 
child 37770  cddb3106adb8 
permissions  rwrr 
25904  1 
(* Title: HOLCF/ConvexPD.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Convex powerdomain *} 

6 

7 
theory ConvexPD 

8 
imports UpperPD LowerPD 

9 
begin 

10 

11 
subsection {* Basis preorder *} 

12 

13 
definition 

14 
convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where 

15 
"convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)" 

16 

17 
lemma convex_le_refl [simp]: "t \<le>\<natural> t" 

18 
unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl) 

19 

20 
lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v" 

21 
unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans) 

22 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29990
diff
changeset

23 
interpretation convex_le: preorder convex_le 
25904  24 
by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans) 
25 

26 
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t" 

27 
unfolding convex_le_def Rep_PDUnit by simp 

28 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

29 
lemma PDUnit_convex_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y" 
25904  30 
unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono) 
31 

32 
lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v" 

33 
unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono) 

34 

35 
lemma convex_le_PDUnit_PDUnit_iff [simp]: 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

36 
"(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b" 
25904  37 
unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast 
38 

39 
lemma convex_le_PDUnit_lemma1: 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

40 
"(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. a \<sqsubseteq> b)" 
25904  41 
unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit 
42 
using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast 

43 

44 
lemma convex_le_PDUnit_PDPlus_iff [simp]: 

45 
"(PDUnit a \<le>\<natural> PDPlus t u) = (PDUnit a \<le>\<natural> t \<and> PDUnit a \<le>\<natural> u)" 

46 
unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast 

47 

48 
lemma convex_le_PDUnit_lemma2: 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

49 
"(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. a \<sqsubseteq> b)" 
25904  50 
unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit 
51 
using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast 

52 

53 
lemma convex_le_PDPlus_PDUnit_iff [simp]: 

54 
"(PDPlus t u \<le>\<natural> PDUnit a) = (t \<le>\<natural> PDUnit a \<and> u \<le>\<natural> PDUnit a)" 

55 
unfolding convex_le_PDUnit_lemma2 Rep_PDPlus by fast 

56 

57 
lemma convex_le_PDPlus_lemma: 

58 
assumes z: "PDPlus t u \<le>\<natural> z" 

59 
shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w" 

60 
proof (intro exI conjI) 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

61 
let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. a \<sqsubseteq> b}" 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

62 
let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. a \<sqsubseteq> b}" 
25904  63 
let ?v = "Abs_pd_basis ?A" 
64 
let ?w = "Abs_pd_basis ?B" 

65 
have Rep_v: "Rep_pd_basis ?v = ?A" 

66 
apply (rule Abs_pd_basis_inverse) 

67 
apply (rule Rep_pd_basis_nonempty [of t, folded ex_in_conv, THEN exE]) 

68 
apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify) 

69 
apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE) 

70 
apply (simp add: pd_basis_def) 

71 
apply fast 

72 
done 

73 
have Rep_w: "Rep_pd_basis ?w = ?B" 

74 
apply (rule Abs_pd_basis_inverse) 

75 
apply (rule Rep_pd_basis_nonempty [of u, folded ex_in_conv, THEN exE]) 

76 
apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify) 

77 
apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE) 

78 
apply (simp add: pd_basis_def) 

79 
apply fast 

80 
done 

81 
show "z = PDPlus ?v ?w" 

82 
apply (insert z) 

83 
apply (simp add: convex_le_def, erule conjE) 

84 
apply (simp add: Rep_pd_basis_inject [symmetric] Rep_PDPlus) 

85 
apply (simp add: Rep_v Rep_w) 

86 
apply (rule equalityI) 

87 
apply (rule subsetI) 

88 
apply (simp only: upper_le_def) 

89 
apply (drule (1) bspec, erule bexE) 

90 
apply (simp add: Rep_PDPlus) 

91 
apply fast 

92 
apply fast 

93 
done 

94 
show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w" 

95 
apply (insert z) 

96 
apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w) 

97 
apply fast+ 

98 
done 

99 
qed 

100 

101 
lemma convex_le_induct [induct set: convex_le]: 

102 
assumes le: "t \<le>\<natural> u" 

103 
assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v" 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

104 
assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" 
25904  105 
assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)" 
106 
shows "P t u" 

107 
using le apply (induct t arbitrary: u rule: pd_basis_induct) 

108 
apply (erule rev_mp) 

109 
apply (induct_tac u rule: pd_basis_induct1) 

110 
apply (simp add: 3) 

111 
apply (simp, clarify, rename_tac a b t) 

112 
apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)") 

113 
apply (simp add: PDPlus_absorb) 

114 
apply (erule (1) 4 [OF 3]) 

115 
apply (drule convex_le_PDPlus_lemma, clarify) 

116 
apply (simp add: 4) 

117 
done 

118 

27405  119 
lemma pd_take_convex_chain: 
120 
"pd_take n t \<le>\<natural> pd_take (Suc n) t" 

25904  121 
apply (induct t rule: pd_basis_induct) 
27289  122 
apply (simp add: compact_basis.take_chain) 
25904  123 
apply (simp add: PDPlus_convex_mono) 
124 
done 

125 

27405  126 
lemma pd_take_convex_le: "pd_take i t \<le>\<natural> t" 
25904  127 
apply (induct t rule: pd_basis_induct) 
27289  128 
apply (simp add: compact_basis.take_less) 
25904  129 
apply (simp add: PDPlus_convex_mono) 
130 
done 

131 

27405  132 
lemma pd_take_convex_mono: 
133 
"t \<le>\<natural> u \<Longrightarrow> pd_take n t \<le>\<natural> pd_take n u" 

25904  134 
apply (erule convex_le_induct) 
135 
apply (erule (1) convex_le_trans) 

27289  136 
apply (simp add: compact_basis.take_mono) 
25904  137 
apply (simp add: PDPlus_convex_mono) 
138 
done 

139 

140 

141 
subsection {* Type definition *} 

142 

27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

143 
typedef (open) 'a convex_pd = 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

144 
"{S::'a pd_basis set. convex_le.ideal S}" 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

145 
by (fast intro: convex_le.ideal_principal) 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

146 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

147 
instantiation convex_pd :: (profinite) below 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

148 
begin 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

149 

5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

150 
definition 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

151 
"x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y" 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

152 

5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

153 
instance .. 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

154 
end 
25904  155 

27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

156 
instance convex_pd :: (profinite) po 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

157 
by (rule convex_le.typedef_ideal_po 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

158 
[OF type_definition_convex_pd below_convex_pd_def]) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

159 

5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

160 
instance convex_pd :: (profinite) cpo 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

161 
by (rule convex_le.typedef_ideal_cpo 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

162 
[OF type_definition_convex_pd below_convex_pd_def]) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

163 

5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

164 
lemma Rep_convex_pd_lub: 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

165 
"chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))" 
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

166 
by (rule convex_le.typedef_ideal_rep_contlub 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

167 
[OF type_definition_convex_pd below_convex_pd_def]) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

168 

5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

169 
lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" 
26927  170 
by (rule Rep_convex_pd [unfolded mem_Collect_eq]) 
25904  171 

172 
definition 

173 
convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where 

27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

174 
"convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}" 
25904  175 

176 
lemma Rep_convex_principal: 

27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

177 
"Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}" 
25904  178 
unfolding convex_principal_def 
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

179 
by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal) 
25904  180 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29990
diff
changeset

181 
interpretation convex_pd: 
29237  182 
ideal_completion convex_le pd_take convex_principal Rep_convex_pd 
25904  183 
apply unfold_locales 
27405  184 
apply (rule pd_take_convex_le) 
185 
apply (rule pd_take_idem) 

186 
apply (erule pd_take_convex_mono) 

187 
apply (rule pd_take_convex_chain) 

188 
apply (rule finite_range_pd_take) 

189 
apply (rule pd_take_covers) 

26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

190 
apply (rule ideal_Rep_convex_pd) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

191 
apply (erule Rep_convex_pd_lub) 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

192 
apply (rule Rep_convex_principal) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

193 
apply (simp only: below_convex_pd_def) 
25904  194 
done 
195 

27289  196 
text {* Convex powerdomain is pointed *} 
25904  197 

198 
lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys" 

199 
by (induct ys rule: convex_pd.principal_induct, simp, simp) 

200 

201 
instance convex_pd :: (bifinite) pcpo 

26927  202 
by intro_classes (fast intro: convex_pd_minimal) 
25904  203 

204 
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)" 

205 
by (rule convex_pd_minimal [THEN UU_I, symmetric]) 

206 

27289  207 
text {* Convex powerdomain is profinite *} 
25904  208 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

209 
instantiation convex_pd :: (profinite) profinite 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

210 
begin 
25904  211 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

212 
definition 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

213 
approx_convex_pd_def: "approx = convex_pd.completion_approx" 
26927  214 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

215 
instance 
26927  216 
apply (intro_classes, unfold approx_convex_pd_def) 
27310  217 
apply (rule convex_pd.chain_completion_approx) 
26927  218 
apply (rule convex_pd.lub_completion_approx) 
219 
apply (rule convex_pd.completion_approx_idem) 

220 
apply (rule convex_pd.finite_fixes_completion_approx) 

221 
done 

222 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

223 
end 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26927
diff
changeset

224 

26927  225 
instance convex_pd :: (bifinite) bifinite .. 
25904  226 

227 
lemma approx_convex_principal [simp]: 

27405  228 
"approx n\<cdot>(convex_principal t) = convex_principal (pd_take n t)" 
25904  229 
unfolding approx_convex_pd_def 
26927  230 
by (rule convex_pd.completion_approx_principal) 
25904  231 

232 
lemma approx_eq_convex_principal: 

27405  233 
"\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (pd_take n t)" 
25904  234 
unfolding approx_convex_pd_def 
26927  235 
by (rule convex_pd.completion_approx_eq_principal) 
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

236 

25904  237 

26927  238 
subsection {* Monadic unit and plus *} 
25904  239 

240 
definition 

241 
convex_unit :: "'a \<rightarrow> 'a convex_pd" where 

242 
"convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))" 

243 

244 
definition 

245 
convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where 

246 
"convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u. 

247 
convex_principal (PDPlus t u)))" 

248 

249 
abbreviation 

250 
convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd" 

251 
(infixl "+\<natural>" 65) where 

252 
"xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" 

253 

26927  254 
syntax 
255 
"_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>") 

256 

257 
translations 

258 
"{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>" 

259 
"{x}\<natural>" == "CONST convex_unit\<cdot>x" 

260 

261 
lemma convex_unit_Rep_compact_basis [simp]: 

262 
"{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)" 

263 
unfolding convex_unit_def 

27289  264 
by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono) 
26927  265 

25904  266 
lemma convex_plus_principal [simp]: 
26927  267 
"convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)" 
25904  268 
unfolding convex_plus_def 
269 
by (simp add: convex_pd.basis_fun_principal 

270 
convex_pd.basis_fun_mono PDPlus_convex_mono) 

271 

26927  272 
lemma approx_convex_unit [simp]: 
273 
"approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>" 

27289  274 
apply (induct x rule: compact_basis.principal_induct, simp) 
26927  275 
apply (simp add: approx_Rep_compact_basis) 
276 
done 

277 

25904  278 
lemma approx_convex_plus [simp]: 
26927  279 
"approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys" 
27289  280 
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) 
25904  281 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

282 
interpretation convex_add!: semilattice convex_add proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

283 
fix xs ys zs :: "'a convex_pd" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

284 
show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

285 
apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

286 
apply (rule_tac x=zs in convex_pd.principal_induct, simp) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

287 
apply (simp add: PDPlus_assoc) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

288 
done 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

289 
show "xs +\<natural> ys = ys +\<natural> xs" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

290 
apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

291 
apply (simp add: PDPlus_commute) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

292 
done 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

293 
show "xs +\<natural> xs = xs" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

294 
apply (induct xs rule: convex_pd.principal_induct, simp) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

295 
apply (simp add: PDPlus_absorb) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

296 
done 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

297 
qed 
26927  298 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

299 
lemmas convex_plus_assoc = convex_add.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

300 
lemmas convex_plus_commute = convex_add.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

301 
lemmas convex_plus_absorb = convex_add.idem 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

302 
lemmas convex_plus_left_commute = convex_add.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

303 
lemmas convex_plus_left_absorb = convex_add.left_idem 
26927  304 

29990
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

305 
text {* Useful for @{text "simp add: convex_plus_ac"} *} 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

306 
lemmas convex_plus_ac = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

307 
convex_plus_assoc convex_plus_commute convex_plus_left_commute 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

308 

b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

309 
text {* Useful for @{text "simp only: convex_plus_aci"} *} 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

310 
lemmas convex_plus_aci = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

311 
convex_plus_ac convex_plus_absorb convex_plus_left_absorb 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

312 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

313 
lemma convex_unit_below_plus_iff [simp]: 
26927  314 
"{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs" 
25904  315 
apply (rule iffI) 
316 
apply (subgoal_tac 

26927  317 
"adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)") 
25925  318 
apply (drule admD, rule chain_approx) 
25904  319 
apply (drule_tac f="approx i" in monofun_cfun_arg) 
27289  320 
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp) 
321 
apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp) 

322 
apply (cut_tac x="approx i\<cdot>zs" in convex_pd.compact_imp_principal, simp) 

25904  323 
apply (clarify, simp) 
324 
apply simp 

325 
apply simp 

326 
apply (erule conjE) 

26927  327 
apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric]) 
25904  328 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 
329 
done 

330 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

331 
lemma convex_plus_below_unit_iff [simp]: 
26927  332 
"xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>" 
25904  333 
apply (rule iffI) 
334 
apply (subgoal_tac 

26927  335 
"adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)") 
25925  336 
apply (drule admD, rule chain_approx) 
25904  337 
apply (drule_tac f="approx i" in monofun_cfun_arg) 
27289  338 
apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp) 
339 
apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp) 

340 
apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp) 

25904  341 
apply (clarify, simp) 
342 
apply simp 

343 
apply simp 

344 
apply (erule conjE) 

26927  345 
apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric]) 
25904  346 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 
347 
done 

348 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

349 
lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y" 
26927  350 
apply (rule iffI) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

351 
apply (rule profinite_below_ext) 
26927  352 
apply (drule_tac f="approx i" in monofun_cfun_arg, simp) 
27289  353 
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp) 
354 
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp) 

355 
apply clarsimp 

26927  356 
apply (erule monofun_cfun_arg) 
357 
done 

358 

359 
lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y" 

360 
unfolding po_eq_conv by simp 

361 

362 
lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>" 

363 
unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp 

364 

365 
lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>" 

366 
unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff) 

367 

368 
lemma compact_convex_unit_iff [simp]: 

369 
"compact {x}\<natural> \<longleftrightarrow> compact x" 

27309  370 
unfolding profinite_compact_iff by simp 
26927  371 

372 
lemma compact_convex_plus [simp]: 

373 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)" 

27289  374 
by (auto dest!: convex_pd.compact_imp_principal) 
26927  375 

25904  376 

377 
subsection {* Induction rules *} 

378 

379 
lemma convex_pd_induct1: 

380 
assumes P: "adm P" 

26927  381 
assumes unit: "\<And>x. P {x}\<natural>" 
382 
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)" 

25904  383 
shows "P (xs::'a convex_pd)" 
27289  384 
apply (induct xs rule: convex_pd.principal_induct, rule P) 
385 
apply (induct_tac a rule: pd_basis_induct1) 

25904  386 
apply (simp only: convex_unit_Rep_compact_basis [symmetric]) 
387 
apply (rule unit) 

388 
apply (simp only: convex_unit_Rep_compact_basis [symmetric] 

389 
convex_plus_principal [symmetric]) 

390 
apply (erule insert [OF unit]) 

391 
done 

392 

393 
lemma convex_pd_induct: 

394 
assumes P: "adm P" 

26927  395 
assumes unit: "\<And>x. P {x}\<natural>" 
396 
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)" 

25904  397 
shows "P (xs::'a convex_pd)" 
27289  398 
apply (induct xs rule: convex_pd.principal_induct, rule P) 
399 
apply (induct_tac a rule: pd_basis_induct) 

25904  400 
apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit) 
401 
apply (simp only: convex_plus_principal [symmetric] plus) 

402 
done 

403 

404 

405 
subsection {* Monadic bind *} 

406 

407 
definition 

408 
convex_bind_basis :: 

409 
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where 

410 
"convex_bind_basis = fold_pd 

411 
(\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) 

26927  412 
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)" 
25904  413 

26927  414 
lemma ACI_convex_bind: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35901
diff
changeset

415 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)" 
25904  416 
apply unfold_locales 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25925
diff
changeset

417 
apply (simp add: convex_plus_assoc) 
25904  418 
apply (simp add: convex_plus_commute) 
29990
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

419 
apply (simp add: eta_cfun) 
25904  420 
done 
421 

422 
lemma convex_bind_basis_simps [simp]: 

423 
"convex_bind_basis (PDUnit a) = 

424 
(\<Lambda> f. f\<cdot>(Rep_compact_basis a))" 

425 
"convex_bind_basis (PDPlus t u) = 

26927  426 
(\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)" 
25904  427 
unfolding convex_bind_basis_def 
428 
apply  

26927  429 
apply (rule fold_pd_PDUnit [OF ACI_convex_bind]) 
430 
apply (rule fold_pd_PDPlus [OF ACI_convex_bind]) 

25904  431 
done 
432 

433 
lemma monofun_LAM: 

434 
"\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

435 
by (simp add: expand_cfun_below) 
25904  436 

437 
lemma convex_bind_basis_mono: 

438 
"t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u" 

439 
apply (erule convex_le_induct) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

440 
apply (erule (1) below_trans) 
27289  441 
apply (simp add: monofun_LAM monofun_cfun) 
442 
apply (simp add: monofun_LAM monofun_cfun) 

25904  443 
done 
444 

445 
definition 

446 
convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where 

447 
"convex_bind = convex_pd.basis_fun convex_bind_basis" 

448 

449 
lemma convex_bind_principal [simp]: 

450 
"convex_bind\<cdot>(convex_principal t) = convex_bind_basis t" 

451 
unfolding convex_bind_def 

452 
apply (rule convex_pd.basis_fun_principal) 

453 
apply (erule convex_bind_basis_mono) 

454 
done 

455 

456 
lemma convex_bind_unit [simp]: 

26927  457 
"convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x" 
27289  458 
by (induct x rule: compact_basis.principal_induct, simp, simp) 
25904  459 

460 
lemma convex_bind_plus [simp]: 

26927  461 
"convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f" 
27289  462 
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) 
25904  463 

464 
lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 

465 
unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit) 

466 

467 

468 
subsection {* Map and join *} 

469 

470 
definition 

471 
convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where 

26927  472 
"convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))" 
25904  473 

474 
definition 

475 
convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where 

476 
"convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 

477 

478 
lemma convex_map_unit [simp]: 

479 
"convex_map\<cdot>f\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(f\<cdot>x)" 

480 
unfolding convex_map_def by simp 

481 

482 
lemma convex_map_plus [simp]: 

26927  483 
"convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys" 
25904  484 
unfolding convex_map_def by simp 
485 

486 
lemma convex_join_unit [simp]: 

26927  487 
"convex_join\<cdot>{xs}\<natural> = xs" 
25904  488 
unfolding convex_join_def by simp 
489 

490 
lemma convex_join_plus [simp]: 

26927  491 
"convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss" 
25904  492 
unfolding convex_join_def by simp 
493 

494 
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 

495 
by (induct xs rule: convex_pd_induct, simp_all) 

496 

33808  497 
lemma convex_map_ID: "convex_map\<cdot>ID = ID" 
498 
by (simp add: expand_cfun_eq ID_def convex_map_ident) 

499 

25904  500 
lemma convex_map_map: 
501 
"convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 

502 
by (induct xs rule: convex_pd_induct, simp_all) 

503 

504 
lemma convex_join_map_unit: 

505 
"convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs" 

506 
by (induct xs rule: convex_pd_induct, simp_all) 

507 

508 
lemma convex_join_map_join: 

509 
"convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)" 

510 
by (induct xsss rule: convex_pd_induct, simp_all) 

511 

512 
lemma convex_join_map_map: 

513 
"convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) = 

514 
convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)" 

515 
by (induct xss rule: convex_pd_induct, simp_all) 

516 

517 
lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs" 

518 
by (induct xs rule: convex_pd_induct, simp_all) 

519 

35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

520 
lemma ep_pair_convex_map: 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

521 
"ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)" 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

522 
apply default 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

523 
apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) 
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

524 
apply (induct_tac y rule: convex_pd_induct) 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

525 
apply (simp_all add: ep_pair.e_p_below monofun_cfun) 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

526 
done 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

527 

8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

528 
lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)" 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

529 
apply default 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

530 
apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) 
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

531 
apply (induct_tac x rule: convex_pd_induct) 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
34973
diff
changeset

532 
apply (simp_all add: deflation.below monofun_cfun) 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

533 
done 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

534 

25904  535 

536 
subsection {* Conversions to other powerdomains *} 

537 

538 
text {* Convex to upper *} 

539 

540 
lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u" 

541 
unfolding convex_le_def by simp 

542 

543 
definition 

544 
convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where 

545 
"convex_to_upper = convex_pd.basis_fun upper_principal" 

546 

547 
lemma convex_to_upper_principal [simp]: 

548 
"convex_to_upper\<cdot>(convex_principal t) = upper_principal t" 

549 
unfolding convex_to_upper_def 

550 
apply (rule convex_pd.basis_fun_principal) 

27289  551 
apply (rule upper_pd.principal_mono) 
25904  552 
apply (erule convex_le_imp_upper_le) 
553 
done 

554 

555 
lemma convex_to_upper_unit [simp]: 

26927  556 
"convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>" 
27289  557 
by (induct x rule: compact_basis.principal_induct, simp, simp) 
25904  558 

559 
lemma convex_to_upper_plus [simp]: 

26927  560 
"convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys" 
27289  561 
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) 
25904  562 

563 
lemma approx_convex_to_upper: 

564 
"approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)" 

565 
by (induct xs rule: convex_pd_induct, simp, simp, simp) 

566 

27289  567 
lemma convex_to_upper_bind [simp]: 
568 
"convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) = 

569 
upper_bind\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper oo f)" 

570 
by (induct xs rule: convex_pd_induct, simp, simp, simp) 

571 

572 
lemma convex_to_upper_map [simp]: 

573 
"convex_to_upper\<cdot>(convex_map\<cdot>f\<cdot>xs) = upper_map\<cdot>f\<cdot>(convex_to_upper\<cdot>xs)" 

574 
by (simp add: convex_map_def upper_map_def cfcomp_LAM) 

575 

576 
lemma convex_to_upper_join [simp]: 

577 
"convex_to_upper\<cdot>(convex_join\<cdot>xss) = 

578 
upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper" 

579 
by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun) 

580 

25904  581 
text {* Convex to lower *} 
582 

583 
lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u" 

584 
unfolding convex_le_def by simp 

585 

586 
definition 

587 
convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where 

588 
"convex_to_lower = convex_pd.basis_fun lower_principal" 

589 

590 
lemma convex_to_lower_principal [simp]: 

591 
"convex_to_lower\<cdot>(convex_principal t) = lower_principal t" 

592 
unfolding convex_to_lower_def 

593 
apply (rule convex_pd.basis_fun_principal) 

27289  594 
apply (rule lower_pd.principal_mono) 
25904  595 
apply (erule convex_le_imp_lower_le) 
596 
done 

597 

598 
lemma convex_to_lower_unit [simp]: 

26927  599 
"convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>" 
27289  600 
by (induct x rule: compact_basis.principal_induct, simp, simp) 
25904  601 

602 
lemma convex_to_lower_plus [simp]: 

26927  603 
"convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys" 
27289  604 
by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) 
25904  605 

606 
lemma approx_convex_to_lower: 

607 
"approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)" 

608 
by (induct xs rule: convex_pd_induct, simp, simp, simp) 

609 

27289  610 
lemma convex_to_lower_bind [simp]: 
611 
"convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) = 

612 
lower_bind\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower oo f)" 

613 
by (induct xs rule: convex_pd_induct, simp, simp, simp) 

614 

615 
lemma convex_to_lower_map [simp]: 

616 
"convex_to_lower\<cdot>(convex_map\<cdot>f\<cdot>xs) = lower_map\<cdot>f\<cdot>(convex_to_lower\<cdot>xs)" 

617 
by (simp add: convex_map_def lower_map_def cfcomp_LAM) 

618 

619 
lemma convex_to_lower_join [simp]: 

620 
"convex_to_lower\<cdot>(convex_join\<cdot>xss) = 

621 
lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower" 

622 
by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun) 

623 

25904  624 
text {* Ordering property *} 
625 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

626 
lemma convex_pd_below_iff: 
25904  627 
"(xs \<sqsubseteq> ys) = 
628 
(convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and> 

629 
convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)" 

630 
apply (safe elim!: monofun_cfun_arg) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

631 
apply (rule profinite_below_ext) 
25904  632 
apply (drule_tac f="approx i" in monofun_cfun_arg) 
633 
apply (drule_tac f="approx i" in monofun_cfun_arg) 

27289  634 
apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp) 
635 
apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp) 

25904  636 
apply clarify 
637 
apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def) 

638 
done 

639 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

640 
lemmas convex_plus_below_plus_iff = 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

641 
convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard] 
26927  642 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

643 
lemmas convex_pd_below_simps = 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

644 
convex_unit_below_plus_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

645 
convex_plus_below_unit_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

646 
convex_plus_below_plus_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

647 
convex_unit_below_iff 
26927  648 
convex_to_upper_unit 
649 
convex_to_upper_plus 

650 
convex_to_lower_unit 

651 
convex_to_lower_plus 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

652 
upper_pd_below_simps 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

653 
lower_pd_below_simps 
26927  654 

25904  655 
end 