# HG changeset patch
# User huffman
# Date 1290892330 28800
# Node ID 1c6f7d4b110e85b3b10375c8938c59056efec72f
# Parent  6023808b38d4b04a81661a8986ba30c897816a6a
renamed several HOLCF theorems (listed in NEWS)

diff -r 6023808b38d4 -r 1c6f7d4b110e NEWS
--- a/NEWS	Sat Nov 27 12:55:12 2010 -0800
+++ b/NEWS	Sat Nov 27 13:12:10 2010 -0800
@@ -461,6 +461,22 @@
 * Case combinators generated by the domain package for type 'foo'
 are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
 
+* Several theorems have been renamed to more accurately reflect the
+names of constants and types involved. INCOMPATIBILITY.
+  thelub_const    ~> lub_const
+  lub_const       ~> is_lub_const
+  thelubI         ~> lub_eqI
+  is_lub_lub      ~> is_lubD2
+  lubI            ~> is_lub_lub
+  unique_lub      ~> is_lub_unique
+  is_ub_lub       ~> is_lub_rangeD1
+  lub_bin_chain   ~> is_lub_bin_chain
+  thelub_Pair     ~> lub_Pair
+  lub_cprod       ~> is_lub_prod
+  thelub_cprod    ~> lub_prod
+  minimal_cprod   ~> minimal_prod
+  inst_cprod_pcpo ~> inst_prod_pcpo
+
 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.
   sq_ord_less_eq_trans ~> below_eq_trans
   sq_ord_eq_less_trans ~> eq_below_trans
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Bifinite.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -642,7 +642,7 @@
 apply (simp add: contlub_cfun_fun)
 apply (simp add: discr_approx_def)
 apply (case_tac x, simp)
-apply (rule thelubI)
+apply (rule lub_eqI)
 apply (rule is_lubI)
 apply (rule ub_rangeI, simp)
 apply (drule ub_rangeD)
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -209,15 +209,9 @@
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
 by (rule cont_Rep_cfun2 [THEN cont2contlubE])
 
-lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_cfun2 [THEN contE])
-
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
 by (rule cont_Rep_cfun1 [THEN cont2contlubE])
 
-lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_cfun1 [THEN contE])
-
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
@@ -287,7 +281,7 @@
 by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
 
 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (rule lub_cfun [THEN thelubI])
+by (rule lub_cfun [THEN lub_eqI])
 
 subsection {* Continuity simplification procedure *}
 
@@ -370,7 +364,7 @@
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
+apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
 done
 
 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Completion.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -55,7 +55,7 @@
 lemma lub_image_principal:
   assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
-apply (rule thelubI)
+apply (rule lub_eqI)
 apply (rule is_lub_maximal)
 apply (rule ub_imageI)
 apply (simp add: f)
@@ -117,7 +117,7 @@
     apply (simp add: below 2 is_ub_def, fast)
     done
   hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
-    by (rule thelubI)
+    by (rule lub_eqI)
   show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
     by (simp add: 4 2)
 qed
@@ -140,13 +140,13 @@
 subsection {* Lemmas about least upper bounds *}
 
 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
-apply (erule exE, drule lubI)
+apply (erule exE, drule is_lub_lub)
 apply (drule is_lubD1)
 apply (erule (1) is_ubD)
 done
 
 lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
-by (erule exE, drule lubI, erule is_lub_lub)
+by (erule exE, drule is_lub_lub, erule is_lubD2)
 
 subsection {* Locale for ideal completion *}
 
@@ -163,7 +163,7 @@
 lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
 apply (frule bin_chain)
 apply (drule rep_lub)
-apply (simp only: thelubI [OF lub_bin_chain])
+apply (simp only: lub_eqI [OF is_lub_bin_chain])
 apply (rule subsetI, rule UN_I [where a=0], simp_all)
 done
 
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Cont.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -72,7 +72,7 @@
 apply (erule contE)
 apply (erule bin_chain)
 apply (rule_tac f=f in arg_cong)
-apply (erule lub_bin_chain [THEN thelubI])
+apply (erule is_lub_bin_chain [THEN lub_eqI])
 done
 
 text {* continuity implies monotonicity *}
@@ -80,7 +80,7 @@
 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
 apply (rule monofunI)
 apply (drule (1) binchain_cont)
-apply (drule_tac i=0 in is_ub_lub)
+apply (drule_tac i=0 in is_lub_rangeD1)
 apply simp
 done
 
@@ -92,7 +92,7 @@
 
 lemma cont2contlubE:
   "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
-apply (rule thelubI [symmetric])
+apply (rule lub_eqI [symmetric])
 apply (erule (1) contE)
 done
 
@@ -142,9 +142,7 @@
 text {* constant functions are continuous *}
 
 lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
-apply (rule contI)
-apply (rule lub_const)
-done
+  using is_lub_const by (rule contI)
 
 text {* application of functions is continuous *}
 
@@ -235,7 +233,7 @@
 lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
 apply (rule contI)
 apply (drule discrete_chain_const, clarify)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
 done
 
 end
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -225,7 +225,7 @@
 lemma fstream_lub_lemma1:
     "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
 apply (case_tac "max_in_chain i Y")
-apply  (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
 apply  (force)
 apply (unfold max_in_chain_def)
 apply auto
@@ -254,7 +254,7 @@
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)
-apply (subst lub_const [THEN thelubI])
+apply (subst lub_const)
 apply (subst lub_range_shift)
 apply  (assumption)
 apply (simp)
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -246,7 +246,7 @@
 apply (drule fstreams_lub_lemma1, auto)
 apply (rule_tac x="j" in exI, auto)
 apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
 apply (rule_tac x="j" in exI)
 apply (erule subst) back back
 apply (simp add: below_prod_def sconc_mono)
@@ -266,7 +266,7 @@
 lemma lub_Pair_not_UU_lemma: 
   "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
       ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
-apply (frule thelub_cprod, clarsimp)
+apply (frule lub_prod, clarsimp)
 apply (drule chain_UU_I_inverse2, clarsimp)
 apply (case_tac "Y i", clarsimp)
 apply (case_tac "max_in_chain i Y")
@@ -298,7 +298,7 @@
 apply (drule fstreams_lub_lemma2, auto)
 apply (rule_tac x="j" in exI, auto)
 apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
 apply (rule_tac x="j" in exI)
 apply (erule subst) back back
 apply (simp add: sconc_mono)
@@ -312,7 +312,7 @@
 apply (rule sconc_mono)
 apply (subgoal_tac "tt ~= tta" "tta << ms")
 apply (blast intro: fstreams_chain_lemma)
-apply (frule lub_cprod [THEN thelubI], auto)
+apply (frule lub_prod, auto)
 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
 apply (drule fstreams_mono, simp)
 apply (rule is_ub_thelub chainI)
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -37,7 +37,7 @@
 prefer 2 apply fast
 apply (unfold finite_chain_def)
 apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
 apply assumption
 apply (erule spec)
 done
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Fix.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -183,7 +183,7 @@
   hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
     by - (rule admD [OF adm'], simp, assumption)
   hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
-    by (simp add: thelub_Pair)
+    by (simp add: lub_Pair)
   hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
     by simp
   thus "P (fix\<cdot>F) (fix\<cdot>G)"
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Fun_Cpo.thy
--- a/src/HOLCF/Fun_Cpo.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Fun_Cpo.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -80,7 +80,7 @@
 lemma thelub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN thelubI])
+by (rule lub_fun [THEN lub_eqI])
 
 instance "fun"  :: (type, cpo) cpo
 by intro_classes (rule exI, erule lub_fun)
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/HOLCF.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -30,5 +30,10 @@
 lemmas cont2cont_Rep_CFun = cont2cont_APP
 lemmas cont_Rep_CFun_app = cont_APP_app
 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
+lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
+lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
+(*
+lemmas thelubI = lub_eqI
+*)
 
 end
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Library/List_Cpo.thy
--- a/src/HOLCF/Library/List_Cpo.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Library/List_Cpo.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -141,7 +141,7 @@
   fix S :: "nat \<Rightarrow> 'a list"
   assume "chain S" thus "\<exists>x. range S <<| x"
   proof (induct rule: list_chain_induct)
-    case Nil thus ?case by (auto intro: lub_const)
+    case Nil thus ?case by (auto intro: is_lub_const)
   next
     case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
   qed
@@ -163,7 +163,7 @@
   fixes A :: "nat \<Rightarrow> 'a::cpo"
   assumes A: "chain A" and B: "chain B"
   shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
-by (intro thelubI is_lub_Cons cpo_lubI A B)
+by (intro lub_eqI is_lub_Cons cpo_lubI A B)
 
 lemma cont2cont_list_case:
   assumes f: "cont (\<lambda>x. f x)"
@@ -175,7 +175,7 @@
 apply (rule cont_apply [OF f])
 apply (rule contI)
 apply (erule list_chain_cases)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
 apply (simp add: lub_Cons)
 apply (simp add: cont2contlubE [OF h2])
 apply (simp add: cont2contlubE [OF h3])
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOLCF/Library/Sum_Cpo.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -98,10 +98,10 @@
 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (simp add: is_ub_lub)
+  apply (simp add: is_lub_rangeD1)
  apply (frule ub_rangeD [where i=arbitrary])
  apply (erule Inl_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
 done
@@ -109,10 +109,10 @@
 lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (simp add: is_ub_lub)
+  apply (simp add: is_lub_rangeD1)
  apply (frule ub_rangeD [where i=arbitrary])
  apply (erule Inr_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
 done
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Pcpo.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -19,19 +19,19 @@
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
-  by (fast dest: cpo elim: lubI)
+  by (fast dest: cpo elim: is_lub_lub)
 
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
-  by (blast dest: cpo intro: lubI)
+  by (blast dest: cpo intro: is_lub_lub)
 
 text {* Properties of the lub *}
 
 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
-  by (blast dest: cpo intro: lubI [THEN is_ub_lub])
+  by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
 
 lemma is_lub_thelub:
   "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
-  by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+  by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
 
 lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
   by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
@@ -70,7 +70,7 @@
 lemma maxinch_is_thelub:
   "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
 apply (rule iffI)
-apply (fast intro!: thelubI lub_finch1)
+apply (fast intro!: lub_eqI lub_finch1)
 apply (unfold max_in_chain_def)
 apply (safe intro!: below_antisym)
 apply (fast elim!: chain_mono)
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Pcpodef.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -107,7 +107,7 @@
     by (rule typedef_is_lubI [OF below])
 qed
 
-lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
+lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
 
 theorem typedef_cpo:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Porder.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -126,7 +126,7 @@
 lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
   unfolding is_lub_def by fast
 
-lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
+lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
   unfolding is_lub_def by fast
 
 lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
@@ -137,40 +137,34 @@
 
 text {* lubs are unique *}
 
-lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
-apply (unfold is_lub_def is_ub_def)
-apply (blast intro: below_antisym)
-done
+lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
+  unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
 
 text {* technical lemmas about @{term lub} and @{term is_lub} *}
 
-lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
-apply (unfold lub_def)
-apply (rule theI)
-apply assumption
-apply (erule (1) unique_lub)
-done
+lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
+  unfolding lub_def by (rule theI [OF _ is_lub_unique])
 
-lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
-  by (rule unique_lub [OF lubI])
+lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
+  by (rule is_lub_unique [OF is_lub_lub])
 
 lemma is_lub_singleton: "{x} <<| x"
   by (simp add: is_lub_def)
 
 lemma lub_singleton [simp]: "lub {x} = x"
-  by (rule thelubI [OF is_lub_singleton])
+  by (rule is_lub_singleton [THEN lub_eqI])
 
 lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
   by (simp add: is_lub_def)
 
 lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
-  by (rule is_lub_bin [THEN thelubI])
+  by (rule is_lub_bin [THEN lub_eqI])
 
 lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
   by (erule is_lubI, erule (1) is_ubD)
 
 lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
-  by (rule is_lub_maximal [THEN thelubI])
+  by (rule is_lub_maximal [THEN lub_eqI])
 
 subsection {* Countable chains *}
 
@@ -197,7 +191,7 @@
 
 text {* technical lemmas about (least) upper bounds of chains *}
 
-lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
+lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
   by (rule is_lubD1 [THEN ub_rangeD])
 
 lemma is_ub_range_shift:
@@ -221,11 +215,11 @@
 lemma chain_const [simp]: "chain (\<lambda>i. c)"
   by (simp add: chainI)
 
-lemma lub_const: "range (\<lambda>x. c) <<| c"
+lemma is_lub_const: "range (\<lambda>x. c) <<| c"
 by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
 
-lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
-  by (rule lub_const [THEN thelubI])
+lemma lub_const [simp]: "(\<Squnion>i. c) = c"
+  by (rule is_lub_const [THEN lub_eqI])
 
 subsection {* Finite chains *}
 
@@ -324,7 +318,7 @@
   "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
   unfolding max_in_chain_def by simp
 
-lemma lub_bin_chain:
+lemma is_lub_bin_chain:
   "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
 apply (frule bin_chain)
 apply (drule bin_chainmax)
@@ -335,7 +329,7 @@
 text {* the maximal element in a chain is its lub *}
 
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
-  by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
+  by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
 
 end
 
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Product_Cpo.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -111,46 +111,30 @@
 
 lemma is_lub_Pair:
   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: below_prod_def is_lub_lub)
-done
+unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
 
-lemma thelub_Pair:
+lemma lub_Pair:
   "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-by (fast intro: thelubI is_lub_Pair elim: thelubE)
+by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
 
-lemma lub_cprod:
+lemma is_lub_prod:
   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))"
-proof -
-  from `chain S` have "chain (\<lambda>i. fst (S i))"
-    by (rule ch2ch_fst)
-  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
-    by (rule cpo_lubI)
-  from `chain S` have "chain (\<lambda>i. snd (S i))"
-    by (rule ch2ch_snd)
-  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
-    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
+using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
 
-lemma thelub_cprod:
+lemma lub_prod:
   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
     \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
+by (rule is_lub_prod [THEN lub_eqI])
 
 instance prod :: (cpo, cpo) cpo
 proof
   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   assume "chain S"
   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-    by (rule lub_cprod)
+    by (rule is_lub_prod)
   thus "\<exists>x. range S <<| x" ..
 qed
 
@@ -164,23 +148,23 @@
 
 subsection {* Product type is pointed *}
 
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
 by (simp add: below_prod_def)
 
 instance prod :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
+by intro_classes (fast intro: minimal_prod)
 
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
+lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
+by (rule minimal_prod [THEN UU_I, symmetric])
 
 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-unfolding inst_cprod_pcpo by simp
+unfolding inst_prod_pcpo by simp
 
 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule fst_conv)
+unfolding inst_prod_pcpo by (rule fst_conv)
 
 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule snd_conv)
+unfolding inst_prod_pcpo by (rule snd_conv)
 
 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
 by simp
@@ -194,25 +178,25 @@
 apply (rule contI)
 apply (rule is_lub_Pair)
 apply (erule cpo_lubI)
-apply (rule lub_const)
+apply (rule is_lub_const)
 done
 
 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
 apply (rule contI)
 apply (rule is_lub_Pair)
-apply (rule lub_const)
+apply (rule is_lub_const)
 apply (erule cpo_lubI)
 done
 
 lemma cont_fst: "cont fst"
 apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
 apply (erule cpo_lubI [OF ch2ch_fst])
 done
 
 lemma cont_snd: "cont snd"
 apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
 apply (erule cpo_lubI [OF ch2ch_snd])
 done
 
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Nov 27 13:12:10 2010 -0800
@@ -711,7 +711,7 @@
         val goal = mk_trp (mk_eq (lhs, rhs));
         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
         val start_rules =
-            @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+            @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
             @ @{thms pair_collapse split_def}
             @ map_apply_thms @ map_ID_thms;
         val rules0 =
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Up.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -111,7 +111,7 @@
   proof (rule up_chain_lemma)
     assume "\<forall>i. S i = Ibottom"
     hence "range (\<lambda>i. S i) <<| Ibottom"
-      by (simp add: lub_const)
+      by (simp add: is_lub_const)
     thus ?thesis ..
   next
     fix A :: "nat \<Rightarrow> 'a"
@@ -160,7 +160,7 @@
     assume A: "\<forall>i. Iup (A i) = Y (i + k)"
     assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
     hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
-      by (simp add: thelubI contlub_cfun_arg)
+      by (simp add: lub_eqI contlub_cfun_arg)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
       by (simp add: A)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
@@ -223,7 +223,7 @@
   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
   | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
 apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
 done
 
 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
diff -r 6023808b38d4 -r 1c6f7d4b110e src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -467,7 +467,7 @@
 lemma lub_take_lemma:
   "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
     = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
-apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
 apply (simp only: map_apply_thms pair_collapse)
 apply (simp only: fix_def2)
 apply (rule lub_eq)