# HG changeset patch # User haftmann # Date 1328914157 -3600 # Node ID 5522e28a566e7584df163821aa35f7dda1e4cf73 # Parent ddf7cc923d192eb923a9ace8dfefb79b581f4005 tuned code diff -r ddf7cc923d19 -r 5522e28a566e src/HOL/Matrix/matrixlp.ML --- a/src/HOL/Matrix/matrixlp.ML Fri Feb 10 23:36:02 2012 +0100 +++ b/src/HOL/Matrix/matrixlp.ML Fri Feb 10 23:49:17 2012 +0100 @@ -4,9 +4,6 @@ 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 @@ -16,69 +13,45 @@ structure MatrixLP : MATRIX_LP = struct -fun inst_real thm = - let val certT = ctyp_of (Thm.theory_of_thm thm) in - Drule.export_without_context (Thm.instantiate - ([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm) - end - -local - -val cert = cterm_of @{theory} +val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let" + "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" + "ComputeHOL.compute_bool" "ComputeHOL.compute_pair" + "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm" + "ComputeNumeral.natnorm"}; -in - -fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = - let - val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"} - fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.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 +val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]} fun lp_dual_estimate_prt lptfile prec = - let - val certificate = - let - open Fspmlp - val l = load lptfile prec false - in - (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) - end - in - lp_dual_estimate_prt_primitive certificate - end + let + val cert = cterm_of @{theory} + fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x) + val l = Fspmlp.load lptfile prec false + val (y, (A1, A2), (c1, c2), b, (r1, r2)) = + let + open Fspmlp + in + (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) + end + in + 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]) + spm_mult_le_dual_prts_no_let_real + end -end - -local - val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let" - "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" - "ComputeHOL.compute_bool" "ComputeHOL.compute_pair" - "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm" - "ComputeNumeral.natnorm"}; - val computer = PCompute.make Compute.SML @{theory} ths [] -in +val computer = PCompute.make Compute.SML @{theory} compute_thms [] fun matrix_compute c = hd (PCompute.rewrite computer [c]) -end - fun matrix_simplify th = - let - val simp_th = matrix_compute (cprop_of th) - val th = Thm.strip_shyps (Thm.equal_elim simp_th th) - fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th - in - removeTrue th - end + let + val simp_th = matrix_compute (cprop_of th) + val th = Thm.strip_shyps (Thm.equal_elim simp_th th) + fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th + in + removeTrue th + end -fun prove_bound lptfile prec = - let - val th = lp_dual_estimate_prt lptfile prec - in - matrix_simplify th - end +fun prove_bound lptfile prec = matrix_simplify (lp_dual_estimate_prt lptfile prec); val realFromStr = the o Real.fromString; fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);