Quelle  LP.thy

(*  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