add fixrec support for HOL pair constructor patterns

--- a/src/HOLCF/Fixrec.thy	Mon Nov 02 17:29:34 2009 -0800
+++ b/src/HOLCF/Fixrec.thy	Mon Nov 02 18:39:41 2009 -0800
@@ -526,7 +526,8 @@
 
 lemma match_cpair_simps [simp]:
   "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
-by (simp add: match_cpair_def)
+  "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
+by (simp_all add: match_cpair_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"
@@ -610,6 +611,7 @@
       (@{const_name sinr}, @{const_name match_sinr}),
       (@{const_name spair}, @{const_name match_spair}),
       (@{const_name cpair}, @{const_name match_cpair}),
+      (@{const_name Pair}, @{const_name match_cpair}),
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),

--- a/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 17:29:34 2009 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 18:39:41 2009 -0800
@@ -36,20 +36,9 @@
 
 infixr 6 ->>; val (op ->>) = cfunT;
 
-fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
-
 fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
-  | binder_cfun _   =  [];
-
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
-  | body_cfun T   =  T;
-
-fun strip_cfun T : typ list * typ =
-  (binder_cfun T, body_cfun T);
-
 fun maybeT T = Type(@{type_name "maybe"}, [T]);
 
 fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
@@ -59,9 +48,27 @@
   | tupleT [T] = T
   | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
 
+local
+
+fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+  | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
+  | binder_cfun _   =  [];
+
+fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
+  | body_cfun T   =  T;
+
+fun strip_cfun T : typ list * typ =
+  (binder_cfun T, body_cfun T);
+
+fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
+
+in
+
 fun matchT (T, U) =
   body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
 
+end
 
 (*************************************************************************)
 (***************************** building terms ****************************)
@@ -235,10 +242,16 @@
   | Const(@{const_name Rep_CFun},_)$f$x =>
       let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
       in pre_build match_name f rhs' (v::vs) taken' end
+  | f$(v as Free(n,T)) =>
+      pre_build match_name f rhs (v::vs) taken
+  | f$x =>
+      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
+      in pre_build match_name f rhs' (v::vs) taken' end
   | Const(c,T) =>
       let
         val n = Name.variant taken "v";
         fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+          | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
         val m = Const(match_name c, matchT (T, fastype_of rhs));

--- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 17:29:34 2009 -0800
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 18:39:41 2009 -0800
@@ -31,6 +31,11 @@
 fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
 where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
 
+text {* Fixrec also works with the HOL pair constructor. *}
+
+fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
+where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
+
 
 subsection {* Examples using @{text fixpat} *}