src/HOL/Matrix/MatrixLP_gensimp.ML
changeset 15178 5f621aa35c25
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Matrix/MatrixLP_gensimp.ML	Fri Sep 03 17:10:36 2004 +0200
     1.3 @@ -0,0 +1,35 @@
     1.4 +open BasisLibrary;
     1.5 +
     1.6 +use "Cplex.ML";
     1.7 +use "CplexMatrixConverter.ML";
     1.8 +use "ExactFloatingPoint.ML";
     1.9 +use "FloatArith.ML";
    1.10 +use "FloatSparseMatrixBuilder.ML";
    1.11 +use "fspmlp.ML";
    1.12 +use "codegen_prep.ML";
    1.13 +use "eq_codegen.ML";
    1.14 +use "conv.ML";
    1.15 +
    1.16 +
    1.17 +val th = theory "MatrixLP"
    1.18 +val sg = sign_of th
    1.19 +	 
    1.20 +fun prep x = standard (mk_meta_eq x)
    1.21 +	     
    1.22 +fun inst_real thm = standard (Thm.instantiate ([(fst (hd (term_tvars (prop_of thm))),
    1.23 +						 ctyp_of sg HOLogic.realT)], []) thm);
    1.24 +    
    1.25 +val spm_lp_dual_estimate_simp = 
    1.26 +    (thms "Float.arith_no_let") @ 
    1.27 +    (map inst_real (thms "SparseMatrix.sparse_row_matrix_arith_simps")) @ 
    1.28 +    (thms "SparseMatrix.sorted_sp_simps") @ 
    1.29 +    [thm "Product_Type.fst_conv", thm "Product_Type.snd_conv"] @ 
    1.30 +    (thms "SparseMatrix.boolarith") 
    1.31 +    
    1.32 +val simp_with = Simplifier.simplify (HOL_basic_ss addsimps [thm "SparseMatrix.if_case_eq", thm "Float.norm_0_1"])
    1.33 +		
    1.34 +val spm_lp_dual_estimate_simp = map simp_with spm_lp_dual_estimate_simp
    1.35 +				
    1.36 +val geninput = codegen_prep.prepare_thms spm_lp_dual_estimate_simp
    1.37 +
    1.38 +val _ = SimprocsCodegen.use_simprocs_code sg geninput