src/HOL/Matrix/MatrixLP_gensimp.ML
author obua
Fri Sep 03 17:10:36 2004 +0200 (2004-09-03)
changeset 15178 5f621aa35c25
permissions -rw-r--r--
Matrix theory, linear programming
     1 open BasisLibrary;
     2 
     3 use "Cplex.ML";
     4 use "CplexMatrixConverter.ML";
     5 use "ExactFloatingPoint.ML";
     6 use "FloatArith.ML";
     7 use "FloatSparseMatrixBuilder.ML";
     8 use "fspmlp.ML";
     9 use "codegen_prep.ML";
    10 use "eq_codegen.ML";
    11 use "conv.ML";
    12 
    13 
    14 val th = theory "MatrixLP"
    15 val sg = sign_of th
    16 	 
    17 fun prep x = standard (mk_meta_eq x)
    18 	     
    19 fun inst_real thm = standard (Thm.instantiate ([(fst (hd (term_tvars (prop_of thm))),
    20 						 ctyp_of sg HOLogic.realT)], []) thm);
    21     
    22 val spm_lp_dual_estimate_simp = 
    23     (thms "Float.arith_no_let") @ 
    24     (map inst_real (thms "SparseMatrix.sparse_row_matrix_arith_simps")) @ 
    25     (thms "SparseMatrix.sorted_sp_simps") @ 
    26     [thm "Product_Type.fst_conv", thm "Product_Type.snd_conv"] @ 
    27     (thms "SparseMatrix.boolarith") 
    28     
    29 val simp_with = Simplifier.simplify (HOL_basic_ss addsimps [thm "SparseMatrix.if_case_eq", thm "Float.norm_0_1"])
    30 		
    31 val spm_lp_dual_estimate_simp = map simp_with spm_lp_dual_estimate_simp
    32 				
    33 val geninput = codegen_prep.prepare_thms spm_lp_dual_estimate_simp
    34 
    35 val _ = SimprocsCodegen.use_simprocs_code sg geninput