add map_map lemmas
authorhuffman
Mon Nov 09 15:51:32 2009 -0800 (2009-11-09)
changeset 3358754f98d225163
parent 33586 0e745228d605
child 33588 ea9becc59636
add map_map lemmas
src/HOLCF/Bifinite.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Mon Nov 09 15:29:58 2009 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Mon Nov 09 15:51:32 2009 -0800
     1.3 @@ -114,6 +114,11 @@
     1.4  lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
     1.5  unfolding cprod_map_def by simp
     1.6  
     1.7 +lemma cprod_map_map:
     1.8 +  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
     1.9 +    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.10 +by (induct p) simp
    1.11 +
    1.12  lemma ep_pair_cprod_map:
    1.13    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.14    shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    1.15 @@ -202,6 +207,11 @@
    1.16  lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    1.17  unfolding cfun_map_def by simp
    1.18  
    1.19 +lemma cfun_map_map:
    1.20 +  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.21 +    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.22 +by (rule ext_cfun) simp
    1.23 +
    1.24  lemma ep_pair_cfun_map:
    1.25    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.26    shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
     2.1 --- a/src/HOLCF/Sprod.thy	Mon Nov 09 15:29:58 2009 -0800
     2.2 +++ b/src/HOLCF/Sprod.thy	Mon Nov 09 15:51:32 2009 -0800
     2.3 @@ -245,6 +245,16 @@
     2.4    "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
     2.5  by (simp add: sprod_map_def)
     2.6  
     2.7 +lemma sprod_map_map:
     2.8 +  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     2.9 +    sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    2.10 +     sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    2.11 +apply (induct p, simp)
    2.12 +apply (case_tac "f2\<cdot>x = \<bottom>", simp)
    2.13 +apply (case_tac "g2\<cdot>y = \<bottom>", simp)
    2.14 +apply simp
    2.15 +done
    2.16 +
    2.17  lemma ep_pair_sprod_map:
    2.18    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    2.19    shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
     3.1 --- a/src/HOLCF/Ssum.thy	Mon Nov 09 15:29:58 2009 -0800
     3.2 +++ b/src/HOLCF/Ssum.thy	Mon Nov 09 15:51:32 2009 -0800
     3.3 @@ -226,6 +226,15 @@
     3.4  lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
     3.5  unfolding ssum_map_def by simp
     3.6  
     3.7 +lemma ssum_map_map:
     3.8 +  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     3.9 +    ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
    3.10 +     ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    3.11 +apply (induct p, simp)
    3.12 +apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
    3.13 +apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
    3.14 +done
    3.15 +
    3.16  lemma ep_pair_ssum_map:
    3.17    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    3.18    shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
     4.1 --- a/src/HOLCF/Up.thy	Mon Nov 09 15:29:58 2009 -0800
     4.2 +++ b/src/HOLCF/Up.thy	Mon Nov 09 15:51:32 2009 -0800
     4.3 @@ -303,6 +303,9 @@
     4.4  lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
     4.5  unfolding u_map_def by simp
     4.6  
     4.7 +lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
     4.8 +by (induct p) simp_all
     4.9 +
    4.10  lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
    4.11  apply default
    4.12  apply (case_tac x, simp, simp add: ep_pair.e_inverse)