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

4 

5 
header {* Domain package support *} 

6 

7 
theory Domain_Aux 

40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset

8 
imports Map_Functions Fixrec 
35652  9 
uses 
10 
("Tools/Domain/domain_take_proofs.ML") 

40503  11 
("Tools/cont_consts.ML") 
12 
("Tools/cont_proc.ML") 

13 
("Tools/Domain/domain_constructors.ML") 

14 
("Tools/Domain/domain_induction.ML") 

35652  15 
begin 
16 

35653  17 
subsection {* Continuous isomorphisms *} 
18 

19 
text {* A locale for continuous isomorphisms *} 

20 

21 
locale iso = 

22 
fixes abs :: "'a \<rightarrow> 'b" 

23 
fixes rep :: "'b \<rightarrow> 'a" 

24 
assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x" 

25 
assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y" 

26 
begin 

27 

28 
lemma swap: "iso rep abs" 

29 
by (rule iso.intro [OF rep_iso abs_iso]) 

30 

31 
lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)" 

32 
proof 

33 
assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" 

34 
then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg) 

35 
then show "x \<sqsubseteq> y" by simp 

36 
next 

37 
assume "x \<sqsubseteq> y" 

38 
then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg) 

39 
qed 

40 

41 
lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)" 

42 
by (rule iso.abs_below [OF swap]) 

43 

44 
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)" 

45 
by (simp add: po_eq_conv abs_below) 

46 

47 
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)" 

48 
by (rule iso.abs_eq [OF swap]) 

49 

50 
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>" 

51 
proof  

52 
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" .. 

53 
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg) 

54 
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp 

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

55 
then show ?thesis by (rule bottomI) 
35653  56 
qed 
57 

58 
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>" 

59 
by (rule iso.abs_strict [OF swap]) 

60 

61 
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>" 

62 
proof  

63 
have "x = rep\<cdot>(abs\<cdot>x)" by simp 

64 
also assume "abs\<cdot>x = \<bottom>" 

65 
also note rep_strict 

66 
finally show "x = \<bottom>" . 

67 
qed 

68 

69 
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" 

70 
by (rule iso.abs_defin' [OF swap]) 

71 

72 
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>" 

73 
by (erule contrapos_nn, erule abs_defin') 

74 

75 
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" 

76 
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms) 

77 

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

78 
lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)" 
35653  79 
by (auto elim: abs_defin' intro: abs_strict) 
80 

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

81 
lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)" 
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40216
diff
changeset

82 
by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms) 
35653  83 

84 
lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P" 

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

85 
by (simp add: rep_bottom_iff) 
35653  86 

87 
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" 

88 
proof (unfold compact_def) 

41182  89 
assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> y)" 
40327  90 
with cont_Rep_cfun2 
41182  91 
have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst) 
92 
then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp 

35653  93 
qed 
94 

95 
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x" 

96 
by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms) 

97 

98 
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)" 

99 
by (rule compact_rep_rev) simp 

100 

101 
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)" 

102 
by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms) 

103 

104 
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)" 

105 
proof 

106 
assume "x = abs\<cdot>y" 

107 
then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp 

108 
then show "rep\<cdot>x = y" by simp 

109 
next 

110 
assume "rep\<cdot>x = y" 

111 
then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp 

112 
then show "x = abs\<cdot>y" by simp 

113 
qed 

114 

115 
end 

116 

35652  117 
subsection {* Proofs about take functions *} 
118 

119 
text {* 

120 
This section contains lemmas that are used in a module that supports 

121 
the domain isomorphism package; the module contains proofs related 

122 
to take functions and the finiteness predicate. 

123 
*} 

124 

125 
lemma deflation_abs_rep: 

126 
fixes abs and rep and d 

127 
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" 

128 
assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" 

129 
shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" 

130 
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) 

131 

132 
lemma deflation_chain_min: 

133 
assumes chain: "chain d" 

134 
assumes defl: "\<And>n. deflation (d n)" 

135 
shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" 

136 
proof (rule linorder_le_cases) 

137 
assume "m \<le> n" 

138 
with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) 

139 
then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" 

140 
by (rule deflation_below_comp1 [OF defl defl]) 

141 
moreover from `m \<le> n` have "min m n = m" by simp 

142 
ultimately show ?thesis by simp 

143 
next 

144 
assume "n \<le> m" 

145 
with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) 

146 
then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" 

147 
by (rule deflation_below_comp2 [OF defl defl]) 

148 
moreover from `n \<le> m` have "min m n = n" by simp 

149 
ultimately show ?thesis by simp 

150 
qed 

151 

35653  152 
lemma lub_ID_take_lemma: 
153 
assumes "chain t" and "(\<Squnion>n. t n) = ID" 

154 
assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y" 

155 
proof  

156 
have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)" 

157 
using assms(3) by simp 

158 
then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y" 

159 
using assms(1) by (simp add: lub_distribs) 

160 
then show "x = y" 

161 
using assms(2) by simp 

162 
qed 

163 

164 
lemma lub_ID_reach: 

165 
assumes "chain t" and "(\<Squnion>n. t n) = ID" 

166 
shows "(\<Squnion>n. t n\<cdot>x) = x" 

167 
using assms by (simp add: lub_distribs) 

168 

35655  169 
lemma lub_ID_take_induct: 
170 
assumes "chain t" and "(\<Squnion>n. t n) = ID" 

171 
assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x" 

172 
proof  

173 
from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp 

174 
from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD) 

175 
with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs) 

176 
qed 

177 

35653  178 
subsection {* Finiteness *} 
179 

180 
text {* 

181 
Let a ``decisive'' function be a deflation that maps every input to 

182 
either itself or bottom. Then if a domain's take functions are all 

183 
decisive, then all values in the domain are finite. 

184 
*} 

185 

186 
definition 

187 
decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool" 

188 
where 

189 
"decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)" 

190 

191 
lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d" 

192 
unfolding decisive_def by simp 

193 

194 
lemma decisive_cases: 

195 
assumes "decisive d" obtains "d\<cdot>x = x"  "d\<cdot>x = \<bottom>" 

196 
using assms unfolding decisive_def by auto 

197 

198 
lemma decisive_bottom: "decisive \<bottom>" 

199 
unfolding decisive_def by simp 

200 

201 
lemma decisive_ID: "decisive ID" 

202 
unfolding decisive_def by simp 

203 

204 
lemma decisive_ssum_map: 

205 
assumes f: "decisive f" 

206 
assumes g: "decisive g" 

207 
shows "decisive (ssum_map\<cdot>f\<cdot>g)" 

208 
apply (rule decisiveI, rename_tac s) 

209 
apply (case_tac s, simp_all) 

210 
apply (rule_tac x=x in decisive_cases [OF f], simp_all) 

211 
apply (rule_tac x=y in decisive_cases [OF g], simp_all) 

212 
done 

213 

214 
lemma decisive_sprod_map: 

215 
assumes f: "decisive f" 

216 
assumes g: "decisive g" 

217 
shows "decisive (sprod_map\<cdot>f\<cdot>g)" 

218 
apply (rule decisiveI, rename_tac s) 

219 
apply (case_tac s, simp_all) 

220 
apply (rule_tac x=x in decisive_cases [OF f], simp_all) 

221 
apply (rule_tac x=y in decisive_cases [OF g], simp_all) 

222 
done 

223 

224 
lemma decisive_abs_rep: 

225 
fixes abs rep 

226 
assumes iso: "iso abs rep" 

227 
assumes d: "decisive d" 

228 
shows "decisive (abs oo d oo rep)" 

229 
apply (rule decisiveI) 

230 
apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d]) 

231 
apply (simp add: iso.rep_iso [OF iso]) 

232 
apply (simp add: iso.abs_strict [OF iso]) 

233 
done 

234 

235 
lemma lub_ID_finite: 

236 
assumes chain: "chain d" 

237 
assumes lub: "(\<Squnion>n. d n) = ID" 

238 
assumes decisive: "\<And>n. decisive (d n)" 

239 
shows "\<exists>n. d n\<cdot>x = x" 

240 
proof  

241 
have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp 

242 
have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach) 

243 
have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>" 

244 
using decisive unfolding decisive_def by simp 

245 
hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}" 

246 
by auto 

247 
hence "finite (range (\<lambda>n. d n\<cdot>x))" 

248 
by (rule finite_subset, simp) 

249 
with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)" 

250 
by (rule finite_range_imp_finch) 

251 
then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x" 

252 
unfolding finite_chain_def by (auto simp add: maxinch_is_thelub) 

253 
with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym) 

254 
qed 

255 

35655  256 
lemma lub_ID_finite_take_induct: 
257 
assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)" 

258 
shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x" 

259 
using lub_ID_finite [OF assms] by metis 

260 

40503  261 
subsection {* Proofs about constructor functions *} 
262 

263 
text {* Lemmas for proving nchotomy rule: *} 

264 

265 
lemma ex_one_bottom_iff: 

266 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE" 

267 
by simp 

268 

269 
lemma ex_up_bottom_iff: 

270 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" 

271 
by (safe, case_tac x, auto) 

272 

273 
lemma ex_sprod_bottom_iff: 

274 
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = 

275 
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" 

276 
by (safe, case_tac y, auto) 

277 

278 
lemma ex_sprod_up_bottom_iff: 

279 
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = 

280 
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" 

281 
by (safe, case_tac y, simp, case_tac x, auto) 

282 

283 
lemma ex_ssum_bottom_iff: 

284 
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = 

285 
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or> 

286 
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))" 

287 
by (safe, case_tac x, auto) 

288 

289 
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)" 

290 
by auto 

291 

292 
lemmas ex_bottom_iffs = 

293 
ex_ssum_bottom_iff 

294 
ex_sprod_up_bottom_iff 

295 
ex_sprod_bottom_iff 

296 
ex_up_bottom_iff 

297 
ex_one_bottom_iff 

298 

299 
text {* Rules for turning nchotomy into exhaust: *} 

300 

301 
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *) 

302 
by auto 

303 

304 
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)" 

305 
by rule auto 

306 

307 
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" 

308 
by rule auto 

309 

310 
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)" 

311 
by rule auto 

312 

313 
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 

314 

315 
text {* Rules for proving constructor properties *} 

316 

317 
lemmas con_strict_rules = 

318 
sinl_strict sinr_strict spair_strict1 spair_strict2 

319 

320 
lemmas con_bottom_iff_rules = 

321 
sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined 

322 

323 
lemmas con_below_iff_rules = 

324 
sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules 

325 

326 
lemmas con_eq_iff_rules = 

327 
sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules 

328 

329 
lemmas sel_strict_rules = 

330 
cfcomp2 sscase1 sfst_strict ssnd_strict fup1 

331 

332 
lemma sel_app_extra_rules: 

333 
"sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>" 

334 
"sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x" 

335 
"sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>" 

336 
"sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x" 

337 
"fup\<cdot>ID\<cdot>(up\<cdot>x) = x" 

338 
by (cases "x = \<bottom>", simp, simp)+ 

339 

340 
lemmas sel_app_rules = 

341 
sel_strict_rules sel_app_extra_rules 

342 
ssnd_spair sfst_spair up_defined spair_defined 

343 

344 
lemmas sel_bottom_iff_rules = 

345 
cfcomp2 sfst_bottom_iff ssnd_bottom_iff 

346 

347 
lemmas take_con_rules = 

348 
ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up 

349 
deflation_strict deflation_ID ID1 cfcomp2 

350 

35653  351 
subsection {* ML setup *} 
352 

35652  353 
use "Tools/Domain/domain_take_proofs.ML" 
40503  354 
use "Tools/cont_consts.ML" 
355 
use "Tools/cont_proc.ML" 

356 
use "Tools/Domain/domain_constructors.ML" 

357 
use "Tools/Domain/domain_induction.ML" 

35652  358 

40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
35655
diff
changeset

359 
setup Domain_Take_Proofs.setup 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
35655
diff
changeset

360 

35652  361 
end 