# HG changeset patch # User obua # Date 1144677634 -7200 # Node ID 9bf2cdc9e8e830c3a7d522a730a2dad58366cd36 # Parent 5c15cd397a82e71288a74ec5ac19f3ae2fc90cb5 Moved stuff from Ring_and_Field to Matrix diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/IsaMakefile --- 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 \ diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/Matrix/SparseMatrix.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" diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/Matrix/cplex/MatrixLP.ML --- 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); diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/Matrix/cplex/fspmlp.ML --- 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 diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/OrderedGroup.thy --- 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 \ 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) \ (A \ 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"; diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/Ring_and_Field.thy --- 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 \ (b::'a::lordered_ring)" - "0 \ y" - "abs (A - A') \ \A" - "b \ b'" - "abs (c - c') \ \c" - "abs x \ r" - shows - "c * x \ y * b' + (y * \A + abs (y * A' - c') + \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') + \c) * abs x" - by (simp add: 11 prems mult_right_mono) - have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \c) * abs x <= (abs y * \A + abs (y*A'-c') + \c) * abs x" - by (simp add: prems mult_right_mono mult_left_mono) - have r: "(abs y * \A + abs (y*A'-c') + \c) * abs x <= (abs y * \A + abs (y*A'-c') + \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" "\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 * \A + abs (y*A'-c') + \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 \ (b::'a::lordered_ring)" - "0 \ y" - "A1 \ A" - "A \ A2" - "c1 \ c" - "c \ c2" - "r1 \ x" - "x \ r2" + "a1 <= (a::'a::lordered_ring)" + "a <= a2" + "b1 <= b" + "b <= b2" 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 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 {* diff -r 5c15cd397a82 -r 9bf2cdc9e8e8 src/HOL/Wellfounded_Relations.thy --- 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)