src/HOL/Matrix_LP/LP.thy
 changeset 50252 4aa34bd43228 parent 47455 26315a545e26 child 54230 b1d955791529
```     1.1 --- a/src/HOL/Matrix_LP/LP.thy	Wed Nov 28 15:38:12 2012 +0100
1.2 +++ b/src/HOL/Matrix_LP/LP.thy	Wed Nov 28 15:59:18 2012 +0100
1.3 @@ -19,12 +19,12 @@
1.4    assumes
1.5    "A * x \<le> (b::'a::lattice_ring)"
1.6    "0 \<le> y"
1.7 -  "abs (A - A') \<le> \<delta>A"
1.8 +  "abs (A - A') \<le> \<delta>_A"
1.9    "b \<le> b'"
1.10 -  "abs (c - c') \<le> \<delta>c"
1.11 +  "abs (c - c') \<le> \<delta>_c"
1.12    "abs x \<le> r"
1.13    shows
1.14 -  "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
1.15 +  "c * x \<le> y * b' + (y * \<delta>_A + abs (y * A' - c') + \<delta>_c) * r"
1.16  proof -
1.17    from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
1.18    from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono)
1.19 @@ -43,20 +43,20 @@
1.20    have 10: "c'-c = -(c-c')" by (simp add: algebra_simps)
1.21    have 11: "abs (c'-c) = abs (c-c')"
1.22      by (subst 10, subst abs_minus_cancel, simp)
1.23 -  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"
1.24 +  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"
1.25      by (simp add: 11 assms mult_right_mono)
1.26 -  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"
1.27 +  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"
1.28      by (simp add: assms mult_right_mono mult_left_mono)
1.29 -  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"
1.30 +  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"
1.31      apply (rule mult_left_mono)