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/LowerPD.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Lower powerdomain *} 

6 

7 
theory LowerPD 

8 
imports CompactBasis 

9 
begin 

10 

11 
subsection {* Basis preorder *} 

12 

13 
definition 

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

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

15 
"lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)" 
25904  16 

17 
lemma lower_le_refl [simp]: "t \<le>\<flat> t" 

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

18 
unfolding lower_le_def by fast 
25904  19 

20 
lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v" 

21 
unfolding lower_le_def 

22 
apply (rule ballI) 

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

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

25 
apply (erule rev_bexI) 

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

26 
apply (erule (1) below_trans) 
25904  27 
done 
28 

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

29 
interpretation lower_le: preorder lower_le 
25904  30 
by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans) 
31 

32 
lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t" 

33 
unfolding lower_le_def Rep_PDUnit 

34 
by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv]) 

35 

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

36 
lemma PDUnit_lower_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y" 
25904  37 
unfolding lower_le_def Rep_PDUnit by fast 
38 

39 
lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v" 

40 
unfolding lower_le_def Rep_PDPlus by fast 

41 

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

42 
lemma PDPlus_lower_le: "t \<le>\<flat> PDPlus t u" 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

43 
unfolding lower_le_def Rep_PDPlus by fast 
25904  44 

45 
lemma lower_le_PDUnit_PDUnit_iff [simp]: 

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

46 
"(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b" 
25904  47 
unfolding lower_le_def Rep_PDUnit by fast 
48 

49 
lemma lower_le_PDUnit_PDPlus_iff: 

50 
"(PDUnit a \<le>\<flat> PDPlus t u) = (PDUnit a \<le>\<flat> t \<or> PDUnit a \<le>\<flat> u)" 

51 
unfolding lower_le_def Rep_PDPlus Rep_PDUnit by fast 

52 

53 
lemma lower_le_PDPlus_iff: "(PDPlus t u \<le>\<flat> v) = (t \<le>\<flat> v \<and> u \<le>\<flat> v)" 

54 
unfolding lower_le_def Rep_PDPlus by fast 

55 

56 
lemma lower_le_induct [induct set: lower_le]: 

57 
assumes le: "t \<le>\<flat> u" 

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

58 
assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" 
25904  59 
assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)" 
60 
assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v" 

61 
shows "P t u" 

62 
using le 

63 
apply (induct t arbitrary: u rule: pd_basis_induct) 

64 
apply (erule rev_mp) 

65 
apply (induct_tac u rule: pd_basis_induct) 

66 
apply (simp add: 1) 

67 
apply (simp add: lower_le_PDUnit_PDPlus_iff) 

68 
apply (simp add: 2) 

69 
apply (subst PDPlus_commute) 

70 
apply (simp add: 2) 

71 
apply (simp add: lower_le_PDPlus_iff 3) 

72 
done 

73 

27405  74 
lemma pd_take_lower_chain: 
75 
"pd_take n t \<le>\<flat> pd_take (Suc n) t" 

25904  76 
apply (induct t rule: pd_basis_induct) 
27289  77 
apply (simp add: compact_basis.take_chain) 
25904  78 
apply (simp add: PDPlus_lower_mono) 
79 
done 

80 

27405  81 
lemma pd_take_lower_le: "pd_take i t \<le>\<flat> t" 
25904  82 
apply (induct t rule: pd_basis_induct) 
27289  83 
apply (simp add: compact_basis.take_less) 
25904  84 
apply (simp add: PDPlus_lower_mono) 
85 
done 

86 

27405  87 
lemma pd_take_lower_mono: 
88 
"t \<le>\<flat> u \<Longrightarrow> pd_take n t \<le>\<flat> pd_take n u" 

25904  89 
apply (erule lower_le_induct) 
27289  90 
apply (simp add: compact_basis.take_mono) 
25904  91 
apply (simp add: lower_le_PDUnit_PDPlus_iff) 
92 
apply (simp add: lower_le_PDPlus_iff) 

93 
done 

94 

95 

96 
subsection {* Type definition *} 

97 

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

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

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

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

101 

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

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

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

104 

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

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

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

107 

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

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

109 
end 
25904  110 

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

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

112 
by (rule lower_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

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

114 

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

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

116 
by (rule lower_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

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

118 

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

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

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

121 
by (rule lower_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

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

123 

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

124 
lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)" 
26927  125 
by (rule Rep_lower_pd [unfolded mem_Collect_eq]) 
25904  126 

127 
definition 

128 
lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where 

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

129 
"lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}" 
25904  130 

131 
lemma Rep_lower_principal: 

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

132 
"Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}" 
25904  133 
unfolding lower_principal_def 
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

134 
by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) 
25904  135 

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

136 
interpretation lower_pd: 
29237  137 
ideal_completion lower_le pd_take lower_principal Rep_lower_pd 
25904  138 
apply unfold_locales 
27405  139 
apply (rule pd_take_lower_le) 
140 
apply (rule pd_take_idem) 

141 
apply (erule pd_take_lower_mono) 

142 
apply (rule pd_take_lower_chain) 

143 
apply (rule finite_range_pd_take) 

144 
apply (rule pd_take_covers) 

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

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

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

147 
apply (rule Rep_lower_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

148 
apply (simp only: below_lower_pd_def) 
25904  149 
done 
150 

27289  151 
text {* Lower powerdomain is pointed *} 
25904  152 

153 
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys" 

154 
by (induct ys rule: lower_pd.principal_induct, simp, simp) 

155 

156 
instance lower_pd :: (bifinite) pcpo 

26927  157 
by intro_classes (fast intro: lower_pd_minimal) 
25904  158 

159 
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)" 

160 
by (rule lower_pd_minimal [THEN UU_I, symmetric]) 

161 

27289  162 
text {* Lower powerdomain is profinite *} 
25904  163 

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

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

165 
begin 
25904  166 

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

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

168 
approx_lower_pd_def: "approx = lower_pd.completion_approx" 
26927  169 

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

170 
instance 
26927  171 
apply (intro_classes, unfold approx_lower_pd_def) 
27310  172 
apply (rule lower_pd.chain_completion_approx) 
26927  173 
apply (rule lower_pd.lub_completion_approx) 
174 
apply (rule lower_pd.completion_approx_idem) 

175 
apply (rule lower_pd.finite_fixes_completion_approx) 

176 
done 

177 

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

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

179 

26927  180 
instance lower_pd :: (bifinite) bifinite .. 
25904  181 

182 
lemma approx_lower_principal [simp]: 

27405  183 
"approx n\<cdot>(lower_principal t) = lower_principal (pd_take n t)" 
25904  184 
unfolding approx_lower_pd_def 
26927  185 
by (rule lower_pd.completion_approx_principal) 
25904  186 

187 
lemma approx_eq_lower_principal: 

27405  188 
"\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (pd_take n t)" 
25904  189 
unfolding approx_lower_pd_def 
26927  190 
by (rule lower_pd.completion_approx_eq_principal) 
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

191 

25904  192 

26927  193 
subsection {* Monadic unit and plus *} 
25904  194 

195 
definition 

196 
lower_unit :: "'a \<rightarrow> 'a lower_pd" where 

197 
"lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))" 

198 

199 
definition 

200 
lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where 

201 
"lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u. 

202 
lower_principal (PDPlus t u)))" 

203 

204 
abbreviation 

205 
lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd" 

206 
(infixl "+\<flat>" 65) where 

207 
"xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys" 

208 

26927  209 
syntax 
210 
"_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>") 

211 

212 
translations 

213 
"{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>" 

214 
"{x}\<flat>" == "CONST lower_unit\<cdot>x" 

215 

216 
lemma lower_unit_Rep_compact_basis [simp]: 

217 
"{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)" 

218 
unfolding lower_unit_def 

27289  219 
by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono) 
26927  220 

25904  221 
lemma lower_plus_principal [simp]: 
26927  222 
"lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)" 
25904  223 
unfolding lower_plus_def 
224 
by (simp add: lower_pd.basis_fun_principal 

225 
lower_pd.basis_fun_mono PDPlus_lower_mono) 

226 

26927  227 
lemma approx_lower_unit [simp]: 
228 
"approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>" 

27289  229 
apply (induct x rule: compact_basis.principal_induct, simp) 
26927  230 
apply (simp add: approx_Rep_compact_basis) 
231 
done 

232 

25904  233 
lemma approx_lower_plus [simp]: 
26927  234 
"approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)" 
27289  235 
by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp) 
25904  236 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

252 
qed 
26927  253 

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

254 
lemmas lower_plus_assoc = lower_add.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

255 
lemmas lower_plus_commute = lower_add.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

256 
lemmas lower_plus_absorb = lower_add.idem 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

257 
lemmas lower_plus_left_commute = lower_add.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

258 
lemmas lower_plus_left_absorb = lower_add.left_idem 
26927  259 

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

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

261 
lemmas lower_plus_ac = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

262 
lower_plus_assoc lower_plus_commute lower_plus_left_commute 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

263 

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

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

265 
lemmas lower_plus_aci = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

266 
lower_plus_ac lower_plus_absorb lower_plus_left_absorb 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

267 

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

268 
lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys" 
27289  269 
apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp) 
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

270 
apply (simp add: PDPlus_lower_le) 
25904  271 
done 
272 

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

273 
lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

274 
by (subst lower_plus_commute, rule lower_plus_below1) 
25904  275 

26927  276 
lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs" 
25904  277 
apply (subst lower_plus_absorb [of zs, symmetric]) 
278 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 

279 
done 

280 

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

281 
lemma lower_plus_below_iff: 
26927  282 
"xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs" 
25904  283 
apply safe 
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

284 
apply (erule below_trans [OF lower_plus_below1]) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

285 
apply (erule below_trans [OF lower_plus_below2]) 
25904  286 
apply (erule (1) lower_plus_least) 
287 
done 

288 

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

289 
lemma lower_unit_below_plus_iff: 
26927  290 
"{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs" 
25904  291 
apply (rule iffI) 
292 
apply (subgoal_tac 

26927  293 
"adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)") 
25925  294 
apply (drule admD, rule chain_approx) 
25904  295 
apply (drule_tac f="approx i" in monofun_cfun_arg) 
27289  296 
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp) 
297 
apply (cut_tac x="approx i\<cdot>ys" in lower_pd.compact_imp_principal, simp) 

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

25904  299 
apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff) 
300 
apply simp 

301 
apply simp 

302 
apply (erule disjE) 

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

303 
apply (erule below_trans [OF _ lower_plus_below1]) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

304 
apply (erule below_trans [OF _ lower_plus_below2]) 
25904  305 
done 
306 

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

307 
lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y" 
26927  308 
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

309 
apply (rule profinite_below_ext) 
26927  310 
apply (drule_tac f="approx i" in monofun_cfun_arg, simp) 
27289  311 
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp) 
312 
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp) 

313 
apply clarsimp 

26927  314 
apply (erule monofun_cfun_arg) 
315 
done 

316 

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

317 
lemmas lower_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

318 
lower_unit_below_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

319 
lower_plus_below_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

320 
lower_unit_below_plus_iff 
25904  321 

26927  322 
lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y" 
29990
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

323 
by (simp add: po_eq_conv) 
26927  324 

325 
lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>" 

326 
unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp 

327 

328 
lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>" 

329 
unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff) 

330 

331 
lemma lower_plus_strict_iff [simp]: 

332 
"xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>" 

333 
apply safe 

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

334 
apply (rule UU_I, erule subst, rule lower_plus_below1) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

335 
apply (rule UU_I, erule subst, rule lower_plus_below2) 
26927  336 
apply (rule lower_plus_absorb) 
337 
done 

338 

339 
lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys" 

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

340 
apply (rule below_antisym [OF _ lower_plus_below2]) 
26927  341 
apply (simp add: lower_plus_least) 
342 
done 

343 

344 
lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs" 

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

345 
apply (rule below_antisym [OF _ lower_plus_below1]) 
26927  346 
apply (simp add: lower_plus_least) 
347 
done 

348 

349 
lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x" 

27309  350 
unfolding profinite_compact_iff by simp 
26927  351 

352 
lemma compact_lower_plus [simp]: 

353 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)" 

27289  354 
by (auto dest!: lower_pd.compact_imp_principal) 
26927  355 

25904  356 

357 
subsection {* Induction rules *} 

358 

359 
lemma lower_pd_induct1: 

360 
assumes P: "adm P" 

26927  361 
assumes unit: "\<And>x. P {x}\<flat>" 
25904  362 
assumes insert: 
26927  363 
"\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)" 
25904  364 
shows "P (xs::'a lower_pd)" 
27289  365 
apply (induct xs rule: lower_pd.principal_induct, rule P) 
366 
apply (induct_tac a rule: pd_basis_induct1) 

25904  367 
apply (simp only: lower_unit_Rep_compact_basis [symmetric]) 
368 
apply (rule unit) 

369 
apply (simp only: lower_unit_Rep_compact_basis [symmetric] 

370 
lower_plus_principal [symmetric]) 

371 
apply (erule insert [OF unit]) 

372 
done 

373 

374 
lemma lower_pd_induct: 

375 
assumes P: "adm P" 

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

25904  378 
shows "P (xs::'a lower_pd)" 
27289  379 
apply (induct xs rule: lower_pd.principal_induct, rule P) 
380 
apply (induct_tac a rule: pd_basis_induct) 

25904  381 
apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit) 
382 
apply (simp only: lower_plus_principal [symmetric] plus) 

383 
done 

384 

385 

386 
subsection {* Monadic bind *} 

387 

388 
definition 

389 
lower_bind_basis :: 

390 
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where 

391 
"lower_bind_basis = fold_pd 

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

26927  393 
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)" 
25904  394 

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

396 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)" 
25904  397 
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

398 
apply (simp add: lower_plus_assoc) 
25904  399 
apply (simp add: lower_plus_commute) 
29990
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

400 
apply (simp add: eta_cfun) 
25904  401 
done 
402 

403 
lemma lower_bind_basis_simps [simp]: 

404 
"lower_bind_basis (PDUnit a) = 

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

406 
"lower_bind_basis (PDPlus t u) = 

26927  407 
(\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)" 
25904  408 
unfolding lower_bind_basis_def 
409 
apply  

26927  410 
apply (rule fold_pd_PDUnit [OF ACI_lower_bind]) 
411 
apply (rule fold_pd_PDPlus [OF ACI_lower_bind]) 

25904  412 
done 
413 

414 
lemma lower_bind_basis_mono: 

415 
"t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u" 

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

416 
unfolding expand_cfun_below 
25904  417 
apply (erule lower_le_induct, safe) 
27289  418 
apply (simp add: monofun_cfun) 
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

419 
apply (simp add: rev_below_trans [OF lower_plus_below1]) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

420 
apply (simp add: lower_plus_below_iff) 
25904  421 
done 
422 

423 
definition 

424 
lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where 

425 
"lower_bind = lower_pd.basis_fun lower_bind_basis" 

426 

427 
lemma lower_bind_principal [simp]: 

428 
"lower_bind\<cdot>(lower_principal t) = lower_bind_basis t" 

429 
unfolding lower_bind_def 

430 
apply (rule lower_pd.basis_fun_principal) 

431 
apply (erule lower_bind_basis_mono) 

432 
done 

433 

434 
lemma lower_bind_unit [simp]: 

26927  435 
"lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x" 
27289  436 
by (induct x rule: compact_basis.principal_induct, simp, simp) 
25904  437 

438 
lemma lower_bind_plus [simp]: 

26927  439 
"lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f" 
27289  440 
by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp) 
25904  441 

442 
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 

443 
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit) 

444 

445 

446 
subsection {* Map and join *} 

447 

448 
definition 

449 
lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where 

26927  450 
"lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))" 
25904  451 

452 
definition 

453 
lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where 

454 
"lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 

455 

456 
lemma lower_map_unit [simp]: 

26927  457 
"lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>" 
25904  458 
unfolding lower_map_def by simp 
459 

460 
lemma lower_map_plus [simp]: 

26927  461 
"lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys" 
25904  462 
unfolding lower_map_def by simp 
463 

464 
lemma lower_join_unit [simp]: 

26927  465 
"lower_join\<cdot>{xs}\<flat> = xs" 
25904  466 
unfolding lower_join_def by simp 
467 

468 
lemma lower_join_plus [simp]: 

26927  469 
"lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss" 
25904  470 
unfolding lower_join_def by simp 
471 

472 
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 

473 
by (induct xs rule: lower_pd_induct, simp_all) 

474 

33808  475 
lemma lower_map_ID: "lower_map\<cdot>ID = ID" 
476 
by (simp add: expand_cfun_eq ID_def lower_map_ident) 

477 

25904  478 
lemma lower_map_map: 
479 
"lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 

480 
by (induct xs rule: lower_pd_induct, simp_all) 

481 

482 
lemma lower_join_map_unit: 

483 
"lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs" 

484 
by (induct xs rule: lower_pd_induct, simp_all) 

485 

486 
lemma lower_join_map_join: 

487 
"lower_join\<cdot>(lower_map\<cdot>lower_join\<cdot>xsss) = lower_join\<cdot>(lower_join\<cdot>xsss)" 

488 
by (induct xsss rule: lower_pd_induct, simp_all) 

489 

490 
lemma lower_join_map_map: 

491 
"lower_join\<cdot>(lower_map\<cdot>(lower_map\<cdot>f)\<cdot>xss) = 

492 
lower_map\<cdot>f\<cdot>(lower_join\<cdot>xss)" 

493 
by (induct xss rule: lower_pd_induct, simp_all) 

494 

495 
lemma lower_map_approx: "lower_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs" 

496 
by (induct xs rule: lower_pd_induct, simp_all) 

497 

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

498 
lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)" 
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

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

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

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

502 
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

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

504 

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

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

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

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

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

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

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

511 

25904  512 
end 