src/HOL/HOLCF/Bifinite.thy

   assumes "approx_chain a" and "approx_chain b"
   shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
   using assms unfolding approx_chain_def
   by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
 
-lemma approx_chain_cprod_map:
-  assumes "approx_chain a" and "approx_chain b"
-  shows "approx_chain (\<lambda>i. cprod_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)
+lemma approx_chain_prod_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
 
 text {* Approx chains for countable discrete types. *}
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"

 
 instance prod :: (bifinite, bifinite) bifinite
 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
 proof
   show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"