--- 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 *}
--- 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"
--- 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
--- 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} *}