--- 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 \
--- 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
--- 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"];
--- 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
--- 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"
--- 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