Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: LP.thy Sprache: Isabelle

Original von: Isabelle^©

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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.