# HG changeset patch
# User huffman
# Date 1257216593 28800
# Node ID d9a25a87da4a226c1531daa79857bc5f220a8543
# Parent  fc43fa403a695c785731dc994a5278a568be6ee7# Parent  daa526c9e5d20ef6e63e684cb042982d27c16c38
merge

diff -r daa526c9e5d2 -r d9a25a87da4a src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Nov 02 23:06:06 2009 +0100
+++ b/src/HOLCF/Cprod.thy	Mon Nov 02 18:49:53 2009 -0800
@@ -52,6 +52,7 @@
 
 translations
   "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
+  "\<Lambda>(CONST Pair x y). t" => "CONST csplit\<cdot>(\<Lambda> x y. t)"
 
 
 subsection {* Convert all lemmas to the continuous versions *}
@@ -150,6 +151,9 @@
 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
 by (simp add: csplit_def cpair_cfst_csnd)
 
+lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
+by (simp add: csplit_def cfst_def csnd_def)
+
 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
 
 subsection {* Product type is a bifinite domain *}
diff -r daa526c9e5d2 -r d9a25a87da4a src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Mon Nov 02 23:06:06 2009 +0100
+++ b/src/HOLCF/Domain.thy	Mon Nov 02 18:49:53 2009 -0800
@@ -222,7 +222,7 @@
 definition
   cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
 where
-  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. <f\<cdot>x, g\<cdot>y>))"
+  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
 
 definition
   u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
diff -r daa526c9e5d2 -r d9a25a87da4a src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Nov 02 23:06:06 2009 +0100
+++ b/src/HOLCF/Fixrec.thy	Mon Nov 02 18:49:53 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}),
diff -r daa526c9e5d2 -r d9a25a87da4a src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 23:06:06 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 18:49:53 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));
diff -r daa526c9e5d2 -r d9a25a87da4a src/HOLCF/ex/Fixrec_ex.thy
--- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 23:06:06 2009 +0100
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 18:49:53 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} *}