src/HOL/Matrix_LP/fspmlp.ML

added various facts

(*  Title:      HOL/Matrix_LP/fspmlp.ML
    Author:     Steven Obua
*)

signature FSPMLP =
sig
    type linprog
    type vector = FloatSparseMatrixBuilder.vector
    type matrix = FloatSparseMatrixBuilder.matrix

    val y : linprog -> term
    val A : linprog -> term * term
    val b : linprog -> term
    val c : linprog -> term * term
    val r12 : linprog -> term * term

    exception Load of string

    val load : string -> int -> bool -> linprog
end

structure Fspmlp : FSPMLP =
struct

type vector = FloatSparseMatrixBuilder.vector
type matrix = FloatSparseMatrixBuilder.matrix

type linprog = term * (term * term) * term * (term * term) * (term * term)

fun y (c1, _, _, _, _) = c1
fun A (_, c2, _, _, _) = c2
fun b (_, _, c3, _, _) = c3
fun c (_, _, _, c4, _) = c4
fun r12 (_, _, _, _, c6) = c6

structure CplexFloatSparseMatrixConverter =
MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);

datatype bound_type = LOWER | UPPER

fun intbound_ord ((i1: int, b1),(i2,b2)) =
    if i1 < i2 then LESS
    else if i1 = i2 then
        (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
    else GREATER

structure Inttab = Table(type key = int val ord = (rev_order o int_ord));

structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)

exception Internal of string;

fun add_row_bound g dest_key row_index row_bound =
    let
        val x =
            case VarGraph.lookup g dest_key of
                NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty)
              | SOME (sure_bound, f) =>
                (sure_bound,
                 case Inttab.lookup f row_index of
                     NONE => Inttab.update (row_index, (row_bound, [])) f
                   | SOME _ => raise (Internal "add_row_bound"))
    in
        VarGraph.update (dest_key, x) g
    end

fun update_sure_bound g (key as (_, btype)) bound =
    let
        val x =
            case VarGraph.lookup g key of
                NONE => (SOME bound, Inttab.empty)
              | SOME (NONE, f) => (SOME bound, f)
              | SOME (SOME old_bound, f) =>
                (SOME ((case btype of
                            UPPER => Float.min
                          | LOWER => Float.max)