src/HOL/Matrix_LP/matrixlp.ML
author wenzelm
Fri Apr 13 14:00:26 2012 +0200 (2012-04-13)
changeset 47455 26315a545e26
parent 46988 9f492f5b0cec
child 51989 700693cb96f1
permissions -rw-r--r--
updated headers;
     1 (*  Title:      HOL/Matrix_LP/matrixlp.ML
     2     Author:     Steven Obua
     3 *)
     4 
     5 signature MATRIX_LP =
     6 sig
     7   val matrix_compute : cterm -> thm
     8   val matrix_simplify : thm -> thm
     9   val prove_bound : string -> int -> thm
    10   val float2real : string * string -> Real.real
    11 end
    12 
    13 structure MatrixLP : MATRIX_LP =
    14 struct
    15 
    16 val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
    17   "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
    18   "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    19   "SparseMatrix.sorted_sp_simps"
    20   "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
    21 
    22 val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}
    23 
    24 fun lp_dual_estimate_prt lptfile prec =
    25   let
    26     val cert = cterm_of @{theory}
    27     fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x)
    28     val l = Fspmlp.load lptfile prec false
    29     val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
    30       let
    31         open Fspmlp
    32       in
    33         (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
    34       end
    35   in
    36     Thm.instantiate ([],
    37       [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b])
    38       spm_mult_le_dual_prts_no_let_real
    39   end
    40 
    41 val computer = PCompute.make Compute.SML @{theory} compute_thms []
    42 
    43 fun matrix_compute c = hd (PCompute.rewrite computer [c])
    44 
    45 fun matrix_simplify th =
    46   let
    47     val simp_th = matrix_compute (cprop_of th)
    48     val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
    49     fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
    50   in
    51     removeTrue th
    52   end
    53 
    54 val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
    55 
    56 val realFromStr = the o Real.fromString;
    57 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
    58 
    59 end