author  huffman 
Mon, 20 Dec 2010 09:48:16 0800  
changeset 41323  ae1c227534f5 
parent 41321  4e72b6fc9dd4 
child 41392  d1ff42a70f77 
permissions  rwrr 
29534  1 
(* Title: HOLCF/Sum_Cpo.thy 
29130  2 
Author: Brian Huffman 
3 
*) 

4 

5 
header {* The cpo of disjoint sums *} 

6 

29534  7 
theory Sum_Cpo 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39808
diff
changeset

8 
imports HOLCF 
29130  9 
begin 
10 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
31076
diff
changeset

11 
subsection {* Ordering on sum type *} 
29130  12 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37111
diff
changeset

13 
instantiation sum :: (below, below) below 
29130  14 
begin 
15 

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

16 
definition below_sum_def: 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

17 
"x \<sqsubseteq> y \<equiv> case x of 
29130  18 
Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b  Inr b \<Rightarrow> False)  
19 
Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False  Inr b \<Rightarrow> a \<sqsubseteq> b)" 

20 

21 
instance .. 

22 
end 

23 

40436  24 
lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

25 
unfolding below_sum_def by simp 
29130  26 

40436  27 
lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

28 
unfolding below_sum_def by simp 
29130  29 

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

30 
lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

31 
unfolding below_sum_def by simp 
29130  32 

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

33 
lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

34 
unfolding below_sum_def by simp 
29130  35 

36 
lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y" 

37 
by simp 

38 

39 
lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y" 

40 
by simp 

41 

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

42 
lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 
29130  43 
by (cases x, simp_all) 
44 

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

45 
lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 
29130  46 
by (cases x, simp_all) 
47 

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

48 
lemmas sum_below_elims = Inl_belowE Inr_belowE 
29130  49 

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

50 
lemma sum_below_cases: 
29130  51 
"\<lbrakk>x \<sqsubseteq> y; 
52 
\<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R; 

53 
\<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> 

54 
\<Longrightarrow> R" 

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

55 
by (cases x, safe elim!: sum_below_elims, auto) 
29130  56 

57 
subsection {* Sum type is a complete partial order *} 

58 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37111
diff
changeset

59 
instance sum :: (po, po) po 
29130  60 
proof 
61 
fix x :: "'a + 'b" 

62 
show "x \<sqsubseteq> x" 

63 
by (induct x, simp_all) 

64 
next 

65 
fix x y :: "'a + 'b" 

66 
assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y" 

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

67 
by (induct x, auto elim!: sum_below_elims intro: below_antisym) 
29130  68 
next 
69 
fix x y z :: "'a + 'b" 

70 
assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" 

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

71 
by (induct x, auto elim!: sum_below_elims intro: below_trans) 
29130  72 
qed 
73 

74 
lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)" 

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

75 
by (rule monofunI, erule sum_below_cases, simp_all) 
29130  76 

77 
lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)" 

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

78 
by (rule monofunI, erule sum_below_cases, simp_all) 
29130  79 

80 
lemma sum_chain_cases: 

81 
assumes Y: "chain Y" 

82 
assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R" 

83 
assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R" 

84 
shows "R" 

85 
apply (cases "Y 0") 

86 
apply (rule A) 

87 
apply (rule ch2ch_monofun [OF monofun_inv_Inl Y]) 

88 
apply (rule ext) 

89 
apply (cut_tac j=i in chain_mono [OF Y le0], simp) 

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

90 
apply (erule Inl_belowE, simp) 
29130  91 
apply (rule B) 
92 
apply (rule ch2ch_monofun [OF monofun_inv_Inr Y]) 

93 
apply (rule ext) 

94 
apply (cut_tac j=i in chain_mono [OF Y le0], simp) 

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

95 
apply (erule Inr_belowE, simp) 
29130  96 
done 
97 

98 
lemma is_lub_Inl: "range S << x \<Longrightarrow> range (\<lambda>i. Inl (S i)) << Inl x" 

99 
apply (rule is_lubI) 

100 
apply (rule ub_rangeI) 

40771  101 
apply (simp add: is_lub_rangeD1) 
29130  102 
apply (frule ub_rangeD [where i=arbitrary]) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

103 
apply (erule Inl_belowE, simp) 
40771  104 
apply (erule is_lubD2) 
29130  105 
apply (rule ub_rangeI) 
106 
apply (drule ub_rangeD, simp) 

107 
done 

108 

109 
lemma is_lub_Inr: "range S << x \<Longrightarrow> range (\<lambda>i. Inr (S i)) << Inr x" 

110 
apply (rule is_lubI) 

111 
apply (rule ub_rangeI) 

40771  112 
apply (simp add: is_lub_rangeD1) 
29130  113 
apply (frule ub_rangeD [where i=arbitrary]) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

114 
apply (erule Inr_belowE, simp) 
40771  115 
apply (erule is_lubD2) 
29130  116 
apply (rule ub_rangeI) 
117 
apply (drule ub_rangeD, simp) 

118 
done 

119 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37111
diff
changeset

120 
instance sum :: (cpo, cpo) cpo 
29130  121 
apply intro_classes 
122 
apply (erule sum_chain_cases, safe) 

123 
apply (rule exI) 

124 
apply (rule is_lub_Inl) 

125 
apply (erule cpo_lubI) 

126 
apply (rule exI) 

127 
apply (rule is_lub_Inr) 

128 
apply (erule cpo_lubI) 

129 
done 

130 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
31076
diff
changeset

131 
subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *} 
29130  132 

133 
lemma cont_Inl: "cont Inl" 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

134 
by (intro contI is_lub_Inl cpo_lubI) 
29130  135 

136 
lemma cont_Inr: "cont Inr" 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

137 
by (intro contI is_lub_Inr cpo_lubI) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

138 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
35900
diff
changeset

139 
lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl] 
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
35900
diff
changeset

140 
lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr] 
29130  141 

142 
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl] 

143 
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr] 

144 

145 
lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric] 

146 
lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric] 

147 

148 
lemma cont_sum_case1: 

149 
assumes f: "\<And>a. cont (\<lambda>x. f x a)" 

150 
assumes g: "\<And>b. cont (\<lambda>x. g x b)" 

151 
shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a  Inr b \<Rightarrow> g x b)" 

152 
by (induct y, simp add: f, simp add: g) 

153 

154 
lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)" 

155 
apply (rule contI) 

156 
apply (erule sum_chain_cases) 

157 
apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE) 

158 
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE) 

159 
done 

160 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

161 
lemma cont2cont_sum_case: 
29130  162 
assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)" 
163 
assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)" 

164 
assumes h: "cont (\<lambda>x. h x)" 

165 
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a  Inr b \<Rightarrow> g x b)" 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

166 
apply (rule cont_apply [OF h]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

167 
apply (rule cont_sum_case2 [OF f2 g2]) 
29130  168 
apply (rule cont_sum_case1 [OF f1 g1]) 
169 
done 

170 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
35900
diff
changeset

171 
lemma cont2cont_sum_case' [simp, cont2cont]: 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

172 
assumes f: "cont (\<lambda>p. f (fst p) (snd p))" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

173 
assumes g: "cont (\<lambda>p. g (fst p) (snd p))" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

174 
assumes h: "cont (\<lambda>x. h x)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

175 
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a  Inr b \<Rightarrow> g x b)" 
39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
37678
diff
changeset

176 
using assms by (simp add: cont2cont_sum_case prod_cont_iff) 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29534
diff
changeset

177 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

178 
text {* Continuity of map function. *} 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

179 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

180 
lemma sum_map_eq: "sum_map f g = sum_case (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

181 
by (rule ext, case_tac x, simp_all) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

182 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

183 
lemma cont2cont_sum_map [simp, cont2cont]: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

184 
assumes f: "cont (\<lambda>(x, y). f x y)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

185 
assumes g: "cont (\<lambda>(x, y). g x y)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

186 
assumes h: "cont (\<lambda>x. h x)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

187 
shows "cont (\<lambda>x. sum_map (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

188 
using assms by (simp add: sum_map_eq prod_cont_iff) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

189 

29130  190 
subsection {* Compactness and chainfiniteness *} 
191 

192 
lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)" 

193 
apply (rule compactI2) 

194 
apply (erule sum_chain_cases, safe) 

195 
apply (simp add: lub_Inl) 

196 
apply (erule (2) compactD2) 

197 
apply (simp add: lub_Inr) 

198 
done 

199 

200 
lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)" 

201 
apply (rule compactI2) 

202 
apply (erule sum_chain_cases, safe) 

203 
apply (simp add: lub_Inl) 

204 
apply (simp add: lub_Inr) 

205 
apply (erule (2) compactD2) 

206 
done 

207 

208 
lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a" 

209 
unfolding compact_def 

210 
by (drule adm_subst [OF cont_Inl], simp) 

211 

212 
lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a" 

213 
unfolding compact_def 

214 
by (drule adm_subst [OF cont_Inr], simp) 

215 

216 
lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a" 

217 
by (safe elim!: compact_Inl compact_Inl_rev) 

218 

219 
lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a" 

220 
by (safe elim!: compact_Inr compact_Inr_rev) 

221 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37111
diff
changeset

222 
instance sum :: (chfin, chfin) chfin 
29130  223 
apply intro_classes 
224 
apply (erule compact_imp_max_in_chain) 

225 
apply (case_tac "\<Squnion>i. Y i", simp_all) 

226 
done 

227 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37111
diff
changeset

228 
instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

229 
by intro_classes (simp add: below_sum_def split: sum.split) 
29130  230 

40495  231 
subsection {* Using sum types with fixrec *} 
232 

233 
definition 

234 
"match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a  Inr b \<Rightarrow> Fixrec.fail)" 

235 

236 
definition 

237 
"match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail  Inr b \<Rightarrow> k\<cdot>b)" 

238 

239 
lemma match_Inl_simps [simp]: 

240 
"match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a" 

241 
"match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail" 

242 
unfolding match_Inl_def by simp_all 

243 

244 
lemma match_Inr_simps [simp]: 

245 
"match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail" 

246 
"match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b" 

247 
unfolding match_Inr_def by simp_all 

248 

249 
setup {* 

250 
Fixrec.add_matchers 

251 
[ (@{const_name Inl}, @{const_name match_Inl}), 

252 
(@{const_name Inr}, @{const_name match_Inr}) ] 

253 
*} 

254 

40496  255 
subsection {* Disjoint sum is a predomain *} 
256 

257 
definition 

258 
"encode_sum_u = 

259 
(\<Lambda>(up\<cdot>x). case x of Inl a \<Rightarrow> sinl\<cdot>(up\<cdot>a)  Inr b \<Rightarrow> sinr\<cdot>(up\<cdot>b))" 

260 

261 
definition 

262 
"decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))" 

263 

264 
lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x" 

265 
unfolding decode_sum_u_def encode_sum_u_def 

266 
by (case_tac x, simp, rename_tac y, case_tac y, simp_all) 

267 

268 
lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x" 

269 
unfolding decode_sum_u_def encode_sum_u_def 

270 
apply (case_tac x, simp) 

271 
apply (rename_tac a, case_tac a, simp, simp) 

272 
apply (rename_tac b, case_tac b, simp, simp) 

273 
done 

274 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

275 
text {* A deflation combinator for making unpointed types *} 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

276 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

277 
definition udefl :: "udom defl \<rightarrow> udom u defl" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

278 
where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

279 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

280 
lemma ep_pair_strictify_up: 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

281 
"ep_pair (strictify\<cdot>up) (fup\<cdot>ID)" 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

282 
apply (rule ep_pair.intro) 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

283 
apply (simp add: strictify_conv_if) 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

284 
apply (case_tac y, simp, simp add: strictify_conv_if) 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

285 
done 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

286 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

287 
lemma cast_udefl: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

288 
"cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

289 
unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

290 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

291 
definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

292 
where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>b)))" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

293 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

294 
lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

295 
by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

296 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

297 
(* 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

298 
definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

299 
where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up) 
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

300 
(fup\<cdot>ID oo u_map\<cdot>prj) ssum_map" 
41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

301 
*) 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

302 

40496  303 
instantiation sum :: (predomain, predomain) predomain 
304 
begin 

305 

306 
definition 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

307 
"liftemb = (strictify\<cdot>up oo ssum_emb) oo 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

308 
(ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)" 
40496  309 

310 
definition 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

311 
"liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj)) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

312 
oo (ssum_prj oo fup\<cdot>ID)" 
40496  313 

314 
definition 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

315 
"liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 
40496  316 

317 
instance proof 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

318 
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)" 
40496  319 
unfolding liftemb_sum_def liftprj_sum_def 
41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

320 
by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

321 
ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro) 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
40830
diff
changeset

322 
show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)" 
40496  323 
unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def 
41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

324 
by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

325 
cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom) 
40496  326 
qed 
327 

29130  328 
end 
40496  329 

41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

330 
subsection {* Configuring domain package to work with sum type *} 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

331 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

332 
lemma liftdefl_sum [domain_defl_simps]: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

333 
"LIFTDEFL('a::predomain + 'b::predomain) = 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

334 
sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

335 
by (rule liftdefl_sum_def) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

336 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

337 
abbreviation sum_map' 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

338 
where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

339 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

340 
lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" 
41323  341 
by (simp add: ID_def cfun_eq_iff sum_map.identity) 
41321
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

342 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

343 
lemma deflation_sum_map [domain_deflation]: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

344 
"\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

345 
apply default 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

346 
apply (induct_tac x, simp_all add: deflation.idem) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

347 
apply (induct_tac x, simp_all add: deflation.below) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

348 
done 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

349 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

350 
lemma encode_sum_u_sum_map: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

351 
"encode_sum_u\<cdot>(u_map\<cdot>(sum_map' f g)\<cdot>(decode_sum_u\<cdot>x)) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

352 
= ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

353 
apply (induct x, simp add: decode_sum_u_def encode_sum_u_def) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

354 
apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

355 
apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

356 
done 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

357 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

358 
lemma isodefl_sum [domain_isodefl]: 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

359 
fixes d :: "'a::predomain \<rightarrow> 'a" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

360 
assumes "isodefl' d1 t1" and "isodefl' d2 t2" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

361 
shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)" 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

362 
using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

363 
apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

364 
apply (simp add: cfcomp1 encode_sum_u_sum_map) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

365 
apply (simp add: ssum_map_map u_emb_bottom) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

366 
done 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

367 

4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

368 
setup {* 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

369 
Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true]) 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

370 
*} 
4e72b6fc9dd4
configure domain package to work with HOL sum type
huffman
parents:
41292
diff
changeset

371 

40496  372 
end 