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

3 
*) 

4 

5 
header {* Upper powerdomain *} 

6 

7 
theory UpperPD 

8 
imports CompactBasis 

9 
begin 

10 

11 
subsection {* Basis preorder *} 

12 

13 
definition 

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

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

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

17 
lemma upper_le_refl [simp]: "t \<le>\<sharp> t" 

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

18 
unfolding upper_le_def by fast 
25904  19 

20 
lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v" 

21 
unfolding upper_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 upper_le: preorder upper_le 
25904  30 
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans) 
31 

32 
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t" 

33 
unfolding upper_le_def Rep_PDUnit by simp 

34 

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

35 
lemma PDUnit_upper_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y" 
25904  36 
unfolding upper_le_def Rep_PDUnit by simp 
37 

38 
lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v" 

39 
unfolding upper_le_def Rep_PDPlus by fast 

40 

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

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

42 
unfolding upper_le_def Rep_PDPlus by fast 
25904  43 

44 
lemma upper_le_PDUnit_PDUnit_iff [simp]: 

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

45 
"(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b" 
25904  46 
unfolding upper_le_def Rep_PDUnit by fast 
47 

48 
lemma upper_le_PDPlus_PDUnit_iff: 

49 
"(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)" 

50 
unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast 

51 

52 
lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)" 

53 
unfolding upper_le_def Rep_PDPlus by fast 

54 

55 
lemma upper_le_induct [induct set: upper_le]: 

56 
assumes le: "t \<le>\<sharp> u" 

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

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

60 
shows "P t u" 

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

62 
apply (erule rev_mp) 

63 
apply (induct_tac t rule: pd_basis_induct) 

64 
apply (simp add: 1) 

65 
apply (simp add: upper_le_PDPlus_PDUnit_iff) 

66 
apply (simp add: 2) 

67 
apply (subst PDPlus_commute) 

68 
apply (simp add: 2) 

69 
apply (simp add: upper_le_PDPlus_iff 3) 

70 
done 

71 

27405  72 
lemma pd_take_upper_chain: 
73 
"pd_take n t \<le>\<sharp> pd_take (Suc n) t" 

25904  74 
apply (induct t rule: pd_basis_induct) 
27289  75 
apply (simp add: compact_basis.take_chain) 
25904  76 
apply (simp add: PDPlus_upper_mono) 
77 
done 

78 

27405  79 
lemma pd_take_upper_le: "pd_take i t \<le>\<sharp> t" 
25904  80 
apply (induct t rule: pd_basis_induct) 
27289  81 
apply (simp add: compact_basis.take_less) 
25904  82 
apply (simp add: PDPlus_upper_mono) 
83 
done 

84 

27405  85 
lemma pd_take_upper_mono: 
86 
"t \<le>\<sharp> u \<Longrightarrow> pd_take n t \<le>\<sharp> pd_take n u" 

25904  87 
apply (erule upper_le_induct) 
27289  88 
apply (simp add: compact_basis.take_mono) 
25904  89 
apply (simp add: upper_le_PDPlus_PDUnit_iff) 
90 
apply (simp add: upper_le_PDPlus_iff) 

91 
done 

92 

93 

94 
subsection {* Type definition *} 

95 

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

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

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

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

99 

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

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

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

102 

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

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

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

105 

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

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

107 
end 
25904  108 

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

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

110 
by (rule upper_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

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

112 

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

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

114 
by (rule upper_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

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

116 

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

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

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

119 
by (rule upper_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

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

121 

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

122 
lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)" 
26927  123 
by (rule Rep_upper_pd [unfolded mem_Collect_eq]) 
25904  124 

125 
definition 

126 
upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where 

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

127 
"upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}" 
25904  128 

129 
lemma Rep_upper_principal: 

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

130 
"Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}" 
25904  131 
unfolding upper_principal_def 
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

132 
by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) 
25904  133 

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

134 
interpretation upper_pd: 
29237  135 
ideal_completion upper_le pd_take upper_principal Rep_upper_pd 
25904  136 
apply unfold_locales 
27405  137 
apply (rule pd_take_upper_le) 
138 
apply (rule pd_take_idem) 

139 
apply (erule pd_take_upper_mono) 

140 
apply (rule pd_take_upper_chain) 

141 
apply (rule finite_range_pd_take) 

142 
apply (rule pd_take_covers) 

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

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

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

145 
apply (rule Rep_upper_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

146 
apply (simp only: below_upper_pd_def) 
25904  147 
done 
148 

27289  149 
text {* Upper powerdomain is pointed *} 
25904  150 

151 
lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" 

152 
by (induct ys rule: upper_pd.principal_induct, simp, simp) 

153 

154 
instance upper_pd :: (bifinite) pcpo 

26927  155 
by intro_classes (fast intro: upper_pd_minimal) 
25904  156 

157 
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)" 

158 
by (rule upper_pd_minimal [THEN UU_I, symmetric]) 

159 

27289  160 
text {* Upper powerdomain is profinite *} 
25904  161 

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

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

163 
begin 
25904  164 

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

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

166 
approx_upper_pd_def: "approx = upper_pd.completion_approx" 
26927  167 

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

168 
instance 
26927  169 
apply (intro_classes, unfold approx_upper_pd_def) 
27310  170 
apply (rule upper_pd.chain_completion_approx) 
26927  171 
apply (rule upper_pd.lub_completion_approx) 
172 
apply (rule upper_pd.completion_approx_idem) 

173 
apply (rule upper_pd.finite_fixes_completion_approx) 

174 
done 

175 

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

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

177 

26927  178 
instance upper_pd :: (bifinite) bifinite .. 
25904  179 

180 
lemma approx_upper_principal [simp]: 

27405  181 
"approx n\<cdot>(upper_principal t) = upper_principal (pd_take n t)" 
25904  182 
unfolding approx_upper_pd_def 
26927  183 
by (rule upper_pd.completion_approx_principal) 
25904  184 

185 
lemma approx_eq_upper_principal: 

27405  186 
"\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (pd_take n t)" 
25904  187 
unfolding approx_upper_pd_def 
26927  188 
by (rule upper_pd.completion_approx_eq_principal) 
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

189 

25904  190 

26927  191 
subsection {* Monadic unit and plus *} 
25904  192 

193 
definition 

194 
upper_unit :: "'a \<rightarrow> 'a upper_pd" where 

195 
"upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))" 

196 

197 
definition 

198 
upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where 

199 
"upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u. 

200 
upper_principal (PDPlus t u)))" 

201 

202 
abbreviation 

203 
upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd" 

204 
(infixl "+\<sharp>" 65) where 

205 
"xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys" 

206 

26927  207 
syntax 
208 
"_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>") 

209 

210 
translations 

211 
"{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>" 

212 
"{x}\<sharp>" == "CONST upper_unit\<cdot>x" 

213 

214 
lemma upper_unit_Rep_compact_basis [simp]: 

215 
"{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)" 

216 
unfolding upper_unit_def 

27289  217 
by (simp add: compact_basis.basis_fun_principal PDUnit_upper_mono) 
26927  218 

25904  219 
lemma upper_plus_principal [simp]: 
26927  220 
"upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)" 
25904  221 
unfolding upper_plus_def 
222 
by (simp add: upper_pd.basis_fun_principal 

223 
upper_pd.basis_fun_mono PDPlus_upper_mono) 

224 

26927  225 
lemma approx_upper_unit [simp]: 
226 
"approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>" 

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

230 

25904  231 
lemma approx_upper_plus [simp]: 
26927  232 
"approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)" 
27289  233 
by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp) 
25904  234 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

250 
qed 
26927  251 

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

252 
lemmas upper_plus_assoc = upper_add.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

253 
lemmas upper_plus_commute = upper_add.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

254 
lemmas upper_plus_absorb = upper_add.idem 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

255 
lemmas upper_plus_left_commute = upper_add.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
33808
diff
changeset

256 
lemmas upper_plus_left_absorb = upper_add.left_idem 
26927  257 

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

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

259 
lemmas upper_plus_ac = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

260 
upper_plus_assoc upper_plus_commute upper_plus_left_commute 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

261 

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

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

263 
lemmas upper_plus_aci = 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

264 
upper_plus_ac upper_plus_absorb upper_plus_left_absorb 
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

265 

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

266 
lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs" 
27289  267 
apply (induct xs ys rule: upper_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

268 
apply (simp add: PDPlus_upper_le) 
25904  269 
done 
270 

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

271 
lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> 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

272 
by (subst upper_plus_commute, rule upper_plus_below1) 
25904  273 

26927  274 
lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs" 
25904  275 
apply (subst upper_plus_absorb [of xs, symmetric]) 
276 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 

277 
done 

278 

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

279 
lemma upper_below_plus_iff: 
26927  280 
"xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs" 
25904  281 
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

282 
apply (erule below_trans [OF _ upper_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

283 
apply (erule below_trans [OF _ upper_plus_below2]) 
25904  284 
apply (erule (1) upper_plus_greatest) 
285 
done 

286 

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

287 
lemma upper_plus_below_unit_iff: 
26927  288 
"xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>" 
25904  289 
apply (rule iffI) 
290 
apply (subgoal_tac 

26927  291 
"adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)") 
25925  292 
apply (drule admD, rule chain_approx) 
25904  293 
apply (drule_tac f="approx i" in monofun_cfun_arg) 
27289  294 
apply (cut_tac x="approx i\<cdot>xs" in upper_pd.compact_imp_principal, simp) 
295 
apply (cut_tac x="approx i\<cdot>ys" in upper_pd.compact_imp_principal, simp) 

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

25904  297 
apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff) 
298 
apply simp 

299 
apply simp 

300 
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

301 
apply (erule below_trans [OF upper_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

302 
apply (erule below_trans [OF upper_plus_below2]) 
25904  303 
done 
304 

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

305 
lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y" 
26927  306 
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

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

311 
apply clarsimp 

26927  312 
apply (erule monofun_cfun_arg) 
313 
done 

314 

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

315 
lemmas 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

316 
upper_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

317 
upper_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

318 
upper_plus_below_unit_iff 
25904  319 

26927  320 
lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y" 
321 
unfolding po_eq_conv by simp 

322 

323 
lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>" 

324 
unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp 

325 

326 
lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>" 

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

327 
by (rule UU_I, rule upper_plus_below1) 
26927  328 

329 
lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>" 

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

330 
by (rule UU_I, rule upper_plus_below2) 
26927  331 

332 
lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>" 

333 
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff) 

334 

335 
lemma upper_plus_strict_iff [simp]: 

336 
"xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>" 

337 
apply (rule iffI) 

338 
apply (erule rev_mp) 

27289  339 
apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp) 
340 
apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff 

26927  341 
upper_le_PDPlus_PDUnit_iff) 
342 
apply auto 

343 
done 

344 

345 
lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x" 

27309  346 
unfolding profinite_compact_iff by simp 
26927  347 

348 
lemma compact_upper_plus [simp]: 

349 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)" 

27289  350 
by (auto dest!: upper_pd.compact_imp_principal) 
26927  351 

25904  352 

353 
subsection {* Induction rules *} 

354 

355 
lemma upper_pd_induct1: 

356 
assumes P: "adm P" 

26927  357 
assumes unit: "\<And>x. P {x}\<sharp>" 
358 
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)" 

25904  359 
shows "P (xs::'a upper_pd)" 
27289  360 
apply (induct xs rule: upper_pd.principal_induct, rule P) 
361 
apply (induct_tac a rule: pd_basis_induct1) 

25904  362 
apply (simp only: upper_unit_Rep_compact_basis [symmetric]) 
363 
apply (rule unit) 

364 
apply (simp only: upper_unit_Rep_compact_basis [symmetric] 

365 
upper_plus_principal [symmetric]) 

366 
apply (erule insert [OF unit]) 

367 
done 

368 

369 
lemma upper_pd_induct: 

370 
assumes P: "adm P" 

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

25904  373 
shows "P (xs::'a upper_pd)" 
27289  374 
apply (induct xs rule: upper_pd.principal_induct, rule P) 
375 
apply (induct_tac a rule: pd_basis_induct) 

25904  376 
apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit) 
377 
apply (simp only: upper_plus_principal [symmetric] plus) 

378 
done 

379 

380 

381 
subsection {* Monadic bind *} 

382 

383 
definition 

384 
upper_bind_basis :: 

385 
"'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where 

386 
"upper_bind_basis = fold_pd 

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

26927  388 
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)" 
25904  389 

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

391 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)" 
25904  392 
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

393 
apply (simp add: upper_plus_assoc) 
25904  394 
apply (simp add: upper_plus_commute) 
29990
b11793ea15a3
avoid using ab_semigroup_idem_mult locale for powerdomains
huffman
parents:
29672
diff
changeset

395 
apply (simp add: eta_cfun) 
25904  396 
done 
397 

398 
lemma upper_bind_basis_simps [simp]: 

399 
"upper_bind_basis (PDUnit a) = 

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

401 
"upper_bind_basis (PDPlus t u) = 

26927  402 
(\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)" 
25904  403 
unfolding upper_bind_basis_def 
404 
apply  

26927  405 
apply (rule fold_pd_PDUnit [OF ACI_upper_bind]) 
406 
apply (rule fold_pd_PDPlus [OF ACI_upper_bind]) 

25904  407 
done 
408 

409 
lemma upper_bind_basis_mono: 

410 
"t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_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

411 
unfolding expand_cfun_below 
25904  412 
apply (erule upper_le_induct, safe) 
27289  413 
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

414 
apply (simp add: below_trans [OF upper_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

415 
apply (simp add: upper_below_plus_iff) 
25904  416 
done 
417 

418 
definition 

419 
upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where 

420 
"upper_bind = upper_pd.basis_fun upper_bind_basis" 

421 

422 
lemma upper_bind_principal [simp]: 

423 
"upper_bind\<cdot>(upper_principal t) = upper_bind_basis t" 

424 
unfolding upper_bind_def 

425 
apply (rule upper_pd.basis_fun_principal) 

426 
apply (erule upper_bind_basis_mono) 

427 
done 

428 

429 
lemma upper_bind_unit [simp]: 

26927  430 
"upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x" 
27289  431 
by (induct x rule: compact_basis.principal_induct, simp, simp) 
25904  432 

433 
lemma upper_bind_plus [simp]: 

26927  434 
"upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f" 
27289  435 
by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp) 
25904  436 

437 
lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 

438 
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) 

439 

440 

441 
subsection {* Map and join *} 

442 

443 
definition 

444 
upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where 

26927  445 
"upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))" 
25904  446 

447 
definition 

448 
upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where 

449 
"upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 

450 

451 
lemma upper_map_unit [simp]: 

26927  452 
"upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>" 
25904  453 
unfolding upper_map_def by simp 
454 

455 
lemma upper_map_plus [simp]: 

26927  456 
"upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys" 
25904  457 
unfolding upper_map_def by simp 
458 

459 
lemma upper_join_unit [simp]: 

26927  460 
"upper_join\<cdot>{xs}\<sharp> = xs" 
25904  461 
unfolding upper_join_def by simp 
462 

463 
lemma upper_join_plus [simp]: 

26927  464 
"upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss" 
25904  465 
unfolding upper_join_def by simp 
466 

467 
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 

468 
by (induct xs rule: upper_pd_induct, simp_all) 

469 

33808  470 
lemma upper_map_ID: "upper_map\<cdot>ID = ID" 
471 
by (simp add: expand_cfun_eq ID_def upper_map_ident) 

472 

25904  473 
lemma upper_map_map: 
474 
"upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 

475 
by (induct xs rule: upper_pd_induct, simp_all) 

476 

477 
lemma upper_join_map_unit: 

478 
"upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs" 

479 
by (induct xs rule: upper_pd_induct, simp_all) 

480 

481 
lemma upper_join_map_join: 

482 
"upper_join\<cdot>(upper_map\<cdot>upper_join\<cdot>xsss) = upper_join\<cdot>(upper_join\<cdot>xsss)" 

483 
by (induct xsss rule: upper_pd_induct, simp_all) 

484 

485 
lemma upper_join_map_map: 

486 
"upper_join\<cdot>(upper_map\<cdot>(upper_map\<cdot>f)\<cdot>xss) = 

487 
upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)" 

488 
by (induct xss rule: upper_pd_induct, simp_all) 

489 

490 
lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs" 

491 
by (induct xs rule: upper_pd_induct, simp_all) 

492 

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

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

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

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

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

497 
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

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

499 

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

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

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

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

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

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

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

506 

25904  507 
end 