1 (* Title: HOL/Matrix/LP.thy |
|
2 Author: Steven Obua |
|
3 *) |
|
4 |
|
5 theory LP |
|
6 imports Main "~~/src/HOL/Library/Lattice_Algebras" |
|
7 begin |
|
8 |
|
9 lemma le_add_right_mono: |
|
10 assumes |
|
11 "a <= b + (c::'a::ordered_ab_group_add)" |
|
12 "c <= d" |
|
13 shows "a <= b + d" |
|
14 apply (rule_tac order_trans[where y = "b+c"]) |
|
15 apply (simp_all add: assms) |
|
16 done |
|
17 |
|
18 lemma linprog_dual_estimate: |
|
19 assumes |
|
20 "A * x \<le> (b::'a::lattice_ring)" |
|
21 "0 \<le> y" |
|
22 "abs (A - A') \<le> \<delta>A" |
|
23 "b \<le> b'" |
|
24 "abs (c - c') \<le> \<delta>c" |
|
25 "abs x \<le> r" |
|
26 shows |
|
27 "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r" |
|
28 proof - |
|
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) |
|
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 |
|
33 have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)" |
|
34 by (simp only: 4 estimate_by_abs) |
|
35 have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x" |
|
36 by (simp add: abs_le_mult) |
|
37 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" |
|
38 by(rule abs_triangle_ineq [THEN mult_right_mono]) simp |
|
39 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" |
|
40 by (simp add: abs_triangle_ineq mult_right_mono) |
|
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) |
|
43 have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) |
|
44 have 11: "abs (c'-c) = abs (c-c')" |
|
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" |
|
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" |
|
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" |
|
51 apply (rule mult_left_mono) |
|
52 apply (simp add: assms) |
|
53 apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+ |
|
54 apply (rule mult_left_mono[of "0" "\<delta>A", simplified]) |
|
55 apply (simp_all) |
|
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) |
|
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" |
|
60 by (simp) |
|
61 show ?thesis |
|
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]]) |
|
64 done |
|
65 qed |
|
66 |
|
67 lemma le_ge_imp_abs_diff_1: |
|
68 assumes |
|
69 "A1 <= (A::'a::lattice_ring)" |
|
70 "A <= A2" |
|
71 shows "abs (A-A1) <= A2-A1" |
|
72 proof - |
|
73 have "0 <= A - A1" |
|
74 proof - |
|
75 have 1: "A - A1 = A + (- A1)" by simp |
|
76 show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms]) |
|
77 qed |
|
78 then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg) |
|
79 with assms show "abs (A-A1) <= (A2-A1)" by simp |
|
80 qed |
|
81 |
|
82 lemma mult_le_prts: |
|
83 assumes |
|
84 "a1 <= (a::'a::lattice_ring)" |
|
85 "a <= a2" |
|
86 "b1 <= b" |
|
87 "b <= b2" |
|
88 shows |
|
89 "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" |
|
90 proof - |
|
91 have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" |
|
92 apply (subst prts[symmetric])+ |
|
93 apply simp |
|
94 done |
|
95 then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" |
|
96 by (simp add: algebra_simps) |
|
97 moreover have "pprt a * pprt b <= pprt a2 * pprt b2" |
|
98 by (simp_all add: assms mult_mono) |
|
99 moreover have "pprt a * nprt b <= pprt a1 * nprt b2" |
|
100 proof - |
|
101 have "pprt a * nprt b <= pprt a * nprt b2" |
|
102 by (simp add: mult_left_mono assms) |
|
103 moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2" |
|
104 by (simp add: mult_right_mono_neg assms) |
|
105 ultimately show ?thesis |
|
106 by simp |
|
107 qed |
|
108 moreover have "nprt a * pprt b <= nprt a2 * pprt b1" |
|
109 proof - |
|
110 have "nprt a * pprt b <= nprt a2 * pprt b" |
|
111 by (simp add: mult_right_mono assms) |
|
112 moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" |
|
113 by (simp add: mult_left_mono_neg assms) |
|
114 ultimately show ?thesis |
|
115 by simp |
|
116 qed |
|
117 moreover have "nprt a * nprt b <= nprt a1 * nprt b1" |
|
118 proof - |
|
119 have "nprt a * nprt b <= nprt a * nprt b1" |
|
120 by (simp add: mult_left_mono_neg assms) |
|
121 moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1" |
|
122 by (simp add: mult_right_mono_neg assms) |
|
123 ultimately show ?thesis |
|
124 by simp |
|
125 qed |
|
126 ultimately show ?thesis |
|
127 by - (rule add_mono | simp)+ |
|
128 qed |
|
129 |
|
130 lemma mult_le_dual_prts: |
|
131 assumes |
|
132 "A * x \<le> (b::'a::lattice_ring)" |
|
133 "0 \<le> y" |
|
134 "A1 \<le> A" |
|
135 "A \<le> A2" |
|
136 "c1 \<le> c" |
|
137 "c \<le> c2" |
|
138 "r1 \<le> x" |
|
139 "x \<le> r2" |
|
140 shows |
|
141 "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)" |
|
142 (is "_ <= _ + ?C") |
|
143 proof - |
|
144 from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) |
|
145 moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps) |
|
146 ultimately have "c * x + (y * A - c) * x <= y * b" by simp |
|
147 then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq) |
|
148 then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps) |
|
149 have s2: "c - y * A <= c2 - y * A1" |
|
150 by (simp add: diff_minus assms add_mono mult_left_mono) |
|
151 have s1: "c1 - y * A2 <= c - y * A" |
|
152 by (simp add: diff_minus assms add_mono mult_left_mono) |
|
153 have prts: "(c - y * A) * x <= ?C" |
|
154 apply (simp add: Let_def) |
|
155 apply (rule mult_le_prts) |
|
156 apply (simp_all add: assms s1 s2) |
|
157 done |
|
158 then have "y * b + (c - y * A) * x <= y * b + ?C" |
|
159 by simp |
|
160 with cx show ?thesis |
|
161 by(simp only:) |
|
162 qed |
|
163 |
|
164 end |
|