rename function cprod_map to prod_map
authorhuffman
Sun Dec 19 18:38:50 2010 -0800 (2010-12-19)
changeset 4129701b2de947cff
parent 41296 6aaf80ea9715
child 41299 fc8419fd4735
child 41300 528f5d00b542
rename function cprod_map to prod_map
NEWS
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Map_Functions.thy
src/HOL/HOLCF/Representable.thy
     1.1 --- a/NEWS	Sun Dec 19 18:15:21 2010 -0800
     1.2 +++ b/NEWS	Sun Dec 19 18:38:50 2010 -0800
     1.3 @@ -275,7 +275,7 @@
     1.4      mem_iff ~> member_def
     1.5      null_empty ~> null_def
     1.6  
     1.7 -INCOMPATIBILITY.  Note that these were not suppossed to be used
     1.8 +INCOMPATIBILITY.  Note that these were not supposed to be used
     1.9  regularly unless for striking reasons; their main purpose was code
    1.10  generation.
    1.11  
    1.12 @@ -501,6 +501,8 @@
    1.13  
    1.14  * The type class 'finite_po' has been removed. INCOMPATIBILITY.
    1.15  
    1.16 +* The function 'cprod_map' has been renamed to 'prod_map'.
    1.17 +
    1.18  * Renamed some theorems (the original names are also still available).
    1.19    expand_fun_below   ~> fun_below_iff
    1.20    below_fun_ext      ~> fun_belowI
     2.1 --- a/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 18:15:21 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 18:38:50 2010 -0800
     2.3 @@ -96,11 +96,11 @@
     2.4    using assms unfolding approx_chain_def
     2.5    by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
     2.6  
     2.7 -lemma approx_chain_cprod_map:
     2.8 +lemma approx_chain_prod_map:
     2.9    assumes "approx_chain a" and "approx_chain b"
    2.10 -  shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
    2.11 +  shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
    2.12    using assms unfolding approx_chain_def
    2.13 -  by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
    2.14 +  by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
    2.15  
    2.16  text {* Approx chains for countable discrete types. *}
    2.17  
    2.18 @@ -228,7 +228,7 @@
    2.19  proof
    2.20    show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
    2.21      using bifinite [where 'a='a] and bifinite [where 'a='b]
    2.22 -    by (fast intro!: approx_chain_cprod_map)
    2.23 +    by (fast intro!: approx_chain_prod_map)
    2.24  qed
    2.25  
    2.26  instance sfun :: (bifinite, bifinite) bifinite
     3.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Dec 19 18:15:21 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Dec 19 18:38:50 2010 -0800
     3.3 @@ -264,13 +264,13 @@
     3.4  apply (simp add: sprod_map_map isodefl_strict)
     3.5  done
     3.6  
     3.7 -lemma isodefl_cprod:
     3.8 +lemma isodefl_prod:
     3.9    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
    3.10 -    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
    3.11 +    isodefl (prod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
    3.12  apply (rule isodeflI)
    3.13  apply (simp add: cast_prod_defl cast_isodefl)
    3.14  apply (simp add: emb_prod_def prj_prod_def)
    3.15 -apply (simp add: cprod_map_map cfcomp1)
    3.16 +apply (simp add: prod_map_map cfcomp1)
    3.17  done
    3.18  
    3.19  lemma isodefl_u:
    3.20 @@ -281,16 +281,16 @@
    3.21  done
    3.22  
    3.23  lemma encode_prod_u_map:
    3.24 -  "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
    3.25 +  "encode_prod_u\<cdot>(u_map\<cdot>(prod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
    3.26      = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
    3.27  unfolding encode_prod_u_def decode_prod_u_def
    3.28  apply (case_tac x, simp, rename_tac a b)
    3.29  apply (case_tac a, simp, case_tac b, simp, simp)
    3.30  done
    3.31  
    3.32 -lemma isodefl_cprod_u:
    3.33 +lemma isodefl_prod_u:
    3.34    assumes "isodefl' d1 t1" and "isodefl' d2 t2"
    3.35 -  shows "isodefl' (cprod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
    3.36 +  shows "isodefl' (prod_map\<cdot>d1\<cdot>d2) (prod_liftdefl\<cdot>t1\<cdot>t2)"
    3.37  using assms unfolding isodefl'_def
    3.38  unfolding liftemb_prod_def liftprj_prod_def
    3.39  by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map)
    3.40 @@ -322,15 +322,15 @@
    3.41    liftdefl_eq LIFTDEFL_prod
    3.42  
    3.43  lemmas [domain_map_ID] =
    3.44 -  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
    3.45 +  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID
    3.46  
    3.47  lemmas [domain_isodefl] =
    3.48    isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
    3.49 -  isodefl_cfun isodefl_cprod isodefl_cprod_u isodefl'_pdefl
    3.50 +  isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_pdefl
    3.51  
    3.52  lemmas [domain_deflation] =
    3.53    deflation_cfun_map deflation_sfun_map deflation_ssum_map
    3.54 -  deflation_sprod_map deflation_cprod_map deflation_u_map
    3.55 +  deflation_sprod_map deflation_prod_map deflation_u_map
    3.56  
    3.57  setup {*
    3.58    fold Domain_Take_Proofs.add_rec_type
     4.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 18:15:21 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 18:38:50 2010 -0800
     4.3 @@ -118,57 +118,57 @@
     4.4  subsection {* Map operator for product type *}
     4.5  
     4.6  definition
     4.7 -  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
     4.8 +  prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
     4.9  where
    4.10 -  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    4.11 +  "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    4.12  
    4.13 -lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    4.14 -unfolding cprod_map_def by simp
    4.15 +lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    4.16 +unfolding prod_map_def by simp
    4.17  
    4.18 -lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    4.19 +lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID"
    4.20  unfolding cfun_eq_iff by auto
    4.21  
    4.22 -lemma cprod_map_map:
    4.23 -  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    4.24 -    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    4.25 +lemma prod_map_map:
    4.26 +  "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    4.27 +    prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    4.28  by (induct p) simp
    4.29  
    4.30 -lemma ep_pair_cprod_map:
    4.31 +lemma ep_pair_prod_map:
    4.32    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    4.33 -  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    4.34 +  shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)"
    4.35  proof
    4.36    interpret e1p1: ep_pair e1 p1 by fact
    4.37    interpret e2p2: ep_pair e2 p2 by fact
    4.38 -  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    4.39 +  fix x show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    4.40      by (induct x) simp
    4.41 -  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    4.42 +  fix y show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    4.43      by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    4.44  qed
    4.45  
    4.46 -lemma deflation_cprod_map:
    4.47 +lemma deflation_prod_map:
    4.48    assumes "deflation d1" and "deflation d2"
    4.49 -  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    4.50 +  shows "deflation (prod_map\<cdot>d1\<cdot>d2)"
    4.51  proof
    4.52    interpret d1: deflation d1 by fact
    4.53    interpret d2: deflation d2 by fact
    4.54    fix x
    4.55 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    4.56 +  show "prod_map\<cdot>d1\<cdot>d2\<cdot>(prod_map\<cdot>d1\<cdot>d2\<cdot>x) = prod_map\<cdot>d1\<cdot>d2\<cdot>x"
    4.57      by (induct x) (simp add: d1.idem d2.idem)
    4.58 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    4.59 +  show "prod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    4.60      by (induct x) (simp add: d1.below d2.below)
    4.61  qed
    4.62  
    4.63 -lemma finite_deflation_cprod_map:
    4.64 +lemma finite_deflation_prod_map:
    4.65    assumes "finite_deflation d1" and "finite_deflation d2"
    4.66 -  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    4.67 +  shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)"
    4.68  proof (rule finite_deflation_intro)
    4.69    interpret d1: finite_deflation d1 by fact
    4.70    interpret d2: finite_deflation d2 by fact
    4.71    have "deflation d1" and "deflation d2" by fact+
    4.72 -  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    4.73 -  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    4.74 +  thus "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
    4.75 +  have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    4.76      by clarsimp
    4.77 -  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    4.78 +  thus "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    4.79      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    4.80  qed
    4.81  
     5.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 18:15:21 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 18:38:50 2010 -0800
     5.3 @@ -129,8 +129,8 @@
     5.4  definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
     5.5  definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
     5.6  
     5.7 -definition "prod_emb = udom_emb (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
     5.8 -definition "prod_prj = udom_prj (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
     5.9 +definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.10 +definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.11  
    5.12  definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.13  definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.14 @@ -147,7 +147,7 @@
    5.15  
    5.16  lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
    5.17    unfolding prod_emb_def prod_prj_def
    5.18 -  by (simp add: ep_pair_udom approx_chain_cprod_map)
    5.19 +  by (simp add: ep_pair_udom approx_chain_prod_map)
    5.20  
    5.21  lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
    5.22    unfolding sprod_emb_def sprod_prj_def
    5.23 @@ -167,7 +167,7 @@
    5.24    where "u_defl = defl_fun1 u_emb u_prj ID"
    5.25  
    5.26  definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    5.27 -  where "prod_defl = defl_fun2 prod_emb prod_prj cprod_map"
    5.28 +  where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
    5.29  
    5.30  definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    5.31    where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
    5.32 @@ -184,8 +184,8 @@
    5.33  
    5.34  lemma cast_prod_defl:
    5.35    "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
    5.36 -    prod_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
    5.37 -using ep_pair_prod finite_deflation_cprod_map
    5.38 +    prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
    5.39 +using ep_pair_prod finite_deflation_prod_map
    5.40  unfolding prod_defl_def by (rule cast_defl_fun2)
    5.41  
    5.42  lemma cast_sprod_defl:
    5.43 @@ -450,10 +450,10 @@
    5.44  begin
    5.45  
    5.46  definition
    5.47 -  "emb = prod_emb oo cprod_map\<cdot>emb\<cdot>emb"
    5.48 +  "emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb"
    5.49  
    5.50  definition
    5.51 -  "prj = cprod_map\<cdot>prj\<cdot>prj oo prod_prj"
    5.52 +  "prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj"
    5.53  
    5.54  definition
    5.55    "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
    5.56 @@ -461,10 +461,10 @@
    5.57  instance proof
    5.58    show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
    5.59      unfolding emb_prod_def prj_prod_def
    5.60 -    by (intro ep_pair_comp ep_pair_prod ep_pair_cprod_map ep_pair_emb_prj)
    5.61 +    by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj)
    5.62    show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
    5.63      unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
    5.64 -    by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
    5.65 +    by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map)
    5.66    show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
    5.67      unfolding emb_prod_def liftemb_prod_def liftemb_eq
    5.68      unfolding encode_prod_u_def decode_prod_u_def