|
(* Title: HOL/HOLCF/Library/List_Predomain.thy
Author: Brian Huffman
*)
section \<open>Predomain class instance for HOL list type\<close>
theory List_Predomain
imports List_Cpo Sum_Cpo
begin
subsection \<open>Strict list type\<close>
domain 'a slist = SNil | SCons "'a" "'a slist"
text \<open>Polymorphic map function for strict lists.\<close>
text \<open>FIXME: The domain package should generate this!\<close>
fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
where "slist_map'\f\SNil = SNil"
| "\x \ \; xs \ \\ \
slist_map'\f\(SCons\x\xs) = SCons\(f\x)\(slist_map'\f\xs)"
lemma slist_map'_strict [simp]: "slist_map'\<cdot>f\<cdot>\<bottom> = \<bottom>"
by fixrec_simp
lemma slist_map_conv [simp]: "slist_map = slist_map'"
apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs)
apply (induct_tac xs, simp_all)
apply (subst slist_map_unfold, simp)
apply (subst slist_map_unfold, simp add: SNil_def)
apply (subst slist_map_unfold, simp add: SCons_def)
done
lemma slist_map'_slist_map':
"f\\ = \ \ slist_map'\f\(slist_map'\g\xs) = slist_map'\(\ x. f\(g\x))\xs"
apply (induct xs, simp, simp)
apply (case_tac "g\a = \", simp, simp)
apply (case_tac "slist_map'\g\xs = \", simp, simp)
done
lemma slist_map'_oo:
"f\\ = \ \ slist_map'\(f oo g) = slist_map'\f oo slist_map'\g"
by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun)
lemma slist_map'_ID: "slist_map'\<cdot>ID = ID"
by (rule cfun_eqI, induct_tac x, simp_all)
lemma ep_pair_slist_map':
"ep_pair e p \ ep_pair (slist_map'\e) (slist_map'\p)"
apply (rule ep_pair.intro)
apply (subst slist_map'_slist_map')
apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def])
apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID)
apply (subst slist_map'_slist_map')
apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def])
apply (rule below_eq_trans [OF _ ID1])
apply (subst slist_map'_ID [symmetric])
apply (intro monofun_cfun below_refl)
apply (simp add: cfun_below_iff ep_pair.e_p_below)
done
text \<open>
Types \<^typ>\<open>'a list u\<close>. and \<^typ>\<open>'a u slist\<close> are isomorphic.
\<close>
fixrec encode_list_u where
"encode_list_u\(up\[]) = SNil" |
"encode_list_u\(up\(x # xs)) = SCons\(up\x)\(encode_list_u\(up\xs))"
lemma encode_list_u_strict [simp]: "encode_list_u\\ = \"
by fixrec_simp
lemma encode_list_u_bottom_iff [simp]:
"encode_list_u\x = \ \ x = \"
apply (induct x, simp_all)
apply (rename_tac xs, induct_tac xs, simp_all)
done
fixrec decode_list_u where
"decode_list_u\SNil = up\[]" |
"ys \ \ \ decode_list_u\(SCons\(up\x)\ys) =
(case decode_list_u\<cdot>ys of up\<cdot>xs \<Rightarrow> up\<cdot>(x # xs))"
lemma decode_list_u_strict [simp]: "decode_list_u\\ = \"
by fixrec_simp
lemma decode_encode_list_u [simp]: "decode_list_u\(encode_list_u\x) = x"
by (induct x, simp, rename_tac xs, induct_tac xs, simp_all)
lemma encode_decode_list_u [simp]: "encode_list_u\(decode_list_u\y) = y"
apply (induct y, simp, simp)
apply (case_tac a, simp)
apply (case_tac "decode_list_u\y", simp, simp)
done
subsection \<open>Lists are a predomain\<close>
definition list_liftdefl :: "udom u defl \ udom u defl"
where "list_liftdefl = (\ a. udefl\(slist_defl\(u_liftdefl\a)))"
lemma cast_slist_defl: "cast\(slist_defl\a) = emb oo slist_map\(cast\a) oo prj"
using isodefl_slist [where fa="cast\a" and da="a"]
unfolding isodefl_def by simp
instantiation list :: (predomain) predomain
begin
definition
"liftemb = (strictify\up oo emb oo slist_map'\u_emb) oo slist_map'\liftemb oo encode_list_u"
definition
"liftprj = (decode_list_u oo slist_map'\liftprj) oo (slist_map'\u_prj oo prj) oo fup\ID"
definition
"liftdefl (t::('a list) itself) = list_liftdefl\LIFTDEFL('a)"
instance proof
show "ep_pair liftemb (liftprj :: udom u \ ('a list) u)"
unfolding liftemb_list_def liftprj_list_def
by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up
ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
show "cast\LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \ ('a list) u)"
unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl)
apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
done
qed
end
subsection \<open>Configuring domain package to work with list type\<close>
lemma liftdefl_list [domain_defl_simps]:
"LIFTDEFL('a::predomain list) = list_liftdefl\LIFTDEFL('a)"
by (rule liftdefl_list_def)
abbreviation list_map :: "('a::cpo \ 'b::cpo) \ 'a list \ 'b list"
where "list_map f \ Abs_cfun (map (Rep_cfun f))"
lemma list_map_ID [domain_map_ID]: "list_map ID = ID"
by (simp add: ID_def)
lemma deflation_list_map [domain_deflation]:
"deflation d \ deflation (list_map d)"
apply standard
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done
lemma encode_list_u_map:
"encode_list_u\(u_map\(list_map f)\(decode_list_u\xs))
= slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
apply (induct xs, simp, simp)
apply (case_tac a, simp, rename_tac b)
apply (case_tac "decode_list_u\xs")
apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp)
done
lemma isodefl_list_u [domain_isodefl]:
fixes d :: "'a::predomain \ 'a"
assumes "isodefl' d t"
shows "isodefl' (list_map d) (list_liftdefl\t)"
using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
apply (simp add: cfcomp1 encode_list_u_map)
apply (simp add: slist_map'_slist_map' u_emb_bottom)
done
setup \<open>
Domain_Take_Proofs.add_rec_type (\<^type_name>\<open>list\<close>, [true])
\<close>
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
