reactivated HOL-Matrix;
authorwenzelm
Fri Oct 17 10:39:39 2008 +0200 (2008-10-17)
changeset 286377aabaf1ba263
parent 28636 d5342d4c7360
child 28638 809dda85079d
reactivated HOL-Matrix;
minor cleanup;
src/HOL/IsaMakefile
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/ROOT.ML
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Matrix/cplex/Cplex.thy
src/HOL/Matrix/cplex/matrixlp.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 17 10:21:03 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 17 10:39:39 2008 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    HOL-Isar_examples \
     1.5    HOL-Lambda \
     1.6    HOL-Lattice \
     1.7 +  HOL-Matrix \
     1.8    HOL-MetisExamples \
     1.9    HOL-MicroJava \
    1.10    HOL-Modelcheck \
    1.11 @@ -831,9 +832,9 @@
    1.12  
    1.13  ## HOL-Matrix
    1.14  
    1.15 -HOL-Matrix: HOL $(OUT)/HOL-Matrix
    1.16 +HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
    1.17  
    1.18 -$(OUT)/HOL-Matrix: $(OUT)/HOL				\
    1.19 +$(LOG)/HOL-Matrix.gz: $(OUT)/HOL				\
    1.20    $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy			\
    1.21    $(SRC)/Tools/Compute_Oracle/am_compiler.ML				\
    1.22    $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
     2.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:21:03 2008 +0200
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:39:39 2008 +0200
     2.3 @@ -1293,7 +1293,7 @@
     2.4    le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
     2.5  
     2.6  definition
     2.7 -  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
     2.8 +  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
     2.9  
    2.10  instance ..
    2.11  
    2.12 @@ -1310,7 +1310,8 @@
    2.13  apply (rule ext)+
    2.14  apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
    2.15  apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
    2.16 -by simp
    2.17 +apply simp
    2.18 +done
    2.19  
    2.20  lemma le_apply_matrix:
    2.21    assumes
     3.1 --- a/src/HOL/Matrix/ROOT.ML	Fri Oct 17 10:21:03 2008 +0200
     3.2 +++ b/src/HOL/Matrix/ROOT.ML	Fri Oct 17 10:39:39 2008 +0200
     3.3 @@ -2,5 +2,4 @@
     3.4      ID:         $Id$
     3.5  *)
     3.6  
     3.7 -use_thy "SparseMatrix";
     3.8 -with_path "cplex" use_thy "Cplex";
     3.9 +use_thys ["SparseMatrix", "cplex/Cplex"];
     4.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 17 10:21:03 2008 +0200
     4.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 17 10:39:39 2008 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  *)
     4.5  
     4.6  theory SparseMatrix
     4.7 -imports "./Matrix"
     4.8 +imports Matrix
     4.9  begin
    4.10  
    4.11  types 
     5.1 --- a/src/HOL/Matrix/cplex/Cplex.thy	Fri Oct 17 10:21:03 2008 +0200
     5.2 +++ b/src/HOL/Matrix/cplex/Cplex.thy	Fri Oct 17 10:39:39 2008 +0200
     5.3 @@ -5,7 +5,8 @@
     5.4  
     5.5  theory Cplex 
     5.6  imports SparseMatrix LP "~~/src/HOL/Real/Float" "~~/src/HOL/Tools/ComputeNumeral"
     5.7 -uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" ("matrixlp.ML")
     5.8 +uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
     5.9 +  "fspmlp.ML" ("matrixlp.ML")
    5.10  begin
    5.11  
    5.12  lemma spm_mult_le_dual_prts: 
    5.13 @@ -32,7 +33,7 @@
    5.14    add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
    5.15    add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
    5.16    apply (simp add: Let_def)
    5.17 -  apply (insert prems)
    5.18 +  apply (insert assms)
    5.19    apply (simp add: sparse_row_matrix_op_simps ring_simps)  
    5.20    apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
    5.21    apply (auto)
    5.22 @@ -59,7 +60,7 @@
    5.23    shows
    5.24    "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
    5.25    mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
    5.26 -  by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    5.27 +  by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    5.28  
    5.29  use "matrixlp.ML"
    5.30  
     6.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Fri Oct 17 10:21:03 2008 +0200
     6.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Fri Oct 17 10:39:39 2008 +0200
     6.3 @@ -25,7 +25,7 @@
     6.4  
     6.5  local
     6.6  
     6.7 -val cert =  cterm_of (the_context ())
     6.8 +val cert =  cterm_of @{theory}
     6.9  
    6.10  in
    6.11  
    6.12 @@ -72,7 +72,7 @@
    6.13        "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    6.14        "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
    6.15        "ComputeNumeral.natnorm"};
    6.16 -    val computer = PCompute.make Compute.SML (the_context ()) ths []
    6.17 +    val computer = PCompute.make Compute.SML @{theory} ths []
    6.18  in
    6.19  
    6.20  fun matrix_compute c = hd (PCompute.rewrite computer [c])
    6.21 @@ -90,7 +90,7 @@
    6.22  
    6.23  fun prove_bound lptfile prec =
    6.24      let
    6.25 -        val th = lp_dual_estimate_llprt lptfile prec
    6.26 +        val th = lp_dual_estimate_prt lptfile prec
    6.27      in
    6.28          matrix_simplify th
    6.29      end