fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
authorchaieb@chaieb-laptop
Fri Feb 06 00:10:58 2009 +0000 (2009-02-06)
changeset 29811026b0f9f579f
parent 29810 fa4ec7a7215c
child 29812 a521a6fab39b
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
src/HOL/Fundamental_Theorem_Algebra.thy
src/HOL/Integration.thy
src/HOL/Library/Library.thy
src/HOL/MacLaurin.thy
src/HOL/PReal.thy
src/HOL/Reflection/Ferrack.thy
src/HOL/Reflection/MIR.thy
     1.1 --- a/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Feb 05 15:35:06 2009 +0100
     1.2 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Fri Feb 06 00:10:58 2009 +0000
     1.3 @@ -3,7 +3,7 @@
     1.4  header{*Fundamental Theorem of Algebra*}
     1.5  
     1.6  theory Fundamental_Theorem_Algebra
     1.7 -imports Polynomial Dense_Linear_Order Complex
     1.8 +imports Polynomial Complex
     1.9  begin
    1.10  
    1.11  subsection {* Square root of complex numbers *}
    1.12 @@ -59,7 +59,8 @@
    1.13    by (rule of_real_power [symmetric])
    1.14  
    1.15  lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
    1.16 -  apply ferrack apply arith done
    1.17 +  apply (rule exI[where x = "min d1 d2 / 2"])
    1.18 +  by (simp add: field_simps min_def)
    1.19  
    1.20  text{* The triangle inequality for cmod *}
    1.21  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
     2.1 --- a/src/HOL/Integration.thy	Thu Feb 05 15:35:06 2009 +0100
     2.2 +++ b/src/HOL/Integration.thy	Fri Feb 06 00:10:58 2009 +0000
     2.3 @@ -557,8 +557,8 @@
     2.4  apply (drule_tac n = m in partition_lt_gen, auto)
     2.5  apply (frule partition_eq_bound)
     2.6  apply (drule_tac [2] partition_gt, auto)
     2.7 -apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
     2.8 -apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
     2.9 +apply (metis linear not_less partition_rhs partition_rhs2)
    2.10 +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))
    2.11  done
    2.12  
    2.13  lemma lemma_additivity4_psize_eq:
     3.1 --- a/src/HOL/Library/Library.thy	Thu Feb 05 15:35:06 2009 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Fri Feb 06 00:10:58 2009 +0000
     3.3 @@ -15,6 +15,7 @@
     3.4    Continuity
     3.5    ContNotDenum
     3.6    Countable
     3.7 +  Dense_Linear_Order
     3.8    Efficient_Nat
     3.9    Enum
    3.10    Eval_Witness
     4.1 --- a/src/HOL/MacLaurin.thy	Thu Feb 05 15:35:06 2009 +0100
     4.2 +++ b/src/HOL/MacLaurin.thy	Fri Feb 06 00:10:58 2009 +0000
     4.3 @@ -6,7 +6,7 @@
     4.4  header{*MacLaurin Series*}
     4.5  
     4.6  theory MacLaurin
     4.7 -imports Dense_Linear_Order Transcendental
     4.8 +imports Transcendental
     4.9  begin
    4.10  
    4.11  subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
     5.1 --- a/src/HOL/PReal.thy	Thu Feb 05 15:35:06 2009 +0100
     5.2 +++ b/src/HOL/PReal.thy	Fri Feb 06 00:10:58 2009 +0000
     5.3 @@ -9,7 +9,7 @@
     5.4  header {* Positive real numbers *}
     5.5  
     5.6  theory PReal
     5.7 -imports Rational Dense_Linear_Order
     5.8 +imports Rational 
     5.9  begin
    5.10  
    5.11  text{*Could be generalized and moved to @{text Ring_and_Field}*}
    5.12 @@ -22,6 +22,11 @@
    5.13              A < {r. 0 < r} &
    5.14              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    5.15  
    5.16 +lemma interval_empty_iff:
    5.17 +  "{y. (x::'a::dense_linear_order) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
    5.18 +  by (auto dest: dense)
    5.19 +
    5.20 +
    5.21  lemma cut_of_rat: 
    5.22    assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
    5.23  proof -
     6.1 --- a/src/HOL/Reflection/Ferrack.thy	Thu Feb 05 15:35:06 2009 +0100
     6.2 +++ b/src/HOL/Reflection/Ferrack.thy	Fri Feb 06 00:10:58 2009 +0000
     6.3 @@ -3,7 +3,7 @@
     6.4  *)
     6.5  
     6.6  theory Ferrack
     6.7 -imports Complex_Main Efficient_Nat
     6.8 +imports Complex_Main Dense_linear_Order Efficient_Nat
     6.9  uses ("ferrack_tac.ML")
    6.10  begin
    6.11  
     7.1 --- a/src/HOL/Reflection/MIR.thy	Thu Feb 05 15:35:06 2009 +0100
     7.2 +++ b/src/HOL/Reflection/MIR.thy	Fri Feb 06 00:10:58 2009 +0000
     7.3 @@ -3,7 +3,7 @@
     7.4  *)
     7.5  
     7.6  theory MIR
     7.7 -imports Complex_Main Efficient_Nat
     7.8 +imports Complex_Main Dense_Linear_Order Efficient_Nat
     7.9  uses ("mir_tac.ML")
    7.10  begin
    7.11