# HG changeset patch
# User wenzelm
# Date 1224232779 -7200
# Node ID 7aabaf1ba263067c08aa973ddc872e3ace89429e
# Parent  d5342d4c736073de33a844180717f787f370b174
reactivated HOL-Matrix;
minor cleanup;

diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 17 10:39:39 2008 +0200
@@ -27,6 +27,7 @@
   HOL-Isar_examples \
   HOL-Lambda \
   HOL-Lattice \
+  HOL-Matrix \
   HOL-MetisExamples \
   HOL-MicroJava \
   HOL-Modelcheck \
@@ -831,9 +832,9 @@
 
 ## HOL-Matrix
 
-HOL-Matrix: HOL $(OUT)/HOL-Matrix
+HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
 
-$(OUT)/HOL-Matrix: $(OUT)/HOL				\
+$(LOG)/HOL-Matrix.gz: $(OUT)/HOL				\
   $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy			\
   $(SRC)/Tools/Compute_Oracle/am_compiler.ML				\
   $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:39:39 2008 +0200
@@ -1293,7 +1293,7 @@
   le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
 
 definition
-  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
+  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
 
 instance ..
 
@@ -1310,7 +1310,8 @@
 apply (rule ext)+
 apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
 apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
-by simp
+apply simp
+done
 
 lemma le_apply_matrix:
   assumes
diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/Matrix/ROOT.ML
--- a/src/HOL/Matrix/ROOT.ML	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/ROOT.ML	Fri Oct 17 10:39:39 2008 +0200
@@ -2,5 +2,4 @@
     ID:         $Id$
 *)
 
-use_thy "SparseMatrix";
-with_path "cplex" use_thy "Cplex";
+use_thys ["SparseMatrix", "cplex/Cplex"];
diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 17 10:39:39 2008 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory SparseMatrix
-imports "./Matrix"
+imports Matrix
 begin
 
 types 
diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/Matrix/cplex/Cplex.thy
--- a/src/HOL/Matrix/cplex/Cplex.thy	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy	Fri Oct 17 10:39:39 2008 +0200
@@ -5,7 +5,8 @@
 
 theory Cplex 
 imports SparseMatrix LP "~~/src/HOL/Real/Float" "~~/src/HOL/Tools/ComputeNumeral"
-uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" ("matrixlp.ML")
+uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
+  "fspmlp.ML" ("matrixlp.ML")
 begin
 
 lemma spm_mult_le_dual_prts: 
@@ -32,7 +33,7 @@
   add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
   add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
   apply (simp add: Let_def)
-  apply (insert prems)
+  apply (insert assms)
   apply (simp add: sparse_row_matrix_op_simps ring_simps)  
   apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
   apply (auto)
@@ -59,7 +60,7 @@
   shows
   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
   mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
-  by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
+  by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
 
 use "matrixlp.ML"
 
diff -r d5342d4c7360 -r 7aabaf1ba263 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Fri Oct 17 10:39:39 2008 +0200
@@ -25,7 +25,7 @@
 
 local
 
-val cert =  cterm_of (the_context ())
+val cert =  cterm_of @{theory}
 
 in
 
@@ -72,7 +72,7 @@
       "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
       "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
       "ComputeNumeral.natnorm"};
-    val computer = PCompute.make Compute.SML (the_context ()) ths []
+    val computer = PCompute.make Compute.SML @{theory} ths []
 in
 
 fun matrix_compute c = hd (PCompute.rewrite computer [c])
@@ -90,7 +90,7 @@
 
 fun prove_bound lptfile prec =
     let
-        val th = lp_dual_estimate_llprt lptfile prec
+        val th = lp_dual_estimate_prt lptfile prec
     in
         matrix_simplify th
     end