# HG changeset patch
# User hoelzl
# Date 1377607076 -7200
# Node ID 5e47c31c6f7c391a10e4a4df700e68ba7b0917d7
# Parent  bae01293f4dd2bcb0d04a1399e14eee08c211388
renamed typeclass dense_linorder to unbounded_dense_linorder

diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Conditionally_Complete_Lattices.thy
--- 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
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- 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
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Fields.thy
--- 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" .. 
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Library/Float.thy
--- 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"
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Orderings.thy
--- 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 *}
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/Topological_Spaces.thy
--- 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)
 
diff -r bae01293f4dd -r 5e47c31c6f7c src/HOL/ex/Dedekind_Real.thy
--- 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)