--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Aug 28 11:15:14 2013 +0200
@@ -246,7 +246,7 @@
end
-class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
+class linear_continuum = conditionally_complete_linorder + dense_linorder +
assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
begin
@@ -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 Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 28 11:15:14 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 Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Fields.thy Wed Aug 28 11:15:14 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/Extended_Real.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Aug 28 11:15:14 2013 +0200
@@ -293,7 +293,7 @@
lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
-instance ereal :: inner_dense_linorder
+instance ereal :: dense_linorder
by default (blast dest: ereal_dense2)
instance ereal :: ordered_ab_semigroup_add
--- a/src/HOL/Library/Float.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Library/Float.thy Wed Aug 28 11:15:14 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/Library/Liminf_Limsup.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Wed Aug 28 11:15:14 2013 +0200
@@ -9,13 +9,13 @@
begin
lemma le_Sup_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
unfolding le_SUP_iff
by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
lemma Inf_le_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
unfolding INF_le_iff
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
--- a/src/HOL/Orderings.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Orderings.thy Wed Aug 28 11:15:14 2013 +0200
@@ -1230,10 +1230,10 @@
subsection {* Dense orders *}
-class inner_dense_order = order +
+class dense_order = order +
assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
-class inner_dense_linorder = linorder + inner_dense_order
+class dense_linorder = linorder + dense_order
begin
lemma dense_le:
@@ -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 = dense_linorder + no_top + no_bot
subsection {* Wellorders *}
--- a/src/HOL/Probability/Borel_Space.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Aug 28 11:15:14 2013 +0200
@@ -251,7 +251,7 @@
by (blast intro: borel_open borel_closed)+
lemma open_Collect_less:
- fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+ fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
assumes "continuous_on UNIV f"
assumes "continuous_on UNIV g"
shows "open {x. f x < g x}"
@@ -264,14 +264,14 @@
qed
lemma closed_Collect_le:
- fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+ fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
assumes f: "continuous_on UNIV f"
assumes g: "continuous_on UNIV g"
shows "closed {x. f x \<le> g x}"
using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
lemma borel_measurable_less[measurable]:
- fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+ fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -285,7 +285,7 @@
qed
lemma
- fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+ fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
assumes f[measurable]: "f \<in> borel_measurable M"
assumes g[measurable]: "g \<in> borel_measurable M"
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -755,11 +755,11 @@
by (simp add: field_divide_inverse)
lemma borel_measurable_max[measurable (raw)]:
- "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+ "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
by (simp add: max_def)
lemma borel_measurable_min[measurable (raw)]:
- "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+ "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
by (simp add: min_def)
lemma borel_measurable_abs[measurable (raw)]:
--- a/src/HOL/Set_Interval.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Set_Interval.thy Wed Aug 28 11:15:14 2013 +0200
@@ -373,7 +373,7 @@
end
-context inner_dense_linorder
+context dense_linorder
begin
lemma greaterThanLessThan_empty_iff[simp]:
@@ -519,7 +519,7 @@
end
lemma
- fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+ fixes x y :: "'a :: {complete_lattice, dense_linorder}"
shows Sup_lessThan[simp]: "Sup {..< y} = y"
and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
--- a/src/HOL/Topological_Spaces.thy Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Aug 28 11:15:14 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 Wed Aug 28 08:56:57 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Wed Aug 28 11:15:14 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)