# HG changeset patch
# User chaieb@chaieb-laptop
# Date 1233879058 0
# Node ID 026b0f9f579f18a356e870e68045098c63a84f5e
# Parent  fa4ec7a7215c91a6293b8c6f14d7ca00bb9a34a0
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library

diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
 header{*Fundamental Theorem of Algebra*}
 
 theory Fundamental_Theorem_Algebra
-imports Polynomial Dense_Linear_Order Complex
+imports Polynomial Complex
 begin
 
 subsection {* Square root of complex numbers *}
@@ -59,7 +59,8 @@
   by (rule of_real_power [symmetric])
 
 lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
-  apply ferrack apply arith done
+  apply (rule exI[where x = "min d1 d2 / 2"])
+  by (simp add: field_simps min_def)
 
 text{* The triangle inequality for cmod *}
 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Integration.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -557,8 +557,8 @@
 apply (drule_tac n = m in partition_lt_gen, auto)
 apply (frule partition_eq_bound)
 apply (drule_tac [2] partition_gt, auto)
-apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
-apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
+apply (metis linear not_less partition_rhs partition_rhs2)
+apply (metis add_diff_inverse diff_is_0_eq le0 le_diff_conv nat_add_commute partition partition_eq_bound partition_rhs real_less_def termination_basic_simps(5))
 done
 
 lemma lemma_additivity4_psize_eq:
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Library/Library.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -15,6 +15,7 @@
   Continuity
   ContNotDenum
   Countable
+  Dense_Linear_Order
   Efficient_Nat
   Enum
   Eval_Witness
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/MacLaurin.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -6,7 +6,7 @@
 header{*MacLaurin Series*}
 
 theory MacLaurin
-imports Dense_Linear_Order Transcendental
+imports Transcendental
 begin
 
 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/PReal.thy
--- a/src/HOL/PReal.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/PReal.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -9,7 +9,7 @@
 header {* Positive real numbers *}
 
 theory PReal
-imports Rational Dense_Linear_Order
+imports Rational 
 begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}
@@ -22,6 +22,11 @@
             A < {r. 0 < r} &
             (\<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_linear_order) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+  by (auto dest: dense)
+
+
 lemma cut_of_rat: 
   assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
 proof -
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/Reflection/Ferrack.thy
--- a/src/HOL/Reflection/Ferrack.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Reflection/Ferrack.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
 *)
 
 theory Ferrack
-imports Complex_Main Efficient_Nat
+imports Complex_Main Dense_linear_Order Efficient_Nat
 uses ("ferrack_tac.ML")
 begin
 
diff -r fa4ec7a7215c -r 026b0f9f579f src/HOL/Reflection/MIR.thy
--- a/src/HOL/Reflection/MIR.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Reflection/MIR.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
 *)
 
 theory MIR
-imports Complex_Main Efficient_Nat
+imports Complex_Main Dense_Linear_Order Efficient_Nat
 uses ("mir_tac.ML")
 begin