1(*  Title:      HOL/HOLCF/Library/List_Predomain.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Predomain class instance for HOL list type\<close>
6
7theory List_Predomain
8imports List_Cpo Sum_Cpo
9begin
10
11subsection \<open>Strict list type\<close>
12
13domain 'a slist = SNil | SCons "'a" "'a slist"
14
15text \<open>Polymorphic map function for strict lists.\<close>
16
17text \<open>FIXME: The domain package should generate this!\<close>
18
19fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
20  where "slist_map'\<cdot>f\<cdot>SNil = SNil"
21  | "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow>
22      slist_map'\<cdot>f\<cdot>(SCons\<cdot>x\<cdot>xs) = SCons\<cdot>(f\<cdot>x)\<cdot>(slist_map'\<cdot>f\<cdot>xs)"
23
24lemma slist_map'_strict [simp]: "slist_map'\<cdot>f\<cdot>\<bottom> = \<bottom>"
25by fixrec_simp
26
27lemma slist_map_conv [simp]: "slist_map = slist_map'"
28apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs)
29apply (induct_tac xs, simp_all)
30apply (subst slist_map_unfold, simp)
31apply (subst slist_map_unfold, simp add: SNil_def)
32apply (subst slist_map_unfold, simp add: SCons_def)
33done
34
35lemma slist_map'_slist_map':
36  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>f\<cdot>(slist_map'\<cdot>g\<cdot>xs) = slist_map'\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
37apply (induct xs, simp, simp)
38apply (case_tac "g\<cdot>a = \<bottom>", simp, simp)
39apply (case_tac "slist_map'\<cdot>g\<cdot>xs = \<bottom>", simp, simp)
40done
41
42lemma slist_map'_oo:
43  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>(f oo g) = slist_map'\<cdot>f oo slist_map'\<cdot>g"
44by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun)
45
46lemma slist_map'_ID: "slist_map'\<cdot>ID = ID"
47by (rule cfun_eqI, induct_tac x, simp_all)
48
49lemma ep_pair_slist_map':
50  "ep_pair e p \<Longrightarrow> ep_pair (slist_map'\<cdot>e) (slist_map'\<cdot>p)"
51apply (rule ep_pair.intro)
52apply (subst slist_map'_slist_map')
53apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def])
54apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID)
55apply (subst slist_map'_slist_map')
56apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def])
57apply (rule below_eq_trans [OF _ ID1])
58apply (subst slist_map'_ID [symmetric])
59apply (intro monofun_cfun below_refl)
60apply (simp add: cfun_below_iff ep_pair.e_p_below)
61done
62
63text \<open>
64  Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
65\<close>
66
67fixrec encode_list_u where
68  "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
69  "encode_list_u\<cdot>(up\<cdot>(x # xs)) = SCons\<cdot>(up\<cdot>x)\<cdot>(encode_list_u\<cdot>(up\<cdot>xs))"
70
71lemma encode_list_u_strict [simp]: "encode_list_u\<cdot>\<bottom> = \<bottom>"
72by fixrec_simp
73
74lemma encode_list_u_bottom_iff [simp]:
75  "encode_list_u\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
76apply (induct x, simp_all)
77apply (rename_tac xs, induct_tac xs, simp_all)
78done
79
80fixrec decode_list_u where
81  "decode_list_u\<cdot>SNil = up\<cdot>[]" |
82  "ys \<noteq> \<bottom> \<Longrightarrow> decode_list_u\<cdot>(SCons\<cdot>(up\<cdot>x)\<cdot>ys) =
83    (case decode_list_u\<cdot>ys of up\<cdot>xs \<Rightarrow> up\<cdot>(x # xs))"
84
85lemma decode_list_u_strict [simp]: "decode_list_u\<cdot>\<bottom> = \<bottom>"
86by fixrec_simp
87
88lemma decode_encode_list_u [simp]: "decode_list_u\<cdot>(encode_list_u\<cdot>x) = x"
89by (induct x, simp, rename_tac xs, induct_tac xs, simp_all)
90
91lemma encode_decode_list_u [simp]: "encode_list_u\<cdot>(decode_list_u\<cdot>y) = y"
92apply (induct y, simp, simp)
93apply (case_tac a, simp)
94apply (case_tac "decode_list_u\<cdot>y", simp, simp)
95done
96
97subsection \<open>Lists are a predomain\<close>
98
99definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
100  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
101
102lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
103using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
104unfolding isodefl_def by simp
105
106instantiation list :: (predomain) predomain
107begin
108
109definition
110  "liftemb = (strictify\<cdot>up oo emb oo slist_map'\<cdot>u_emb) oo slist_map'\<cdot>liftemb oo encode_list_u"
111
112definition
113  "liftprj = (decode_list_u oo slist_map'\<cdot>liftprj) oo (slist_map'\<cdot>u_prj oo prj) oo fup\<cdot>ID"
114
115definition
116  "liftdefl (t::('a list) itself) = list_liftdefl\<cdot>LIFTDEFL('a)"
117
118instance proof
119  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a list) u)"
120    unfolding liftemb_list_def liftprj_list_def
121    by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up
122      ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
123  show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
124    unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
125    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl)
126    apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
127    done
128qed
129
130end
131
132subsection \<open>Configuring domain package to work with list type\<close>
133
134lemma liftdefl_list [domain_defl_simps]:
135  "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
136by (rule liftdefl_list_def)
137
138abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list"
139  where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"
140
141lemma list_map_ID [domain_map_ID]: "list_map ID = ID"
142by (simp add: ID_def)
143
144lemma deflation_list_map [domain_deflation]:
145  "deflation d \<Longrightarrow> deflation (list_map d)"
146apply standard
147apply (induct_tac x, simp_all add: deflation.idem)
148apply (induct_tac x, simp_all add: deflation.below)
149done
150
151lemma encode_list_u_map:
152  "encode_list_u\<cdot>(u_map\<cdot>(list_map f)\<cdot>(decode_list_u\<cdot>xs))
153    = slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
154apply (induct xs, simp, simp)
155apply (case_tac a, simp, rename_tac b)
156apply (case_tac "decode_list_u\<cdot>xs")
157apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp)
158done
159
160lemma isodefl_list_u [domain_isodefl]:
161  fixes d :: "'a::predomain \<rightarrow> 'a"
162  assumes "isodefl' d t"
163  shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
164using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
165apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
166apply (simp add: cfcomp1 encode_list_u_map)
167apply (simp add: slist_map'_slist_map' u_emb_bottom)
168done
169
170setup \<open>
171  Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
172\<close>
173
174end
175