# HG changeset patch
# User huffman
# Date 1117830103 -7200
# Node ID b3268fe39838bdf701b1843d1a3510dec1c64cc1
# Parent  61811f31ce5a77185e6d3edca65c8874c21e94d7
added theorem ch2ch_lub

diff -r 61811f31ce5a -r b3268fe39838 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Jun 03 22:07:30 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Fri Jun 03 22:21:43 2005 +0200
@@ -125,6 +125,16 @@
 apply assumption
 done
 
+lemma ch2ch_lub:
+  fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo"
+  assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
+  assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
+  shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
+apply (rule chainI)
+apply (rule lub_mono [rule_format, OF 2 2])
+apply (rule chainE [OF 1])
+done
+
 lemma diag_lub:
   fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo"
   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
@@ -138,21 +148,18 @@
     apply (rule chainE [OF 2])
     done
   have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
-    apply (rule chainI)
-    apply (rule lub_mono [OF 2 2, rule_format])
-    apply (rule chainE [OF 1])
-    done
+    by (rule ch2ch_lub [OF 1 2])
   show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
     apply (rule is_lub_thelub [OF 4])
     apply (rule ub_rangeI)
-    apply (rule lub_mono3 [OF 2 3, rule_format])
+    apply (rule lub_mono3 [rule_format, OF 2 3])
     apply (rule exI)
     apply (rule trans_less)
     apply (rule chain_mono3 [OF 1 le_maxI1])
     apply (rule chain_mono3 [OF 2 le_maxI2])
     done
   show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
-    apply (rule lub_mono [OF 3 4, rule_format])
+    apply (rule lub_mono [rule_format, OF 3 4])
     apply (rule is_ub_thelub [OF 2])
     done
 qed