merged
authorhaftmann
Mon Feb 08 14:08:32 2010 +0100 (2010-02-08)
changeset 35039e682bb587071
parent 35031 2ddc7edce107
parent 35038 a1d93ce94235
child 35040 e42e7f133d94
child 35041 6eb917794a5c
merged
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/NEWS	Mon Feb 08 14:04:51 2010 +0100
     1.2 +++ b/NEWS	Mon Feb 08 14:08:32 2010 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* more consistent naming of type classes involving orderings (and lattices):
     1.8 +* More consistent naming of type classes involving orderings (and lattices):
     1.9  
    1.10      lower_semilattice                   ~> semilattice_inf
    1.11      upper_semilattice                   ~> semilattice_sup
    1.12 @@ -33,12 +33,6 @@
    1.13      pordered_ring_abs                   ~> ordered_ring_abs
    1.14      pordered_semiring                   ~> ordered_semiring
    1.15  
    1.16 -    lordered_ab_group_add               ~> lattice_ab_group_add
    1.17 -    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
    1.18 -    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
    1.19 -    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
    1.20 -    lordered_ring                       ~> lattice_ring
    1.21 -
    1.22      ordered_ab_group_add                ~> linordered_ab_group_add
    1.23      ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
    1.24      ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
    1.25 @@ -58,6 +52,15 @@
    1.26      ordered_semiring_1_strict           ~> linordered_semiring_1_strict
    1.27      ordered_semiring_strict             ~> linordered_semiring_strict
    1.28  
    1.29 +  The following slightly odd type classes have been moved to
    1.30 +  a separate theory Library/Lattice_Algebras.thy:
    1.31 +
    1.32 +    lordered_ab_group_add               ~> lattice_ab_group_add
    1.33 +    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
    1.34 +    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
    1.35 +    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
    1.36 +    lordered_ring                       ~> lattice_ring
    1.37 +
    1.38  INCOMPATIBILITY.
    1.39  
    1.40  * Index syntax for structures must be imported explicitly from library
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:04:51 2010 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 14:08:32 2010 +0100
     2.3 @@ -2187,10 +2187,7 @@
     2.4    {assume dc: "?c*?d < 0" 
     2.5  
     2.6      from dc one_plus_one_pos[where ?'a='a] have dc': "(1 + 1)*?c *?d < 0"
     2.7 -      apply (simp add: mult_less_0_iff field_simps) 
     2.8 -      apply (rule add_neg_neg)
     2.9 -      apply (simp_all add: mult_less_0_iff)
    2.10 -      done
    2.11 +      by (simp add: mult_less_0_iff field_simps) 
    2.12      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
    2.13      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
    2.14      have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" 
     3.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 08 14:04:51 2010 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 08 14:08:32 2010 +0100
     3.3 @@ -3324,6 +3324,19 @@
     3.4  
     3.5  end
     3.6  
     3.7 +context linordered_ab_group_add
     3.8 +begin
     3.9 +
    3.10 +lemma minus_Max_eq_Min [simp]:
    3.11 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
    3.12 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
    3.13 +
    3.14 +lemma minus_Min_eq_Max [simp]:
    3.15 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
    3.16 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
    3.17 +
    3.18 +end
    3.19 +
    3.20  
    3.21  subsection {* Expressing set operations via @{const fold} *}
    3.22  
     4.1 --- a/src/HOL/Int.thy	Mon Feb 08 14:04:51 2010 +0100
     4.2 +++ b/src/HOL/Int.thy	Mon Feb 08 14:08:32 2010 +0100
     4.3 @@ -256,13 +256,6 @@
     4.4      by (simp only: zsgn_def)
     4.5  qed
     4.6  
     4.7 -instance int :: lattice_ring
     4.8 -proof  
     4.9 -  fix k :: int
    4.10 -  show "abs k = sup k (- k)"
    4.11 -    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
    4.12 -qed
    4.13 -
    4.14  lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
    4.15  apply (cases w, cases z) 
    4.16  apply (simp add: less le add One_int_def)
     5.1 --- a/src/HOL/IsaMakefile	Mon Feb 08 14:04:51 2010 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Mon Feb 08 14:08:32 2010 +0100
     5.3 @@ -384,6 +384,7 @@
     5.4    Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
     5.5    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
     5.6    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
     5.7 +  Library/Lattice_Algebras.thy						\
     5.8    Library/Lattice_Syntax.thy Library/Library.thy			\
     5.9    Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
    5.10    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
     6.1 --- a/src/HOL/Library/Float.thy	Mon Feb 08 14:04:51 2010 +0100
     6.2 +++ b/src/HOL/Library/Float.thy	Mon Feb 08 14:08:32 2010 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Floating-Point Numbers *}
     6.5  
     6.6  theory Float
     6.7 -imports Complex_Main
     6.8 +imports Complex_Main Lattice_Algebras
     6.9  begin
    6.10  
    6.11  definition
     7.1 --- a/src/HOL/Library/Library.thy	Mon Feb 08 14:04:51 2010 +0100
     7.2 +++ b/src/HOL/Library/Library.thy	Mon Feb 08 14:08:32 2010 +0100
     7.3 @@ -28,6 +28,7 @@
     7.4    Fundamental_Theorem_Algebra
     7.5    Infinite_Set
     7.6    Inner_Product
     7.7 +  Lattice_Algebras
     7.8    Lattice_Syntax
     7.9    ListVector
    7.10    Kleene_Algebra
     8.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Mon Feb 08 14:04:51 2010 +0100
     8.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Mon Feb 08 14:08:32 2010 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* Floating Point Representation of the Reals *}
     8.5  
     8.6  theory ComputeFloat
     8.7 -imports Complex_Main
     8.8 +imports Complex_Main Lattice_Algebras
     8.9  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    8.10  begin
    8.11  
     9.1 --- a/src/HOL/Matrix/LP.thy	Mon Feb 08 14:04:51 2010 +0100
     9.2 +++ b/src/HOL/Matrix/LP.thy	Mon Feb 08 14:08:32 2010 +0100
     9.3 @@ -3,7 +3,7 @@
     9.4  *)
     9.5  
     9.6  theory LP 
     9.7 -imports Main
     9.8 +imports Main Lattice_Algebras
     9.9  begin
    9.10  
    9.11  lemma linprog_dual_estimate:
    10.1 --- a/src/HOL/Matrix/Matrix.thy	Mon Feb 08 14:04:51 2010 +0100
    10.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Feb 08 14:08:32 2010 +0100
    10.3 @@ -3,7 +3,7 @@
    10.4  *)
    10.5  
    10.6  theory Matrix
    10.7 -imports Main
    10.8 +imports Main Lattice_Algebras
    10.9  begin
   10.10  
   10.11  types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
    11.1 --- a/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:04:51 2010 +0100
    11.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:08:32 2010 +0100
    11.3 @@ -849,12 +849,7 @@
    11.4      simp add: abs_ge_self abs_leI abs_triangle_ineq)+
    11.5  
    11.6  instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
    11.7 -instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add ..
    11.8 -instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add ..
    11.9 -instance star :: (lattice_ab_group_add) lattice_ab_group_add ..
   11.10  
   11.11 -instance star :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
   11.12 -by (intro_classes, transfer, rule abs_lattice)
   11.13  
   11.14  subsection {* Ring and field classes *}
   11.15  
   11.16 @@ -934,7 +929,6 @@
   11.17  instance star :: (ordered_ring) ordered_ring ..
   11.18  instance star :: (ordered_ring_abs) ordered_ring_abs
   11.19    by intro_classes  (transfer, rule abs_eq_mult)
   11.20 -instance star :: (lattice_ring) lattice_ring ..
   11.21  
   11.22  instance star :: (abs_if) abs_if
   11.23  by (intro_classes, transfer, rule abs_if)
    12.1 --- a/src/HOL/OrderedGroup.thy	Mon Feb 08 14:04:51 2010 +0100
    12.2 +++ b/src/HOL/OrderedGroup.thy	Mon Feb 08 14:08:32 2010 +0100
    12.3 @@ -710,7 +710,7 @@
    12.4  
    12.5  subclass linordered_cancel_ab_semigroup_add ..
    12.6  
    12.7 -lemma neg_less_eq_nonneg:
    12.8 +lemma neg_less_eq_nonneg [simp]:
    12.9    "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   12.10  proof
   12.11    assume A: "- a \<le> a" show "0 \<le> a"
   12.12 @@ -728,8 +728,27 @@
   12.13      show "0 \<le> a" using A .
   12.14    qed
   12.15  qed
   12.16 -  
   12.17 -lemma less_eq_neg_nonpos:
   12.18 +
   12.19 +lemma neg_less_nonneg [simp]:
   12.20 +  "- a < a \<longleftrightarrow> 0 < a"
   12.21 +proof
   12.22 +  assume A: "- a < a" show "0 < a"
   12.23 +  proof (rule classical)
   12.24 +    assume "\<not> 0 < a"
   12.25 +    then have "a \<le> 0" by auto
   12.26 +    with A have "- a < 0" by (rule less_le_trans)
   12.27 +    then show ?thesis by auto
   12.28 +  qed
   12.29 +next
   12.30 +  assume A: "0 < a" show "- a < a"
   12.31 +  proof (rule less_trans)
   12.32 +    show "- a < 0" using A by (simp add: minus_le_iff)
   12.33 +  next
   12.34 +    show "0 < a" using A .
   12.35 +  qed
   12.36 +qed
   12.37 +
   12.38 +lemma less_eq_neg_nonpos [simp]:
   12.39    "a \<le> - a \<longleftrightarrow> a \<le> 0"
   12.40  proof
   12.41    assume A: "a \<le> - a" show "a \<le> 0"
   12.42 @@ -748,7 +767,7 @@
   12.43    qed
   12.44  qed
   12.45  
   12.46 -lemma equal_neg_zero:
   12.47 +lemma equal_neg_zero [simp]:
   12.48    "a = - a \<longleftrightarrow> a = 0"
   12.49  proof
   12.50    assume "a = 0" then show "a = - a" by simp
   12.51 @@ -765,9 +784,81 @@
   12.52    qed
   12.53  qed
   12.54  
   12.55 -lemma neg_equal_zero:
   12.56 +lemma neg_equal_zero [simp]:
   12.57    "- a = a \<longleftrightarrow> a = 0"
   12.58 -  unfolding equal_neg_zero [symmetric] by auto
   12.59 +  by (auto dest: sym)
   12.60 +
   12.61 +lemma double_zero [simp]:
   12.62 +  "a + a = 0 \<longleftrightarrow> a = 0"
   12.63 +proof
   12.64 +  assume assm: "a + a = 0"
   12.65 +  then have a: "- a = a" by (rule minus_unique)
   12.66 +  then show "a = 0" by (simp add: neg_equal_zero)
   12.67 +qed simp
   12.68 +
   12.69 +lemma double_zero_sym [simp]:
   12.70 +  "0 = a + a \<longleftrightarrow> a = 0"
   12.71 +  by (rule, drule sym) simp_all
   12.72 +
   12.73 +lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   12.74 +  "0 < a + a \<longleftrightarrow> 0 < a"
   12.75 +proof
   12.76 +  assume "0 < a + a"
   12.77 +  then have "0 - a < a" by (simp only: diff_less_eq)
   12.78 +  then have "- a < a" by simp
   12.79 +  then show "0 < a" by (simp add: neg_less_nonneg)
   12.80 +next
   12.81 +  assume "0 < a"
   12.82 +  with this have "0 + 0 < a + a"
   12.83 +    by (rule add_strict_mono)
   12.84 +  then show "0 < a + a" by simp
   12.85 +qed
   12.86 +
   12.87 +lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   12.88 +  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   12.89 +  by (auto simp add: le_less)
   12.90 +
   12.91 +lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   12.92 +  "a + a < 0 \<longleftrightarrow> a < 0"
   12.93 +proof -
   12.94 +  have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   12.95 +    by (simp add: not_less)
   12.96 +  then show ?thesis by simp
   12.97 +qed
   12.98 +
   12.99 +lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  12.100 +  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  12.101 +proof -
  12.102 +  have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  12.103 +    by (simp add: not_le)
  12.104 +  then show ?thesis by simp
  12.105 +qed
  12.106 +
  12.107 +lemma le_minus_self_iff:
  12.108 +  "a \<le> - a \<longleftrightarrow> a \<le> 0"
  12.109 +proof -
  12.110 +  from add_le_cancel_left [of "- a" "a + a" 0]
  12.111 +  have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  12.112 +    by (simp add: add_assoc [symmetric])
  12.113 +  thus ?thesis by simp
  12.114 +qed
  12.115 +
  12.116 +lemma minus_le_self_iff:
  12.117 +  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  12.118 +proof -
  12.119 +  from add_le_cancel_left [of "- a" 0 "a + a"]
  12.120 +  have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  12.121 +    by (simp add: add_assoc [symmetric])
  12.122 +  thus ?thesis by simp
  12.123 +qed
  12.124 +
  12.125 +lemma minus_max_eq_min:
  12.126 +  "- max x y = min (-x) (-y)"
  12.127 +  by (auto simp add: max_def min_def)
  12.128 +
  12.129 +lemma minus_min_eq_max:
  12.130 +  "- min x y = max (-x) (-y)"
  12.131 +  by (auto simp add: max_def min_def)
  12.132  
  12.133  end
  12.134  
  12.135 @@ -941,375 +1032,6 @@
  12.136  
  12.137  end
  12.138  
  12.139 -
  12.140 -subsection {* Lattice Ordered (Abelian) Groups *}
  12.141 -
  12.142 -class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
  12.143 -begin
  12.144 -
  12.145 -lemma add_inf_distrib_left:
  12.146 -  "a + inf b c = inf (a + b) (a + c)"
  12.147 -apply (rule antisym)
  12.148 -apply (simp_all add: le_infI)
  12.149 -apply (rule add_le_imp_le_left [of "uminus a"])
  12.150 -apply (simp only: add_assoc [symmetric], simp)
  12.151 -apply rule
  12.152 -apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
  12.153 -done
  12.154 -
  12.155 -lemma add_inf_distrib_right:
  12.156 -  "inf a b + c = inf (a + c) (b + c)"
  12.157 -proof -
  12.158 -  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
  12.159 -  thus ?thesis by (simp add: add_commute)
  12.160 -qed
  12.161 -
  12.162 -end
  12.163 -
  12.164 -class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup
  12.165 -begin
  12.166 -
  12.167 -lemma add_sup_distrib_left:
  12.168 -  "a + sup b c = sup (a + b) (a + c)" 
  12.169 -apply (rule antisym)
  12.170 -apply (rule add_le_imp_le_left [of "uminus a"])
  12.171 -apply (simp only: add_assoc[symmetric], simp)
  12.172 -apply rule
  12.173 -apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
  12.174 -apply (rule le_supI)
  12.175 -apply (simp_all)
  12.176 -done
  12.177 -
  12.178 -lemma add_sup_distrib_right:
  12.179 -  "sup a b + c = sup (a+c) (b+c)"
  12.180 -proof -
  12.181 -  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
  12.182 -  thus ?thesis by (simp add: add_commute)
  12.183 -qed
  12.184 -
  12.185 -end
  12.186 -
  12.187 -class lattice_ab_group_add = ordered_ab_group_add + lattice
  12.188 -begin
  12.189 -
  12.190 -subclass semilattice_inf_ab_group_add ..
  12.191 -subclass semilattice_sup_ab_group_add ..
  12.192 -
  12.193 -lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
  12.194 -
  12.195 -lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
  12.196 -proof (rule inf_unique)
  12.197 -  fix a b :: 'a
  12.198 -  show "- sup (-a) (-b) \<le> a"
  12.199 -    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
  12.200 -      (simp, simp add: add_sup_distrib_left)
  12.201 -next
  12.202 -  fix a b :: 'a
  12.203 -  show "- sup (-a) (-b) \<le> b"
  12.204 -    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
  12.205 -      (simp, simp add: add_sup_distrib_left)
  12.206 -next
  12.207 -  fix a b c :: 'a
  12.208 -  assume "a \<le> b" "a \<le> c"
  12.209 -  then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
  12.210 -    (simp add: le_supI)
  12.211 -qed
  12.212 -  
  12.213 -lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
  12.214 -proof (rule sup_unique)
  12.215 -  fix a b :: 'a
  12.216 -  show "a \<le> - inf (-a) (-b)"
  12.217 -    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
  12.218 -      (simp, simp add: add_inf_distrib_left)
  12.219 -next
  12.220 -  fix a b :: 'a
  12.221 -  show "b \<le> - inf (-a) (-b)"
  12.222 -    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
  12.223 -      (simp, simp add: add_inf_distrib_left)
  12.224 -next
  12.225 -  fix a b c :: 'a
  12.226 -  assume "a \<le> c" "b \<le> c"
  12.227 -  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
  12.228 -    (simp add: le_infI)
  12.229 -qed
  12.230 -
  12.231 -lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
  12.232 -by (simp add: inf_eq_neg_sup)
  12.233 -
  12.234 -lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
  12.235 -by (simp add: sup_eq_neg_inf)
  12.236 -
  12.237 -lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
  12.238 -proof -
  12.239 -  have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
  12.240 -  hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
  12.241 -  hence "0 = (-a + sup a b) + (inf a b + (-b))"
  12.242 -    by (simp add: add_sup_distrib_left add_inf_distrib_right)
  12.243 -       (simp add: algebra_simps)
  12.244 -  thus ?thesis by (simp add: algebra_simps)
  12.245 -qed
  12.246 -
  12.247 -subsection {* Positive Part, Negative Part, Absolute Value *}
  12.248 -
  12.249 -definition
  12.250 -  nprt :: "'a \<Rightarrow> 'a" where
  12.251 -  "nprt x = inf x 0"
  12.252 -
  12.253 -definition
  12.254 -  pprt :: "'a \<Rightarrow> 'a" where
  12.255 -  "pprt x = sup x 0"
  12.256 -
  12.257 -lemma pprt_neg: "pprt (- x) = - nprt x"
  12.258 -proof -
  12.259 -  have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
  12.260 -  also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
  12.261 -  finally have "sup (- x) 0 = - inf x 0" .
  12.262 -  then show ?thesis unfolding pprt_def nprt_def .
  12.263 -qed
  12.264 -
  12.265 -lemma nprt_neg: "nprt (- x) = - pprt x"
  12.266 -proof -
  12.267 -  from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
  12.268 -  then have "pprt x = - nprt (- x)" by simp
  12.269 -  then show ?thesis by simp
  12.270 -qed
  12.271 -
  12.272 -lemma prts: "a = pprt a + nprt a"
  12.273 -by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
  12.274 -
  12.275 -lemma zero_le_pprt[simp]: "0 \<le> pprt a"
  12.276 -by (simp add: pprt_def)
  12.277 -
  12.278 -lemma nprt_le_zero[simp]: "nprt a \<le> 0"
  12.279 -by (simp add: nprt_def)
  12.280 -
  12.281 -lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
  12.282 -proof -
  12.283 -  have a: "?l \<longrightarrow> ?r"
  12.284 -    apply (auto)
  12.285 -    apply (rule add_le_imp_le_right[of _ "uminus b" _])
  12.286 -    apply (simp add: add_assoc)
  12.287 -    done
  12.288 -  have b: "?r \<longrightarrow> ?l"
  12.289 -    apply (auto)
  12.290 -    apply (rule add_le_imp_le_right[of _ "b" _])
  12.291 -    apply (simp)
  12.292 -    done
  12.293 -  from a b show ?thesis by blast
  12.294 -qed
  12.295 -
  12.296 -lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
  12.297 -lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
  12.298 -
  12.299 -lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
  12.300 -  by (simp add: pprt_def sup_aci sup_absorb1)
  12.301 -
  12.302 -lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
  12.303 -  by (simp add: nprt_def inf_aci inf_absorb1)
  12.304 -
  12.305 -lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
  12.306 -  by (simp add: pprt_def sup_aci sup_absorb2)
  12.307 -
  12.308 -lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
  12.309 -  by (simp add: nprt_def inf_aci inf_absorb2)
  12.310 -
  12.311 -lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
  12.312 -proof -
  12.313 -  {
  12.314 -    fix a::'a
  12.315 -    assume hyp: "sup a (-a) = 0"
  12.316 -    hence "sup a (-a) + a = a" by (simp)
  12.317 -    hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) 
  12.318 -    hence "sup (a+a) 0 <= a" by (simp)
  12.319 -    hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
  12.320 -  }
  12.321 -  note p = this
  12.322 -  assume hyp:"sup a (-a) = 0"
  12.323 -  hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
  12.324 -  from p[OF hyp] p[OF hyp2] show "a = 0" by simp
  12.325 -qed
  12.326 -
  12.327 -lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
  12.328 -apply (simp add: inf_eq_neg_sup)
  12.329 -apply (simp add: sup_commute)
  12.330 -apply (erule sup_0_imp_0)
  12.331 -done
  12.332 -
  12.333 -lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
  12.334 -by (rule, erule inf_0_imp_0) simp
  12.335 -
  12.336 -lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
  12.337 -by (rule, erule sup_0_imp_0) simp
  12.338 -
  12.339 -lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  12.340 -  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  12.341 -proof
  12.342 -  assume "0 <= a + a"
  12.343 -  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
  12.344 -  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
  12.345 -    by (simp add: add_sup_inf_distribs inf_aci)
  12.346 -  hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
  12.347 -  hence "inf a 0 = 0" by (simp only: add_right_cancel)
  12.348 -  then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
  12.349 -next
  12.350 -  assume a: "0 <= a"
  12.351 -  show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
  12.352 -qed
  12.353 -
  12.354 -lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0"
  12.355 -proof
  12.356 -  assume assm: "a + a = 0"
  12.357 -  then have "a + a + - a = - a" by simp
  12.358 -  then have "a + (a + - a) = - a" by (simp only: add_assoc)
  12.359 -  then have a: "- a = a" by simp
  12.360 -  show "a = 0" apply (rule antisym)
  12.361 -  apply (unfold neg_le_iff_le [symmetric, of a])
  12.362 -  unfolding a apply simp
  12.363 -  unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
  12.364 -  unfolding assm unfolding le_less apply simp_all done
  12.365 -next
  12.366 -  assume "a = 0" then show "a + a = 0" by simp
  12.367 -qed
  12.368 -
  12.369 -lemma zero_less_double_add_iff_zero_less_single_add:
  12.370 -  "0 < a + a \<longleftrightarrow> 0 < a"
  12.371 -proof (cases "a = 0")
  12.372 -  case True then show ?thesis by auto
  12.373 -next
  12.374 -  case False then show ?thesis (*FIXME tune proof*)
  12.375 -  unfolding less_le apply simp apply rule
  12.376 -  apply clarify
  12.377 -  apply rule
  12.378 -  apply assumption
  12.379 -  apply (rule notI)
  12.380 -  unfolding double_zero [symmetric, of a] apply simp
  12.381 -  done
  12.382 -qed
  12.383 -
  12.384 -lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  12.385 -  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  12.386 -proof -
  12.387 -  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
  12.388 -  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
  12.389 -  ultimately show ?thesis by blast
  12.390 -qed
  12.391 -
  12.392 -lemma double_add_less_zero_iff_single_less_zero [simp]:
  12.393 -  "a + a < 0 \<longleftrightarrow> a < 0"
  12.394 -proof -
  12.395 -  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
  12.396 -  moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
  12.397 -  ultimately show ?thesis by blast
  12.398 -qed
  12.399 -
  12.400 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
  12.401 -
  12.402 -lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
  12.403 -proof -
  12.404 -  from add_le_cancel_left [of "uminus a" "plus a a" zero]
  12.405 -  have "(a <= -a) = (a+a <= 0)" 
  12.406 -    by (simp add: add_assoc[symmetric])
  12.407 -  thus ?thesis by simp
  12.408 -qed
  12.409 -
  12.410 -lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  12.411 -proof -
  12.412 -  from add_le_cancel_left [of "uminus a" zero "plus a a"]
  12.413 -  have "(-a <= a) = (0 <= a+a)" 
  12.414 -    by (simp add: add_assoc[symmetric])
  12.415 -  thus ?thesis by simp
  12.416 -qed
  12.417 -
  12.418 -lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
  12.419 -unfolding le_iff_inf by (simp add: nprt_def inf_commute)
  12.420 -
  12.421 -lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
  12.422 -unfolding le_iff_sup by (simp add: pprt_def sup_commute)
  12.423 -
  12.424 -lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
  12.425 -unfolding le_iff_sup by (simp add: pprt_def sup_commute)
  12.426 -
  12.427 -lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
  12.428 -unfolding le_iff_inf by (simp add: nprt_def inf_commute)
  12.429 -
  12.430 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
  12.431 -unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
  12.432 -
  12.433 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
  12.434 -unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
  12.435 -
  12.436 -end
  12.437 -
  12.438 -lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
  12.439 -
  12.440 -
  12.441 -class lattice_ab_group_add_abs = lattice_ab_group_add + abs +
  12.442 -  assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
  12.443 -begin
  12.444 -
  12.445 -lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
  12.446 -proof -
  12.447 -  have "0 \<le> \<bar>a\<bar>"
  12.448 -  proof -
  12.449 -    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
  12.450 -    show ?thesis by (rule add_mono [OF a b, simplified])
  12.451 -  qed
  12.452 -  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
  12.453 -  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
  12.454 -  then show ?thesis
  12.455 -    by (simp add: add_sup_inf_distribs sup_aci
  12.456 -      pprt_def nprt_def diff_minus abs_lattice)
  12.457 -qed
  12.458 -
  12.459 -subclass ordered_ab_group_add_abs
  12.460 -proof
  12.461 -  have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
  12.462 -  proof -
  12.463 -    fix a b
  12.464 -    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
  12.465 -    show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified])
  12.466 -  qed
  12.467 -  have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  12.468 -    by (simp add: abs_lattice le_supI)
  12.469 -  fix a b
  12.470 -  show "0 \<le> \<bar>a\<bar>" by simp
  12.471 -  show "a \<le> \<bar>a\<bar>"
  12.472 -    by (auto simp add: abs_lattice)
  12.473 -  show "\<bar>-a\<bar> = \<bar>a\<bar>"
  12.474 -    by (simp add: abs_lattice sup_commute)
  12.475 -  show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI)
  12.476 -  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  12.477 -  proof -
  12.478 -    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
  12.479 -      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
  12.480 -    have a:"a+b <= sup ?m ?n" by (simp)
  12.481 -    have b:"-a-b <= ?n" by (simp) 
  12.482 -    have c:"?n <= sup ?m ?n" by (simp)
  12.483 -    from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
  12.484 -    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
  12.485 -    from a d e have "abs(a+b) <= sup ?m ?n" 
  12.486 -      by (drule_tac abs_leI, auto)
  12.487 -    with g[symmetric] show ?thesis by simp
  12.488 -  qed
  12.489 -qed
  12.490 -
  12.491 -end
  12.492 -
  12.493 -lemma sup_eq_if:
  12.494 -  fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}"
  12.495 -  shows "sup a (- a) = (if a < 0 then - a else a)"
  12.496 -proof -
  12.497 -  note add_le_cancel_right [of a a "- a", symmetric, simplified]
  12.498 -  moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
  12.499 -  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
  12.500 -qed
  12.501 -
  12.502 -lemma abs_if_lattice:
  12.503 -  fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}"
  12.504 -  shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
  12.505 -by auto
  12.506 -
  12.507 -
  12.508  text {* Needed for abelian cancellation simprocs: *}
  12.509  
  12.510  lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
  12.511 @@ -1346,14 +1068,6 @@
  12.512    apply (simp_all add: prems)
  12.513    done
  12.514  
  12.515 -lemma estimate_by_abs:
  12.516 -  "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
  12.517 -proof -
  12.518 -  assume "a+b <= c"
  12.519 -  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
  12.520 -  have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
  12.521 -  show ?thesis by (rule le_add_right_mono[OF 2 3])
  12.522 -qed
  12.523  
  12.524  subsection {* Tools setup *}
  12.525  
    13.1 --- a/src/HOL/RealDef.thy	Mon Feb 08 14:04:51 2010 +0100
    13.2 +++ b/src/HOL/RealDef.thy	Mon Feb 08 14:08:32 2010 +0100
    13.3 @@ -426,8 +426,6 @@
    13.4      by (simp only: real_sgn_def)
    13.5  qed
    13.6  
    13.7 -instance real :: lattice_ab_group_add ..
    13.8 -
    13.9  text{*The function @{term real_of_preal} requires many proofs, but it seems
   13.10  to be essential for proving completeness of the reals from that of the
   13.11  positive reals.*}
   13.12 @@ -1046,13 +1044,6 @@
   13.13  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
   13.14  by simp
   13.15  
   13.16 -instance real :: lattice_ring
   13.17 -proof
   13.18 -  fix a::real
   13.19 -  show "abs a = sup a (-a)"
   13.20 -    by (auto simp add: real_abs_def sup_real_def)
   13.21 -qed
   13.22 -
   13.23  
   13.24  subsection {* Implementation of rational real numbers *}
   13.25  
    14.1 --- a/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:04:51 2010 +0100
    14.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:08:32 2010 +0100
    14.3 @@ -2143,100 +2143,6 @@
    14.4    assumes abs_eq_mult:
    14.5      "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
    14.6  
    14.7 -
    14.8 -class lattice_ring = ordered_ring + lattice_ab_group_add_abs
    14.9 -begin
   14.10 -
   14.11 -subclass semilattice_inf_ab_group_add ..
   14.12 -subclass semilattice_sup_ab_group_add ..
   14.13 -
   14.14 -end
   14.15 -
   14.16 -lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))" 
   14.17 -proof -
   14.18 -  let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
   14.19 -  let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   14.20 -  have a: "(abs a) * (abs b) = ?x"
   14.21 -    by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
   14.22 -  {
   14.23 -    fix u v :: 'a
   14.24 -    have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
   14.25 -              u * v = pprt a * pprt b + pprt a * nprt b + 
   14.26 -                      nprt a * pprt b + nprt a * nprt b"
   14.27 -      apply (subst prts[of u], subst prts[of v])
   14.28 -      apply (simp add: algebra_simps) 
   14.29 -      done
   14.30 -  }
   14.31 -  note b = this[OF refl[of a] refl[of b]]
   14.32 -  note addm = add_mono[of "0::'a" _ "0::'a", simplified]
   14.33 -  note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
   14.34 -  have xy: "- ?x <= ?y"
   14.35 -    apply (simp)
   14.36 -    apply (rule_tac y="0::'a" in order_trans)
   14.37 -    apply (rule addm2)
   14.38 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
   14.39 -    apply (rule addm)
   14.40 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
   14.41 -    done
   14.42 -  have yx: "?y <= ?x"
   14.43 -    apply (simp add:diff_def)
   14.44 -    apply (rule_tac y=0 in order_trans)
   14.45 -    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
   14.46 -    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
   14.47 -    done
   14.48 -  have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   14.49 -  have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
   14.50 -  show ?thesis
   14.51 -    apply (rule abs_leI)
   14.52 -    apply (simp add: i1)
   14.53 -    apply (simp add: i2[simplified minus_le_iff])
   14.54 -    done
   14.55 -qed
   14.56 -
   14.57 -instance lattice_ring \<subseteq> ordered_ring_abs
   14.58 -proof
   14.59 -  fix a b :: "'a\<Colon> lattice_ring"
   14.60 -  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   14.61 -  show "abs (a*b) = abs a * abs b"
   14.62 -proof -
   14.63 -  have s: "(0 <= a*b) | (a*b <= 0)"
   14.64 -    apply (auto)    
   14.65 -    apply (rule_tac split_mult_pos_le)
   14.66 -    apply (rule_tac contrapos_np[of "a*b <= 0"])
   14.67 -    apply (simp)
   14.68 -    apply (rule_tac split_mult_neg_le)
   14.69 -    apply (insert prems)
   14.70 -    apply (blast)
   14.71 -    done
   14.72 -  have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
   14.73 -    by (simp add: prts[symmetric])
   14.74 -  show ?thesis
   14.75 -  proof cases
   14.76 -    assume "0 <= a * b"
   14.77 -    then show ?thesis
   14.78 -      apply (simp_all add: mulprts abs_prts)
   14.79 -      apply (insert prems)
   14.80 -      apply (auto simp add: 
   14.81 -        algebra_simps 
   14.82 -        iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
   14.83 -        iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
   14.84 -        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
   14.85 -        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
   14.86 -      done
   14.87 -  next
   14.88 -    assume "~(0 <= a*b)"
   14.89 -    with s have "a*b <= 0" by simp
   14.90 -    then show ?thesis
   14.91 -      apply (simp_all add: mulprts abs_prts)
   14.92 -      apply (insert prems)
   14.93 -      apply (auto simp add: algebra_simps)
   14.94 -      apply(drule (1) mult_nonneg_nonneg[of a b],simp)
   14.95 -      apply(drule (1) mult_nonpos_nonpos[of a b],simp)
   14.96 -      done
   14.97 -  qed
   14.98 -qed
   14.99 -qed
  14.100 -
  14.101  context linordered_idom
  14.102  begin
  14.103  
  14.104 @@ -2308,76 +2214,6 @@
  14.105    apply (simp add: order_less_imp_le)
  14.106  done
  14.107  
  14.108 -
  14.109 -subsection {* Bounds of products via negative and positive Part *}
  14.110 -
  14.111 -lemma mult_le_prts:
  14.112 -  assumes
  14.113 -  "a1 <= (a::'a::lattice_ring)"
  14.114 -  "a <= a2"
  14.115 -  "b1 <= b"
  14.116 -  "b <= b2"
  14.117 -  shows
  14.118 -  "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  14.119 -proof - 
  14.120 -  have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  14.121 -    apply (subst prts[symmetric])+
  14.122 -    apply simp
  14.123 -    done
  14.124 -  then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  14.125 -    by (simp add: algebra_simps)
  14.126 -  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  14.127 -    by (simp_all add: prems mult_mono)
  14.128 -  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  14.129 -  proof -
  14.130 -    have "pprt a * nprt b <= pprt a * nprt b2"
  14.131 -      by (simp add: mult_left_mono prems)
  14.132 -    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  14.133 -      by (simp add: mult_right_mono_neg prems)
  14.134 -    ultimately show ?thesis
  14.135 -      by simp
  14.136 -  qed
  14.137 -  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  14.138 -  proof - 
  14.139 -    have "nprt a * pprt b <= nprt a2 * pprt b"
  14.140 -      by (simp add: mult_right_mono prems)
  14.141 -    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  14.142 -      by (simp add: mult_left_mono_neg prems)
  14.143 -    ultimately show ?thesis
  14.144 -      by simp
  14.145 -  qed
  14.146 -  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  14.147 -  proof -
  14.148 -    have "nprt a * nprt b <= nprt a * nprt b1"
  14.149 -      by (simp add: mult_left_mono_neg prems)
  14.150 -    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  14.151 -      by (simp add: mult_right_mono_neg prems)
  14.152 -    ultimately show ?thesis
  14.153 -      by simp
  14.154 -  qed
  14.155 -  ultimately show ?thesis
  14.156 -    by - (rule add_mono | simp)+
  14.157 -qed
  14.158 -
  14.159 -lemma mult_ge_prts:
  14.160 -  assumes
  14.161 -  "a1 <= (a::'a::lattice_ring)"
  14.162 -  "a <= a2"
  14.163 -  "b1 <= b"
  14.164 -  "b <= b2"
  14.165 -  shows
  14.166 -  "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  14.167 -proof - 
  14.168 -  from prems have a1:"- a2 <= -a" by auto
  14.169 -  from prems have a2: "-a <= -a1" by auto
  14.170 -  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  14.171 -  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  14.172 -  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  14.173 -    by (simp only: minus_le_iff)
  14.174 -  then show ?thesis by simp
  14.175 -qed
  14.176 -
  14.177 -
  14.178  code_modulename SML
  14.179    Ring_and_Field Arith
  14.180  
    15.1 --- a/src/HOL/SupInf.thy	Mon Feb 08 14:04:51 2010 +0100
    15.2 +++ b/src/HOL/SupInf.thy	Mon Feb 08 14:08:32 2010 +0100
    15.3 @@ -6,38 +6,6 @@
    15.4  imports RComplete
    15.5  begin
    15.6  
    15.7 -lemma minus_max_eq_min:
    15.8 -  fixes x :: "'a::{lattice_ab_group_add, linorder}"
    15.9 -  shows "- (max x y) = min (-x) (-y)"
   15.10 -by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
   15.11 -
   15.12 -lemma minus_min_eq_max:
   15.13 -  fixes x :: "'a::{lattice_ab_group_add, linorder}"
   15.14 -  shows "- (min x y) = max (-x) (-y)"
   15.15 -by (metis minus_max_eq_min minus_minus)
   15.16 -
   15.17 -lemma minus_Max_eq_Min [simp]:
   15.18 -  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
   15.19 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
   15.20 -proof (induct S rule: finite_ne_induct)
   15.21 -  case (singleton x)
   15.22 -  thus ?case by simp
   15.23 -next
   15.24 -  case (insert x S)
   15.25 -  thus ?case by (simp add: minus_max_eq_min) 
   15.26 -qed
   15.27 -
   15.28 -lemma minus_Min_eq_Max [simp]:
   15.29 -  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
   15.30 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
   15.31 -proof (induct S rule: finite_ne_induct)
   15.32 -  case (singleton x)
   15.33 -  thus ?case by simp
   15.34 -next
   15.35 -  case (insert x S)
   15.36 -  thus ?case by (simp add: minus_min_eq_max) 
   15.37 -qed
   15.38 -
   15.39  instantiation real :: Sup 
   15.40  begin
   15.41  definition
    16.1 --- a/src/HOL/Transcendental.thy	Mon Feb 08 14:04:51 2010 +0100
    16.2 +++ b/src/HOL/Transcendental.thy	Mon Feb 08 14:08:32 2010 +0100
    16.3 @@ -2904,10 +2904,12 @@
    16.4      next
    16.5        case False hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
    16.6        have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
    16.7 -        by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
    16.8 +        by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
    16.9 +          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
   16.10        moreover
   16.11        have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
   16.12 -        by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
   16.13 +        by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
   16.14 +          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
   16.15        ultimately 
   16.16        show ?thesis using suminf_arctan_zero by auto
   16.17      qed