src/HOL/Ring_and_Field.thy
 changeset 15580 900291ee0af8 parent 15481 fc075ae929e4 child 15769 38c8ea8521e7
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Mar 07 16:55:36 2005 +0100
1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Mar 07 18:19:55 2005 +0100
1.3 @@ -1532,12 +1532,6 @@
1.4  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
1.5    by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
1.6
1.7 -lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
1.8 -by (simp add: abs_if linorder_not_less [symmetric])
1.9 -
1.10 -lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
1.11 -by (simp add: abs_if linorder_not_less [symmetric])
1.12 -
1.13  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
1.14  proof -
1.15    let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
1.16 @@ -1599,10 +1593,6 @@
1.17      assume "0 <= a * b"
1.18      then show ?thesis
1.19        apply (simp_all add: mulprts abs_prts)
1.21 -	iff2imp[OF zero_le_iff_zero_nprt]
1.22 -	iff2imp[OF le_zero_iff_pprt_id]
1.23 -      )
1.24        apply (insert prems)
1.26  	ring_eq_simps
1.27 @@ -1617,8 +1607,7 @@
1.28      then show ?thesis
1.29        apply (simp_all add: mulprts abs_prts)
1.30        apply (insert prems)
1.31 -      apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
1.32 -	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
1.33 +      apply (auto simp add: ring_eq_simps)
1.34        apply(drule (1) mult_pos_le[of a b],simp)
1.35        apply(drule (1) mult_neg_le[of a b],simp)
1.36        done
1.37 @@ -1740,24 +1729,86 @@
1.38    with prems show "abs (A-A1) <= (A2-A1)" by simp
1.39  qed
1.40
1.41 -lemma linprog_dual_estimate_1:
1.42 +lemma mult_le_prts:
1.43 +  assumes
1.44 +  "a1 <= (a::'a::lordered_ring)"
1.45 +  "a <= a2"
1.46 +  "b1 <= b"
1.47 +  "b <= b2"
1.48 +  shows
1.49 +  "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
1.50 +proof -
1.51 +  have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1.52 +    apply (subst prts[symmetric])+
1.53 +    apply simp
1.54 +    done
1.55 +  then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.56 +    by (simp add: ring_eq_simps)
1.57 +  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
1.58 +    by (simp_all add: prems mult_mono)
1.59 +  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
1.60 +  proof -
1.61 +    have "pprt a * nprt b <= pprt a * nprt b2"
1.62 +      by (simp add: mult_left_mono prems)
1.63 +    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
1.64 +      by (simp add: mult_right_mono_neg prems)
1.65 +    ultimately show ?thesis
1.66 +      by simp
1.67 +  qed
1.68 +  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
1.69 +  proof -
1.70 +    have "nprt a * pprt b <= nprt a2 * pprt b"
1.71 +      by (simp add: mult_right_mono prems)
1.72 +    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
1.73 +      by (simp add: mult_left_mono_neg prems)
1.74 +    ultimately show ?thesis
1.75 +      by simp
1.76 +  qed
1.77 +  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
1.78 +  proof -
1.79 +    have "nprt a * nprt b <= nprt a * nprt b1"
1.80 +      by (simp add: mult_left_mono_neg prems)
1.81 +    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
1.82 +      by (simp add: mult_right_mono_neg prems)
1.83 +    ultimately show ?thesis
1.84 +      by simp
1.85 +  qed
1.86 +  ultimately show ?thesis
1.87 +    by - (rule add_mono | simp)+
1.88 +qed
1.89 +
1.90 +lemma mult_le_dual_prts:
1.91    assumes
1.92    "A * x \<le> (b::'a::lordered_ring)"
1.93    "0 \<le> y"
1.94 -  "A1 <= A"
1.95 -  "A <= A2"
1.96 -  "c1 <= c"
1.97 -  "c <= c2"
1.98 -  "abs x \<le> r"
1.99 +  "A1 \<le> A"
1.100 +  "A \<le> A2"
1.101 +  "c1 \<le> c"
1.102 +  "c \<le> c2"
1.103 +  "r1 \<le> x"
1.104 +  "x \<le> r2"
1.105    shows
1.106 -  "c * x \<le> y * b + (y * (A2 - A1) + abs (y * A1 - c1) + (c2 - c1)) * r"
1.107 +  "c * x \<le> y * b + (let s1 = c1 - y * A2; s2 = c2 - y * A1 in pprt s2 * pprt r2 + pprt s1 * nprt r2 + nprt s2 * pprt r1 + nprt s1 * nprt r1)"
1.108 +  (is "_ <= _ + ?C")
1.109  proof -
1.110 -  from prems have delta_A: "abs (A-A1) <= (A2-A1)" by (simp add: le_ge_imp_abs_diff_1)
1.111 -  from prems have delta_c: "abs (c-c1) <= (c2-c1)" by (simp add: le_ge_imp_abs_diff_1)
1.112 -  show ?thesis
1.113 -    apply (rule_tac linprog_dual_estimate)
1.114 -    apply (auto intro: delta_A delta_c simp add: prems)
1.115 +  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono)
1.116 +  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_eq_simps)
1.117 +  ultimately have "c * x + (y * A - c) * x <= y * b" by simp
1.118 +  then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
1.119 +  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_eq_simps)
1.120 +  have s2: "c - y * A <= c2 - y * A1"
1.122 +  have s1: "c1 - y * A2 <= c - y * A"