# HG changeset patch
# User huffman
# Date 1199981201 -3600
# Node ID a69e665b7df8ef4974d27adcc8d398fabbc5139b
# Parent  e60b59e7da3f6d7d643e791832493a2a950d39f1
declare ch2ch_LAM [simp]

diff -r e60b59e7da3f -r a69e665b7df8 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Jan 10 08:21:03 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Jan 10 17:06:41 2008 +0100
@@ -225,14 +225,10 @@
 
 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)
-apply (erule chainE)
-done
+by (simp add: chain_def monofun_cfun)
 
-lemma ch2ch_LAM: "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk>
-    \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
+lemma ch2ch_LAM [simp]:
+  "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
 by (simp add: chain_def expand_cfun_less)
 
 text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
@@ -251,7 +247,7 @@
 lemma contlub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_CFun ch2ch_LAM)
+apply (simp add: thelub_CFun)
 apply (simp add: Abs_CFun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done