--- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Aug 27 14:37:56 2013 +0200
@@ -283,22 +283,22 @@
lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq_non_empty intro: dense_le)
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, dense_linorder} <..} = x"
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
by (auto intro!: cInf_eq intro: dense_ge)
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Aug 27 14:37:56 2013 +0200
@@ -243,7 +243,7 @@
section {* The classical QE after Langford for dense linear orders *}
-context dense_linorder
+context unbounded_dense_linorder
begin
lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
@@ -299,7 +299,8 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
+ by (rule unbounded_dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
@@ -452,7 +453,7 @@
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
and between_same: "between x x = x"
-sublocale constr_dense_linorder < dlo: dense_linorder
+sublocale constr_dense_linorder < dlo: unbounded_dense_linorder
apply unfold_locales
using gt_ex lt_ex between_less
apply auto
--- a/src/HOL/Fields.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Fields.thy Tue Aug 27 14:37:56 2013 +0200
@@ -842,7 +842,7 @@
lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
by (simp add: field_simps zero_less_two)
-subclass dense_linorder
+subclass unbounded_dense_linorder
proof
fix x y :: 'a
from less_add_one show "\<exists>y. x < y" ..
--- a/src/HOL/Library/Float.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Library/Float.thy Tue Aug 27 14:37:56 2013 +0200
@@ -180,7 +180,7 @@
and real_of_float_max: "real (max x y) = max (real x) (real y)"
by (simp_all add: min_def max_def)
-instance float :: dense_linorder
+instance float :: unbounded_dense_linorder
proof
fix a b :: float
show "\<exists>c. a < c"
--- a/src/HOL/Orderings.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Orderings.thy Tue Aug 27 14:37:56 2013 +0200
@@ -1312,7 +1312,7 @@
class no_bot = order +
assumes lt_ex: "\<exists>y. y < x"
-class dense_linorder = inner_dense_linorder + no_top + no_bot
+class unbounded_dense_linorder = inner_dense_linorder + no_top + no_bot
subsection {* Wellorders *}
--- a/src/HOL/Topological_Spaces.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Aug 27 14:37:56 2013 +0200
@@ -567,7 +567,7 @@
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
unfolding eventually_at_top_linorder by auto
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
+lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
unfolding eventually_at_top_linorder
proof safe
fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
@@ -578,7 +578,7 @@
qed
lemma eventually_gt_at_top:
- "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
+ "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
unfolding eventually_at_top_dense by auto
definition at_bot :: "('a::order) filter"
@@ -600,7 +600,7 @@
unfolding eventually_at_bot_linorder by auto
lemma eventually_at_bot_dense:
- fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
+ fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
unfolding eventually_at_bot_linorder
proof safe
fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
@@ -611,7 +611,7 @@
qed
lemma eventually_gt_at_bot:
- "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
+ "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
unfolding eventually_at_bot_dense by auto
subsection {* Sequentially *}
@@ -794,11 +794,11 @@
qed
lemma trivial_limit_at_left_real [simp]:
- "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))"
+ "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
lemma trivial_limit_at_right_real [simp]:
- "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
+ "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
@@ -1047,7 +1047,7 @@
by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
lemma filterlim_at_top_dense:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
filterlim_at_top[of f F] filterlim_iff[of f at_top F])
@@ -1084,7 +1084,7 @@
qed
lemma filterlim_at_top_gt:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
@@ -1104,7 +1104,7 @@
qed simp
lemma filterlim_at_bot_lt:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
--- a/src/HOL/ex/Dedekind_Real.thy Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Aug 27 14:37:56 2013 +0200
@@ -24,7 +24,7 @@
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
lemma interval_empty_iff:
- "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+ "{y. (x::'a::unbounded_dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
by (auto dest: dense)