# HG changeset patch
# User huffman
# Date 1119654241 -7200
# Node ID 6fc73c9dd5f470cd8d76f0fdfe8b3271085c4d96
# Parent  a92f96951355768148afd997e94937aa5255144d
cleaned up proof of contlub_abstraction

diff -r a92f96951355 -r 6fc73c9dd5f4 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri Jun 24 17:25:10 2005 +0200
+++ b/src/HOLCF/Cont.thy	Sat Jun 25 01:04:01 2005 +0200
@@ -245,16 +245,12 @@
   never used here
 *}
 
-lemma contlub_abstraction: 
-"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==> 
-  (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
-apply (rule trans)
-prefer 2 apply (rule cont2contlub [THEN contlubE])
-prefer 2 apply (assumption)
+lemma contlub_abstraction:
+  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
+    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
+apply (rule thelub_fun [symmetric])
+apply (rule cont2mono [THEN ch2ch_monofun])
 apply (erule cont2cont_CF1L_rev)
-apply (rule ext)
-apply (rule cont2contlub [THEN contlubE, symmetric])
-apply (erule spec)
 apply assumption
 done