1(*  Title:      HOL/HOLCF/Library/Sum_Cpo.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>The cpo of disjoint sums\<close>
6
7theory Sum_Cpo
8imports HOLCF
9begin
10
11subsection \<open>Ordering on sum type\<close>
12
13instantiation sum :: (below, below) below
14begin
15
16definition below_sum_def:
17  "x \<sqsubseteq> y \<equiv> case x of
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
21instance ..
22end
23
24lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y"
25unfolding below_sum_def by simp
26
27lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y"
28unfolding below_sum_def by simp
29
30lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
31unfolding below_sum_def by simp
32
33lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
34unfolding below_sum_def by simp
35
36lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
37by simp
38
39lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
40by simp
41
42lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
43by (cases x, simp_all)
44
45lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
46by (cases x, simp_all)
47
48lemmas sum_below_elims = Inl_belowE Inr_belowE
49
50lemma sum_below_cases:
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"
55by (cases x, safe elim!: sum_below_elims, auto)
56
57subsection \<open>Sum type is a complete partial order\<close>
58
59instance sum :: (po, po) po
60proof
61  fix x :: "'a + 'b"
62  show "x \<sqsubseteq> x"
63    by (induct x, simp_all)
64next
65  fix x y :: "'a + 'b"
66  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
67    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
68next
69  fix x y z :: "'a + 'b"
70  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
71    by (induct x, auto elim!: sum_below_elims intro: below_trans)
72qed
73
74lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
75by (rule monofunI, erule sum_below_cases, simp_all)
76
77lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
78by (rule monofunI, erule sum_below_cases, simp_all)
79
80lemma 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)
90  apply (erule Inl_belowE, simp)
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)
95 apply (erule Inr_belowE, simp)
96done
97
98lemma 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)
101  apply (simp add: is_lub_rangeD1)
102 apply (frule ub_rangeD [where i=arbitrary])
103 apply (erule Inl_belowE, simp)
104 apply (erule is_lubD2)
105 apply (rule ub_rangeI)
106 apply (drule ub_rangeD, simp)
107done
108
109lemma 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)
112  apply (simp add: is_lub_rangeD1)
113 apply (frule ub_rangeD [where i=arbitrary])
114 apply (erule Inr_belowE, simp)
115 apply (erule is_lubD2)
116 apply (rule ub_rangeI)
117 apply (drule ub_rangeD, simp)
118done
119
120instance sum :: (cpo, cpo) cpo
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)
129done
130
131subsection \<open>Continuity of \emph{Inl}, \emph{Inr}, and case function\<close>
132
133lemma cont_Inl: "cont Inl"
134by (intro contI is_lub_Inl cpo_lubI)
135
136lemma cont_Inr: "cont Inr"
137by (intro contI is_lub_Inr cpo_lubI)
138
139lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
140lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
141
142lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
143lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
144
145lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
146lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
147
148lemma cont_case_sum1:
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)"
152by (induct y, simp add: f, simp add: g)
153
154lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)"
155apply (rule contI)
156apply (erule sum_chain_cases)
157apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
158apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
159done
160
161lemma cont2cont_case_sum:
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)"
166apply (rule cont_apply [OF h])
167apply (rule cont_case_sum2 [OF f2 g2])
168apply (rule cont_case_sum1 [OF f1 g1])
169done
170
171lemma cont2cont_case_sum' [simp, cont2cont]:
172  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
173  assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
174  assumes h: "cont (\<lambda>x. h x)"
175  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
176using assms by (simp add: cont2cont_case_sum prod_cont_iff)
177
178text \<open>Continuity of map function.\<close>
179
180lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
181by (rule ext, case_tac x, simp_all)
182
183lemma cont2cont_map_sum [simp, cont2cont]:
184  assumes f: "cont (\<lambda>(x, y). f x y)"
185  assumes g: "cont (\<lambda>(x, y). g x y)"
186  assumes h: "cont (\<lambda>x. h x)"
187  shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
188using assms by (simp add: map_sum_eq prod_cont_iff)
189
190subsection \<open>Compactness and chain-finiteness\<close>
191
192lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
193apply (rule compactI2)
194apply (erule sum_chain_cases, safe)
195apply (simp add: lub_Inl)
196apply (erule (2) compactD2)
197apply (simp add: lub_Inr)
198done
199
200lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
201apply (rule compactI2)
202apply (erule sum_chain_cases, safe)
203apply (simp add: lub_Inl)
204apply (simp add: lub_Inr)
205apply (erule (2) compactD2)
206done
207
208lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
209unfolding compact_def
210by (drule adm_subst [OF cont_Inl], simp)
211
212lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
213unfolding compact_def
214by (drule adm_subst [OF cont_Inr], simp)
215
216lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
217by (safe elim!: compact_Inl compact_Inl_rev)
218
219lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
220by (safe elim!: compact_Inr compact_Inr_rev)
221
222instance sum :: (chfin, chfin) chfin
223apply intro_classes
224apply (erule compact_imp_max_in_chain)
225apply (case_tac "\<Squnion>i. Y i", simp_all)
226done
227
228instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
229by intro_classes (simp add: below_sum_def split: sum.split)
230
231subsection \<open>Using sum types with fixrec\<close>
232
233definition
234  "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
235
236definition
237  "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)"
238
239lemma 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"
242unfolding match_Inl_def by simp_all
243
244lemma 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"
247unfolding match_Inr_def by simp_all
248
249setup \<open>
250  Fixrec.add_matchers
251    [ (@{const_name Inl}, @{const_name match_Inl}),
252      (@{const_name Inr}, @{const_name match_Inr}) ]
253\<close>
254
255subsection \<open>Disjoint sum is a predomain\<close>
256
257definition
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
261definition
262  "decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))"
263
264lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x"
265unfolding decode_sum_u_def encode_sum_u_def
266by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
267
268lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x"
269unfolding decode_sum_u_def encode_sum_u_def
270apply (case_tac x, simp)
271apply (rename_tac a, case_tac a, simp, simp)
272apply (rename_tac b, case_tac b, simp, simp)
273done
274
275text \<open>A deflation combinator for making unpointed types\<close>
276
277definition udefl :: "udom defl \<rightarrow> udom u defl"
278  where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
279
280lemma ep_pair_strictify_up:
281  "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)"
282apply (rule ep_pair.intro)
283apply (simp add: strictify_conv_if)
284apply (case_tac y, simp, simp add: strictify_conv_if)
285done
286
287lemma cast_udefl:
288  "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
289unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
290
291definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
292  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))"
293
294lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
295by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
296
297(*
298definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
299  where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
300    (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
301*)
302
303instantiation sum :: (predomain, predomain) predomain
304begin
305
306definition
307  "liftemb = (strictify\<cdot>up oo ssum_emb) oo
308    (ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)"
309
310definition
311  "liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj))
312    oo (ssum_prj oo fup\<cdot>ID)"
313
314definition
315  "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
316
317instance proof
318  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
319    unfolding liftemb_sum_def liftprj_sum_def
320    by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep
321      ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro)
322  show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
323    unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
324    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl
325      cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom)
326qed
327
328end
329
330subsection \<open>Configuring domain package to work with sum type\<close>
331
332lemma liftdefl_sum [domain_defl_simps]:
333  "LIFTDEFL('a::predomain + 'b::predomain) =
334    sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
335by (rule liftdefl_sum_def)
336
337abbreviation map_sum'
338  where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))"
339
340lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID"
341by (simp add: ID_def cfun_eq_iff map_sum.identity id_def)
342
343lemma deflation_map_sum [domain_deflation]:
344  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
345apply standard
346apply (induct_tac x, simp_all add: deflation.idem)
347apply (induct_tac x, simp_all add: deflation.below)
348done
349
350lemma encode_sum_u_map_sum:
351  "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
352    = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
353apply (induct x, simp add: decode_sum_u_def encode_sum_u_def)
354apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def)
355apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def)
356done
357
358lemma isodefl_sum [domain_isodefl]:
359  fixes d :: "'a::predomain \<rightarrow> 'a"
360  assumes "isodefl' d1 t1" and "isodefl' d2 t2"
361  shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
362using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
363apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
364apply (simp add: cfcomp1 encode_sum_u_map_sum)
365apply (simp add: ssum_map_map u_emb_bottom)
366done
367
368setup \<open>
369  Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true])
370\<close>
371
372end
373