1.1 --- a/src/HOLCF/Completion.thy	Sat Nov 27 12:27:57 2010 -0800
     1.2 +++ b/src/HOLCF/Completion.thy	Sat Nov 27 12:38:02 2010 -0800
     1.3 @@ -100,7 +100,7 @@
     1.4    assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
     1.5    assumes S: "chain S"
     1.6    shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
     1.7 -    and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
     1.8 +    and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
     1.9  proof -
    1.10    have 1: "ideal (\<Union>i. Rep (S i))"
    1.11      apply (rule ideal_UN)
    1.12 @@ -154,7 +154,7 @@
    1.13    fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
    1.14    fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
    1.15    assumes ideal_rep: "\<And>x. ideal (rep x)"
    1.16 -  assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
    1.17 +  assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
    1.18    assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
    1.19    assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
    1.20    assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
    1.21 @@ -162,7 +162,7 @@
    1.22  
    1.23  lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
    1.24  apply (frule bin_chain)
    1.25 -apply (drule rep_contlub)
    1.26 +apply (drule rep_lub)
    1.27  apply (simp only: thelubI [OF lub_bin_chain])
    1.28  apply (rule subsetI, rule UN_I [where a=0], simp_all)
    1.29  done
    1.30 @@ -215,7 +215,7 @@
    1.31  subsubsection {* Principal ideals approximate all elements *}
    1.32  
    1.33  lemma compact_principal [simp]: "compact (principal a)"
    1.34 -by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
    1.35 +by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub)
    1.36  
    1.37  text {* Construct a chain whose lub is the same as a given ideal *}
    1.38  
    1.39 @@ -285,7 +285,7 @@
    1.40    have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
    1.41      by (simp add: X_chain)
    1.42    have 2: "x = (\<Squnion>n. principal (enum (X n)))"
    1.43 -    apply (simp add: eq_iff rep_contlub 1 rep_principal)
    1.44 +    apply (simp add: eq_iff rep_lub 1 rep_principal)
    1.45      apply (auto, rename_tac a)
    1.46      apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
    1.47      apply (rule_tac x=i in exI, simp add: X_covers)
    1.48 @@ -345,7 +345,7 @@
    1.49    have chain: "chain (\<lambda>i. f (Y i))"
    1.50      by (rule chainI, simp add: f_mono Y)
    1.51    have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})"
    1.52 -    by (simp add: x rep_contlub Y rep_principal)
    1.53 +    by (simp add: x rep_lub Y rep_principal)
    1.54    have "f ` rep x <<| (\<Squnion>n. f (Y n))"
    1.55      apply (rule is_lubI)
    1.56      apply (rule ub_imageI, rename_tac a)
    1.57 @@ -375,7 +375,7 @@
    1.58       apply (rule is_ub_thelub_ex [OF lub imageI])
    1.59       apply (erule (1) subsetD [OF rep_mono])
    1.60      apply (rule is_lub_thelub_ex [OF lub ub_imageI])
    1.61 -    apply (simp add: rep_contlub, clarify)
    1.62 +    apply (simp add: rep_lub, clarify)
    1.63      apply (erule rev_below_trans [OF is_ub_thelub])
    1.64      apply (erule is_ub_thelub_ex [OF lub imageI])
    1.65      done
    1.66 @@ -421,7 +421,7 @@
    1.67    show "ideal (Rep x)"
    1.68      using Rep [of x] by simp
    1.69    show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
    1.70 -    using type below by (rule typedef_ideal_rep_contlub)
    1.71 +    using type below by (rule typedef_ideal_rep_lub)
    1.72    show "Rep (principal a) = {b. b \<preceq> a}"
    1.73      by (simp add: principal Abs_inverse ideal_principal)
    1.74    show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"