src/HOL/Matrix/cplex/matrixlp.ML
author wenzelm
Thu Mar 20 00:20:44 2008 +0100 (2008-03-20)
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 27484 dbb9981c3d18
permissions -rw-r--r--
simplified get_thm(s): back to plain name argument;
     1 (*  Title:      HOL/Matrix/cplex/matrixlp.ML
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 signature MATRIX_LP =
     7 sig
     8   val lp_dual_estimate_prt : string -> int -> thm
     9   val lp_dual_estimate_prt_primitive :
    10     cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
    11   val matrix_compute : cterm -> thm
    12   val matrix_simplify : thm -> thm
    13   val prove_bound : string -> int -> thm
    14   val float2real : string * string -> Real.real
    15 end
    16 
    17 structure MatrixLP : MATRIX_LP =
    18 struct
    19 
    20 fun inst_real thm =
    21   let val certT = ctyp_of (Thm.theory_of_thm thm) in
    22     standard (Thm.instantiate
    23       ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    24   end
    25 
    26 local
    27 
    28 val cert =  cterm_of @{theory "Cplex"}
    29 
    30 in
    31 
    32 fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
    33   let
    34     val th = inst_real @{thm "SparseMatrix.spm_mult_le_dual_prts_no_let"}
    35     fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x)
    36     val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
    37                                    var "r1" r1, var "r2" r2, var "b" b]) th
    38   in th end
    39 
    40 fun lp_dual_estimate_prt lptfile prec =
    41     let
    42         val certificate =
    43             let
    44                 open Fspmlp
    45                 val l = load lptfile prec false
    46             in
    47                 (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
    48             end
    49     in
    50         lp_dual_estimate_prt_primitive certificate
    51     end
    52 
    53 end
    54 
    55 fun prep ths = ComputeHOL.prep_thms ths
    56 
    57 fun inst_tvar ty thm =
    58     let
    59         val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
    60         val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
    61         val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
    62     in
    63         standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
    64     end
    65 
    66 fun inst_tvars [] thms = thms
    67   | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
    68 
    69 local
    70     val matrix_lemmas = [
    71 	"ComputeHOL.compute_list_case",
    72 	"ComputeHOL.compute_let",
    73         "ComputeHOL.compute_if",
    74         "Float.arith",
    75         "SparseMatrix.sparse_row_matrix_arith_simps",
    76         "ComputeHOL.compute_bool",
    77         "ComputeHOL.compute_pair", 
    78 	"SparseMatrix.sorted_sp_simps",
    79         "ComputeNumeral.number_norm",
    80 	"ComputeNumeral.natnorm"]
    81     fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n)
    82     val ths = maps get_thms matrix_lemmas
    83     val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
    84 in
    85 
    86 fun matrix_compute c = hd (PCompute.rewrite computer [c])
    87 
    88 end
    89         
    90 fun matrix_simplify th =
    91     let
    92         val simp_th = matrix_compute (cprop_of th)
    93         val th = strip_shyps (equal_elim simp_th th)
    94         fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
    95     in
    96         removeTrue th
    97     end
    98 
    99 fun prove_bound lptfile prec =
   100     let
   101         val th = lp_dual_estimate_prt lptfile prec
   102     in
   103         matrix_simplify th
   104     end
   105 
   106 val realFromStr = the o Real.fromString;
   107 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
   108 
   109 end