author | wenzelm |
Wed, 26 Oct 2016 15:14:17 +0200 | |
changeset 64406 | 492de9062cd2 |
parent 62390 | 842917225d56 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
47455 | 1 |
(* Title: HOL/Matrix_LP/LP.thy |
19453 | 2 |
Author: Steven Obua |
3 |
*) |
|
4 |
||
5 |
theory LP |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
37884
diff
changeset
|
6 |
imports Main "~~/src/HOL/Library/Lattice_Algebras" |
19453 | 7 |
begin |
8 |
||
37884
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
9 |
lemma le_add_right_mono: |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
10 |
assumes |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
11 |
"a <= b + (c::'a::ordered_ab_group_add)" |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
12 |
"c <= d" |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
13 |
shows "a <= b + d" |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
14 |
apply (rule_tac order_trans[where y = "b+c"]) |
41550 | 15 |
apply (simp_all add: assms) |
37884
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
16 |
done |
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
17 |
|
19453 | 18 |
lemma linprog_dual_estimate: |
19 |
assumes |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
20 |
"A * x \<le> (b::'a::lattice_ring)" |
19453 | 21 |
"0 \<le> y" |
61945 | 22 |
"\<bar>A - A'\<bar> \<le> \<delta>_A" |
19453 | 23 |
"b \<le> b'" |
61945 | 24 |
"\<bar>c - c'\<bar> \<le> \<delta>_c" |
25 |
"\<bar>x\<bar> \<le> r" |
|
19453 | 26 |
shows |
61945 | 27 |
"c * x \<le> y * b' + (y * \<delta>_A + \<bar>y * A' - c'\<bar> + \<delta>_c) * r" |
19453 | 28 |
proof - |
41550 | 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) |
|
29667 | 31 |
have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps) |
19453 | 32 |
from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp |
61945 | 33 |
have 5: "c * x <= y * b' + \<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>" |
19453 | 34 |
by (simp only: 4 estimate_by_abs) |
61945 | 35 |
have 6: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= \<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar> * \<bar>x\<bar>" |
19453 | 36 |
by (simp add: abs_le_mult) |
61945 | 37 |
have 7: "(\<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>" |
19453 | 38 |
by(rule abs_triangle_ineq [THEN mult_right_mono]) simp |
61945 | 39 |
have 8: "(\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>" |
19453 | 40 |
by (simp add: abs_triangle_ineq mult_right_mono) |
61945 | 41 |
have 9: "(\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar>" |
19453 | 42 |
by (simp add: abs_le_mult mult_right_mono) |
29667 | 43 |
have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) |
61945 | 44 |
have 11: "\<bar>c'-c\<bar> = \<bar>c-c'\<bar>" |
19453 | 45 |
by (subst 10, subst abs_minus_cancel, simp) |
61945 | 46 |
have 12: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>" |
41550 | 47 |
by (simp add: 11 assms mult_right_mono) |
61945 | 48 |
have 13: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>" |
41550 | 49 |
by (simp add: assms mult_right_mono mult_left_mono) |
61945 | 50 |
have r: "(\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r" |
19453 | 51 |
apply (rule mult_left_mono) |
41550 | 52 |
apply (simp add: assms) |
19453 | 53 |
apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+ |
50252 | 54 |
apply (rule mult_left_mono[of "0" "\<delta>_A", simplified]) |
19453 | 55 |
apply (simp_all) |
61945 | 56 |
apply (rule order_trans[where y="\<bar>A-A'\<bar>"], simp_all add: assms) |
57 |
apply (rule order_trans[where y="\<bar>c-c'\<bar>"], simp_all add: assms) |
|
19453 | 58 |
done |
61945 | 59 |
from 6 7 8 9 12 13 r have 14: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r" |
19453 | 60 |
by (simp) |
37884
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
35032
diff
changeset
|
61 |
show ?thesis |
61945 | 62 |
apply (rule le_add_right_mono[of _ _ "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"]) |
41550 | 63 |
apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]]) |
19453 | 64 |
done |
65 |
qed |
|
66 |
||
67 |
lemma le_ge_imp_abs_diff_1: |
|
68 |
assumes |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
69 |
"A1 <= (A::'a::lattice_ring)" |
19453 | 70 |
"A <= A2" |
61945 | 71 |
shows "\<bar>A-A1\<bar> <= A2-A1" |
19453 | 72 |
proof - |
73 |
have "0 <= A - A1" |
|
74 |
proof - |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
50252
diff
changeset
|
75 |
from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp |
19453 | 76 |
qed |
61945 | 77 |
then have "\<bar>A-A1\<bar> = A-A1" by (rule abs_of_nonneg) |
78 |
with assms show "\<bar>A-A1\<bar> <= (A2-A1)" by simp |
|
19453 | 79 |
qed |
80 |
||
81 |
lemma mult_le_prts: |
|
82 |
assumes |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
83 |
"a1 <= (a::'a::lattice_ring)" |
19453 | 84 |
"a <= a2" |
85 |
"b1 <= b" |
|
86 |
"b <= b2" |
|
87 |
shows |
|
88 |
"a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" |
|
89 |
proof - |
|
90 |
have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" |
|
91 |
apply (subst prts[symmetric])+ |
|
92 |
apply simp |
|
93 |
done |
|
94 |
then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" |
|
29667 | 95 |
by (simp add: algebra_simps) |
19453 | 96 |
moreover have "pprt a * pprt b <= pprt a2 * pprt b2" |
41550 | 97 |
by (simp_all add: assms mult_mono) |
19453 | 98 |
moreover have "pprt a * nprt b <= pprt a1 * nprt b2" |
99 |
proof - |
|
100 |
have "pprt a * nprt b <= pprt a * nprt b2" |
|
41550 | 101 |
by (simp add: mult_left_mono assms) |
19453 | 102 |
moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2" |
41550 | 103 |
by (simp add: mult_right_mono_neg assms) |
19453 | 104 |
ultimately show ?thesis |
105 |
by simp |
|
106 |
qed |
|
107 |
moreover have "nprt a * pprt b <= nprt a2 * pprt b1" |
|
108 |
proof - |
|
109 |
have "nprt a * pprt b <= nprt a2 * pprt b" |
|
41550 | 110 |
by (simp add: mult_right_mono assms) |
19453 | 111 |
moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" |
41550 | 112 |
by (simp add: mult_left_mono_neg assms) |
19453 | 113 |
ultimately show ?thesis |
114 |
by simp |
|
115 |
qed |
|
116 |
moreover have "nprt a * nprt b <= nprt a1 * nprt b1" |
|
117 |
proof - |
|
118 |
have "nprt a * nprt b <= nprt a * nprt b1" |
|
41550 | 119 |
by (simp add: mult_left_mono_neg assms) |
19453 | 120 |
moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1" |
41550 | 121 |
by (simp add: mult_right_mono_neg assms) |
19453 | 122 |
ultimately show ?thesis |
123 |
by simp |
|
124 |
qed |
|
125 |
ultimately show ?thesis |
|
126 |
by - (rule add_mono | simp)+ |
|
127 |
qed |
|
128 |
||
129 |
lemma mult_le_dual_prts: |
|
130 |
assumes |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
131 |
"A * x \<le> (b::'a::lattice_ring)" |
19453 | 132 |
"0 \<le> y" |
133 |
"A1 \<le> A" |
|
134 |
"A \<le> A2" |
|
135 |
"c1 \<le> c" |
|
136 |
"c \<le> c2" |
|
137 |
"r1 \<le> x" |
|
138 |
"x \<le> r2" |
|
139 |
shows |
|
140 |
"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)" |
|
141 |
(is "_ <= _ + ?C") |
|
142 |
proof - |
|
41550 | 143 |
from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) |
29667 | 144 |
moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps) |
19453 | 145 |
ultimately have "c * x + (y * A - c) * x <= y * b" by simp |
146 |
then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq) |
|
29667 | 147 |
then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps) |
19453 | 148 |
have s2: "c - y * A <= c2 - y * A1" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
50252
diff
changeset
|
149 |
by (simp add: assms add_mono mult_left_mono algebra_simps) |
19453 | 150 |
have s1: "c1 - y * A2 <= c - y * A" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
50252
diff
changeset
|
151 |
by (simp add: assms add_mono mult_left_mono algebra_simps) |
19453 | 152 |
have prts: "(c - y * A) * x <= ?C" |
153 |
apply (simp add: Let_def) |
|
154 |
apply (rule mult_le_prts) |
|
41550 | 155 |
apply (simp_all add: assms s1 s2) |
19453 | 156 |
done |
157 |
then have "y * b + (c - y * A) * x <= y * b + ?C" |
|
158 |
by simp |
|
159 |
with cx show ?thesis |
|
160 |
by(simp only:) |
|
161 |
qed |
|
162 |
||
62390 | 163 |
end |