--- a/src/HOL/IsaMakefile Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/IsaMakefile Mon Apr 10 16:00:34 2006 +0200
@@ -672,7 +672,7 @@
HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
- Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
+ Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
Matrix/document/root.tex Matrix/ROOT.ML \
Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
--- a/src/HOL/Matrix/SparseMatrix.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Mon Apr 10 16:00:34 2006 +0200
@@ -3,7 +3,7 @@
Author: Steven Obua
*)
-theory SparseMatrix imports Matrix begin
+theory SparseMatrix imports Matrix LP begin
types
'a spvec = "(nat * 'a) list"
--- a/src/HOL/Matrix/cplex/MatrixLP.ML Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.ML Mon Apr 10 16:00:34 2006 +0200
@@ -6,6 +6,7 @@
signature MATRIX_LP =
sig
val lp_dual_estimate_prt : string -> int -> thm
+ val lp_dual_estimate_prt_primitive : cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
val matrix_compute : cterm -> thm
val matrix_simplify : thm -> thm
val prove_bound : string -> int -> thm
@@ -20,21 +21,27 @@
fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
ctyp_of sg HOLogic.realT)], []) thm)
+fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
+ let
+ val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
+ fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
+ val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
+ var "r1" r1, var "r2" r2, var "b" b]) th
+ in
+ th
+ end
+
fun lp_dual_estimate_prt lptfile prec =
let
- val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
- val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
+ val certificate =
let
open fspmlp
val l = load lptfile prec false
in
(y l, A l, c l, b l, r12 l)
end
- fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
- val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
- var "r1" r1, var "r2" r2, var "b" b]) th
in
- th
+ lp_dual_estimate_prt_primitive certificate
end
fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
--- a/src/HOL/Matrix/cplex/fspmlp.ML Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Mon Apr 10 16:00:34 2006 +0200
@@ -6,6 +6,8 @@
signature FSPMLP =
sig
type linprog
+ type vector = FloatSparseMatrixBuilder.vector
+ type matrix = FloatSparseMatrixBuilder.matrix
val y : linprog -> cterm
val A : linprog -> cterm * cterm
@@ -22,6 +24,9 @@
structure fspmlp : FSPMLP =
struct
+type vector = FloatSparseMatrixBuilder.vector
+type matrix = FloatSparseMatrixBuilder.matrix
+
type linprog = cterm * (cterm * cterm) * cterm * (cterm * cterm) * cterm * (cterm * cterm)
fun y (c1, c2, c3, c4, c5, _) = c1
@@ -314,6 +319,7 @@
val c = FloatSparseMatrixBuilder.approx_matrix prec id c
in
(y1, A, b2, c, r, (r1, r2))
- end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
+ end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
+
end
--- a/src/HOL/OrderedGroup.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/OrderedGroup.thy Mon Apr 10 16:00:34 2006 +0200
@@ -854,6 +854,12 @@
lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
by (simp add: le_def_meet nprt_def meet_aci)
+lemma pprt_neg: "pprt (-x) = - nprt x"
+ by (simp add: pprt_def nprt_def)
+
+lemma nprt_neg: "nprt (-x) = - pprt x"
+ by (simp add: pprt_def nprt_def)
+
lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
by (simp)
@@ -1029,6 +1035,8 @@
declare diff_le_0_iff_le [simp]
+
+
ML {*
val add_zero_left = thm"add_0";
val add_zero_right = thm"add_0_right";
--- a/src/HOL/Ring_and_Field.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Ring_and_Field.thy Mon Apr 10 16:00:34 2006 +0200
@@ -1932,71 +1932,7 @@
apply (simp add: order_less_imp_le);
done;
-subsection {* Miscellaneous *}
-
-lemma linprog_dual_estimate:
- assumes
- "A * x \<le> (b::'a::lordered_ring)"
- "0 \<le> y"
- "abs (A - A') \<le> \<delta>A"
- "b \<le> b'"
- "abs (c - c') \<le> \<delta>c"
- "abs x \<le> r"
- shows
- "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
-proof -
- from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
- from prems 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: ring_eq_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' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
- by (simp only: 4 estimate_by_abs)
- have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
- by (simp add: abs_le_mult)
- have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
- by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
- have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <= (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
- by (simp add: abs_triangle_ineq mult_right_mono)
- have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
- by (simp add: abs_le_mult mult_right_mono)
- have 10: "c'-c = -(c-c')" by (simp add: ring_eq_simps)
- have 11: "abs (c'-c) = abs (c-c')"
- by (subst 10, subst abs_minus_cancel, simp)
- 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"
- by (simp add: 11 prems mult_right_mono)
- 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"
- by (simp add: prems mult_right_mono mult_left_mono)
- 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"
- apply (rule mult_left_mono)
- apply (simp add: prems)
- apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
- apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
- apply (simp_all)
- apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
- apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
- done
- 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"
- by (simp)
- show ?thesis
- apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
- apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
- done
-qed
-
-lemma le_ge_imp_abs_diff_1:
- assumes
- "A1 <= (A::'a::lordered_ring)"
- "A <= A2"
- shows "abs (A-A1) <= A2-A1"
-proof -
- have "0 <= A - A1"
- proof -
- have 1: "A - A1 = A + (- A1)" by simp
- show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
- qed
- then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
- with prems show "abs (A-A1) <= (A2-A1)" by simp
-qed
+subsection {* Bounds of products via negative and positive Part *}
lemma mult_le_prts:
assumes
@@ -2045,39 +1981,23 @@
ultimately show ?thesis
by - (rule add_mono | simp)+
qed
-
-lemma mult_le_dual_prts:
+
+lemma mult_ge_prts:
assumes
- "A * x \<le> (b::'a::lordered_ring)"
- "0 \<le> y"
- "A1 \<le> A"
- "A \<le> A2"
- "c1 \<le> c"
- "c \<le> c2"
- "r1 \<le> x"
- "x \<le> r2"
+ "a1 <= (a::'a::lordered_ring)"
+ "a <= a2"
+ "b1 <= b"
+ "b <= b2"
shows
- "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)"
- (is "_ <= _ + ?C")
-proof -
- from prems 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: ring_eq_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: ring_eq_simps)
- have s2: "c - y * A <= c2 - y * A1"
- by (simp add: diff_def prems add_mono mult_left_mono)
- have s1: "c1 - y * A2 <= c - y * A"
- by (simp add: diff_def prems add_mono mult_left_mono)
- have prts: "(c - y * A) * x <= ?C"
- apply (simp add: Let_def)
- apply (rule mult_le_prts)
- apply (simp_all add: prems s1 s2)
- done
- then have "y * b + (c - y * A) * x <= y * b + ?C"
- by simp
- with cx show ?thesis
- by(simp only:)
+ "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
+proof -
+ from prems have a1:"- a2 <= -a" by auto
+ from prems have a2: "-a <= -a1" by auto
+ from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]
+ have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp
+ then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
+ by (simp only: minus_le_iff)
+ then show ?thesis by simp
qed
ML {*
--- a/src/HOL/Wellfounded_Relations.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Mon Apr 10 16:00:34 2006 +0200
@@ -116,13 +116,11 @@
apply (drule spec, erule mp, blast)
done
-
text{*Transitivity of WF combinators.*}
lemma trans_lex_prod [intro!]:
"[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
by (unfold trans_def lex_prod_def, blast)
-
subsubsection{*Wellfoundedness of proper subset on finite sets.*}
lemma wf_finite_psubset: "wf(finite_psubset)"
apply (unfold finite_psubset_def)