# HG changeset patch
# User huffman
# Date 1201812494 -3600
# Node ID 87cb69d275589a4763beb5882cf4d7f2a08a944c
# Parent  f9647c040b58102329d57c1790d3dc66c095a424
add lemma cpo_lubI

diff -r f9647c040b58 -r 87cb69d27558 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Thu Jan 31 21:37:20 2008 +0100
+++ b/src/HOLCF/Cont.thy	Thu Jan 31 21:48:14 2008 +0100
@@ -165,7 +165,7 @@
 apply (erule ch2ch_monofun [OF mono])
 apply (rule ub2ub_monofun [OF mono])
 apply (rule is_lubD1)
-apply (erule thelubE, rule refl)
+apply (erule cpo_lubI)
 done
 
 subsection {* Continuity of basic functions *}
@@ -174,8 +174,7 @@
 
 lemma cont_id: "cont (\<lambda>x. x)"
 apply (rule contI)
-apply (erule thelubE)
-apply (rule refl)
+apply (erule cpo_lubI)
 done
 
 text {* constant functions are continuous *}
diff -r f9647c040b58 -r 87cb69d27558 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jan 31 21:37:20 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 31 21:48:14 2008 +0100
@@ -111,11 +111,11 @@
   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])
+    by (rule cpo_lubI)
   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])
+    by (rule cpo_lubI)
   show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
     using is_lub_Pair [OF 1 2] by simp
 qed
@@ -161,7 +161,7 @@
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
 apply (rule contI)
 apply (rule is_lub_Pair)
-apply (erule thelubE [OF _ refl])
+apply (erule cpo_lubI)
 apply (rule lub_const)
 done
 
@@ -169,7 +169,7 @@
 apply (rule contI)
 apply (rule is_lub_Pair)
 apply (rule lub_const)
-apply (erule thelubE [OF _ refl])
+apply (erule cpo_lubI)
 done
 
 lemma contlub_fst: "contlub fst"
diff -r f9647c040b58 -r 87cb69d27558 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:37:20 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:48:14 2008 +0100
@@ -151,7 +151,7 @@
  apply (rule contI)
  apply (simp only: typedef_thelub [OF type less adm])
  apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
- apply (rule thelubE [OF _ refl])
+ apply (rule cpo_lubI)
  apply (erule ch2ch_Rep [OF less])
 done
 
diff -r f9647c040b58 -r 87cb69d27558 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Jan 31 21:37:20 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Jan 31 21:48:14 2008 +0100
@@ -148,7 +148,7 @@
 apply assumption
 apply (subst up_lemma5, assumption+)
 apply (rule is_lub_Iup)
-apply (rule thelubE [OF _ refl])
+apply (rule cpo_lubI)
 apply (erule (1) up_lemma4)
 done
 
@@ -170,7 +170,7 @@
 apply (frule up_chain_lemma, safe)
 apply (rule_tac x="Iup (lub (range A))" in exI)
 apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
-apply (simp add: is_lub_Iup thelubE)
+apply (simp add: is_lub_Iup cpo_lubI)
 apply (rule exI, rule lub_const)
 done
 
@@ -198,7 +198,7 @@
 lemma cont_Iup: "cont Iup"
 apply (rule contI)
 apply (rule is_lub_Iup)
-apply (erule thelubE [OF _ refl])
+apply (erule cpo_lubI)
 done
 
 text {* continuity for @{term Ifup} *}