src/HOL/HOLCF/Library/Sum_Cpo.thy
changeset 55931 62156e694f3d
parent 55414 eab03e9cee8a
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Mar 06 12:17:26 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Mar 06 13:36:15 2014 +0100
     1.3 @@ -177,15 +177,15 @@
     1.4  
     1.5  text {* Continuity of map function. *}
     1.6  
     1.7 -lemma sum_map_eq: "sum_map f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
     1.8 +lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
     1.9  by (rule ext, case_tac x, simp_all)
    1.10  
    1.11 -lemma cont2cont_sum_map [simp, cont2cont]:
    1.12 +lemma cont2cont_map_sum [simp, cont2cont]:
    1.13    assumes f: "cont (\<lambda>(x, y). f x y)"
    1.14    assumes g: "cont (\<lambda>(x, y). g x y)"
    1.15    assumes h: "cont (\<lambda>x. h x)"
    1.16 -  shows "cont (\<lambda>x. sum_map (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
    1.17 -using assms by (simp add: sum_map_eq prod_cont_iff)
    1.18 +  shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
    1.19 +using assms by (simp add: map_sum_eq prod_cont_iff)
    1.20  
    1.21  subsection {* Compactness and chain-finiteness *}
    1.22  
    1.23 @@ -334,21 +334,21 @@
    1.24      sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
    1.25  by (rule liftdefl_sum_def)
    1.26  
    1.27 -abbreviation sum_map'
    1.28 -  where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"
    1.29 +abbreviation map_sum'
    1.30 +  where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))"
    1.31  
    1.32 -lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID"
    1.33 -by (simp add: ID_def cfun_eq_iff sum_map.identity id_def)
    1.34 +lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID"
    1.35 +by (simp add: ID_def cfun_eq_iff map_sum.identity id_def)
    1.36  
    1.37 -lemma deflation_sum_map [domain_deflation]:
    1.38 -  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"
    1.39 +lemma deflation_map_sum [domain_deflation]:
    1.40 +  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
    1.41  apply default
    1.42  apply (induct_tac x, simp_all add: deflation.idem)
    1.43  apply (induct_tac x, simp_all add: deflation.below)
    1.44  done
    1.45  
    1.46 -lemma encode_sum_u_sum_map:
    1.47 -  "encode_sum_u\<cdot>(u_map\<cdot>(sum_map' f g)\<cdot>(decode_sum_u\<cdot>x))
    1.48 +lemma encode_sum_u_map_sum:
    1.49 +  "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
    1.50      = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
    1.51  apply (induct x, simp add: decode_sum_u_def encode_sum_u_def)
    1.52  apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def)
    1.53 @@ -358,10 +358,10 @@
    1.54  lemma isodefl_sum [domain_isodefl]:
    1.55    fixes d :: "'a::predomain \<rightarrow> 'a"
    1.56    assumes "isodefl' d1 t1" and "isodefl' d2 t2"
    1.57 -  shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
    1.58 +  shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
    1.59  using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
    1.60  apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
    1.61 -apply (simp add: cfcomp1 encode_sum_u_sum_map)
    1.62 +apply (simp add: cfcomp1 encode_sum_u_map_sum)
    1.63  apply (simp add: ssum_map_map u_emb_bottom)
    1.64  done
    1.65