# HG changeset patch
# User huffman
# Date 1130975855 -3600
# Node ID e2e626b673b3fd7787bf64dd5d1cb16ce760871a
# Parent  43000d7a017cd4c6d9b33d7ee883f177c9f914bc
cleaned up; ch2ch_Rep_CFun is a simp rule

diff -r 43000d7a017c -r e2e626b673b3 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Nov 03 00:43:50 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Nov 03 00:57:35 2005 +0100
@@ -204,7 +204,8 @@
 lemma ch2ch_Rep_CFunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
 by (rule monofun_Rep_CFun1 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFun: "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
+lemma ch2ch_Rep_CFun [simp]:
+  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
 apply (rule chainI)
 apply (rule monofun_cfun)
 apply (erule chainE)
@@ -215,12 +216,7 @@
 
 lemma contlub_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
-apply (simp only: contlub_cfun_fun)
-apply (simp only: contlub_cfun_arg)
-apply (rule diag_lub)
-apply (erule monofun_Rep_CFun1 [THEN ch2ch_monofun])
-apply (erule monofun_Rep_CFun2 [THEN ch2ch_monofun])
-done
+by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
 
 lemma cont_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
@@ -250,7 +246,7 @@
 
 lemma ex_lub_cfun:
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>j. \<Squnion>i. F j\<cdot>(Y i)) = (\<Squnion>i. \<Squnion>j. F j\<cdot>(Y i))"
-by (simp add: diag_lub ch2ch_Rep_CFunL ch2ch_Rep_CFunR)
+by (simp add: diag_lub)
 
 text {* the lub of a chain of cont. functions is continuous *}
 
@@ -417,7 +413,7 @@
 
 syntax  "@oo" :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100)
      
-translations  "f1 oo f2" == "cfcomp$f1$f2"
+translations  "f oo g" == "cfcomp\<cdot>f\<cdot>g"
 
 defs
   ID_def: "ID \<equiv> (\<Lambda> x. x)"
@@ -473,7 +469,7 @@
 apply (rule contlubI)
 apply (case_tac "lub (range Y) = \<bottom>")
 apply (drule (1) chain_UU_I)
-apply (simp add: thelub_const)
+apply simp
 apply (simp del: if_image_distrib)
 apply (simp only: contlub_cfun_arg)
 apply (rule lub_equal2)
@@ -508,6 +504,6 @@
 
 translations
   "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
-  "Let x = a in e" == "CLet$a$(LAM x. e)"
+  "Let x = a in e" == "CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
 
 end