author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 49834  b27bbb021df1 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/LowerPD.thy 
25904  2 
Author: Brian Huffman 
3 
*) 

4 

5 
header {* Lower powerdomain *} 

6 

7 
theory LowerPD 

41284  8 
imports Compact_Basis 
25904  9 
begin 
10 

11 
subsection {* Basis preorder *} 

12 

13 
definition 

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

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

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

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

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

18 
unfolding lower_le_def by fast 
25904  19 

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

21 
unfolding lower_le_def 

22 
apply (rule ballI) 

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

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

25 
apply (erule rev_bexI) 

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

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

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

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

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

33 
unfolding lower_le_def Rep_PDUnit 

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

35 

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

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

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

40 
unfolding lower_le_def Rep_PDPlus by fast 

41 

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

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

43 
unfolding lower_le_def Rep_PDPlus by fast 
25904  44 

45 
lemma lower_le_PDUnit_PDUnit_iff [simp]: 

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

49 
lemma lower_le_PDUnit_PDPlus_iff: 

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

51 
unfolding lower_le_def Rep_PDPlus Rep_PDUnit by fast 

52 

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

54 
unfolding lower_le_def Rep_PDPlus by fast 

55 

56 
lemma lower_le_induct [induct set: lower_le]: 

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

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

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

61 
shows "P t u" 

62 
using le 

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

64 
apply (erule rev_mp) 

65 
apply (induct_tac u rule: pd_basis_induct) 

66 
apply (simp add: 1) 

67 
apply (simp add: lower_le_PDUnit_PDPlus_iff) 

68 
apply (simp add: 2) 

69 
apply (subst PDPlus_commute) 

70 
apply (simp add: 2) 

71 
apply (simp add: lower_le_PDPlus_iff 3) 

72 
done 

73 

74 

75 
subsection {* Type definition *} 

76 

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

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

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

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

80 

41111  81 
type_notation (xsymbols) lower_pd ("('(_')\<flat>)") 
82 

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

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

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

85 

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

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

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

88 

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

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

90 
end 
25904  91 

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

92 
instance lower_pd :: (bifinite) po 
39984  93 
using type_definition_lower_pd below_lower_pd_def 
94 
by (rule lower_le.typedef_ideal_po) 

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

95 

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

96 
instance lower_pd :: (bifinite) cpo 
39984  97 
using type_definition_lower_pd below_lower_pd_def 
98 
by (rule lower_le.typedef_ideal_cpo) 

25904  99 

100 
definition 

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

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

102 
"lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}" 
25904  103 

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

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

105 
ideal_completion lower_le lower_principal Rep_lower_pd 
39984  106 
using type_definition_lower_pd below_lower_pd_def 
107 
using lower_principal_def pd_basis_countable 

108 
by (rule lower_le.typedef_ideal_completion) 

25904  109 

27289  110 
text {* Lower powerdomain is pointed *} 
25904  111 

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

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

114 

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

115 
instance lower_pd :: (bifinite) pcpo 
26927  116 
by intro_classes (fast intro: lower_pd_minimal) 
25904  117 

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

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

119 
by (rule lower_pd_minimal [THEN bottomI, symmetric]) 
25904  120 

121 

26927  122 
subsection {* Monadic unit and plus *} 
25904  123 

124 
definition 

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

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

126 
"lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))" 
25904  127 

128 
definition 

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

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

130 
"lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u. 
25904  131 
lower_principal (PDPlus t u)))" 
132 

133 
abbreviation 

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

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

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

136 
"xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys" 
25904  137 

26927  138 
syntax 
41479  139 
"_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>") 
26927  140 

141 
translations 

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

142 
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>" 
26927  143 
"{x}\<flat>" == "CONST lower_unit\<cdot>x" 
144 

145 
lemma lower_unit_Rep_compact_basis [simp]: 

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

147 
unfolding lower_unit_def 

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

148 
by (simp add: compact_basis.extension_principal PDUnit_lower_mono) 
26927  149 

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

151 
"lower_principal t \<union>\<flat> lower_principal u = lower_principal (PDPlus t u)" 
25904  152 
unfolding lower_plus_def 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

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

154 
lower_pd.extension_mono PDPlus_lower_mono) 
25904  155 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

173 
qed 
26927  174 

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

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

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

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

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

179 
lemmas lower_plus_left_absorb = lower_add.left_idem 
26927  180 

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

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

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

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

184 

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

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

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

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

188 

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

189 
lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

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

191 
apply (induct ys rule: lower_pd.principal_induct, 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

192 
apply (simp add: PDPlus_lower_le) 
25904  193 
done 
194 

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

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

196 
by (subst lower_plus_commute, rule lower_plus_below1) 
25904  197 

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

198 
lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<union>\<flat> ys \<sqsubseteq> zs" 
25904  199 
apply (subst lower_plus_absorb [of zs, symmetric]) 
200 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 

201 
done 

202 

40734  203 
lemma lower_plus_below_iff [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

204 
"xs \<union>\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs" 
25904  205 
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

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

207 
apply (erule below_trans [OF lower_plus_below2]) 
25904  208 
apply (erule (1) lower_plus_least) 
209 
done 

210 

40734  211 
lemma lower_unit_below_plus_iff [simp]: 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

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

213 
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

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

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

216 
apply (simp add: lower_le_PDUnit_PDPlus_iff) 
25904  217 
done 
218 

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

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

220 
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

221 
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

222 
apply simp 
26927  223 
done 
224 

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

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

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

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

228 
lower_unit_below_plus_iff 
25904  229 

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

231 
by (simp add: po_eq_conv) 
26927  232 

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

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

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

235 
by (simp add: inst_lower_pd_pcpo) 
26927  236 

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

237 
lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>" 
26927  238 
unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff) 
239 

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

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

241 
"xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>" 
26927  242 
apply safe 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41402
diff
changeset

243 
apply (rule bottomI, erule subst, rule lower_plus_below1) 
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41402
diff
changeset

244 
apply (rule bottomI, erule subst, rule lower_plus_below2) 
26927  245 
apply (rule lower_plus_absorb) 
246 
done 

247 

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

248 
lemma lower_plus_strict1 [simp]: "\<bottom> \<union>\<flat> ys = ys" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

249 
apply (rule below_antisym [OF _ lower_plus_below2]) 
26927  250 
apply (simp add: lower_plus_least) 
251 
done 

252 

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

253 
lemma lower_plus_strict2 [simp]: "xs \<union>\<flat> \<bottom> = xs" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

254 
apply (rule below_antisym [OF _ lower_plus_below1]) 
26927  255 
apply (simp add: lower_plus_least) 
256 
done 

257 

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

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

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

260 

26927  261 
lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

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

265 
done 
26927  266 

267 
lemma compact_lower_plus [simp]: 

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

268 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<flat> ys)" 
27289  269 
by (auto dest!: lower_pd.compact_imp_principal) 
26927  270 

25904  271 

272 
subsection {* Induction rules *} 

273 

274 
lemma lower_pd_induct1: 

275 
assumes P: "adm P" 

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

278 
"\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)" 
25904  279 
shows "P (xs::'a lower_pd)" 
27289  280 
apply (induct xs rule: lower_pd.principal_induct, rule P) 
281 
apply (induct_tac a rule: pd_basis_induct1) 

25904  282 
apply (simp only: lower_unit_Rep_compact_basis [symmetric]) 
283 
apply (rule unit) 

284 
apply (simp only: lower_unit_Rep_compact_basis [symmetric] 

285 
lower_plus_principal [symmetric]) 

286 
apply (erule insert [OF unit]) 

287 
done 

288 

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

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

290 
[case_names adm lower_unit lower_plus, induct type: lower_pd]: 
25904  291 
assumes P: "adm P" 
26927  292 
assumes unit: "\<And>x. P {x}\<flat>" 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

293 
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)" 
25904  294 
shows "P (xs::'a lower_pd)" 
27289  295 
apply (induct xs rule: lower_pd.principal_induct, rule P) 
296 
apply (induct_tac a rule: pd_basis_induct) 

25904  297 
apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit) 
298 
apply (simp only: lower_plus_principal [symmetric] plus) 

299 
done 

300 

301 

302 
subsection {* Monadic bind *} 

303 

304 
definition 

305 
lower_bind_basis :: 

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

307 
"lower_bind_basis = fold_pd 

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

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

309 
(\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)" 
25904  310 

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

312 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)" 
25904  313 
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

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

316 
apply (simp add: eta_cfun) 
25904  317 
done 
318 

319 
lemma lower_bind_basis_simps [simp]: 

320 
"lower_bind_basis (PDUnit a) = 

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

322 
"lower_bind_basis (PDPlus t u) = 

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

323 
(\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)" 
25904  324 
unfolding lower_bind_basis_def 
325 
apply  

26927  326 
apply (rule fold_pd_PDUnit [OF ACI_lower_bind]) 
327 
apply (rule fold_pd_PDPlus [OF ACI_lower_bind]) 

25904  328 
done 
329 

330 
lemma lower_bind_basis_mono: 

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

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

332 
unfolding cfun_below_iff 
25904  333 
apply (erule lower_le_induct, safe) 
27289  334 
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

335 
apply (simp add: rev_below_trans [OF lower_plus_below1]) 
40734  336 
apply simp 
25904  337 
done 
338 

339 
definition 

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

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

341 
"lower_bind = lower_pd.extension lower_bind_basis" 
25904  342 

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

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

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

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

346 

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

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

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

349 

25904  350 
lemma lower_bind_principal [simp]: 
351 
"lower_bind\<cdot>(lower_principal t) = lower_bind_basis t" 

352 
unfolding lower_bind_def 

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

353 
apply (rule lower_pd.extension_principal) 
25904  354 
apply (erule lower_bind_basis_mono) 
355 
done 

356 

357 
lemma lower_bind_unit [simp]: 

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

361 
lemma lower_bind_plus [simp]: 

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

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

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

364 
induct ys rule: lower_pd.principal_induct, simp, simp) 
25904  365 

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

367 
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit) 

368 

40589  369 
lemma lower_bind_bind: 
370 
"lower_bind\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_bind\<cdot>(f\<cdot>x)\<cdot>g)" 

371 
by (induct xs, simp_all) 

372 

25904  373 

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

374 
subsection {* Map *} 
25904  375 

376 
definition 

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

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

380 
lemma lower_map_unit [simp]: 

26927  381 
"lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>" 
25904  382 
unfolding lower_map_def by simp 
383 

384 
lemma lower_map_plus [simp]: 

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

385 
"lower_map\<cdot>f\<cdot>(xs \<union>\<flat> ys) = lower_map\<cdot>f\<cdot>xs \<union>\<flat> lower_map\<cdot>f\<cdot>ys" 
25904  386 
unfolding lower_map_def by simp 
387 

40577  388 
lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>" 
389 
unfolding lower_map_def by simp 

390 

25904  391 
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 
392 
by (induct xs rule: lower_pd_induct, simp_all) 

393 

33808  394 
lemma lower_map_ID: "lower_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

395 
by (simp add: cfun_eq_iff ID_def lower_map_ident) 
33808  396 

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

399 
by (induct xs rule: lower_pd_induct, simp_all) 

400 

41110  401 
lemma lower_bind_map: 
402 
"lower_bind\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 

403 
by (simp add: lower_map_def lower_bind_bind) 

404 

405 
lemma lower_map_bind: 

406 
"lower_map\<cdot>f\<cdot>(lower_bind\<cdot>xs\<cdot>g) = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_map\<cdot>f\<cdot>(g\<cdot>x))" 

407 
by (simp add: lower_map_def lower_bind_bind) 

408 

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

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

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

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

412 
apply (induct_tac y rule: lower_pd_induct) 
40734  413 
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff) 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

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

415 

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

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

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

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

419 
apply (induct_tac x rule: lower_pd_induct) 
40734  420 
apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff) 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

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

422 

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

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

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

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

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

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

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

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

430 
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

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

432 
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

433 
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

434 
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

435 
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

436 
hence *: "finite (lower_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

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

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

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

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

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

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

443 
apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

445 
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

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

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

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

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

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

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

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

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

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

455 
apply (simp only: lower_plus_principal [symmetric] lower_map_plus) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

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

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

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

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

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

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

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

464 

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

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

466 

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

467 
lemma approx_chain_lower_map: 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41284
diff
changeset

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

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

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

471 
by (simp add: lub_APP lower_map_ID finite_deflation_lower_map) 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41284
diff
changeset

472 

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

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

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

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

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

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

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

479 

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

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

481 

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

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

483 
lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

485 

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

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

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

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

489 

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

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

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

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

493 

40577  494 
lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>" 
495 
unfolding lower_join_def by simp 

496 

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

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

498 
"lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

499 
by (induct xs rule: lower_pd_induct, simp_all) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

500 

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

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

502 
"lower_join\<cdot>(lower_map\<cdot>lower_join\<cdot>xsss) = lower_join\<cdot>(lower_join\<cdot>xsss)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

503 
by (induct xsss rule: lower_pd_induct, simp_all) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

504 

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

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

506 
"lower_join\<cdot>(lower_map\<cdot>(lower_map\<cdot>f)\<cdot>xss) = 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

507 
lower_map\<cdot>f\<cdot>(lower_join\<cdot>xss)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

508 
by (induct xss rule: lower_pd_induct, simp_all) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

509 

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

510 
end 