src/HOL/Ring_and_Field.thy
changeset 15178 5f621aa35c25
parent 15140 322485b816ac
child 15197 19e735596e51
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Sep 03 10:27:05 2004 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Sep 03 17:10:36 2004 +0200
     1.3 @@ -546,14 +546,14 @@
     1.4  done
     1.5  
     1.6  text{*This list of rewrites decides ring equalities by ordered rewriting.*}
     1.7 -lemmas ring_eq_simps =
     1.8 -  mult_ac
     1.9 +lemmas ring_eq_simps =  
    1.10 +(*  mult_ac*)
    1.11    left_distrib right_distrib left_diff_distrib right_diff_distrib
    1.12 -  add_ac
    1.13 +  group_eq_simps
    1.14 +(*  add_ac
    1.15    add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    1.16 -  diff_eq_eq eq_diff_eq
    1.17 +  diff_eq_eq eq_diff_eq *)
    1.18      
    1.19 -
    1.20  subsection {* Fields *}
    1.21  
    1.22  lemma right_inverse [simp]:
    1.23 @@ -1503,6 +1503,90 @@
    1.24  text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
    1.25  declare times_divide_eq_left [simp]
    1.26  
    1.27 +lemma linprog_dual_estimate:
    1.28 +  assumes
    1.29 +  "A * x \<le> (b::'a::lordered_ring)"
    1.30 +  "0 \<le> y"
    1.31 +  "abs (A - A') \<le> \<delta>A"
    1.32 +  "b \<le> b'"
    1.33 +  "abs (c - c') \<le> \<delta>c"
    1.34 +  "abs x \<le> r"
    1.35 +  shows
    1.36 +  "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
    1.37 +proof -
    1.38 +  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    1.39 +  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    1.40 +  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_eq_simps)  
    1.41 +  from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
    1.42 +  have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
    1.43 +    by (simp only: 4 estimate_by_abs)  
    1.44 +  have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
    1.45 +    by (simp add: abs_le_mult)
    1.46 +  have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
    1.47 +    by (simp add: abs_triangle_ineq mult_right_mono)
    1.48 +  have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <=  (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
    1.49 +    by (simp add: abs_triangle_ineq mult_right_mono)    
    1.50 +  have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
    1.51 +    by (simp add: abs_le_mult mult_right_mono)  
    1.52 +  have 10: "c'-c = -(c-c')" by (simp add: ring_eq_simps)
    1.53 +  have 11: "abs (c'-c) = abs (c-c')" 
    1.54 +    by (subst 10, subst abs_minus_cancel, simp)
    1.55 +  have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
    1.56 +    by (simp add: 11 prems mult_right_mono)
    1.57 +  have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x"
    1.58 +    by (simp add: prems mult_right_mono mult_left_mono)  
    1.59 +  have r: "(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x <=  (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
    1.60 +    apply (rule mult_left_mono)
    1.61 +    apply (simp add: prems)
    1.62 +    apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    1.63 +    apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    1.64 +    apply (simp_all)
    1.65 +    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
    1.66 +    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
    1.67 +    done    
    1.68 +  from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
    1.69 +    by (simp)
    1.70 +  show ?thesis 
    1.71 +    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    1.72 +    apply (simp_all add: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
    1.73 +    done
    1.74 +qed
    1.75 +
    1.76 +lemma le_ge_imp_abs_diff_1:
    1.77 +  assumes
    1.78 +  "A1 <= (A::'a::lordered_ring)"
    1.79 +  "A <= A2" 
    1.80 +  shows "abs (A-A1) <= A2-A1"
    1.81 +proof -
    1.82 +  have "0 <= A - A1"    
    1.83 +  proof -
    1.84 +    have 1: "A - A1 = A + (- A1)" by simp
    1.85 +    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
    1.86 +  qed
    1.87 +  then have "abs (A-A1) = A-A1" by (rule abs_of_ge_0)
    1.88 +  with prems show "abs (A-A1) <= (A2-A1)" by simp
    1.89 +qed
    1.90 +
    1.91 +lemma linprog_dual_estimate_1:
    1.92 +  assumes
    1.93 +  "A * x \<le> (b::'a::lordered_ring)"
    1.94 +  "0 \<le> y"
    1.95 +  "A1 <= A"
    1.96 +  "A <= A2"
    1.97 +  "c1 <= c"
    1.98 +  "c <= c2"
    1.99 +  "abs x \<le> r"
   1.100 +  shows
   1.101 +  "c * x \<le> y * b + (y * (A2 - A1) + abs (y * A1 - c1) + (c2 - c1)) * r"
   1.102 +proof -
   1.103 +  from prems have delta_A: "abs (A-A1) <= (A2-A1)" by (simp add: le_ge_imp_abs_diff_1)
   1.104 +  from prems have delta_c: "abs (c-c1) <= (c2-c1)" by (simp add: le_ge_imp_abs_diff_1)
   1.105 +  show ?thesis
   1.106 +    apply (rule_tac linprog_dual_estimate)
   1.107 +    apply (auto intro: delta_A delta_c simp add: prems)
   1.108 +    done
   1.109 +qed
   1.110 +
   1.111  ML {*
   1.112  val left_distrib = thm "left_distrib";
   1.113  val right_distrib = thm "right_distrib";