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
```