src/HOLCF/Fixrec.thy

   match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
 where
   "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
 
 definition
-  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
-where
-  "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
+  match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+where
+  "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
 
 definition
   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
 where
   "match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)"

 lemma match_UU_simps [simp]:
   "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
   "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
 by (simp_all add: match_UU_def)
 
-lemma match_cpair_simps [simp]:
-  "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
-by (simp_all add: match_cpair_def)
+lemma match_Pair_simps [simp]:
+  "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
+by (simp_all add: match_Pair_def)
 
 lemma match_spair_simps [simp]:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
   "match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_spair_def)

   Fixrec.add_matchers
     [ (@{const_name up}, @{const_name match_up}),
       (@{const_name sinl}, @{const_name match_sinl}),
       (@{const_name sinr}, @{const_name match_sinr}),
       (@{const_name spair}, @{const_name match_spair}),
-      (@{const_name Pair}, @{const_name match_cpair}),
+      (@{const_name Pair}, @{const_name match_Pair}),
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),
       (@{const_name UU}, @{const_name match_UU}) ]
 *}