# HG changeset patch
# User huffman
# Date 1292812730 28800
# Node ID 01b2de947cff28b62c4ea60c3bab6d0b11408590
# Parent  6aaf80ea9715ab938518999aaca913809ae439d7
rename function cprod_map to prod_map

diff -r 6aaf80ea9715 -r 01b2de947cff NEWS
--- a/NEWS	Sun Dec 19 18:15:21 2010 -0800
+++ b/NEWS	Sun Dec 19 18:38:50 2010 -0800
@@ -275,7 +275,7 @@
     mem_iff ~> member_def
     null_empty ~> null_def
 
-INCOMPATIBILITY.  Note that these were not suppossed to be used
+INCOMPATIBILITY.  Note that these were not supposed to be used
 regularly unless for striking reasons; their main purpose was code
 generation.
 
@@ -501,6 +501,8 @@
 
 * The type class 'finite_po' has been removed. INCOMPATIBILITY.
 
+* The function 'cprod_map' has been renamed to 'prod_map'.
+
 * Renamed some theorems (the original names are also still available).
   expand_fun_below   ~> fun_below_iff
   below_fun_ext      ~> fun_belowI
diff -r 6aaf80ea9715 -r 01b2de947cff src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 18:15:21 2010 -0800
+++ b/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 18:38:50 2010 -0800
@@ -96,11 +96,11 @@
   using assms unfolding approx_chain_def
   by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
 
-lemma approx_chain_cprod_map:
+lemma approx_chain_prod_map:
   assumes "approx_chain a" and "approx_chain b"
-  shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
+  shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
   using assms unfolding approx_chain_def
-  by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
+  by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
 
 text {* Approx chains for countable discrete types. *}
 
@@ -228,7 +228,7 @@
 proof
   show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
     using bifinite [where 'a='a] and bifinite [where 'a='b]
-    by (fast intro!: approx_chain_cprod_map)
+    by (fast intro!: approx_chain_prod_map)
 qed
 
 instance sfun :: (bifinite, bifinite) bifinite
diff -r 6aaf80ea9715 -r 01b2de947cff src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Sun Dec 19 18:15:21 2010 -0800
+++ b/src/HOL/HOLCF/Domain.thy	Sun Dec 19 18:38:50 2010 -0800
@@ -264,13 +264,13 @@
 apply (simp add: sprod_map_map isodefl_strict)
 done
 
-lemma isodefl_cprod:
+lemma isodefl_prod:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
+    isodefl (prod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
 apply (simp add: cast_prod_defl cast_isodefl)
 apply (simp add: emb_prod_def prj_prod_def)
-apply (simp add: cprod_map_map cfcomp1)
+apply (simp add: prod_map_map cfcomp1)
 done
 
 lemma isodefl_u:
@@ -281,16 +281,16 @@
 done
 
 lemma encode_prod_u_map:
-  "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
+  "encode_prod_u\<cdot>(u_map\<cdot>(prod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
     = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
 unfolding encode_prod_u_def decode_prod_u_def
 apply (case_tac x, simp, rename_tac a b)
 apply (case_tac a, simp, case_tac b, simp, simp)
 done
 
-lemma isodefl_cprod_u:
+lemma isodefl_prod_u:
   assumes "isodefl' d1 t1" and "isodefl' d2 t2"
-  shows "isodefl' (cprod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
+  shows "isodefl' (prod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
 using assms unfolding isodefl'_def
 unfolding liftemb_prod_def liftprj_prod_def
 by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map)
@@ -322,15 +322,15 @@
   liftdefl_eq LIFTDEFL_prod
 
 lemmas [domain_map_ID] =
-  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID
 
 lemmas [domain_isodefl] =
   isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
-  isodefl_cfun isodefl_cprod isodefl_cprod_u isodefl'_pdefl
+  isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_pdefl
 
 lemmas [domain_deflation] =
   deflation_cfun_map deflation_sfun_map deflation_ssum_map
-  deflation_sprod_map deflation_cprod_map deflation_u_map
+  deflation_sprod_map deflation_prod_map deflation_u_map
 
 setup {*
   fold Domain_Take_Proofs.add_rec_type
diff -r 6aaf80ea9715 -r 01b2de947cff src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 18:15:21 2010 -0800
+++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 18:38:50 2010 -0800
@@ -118,57 +118,57 @@
 subsection {* Map operator for product type *}
 
 definition
-  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+  prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
 where
-  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+  "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
 
-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 prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
+unfolding prod_map_def by simp
 
-lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
+lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID"
 unfolding cfun_eq_iff 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"
+lemma prod_map_map:
+  "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+    prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
 by (induct p) simp
 
-lemma ep_pair_cprod_map:
+lemma ep_pair_prod_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
-  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
+  shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)"
 proof
   interpret e1p1: ep_pair e1 p1 by fact
   interpret e2p2: ep_pair e2 p2 by fact
-  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+  fix x show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
     by (induct x) simp
-  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+  fix y show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
     by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
 qed
 
-lemma deflation_cprod_map:
+lemma deflation_prod_map:
   assumes "deflation d1" and "deflation d2"
-  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
+  shows "deflation (prod_map\<cdot>d1\<cdot>d2)"
 proof
   interpret d1: deflation d1 by fact
   interpret d2: deflation d2 by fact
   fix x
-  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+  show "prod_map\<cdot>d1\<cdot>d2\<cdot>(prod_map\<cdot>d1\<cdot>d2\<cdot>x) = prod_map\<cdot>d1\<cdot>d2\<cdot>x"
     by (induct x) (simp add: d1.idem d2.idem)
-  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+  show "prod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
     by (induct x) (simp add: d1.below d2.below)
 qed
 
-lemma finite_deflation_cprod_map:
+lemma finite_deflation_prod_map:
   assumes "finite_deflation d1" and "finite_deflation d2"
-  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
+  shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)"
 proof (rule finite_deflation_intro)
   interpret d1: finite_deflation d1 by fact
   interpret d2: finite_deflation d2 by fact
   have "deflation d1" and "deflation d2" by fact+
-  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
-  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
+  thus "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
+  have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
     by clarsimp
-  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
+  thus "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
diff -r 6aaf80ea9715 -r 01b2de947cff src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 18:15:21 2010 -0800
+++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 18:38:50 2010 -0800
@@ -129,8 +129,8 @@
 definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
 definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
 
-definition "prod_emb = udom_emb (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-definition "prod_prj = udom_prj (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
 
 definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
 definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
@@ -147,7 +147,7 @@
 
 lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
   unfolding prod_emb_def prod_prj_def
-  by (simp add: ep_pair_udom approx_chain_cprod_map)
+  by (simp add: ep_pair_udom approx_chain_prod_map)
 
 lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
   unfolding sprod_emb_def sprod_prj_def
@@ -167,7 +167,7 @@
   where "u_defl = defl_fun1 u_emb u_prj ID"
 
 definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
-  where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
+  where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
 
 definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
@@ -184,8 +184,8 @@
 
 lemma cast_prod_defl:
   "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
-    prod_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
-using ep_pair_prod finite_deflation_cprod_map
+    prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
+using ep_pair_prod finite_deflation_prod_map
 unfolding prod_defl_def by (rule cast_defl_fun2)
 
 lemma cast_sprod_defl:
@@ -450,10 +450,10 @@
 begin
 
 definition
-  "emb = prod_emb oo cprod_map\<cdot>emb\<cdot>emb"
+  "emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb"
 
 definition
-  "prj = cprod_map\<cdot>prj\<cdot>prj oo prod_prj"
+  "prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj"
 
 definition
   "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
@@ -461,10 +461,10 @@
 instance proof
   show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
     unfolding emb_prod_def prj_prod_def
-    by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
+    by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj)
   show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
     unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map)
   show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
     unfolding emb_prod_def liftemb_prod_def liftemb_eq
     unfolding encode_prod_u_def decode_prod_u_def