src/HOL/Matrix/MatrixLP.ML
author obua
Fri Sep 03 17:10:36 2004 +0200 (2004-09-03)
changeset 15178 5f621aa35c25
child 15180 6d3f59785197
permissions -rw-r--r--
Matrix theory, linear programming
     1 use "MatrixLP_gensimp.ML";
     2 
     3 signature MATRIX_LP = 
     4 sig
     5   val lp_dual_estimate : string -> int -> thm
     6   val simplify : thm -> thm
     7 end
     8 
     9 structure MatrixLP : MATRIX_LP =
    10 struct
    11 
    12 val _ = SimprocsCodegen.use_simprocs_code sg geninput
    13 
    14 val simp_le_spmat = simp_SparseMatrix_le_spmat_'_mult__'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_bool'
    15 val simp_add_spmat = simp_SparseMatrix_add_spmat_'_mult__'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
    16 val simp_diff_spmat = simp_SparseMatrix_diff_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''' 
    17 val simp_abs_spmat = simp_SparseMatrix_abs_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''' 
    18 val simp_mult_spmat = simp_SparseMatrix_mult_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
    19 val simp_sorted_sparse_matrix = simp_SparseMatrix_sorted_sparse_matrix
    20 val simp_sorted_spvec = simp_SparseMatrix_sorted_spvec
    21 	   
    22 fun single_arg simp ct = snd (simp (snd (Thm.dest_comb ct)))
    23 
    24 fun double_arg simp ct =  
    25 	let
    26 	    val (a, y) = Thm.dest_comb ct
    27 	    val (_, x) = Thm.dest_comb a
    28 	in
    29 	    snd (simp x y)
    30 	end      
    31 
    32 fun spmc ct =
    33     (case term_of ct of	 
    34 	 ((Const ("SparseMatrix.le_spmat", _)) $ _) =>
    35 	 single_arg simp_le_spmat ct
    36        | ((Const ("SparseMatrix.add_spmat", _)) $ _) =>
    37 	 single_arg simp_add_spmat ct
    38        | ((Const ("SparseMatrix.diff_spmat", _)) $ _ $ _) =>
    39 	 double_arg simp_diff_spmat ct
    40        | ((Const ("SparseMatrix.abs_spmat", _)) $ _) =>
    41 	 single_arg simp_abs_spmat ct
    42        | ((Const ("SparseMatrix.mult_spmat", _)) $ _ $ _) =>
    43 	 double_arg simp_mult_spmat ct
    44        | ((Const ("SparseMatrix.sorted_sparse_matrix", _)) $ _) =>
    45 	 single_arg simp_sorted_sparse_matrix ct
    46        | ((Const ("SparseMatrix.sorted_spvec", ty)) $ _) =>
    47 	 single_arg simp_sorted_spvec ct 
    48       | _ => raise Fail_conv)
    49 
    50 fun lp_dual_estimate lptfile prec =
    51     let
    52 	val th = inst_real (thm "SparseMatrix.spm_linprog_dual_estimate_1")
    53 	val sg = sign_of (theory "MatrixLP")
    54 	val (y, (A1, A2), (c1, c2), b, r) = 
    55 	    let
    56 		open fspmlp
    57 		val l = load lptfile prec false
    58 	    in
    59 		(y l, A l, c l, b l, r l)
    60 	    end		
    61 	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
    62 	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r" r, var "b" b]) th
    63     in
    64 	th
    65     end
    66 
    67 fun simplify th = 
    68     let
    69 	val simp_th = botc spmc (cprop_of th)
    70 	val th = strip_shyps (equal_elim simp_th th)
    71 	fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
    72     in
    73 	removeTrue th
    74     end
    75 
    76 fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
    77 
    78 end
    79 
    80 val result = ref ([]:thm list)
    81 
    82 fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ()))
    83