src/HOL/Matrix/cplex/matrixlp.ML
author haftmann
Fri, 04 Jul 2008 07:39:01 +0200
changeset 27484 dbb9981c3d18
parent 26343 0dd2eab7b296
child 28262 aa7ca36d67fd
permissions -rw-r--r--
added marginal setup for code generation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 23665
diff changeset
     1
(*  Title:      HOL/Matrix/cplex/matrixlp.ML
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Steven Obua
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     4
*)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     5
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     6
signature MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     7
sig
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     8
  val lp_dual_estimate_prt : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     9
  val lp_dual_estimate_prt_primitive :
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    10
    cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    11
  val matrix_compute : cterm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    12
  val matrix_simplify : thm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    13
  val prove_bound : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    14
  val float2real : string * string -> Real.real
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    15
end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    16
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    17
structure MatrixLP : MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    18
struct
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    19
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    20
fun inst_real thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    21
  let val certT = ctyp_of (Thm.theory_of_thm thm) in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    22
    standard (Thm.instantiate
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    23
      ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    24
  end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    25
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    26
local
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    27
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    28
val cert =  cterm_of @{theory}
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    29
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    30
in
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    31
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    32
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    33
  let
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    34
    val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"}
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 20787
diff changeset
    35
    fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x)
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    36
    val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    37
                                   var "r1" r1, var "r2" r2, var "b" b]) th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    38
  in th end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    39
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    40
fun lp_dual_estimate_prt lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    41
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    42
        val certificate =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    43
            let
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 20787
diff changeset
    44
                open Fspmlp
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    45
                val l = load lptfile prec false
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    46
            in
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    47
                (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    48
            end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    49
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    50
        lp_dual_estimate_prt_primitive certificate
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    51
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    52
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    53
end
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    54
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    55
fun prep ths = ComputeHOL.prep_thms ths
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    56
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    57
fun inst_tvar ty thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    58
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    59
        val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    60
        val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    61
        val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    62
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    63
        standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    64
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    65
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    66
fun inst_tvars [] thms = thms
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    67
  | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    68
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    69
local
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    70
    val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    71
      "ComputeHOL.compute_if" "Float.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    72
      "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    73
      "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    74
      "ComputeNumeral.natnorm"};
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    75
    val computer = PCompute.make Compute.SML @{theory} ths []
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    76
in
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    77
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    78
fun matrix_compute c = hd (PCompute.rewrite computer [c])
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    79
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    80
end
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    81
        
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    82
fun matrix_simplify th =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    83
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    84
        val simp_th = matrix_compute (cprop_of th)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    85
        val th = strip_shyps (equal_elim simp_th th)
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    86
        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    87
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    88
        removeTrue th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    89
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    90
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    91
fun prove_bound lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    92
    let
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    93
        val th = lp_dual_estimate_llprt lptfile prec
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    94
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    95
        matrix_simplify th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    96
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    97
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    98
val realFromStr = the o Real.fromString;
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    99
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   100
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   101
end