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