17 |
17 |
18 lemma linprog_dual_estimate: |
18 lemma linprog_dual_estimate: |
19 assumes |
19 assumes |
20 "A * x \<le> (b::'a::lattice_ring)" |
20 "A * x \<le> (b::'a::lattice_ring)" |
21 "0 \<le> y" |
21 "0 \<le> y" |
22 "abs (A - A') \<le> \<delta>A" |
22 "abs (A - A') \<le> \<delta>_A" |
23 "b \<le> b'" |
23 "b \<le> b'" |
24 "abs (c - c') \<le> \<delta>c" |
24 "abs (c - c') \<le> \<delta>_c" |
25 "abs x \<le> r" |
25 "abs x \<le> r" |
26 shows |
26 shows |
27 "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r" |
27 "c * x \<le> y * b' + (y * \<delta>_A + abs (y * A' - c') + \<delta>_c) * r" |
28 proof - |
28 proof - |
29 from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono) |
29 from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono) |
30 from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) |
30 from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) |
31 have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps) |
31 have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps) |
32 from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp |
32 from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp |
41 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" |
41 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" |
42 by (simp add: abs_le_mult mult_right_mono) |
42 by (simp add: abs_le_mult mult_right_mono) |
43 have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) |
43 have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) |
44 have 11: "abs (c'-c) = abs (c-c')" |
44 have 11: "abs (c'-c) = abs (c-c')" |
45 by (subst 10, subst abs_minus_cancel, simp) |
45 by (subst 10, subst abs_minus_cancel, simp) |
46 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" |
46 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" |
47 by (simp add: 11 assms mult_right_mono) |
47 by (simp add: 11 assms mult_right_mono) |
48 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" |
48 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" |
49 by (simp add: assms mult_right_mono mult_left_mono) |
49 by (simp add: assms mult_right_mono mult_left_mono) |
50 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" |
50 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" |
51 apply (rule mult_left_mono) |
51 apply (rule mult_left_mono) |
52 apply (simp add: assms) |
52 apply (simp add: assms) |
53 apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+ |
53 apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+ |
54 apply (rule mult_left_mono[of "0" "\<delta>A", simplified]) |
54 apply (rule mult_left_mono[of "0" "\<delta>_A", simplified]) |
55 apply (simp_all) |
55 apply (simp_all) |
56 apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms) |
56 apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms) |
57 apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms) |
57 apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms) |
58 done |
58 done |
59 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" |
59 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" |
60 by (simp) |
60 by (simp) |
61 show ?thesis |
61 show ?thesis |
62 apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"]) |
62 apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"]) |
63 apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]]) |
63 apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]]) |
64 done |
64 done |