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