author chaieb@chaieb-laptop Fri, 06 Feb 2009 00:10:58 +0000 changeset 29811 026b0f9f579f parent 29810 fa4ec7a7215c child 29812 a521a6fab39b
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
 src/HOL/Fundamental_Theorem_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Integration.thy file | annotate | diff | comparison | revisions src/HOL/Library/Library.thy file | annotate | diff | comparison | revisions src/HOL/MacLaurin.thy file | annotate | diff | comparison | revisions src/HOL/PReal.thy file | annotate | diff | comparison | revisions src/HOL/Reflection/Ferrack.thy file | annotate | diff | comparison | revisions src/HOL/Reflection/MIR.thy file | annotate | diff | comparison | revisions
```--- 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 @@

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"```
```--- 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

```--- 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```
```--- 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 @@

theory MacLaurin
-imports Dense_Linear_Order Transcendental
+imports Transcendental
begin

subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}```
```--- 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 -```
```--- 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
```
```--- 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
```