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.20 -      apply (simp add: 
    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.25        apply (auto simp add: 
    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.121 +    by (simp add: diff_def prems add_mono mult_left_mono)
   1.122 +  have s1: "c1 - y * A2 <= c - y * A"
   1.123 +    by (simp add: diff_def prems add_mono mult_left_mono)
   1.124 +  have prts: "(c - y * A) * x <= ?C"
   1.125 +    apply (simp add: Let_def)
   1.126 +    apply (rule mult_le_prts)
   1.127 +    apply (simp_all add: prems s1 s2)
   1.128      done
   1.129 +  then have "y * b + (c - y * A) * x <= y * b + ?C"
   1.130 +    by simp
   1.131 +  with cx show ?thesis
   1.132 +    by(simp only:)
   1.133  qed
   1.134  
   1.135  ML {*