src/HOL/Matrix/LP.thy
changeset 41550 efa734d9b221
parent 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Matrix/LP.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Matrix/LP.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    "c <= d"    
     1.5    shows "a <= b + d"
     1.6    apply (rule_tac order_trans[where y = "b+c"])
     1.7 -  apply (simp_all add: prems)
     1.8 +  apply (simp_all add: assms)
     1.9    done
    1.10  
    1.11  lemma linprog_dual_estimate:
    1.12 @@ -26,8 +26,8 @@
    1.13    shows
    1.14    "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
    1.15  proof -
    1.16 -  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    1.17 -  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    1.18 +  from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    1.19 +  from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    1.20    have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)  
    1.21    from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
    1.22    have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
    1.23 @@ -44,23 +44,23 @@
    1.24    have 11: "abs (c'-c) = abs (c-c')" 
    1.25      by (subst 10, subst abs_minus_cancel, simp)
    1.26    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.27 -    by (simp add: 11 prems mult_right_mono)
    1.28 +    by (simp add: 11 assms mult_right_mono)
    1.29    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.30 -    by (simp add: prems mult_right_mono mult_left_mono)  
    1.31 +    by (simp add: assms mult_right_mono mult_left_mono)  
    1.32    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.33      apply (rule mult_left_mono)
    1.34 -    apply (simp add: prems)
    1.35 +    apply (simp add: assms)
    1.36      apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    1.37      apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    1.38      apply (simp_all)
    1.39 -    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
    1.40 -    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
    1.41 +    apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
    1.42 +    apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
    1.43      done    
    1.44    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.45      by (simp)
    1.46    show ?thesis
    1.47      apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    1.48 -    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
    1.49 +    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
    1.50      done
    1.51  qed
    1.52  
    1.53 @@ -73,10 +73,10 @@
    1.54    have "0 <= A - A1"    
    1.55    proof -
    1.56      have 1: "A - A1 = A + (- A1)" by simp
    1.57 -    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
    1.58 +    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms])
    1.59    qed
    1.60    then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
    1.61 -  with prems show "abs (A-A1) <= (A2-A1)" by simp
    1.62 +  with assms show "abs (A-A1) <= (A2-A1)" by simp
    1.63  qed
    1.64  
    1.65  lemma mult_le_prts:
    1.66 @@ -95,31 +95,31 @@
    1.67    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
    1.68      by (simp add: algebra_simps)
    1.69    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
    1.70 -    by (simp_all add: prems mult_mono)
    1.71 +    by (simp_all add: assms mult_mono)
    1.72    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
    1.73    proof -
    1.74      have "pprt a * nprt b <= pprt a * nprt b2"
    1.75 -      by (simp add: mult_left_mono prems)
    1.76 +      by (simp add: mult_left_mono assms)
    1.77      moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
    1.78 -      by (simp add: mult_right_mono_neg prems)
    1.79 +      by (simp add: mult_right_mono_neg assms)
    1.80      ultimately show ?thesis
    1.81        by simp
    1.82    qed
    1.83    moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
    1.84    proof - 
    1.85      have "nprt a * pprt b <= nprt a2 * pprt b"
    1.86 -      by (simp add: mult_right_mono prems)
    1.87 +      by (simp add: mult_right_mono assms)
    1.88      moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
    1.89 -      by (simp add: mult_left_mono_neg prems)
    1.90 +      by (simp add: mult_left_mono_neg assms)
    1.91      ultimately show ?thesis
    1.92        by simp
    1.93    qed
    1.94    moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
    1.95    proof -
    1.96      have "nprt a * nprt b <= nprt a * nprt b1"
    1.97 -      by (simp add: mult_left_mono_neg prems)
    1.98 +      by (simp add: mult_left_mono_neg assms)
    1.99      moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
   1.100 -      by (simp add: mult_right_mono_neg prems)
   1.101 +      by (simp add: mult_right_mono_neg assms)
   1.102      ultimately show ?thesis
   1.103        by simp
   1.104    qed
   1.105 @@ -141,19 +141,19 @@
   1.106    "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)"
   1.107    (is "_ <= _ + ?C")
   1.108  proof -
   1.109 -  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   1.110 +  from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   1.111    moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps)  
   1.112    ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   1.113    then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   1.114    then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   1.115    have s2: "c - y * A <= c2 - y * A1"
   1.116 -    by (simp add: diff_minus prems add_mono mult_left_mono)
   1.117 +    by (simp add: diff_minus assms add_mono mult_left_mono)
   1.118    have s1: "c1 - y * A2 <= c - y * A"
   1.119 -    by (simp add: diff_minus prems add_mono mult_left_mono)
   1.120 +    by (simp add: diff_minus assms add_mono mult_left_mono)
   1.121    have prts: "(c - y * A) * x <= ?C"
   1.122      apply (simp add: Let_def)
   1.123      apply (rule mult_le_prts)
   1.124 -    apply (simp_all add: prems s1 s2)
   1.125 +    apply (simp_all add: assms s1 s2)
   1.126      done
   1.127    then have "y * b + (c - y * A) * x <= y * b + ?C"
   1.128      by simp