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)
    1.32      apply (simp add: assms)
    1.33      apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    1.34 -    apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    1.35 +    apply (rule mult_left_mono[of "0" "\<delta>_A", simplified])
    1.36      apply (simp_all)
    1.37      apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
    1.38      apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
    1.39      done    
    1.40 -  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"     
    1.41 +  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"     
    1.42      by (simp)
    1.43    show ?thesis
    1.44      apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])