(* Title: HOL/Matrix_LP/LP.thy Author: Steven Obua *) theory LP imports Main "HOL-Library.Lattice_Algebras" begin lemma le_add_right_mono: assumes "a <= b + (c::'a::ordered_ab_group_add)" "c <= d" shows "a <= b + d" apply (rule_tac order_trans[where y = "b+c"]) apply (simp_all add: assms) done lemma linprog_dual_estimate: assumes "A * x ≤ (b::'a::lattice_ring)" "0 ≤ y" "¦A - A'¦ ≤ δ_A" "b ≤ b'" "¦c - c'¦ ≤ δ_c" "¦x¦ ≤ r" shows "c * x ≤ y * b' + (y * δ_A + ¦y * A' - c'¦ + δ_c) * r" proof - from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono) from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps) from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp have 5: "c * x <= y * b' + ¦(y * (A - A') + (y * A' - c') + (c'-c)) * x¦" by (simp only: 4 estimate_by_abs) have 6: "¦(y * (A - A') + (y * A' - c') + (c'-c)) * x¦ <= ¦y * (A - A') + (y * A' - c') + (c'-c)¦ * ¦x¦" by (simp add: abs_le_mult) have 7: "(¦y * (A - A') + (y * A' - c') + (c'-c)¦) * ¦x¦ <= (¦y * (A-A') + (y*A'-c')¦ + ¦c' - c¦) * ¦x¦" by(rule abs_triangle_ineq [THEN mult_right_mono]) simp have 8: "(¦y * (A-A') + (y*A'-c')¦ + ¦c' - c¦) * ¦x¦ <= (¦y * (A-A')¦ + ¦y*A'-c'¦ + ¦c' - c¦) * ¦x¦" by (simp add: abs_triangle_ineq mult_right_mono) have 9: "(¦y * (A-A')¦ + ¦y*A'-c'¦ + ¦c'-c¦) * ¦x¦ <= (¦y¦ * ¦A-A'¦ + ¦y*A'-c'¦ + ¦c'-c¦) * ¦x¦" by (simp add: abs_le_mult mult_right_mono) have 10: "c'-c = -(c-c')" by (simp add: algebra_simps) have 11: "¦c'-c¦ = ¦c-c'¦" by (subst 10, subst abs_minus_cancel, simp) have 12: "(¦y¦ * ¦A-A'¦ + ¦y*A'-c'¦ + ¦c'-c¦) * ¦x¦ <= (¦y¦ * ¦A-A'¦ + ¦y*A'-c'¦ + δ_c) * ¦x¦" by (simp add: 11 assms mult_right_mono) have 13: "(¦y¦ * ¦A-A'¦ + ¦y*A'-c'¦ + δ_c) * ¦x¦ <= (¦y¦ * δ_A + ¦y*A'-c'¦ + δ_c) * ¦x¦" by (simp add: assms mult_right_mono mult_left_mono) have r: "(¦y¦ * δ_A + ¦y*A'-c'¦ + δ_c) * ¦x¦ <= (¦y¦ * δ_A + ¦y*A'-c'¦ + δ_c) * r" apply (rule mult_left_mono) apply (simp add: assms) apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+ apply (rule mult_left_mono[of "0" "δ_A", simplified]) apply (simp_all) apply (rule order_trans[where y="¦A-A'¦"], simp_all add: assms) apply (rule order_trans[where y="¦c-c'¦"], simp_all add: assms) done from 6 7 8 9 12 13 r have 14: "¦(y * (A - A') + (y * A' - c') + (c'-c)) * x¦ <= (¦y¦ * δ_A + ¦y*A'-c'¦ + δ_c) * r" by (simp) show ?thesis apply (rule le_add_right_mono[of _ _ "¦(y * (A - A') + (y * A' - c') + (c'-c)) * x¦"]) apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]]) done qed lemma le_ge_imp_abs_diff_1: assumes "A1 <= (A::'a::lattice_ring)" "A <= A2" shows "¦A-A1¦ <= A2-A1" proof - have "0 <= A - A1" proof - from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp qed then have "¦A-A1¦ = A-A1" by (rule abs_of_nonneg) with assms show "¦A-A1¦ <= (A2-A1)" by simp qed lemma mult_le_prts: assumes "a1 <= (a::'a::lattice_ring)" "a <= a2" "b1 <= b" "b <= b2" shows "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" proof - have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" apply (subst prts[symmetric])+ apply simp done then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" by (simp add: algebra_simps) moreover have "pprt a * pprt b <= pprt a2 * pprt b2" by (simp_all add: assms mult_mono) moreover have "pprt a * nprt b <= pprt a1 * nprt b2" proof - have "pprt a * nprt b <= pprt a * nprt b2" by (simp add: mult_left_mono assms) moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2" by (simp add: mult_right_mono_neg assms) ultimately show ?thesis by simp qed moreover have "nprt a * pprt b <= nprt a2 * pprt b1" proof - have "nprt a * pprt b <= nprt a2 * pprt b" by (simp add: mult_right_mono assms) moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" by (simp add: mult_left_mono_neg assms) ultimately show ?thesis by simp qed moreover have "nprt a * nprt b <= nprt a1 * nprt b1" proof - have "nprt a * nprt b <= nprt a * nprt b1" by (simp add: mult_left_mono_neg assms) moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1" by (simp add: mult_right_mono_neg assms) ultimately show ?thesis by simp qed ultimately show ?thesis by - (rule add_mono | simp)+ qed lemma mult_le_dual_prts: assumes "A * x ≤ (b::'a::lattice_ring)" "0 ≤ y" "A1 ≤ A" "A ≤ A2" "c1 ≤ c" "c ≤ c2" "r1 ≤ x" "x ≤ r2" shows "c * x ≤ 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)" (is "_ <= _ + ?C") proof - from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps) ultimately have "c * x + (y * A - c) * x <= y * b" by simp then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq) then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps) have s2: "c - y * A <= c2 - y * A1" by (simp add: assms add_mono mult_left_mono algebra_simps) have s1: "c1 - y * A2 <= c - y * A" by (simp add: assms add_mono mult_left_mono algebra_simps) have prts: "(c - y * A) * x <= ?C" apply (simp add: Let_def) apply (rule mult_le_prts) apply (simp_all add: assms s1 s2) done then have "y * b + (c - y * A) * x <= y * b + ?C" by simp with cx show ?thesis by(simp only:) qed end