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;
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
obua@23665
    28
val cert =  cterm_of @{theory "Cplex"}
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
obua@23665
    34
    val th = inst_real @{thm "SparseMatrix.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
obua@23665
    70
    val matrix_lemmas = [
obua@23665
    71
	"ComputeHOL.compute_list_case",
obua@23665
    72
	"ComputeHOL.compute_let",
obua@23665
    73
        "ComputeHOL.compute_if",
obua@23665
    74
        "Float.arith",
obua@23665
    75
        "SparseMatrix.sparse_row_matrix_arith_simps",
obua@23665
    76
        "ComputeHOL.compute_bool",
obua@23665
    77
        "ComputeHOL.compute_pair", 
obua@23665
    78
	"SparseMatrix.sorted_sp_simps",
obua@23665
    79
        "ComputeNumeral.number_norm",
obua@23665
    80
	"ComputeNumeral.natnorm"]
wenzelm@26343
    81
    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n)
wenzelm@26343
    82
    val ths = maps get_thms matrix_lemmas
obua@23665
    83
    val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
obua@23665
    84
in
wenzelm@20787
    85
obua@23665
    86
fun matrix_compute c = hd (PCompute.rewrite computer [c])
wenzelm@20787
    87
obua@23665
    88
end
obua@23665
    89
        
wenzelm@20787
    90
fun matrix_simplify th =
wenzelm@20787
    91
    let
wenzelm@20787
    92
        val simp_th = matrix_compute (cprop_of th)
wenzelm@20787
    93
        val th = strip_shyps (equal_elim simp_th th)
wenzelm@20787
    94
        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
wenzelm@20787
    95
    in
wenzelm@20787
    96
        removeTrue th
wenzelm@20787
    97
    end
wenzelm@20787
    98
wenzelm@20787
    99
fun prove_bound lptfile prec =
wenzelm@20787
   100
    let
wenzelm@20787
   101
        val th = lp_dual_estimate_prt lptfile prec
wenzelm@20787
   102
    in
wenzelm@20787
   103
        matrix_simplify th
wenzelm@20787
   104
    end
wenzelm@20787
   105
wenzelm@20787
   106
val realFromStr = the o Real.fromString;
wenzelm@20787
   107
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
wenzelm@20787
   108
wenzelm@20787
   109
end