--- a/src/HOL/Conditionally_Complete_Lattices.thy Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Aug 27 16:06:27 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
--- a/src/HOL/Library/Extended_Real.thy Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Aug 27 16:06:27 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/Liminf_Limsup.thy Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Aug 27 16:06:27 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 Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Orderings.thy Tue Aug 27 16:06:27 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 unbounded_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 Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Tue Aug 27 16:06:27 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 Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Set_Interval.thy Tue Aug 27 16:06:27 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"