--- 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
--- 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
--- 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
--- 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
--- 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