# HG changeset patch
# User haftmann
# Date 1328914157 -3600
# Node ID 5522e28a566e7584df163821aa35f7dda1e4cf73
# Parent  ddf7cc923d192eb923a9ace8dfefb79b581f4005
tuned code

diff -r ddf7cc923d19 -r 5522e28a566e src/HOL/Matrix/matrixlp.ML
--- a/src/HOL/Matrix/matrixlp.ML	Fri Feb 10 23:36:02 2012 +0100
+++ b/src/HOL/Matrix/matrixlp.ML	Fri Feb 10 23:49:17 2012 +0100
@@ -4,9 +4,6 @@
 
 signature MATRIX_LP =
 sig
-  val lp_dual_estimate_prt : string -> int -> thm
-  val lp_dual_estimate_prt_primitive :
-    cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
   val matrix_compute : cterm -> thm
   val matrix_simplify : thm -> thm
   val prove_bound : string -> int -> thm
@@ -16,69 +13,45 @@
 structure MatrixLP : MATRIX_LP =
 struct
 
-fun inst_real thm =
-  let val certT = ctyp_of (Thm.theory_of_thm thm) in
-    Drule.export_without_context (Thm.instantiate
-      ([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
-  end
-
-local
-
-val cert =  cterm_of @{theory}
+val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
+  "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
+  "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
+  "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
+  "ComputeNumeral.natnorm"};
 
-in
-
-fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
-  let
-    val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"}
-    fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x)
-    val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
-                                   var "r1" r1, var "r2" r2, var "b" b]) th
-  in th end
+val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}
 
 fun lp_dual_estimate_prt lptfile prec =
-    let
-        val certificate =
-            let
-                open Fspmlp
-                val l = load lptfile prec false
-            in
-                (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
-            end
-    in
-        lp_dual_estimate_prt_primitive certificate
-    end
+  let
+    val cert = cterm_of @{theory}
+    fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x)
+    val l = Fspmlp.load lptfile prec false
+    val (y, (A1, A2), (c1, c2), b, (r1, r2)) =
+      let
+        open Fspmlp
+      in
+        (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
+      end
+  in
+    Thm.instantiate ([],
+      [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b])
+      spm_mult_le_dual_prts_no_let_real
+  end
 
-end
-
-local
-    val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
-      "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
-      "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
-      "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
-      "ComputeNumeral.natnorm"};
-    val computer = PCompute.make Compute.SML @{theory} ths []
-in
+val computer = PCompute.make Compute.SML @{theory} compute_thms []
 
 fun matrix_compute c = hd (PCompute.rewrite computer [c])
 
-end
-        
 fun matrix_simplify th =
-    let
-        val simp_th = matrix_compute (cprop_of th)
-        val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
-        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
-    in
-        removeTrue th
-    end
+  let
+    val simp_th = matrix_compute (cprop_of th)
+    val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
+    fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
+  in
+    removeTrue th
+  end
 
-fun prove_bound lptfile prec =
-    let
-        val th = lp_dual_estimate_prt lptfile prec
-    in
-        matrix_simplify th
-    end
+fun prove_bound lptfile prec = matrix_simplify (lp_dual_estimate_prt lptfile prec);
 
 val realFromStr = the o Real.fromString;
 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);