author  haftmann 
Tue, 02 Sep 2008 12:07:34 +0200  
changeset 28073  5e9f00f4f209 
parent 27296  eec7a1889ca5 
child 29138  661a8db7e647 
permissions  rwrr 
16697  1 
(* Title: HOLCF/Pcpodef.thy 
2 
ID: $Id$ 

3 
Author: Brian Huffman 

4 
*) 

5 

6 
header {* Subtypes of pcpos *} 

7 

8 
theory Pcpodef 

9 
imports Adm 

23152  10 
uses ("Tools/pcpodef_package.ML") 
16697  11 
begin 
12 

13 
subsection {* Proving a subtype is a partial order *} 

14 

15 
text {* 

16 
A subtype of a partial order is itself a partial order, 

17 
if the ordering is defined in the standard way. 

18 
*} 

19 

28073  20 
setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *} 
21 

16697  22 
theorem typedef_po: 
28073  23 
fixes Abs :: "'a::po \<Rightarrow> 'b::type" 
16697  24 
assumes type: "type_definition Rep Abs A" 
25 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

26 
shows "OFCLASS('b, po_class)" 

27 
apply (intro_classes, unfold less) 

28 
apply (rule refl_less) 

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

29 
apply (erule (1) trans_less) 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26027
diff
changeset

30 
apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26027
diff
changeset

31 
apply (erule (1) antisym_less) 
16697  32 
done 
33 

28073  34 
setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, 
35 
SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *} 

36 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

37 
subsection {* Proving a subtype is finite *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

38 

27296
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

39 
lemma typedef_finite_UNIV: 
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

40 
fixes Abs :: "'a::type \<Rightarrow> 'b::type" 
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

41 
assumes type: "type_definition Rep Abs A" 
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

42 
shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)" 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

43 
proof  
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

44 
assume "finite A" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

45 
hence "finite (Abs ` A)" by (rule finite_imageI) 
27296
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

46 
thus "finite (UNIV :: 'b set)" 
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

47 
by (simp only: type_definition.Abs_image [OF type]) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

48 
qed 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

49 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

50 
theorem typedef_finite_po: 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

51 
fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

52 
assumes type: "type_definition Rep Abs A" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

53 
shows "OFCLASS('b, finite_po_class)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

54 
apply (intro_classes) 
27296
eec7a1889ca5
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman
parents:
26420
diff
changeset

55 
apply (rule typedef_finite_UNIV [OF type]) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

56 
apply (rule finite) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

57 
done 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
23152
diff
changeset

58 

17812  59 
subsection {* Proving a subtype is chainfinite *} 
60 

61 
lemma monofun_Rep: 

62 
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

63 
shows "monofun Rep" 

64 
by (rule monofunI, unfold less) 

65 

66 
lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep] 

67 
lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep] 

68 

69 
theorem typedef_chfin: 

70 
fixes Abs :: "'a::chfin \<Rightarrow> 'b::po" 

71 
assumes type: "type_definition Rep Abs A" 

72 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

73 
shows "OFCLASS('b, chfin_class)" 

25921  74 
apply intro_classes 
17812  75 
apply (drule ch2ch_Rep [OF less]) 
25921  76 
apply (drule chfin) 
17812  77 
apply (unfold max_in_chain_def) 
78 
apply (simp add: type_definition.Rep_inject [OF type]) 

79 
done 

80 

16697  81 
subsection {* Proving a subtype is complete *} 
82 

83 
text {* 

84 
A subtype of a cpo is itself a cpo if the ordering is 

85 
defined in the standard way, and the defining subset 

86 
is closed with respect to limits of chains. A set is 

87 
closed if and only if membership in the set is an 

88 
admissible predicate. 

89 
*} 

90 

16918  91 
lemma Abs_inverse_lub_Rep: 
16697  92 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 
93 
assumes type: "type_definition Rep Abs A" 

94 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

95 
and adm: "adm (\<lambda>x. x \<in> A)" 

16918  96 
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))" 
97 
apply (rule type_definition.Abs_inverse [OF type]) 

25925  98 
apply (erule admD [OF adm ch2ch_Rep [OF less]]) 
16697  99 
apply (rule type_definition.Rep [OF type]) 
100 
done 

101 

16918  102 
theorem typedef_lub: 
16697  103 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 
104 
assumes type: "type_definition Rep Abs A" 

105 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

106 
and adm: "adm (\<lambda>x. x \<in> A)" 

16918  107 
shows "chain S \<Longrightarrow> range S << Abs (\<Squnion>i. Rep (S i))" 
108 
apply (frule ch2ch_Rep [OF less]) 

16697  109 
apply (rule is_lubI) 
110 
apply (rule ub_rangeI) 

16918  111 
apply (simp only: less Abs_inverse_lub_Rep [OF type less adm]) 
112 
apply (erule is_ub_thelub) 

113 
apply (simp only: less Abs_inverse_lub_Rep [OF type less adm]) 

114 
apply (erule is_lub_thelub) 

115 
apply (erule ub2ub_Rep [OF less]) 

16697  116 
done 
117 

16918  118 
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard] 
119 

16697  120 
theorem typedef_cpo: 
121 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 

122 
assumes type: "type_definition Rep Abs A" 

123 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

124 
and adm: "adm (\<lambda>x. x \<in> A)" 

125 
shows "OFCLASS('b, cpo_class)" 

16918  126 
proof 
127 
fix S::"nat \<Rightarrow> 'b" assume "chain S" 

128 
hence "range S << Abs (\<Squnion>i. Rep (S i))" 

129 
by (rule typedef_lub [OF type less adm]) 

130 
thus "\<exists>x. range S << x" .. 

131 
qed 

16697  132 

133 
subsubsection {* Continuity of @{term Rep} and @{term Abs} *} 

134 

135 
text {* For any subcpo, the @{term Rep} function is continuous. *} 

136 

137 
theorem typedef_cont_Rep: 

138 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

139 
assumes type: "type_definition Rep Abs A" 

140 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

141 
and adm: "adm (\<lambda>x. x \<in> A)" 

142 
shows "cont Rep" 

143 
apply (rule contI) 

16918  144 
apply (simp only: typedef_thelub [OF type less adm]) 
145 
apply (simp only: Abs_inverse_lub_Rep [OF type less adm]) 

26027  146 
apply (rule cpo_lubI) 
16918  147 
apply (erule ch2ch_Rep [OF less]) 
16697  148 
done 
149 

150 
text {* 

151 
For a subcpo, we can make the @{term Abs} function continuous 

152 
only if we restrict its domain to the defining subset by 

153 
composing it with another continuous function. 

154 
*} 

155 

16918  156 
theorem typedef_is_lubI: 
157 
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

158 
shows "range (\<lambda>i. Rep (S i)) << Rep x \<Longrightarrow> range S << x" 

159 
apply (rule is_lubI) 

160 
apply (rule ub_rangeI) 

161 
apply (subst less) 

162 
apply (erule is_ub_lub) 

163 
apply (subst less) 

164 
apply (erule is_lub_lub) 

165 
apply (erule ub2ub_Rep [OF less]) 

166 
done 

167 

16697  168 
theorem typedef_cont_Abs: 
169 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

170 
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" 

171 
assumes type: "type_definition Rep Abs A" 

172 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

16918  173 
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) 
16697  174 
and f_in_A: "\<And>x. f x \<in> A" 
175 
and cont_f: "cont f" 

176 
shows "cont (\<lambda>x. Abs (f x))" 

177 
apply (rule contI) 

16918  178 
apply (rule typedef_is_lubI [OF less]) 
179 
apply (simp only: type_definition.Abs_inverse [OF type f_in_A]) 

180 
apply (erule cont_f [THEN contE]) 

16697  181 
done 
182 

17833  183 
subsection {* Proving subtype elements are compact *} 
184 

185 
theorem typedef_compact: 

186 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

187 
assumes type: "type_definition Rep Abs A" 

188 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

189 
and adm: "adm (\<lambda>x. x \<in> A)" 

190 
shows "compact (Rep k) \<Longrightarrow> compact k" 

191 
proof (unfold compact_def) 

192 
have cont_Rep: "cont Rep" 

193 
by (rule typedef_cont_Rep [OF type less adm]) 

194 
assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)" 

195 
with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst) 

196 
thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less) 

197 
qed 

198 

16697  199 
subsection {* Proving a subtype is pointed *} 
200 

201 
text {* 

202 
A subtype of a cpo has a least element if and only if 

203 
the defining subset has a least element. 

204 
*} 

205 

16918  206 
theorem typedef_pcpo_generic: 
16697  207 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 
208 
assumes type: "type_definition Rep Abs A" 

209 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

210 
and z_in_A: "z \<in> A" 

211 
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x" 

212 
shows "OFCLASS('b, pcpo_class)" 

213 
apply (intro_classes) 

214 
apply (rule_tac x="Abs z" in exI, rule allI) 

215 
apply (unfold less) 

216 
apply (subst type_definition.Abs_inverse [OF type z_in_A]) 

217 
apply (rule z_least [OF type_definition.Rep [OF type]]) 

218 
done 

219 

220 
text {* 

221 
As a special case, a subtype of a pcpo has a least element 

222 
if the defining subset contains @{term \<bottom>}. 

223 
*} 

224 

16918  225 
theorem typedef_pcpo: 
16697  226 
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" 
227 
assumes type: "type_definition Rep Abs A" 

228 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

229 
and UU_in_A: "\<bottom> \<in> A" 

230 
shows "OFCLASS('b, pcpo_class)" 

16918  231 
by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal) 
16697  232 

233 
subsubsection {* Strictness of @{term Rep} and @{term Abs} *} 

234 

235 
text {* 

236 
For a subpcpo where @{term \<bottom>} is a member of the defining 

237 
subset, @{term Rep} and @{term Abs} are both strict. 

238 
*} 

239 

240 
theorem typedef_Abs_strict: 

241 
assumes type: "type_definition Rep Abs A" 

242 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

243 
and UU_in_A: "\<bottom> \<in> A" 

244 
shows "Abs \<bottom> = \<bottom>" 

245 
apply (rule UU_I, unfold less) 

246 
apply (simp add: type_definition.Abs_inverse [OF type UU_in_A]) 

247 
done 

248 

249 
theorem typedef_Rep_strict: 

250 
assumes type: "type_definition Rep Abs A" 

251 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

252 
and UU_in_A: "\<bottom> \<in> A" 

253 
shows "Rep \<bottom> = \<bottom>" 

254 
apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst]) 

255 
apply (rule type_definition.Abs_inverse [OF type UU_in_A]) 

256 
done 

257 

25926  258 
theorem typedef_Abs_strict_iff: 
259 
assumes type: "type_definition Rep Abs A" 

260 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

261 
and UU_in_A: "\<bottom> \<in> A" 

262 
shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)" 

263 
apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst]) 

264 
apply (simp add: type_definition.Abs_inject [OF type] UU_in_A) 

265 
done 

266 

267 
theorem typedef_Rep_strict_iff: 

268 
assumes type: "type_definition Rep Abs A" 

269 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

270 
and UU_in_A: "\<bottom> \<in> A" 

271 
shows "(Rep x = \<bottom>) = (x = \<bottom>)" 

272 
apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst]) 

273 
apply (simp add: type_definition.Rep_inject [OF type]) 

274 
done 

275 

16697  276 
theorem typedef_Abs_defined: 
277 
assumes type: "type_definition Rep Abs A" 

278 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

279 
and UU_in_A: "\<bottom> \<in> A" 

280 
shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>" 

25926  281 
by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A]) 
16697  282 

283 
theorem typedef_Rep_defined: 

284 
assumes type: "type_definition Rep Abs A" 

285 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

286 
and UU_in_A: "\<bottom> \<in> A" 

287 
shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>" 

25926  288 
by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A]) 
16697  289 

19519  290 
subsection {* Proving a subtype is flat *} 
291 

292 
theorem typedef_flat: 

293 
fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" 

294 
assumes type: "type_definition Rep Abs A" 

295 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

296 
and UU_in_A: "\<bottom> \<in> A" 

297 
shows "OFCLASS('b, flat_class)" 

298 
apply (intro_classes) 

299 
apply (unfold less) 

300 
apply (simp add: type_definition.Rep_inject [OF type, symmetric]) 

301 
apply (simp add: typedef_Rep_strict [OF type less UU_in_A]) 

302 
apply (simp add: ax_flat) 

303 
done 

304 

16697  305 
subsection {* HOLCF type definition package *} 
306 

23152  307 
use "Tools/pcpodef_package.ML" 
16697  308 

309 
end 