src/HOL/Matrix/matrixlp.ML
author haftmann
Tue, 13 Jul 2010 11:38:04 +0200
changeset 37788 261c61fabc98
parent 37764 3489daf839d5
child 40298 2bdb14323fbf
permissions -rw-r--r--
corrected title
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37788
261c61fabc98 corrected title
haftmann
parents: 37764
diff changeset
     1
(*  Title:      HOL/Matrix/matrixlp.ML
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Steven Obua
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     3
*)
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
signature MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     6
sig
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     7
  val lp_dual_estimate_prt : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     8
  val lp_dual_estimate_prt_primitive :
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
     9
    cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    10
  val matrix_compute : cterm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    11
  val matrix_simplify : thm -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    12
  val prove_bound : string -> int -> thm
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    13
  val float2real : string * string -> Real.real
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    14
end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    15
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    16
structure MatrixLP : MATRIX_LP =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    17
struct
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    18
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    19
fun inst_real thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    20
  let val certT = ctyp_of (Thm.theory_of_thm thm) in
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 32957
diff changeset
    21
    Drule.export_without_context (Thm.instantiate
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28637
diff changeset
    22
      ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    23
  end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    24
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    25
local
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    26
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 28397
diff changeset
    27
val cert =  cterm_of @{theory}
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    28
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    29
in
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    30
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    31
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
    32
  let
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    33
    val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"}
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 20787
diff changeset
    34
    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
    35
    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
    36
                                   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
    37
  in th end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    38
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    39
fun lp_dual_estimate_prt lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    40
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    41
        val certificate =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    42
            let
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 20787
diff changeset
    43
                open Fspmlp
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    44
                val l = load lptfile prec false
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    45
            in
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    46
                (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
    47
            end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    48
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    49
        lp_dual_estimate_prt_primitive certificate
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    50
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    51
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    52
end
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    53
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    54
fun prep ths = ComputeHOL.prep_thms ths
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    55
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    56
fun inst_tvar ty thm =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    57
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    58
        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
    59
        val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 28637
diff changeset
    60
        val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    61
    in
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 32957
diff changeset
    62
        Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    63
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    64
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    65
fun inst_tvars [] thms = thms
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    66
  | 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
    67
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    68
local
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    69
    val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29270
diff changeset
    70
      "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    71
      "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    72
      "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 26343
diff changeset
    73
      "ComputeNumeral.natnorm"};
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 28397
diff changeset
    74
    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
    75
in
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    76
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    77
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
    78
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    79
end
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 22964
diff changeset
    80
        
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    81
fun matrix_simplify th =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    82
    let
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    83
        val simp_th = matrix_compute (cprop_of th)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36614
diff changeset
    84
        val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36614
diff changeset
    85
        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    86
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    87
        removeTrue th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    88
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    89
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    90
fun prove_bound lptfile prec =
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    91
    let
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 28397
diff changeset
    92
        val th = lp_dual_estimate_prt lptfile prec
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    93
    in
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    94
        matrix_simplify th
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    95
    end
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    96
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    97
val realFromStr = the o Real.fromString;
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
    98
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
    99
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff changeset
   100
end