author  huffman 
Tue, 02 Mar 2010 17:21:10 0800  
changeset 35525  fa231b86cb1e 
parent 35514  a2cfa413eaab 
child 35527  f4282471461d 
permissions  rwrr 
33589  1 
(* Title: HOLCF/Representable.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

33588  5 
header {* Representable Types *} 
6 

7 
theory Representable 

35473  8 
imports Algebraic Universal Ssum Sprod One Fixrec 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

9 
uses 
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

10 
("Tools/repdef.ML") 
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35473
diff
changeset

11 
("Tools/holcf_library.ML") 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35490
diff
changeset

12 
("Tools/Domain/domain_take_proofs.ML") 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

13 
("Tools/Domain/domain_isomorphism.ML") 
33588  14 
begin 
15 

16 
subsection {* Class of representable types *} 

17 

18 
text "Overloaded embedding and projection functions between 

19 
a representable type and the universal domain." 

20 

21 
class rep = bifinite + 

22 
fixes emb :: "'a::pcpo \<rightarrow> udom" 

23 
fixes prj :: "udom \<rightarrow> 'a::pcpo" 

24 
assumes ep_pair_emb_prj: "ep_pair emb prj" 

25 

26 
interpretation rep!: 

27 
pcpo_ep_pair 

28 
"emb :: 'a::rep \<rightarrow> udom" 

29 
"prj :: udom \<rightarrow> 'a::rep" 

30 
unfolding pcpo_ep_pair_def 

31 
by (rule ep_pair_emb_prj) 

32 

33 
lemmas emb_inverse = rep.e_inverse 

34 
lemmas emb_prj_below = rep.e_p_below 

35 
lemmas emb_eq_iff = rep.e_eq_iff 

36 
lemmas emb_strict = rep.e_strict 

37 
lemmas prj_strict = rep.p_strict 

38 

39 

40 
subsection {* Making @{term rep} the default class *} 

41 

42 
text {* 

43 
From now on, free type variables are assumed to be in class 

44 
@{term rep}, unless specified otherwise. 

45 
*} 

46 

47 
defaultsort rep 

48 

49 
subsection {* Representations of types *} 

50 

51 
text "A TypeRep is an algebraic deflation over the universe of values." 

52 

53 
types TypeRep = "udom alg_defl" 

54 
translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl" 

55 

56 
definition 

57 
Rep_of :: "'a::rep itself \<Rightarrow> TypeRep" 

58 
where 

59 
"Rep_of TYPE('a::rep) = 

60 
(\<Squnion>i. alg_defl_principal (Abs_fin_defl 

61 
(emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))" 

62 

63 
syntax "_REP" :: "type \<Rightarrow> TypeRep" ("(1REP/(1'(_')))") 

64 
translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)" 

65 

66 
lemma cast_REP: 

67 
"cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)" 

68 
proof  

69 
let ?a = "\<lambda>i. emb oo approx i oo (prj::udom \<rightarrow> 'a)" 

70 
have a: "\<And>i. finite_deflation (?a i)" 

71 
apply (rule rep.finite_deflation_e_d_p) 

72 
apply (rule finite_deflation_approx) 

73 
done 

74 
show ?thesis 

75 
unfolding Rep_of_def 

76 
apply (subst contlub_cfun_arg) 

77 
apply (rule chainI) 

78 
apply (rule alg_defl.principal_mono) 

79 
apply (rule Abs_fin_defl_mono [OF a a]) 

80 
apply (rule chainE, simp) 

81 
apply (subst cast_alg_defl_principal) 

82 
apply (simp add: Abs_fin_defl_inverse a) 

83 
apply (simp add: expand_cfun_eq lub_distribs) 

84 
done 

85 
qed 

86 

87 
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::rep) = cast\<cdot>REP('a)\<cdot>x" 

88 
by (simp add: cast_REP) 

89 

90 
lemma in_REP_iff: 

91 
"x ::: REP('a::rep) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x" 

92 
by (simp add: in_deflation_def cast_REP) 

93 

94 
lemma prj_inverse: 

95 
"x ::: REP('a::rep) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x" 

96 
by (simp only: in_REP_iff) 

97 

98 
lemma emb_in_REP [simp]: 

99 
"emb\<cdot>(x::'a::rep) ::: REP('a)" 

100 
by (simp add: in_REP_iff) 

101 

102 
subsection {* Coerce operator *} 

103 

104 
definition coerce :: "'a \<rightarrow> 'b" 

105 
where "coerce = prj oo emb" 

106 

107 
lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)" 

108 
by (simp add: coerce_def) 

109 

110 
lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x" 

111 
by (simp add: coerce_def) 

112 

113 
lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>" 

114 
by (simp add: coerce_def) 

115 

116 
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID" 

117 
by (rule ext_cfun, simp add: beta_coerce) 

118 

119 
lemma emb_coerce: 

120 
"REP('a) \<sqsubseteq> REP('b) 

121 
\<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x" 

122 
apply (simp add: beta_coerce) 

123 
apply (rule prj_inverse) 

124 
apply (erule subdeflationD) 

125 
apply (rule emb_in_REP) 

126 
done 

127 

128 
lemma coerce_prj: 

129 
"REP('a) \<sqsubseteq> REP('b) 

130 
\<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x" 

131 
apply (simp add: coerce_def) 

132 
apply (rule emb_eq_iff [THEN iffD1]) 

133 
apply (simp only: emb_prj) 

134 
apply (rule deflation_below_comp1) 

135 
apply (rule deflation_cast) 

136 
apply (rule deflation_cast) 

137 
apply (erule monofun_cfun_arg) 

138 
done 

139 

140 
lemma coerce_coerce [simp]: 

141 
"REP('a) \<sqsubseteq> REP('b) 

142 
\<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x" 

143 
by (simp add: beta_coerce prj_inverse subdeflationD) 

144 

145 
lemma coerce_inverse: 

146 
"emb\<cdot>(x::'a) ::: REP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x" 

147 
by (simp only: beta_coerce prj_inverse emb_inverse) 

148 

149 
lemma coerce_type: 

150 
"REP('a) \<sqsubseteq> REP('b) 

151 
\<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: REP('a)" 

152 
by (simp add: beta_coerce prj_inverse subdeflationD) 

153 

154 
lemma ep_pair_coerce: 

155 
"REP('a) \<sqsubseteq> REP('b) 

156 
\<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)" 

157 
apply (rule ep_pair.intro) 

158 
apply simp 

159 
apply (simp only: beta_coerce) 

160 
apply (rule below_trans) 

161 
apply (rule monofun_cfun_arg) 

162 
apply (rule emb_prj_below) 

163 
apply simp 

164 
done 

165 

33779  166 
text {* Isomorphism lemmas used internally by the domain package: *} 
167 

168 
lemma domain_abs_iso: 

169 
fixes abs and rep 

170 
assumes REP: "REP('b) = REP('a)" 

171 
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" 

172 
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" 

173 
shows "rep\<cdot>(abs\<cdot>x) = x" 

174 
unfolding abs_def rep_def by (simp add: REP) 

175 

176 
lemma domain_rep_iso: 

177 
fixes abs and rep 

178 
assumes REP: "REP('b) = REP('a)" 

179 
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" 

180 
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" 

181 
shows "abs\<cdot>(rep\<cdot>x) = x" 

182 
unfolding abs_def rep_def by (simp add: REP [symmetric]) 

183 

35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset

184 
lemma deflation_abs_rep: 
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset

185 
fixes abs and rep and d 
35489  186 
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" 
187 
assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" 

35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset

188 
shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" 
35489  189 
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) 
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset

190 

35490  191 
lemma deflation_chain_min: 
192 
assumes chain: "chain d" 

193 
assumes defl: "\<And>i. deflation (d i)" 

194 
shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x" 

195 
proof (rule linorder_le_cases) 

196 
assume "i \<le> j" 

197 
with chain have "d i \<sqsubseteq> d j" by (rule chain_mono) 

198 
then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x" 

199 
by (rule deflation_below_comp1 [OF defl defl]) 

200 
moreover from `i \<le> j` have "min i j = i" by simp 

201 
ultimately show ?thesis by simp 

202 
next 

203 
assume "j \<le> i" 

204 
with chain have "d j \<sqsubseteq> d i" by (rule chain_mono) 

205 
then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x" 

206 
by (rule deflation_below_comp2 [OF defl defl]) 

207 
moreover from `j \<le> i` have "min i j = j" by simp 

208 
ultimately show ?thesis by simp 

209 
qed 

210 

33779  211 

33588  212 
subsection {* Proving a subtype is representable *} 
213 

214 
text {* 

215 
Temporarily relax type constraints for @{term "approx"}, 

216 
@{term emb}, and @{term prj}. 

217 
*} 

218 

219 
setup {* Sign.add_const_constraint 

220 
(@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::cpo \<rightarrow> 'a"}) *} 

221 

222 
setup {* Sign.add_const_constraint 

223 
(@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *} 

224 

225 
setup {* Sign.add_const_constraint 

226 
(@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *} 

227 

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

228 
definition 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

229 
repdef_approx :: 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

230 
"('a::pcpo \<Rightarrow> udom) \<Rightarrow> (udom \<Rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> nat \<Rightarrow> 'a \<rightarrow> 'a" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

231 
where 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

232 
"repdef_approx Rep Abs t = (\<lambda>i. \<Lambda> x. Abs (cast\<cdot>(approx i\<cdot>t)\<cdot>(Rep x)))" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

233 

33588  234 
lemma typedef_rep_class: 
235 
fixes Rep :: "'a::pcpo \<Rightarrow> udom" 

236 
fixes Abs :: "udom \<Rightarrow> 'a::pcpo" 

237 
fixes t :: TypeRep 

238 
assumes type: "type_definition Rep Abs {x. x ::: t}" 

239 
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

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

240 
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

241 
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

242 
assumes approx: "(approx :: nat \<Rightarrow> 'a \<rightarrow> 'a) \<equiv> repdef_approx Rep Abs t" 
33588  243 
shows "OFCLASS('a, rep_class)" 
244 
proof 

245 
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})" 

246 
by (simp add: adm_in_deflation) 

247 
have emb_beta: "\<And>x. emb\<cdot>x = Rep x" 

248 
unfolding emb 

249 
apply (rule beta_cfun) 

250 
apply (rule typedef_cont_Rep [OF type below adm]) 

251 
done 

252 
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" 

253 
unfolding prj 

254 
apply (rule beta_cfun) 

255 
apply (rule typedef_cont_Abs [OF type below adm]) 

256 
apply simp_all 

257 
done 

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

258 
have cast_cast_approx: 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

259 
"\<And>i x. cast\<cdot>t\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>x) = cast\<cdot>(approx i\<cdot>t)\<cdot>x" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

260 
apply (rule cast_fixed) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

261 
apply (rule subdeflationD) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

262 
apply (rule approx.below) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

263 
apply (rule cast_in_deflation) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

264 
done 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

265 
have approx': 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

266 
"approx = (\<lambda>i. \<Lambda>(x::'a). prj\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>(emb\<cdot>x)))" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

267 
unfolding approx repdef_approx_def 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

268 
apply (subst cast_cast_approx [symmetric]) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

269 
apply (simp add: prj_beta [symmetric] emb_beta [symmetric]) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

270 
done 
33588  271 
have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t" 
272 
using type_definition.Rep [OF type] 

273 
by (simp add: emb_beta) 

274 
have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" 

275 
unfolding prj_beta 

276 
apply (simp add: cast_fixed [OF emb_in_deflation]) 

277 
apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) 

278 
done 

279 
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" 

280 
unfolding prj_beta emb_beta 

281 
by (simp add: type_definition.Abs_inverse [OF type]) 

282 
show "ep_pair (emb :: 'a \<rightarrow> udom) prj" 

283 
apply default 

284 
apply (simp add: prj_emb) 

285 
apply (simp add: emb_prj cast.below) 

286 
done 

287 
show "chain (approx :: nat \<Rightarrow> 'a \<rightarrow> 'a)" 

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

288 
unfolding approx' by simp 
33588  289 
show "\<And>x::'a. (\<Squnion>i. approx i\<cdot>x) = x" 
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

290 
unfolding approx' 
33588  291 
apply (simp add: lub_distribs) 
292 
apply (subst cast_fixed [OF emb_in_deflation]) 

293 
apply (rule prj_emb) 

294 
done 

295 
show "\<And>(i::nat) (x::'a). approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 

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

296 
unfolding approx' 
33588  297 
apply simp 
298 
apply (simp add: emb_prj) 

299 
apply (simp add: cast_cast_approx) 

300 
done 

301 
show "\<And>i::nat. finite {x::'a. approx i\<cdot>x = x}" 

302 
apply (rule_tac B="(\<lambda>x. prj\<cdot>x) ` {x. cast\<cdot>(approx i\<cdot>t)\<cdot>x = x}" 

303 
in finite_subset) 

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

304 
apply (clarsimp simp add: approx') 
33588  305 
apply (drule_tac f="\<lambda>x. emb\<cdot>x" in arg_cong) 
306 
apply (rule image_eqI) 

307 
apply (rule prj_emb [symmetric]) 

308 
apply (simp add: emb_prj) 

309 
apply (simp add: cast_cast_approx) 

310 
apply (rule finite_imageI) 

311 
apply (simp add: cast_approx_fixed_iff) 

312 
apply (simp add: Collect_conj_eq) 

313 
apply (simp add: finite_fixes_approx) 

314 
done 

315 
qed 

316 

317 
text {* Restore original typing constraints *} 

318 

319 
setup {* Sign.add_const_constraint 

320 
(@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::profinite \<rightarrow> 'a"}) *} 

321 

322 
setup {* Sign.add_const_constraint 

323 
(@{const_name emb}, SOME @{typ "'a::rep \<rightarrow> udom"}) *} 

324 

325 
setup {* Sign.add_const_constraint 

326 
(@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::rep"}) *} 

327 

328 
lemma typedef_REP: 

329 
fixes Rep :: "'a::rep \<Rightarrow> udom" 

330 
fixes Abs :: "udom \<Rightarrow> 'a::rep" 

331 
fixes t :: TypeRep 

332 
assumes type: "type_definition Rep Abs {x. x ::: t}" 

333 
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

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

334 
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

335 
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" 
33588  336 
shows "REP('a) = t" 
337 
proof  

338 
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})" 

339 
by (simp add: adm_in_deflation) 

340 
have emb_beta: "\<And>x. emb\<cdot>x = Rep x" 

341 
unfolding emb 

342 
apply (rule beta_cfun) 

343 
apply (rule typedef_cont_Rep [OF type below adm]) 

344 
done 

345 
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" 

346 
unfolding prj 

347 
apply (rule beta_cfun) 

348 
apply (rule typedef_cont_Abs [OF type below adm]) 

349 
apply simp_all 

350 
done 

351 
have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t" 

352 
using type_definition.Rep [OF type] 

353 
by (simp add: emb_beta) 

354 
have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" 

355 
unfolding prj_beta 

356 
apply (simp add: cast_fixed [OF emb_in_deflation]) 

357 
apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) 

358 
done 

359 
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" 

360 
unfolding prj_beta emb_beta 

361 
by (simp add: type_definition.Abs_inverse [OF type]) 

362 
show "REP('a) = t" 

363 
apply (rule cast_eq_imp_eq, rule ext_cfun) 

364 
apply (simp add: cast_REP emb_prj) 

365 
done 

366 
qed 

367 

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

368 
lemma adm_mem_Collect_in_deflation: "adm (\<lambda>x. x \<in> {x. x ::: A})" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

369 
unfolding mem_Collect_eq by (rule adm_in_deflation) 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

370 

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

371 
use "Tools/repdef.ML" 
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset

372 

33588  373 

374 
subsection {* Instances of class @{text rep} *} 

375 

376 
subsubsection {* Universal Domain *} 

377 

378 
text "The Universal Domain itself is trivially representable." 

379 

380 
instantiation udom :: rep 

381 
begin 

382 

383 
definition emb_udom_def [simp]: "emb = (ID :: udom \<rightarrow> udom)" 

384 
definition prj_udom_def [simp]: "prj = (ID :: udom \<rightarrow> udom)" 

385 

386 
instance 

387 
apply (intro_classes) 

388 
apply (simp_all add: ep_pair.intro) 

389 
done 

390 

391 
end 

392 

393 
subsubsection {* Lifted types *} 

394 

395 
instantiation lift :: (countable) rep 

396 
begin 

397 

398 
definition emb_lift_def: 

399 
"emb = udom_emb oo (FLIFT x. Def (to_nat x))" 

400 

401 
definition prj_lift_def: 

402 
"prj = (FLIFT n. if (\<exists>x::'a::countable. n = to_nat x) 

403 
then Def (THE x::'a. n = to_nat x) else \<bottom>) oo udom_prj" 

404 

405 
instance 

406 
apply (intro_classes, unfold emb_lift_def prj_lift_def) 

407 
apply (rule ep_pair_comp [OF _ ep_pair_udom]) 

408 
apply (rule ep_pair.intro) 

409 
apply (case_tac x, simp, simp) 

410 
apply (case_tac y, simp, clarsimp) 

411 
done 

412 

413 
end 

414 

415 
subsubsection {* Representable type constructors *} 

416 

417 
text "Functions between representable types are representable." 

418 

35525  419 
instantiation cfun :: (rep, rep) rep 
33588  420 
begin 
421 

422 
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb" 

423 
definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj" 

424 

425 
instance 

426 
apply (intro_classes, unfold emb_cfun_def prj_cfun_def) 

427 
apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom) 

428 
done 

429 

430 
end 

431 

432 
text "Strict products of representable types are representable." 

433 

35525  434 
instantiation sprod :: (rep, rep) rep 
33588  435 
begin 
436 

437 
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb" 

438 
definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj" 

439 

440 
instance 

441 
apply (intro_classes, unfold emb_sprod_def prj_sprod_def) 

442 
apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom) 

443 
done 

444 

445 
end 

446 

447 
text "Strict sums of representable types are representable." 

448 

35525  449 
instantiation ssum :: (rep, rep) rep 
33588  450 
begin 
451 

452 
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb" 

453 
definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj" 

454 

455 
instance 

456 
apply (intro_classes, unfold emb_ssum_def prj_ssum_def) 

457 
apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom) 

458 
done 

459 

460 
end 

461 

462 
text "Up of a representable type is representable." 

463 

464 
instantiation "u" :: (rep) rep 

465 
begin 

466 

467 
definition emb_u_def: "emb = udom_emb oo u_map\<cdot>emb" 

468 
definition prj_u_def: "prj = u_map\<cdot>prj oo udom_prj" 

469 

470 
instance 

471 
apply (intro_classes, unfold emb_u_def prj_u_def) 

472 
apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom) 

473 
done 

474 

475 
end 

476 

477 
text "Cartesian products of representable types are representable." 

478 

479 
instantiation "*" :: (rep, rep) rep 

480 
begin 

481 

482 
definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb" 

483 
definition prj_cprod_def: "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj" 

484 

485 
instance 

486 
apply (intro_classes, unfold emb_cprod_def prj_cprod_def) 

487 
apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom) 

488 
done 

489 

490 
end 

491 

492 
subsection {* Type combinators *} 

493 

494 
definition 

495 
TypeRep_fun1 :: 

496 
"((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) 

497 
\<Rightarrow> (TypeRep \<rightarrow> TypeRep)" 

498 
where 

499 
"TypeRep_fun1 f = 

500 
alg_defl.basis_fun (\<lambda>a. 

501 
alg_defl_principal ( 

502 
Abs_fin_defl (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)))" 

503 

504 
definition 

505 
TypeRep_fun2 :: 

506 
"((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) 

507 
\<Rightarrow> (TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep)" 

508 
where 

509 
"TypeRep_fun2 f = 

510 
alg_defl.basis_fun (\<lambda>a. 

511 
alg_defl.basis_fun (\<lambda>b. 

512 
alg_defl_principal ( 

513 
Abs_fin_defl (udom_emb oo 

514 
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))" 

515 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

516 
definition "cfun_defl = TypeRep_fun2 cfun_map" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

517 
definition "ssum_defl = TypeRep_fun2 ssum_map" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

518 
definition "sprod_defl = TypeRep_fun2 sprod_map" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

519 
definition "cprod_defl = TypeRep_fun2 cprod_map" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

520 
definition "u_defl = TypeRep_fun1 u_map" 
33588  521 

522 
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b" 

523 
unfolding below_fin_defl_def . 

524 

525 
lemma cast_TypeRep_fun1: 

526 
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" 

527 
shows "cast\<cdot>(TypeRep_fun1 f\<cdot>A) = udom_emb oo f\<cdot>(cast\<cdot>A) oo udom_prj" 

528 
proof  

529 
have 1: "\<And>a. finite_deflation (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)" 

530 
apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) 

531 
apply (rule f, rule finite_deflation_Rep_fin_defl) 

532 
done 

533 
show ?thesis 

534 
by (induct A rule: alg_defl.principal_induct, simp) 

535 
(simp only: TypeRep_fun1_def 

536 
alg_defl.basis_fun_principal 

537 
alg_defl.basis_fun_mono 

538 
alg_defl.principal_mono 

539 
Abs_fin_defl_mono [OF 1 1] 

540 
monofun_cfun below_refl 

541 
Rep_fin_defl_mono 

542 
cast_alg_defl_principal 

543 
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) 

544 
qed 

545 

546 
lemma cast_TypeRep_fun2: 

547 
assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> 

548 
finite_deflation (f\<cdot>a\<cdot>b)" 

549 
shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) = udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" 

550 
proof  

551 
have 1: "\<And>a b. finite_deflation 

552 
(udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)" 

553 
apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) 

554 
apply (rule f, (rule finite_deflation_Rep_fin_defl)+) 

555 
done 

556 
show ?thesis 

557 
by (induct A B rule: alg_defl.principal_induct2, simp, simp) 

558 
(simp only: TypeRep_fun2_def 

559 
alg_defl.basis_fun_principal 

560 
alg_defl.basis_fun_mono 

561 
alg_defl.principal_mono 

562 
Abs_fin_defl_mono [OF 1 1] 

563 
monofun_cfun below_refl 

564 
Rep_fin_defl_mono 

565 
cast_alg_defl_principal 

566 
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) 

567 
qed 

568 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

569 
lemma cast_cfun_defl: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

570 
"cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

571 
unfolding cfun_defl_def 
33588  572 
apply (rule cast_TypeRep_fun2) 
573 
apply (erule (1) finite_deflation_cfun_map) 

574 
done 

575 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

576 
lemma cast_ssum_defl: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

577 
"cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

578 
unfolding ssum_defl_def 
33588  579 
apply (rule cast_TypeRep_fun2) 
580 
apply (erule (1) finite_deflation_ssum_map) 

581 
done 

582 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

583 
lemma cast_sprod_defl: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

584 
"cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

585 
unfolding sprod_defl_def 
33588  586 
apply (rule cast_TypeRep_fun2) 
587 
apply (erule (1) finite_deflation_sprod_map) 

588 
done 

589 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

590 
lemma cast_cprod_defl: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

591 
"cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

592 
unfolding cprod_defl_def 
33588  593 
apply (rule cast_TypeRep_fun2) 
594 
apply (erule (1) finite_deflation_cprod_map) 

595 
done 

596 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

597 
lemma cast_u_defl: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

598 
"cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

599 
unfolding u_defl_def 
33588  600 
apply (rule cast_TypeRep_fun1) 
601 
apply (erule finite_deflation_u_map) 

602 
done 

603 

604 
text {* REP of type constructor = type combinator *} 

605 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

606 
lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)" 
33588  607 
apply (rule cast_eq_imp_eq, rule ext_cfun) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

608 
apply (simp add: cast_REP cast_cfun_defl) 
33588  609 
apply (simp add: cfun_map_def) 
610 
apply (simp only: prj_cfun_def emb_cfun_def) 

611 
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom]) 

612 
done 

613 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

614 
lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)" 
33588  615 
apply (rule cast_eq_imp_eq, rule ext_cfun) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

616 
apply (simp add: cast_REP cast_ssum_defl) 
33588  617 
apply (simp add: prj_ssum_def) 
618 
apply (simp add: emb_ssum_def) 

619 
apply (simp add: ssum_map_map cfcomp1) 

620 
done 

621 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

622 
lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)" 
33588  623 
apply (rule cast_eq_imp_eq, rule ext_cfun) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

624 
apply (simp add: cast_REP cast_sprod_defl) 
33588  625 
apply (simp add: prj_sprod_def) 
626 
apply (simp add: emb_sprod_def) 

627 
apply (simp add: sprod_map_map cfcomp1) 

628 
done 

629 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

630 
lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)" 
33588  631 
apply (rule cast_eq_imp_eq, rule ext_cfun) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

632 
apply (simp add: cast_REP cast_cprod_defl) 
33588  633 
apply (simp add: prj_cprod_def) 
634 
apply (simp add: emb_cprod_def) 

635 
apply (simp add: cprod_map_map cfcomp1) 

636 
done 

637 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

638 
lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)" 
33588  639 
apply (rule cast_eq_imp_eq, rule ext_cfun) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

640 
apply (simp add: cast_REP cast_u_defl) 
33588  641 
apply (simp add: prj_u_def) 
642 
apply (simp add: emb_u_def) 

643 
apply (simp add: u_map_map cfcomp1) 

644 
done 

645 

646 
lemmas REP_simps = 

647 
REP_cfun 

648 
REP_ssum 

649 
REP_sprod 

650 
REP_cprod 

651 
REP_up 

652 

653 
subsection {* Isomorphic deflations *} 

654 

655 
definition 

656 
isodefl :: "('a::rep \<rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> bool" 

657 
where 

658 
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj" 

659 

660 
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t" 

661 
unfolding isodefl_def by (simp add: ext_cfun) 

662 

663 
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))" 

664 
unfolding isodefl_def by (simp add: ext_cfun) 

665 

666 
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" 

667 
unfolding isodefl_def 

668 
by (drule cfun_fun_cong [where x="\<bottom>"], simp) 

669 

670 
lemma isodefl_imp_deflation: 

671 
fixes d :: "'a::rep \<rightarrow> 'a" 

672 
assumes "isodefl d t" shows "deflation d" 

673 
proof 

674 
note prems [unfolded isodefl_def, simp] 

675 
fix x :: 'a 

676 
show "d\<cdot>(d\<cdot>x) = d\<cdot>x" 

677 
using cast.idem [of t "emb\<cdot>x"] by simp 

678 
show "d\<cdot>x \<sqsubseteq> x" 

679 
using cast.below [of t "emb\<cdot>x"] by simp 

680 
qed 

681 

682 
lemma isodefl_ID_REP: "isodefl (ID :: 'a \<rightarrow> 'a) REP('a)" 

683 
unfolding isodefl_def by (simp add: cast_REP) 

684 

685 
lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) REP('a) \<Longrightarrow> d = ID" 

686 
unfolding isodefl_def 

687 
apply (simp add: cast_REP) 

688 
apply (simp add: expand_cfun_eq) 

689 
apply (rule allI) 

690 
apply (drule_tac x="emb\<cdot>x" in spec) 

691 
apply simp 

692 
done 

693 

694 
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>" 

695 
unfolding isodefl_def by (simp add: expand_cfun_eq) 

696 

697 
lemma adm_isodefl: 

698 
"cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))" 

699 
unfolding isodefl_def by simp 

700 

701 
lemma isodefl_lub: 

702 
assumes "chain d" and "chain t" 

703 
assumes "\<And>i. isodefl (d i) (t i)" 

704 
shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)" 

705 
using prems unfolding isodefl_def 

706 
by (simp add: contlub_cfun_arg contlub_cfun_fun) 

707 

708 
lemma isodefl_fix: 

709 
assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)" 

710 
shows "isodefl (fix\<cdot>f) (fix\<cdot>g)" 

711 
unfolding fix_def2 

712 
apply (rule isodefl_lub, simp, simp) 

713 
apply (induct_tac i) 

714 
apply (simp add: isodefl_bottom) 

715 
apply (simp add: prems) 

716 
done 

717 

718 
lemma isodefl_coerce: 

719 
fixes d :: "'a \<rightarrow> 'a" 

720 
assumes REP: "REP('b) = REP('a)" 

721 
shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t" 

722 
unfolding isodefl_def 

723 
apply (simp add: expand_cfun_eq) 

724 
apply (simp add: emb_coerce coerce_prj REP) 

725 
done 

726 

33779  727 
lemma isodefl_abs_rep: 
728 
fixes abs and rep and d 

729 
assumes REP: "REP('b) = REP('a)" 

730 
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" 

731 
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" 

732 
shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t" 

733 
unfolding abs_def rep_def using REP by (rule isodefl_coerce) 

734 

33588  735 
lemma isodefl_cfun: 
736 
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

737 
isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)" 
33588  738 
apply (rule isodeflI) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

739 
apply (simp add: cast_cfun_defl cast_isodefl) 
33588  740 
apply (simp add: emb_cfun_def prj_cfun_def) 
741 
apply (simp add: cfun_map_map cfcomp1) 

742 
done 

743 

744 
lemma isodefl_ssum: 

745 
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

746 
isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)" 
33588  747 
apply (rule isodeflI) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

748 
apply (simp add: cast_ssum_defl cast_isodefl) 
33588  749 
apply (simp add: emb_ssum_def prj_ssum_def) 
750 
apply (simp add: ssum_map_map isodefl_strict) 

751 
done 

752 

753 
lemma isodefl_sprod: 

754 
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

755 
isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)" 
33588  756 
apply (rule isodeflI) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

757 
apply (simp add: cast_sprod_defl cast_isodefl) 
33588  758 
apply (simp add: emb_sprod_def prj_sprod_def) 
759 
apply (simp add: sprod_map_map isodefl_strict) 

760 
done 

761 

33786  762 
lemma isodefl_cprod: 
763 
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> 

764 
isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)" 

765 
apply (rule isodeflI) 

766 
apply (simp add: cast_cprod_defl cast_isodefl) 

767 
apply (simp add: emb_cprod_def prj_cprod_def) 

768 
apply (simp add: cprod_map_map cfcomp1) 

769 
done 

770 

33588  771 
lemma isodefl_u: 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

772 
"isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)" 
33588  773 
apply (rule isodeflI) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset

774 
apply (simp add: cast_u_defl cast_isodefl) 
33588  775 
apply (simp add: emb_u_def prj_u_def) 
776 
apply (simp add: u_map_map) 

777 
done 

778 

33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

779 
subsection {* Constructing Domain Isomorphisms *} 
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

780 

35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35473
diff
changeset

781 
use "Tools/holcf_library.ML" 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35490
diff
changeset

782 
use "Tools/Domain/domain_take_proofs.ML" 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

783 
use "Tools/Domain/domain_isomorphism.ML" 
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

784 

364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

785 
setup {* 
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

786 
fold Domain_Isomorphism.add_type_constructor 
35525  787 
[(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun}, 
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

788 
@{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}), 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

789 

35525  790 
(@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum}, 
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

791 
@{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}), 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

792 

35525  793 
(@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod}, 
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

794 
@{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

795 

35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

796 
(@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, 
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

797 
@{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

798 

35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

799 
(@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up}, 
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset

800 
@{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})] 
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

801 
*} 
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset

802 

33588  803 
end 