author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45606  b1e1508643b1 
child 49834  b27bbb021df1 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/ConvexPD.thy 
25904  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]: 

40436  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 

119 

120 
subsection {* Type definition *} 

121 

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

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

123 
"{S::'a pd_basis set. convex_le.ideal S}" 
40888
28cd51cff70c
reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents:
40774
diff
changeset

124 
by (rule convex_le.ex_ideal) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

125 

41111  126 
type_notation (xsymbols) convex_pd ("('(_')\<natural>)") 
127 

41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41287
diff
changeset

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

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

130 

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

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

132 
"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

133 

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

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

135 
end 
25904  136 

41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41287
diff
changeset

137 
instance convex_pd :: (bifinite) po 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

138 
using type_definition_convex_pd below_convex_pd_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

139 
by (rule convex_le.typedef_ideal_po) 
27373
5794a0e3e26c
remove cset theory; define ideal completions using typedef instead of cpodef
huffman
parents:
27310
diff
changeset

140 

41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41287
diff
changeset

141 
instance convex_pd :: (bifinite) cpo 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

142 
using type_definition_convex_pd below_convex_pd_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

144 

25904  145 
definition 
146 
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

147 
"convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}" 
25904  148 

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

149 
interpretation convex_pd: 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

150 
ideal_completion convex_le convex_principal Rep_convex_pd 
39984  151 
using type_definition_convex_pd below_convex_pd_def 
152 
using convex_principal_def pd_basis_countable 

153 
by (rule convex_le.typedef_ideal_completion) 

25904  154 

27289  155 
text {* Convex powerdomain is pointed *} 
25904  156 

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

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

159 

41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41287
diff
changeset

160 
instance convex_pd :: (bifinite) pcpo 
26927  161 
by intro_classes (fast intro: convex_pd_minimal) 
25904  162 

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

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41402
diff
changeset

164 
by (rule convex_pd_minimal [THEN bottomI, symmetric]) 
25904  165 

166 

26927  167 
subsection {* Monadic unit and plus *} 
25904  168 

169 
definition 

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

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

171 
"convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))" 
25904  172 

173 
definition 

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

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

175 
"convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u. 
25904  176 
convex_principal (PDPlus t u)))" 
177 

178 
abbreviation 

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

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

180 
(infixl "\<union>\<natural>" 65) where 
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

181 
"xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" 
25904  182 

26927  183 
syntax 
41479  184 
"_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>") 
26927  185 

186 
translations 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

187 
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" 
26927  188 
"{x}\<natural>" == "CONST convex_unit\<cdot>x" 
189 

190 
lemma convex_unit_Rep_compact_basis [simp]: 

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

192 
unfolding convex_unit_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

193 
by (simp add: compact_basis.extension_principal PDUnit_convex_mono) 
26927  194 

25904  195 
lemma convex_plus_principal [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

196 
"convex_principal t \<union>\<natural> convex_principal u = convex_principal (PDPlus t u)" 
25904  197 
unfolding convex_plus_def 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

198 
by (simp add: convex_pd.extension_principal 
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

199 
convex_pd.extension_mono PDPlus_convex_mono) 
25904  200 

37770
cddb3106adb8
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
haftmann
parents:
36635
diff
changeset

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

202 
fix xs ys zs :: "'a convex_pd" 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

203 
show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

204 
apply (induct xs rule: convex_pd.principal_induct, simp) 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

205 
apply (induct ys rule: convex_pd.principal_induct, simp) 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

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

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

208 
done 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

209 
show "xs \<union>\<natural> ys = ys \<union>\<natural> xs" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

210 
apply (induct xs rule: convex_pd.principal_induct, simp) 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

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

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

213 
done 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

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

215 
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

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

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

218 
qed 
26927  219 

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

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

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

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

223 
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

224 
lemmas convex_plus_left_absorb = convex_add.left_idem 
26927  225 

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

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

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

228 
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

229 

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

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

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

232 
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

233 

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

234 
lemma convex_unit_below_plus_iff [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

235 
"{x}\<natural> \<sqsubseteq> ys \<union>\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs" 
39970
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

236 
apply (induct x rule: compact_basis.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

237 
apply (induct ys rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

238 
apply (induct zs rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

239 
apply simp 
25904  240 
done 
241 

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

242 
lemma convex_plus_below_unit_iff [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

243 
"xs \<union>\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>" 
39970
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

244 
apply (induct xs rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

245 
apply (induct ys rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

246 
apply (induct z rule: compact_basis.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

247 
apply simp 
25904  248 
done 
249 

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

250 
lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y" 
39970
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

251 
apply (induct x rule: compact_basis.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

252 
apply (induct y rule: compact_basis.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

253 
apply simp 
26927  254 
done 
255 

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

257 
unfolding po_eq_conv by simp 

258 

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

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

260 
using convex_unit_Rep_compact_basis [of compact_bot] 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

261 
by (simp add: inst_convex_pd_pcpo) 
26927  262 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40002
diff
changeset

263 
lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>" 
26927  264 
unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff) 
265 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

266 
lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

267 
by (auto dest!: compact_basis.compact_imp_principal) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

268 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

269 
lemma compact_convex_unit_iff [simp]: "compact {x}\<natural> \<longleftrightarrow> compact x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

270 
apply (safe elim!: compact_convex_unit) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

271 
apply (simp only: compact_def convex_unit_below_iff [symmetric]) 
40327  272 
apply (erule adm_subst [OF cont_Rep_cfun2]) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

273 
done 
26927  274 

275 
lemma compact_convex_plus [simp]: 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

276 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<natural> ys)" 
27289  277 
by (auto dest!: convex_pd.compact_imp_principal) 
26927  278 

25904  279 

280 
subsection {* Induction rules *} 

281 

282 
lemma convex_pd_induct1: 

283 
assumes P: "adm P" 

26927  284 
assumes unit: "\<And>x. P {x}\<natural>" 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

285 
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)" 
25904  286 
shows "P (xs::'a convex_pd)" 
27289  287 
apply (induct xs rule: convex_pd.principal_induct, rule P) 
288 
apply (induct_tac a rule: pd_basis_induct1) 

25904  289 
apply (simp only: convex_unit_Rep_compact_basis [symmetric]) 
290 
apply (rule unit) 

291 
apply (simp only: convex_unit_Rep_compact_basis [symmetric] 

292 
convex_plus_principal [symmetric]) 

293 
apply (erule insert [OF unit]) 

294 
done 

295 

40576
fa5e0cacd5e7
declare {upper,lower,convex}_pd_induct as default induction rules
huffman
parents:
40497
diff
changeset

296 
lemma convex_pd_induct 
fa5e0cacd5e7
declare {upper,lower,convex}_pd_induct as default induction rules
huffman
parents:
40497
diff
changeset

297 
[case_names adm convex_unit convex_plus, induct type: convex_pd]: 
25904  298 
assumes P: "adm P" 
26927  299 
assumes unit: "\<And>x. P {x}\<natural>" 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

300 
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)" 
25904  301 
shows "P (xs::'a convex_pd)" 
27289  302 
apply (induct xs rule: convex_pd.principal_induct, rule P) 
303 
apply (induct_tac a rule: pd_basis_induct) 

25904  304 
apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit) 
305 
apply (simp only: convex_plus_principal [symmetric] plus) 

306 
done 

307 

308 

309 
subsection {* Monadic bind *} 

310 

311 
definition 

312 
convex_bind_basis :: 

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

314 
"convex_bind_basis = fold_pd 

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

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

316 
(\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" 
25904  317 

26927  318 
lemma ACI_convex_bind: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

319 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" 
25904  320 
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

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

323 
apply (simp add: eta_cfun) 
25904  324 
done 
325 

326 
lemma convex_bind_basis_simps [simp]: 

327 
"convex_bind_basis (PDUnit a) = 

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

329 
"convex_bind_basis (PDPlus t u) = 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

330 
(\<Lambda> f. convex_bind_basis t\<cdot>f \<union>\<natural> convex_bind_basis u\<cdot>f)" 
25904  331 
unfolding convex_bind_basis_def 
332 
apply  

26927  333 
apply (rule fold_pd_PDUnit [OF ACI_convex_bind]) 
334 
apply (rule fold_pd_PDPlus [OF ACI_convex_bind]) 

25904  335 
done 
336 

337 
lemma convex_bind_basis_mono: 

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

339 
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

340 
apply (erule (1) below_trans) 
27289  341 
apply (simp add: monofun_LAM monofun_cfun) 
342 
apply (simp add: monofun_LAM monofun_cfun) 

25904  343 
done 
344 

345 
definition 

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

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

347 
"convex_bind = convex_pd.extension convex_bind_basis" 
25904  348 

41036
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

349 
syntax 
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

350 
"_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic" 
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

351 
("(3\<Union>\<natural>_\<in>_./ _)" [0, 0, 10] 10) 
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

352 

4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

353 
translations 
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

354 
"\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)" 
4acbacd6c5bc
add setunionlike syntax for powerdomain bind operators
huffman
parents:
40888
diff
changeset

355 

25904  356 
lemma convex_bind_principal [simp]: 
357 
"convex_bind\<cdot>(convex_principal t) = convex_bind_basis t" 

358 
unfolding convex_bind_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

359 
apply (rule convex_pd.extension_principal) 
25904  360 
apply (erule convex_bind_basis_mono) 
361 
done 

362 

363 
lemma convex_bind_unit [simp]: 

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

367 
lemma convex_bind_plus [simp]: 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

368 
"convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

369 
by (induct xs rule: convex_pd.principal_induct, simp, 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

370 
induct ys rule: convex_pd.principal_induct, simp, simp) 
25904  371 

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

373 
unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit) 

374 

40589  375 
lemma convex_bind_bind: 
376 
"convex_bind\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>g = 

377 
convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_bind\<cdot>(f\<cdot>x)\<cdot>g)" 

378 
by (induct xs, simp_all) 

379 

25904  380 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

381 
subsection {* Map *} 
25904  382 

383 
definition 

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

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

387 
lemma convex_map_unit [simp]: 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

388 
"convex_map\<cdot>f\<cdot>{x}\<natural> = {f\<cdot>x}\<natural>" 
25904  389 
unfolding convex_map_def by simp 
390 

391 
lemma convex_map_plus [simp]: 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

392 
"convex_map\<cdot>f\<cdot>(xs \<union>\<natural> ys) = convex_map\<cdot>f\<cdot>xs \<union>\<natural> convex_map\<cdot>f\<cdot>ys" 
25904  393 
unfolding convex_map_def by simp 
394 

40577  395 
lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>" 
396 
unfolding convex_map_def by simp 

397 

25904  398 
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 
399 
by (induct xs rule: convex_pd_induct, simp_all) 

400 

33808  401 
lemma convex_map_ID: "convex_map\<cdot>ID = ID" 
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset

402 
by (simp add: cfun_eq_iff ID_def convex_map_ident) 
33808  403 

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

406 
by (induct xs rule: convex_pd_induct, simp_all) 

407 

41110  408 
lemma convex_bind_map: 
409 
"convex_bind\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>g = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 

410 
by (simp add: convex_map_def convex_bind_bind) 

411 

412 
lemma convex_map_bind: 

413 
"convex_map\<cdot>f\<cdot>(convex_bind\<cdot>xs\<cdot>g) = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_map\<cdot>f\<cdot>(g\<cdot>x))" 

414 
by (simp add: convex_map_def convex_bind_bind) 

415 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

416 
lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

417 
apply default 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

418 
apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

419 
apply (induct_tac y rule: convex_pd_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

420 
apply (simp_all add: ep_pair.e_p_below monofun_cfun) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

421 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

422 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

423 
lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

424 
apply default 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

425 
apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

426 
apply (induct_tac x rule: convex_pd_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

427 
apply (simp_all add: deflation.below monofun_cfun) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

428 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

429 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

430 
(* FIXME: long proof! *) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

431 
lemma finite_deflation_convex_map: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

432 
assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

433 
proof (rule finite_deflation_intro) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

434 
interpret d: finite_deflation d by fact 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

435 
have "deflation d" by fact 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

436 
thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

437 
have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

438 
hence "finite (Rep_compact_basis ` range (\<lambda>x. d\<cdot>x))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

439 
by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

440 
hence "finite (Pow (Rep_compact_basis ` range (\<lambda>x. d\<cdot>x)))" by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

441 
hence "finite (Rep_pd_basis ` (Pow (Rep_compact_basis ` range (\<lambda>x. d\<cdot>x))))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

442 
by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

443 
hence *: "finite (convex_principal ` Rep_pd_basis ` (Pow (Rep_compact_basis ` range (\<lambda>x. d\<cdot>x))))" by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

444 
hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

445 
apply (rule rev_finite_subset) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

446 
apply clarsimp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

447 
apply (induct_tac xs rule: convex_pd.principal_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

448 
apply (simp add: adm_mem_finite *) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

449 
apply (rename_tac t, induct_tac t rule: pd_basis_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

450 
apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

451 
apply simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

452 
apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b") 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

453 
apply clarsimp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

454 
apply (rule imageI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

455 
apply (rule vimageI2) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

456 
apply (simp add: Rep_PDUnit) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

457 
apply (rule range_eqI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

458 
apply (erule sym) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

459 
apply (rule exI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

460 
apply (rule Abs_compact_basis_inverse [symmetric]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

461 
apply (simp add: d.compact) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

462 
apply (simp only: convex_plus_principal [symmetric] convex_map_plus) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

463 
apply clarsimp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

464 
apply (rule imageI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

465 
apply (rule vimageI2) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

466 
apply (simp add: Rep_PDPlus) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

467 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

468 
thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

469 
by (rule finite_range_imp_finite_fixes) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

470 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

471 

41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
41288
diff
changeset

472 
subsection {* Convex powerdomain is bifinite *} 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

473 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

474 
lemma approx_chain_convex_map: 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

475 
assumes "approx_chain a" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

476 
shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

477 
using assms unfolding approx_chain_def 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

478 
by (simp add: lub_APP convex_map_ID finite_deflation_convex_map) 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

479 

41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41287
diff
changeset

480 
instance convex_pd :: (bifinite) bifinite 
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

481 
proof 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

482 
show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

483 
using bifinite [where 'a='a] 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

484 
by (fast intro!: approx_chain_convex_map) 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

485 
qed 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41111
diff
changeset

486 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

487 
subsection {* Join *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

488 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

489 
definition 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

490 
convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

491 
"convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

492 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

493 
lemma convex_join_unit [simp]: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

494 
"convex_join\<cdot>{xs}\<natural> = xs" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

495 
unfolding convex_join_def by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

496 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

497 
lemma convex_join_plus [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

498 
"convex_join\<cdot>(xss \<union>\<natural> yss) = convex_join\<cdot>xss \<union>\<natural> convex_join\<cdot>yss" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

499 
unfolding convex_join_def by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

500 

40577  501 
lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>" 
502 
unfolding convex_join_def by simp 

503 

25904  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 

518 
subsection {* Conversions to other powerdomains *} 

519 

520 
text {* Convex to upper *} 

521 

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

523 
unfolding convex_le_def by simp 

524 

525 
definition 

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

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

527 
"convex_to_upper = convex_pd.extension upper_principal" 
25904  528 

529 
lemma convex_to_upper_principal [simp]: 

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

531 
unfolding convex_to_upper_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

532 
apply (rule convex_pd.extension_principal) 
27289  533 
apply (rule upper_pd.principal_mono) 
25904  534 
apply (erule convex_le_imp_upper_le) 
535 
done 

536 

537 
lemma convex_to_upper_unit [simp]: 

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

541 
lemma convex_to_upper_plus [simp]: 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

542 
"convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

543 
by (induct xs rule: convex_pd.principal_induct, simp, 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

544 
induct ys rule: convex_pd.principal_induct, simp, simp) 
25904  545 

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

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

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

550 

551 
lemma convex_to_upper_map [simp]: 

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

553 
by (simp add: convex_map_def upper_map_def cfcomp_LAM) 

554 

555 
lemma convex_to_upper_join [simp]: 

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

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

558 
by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun) 

559 

25904  560 
text {* Convex to lower *} 
561 

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

563 
unfolding convex_le_def by simp 

564 

565 
definition 

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

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

567 
"convex_to_lower = convex_pd.extension lower_principal" 
25904  568 

569 
lemma convex_to_lower_principal [simp]: 

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

571 
unfolding convex_to_lower_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

572 
apply (rule convex_pd.extension_principal) 
27289  573 
apply (rule lower_pd.principal_mono) 
25904  574 
apply (erule convex_le_imp_lower_le) 
575 
done 

576 

577 
lemma convex_to_lower_unit [simp]: 

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

581 
lemma convex_to_lower_plus [simp]: 

41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

582 
"convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

583 
by (induct xs rule: convex_pd.principal_induct, simp, 
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

584 
induct ys rule: convex_pd.principal_induct, simp, simp) 
25904  585 

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

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

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

590 

591 
lemma convex_to_lower_map [simp]: 

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

593 
by (simp add: convex_map_def lower_map_def cfcomp_LAM) 

594 

595 
lemma convex_to_lower_join [simp]: 

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

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

598 
by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun) 

599 

25904  600 
text {* Ordering property *} 
601 

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

602 
lemma convex_pd_below_iff: 
25904  603 
"(xs \<sqsubseteq> ys) = 
604 
(convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and> 

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

39970
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

606 
apply (induct xs rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

607 
apply (induct ys rule: convex_pd.principal_induct, simp) 
9023b897e67a
simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu>
parents:
37770
diff
changeset

608 
apply (simp add: convex_le_def) 
25904  609 
done 
610 

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

611 
lemmas convex_plus_below_plus_iff = 
45606  612 
convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"] 
613 
for xs ys zs ws 

26927  614 

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

615 
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

616 
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

617 
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

618 
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

619 
convex_unit_below_iff 
26927  620 
convex_to_upper_unit 
621 
convex_to_upper_plus 

622 
convex_to_lower_unit 

623 
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

624 
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

625 
lower_pd_below_simps 
26927  626 

25904  627 
end 