add map_ID lemmas
authorhuffman
Thu Nov 19 21:44:37 2009 -0800 (2009-11-19)
changeset 3380831169fdc5ae7
parent 33807 ce8d2e8bca21
child 33809 033831fd9ef3
add map_ID lemmas
src/HOLCF/Bifinite.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Thu Nov 19 21:06:22 2009 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Thu Nov 19 21:44:37 2009 -0800
     1.3 @@ -114,6 +114,9 @@
     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_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
     1.8 +unfolding expand_cfun_eq by auto
     1.9 +
    1.10  lemma cprod_map_map:
    1.11    "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.12      cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.13 @@ -207,6 +210,9 @@
    1.14  lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    1.15  unfolding cfun_map_def by simp
    1.16  
    1.17 +lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
    1.18 +unfolding expand_cfun_eq by simp
    1.19 +
    1.20  lemma cfun_map_map:
    1.21    "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.22      cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
     2.1 --- a/src/HOLCF/ConvexPD.thy	Thu Nov 19 21:06:22 2009 -0800
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Nov 19 21:44:37 2009 -0800
     2.3 @@ -495,6 +495,9 @@
     2.4  lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
     2.5  by (induct xs rule: convex_pd_induct, simp_all)
     2.6  
     2.7 +lemma convex_map_ID: "convex_map\<cdot>ID = ID"
     2.8 +by (simp add: expand_cfun_eq ID_def convex_map_ident)
     2.9 +
    2.10  lemma convex_map_map:
    2.11    "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
    2.12  by (induct xs rule: convex_pd_induct, simp_all)
     3.1 --- a/src/HOLCF/LowerPD.thy	Thu Nov 19 21:06:22 2009 -0800
     3.2 +++ b/src/HOLCF/LowerPD.thy	Thu Nov 19 21:44:37 2009 -0800
     3.3 @@ -471,6 +471,9 @@
     3.4  lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
     3.5  by (induct xs rule: lower_pd_induct, simp_all)
     3.6  
     3.7 +lemma lower_map_ID: "lower_map\<cdot>ID = ID"
     3.8 +by (simp add: expand_cfun_eq ID_def lower_map_ident)
     3.9 +
    3.10  lemma lower_map_map:
    3.11    "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
    3.12  by (induct xs rule: lower_pd_induct, simp_all)
     4.1 --- a/src/HOLCF/Sprod.thy	Thu Nov 19 21:06:22 2009 -0800
     4.2 +++ b/src/HOLCF/Sprod.thy	Thu Nov 19 21:44:37 2009 -0800
     4.3 @@ -245,6 +245,9 @@
     4.4    "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
     4.5  by (simp add: sprod_map_def)
     4.6  
     4.7 +lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
     4.8 +unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
     4.9 +
    4.10  lemma sprod_map_map:
    4.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    4.12      sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
     5.1 --- a/src/HOLCF/Ssum.thy	Thu Nov 19 21:06:22 2009 -0800
     5.2 +++ b/src/HOLCF/Ssum.thy	Thu Nov 19 21:44:37 2009 -0800
     5.3 @@ -226,6 +226,9 @@
     5.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)"
     5.5  unfolding ssum_map_def by simp
     5.6  
     5.7 +lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
     5.8 +unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
     5.9 +
    5.10  lemma ssum_map_map:
    5.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    5.12      ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
     6.1 --- a/src/HOLCF/Up.thy	Thu Nov 19 21:06:22 2009 -0800
     6.2 +++ b/src/HOLCF/Up.thy	Thu Nov 19 21:44:37 2009 -0800
     6.3 @@ -303,6 +303,9 @@
     6.4  lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
     6.5  unfolding u_map_def by simp
     6.6  
     6.7 +lemma u_map_ID: "u_map\<cdot>ID = ID"
     6.8 +unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
     6.9 +
    6.10  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"
    6.11  by (induct p) simp_all
    6.12  
     7.1 --- a/src/HOLCF/UpperPD.thy	Thu Nov 19 21:06:22 2009 -0800
     7.2 +++ b/src/HOLCF/UpperPD.thy	Thu Nov 19 21:44:37 2009 -0800
     7.3 @@ -466,6 +466,9 @@
     7.4  lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
     7.5  by (induct xs rule: upper_pd_induct, simp_all)
     7.6  
     7.7 +lemma upper_map_ID: "upper_map\<cdot>ID = ID"
     7.8 +by (simp add: expand_cfun_eq ID_def upper_map_ident)
     7.9 +
    7.10  lemma upper_map_map:
    7.11    "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
    7.12  by (induct xs rule: upper_pd_induct, simp_all)