# HG changeset patch
# User huffman
# Date 1258695877 28800
# Node ID 31169fdc5ae749e2863132a4c7ea3a250b0bf676
# Parent  ce8d2e8bca21b8bd4a01e46d3fedbdb0b9718f41
add map_ID lemmas

diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/Bifinite.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -114,6 +114,9 @@
 lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
 unfolding cprod_map_def by simp
 
+lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by auto
+
 lemma cprod_map_map:
   "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
     cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
@@ -207,6 +210,9 @@
 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
 unfolding cfun_map_def by simp
 
+lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
+unfolding expand_cfun_eq by simp
+
 lemma cfun_map_map:
   "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
     cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/ConvexPD.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -495,6 +495,9 @@
 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
+lemma convex_map_ID: "convex_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def convex_map_ident)
+
 lemma convex_map_map:
   "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: convex_pd_induct, simp_all)
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/LowerPD.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -471,6 +471,9 @@
 lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
 by (induct xs rule: lower_pd_induct, simp_all)
 
+lemma lower_map_ID: "lower_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def lower_map_ident)
+
 lemma lower_map_map:
   "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: lower_pd_induct, simp_all)
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/Sprod.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -245,6 +245,9 @@
   "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
 by (simp add: sprod_map_def)
 
+lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
+unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
+
 lemma sprod_map_map:
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/Ssum.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -226,6 +226,9 @@
 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
 unfolding ssum_map_def by simp
 
+lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
+unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+
 lemma ssum_map_map:
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/Up.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -303,6 +303,9 @@
 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
 unfolding u_map_def by simp
 
+lemma u_map_ID: "u_map\<cdot>ID = ID"
+unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
+
 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"
 by (induct p) simp_all
 
diff -r ce8d2e8bca21 -r 31169fdc5ae7 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/UpperPD.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -466,6 +466,9 @@
 lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
 by (induct xs rule: upper_pd_induct, simp_all)
 
+lemma upper_map_ID: "upper_map\<cdot>ID = ID"
+by (simp add: expand_cfun_eq ID_def upper_map_ident)
+
 lemma upper_map_map:
   "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: upper_pd_induct, simp_all)