# HG changeset patch # User huffman # Date 1292862407 28800 # Node ID 4e72b6fc9dd4fc7e524771af6aa124d460f0d2c6 # Parent 4953e21ac76c7cb5e36f2bbcbf0d4ba30ff2e8ca configure domain package to work with HOL sum type diff -r 4953e21ac76c -r 4e72b6fc9dd4 src/HOL/HOLCF/Library/List_Predomain.thy --- a/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 07:50:47 2010 -0800 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 08:26:47 2010 -0800 @@ -96,13 +96,6 @@ subsection {* Lists are a predomain *} -definition udefl :: "udom defl \ udom u defl" - where "udefl = defl_fun1 (strictify\up) (fup\ID) ID" - -lemma cast_udefl: - "cast\(udefl\t) = strictify\up oo cast\t oo fup\ID" -unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) - definition list_liftdefl :: "udom u defl \ udom u defl" where "list_liftdefl = (\ a. udefl\(slist_defl\(u_defl\a)))" @@ -110,9 +103,6 @@ using isodefl_slist [where fa="cast\a" and da="a"] unfolding isodefl_def by simp -lemma u_emb_bottom: "u_emb\\ = \" -by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) - instantiation list :: (predomain) predomain begin @@ -139,12 +129,12 @@ end +subsection {* Configuring domain package to work with list type *} + lemma liftdefl_list [domain_defl_simps]: "LIFTDEFL('a::predomain list) = list_liftdefl\LIFTDEFL('a)" by (rule liftdefl_list_def) -subsection {* Configuring list type to work with domain package *} - abbreviation list_map :: "('a::cpo \ 'b::cpo) \ 'a list \ 'b list" where "list_map f \ Abs_cfun (map (Rep_cfun f))" diff -r 4953e21ac76c -r 4e72b6fc9dd4 src/HOL/HOLCF/Library/Sum_Cpo.thy --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Mon Dec 20 07:50:47 2010 -0800 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Mon Dec 20 08:26:47 2010 -0800 @@ -175,6 +175,18 @@ shows "cont (\x. case h x of Inl a \ f x a | Inr b \ g x b)" using assms by (simp add: cont2cont_sum_case prod_cont_iff) +text {* Continuity of map function. *} + +lemma sum_map_eq: "sum_map f g = sum_case (\a. Inl (f a)) (\b. Inr (g b))" +by (rule ext, case_tac x, simp_all) + +lemma cont2cont_sum_map [simp, cont2cont]: + assumes f: "cont (\(x, y). f x y)" + assumes g: "cont (\(x, y). g x y)" + assumes h: "cont (\x. h x)" + shows "cont (\x. sum_map (\y. f x y) (\y. g x y) (h x))" +using assms by (simp add: sum_map_eq prod_cont_iff) + subsection {* Compactness and chain-finiteness *} lemma compact_Inl: "compact a \ compact (Inl a)" @@ -260,6 +272,11 @@ apply (rename_tac b, case_tac b, simp, simp) done +text {* A deflation combinator for making unpointed types *} + +definition udefl :: "udom defl \ udom u defl" + where "udefl = defl_fun1 (strictify\up) (fup\ID) ID" + lemma ep_pair_strictify_up: "ep_pair (strictify\up) (fup\ID)" apply (rule ep_pair.intro) @@ -267,20 +284,32 @@ apply (case_tac y, simp, simp add: strictify_conv_if) done +lemma cast_udefl: + "cast\(udefl\t) = strictify\up oo cast\t oo fup\ID" +unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up) + +definition sum_liftdefl :: "udom u defl \ udom u defl \ udom u defl" + where "sum_liftdefl = (\ a b. udefl\(ssum_defl\(u_defl\a)\(u_defl\b)))" + +lemma u_emb_bottom: "u_emb\\ = \" +by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u]) + +(* definition sum_liftdefl :: "udom u defl \ udom u defl \ udom u defl" where "sum_liftdefl = defl_fun2 (u_map\emb oo strictify\up) (fup\ID oo u_map\prj) ssum_map" +*) instantiation sum :: (predomain, predomain) predomain begin definition - "liftemb = (u_map\emb oo strictify\up) oo - (ssum_map\liftemb\liftemb oo encode_sum_u)" + "liftemb = (strictify\up oo ssum_emb) oo + (ssum_map\(u_emb oo liftemb)\(u_emb oo liftemb) oo encode_sum_u)" definition - "liftprj = (decode_sum_u oo ssum_map\liftprj\liftprj) oo - (fup\ID oo u_map\prj)" + "liftprj = (decode_sum_u oo ssum_map\(liftprj oo u_prj)\(liftprj oo u_prj)) + oo (ssum_prj oo fup\ID)" definition "liftdefl (t::('a + 'b) itself) = sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" @@ -288,17 +317,56 @@ instance proof show "ep_pair liftemb (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def - by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u_map ep_pair_emb_prj - ep_pair_strictify_up predomain_ep, simp add: ep_pair.intro) + by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep + ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro) show "cast\LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \ ('a + 'b) u)" unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def - apply (subst sum_liftdefl_def, subst cast_defl_fun2) - apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj - ep_pair_strictify_up) - apply (erule (1) finite_deflation_ssum_map) - by (simp add: cast_liftdefl cfcomp1 ssum_map_map) + by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl + cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom) qed end +subsection {* Configuring domain package to work with sum type *} + +lemma liftdefl_sum [domain_defl_simps]: + "LIFTDEFL('a::predomain + 'b::predomain) = + sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" +by (rule liftdefl_sum_def) + +abbreviation sum_map' + where "sum_map' f g \ Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" + +lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" +by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2 sum_map.identity) + +lemma deflation_sum_map [domain_deflation]: + "\deflation d1; deflation d2\ \ deflation (sum_map' d1 d2)" +apply default +apply (induct_tac x, simp_all add: deflation.idem) +apply (induct_tac x, simp_all add: deflation.below) +done + +lemma encode_sum_u_sum_map: + "encode_sum_u\(u_map\(sum_map' f g)\(decode_sum_u\x)) + = ssum_map\(u_map\f)\(u_map\g)\x" +apply (induct x, simp add: decode_sum_u_def encode_sum_u_def) +apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def) +apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def) +done + +lemma isodefl_sum [domain_isodefl]: + fixes d :: "'a::predomain \ 'a" + assumes "isodefl' d1 t1" and "isodefl' d2 t2" + shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\t1\t2)" +using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def +apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl) +apply (simp add: cfcomp1 encode_sum_u_sum_map) +apply (simp add: ssum_map_map u_emb_bottom) +done + +setup {* + Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true]) +*} + end