renamed typeclass dense_linorder to unbounded_dense_linorder
authorhoelzl
Tue Aug 27 14:37:56 2013 +0200 (2013-08-27)
changeset 532155e47c31c6f7c
parent 53214 bae01293f4dd
child 53216 ad2e09c30aa8
renamed typeclass dense_linorder to unbounded_dense_linorder
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Fields.thy
src/HOL/Library/Float.thy
src/HOL/Orderings.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 14:37:56 2013 +0200
     1.3 @@ -283,22 +283,22 @@
     1.4  lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
     1.5    using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
     1.6  
     1.7 -lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
     1.8 +lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
     1.9    by (auto intro!: cSup_eq_non_empty intro: dense_le)
    1.10  
    1.11 -lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.12 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    1.13    by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.14  
    1.15 -lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
    1.16 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
    1.17    by (auto intro!: cSup_eq intro: dense_le_bounded)
    1.18  
    1.19 -lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, dense_linorder} <..} = x"
    1.20 +lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
    1.21    by (auto intro!: cInf_eq intro: dense_ge)
    1.22  
    1.23 -lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.24 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    1.25    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.26  
    1.27 -lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
    1.28 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
    1.29    by (auto intro!: cInf_eq intro: dense_ge_bounded)
    1.30  
    1.31  end
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Aug 26 23:39:53 2013 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Aug 27 14:37:56 2013 +0200
     2.3 @@ -243,7 +243,7 @@
     2.4  
     2.5  section {* The classical QE after Langford for dense linear orders *}
     2.6  
     2.7 -context dense_linorder
     2.8 +context unbounded_dense_linorder
     2.9  begin
    2.10  
    2.11  lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
    2.12 @@ -299,7 +299,8 @@
    2.13  lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
    2.14    le_less neq_iff linear less_not_permute
    2.15  
    2.16 -lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
    2.17 +lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
    2.18 +  by (rule unbounded_dense_linorder_axioms)
    2.19  lemma atoms[no_atp]:
    2.20    shows "TERM (less :: 'a \<Rightarrow> _)"
    2.21      and "TERM (less_eq :: 'a \<Rightarrow> _)"
    2.22 @@ -452,7 +453,7 @@
    2.23    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
    2.24      and between_same: "between x x = x"
    2.25  
    2.26 -sublocale  constr_dense_linorder < dlo: dense_linorder 
    2.27 +sublocale  constr_dense_linorder < dlo: unbounded_dense_linorder 
    2.28    apply unfold_locales
    2.29    using gt_ex lt_ex between_less
    2.30    apply auto
     3.1 --- a/src/HOL/Fields.thy	Mon Aug 26 23:39:53 2013 +0200
     3.2 +++ b/src/HOL/Fields.thy	Tue Aug 27 14:37:56 2013 +0200
     3.3 @@ -842,7 +842,7 @@
     3.4  lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
     3.5  by (simp add: field_simps zero_less_two)
     3.6  
     3.7 -subclass dense_linorder
     3.8 +subclass unbounded_dense_linorder
     3.9  proof
    3.10    fix x y :: 'a
    3.11    from less_add_one show "\<exists>y. x < y" .. 
     4.1 --- a/src/HOL/Library/Float.thy	Mon Aug 26 23:39:53 2013 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Tue Aug 27 14:37:56 2013 +0200
     4.3 @@ -180,7 +180,7 @@
     4.4      and real_of_float_max: "real (max x y) = max (real x) (real y)"
     4.5    by (simp_all add: min_def max_def)
     4.6  
     4.7 -instance float :: dense_linorder
     4.8 +instance float :: unbounded_dense_linorder
     4.9  proof
    4.10    fix a b :: float
    4.11    show "\<exists>c. a < c"
     5.1 --- a/src/HOL/Orderings.thy	Mon Aug 26 23:39:53 2013 +0200
     5.2 +++ b/src/HOL/Orderings.thy	Tue Aug 27 14:37:56 2013 +0200
     5.3 @@ -1312,7 +1312,7 @@
     5.4  class no_bot = order + 
     5.5    assumes lt_ex: "\<exists>y. y < x"
     5.6  
     5.7 -class dense_linorder = inner_dense_linorder + no_top + no_bot
     5.8 +class unbounded_dense_linorder = inner_dense_linorder + no_top + no_bot
     5.9  
    5.10  
    5.11  subsection {* Wellorders *}
     6.1 --- a/src/HOL/Topological_Spaces.thy	Mon Aug 26 23:39:53 2013 +0200
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Aug 27 14:37:56 2013 +0200
     6.3 @@ -567,7 +567,7 @@
     6.4    "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
     6.5    unfolding eventually_at_top_linorder by auto
     6.6  
     6.7 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
     6.8 +lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
     6.9    unfolding eventually_at_top_linorder
    6.10  proof safe
    6.11    fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
    6.12 @@ -578,7 +578,7 @@
    6.13  qed
    6.14  
    6.15  lemma eventually_gt_at_top:
    6.16 -  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
    6.17 +  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
    6.18    unfolding eventually_at_top_dense by auto
    6.19  
    6.20  definition at_bot :: "('a::order) filter"
    6.21 @@ -600,7 +600,7 @@
    6.22    unfolding eventually_at_bot_linorder by auto
    6.23  
    6.24  lemma eventually_at_bot_dense:
    6.25 -  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
    6.26 +  fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
    6.27    unfolding eventually_at_bot_linorder
    6.28  proof safe
    6.29    fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
    6.30 @@ -611,7 +611,7 @@
    6.31  qed
    6.32  
    6.33  lemma eventually_gt_at_bot:
    6.34 -  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
    6.35 +  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
    6.36    unfolding eventually_at_bot_dense by auto
    6.37  
    6.38  subsection {* Sequentially *}
    6.39 @@ -794,11 +794,11 @@
    6.40  qed
    6.41  
    6.42  lemma trivial_limit_at_left_real [simp]:
    6.43 -  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))"
    6.44 +  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
    6.45    unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
    6.46  
    6.47  lemma trivial_limit_at_right_real [simp]:
    6.48 -  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
    6.49 +  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
    6.50    unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
    6.51  
    6.52  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
    6.53 @@ -1047,7 +1047,7 @@
    6.54    by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
    6.55  
    6.56  lemma filterlim_at_top_dense:
    6.57 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
    6.58 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
    6.59    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
    6.60    by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
    6.61              filterlim_at_top[of f F] filterlim_iff[of f at_top F])
    6.62 @@ -1084,7 +1084,7 @@
    6.63  qed
    6.64  
    6.65  lemma filterlim_at_top_gt:
    6.66 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
    6.67 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
    6.68    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
    6.69    by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
    6.70  
    6.71 @@ -1104,7 +1104,7 @@
    6.72  qed simp
    6.73  
    6.74  lemma filterlim_at_bot_lt:
    6.75 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
    6.76 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
    6.77    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
    6.78    by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
    6.79  
     7.1 --- a/src/HOL/ex/Dedekind_Real.thy	Mon Aug 26 23:39:53 2013 +0200
     7.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Aug 27 14:37:56 2013 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
     7.5  
     7.6  lemma interval_empty_iff:
     7.7 -  "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
     7.8 +  "{y. (x::'a::unbounded_dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
     7.9    by (auto dest: dense)
    7.10  
    7.11