src/HOL/Matrix_LP/matrixlp.ML
author wenzelm
Sat Mar 17 12:52:40 2012 +0100 (2012-03-17)
changeset 46988 9f492f5b0cec
parent 46544 src/HOL/Matrix/matrixlp.ML@460b0d81d486
child 47455 26315a545e26
permissions -rw-r--r--
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
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 matrix_compute : cterm -> thm
wenzelm@20787
     8
  val matrix_simplify : thm -> thm
wenzelm@20787
     9
  val prove_bound : string -> int -> thm
wenzelm@20787
    10
  val float2real : string * string -> Real.real
wenzelm@20787
    11
end
wenzelm@20787
    12
wenzelm@20787
    13
structure MatrixLP : MATRIX_LP =
wenzelm@20787
    14
struct
wenzelm@20787
    15
haftmann@46540
    16
val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
haftmann@46540
    17
  "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
haftmann@46540
    18
  "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
haftmann@46544
    19
  "SparseMatrix.sorted_sp_simps"
haftmann@46544
    20
  "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
obua@23665
    21
haftmann@46540
    22
val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}
wenzelm@20787
    23
wenzelm@20787
    24
fun lp_dual_estimate_prt lptfile prec =
haftmann@46540
    25
  let
haftmann@46540
    26
    val cert = cterm_of @{theory}
haftmann@46540
    27
    fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x)
haftmann@46540
    28
    val l = Fspmlp.load lptfile prec false
haftmann@46540
    29
    val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
haftmann@46540
    30
      let
haftmann@46540
    31
        open Fspmlp
haftmann@46540
    32
      in
haftmann@46540
    33
        (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
haftmann@46540
    34
      end
haftmann@46540
    35
  in
haftmann@46540
    36
    Thm.instantiate ([],
haftmann@46540
    37
      [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b])
haftmann@46540
    38
      spm_mult_le_dual_prts_no_let_real
haftmann@46540
    39
  end
wenzelm@20787
    40
haftmann@46540
    41
val computer = PCompute.make Compute.SML @{theory} compute_thms []
wenzelm@20787
    42
obua@23665
    43
fun matrix_compute c = hd (PCompute.rewrite computer [c])
wenzelm@20787
    44
wenzelm@20787
    45
fun matrix_simplify th =
haftmann@46540
    46
  let
haftmann@46540
    47
    val simp_th = matrix_compute (cprop_of th)
haftmann@46540
    48
    val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
haftmann@46540
    49
    fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
haftmann@46540
    50
  in
haftmann@46540
    51
    removeTrue th
haftmann@46540
    52
  end
wenzelm@20787
    53
haftmann@46541
    54
val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
wenzelm@20787
    55
wenzelm@20787
    56
val realFromStr = the o Real.fromString;
wenzelm@20787
    57
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
wenzelm@20787
    58
wenzelm@20787
    59
end