author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46988  9f492f5b0cec 
child 47455  26315a545e26 
permissions  rwrr 
19453  1 
(* Title: HOL/Matrix/LP.thy 
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 logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

9 
lemma le_add_right_mono: 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

10 
assumes 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

11 
"a <= b + (c::'a::ordered_ab_group_add)" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

12 
"c <= d" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

13 
shows "a <= b + d" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; 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 logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

16 
done 
314a88278715
discontinued pretending that abel_cancel is logicindependent; 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" 
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  

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 
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 * (AA') + (y*A'c')) + abs(c'c)) * abs x" 

38 
by(rule abs_triangle_ineq [THEN mult_right_mono]) simp 

39 
have 8: " (abs (y * (AA') + (y*A'c')) + abs(c'c)) * abs x <= (abs (y * (AA')) + abs (y*A'c') + abs(c'c)) * abs x" 

40 
by (simp add: abs_triangle_ineq mult_right_mono) 

41 
have 9: "(abs (y * (AA')) + abs (y*A'c') + abs(c'c)) * abs x <= (abs y * abs (AA') + abs (y*A'c') + abs (c'c)) * abs x" 

42 
by (simp add: abs_le_mult mult_right_mono) 

29667  43 
have 10: "c'c = (cc')" by (simp add: algebra_simps) 
19453  44 
have 11: "abs (c'c) = abs (cc')" 
45 
by (subst 10, subst abs_minus_cancel, simp) 

46 
have 12: "(abs y * abs (AA') + abs (y*A'c') + abs (c'c)) * abs x <= (abs y * abs (AA') + abs (y*A'c') + \<delta>c) * abs x" 

41550  47 
by (simp add: 11 assms mult_right_mono) 
19453  48 
have 13: "(abs y * abs (AA') + abs (y*A'c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'c') + \<delta>c) * abs x" 
41550  49 
by (simp add: assms mult_right_mono mult_left_mono) 
19453  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) 

41550  52 
apply (simp add: assms) 
19453  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) 

41550  56 
apply (rule order_trans[where y="abs (AA')"], simp_all add: assms) 
57 
apply (rule order_trans[where y="abs (cc')"], simp_all add: assms) 

19453  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) 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

61 
show ?thesis 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
35032
diff
changeset

62 
apply (rule le_add_right_mono[of _ _ "abs((y * (A  A') + (y * A'  c') + (c'c)) * x)"]) 
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" 
71 
shows "abs (AA1) <= A2A1" 

72 
proof  

73 
have "0 <= A  A1" 

74 
proof  

75 
have 1: "A  A1 = A + ( A1)" by simp 

41550  76 
show ?thesis by (simp only: 1 add_right_mono[of A1 A "A1", simplified, simplified assms]) 
19453  77 
qed 
78 
then have "abs (AA1) = AA1" by (rule abs_of_nonneg) 

41550  79 
with assms show "abs (AA1) <= (A2A1)" by simp 
19453  80 
qed 
81 

82 
lemma mult_le_prts: 

83 
assumes 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
32491
diff
changeset

84 
"a1 <= (a::'a::lattice_ring)" 
19453  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" 

29667  96 
by (simp add: algebra_simps) 
19453  97 
moreover have "pprt a * pprt b <= pprt a2 * pprt b2" 
41550  98 
by (simp_all add: assms mult_mono) 
19453  99 
moreover have "pprt a * nprt b <= pprt a1 * nprt b2" 
100 
proof  

101 
have "pprt a * nprt b <= pprt a * nprt b2" 

41550  102 
by (simp add: mult_left_mono assms) 
19453  103 
moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2" 
41550  104 
by (simp add: mult_right_mono_neg assms) 
19453  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" 

41550  111 
by (simp add: mult_right_mono assms) 
19453  112 
moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" 
41550  113 
by (simp add: mult_left_mono_neg assms) 
19453  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" 

41550  120 
by (simp add: mult_left_mono_neg assms) 
19453  121 
moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1" 
41550  122 
by (simp add: mult_right_mono_neg assms) 
19453  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 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
32491
diff
changeset

132 
"A * x \<le> (b::'a::lattice_ring)" 
19453  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  

41550  144 
from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
29667  145 
moreover have "y * (A * x) = c * x + (y * A  c) * x" by (simp add: algebra_simps) 
19453  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) 

29667  148 
then have cx: "c * x <= y * b + (c  y * A) * x" by (simp add: algebra_simps) 
19453  149 
have s2: "c  y * A <= c2  y * A1" 
41550  150 
by (simp add: diff_minus assms add_mono mult_left_mono) 
19453  151 
have s1: "c1  y * A2 <= c  y * A" 
41550  152 
by (simp add: diff_minus assms add_mono mult_left_mono) 
19453  153 
have prts: "(c  y * A) * x <= ?C" 
154 
apply (simp add: Let_def) 

155 
apply (rule mult_le_prts) 

41550  156 
apply (simp_all add: assms s1 s2) 
19453  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 