src/HOL/Matrix/cplex/matrixlp.ML
author wenzelm
Mon Sep 29 11:46:47 2008 +0200 (2008-09-29)
changeset 28397 389c5e494605
parent 28262 aa7ca36d67fd
child 28637 7aabaf1ba263
permissions -rw-r--r--
handle _ should be avoided (spurious Interrupt will spoil the game);
     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 (the_context ())
    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 "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 ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
    71       "ComputeHOL.compute_if" "Float.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
    72       "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    73       "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
    74       "ComputeNumeral.natnorm"};
    75     val computer = PCompute.make Compute.SML (the_context ()) ths []
    76 in
    77 
    78 fun matrix_compute c = hd (PCompute.rewrite computer [c])
    79 
    80 end
    81         
    82 fun matrix_simplify th =
    83     let
    84         val simp_th = matrix_compute (cprop_of th)
    85         val th = strip_shyps (equal_elim simp_th th)
    86         fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
    87     in
    88         removeTrue th
    89     end
    90 
    91 fun prove_bound lptfile prec =
    92     let
    93         val th = lp_dual_estimate_llprt lptfile prec
    94     in
    95         matrix_simplify th
    96     end
    97 
    98 val realFromStr = the o Real.fromString;
    99 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
   100 
   101 end