rename constant u_defl to u_liftdefl;
authorhuffman
Thu Jan 06 17:40:38 2011 -0800 (2011-01-06)
changeset 414375bc117c382ec
parent 41436 480978f80eae
child 41438 272fe1f37b65
rename constant u_defl to u_liftdefl;
add new constant u_defl :: udom defl -> udom defl
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Library/List_Predomain.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/ex/Domain_Proofs.thy
     1.1 --- a/src/HOL/HOLCF/Domain.thy	Thu Jan 06 16:52:35 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Domain.thy	Thu Jan 06 17:40:38 2011 -0800
     1.3 @@ -274,9 +274,16 @@
     1.4  done
     1.5  
     1.6  lemma isodefl_u:
     1.7 -  "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
     1.8 +  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
     1.9  apply (rule isodeflI)
    1.10 -apply (simp add: cast_u_defl isodefl'_def)
    1.11 +apply (simp add: cast_u_defl cast_isodefl)
    1.12 +apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq u_map_map)
    1.13 +done
    1.14 +
    1.15 +lemma isodefl_u_liftdefl:
    1.16 +  "isodefl' d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_liftdefl\<cdot>t)"
    1.17 +apply (rule isodeflI)
    1.18 +apply (simp add: cast_u_liftdefl isodefl'_def)
    1.19  apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
    1.20  done
    1.21  
    1.22 @@ -319,7 +326,7 @@
    1.23  
    1.24  lemmas [domain_defl_simps] =
    1.25    DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
    1.26 -  liftdefl_eq LIFTDEFL_prod
    1.27 +  liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of
    1.28  
    1.29  lemmas [domain_map_ID] =
    1.30    cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID
    1.31 @@ -327,6 +334,7 @@
    1.32  lemmas [domain_isodefl] =
    1.33    isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
    1.34    isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of
    1.35 +  isodefl_u_liftdefl
    1.36  
    1.37  lemmas [domain_deflation] =
    1.38    deflation_cfun_map deflation_sfun_map deflation_ssum_map
     2.1 --- a/src/HOL/HOLCF/Library/List_Predomain.thy	Thu Jan 06 16:52:35 2011 -0800
     2.2 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Thu Jan 06 17:40:38 2011 -0800
     2.3 @@ -97,7 +97,7 @@
     2.4  subsection {* Lists are a predomain *}
     2.5  
     2.6  definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
     2.7 -  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_defl\<cdot>a)))"
     2.8 +  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
     2.9  
    2.10  lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
    2.11  using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
    2.12 @@ -122,7 +122,7 @@
    2.13        ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
    2.14    show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
    2.15      unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
    2.16 -    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl cast_liftdefl)
    2.17 +    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl)
    2.18      apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
    2.19      done
    2.20  qed
    2.21 @@ -162,7 +162,7 @@
    2.22    assumes "isodefl' d t"
    2.23    shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
    2.24  using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
    2.25 -apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
    2.26 +apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
    2.27  apply (simp add: cfcomp1 encode_list_u_map)
    2.28  apply (simp add: slist_map'_slist_map' u_emb_bottom)
    2.29  done
     3.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Jan 06 16:52:35 2011 -0800
     3.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Jan 06 17:40:38 2011 -0800
     3.3 @@ -289,7 +289,7 @@
     3.4  unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
     3.5  
     3.6  definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
     3.7 -  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>b)))"
     3.8 +  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))"
     3.9  
    3.10  lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
    3.11  by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
    3.12 @@ -321,7 +321,7 @@
    3.13        ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro)
    3.14    show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
    3.15      unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
    3.16 -    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl
    3.17 +    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl
    3.18        cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom)
    3.19  qed
    3.20  
    3.21 @@ -360,7 +360,7 @@
    3.22    assumes "isodefl' d1 t1" and "isodefl' d2 t2"
    3.23    shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
    3.24  using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
    3.25 -apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_defl)
    3.26 +apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
    3.27  apply (simp add: cfcomp1 encode_sum_u_sum_map)
    3.28  apply (simp add: ssum_map_map u_emb_bottom)
    3.29  done
     4.1 --- a/src/HOL/HOLCF/Representable.thy	Thu Jan 06 16:52:35 2011 -0800
     4.2 +++ b/src/HOL/HOLCF/Representable.thy	Thu Jan 06 17:40:38 2011 -0800
     4.3 @@ -163,8 +163,8 @@
     4.4  
     4.5  subsection {* Type combinators *}
     4.6  
     4.7 -definition u_defl :: "udom u defl \<rightarrow> udom defl"
     4.8 -  where "u_defl = defl_fun1 u_emb u_prj ID"
     4.9 +definition u_defl :: "udom defl \<rightarrow> udom defl"
    4.10 +  where "u_defl = defl_fun1 u_emb u_prj u_map"
    4.11  
    4.12  definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    4.13    where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
    4.14 @@ -179,8 +179,9 @@
    4.15    where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
    4.16  
    4.17  lemma cast_u_defl:
    4.18 -  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
    4.19 -unfolding u_defl_def by (simp add: cast_defl_fun1 ep_pair_u)
    4.20 +  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
    4.21 +using ep_pair_u finite_deflation_u_map
    4.22 +unfolding u_defl_def by (rule cast_defl_fun1)
    4.23  
    4.24  lemma cast_prod_defl:
    4.25    "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
    4.26 @@ -206,6 +207,20 @@
    4.27  using ep_pair_sfun finite_deflation_sfun_map
    4.28  unfolding sfun_defl_def by (rule cast_defl_fun2)
    4.29  
    4.30 +text {* Special deflation combinator for unpointed types. *}
    4.31 +
    4.32 +definition u_liftdefl :: "udom u defl \<rightarrow> udom defl"
    4.33 +  where "u_liftdefl = defl_fun1 u_emb u_prj ID"
    4.34 +
    4.35 +lemma cast_u_liftdefl:
    4.36 +  "cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
    4.37 +unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)
    4.38 +
    4.39 +lemma u_liftdefl_liftdefl_of:
    4.40 +  "u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A"
    4.41 +by (rule cast_eq_imp_eq)
    4.42 +   (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
    4.43 +
    4.44  subsection {* Class instance proofs *}
    4.45  
    4.46  subsubsection {* Universal domain *}
    4.47 @@ -262,7 +277,7 @@
    4.48    "prj = liftprj oo u_prj"
    4.49  
    4.50  definition
    4.51 -  "defl (t::'a u itself) = u_defl\<cdot>LIFTDEFL('a)"
    4.52 +  "defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)"
    4.53  
    4.54  definition
    4.55    "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
    4.56 @@ -279,12 +294,12 @@
    4.57      by (intro ep_pair_comp ep_pair_u predomain_ep)
    4.58    show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
    4.59      unfolding emb_u_def prj_u_def defl_u_def
    4.60 -    by (simp add: cast_u_defl cast_liftdefl assoc_oo)
    4.61 +    by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo)
    4.62  qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
    4.63  
    4.64  end
    4.65  
    4.66 -lemma DEFL_u: "DEFL('a::predomain u) = u_defl\<cdot>LIFTDEFL('a)"
    4.67 +lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
    4.68  by (rule defl_u_def)
    4.69  
    4.70  subsubsection {* Strict function space *}
     5.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 16:52:35 2011 -0800
     5.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Thu Jan 06 17:40:38 2011 -0800
     5.3 @@ -30,15 +30,15 @@
     5.4      "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
     5.5  where
     5.6    "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     5.7 -    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t2)))
     5.8 -    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t3))\<cdot>DEFL(tr)))
     5.9 -    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
    5.10 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
    5.11 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
    5.12 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
    5.13  
    5.14  lemma foo_bar_baz_deflF_beta:
    5.15    "foo_bar_baz_deflF\<cdot>a\<cdot>t =
    5.16 -    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(fst (snd t)))))
    5.17 -    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
    5.18 -    , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
    5.19 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
    5.20 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
    5.21 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
    5.22  unfolding foo_bar_baz_deflF_def
    5.23  by (simp add: split_def)
    5.24  
    5.25 @@ -62,13 +62,13 @@
    5.26  text {* Unfold rules for each combinator. *}
    5.27  
    5.28  lemma foo_defl_unfold:
    5.29 -  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(bar_defl\<cdot>a))))"
    5.30 +  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
    5.31  unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    5.32  
    5.33 -lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
    5.34 +lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
    5.35  unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    5.36  
    5.37 -lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
    5.38 +lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
    5.39  unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    5.40  
    5.41  text "The automation for the previous steps will be quite similar to