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