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

4 

5 
header {* Upper powerdomain *} 

6 

7 
theory UpperPD 

41284  8 
imports Compact_Basis 
25904  9 
begin 
10 

11 
subsection {* Basis preorder *} 

12 

13 
definition 

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

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

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

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

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

18 
unfolding upper_le_def by fast 
25904  19 

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

21 
unfolding upper_le_def 

22 
apply (rule ballI) 

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

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

25 
apply (erule rev_bexI) 

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

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

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

29 
interpretation upper_le: preorder upper_le 
25904  30 
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans) 
31 

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

33 
unfolding upper_le_def Rep_PDUnit by simp 

34 

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

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

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

39 
unfolding upper_le_def Rep_PDPlus by fast 

40 

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

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

42 
unfolding upper_le_def Rep_PDPlus by fast 
25904  43 

44 
lemma upper_le_PDUnit_PDUnit_iff [simp]: 

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

48 
lemma upper_le_PDPlus_PDUnit_iff: 

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

50 
unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast 

51 

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

53 
unfolding upper_le_def Rep_PDPlus by fast 

54 

55 
lemma upper_le_induct [induct set: upper_le]: 

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

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

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

60 
shows "P t u" 

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

62 
apply (erule rev_mp) 

63 
apply (induct_tac t rule: pd_basis_induct) 

64 
apply (simp add: 1) 

65 
apply (simp add: upper_le_PDPlus_PDUnit_iff) 

66 
apply (simp add: 2) 

67 
apply (subst PDPlus_commute) 

68 
apply (simp add: 2) 

69 
apply (simp add: upper_le_PDPlus_iff 3) 

70 
done 

71 

72 

73 
subsection {* Type definition *} 

74 

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

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

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

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

78 

41111  79 
type_notation (xsymbols) upper_pd ("('(_')\<sharp>)") 
80 

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

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

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

83 

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

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

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

86 

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

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

88 
end 
25904  89 

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

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

91 
using type_definition_upper_pd below_upper_pd_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

93 

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

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

95 
using type_definition_upper_pd below_upper_pd_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

97 

25904  98 
definition 
99 
upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where 

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

100 
"upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}" 
25904  101 

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

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

103 
ideal_completion upper_le upper_principal Rep_upper_pd 
39984  104 
using type_definition_upper_pd below_upper_pd_def 
105 
using upper_principal_def pd_basis_countable 

106 
by (rule upper_le.typedef_ideal_completion) 

25904  107 

27289  108 
text {* Upper powerdomain is pointed *} 
25904  109 

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

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

112 

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

113 
instance upper_pd :: (bifinite) pcpo 
26927  114 
by intro_classes (fast intro: upper_pd_minimal) 
25904  115 

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

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

117 
by (rule upper_pd_minimal [THEN bottomI, symmetric]) 
25904  118 

119 

26927  120 
subsection {* Monadic unit and plus *} 
25904  121 

122 
definition 

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

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

124 
"upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))" 
25904  125 

126 
definition 

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

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

128 
"upper_plus = upper_pd.extension (\<lambda>t. upper_pd.extension (\<lambda>u. 
25904  129 
upper_principal (PDPlus t u)))" 
130 

131 
abbreviation 

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

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

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

134 
"xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys" 
25904  135 

26927  136 
syntax 
41479  137 
"_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>") 
26927  138 

139 
translations 

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

140 
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>" 
26927  141 
"{x}\<sharp>" == "CONST upper_unit\<cdot>x" 
142 

143 
lemma upper_unit_Rep_compact_basis [simp]: 

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

145 
unfolding upper_unit_def 

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

146 
by (simp add: compact_basis.extension_principal PDUnit_upper_mono) 
26927  147 

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

149 
"upper_principal t \<union>\<sharp> upper_principal u = upper_principal (PDPlus t u)" 
25904  150 
unfolding upper_plus_def 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41289
diff
changeset

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

152 
upper_pd.extension_mono PDPlus_upper_mono) 
25904  153 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

171 
qed 
26927  172 

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

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

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

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

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

177 
lemmas upper_plus_left_absorb = upper_add.left_idem 
26927  178 

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

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

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

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

182 

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

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

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

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

186 

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

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

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

189 
apply (induct ys rule: upper_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

190 
apply (simp add: PDPlus_upper_le) 
25904  191 
done 
192 

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

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

194 
by (subst upper_plus_commute, rule upper_plus_below1) 
25904  195 

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

196 
lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys \<union>\<sharp> zs" 
25904  197 
apply (subst upper_plus_absorb [of xs, symmetric]) 
198 
apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 

199 
done 

200 

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

202 
"xs \<sqsubseteq> ys \<union>\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs" 
25904  203 
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

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

205 
apply (erule below_trans [OF _ upper_plus_below2]) 
25904  206 
apply (erule (1) upper_plus_greatest) 
207 
done 

208 

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

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

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

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

213 
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

214 
apply (simp add: upper_le_PDPlus_PDUnit_iff) 
25904  215 
done 
216 

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

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

218 
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

219 
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

220 
apply simp 
26927  221 
done 
222 

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

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

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

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

226 
upper_plus_below_unit_iff 
25904  227 

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

230 

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

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

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

233 
by (simp add: inst_upper_pd_pcpo) 
26927  234 

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

235 
lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41402
diff
changeset

236 
by (rule bottomI, rule upper_plus_below1) 
26927  237 

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

238 
lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41402
diff
changeset

239 
by (rule bottomI, rule upper_plus_below2) 
26927  240 

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

241 
lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>" 
26927  242 
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff) 
243 

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

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

245 
"xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>" 
41402
b647212cee03
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
huffman
parents:
41399
diff
changeset

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

247 
apply (induct ys rule: upper_pd.principal_induct, simp) 
27289  248 
apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff 
26927  249 
upper_le_PDPlus_PDUnit_iff) 
250 
done 

251 

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

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

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

254 

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

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

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

259 
done 
26927  260 

261 
lemma compact_upper_plus [simp]: 

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

262 
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)" 
27289  263 
by (auto dest!: upper_pd.compact_imp_principal) 
26927  264 

25904  265 

266 
subsection {* Induction rules *} 

267 

268 
lemma upper_pd_induct1: 

269 
assumes P: "adm P" 

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

271 
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)" 
25904  272 
shows "P (xs::'a upper_pd)" 
27289  273 
apply (induct xs rule: upper_pd.principal_induct, rule P) 
274 
apply (induct_tac a rule: pd_basis_induct1) 

25904  275 
apply (simp only: upper_unit_Rep_compact_basis [symmetric]) 
276 
apply (rule unit) 

277 
apply (simp only: upper_unit_Rep_compact_basis [symmetric] 

278 
upper_plus_principal [symmetric]) 

279 
apply (erule insert [OF unit]) 

280 
done 

281 

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

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

283 
[case_names adm upper_unit upper_plus, induct type: upper_pd]: 
25904  284 
assumes P: "adm P" 
26927  285 
assumes unit: "\<And>x. P {x}\<sharp>" 
41399
ad093e4638e2
changed syntax of powerdomain binary union operators
huffman
parents:
41394
diff
changeset

286 
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)" 
25904  287 
shows "P (xs::'a upper_pd)" 
27289  288 
apply (induct xs rule: upper_pd.principal_induct, rule P) 
289 
apply (induct_tac a rule: pd_basis_induct) 

25904  290 
apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit) 
291 
apply (simp only: upper_plus_principal [symmetric] plus) 

292 
done 

293 

294 

295 
subsection {* Monadic bind *} 

296 

297 
definition 

298 
upper_bind_basis :: 

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

300 
"upper_bind_basis = fold_pd 

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

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

302 
(\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)" 
25904  303 

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

305 
"class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)" 
25904  306 
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

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

309 
apply (simp add: eta_cfun) 
25904  310 
done 
311 

312 
lemma upper_bind_basis_simps [simp]: 

313 
"upper_bind_basis (PDUnit a) = 

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

315 
"upper_bind_basis (PDPlus t u) = 

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

316 
(\<Lambda> f. upper_bind_basis t\<cdot>f \<union>\<sharp> upper_bind_basis u\<cdot>f)" 
25904  317 
unfolding upper_bind_basis_def 
318 
apply  

26927  319 
apply (rule fold_pd_PDUnit [OF ACI_upper_bind]) 
320 
apply (rule fold_pd_PDPlus [OF ACI_upper_bind]) 

25904  321 
done 
322 

323 
lemma upper_bind_basis_mono: 

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

325 
unfolding cfun_below_iff 
25904  326 
apply (erule upper_le_induct, safe) 
27289  327 
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

328 
apply (simp add: below_trans [OF upper_plus_below1]) 
40734  329 
apply simp 
25904  330 
done 
331 

332 
definition 

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

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

334 
"upper_bind = upper_pd.extension upper_bind_basis" 
25904  335 

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

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

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

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

339 

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

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

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

342 

25904  343 
lemma upper_bind_principal [simp]: 
344 
"upper_bind\<cdot>(upper_principal t) = upper_bind_basis t" 

345 
unfolding upper_bind_def 

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

346 
apply (rule upper_pd.extension_principal) 
25904  347 
apply (erule upper_bind_basis_mono) 
348 
done 

349 

350 
lemma upper_bind_unit [simp]: 

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

354 
lemma upper_bind_plus [simp]: 

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

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

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

357 
induct ys rule: upper_pd.principal_induct, simp, simp) 
25904  358 

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

360 
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) 

361 

40589  362 
lemma upper_bind_bind: 
363 
"upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)" 

364 
by (induct xs, simp_all) 

365 

25904  366 

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

367 
subsection {* Map *} 
25904  368 

369 
definition 

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

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

373 
lemma upper_map_unit [simp]: 

26927  374 
"upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>" 
25904  375 
unfolding upper_map_def by simp 
376 

377 
lemma upper_map_plus [simp]: 

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

378 
"upper_map\<cdot>f\<cdot>(xs \<union>\<sharp> ys) = upper_map\<cdot>f\<cdot>xs \<union>\<sharp> upper_map\<cdot>f\<cdot>ys" 
25904  379 
unfolding upper_map_def by simp 
380 

40577  381 
lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>" 
382 
unfolding upper_map_def by simp 

383 

25904  384 
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 
385 
by (induct xs rule: upper_pd_induct, simp_all) 

386 

33808  387 
lemma upper_map_ID: "upper_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

388 
by (simp add: cfun_eq_iff ID_def upper_map_ident) 
33808  389 

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

392 
by (induct xs rule: upper_pd_induct, simp_all) 

393 

41110  394 
lemma upper_bind_map: 
395 
"upper_bind\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 

396 
by (simp add: upper_map_def upper_bind_bind) 

397 

398 
lemma upper_map_bind: 

399 
"upper_map\<cdot>f\<cdot>(upper_bind\<cdot>xs\<cdot>g) = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_map\<cdot>f\<cdot>(g\<cdot>x))" 

400 
by (simp add: upper_map_def upper_bind_bind) 

401 

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

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

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

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

405 
apply (induct_tac y rule: upper_pd_induct) 
40734  406 
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff) 
33585
8d39394fe5cf
ep_pair and deflation lemmas for powerdomain map functions
huffman
parents:
31076
diff
changeset

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

408 

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

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

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

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

412 
apply (induct_tac x rule: upper_pd_induct) 
40734  413 
apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_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 

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

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

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

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

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

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

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

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

423 
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

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

425 
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

426 
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

427 
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

428 
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

429 
hence *: "finite (upper_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

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

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

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

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

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

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

436 
apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

438 
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

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

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

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

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

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

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

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

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

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

448 
apply (simp only: upper_plus_principal [symmetric] upper_map_plus) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

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

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

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

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

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

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

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

457 

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

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

459 

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

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

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

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

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

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

465 

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

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

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

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

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

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

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

472 

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

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

474 

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

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

476 
upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

478 

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

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

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

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

482 

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

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

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

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

486 

40577  487 
lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>" 
488 
unfolding upper_join_def by simp 

489 

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

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

491 
"upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39970
diff
changeset

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

493 

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

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

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

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

497 

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

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

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

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

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

502 

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

503 
end 