author huffman Sat Nov 27 12:38:02 2010 -0800 (2010-11-27) changeset 40769 3af9b0df3521 parent 40768 50a80cf4b7ef child 40770 6023808b38d4
rename rep_contlub lemmas to rep_lub
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.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.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.37  text {* Construct a chain whose lub is the same as a given ideal *}
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"