author  huffman 
Fri, 13 Nov 2009 15:31:20 0800  
changeset 33679  331712879666 
parent 33591  51091e1041a7 
child 33779  b8efeea2cebd 
permissions  rwrr 
33591  1 
(* Title: HOLCF/ex/Domain_Proofs.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Internal domain package proofs done manually *} 

6 

7 
theory Domain_Proofs 

8 
imports HOLCF 

9 
begin 

10 

11 
defaultsort rep 

12 

13 
(* 

14 

15 
The definitions and proofs below are for the following recursive 

16 
datatypes: 

17 

18 
domain 'a foo = Foo1  Foo2 (lazy 'a) (lazy "'a bar") 

19 
and 'a bar = Bar (lazy 'a) (lazy "'a baz") 

20 
and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd") 

21 

22 
*) 

23 

24 
(********************************************************************) 

25 

26 
subsection {* Step 1: Define the new type combinators *} 

27 

28 
text {* Start with the onestep nonrecursive version *} 

29 

30 
definition 

31 
foo_bar_baz_typF :: 

32 
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep" 

33 
where 

34 
"foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3). 

35 
( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2)) 

36 
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3) 

37 
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))" 

38 

39 
lemma foo_bar_baz_typF_beta: 

40 
"foo_bar_baz_typF\<cdot>a\<cdot>t = 

41 
( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t)))) 

42 
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t))) 

43 
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))" 

44 
unfolding foo_bar_baz_typF_def 

45 
by (simp add: csplit_def cfst_def csnd_def) 

46 

47 
text {* Individual type combinators are projected from the fixed point. *} 

48 

49 
definition foo_typ :: "TypeRep \<rightarrow> TypeRep" 

50 
where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))" 

51 

52 
definition bar_typ :: "TypeRep \<rightarrow> TypeRep" 

53 
where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))" 

54 

55 
definition baz_typ :: "TypeRep \<rightarrow> TypeRep" 

56 
where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))" 

57 

58 
text {* Unfold rules for each combinator. *} 

59 

60 
lemma foo_typ_unfold: 

61 
"foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))" 

62 
unfolding foo_typ_def bar_typ_def baz_typ_def 

63 
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) 

64 

65 
lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))" 

66 
unfolding foo_typ_def bar_typ_def baz_typ_def 

67 
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) 

68 

69 
lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))" 

70 
unfolding foo_typ_def bar_typ_def baz_typ_def 

71 
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) 

72 

73 
text "The automation for the previous steps will be quite similar to 

74 
how the fixrec package works." 

75 

76 
(********************************************************************) 

77 

78 
subsection {* Step 2: Define types, prove class instances *} 

79 

80 
text {* Use @{text pcpodef} with the appropriate type combinator. *} 

81 

82 
pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}" 

83 
by (simp_all add: adm_in_deflation) 

84 

85 
pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}" 

86 
by (simp_all add: adm_in_deflation) 

87 

88 
pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}" 

89 
by (simp_all add: adm_in_deflation) 

90 

91 
text {* Prove rep instance using lemma @{text typedef_rep_class}. *} 

92 

93 
instantiation foo :: (rep) rep 

94 
begin 

95 

96 
definition emb_foo :: "'a foo \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

97 
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" 
33591  98 

99 
definition prj_foo :: "udom \<rightarrow> 'a foo" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

100 
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))" 
33591  101 

102 
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

103 
where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))" 
33591  104 

105 
instance 

106 
apply (rule typedef_rep_class) 

107 
apply (rule type_definition_foo) 

108 
apply (rule below_foo_def) 

109 
apply (rule emb_foo_def) 

110 
apply (rule prj_foo_def) 

111 
apply (rule approx_foo_def) 

112 
done 

113 

114 
end 

115 

116 
instantiation bar :: (rep) rep 

117 
begin 

118 

119 
definition emb_bar :: "'a bar \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

120 
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" 
33591  121 

122 
definition prj_bar :: "udom \<rightarrow> 'a bar" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

123 
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))" 
33591  124 

125 
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

126 
where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))" 
33591  127 

128 
instance 

129 
apply (rule typedef_rep_class) 

130 
apply (rule type_definition_bar) 

131 
apply (rule below_bar_def) 

132 
apply (rule emb_bar_def) 

133 
apply (rule prj_bar_def) 

134 
apply (rule approx_bar_def) 

135 
done 

136 

137 
end 

138 

139 
instantiation baz :: (rep) rep 

140 
begin 

141 

142 
definition emb_baz :: "'a baz \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

143 
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" 
33591  144 

145 
definition prj_baz :: "udom \<rightarrow> 'a baz" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

146 
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))" 
33591  147 

148 
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

149 
where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))" 
33591  150 

151 
instance 

152 
apply (rule typedef_rep_class) 

153 
apply (rule type_definition_baz) 

154 
apply (rule below_baz_def) 

155 
apply (rule emb_baz_def) 

156 
apply (rule prj_baz_def) 

157 
apply (rule approx_baz_def) 

158 
done 

159 

160 
end 

161 

162 
text {* Prove REP rules using lemma @{text typedef_REP}. *} 

163 

164 
lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)" 

165 
apply (rule typedef_REP) 

166 
apply (rule type_definition_foo) 

167 
apply (rule below_foo_def) 

168 
apply (rule emb_foo_def) 

169 
apply (rule prj_foo_def) 

170 
done 

171 

172 
lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)" 

173 
apply (rule typedef_REP) 

174 
apply (rule type_definition_bar) 

175 
apply (rule below_bar_def) 

176 
apply (rule emb_bar_def) 

177 
apply (rule prj_bar_def) 

178 
done 

179 

180 
lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)" 

181 
apply (rule typedef_REP) 

182 
apply (rule type_definition_baz) 

183 
apply (rule below_baz_def) 

184 
apply (rule emb_baz_def) 

185 
apply (rule prj_baz_def) 

186 
done 

187 

188 
text {* Prove REP equations using type combinator unfold lemmas. *} 

189 

190 
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" 

191 
unfolding REP_foo REP_bar REP_baz REP_simps 

192 
by (rule foo_typ_unfold) 

193 

194 
lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)" 

195 
unfolding REP_foo REP_bar REP_baz REP_simps 

196 
by (rule bar_typ_unfold) 

197 

198 
lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)" 

199 
unfolding REP_foo REP_bar REP_baz REP_simps 

200 
by (rule baz_typ_unfold) 

201 

202 
(********************************************************************) 

203 

204 
subsection {* Step 3: Define rep and abs functions *} 

205 

206 
text {* Define them all using @{text coerce}! *} 

207 

208 
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" 

209 
where "foo_rep = coerce" 

210 

211 
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" 

212 
where "foo_abs = coerce" 

213 

214 
definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>" 

215 
where "bar_rep = coerce" 

216 

217 
definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar" 

218 
where "bar_abs = coerce" 

219 

220 
definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>" 

221 
where "baz_rep = coerce" 

222 

223 
definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz" 

224 
where "baz_abs = coerce" 

225 

226 
text {* Prove isodefl rules using @{text isodefl_coerce}. *} 

227 

228 
lemma isodefl_foo_abs: 

229 
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" 

230 
unfolding foo_abs_def foo_rep_def 

231 
by (rule isodefl_coerce [OF REP_foo']) 

232 

233 
lemma isodefl_bar_abs: 

234 
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" 

235 
unfolding bar_abs_def bar_rep_def 

236 
by (rule isodefl_coerce [OF REP_bar']) 

237 

238 
lemma isodefl_baz_abs: 

239 
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" 

240 
unfolding baz_abs_def baz_rep_def 

241 
by (rule isodefl_coerce [OF REP_baz']) 

242 

243 
text {* TODO: prove iso predicate for rep and abs. *} 

244 

245 
(********************************************************************) 

246 

247 
subsection {* Step 4: Define map functions, prove isodefl property *} 

248 

249 
text {* Start with the onestep nonrecursive version. *} 

250 

251 
text {* Note that the type of the map function depends on which 

252 
variables are used in positive and negative positions. *} 

253 

254 
definition 

255 
foo_bar_baz_mapF :: 

256 
"('a \<rightarrow> 'b) 

257 
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz) 

258 
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)" 

259 
where 

260 
"foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3). 

261 
( 

262 
foo_abs oo 

263 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) 

264 
oo foo_rep 

265 
, 

266 
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep 

267 
, 

268 
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep 

269 
))" 

270 

271 
lemma foo_bar_baz_mapF_beta: 

272 
"foo_bar_baz_mapF\<cdot>f\<cdot>d = 

273 
( 

274 
foo_abs oo 

275 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) 

276 
oo foo_rep 

277 
, 

278 
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep 

279 
, 

280 
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep 

281 
)" 

282 
unfolding foo_bar_baz_mapF_def 

283 
by (simp add: csplit_def cfst_def csnd_def) 

284 

285 
text {* Individual map functions are projected from the fixed point. *} 

286 

287 
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" 

288 
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" 

289 

290 
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" 

291 
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" 

292 

293 
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)" 

294 
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" 

295 

296 
text {* Prove isodefl rules for all map functions simultaneously. *} 

297 

298 
lemma isodefl_foo_bar_baz: 

299 
assumes isodefl_d: "isodefl d t" 

300 
shows 

301 
"isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and> 

302 
isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and> 

303 
isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)" 

304 
apply (simp add: foo_map_def bar_map_def baz_map_def) 

305 
apply (simp add: foo_typ_def bar_typ_def baz_typ_def) 

306 
apply (rule parallel_fix_ind 

307 
[where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"]) 

308 
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) 

309 
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) 

310 
apply (simp only: foo_bar_baz_mapF_beta 

311 
foo_bar_baz_typF_beta 

312 
fst_conv snd_conv) 

313 
apply (elim conjE) 

314 
apply (intro 

315 
conjI 

316 
isodefl_foo_abs 

317 
isodefl_bar_abs 

318 
isodefl_baz_abs 

319 
isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex 

320 
isodefl_d 

321 
) 

322 
apply assumption+ 

323 
done 

324 

325 
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] 

326 
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] 

327 
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] 

328 

329 
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} 

330 

331 
lemma foo_map_ID: "foo_map\<cdot>ID = ID" 

332 
apply (rule isodefl_REP_imp_ID) 

333 
apply (subst REP_foo) 

334 
apply (rule isodefl_foo) 

335 
apply (rule isodefl_ID_REP) 

336 
done 

337 

338 
lemma bar_map_ID: "bar_map\<cdot>ID = ID" 

339 
apply (rule isodefl_REP_imp_ID) 

340 
apply (subst REP_bar) 

341 
apply (rule isodefl_bar) 

342 
apply (rule isodefl_ID_REP) 

343 
done 

344 

345 
lemma baz_map_ID: "baz_map\<cdot>ID = ID" 

346 
apply (rule isodefl_REP_imp_ID) 

347 
apply (subst REP_baz) 

348 
apply (rule isodefl_baz) 

349 
apply (rule isodefl_ID_REP) 

350 
done 

351 

352 
(********************************************************************) 

353 

354 
subsection {* Step 5: Define copy functions, prove reach lemmas *} 

355 

356 
definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID" 

357 
definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))" 

358 
definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))" 

359 
definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))" 

360 

361 
lemma fix_foo_bar_baz_copy: 

362 
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)" 

363 
unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def 

364 
by simp 

365 

366 
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x" 

367 
unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID) 

368 

369 
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" 

370 
unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID) 

371 

372 
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" 

373 
unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID) 

374 

375 
end 