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