# HG changeset patch
# User huffman
# Date 1201739479 -3600
# Node ID 9b5b4bd44f7adb764abe38faf3119ced9b7aa1b3
# Parent  31115576b8586eb223bb147a5bd5005a63d346ee
new lemma is_lub_Pair; cleaned up some proofs

diff -r 31115576b858 -r 9b5b4bd44f7a src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Jan 30 17:36:03 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 31 01:31:19 2008 +0100
@@ -93,27 +93,31 @@
 
 subsection {* Product type is a cpo *}
 
+lemma is_lub_Pair:
+  "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
+apply (rule is_lubI [OF ub_rangeI])
+apply (simp add: less_cprod_def is_ub_lub)
+apply (frule ub2ub_monofun [OF monofun_fst])
+apply (drule ub2ub_monofun [OF monofun_snd])
+apply (simp add: less_cprod_def is_lub_lub)
+done
+
 lemma lub_cprod:
   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   assumes S: "chain S"
   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
-apply (rule monofun_pair)
-apply (rule is_ub_thelub)
-apply (rule ch2ch_monofun [OF monofun_fst S])
-apply (rule is_ub_thelub)
-apply (rule ch2ch_monofun [OF monofun_snd S])
-apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
-apply (rule monofun_pair)
-apply (rule is_lub_thelub)
-apply (rule ch2ch_monofun [OF monofun_fst S])
-apply (erule monofun_fst [THEN ub2ub_monofun])
-apply (rule is_lub_thelub)
-apply (rule ch2ch_monofun [OF monofun_snd S])
-apply (erule monofun_snd [THEN ub2ub_monofun])
-done
+proof -
+  have "chain (\<lambda>i. fst (S i))"
+    using monofun_fst S by (rule ch2ch_monofun)
+  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
+    by (rule thelubE [OF _ refl])
+  have "chain (\<lambda>i. snd (S i))"
+    using monofun_snd S by (rule ch2ch_monofun)
+  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
+    by (rule thelubE [OF _ refl])
+  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
+    using is_lub_Pair [OF 1 2] by simp
+qed
 
 lemma thelub_cprod:
   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
@@ -145,30 +149,18 @@
 
 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
 
-lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
-apply (rule contlubI)
-apply (subst thelub_cprod)
-apply (erule monofun_pair1 [THEN ch2ch_monofun])
-apply simp
-done
-
-lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
-apply (rule contlubI)
-apply (subst thelub_cprod)
-apply (erule monofun_pair2 [THEN ch2ch_monofun])
-apply simp
-done
-
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
-apply (rule monocontlub2cont)
-apply (rule monofun_pair1)
-apply (rule contlub_pair1)
+apply (rule contI)
+apply (rule is_lub_Pair)
+apply (erule thelubE [OF _ refl])
+apply (rule lub_const)
 done
 
 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
-apply (rule monocontlub2cont)
-apply (rule monofun_pair2)
-apply (rule contlub_pair2)
+apply (rule contI)
+apply (rule is_lub_Pair)
+apply (rule lub_const)
+apply (erule thelubE [OF _ refl])
 done
 
 lemma contlub_fst: "contlub fst"