equal
deleted
inserted
replaced
70 "A <= A2" |
70 "A <= A2" |
71 shows "abs (A-A1) <= A2-A1" |
71 shows "abs (A-A1) <= A2-A1" |
72 proof - |
72 proof - |
73 have "0 <= A - A1" |
73 have "0 <= A - A1" |
74 proof - |
74 proof - |
75 have 1: "A - A1 = A + (- A1)" by simp |
75 from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp |
76 show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms]) |
|
77 qed |
76 qed |
78 then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg) |
77 then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg) |
79 with assms show "abs (A-A1) <= (A2-A1)" by simp |
78 with assms show "abs (A-A1) <= (A2-A1)" by simp |
80 qed |
79 qed |
81 |
80 |
145 moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps) |
144 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 |
145 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) |
146 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) |
147 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" |
148 have s2: "c - y * A <= c2 - y * A1" |
150 by (simp add: diff_minus assms add_mono mult_left_mono) |
149 by (simp add: assms add_mono mult_left_mono algebra_simps) |
151 have s1: "c1 - y * A2 <= c - y * A" |
150 have s1: "c1 - y * A2 <= c - y * A" |
152 by (simp add: diff_minus assms add_mono mult_left_mono) |
151 by (simp add: assms add_mono mult_left_mono algebra_simps) |
153 have prts: "(c - y * A) * x <= ?C" |
152 have prts: "(c - y * A) * x <= ?C" |
154 apply (simp add: Let_def) |
153 apply (simp add: Let_def) |
155 apply (rule mult_le_prts) |
154 apply (rule mult_le_prts) |
156 apply (simp_all add: assms s1 s2) |
155 apply (simp_all add: assms s1 s2) |
157 done |
156 done |