# HG changeset patch
# User huffman
# Date 1258678038 28800
# Node ID 1d73cce2d630e6b751b4639e0ba8158aaffccd2b
# Parent  46cbbcbd4e6825846292be0f0d3bbaaa0d7bf779
fix definitions of copy combinators

diff -r 46cbbcbd4e68 -r 1d73cce2d630 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 15:41:52 2009 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 16:47:18 2009 -0800
@@ -375,8 +375,8 @@
     "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
        'a foo \<rightarrow> 'a foo"
 where
-  "foo_copy = Abs_CFun (\<lambda>(d1, d2, d3). foo_abs oo
-        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d2))
+  "foo_copy = (\<Lambda> p. foo_abs oo
+        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
           oo foo_rep)"
 
 definition
@@ -384,16 +384,16 @@
     "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
        'a bar \<rightarrow> 'a bar"
 where
-  "bar_copy = Abs_CFun (\<lambda>(d1, d2, d3). bar_abs oo
-        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d3) oo bar_rep)"
+  "bar_copy = (\<Lambda> p. bar_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
 
 definition
   baz_copy ::
     "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
        'a baz \<rightarrow> 'a baz"
 where
-  "baz_copy = Abs_CFun (\<lambda>(d1, d2, d3). baz_abs oo
-        sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep)"
+  "baz_copy = (\<Lambda> p. baz_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
 
 definition
   foo_bar_baz_copy ::
@@ -408,10 +408,9 @@
 apply (subst beta_cfun, simp)+
 apply (subst pair_collapse)+
 apply (rule cfun_arg_cong)
+unfolding foo_bar_baz_mapF_def split_def
 unfolding foo_bar_baz_copy_def
 unfolding foo_copy_def bar_copy_def baz_copy_def
-unfolding foo_bar_baz_mapF_def
-unfolding split_def
 apply (subst beta_cfun, simp)+
 apply (rule refl)
 done