1.1 --- a/src/HOL/IsaMakefile Mon Mar 07 16:55:36 2005 +0100
1.2 +++ b/src/HOL/IsaMakefile Mon Mar 07 18:19:55 2005 +0100
1.3 @@ -634,12 +634,6 @@
1.4
1.5 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL-Complex \
1.6 Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
1.7 - Matrix/Float.thy Matrix/FloatArith.ML Matrix/ExactFloatingPoint.ML \
1.8 - Matrix/Cplex.ML Matrix/CplexMatrixConverter.ML \
1.9 - Matrix/FloatSparseMatrixBuilder.ML \
1.10 - Matrix/conv.ML Matrix/eq_codegen.ML Matrix/codegen_prep.ML \
1.11 - Matrix/fspmlp.ML \
1.12 - Matrix/MatrixLP_gensimp.ML Matrix/MatrixLP.ML Matrix/MatrixLP.thy \
1.13 Matrix/document/root.tex Matrix/ROOT.ML
1.14 @cd Matrix; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL-Matrix
1.15
2.1 --- a/src/HOL/Matrix/Cplex.ML Mon Mar 07 16:55:36 2005 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,1027 +0,0 @@
2.4 -signature CPLEX =
2.5 -sig
2.6 -
2.7 - datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
2.8 - | cplexNeg of cplexTerm
2.9 - | cplexProd of cplexTerm * cplexTerm
2.10 - | cplexSum of (cplexTerm list)
2.11 -
2.12 - datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
2.13 -
2.14 - datatype cplexGoal = cplexMinimize of cplexTerm
2.15 - | cplexMaximize of cplexTerm
2.16 -
2.17 - datatype cplexConstr = cplexConstr of cplexComp *
2.18 - (cplexTerm * cplexTerm)
2.19 -
2.20 - datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
2.21 - * cplexComp * cplexTerm
2.22 - | cplexBound of cplexTerm * cplexComp * cplexTerm
2.23 -
2.24 - datatype cplexProg = cplexProg of string
2.25 - * cplexGoal
2.26 - * ((string option * cplexConstr)
2.27 - list)
2.28 - * cplexBounds list
2.29 -
2.30 - datatype cplexResult = Unbounded
2.31 - | Infeasible
2.32 - | Undefined
2.33 - | Optimal of string *
2.34 - (((* name *) string *
2.35 - (* value *) string) list)
2.36 -
2.37 - exception Load_cplexFile of string
2.38 - exception Load_cplexResult of string
2.39 - exception Save_cplexFile of string
2.40 - exception Execute of string
2.41 -
2.42 - val load_cplexFile : string -> cplexProg
2.43 -
2.44 - val save_cplexFile : string -> cplexProg -> unit
2.45 -
2.46 - val elim_nonfree_bounds : cplexProg -> cplexProg
2.47 -
2.48 - val relax_strict_ineqs : cplexProg -> cplexProg
2.49 -
2.50 - val is_normed_cplexProg : cplexProg -> bool
2.51 -
2.52 - val load_cplexResult : string -> cplexResult
2.53 -
2.54 - val solve : cplexProg -> cplexResult
2.55 -end;
2.56 -
2.57 -structure Cplex : CPLEX =
2.58 -struct
2.59 -
2.60 -exception Load_cplexFile of string;
2.61 -exception Load_cplexResult of string;
2.62 -exception Save_cplexFile of string;
2.63 -
2.64 -datatype cplexTerm = cplexVar of string
2.65 - | cplexNum of string
2.66 - | cplexInf
2.67 - | cplexNeg of cplexTerm
2.68 - | cplexProd of cplexTerm * cplexTerm
2.69 - | cplexSum of (cplexTerm list)
2.70 -datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
2.71 -datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
2.72 -datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
2.73 -datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
2.74 - * cplexComp * cplexTerm
2.75 - | cplexBound of cplexTerm * cplexComp * cplexTerm
2.76 -datatype cplexProg = cplexProg of string
2.77 - * cplexGoal
2.78 - * ((string option * cplexConstr) list)
2.79 - * cplexBounds list
2.80 -
2.81 -fun rev_cmp cplexLe = cplexGe
2.82 - | rev_cmp cplexLeq = cplexGeq
2.83 - | rev_cmp cplexGe = cplexLe
2.84 - | rev_cmp cplexGeq = cplexLeq
2.85 - | rev_cmp cplexEq = cplexEq
2.86 -
2.87 -fun the NONE = raise (Load_cplexFile "SOME expected")
2.88 - | the (SOME x) = x;
2.89 -
2.90 -fun modulo_signed is_something (cplexNeg u) = is_something u
2.91 - | modulo_signed is_something u = is_something u
2.92 -
2.93 -fun is_Num (cplexNum _) = true
2.94 - | is_Num _ = false
2.95 -
2.96 -fun is_Inf cplexInf = true
2.97 - | is_Inf _ = false
2.98 -
2.99 -fun is_Var (cplexVar _) = true
2.100 - | is_Var _ = false
2.101 -
2.102 -fun is_Neg (cplexNeg x ) = true
2.103 - | is_Neg _ = false
2.104 -
2.105 -fun is_normed_Prod (cplexProd (t1, t2)) =
2.106 - (is_Num t1) andalso (is_Var t2)
2.107 - | is_normed_Prod x = is_Var x
2.108 -
2.109 -fun is_normed_Sum (cplexSum ts) =
2.110 - (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
2.111 - | is_normed_Sum x = modulo_signed is_normed_Prod x
2.112 -
2.113 -fun is_normed_Constr (cplexConstr (c, (t1, t2))) =
2.114 - (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
2.115 -
2.116 -fun is_Num_or_Inf x = is_Inf x orelse is_Num x
2.117 -
2.118 -fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
2.119 - (c1 = cplexLe orelse c1 = cplexLeq) andalso
2.120 - (c2 = cplexLe orelse c2 = cplexLeq) andalso
2.121 - is_Var t2 andalso
2.122 - modulo_signed is_Num_or_Inf t1 andalso
2.123 - modulo_signed is_Num_or_Inf t3
2.124 - | is_normed_Bounds (cplexBound (t1, c, t2)) =
2.125 - (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
2.126 - orelse
2.127 - (c <> cplexEq andalso
2.128 - is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
2.129 -
2.130 -fun term_of_goal (cplexMinimize x) = x
2.131 - | term_of_goal (cplexMaximize x) = x
2.132 -
2.133 -fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) =
2.134 - is_normed_Sum (term_of_goal goal) andalso
2.135 - forall (fn (_,x) => is_normed_Constr x) constraints andalso
2.136 - forall is_normed_Bounds bounds
2.137 -
2.138 -fun is_NL s = s = "\n"
2.139 -
2.140 -fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
2.141 -
2.142 -fun is_num a =
2.143 - let
2.144 - val b = String.explode a
2.145 - fun num4 cs = forall Char.isDigit cs
2.146 - fun num3 [] = true
2.147 - | num3 (ds as (c::cs)) =
2.148 - if c = #"+" orelse c = #"-" then
2.149 - num4 cs
2.150 - else
2.151 - num4 ds
2.152 - fun num2 [] = true
2.153 - | num2 (c::cs) =
2.154 - if c = #"e" orelse c = #"E" then num3 cs
2.155 - else (Char.isDigit c) andalso num2 cs
2.156 - fun num1 [] = true
2.157 - | num1 (c::cs) =
2.158 - if c = #"." then num2 cs
2.159 - else if c = #"e" orelse c = #"E" then num3 cs
2.160 - else (Char.isDigit c) andalso num1 cs
2.161 - fun num [] = true
2.162 - | num (c::cs) =
2.163 - if c = #"." then num2 cs
2.164 - else (Char.isDigit c) andalso num1 cs
2.165 - in
2.166 - num b
2.167 - end
2.168 -
2.169 -fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
2.170 -
2.171 -fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
2.172 - orelse s = ">=" orelse s = "="
2.173 -
2.174 -fun is_symbol a =
2.175 - let
2.176 - val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
2.177 - fun is_symbol_char c = Char.isAlphaNum c orelse
2.178 - exists (fn d => d=c) symbol_char
2.179 - fun is_symbol_start c = is_symbol_char c andalso
2.180 - not (Char.isDigit c) andalso
2.181 - not (c= #".")
2.182 - val b = String.explode a
2.183 - in
2.184 - b <> [] andalso is_symbol_start (hd b) andalso
2.185 - forall is_symbol_char b
2.186 - end
2.187 -
2.188 -fun to_upper s = String.implode (map Char.toUpper (String.explode s))
2.189 -
2.190 -fun keyword x =
2.191 - let
2.192 - val a = to_upper x
2.193 - in
2.194 - if a = "BOUNDS" orelse a = "BOUND" then
2.195 - SOME "BOUNDS"
2.196 - else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
2.197 - SOME "MINIMIZE"
2.198 - else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
2.199 - SOME "MAXIMIZE"
2.200 - else if a = "ST" orelse a = "S.T." orelse a = "ST." then
2.201 - SOME "ST"
2.202 - else if a = "FREE" orelse a = "END" then
2.203 - SOME a
2.204 - else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
2.205 - SOME "GENERAL"
2.206 - else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
2.207 - SOME "INTEGER"
2.208 - else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
2.209 - SOME "BINARY"
2.210 - else if a = "INF" orelse a = "INFINITY" then
2.211 - SOME "INF"
2.212 - else
2.213 - NONE
2.214 - end
2.215 -
2.216 -val TOKEN_ERROR = ~1
2.217 -val TOKEN_BLANK = 0
2.218 -val TOKEN_NUM = 1
2.219 -val TOKEN_DELIMITER = 2
2.220 -val TOKEN_SYMBOL = 3
2.221 -val TOKEN_LABEL = 4
2.222 -val TOKEN_CMP = 5
2.223 -val TOKEN_KEYWORD = 6
2.224 -val TOKEN_NL = 7
2.225 -
2.226 -(* tokenize takes a list of chars as argument and returns a list of
2.227 - int * string pairs, each string representing a "cplex token",
2.228 - and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
2.229 - or TOKEN_SYMBOL *)
2.230 -fun tokenize s =
2.231 - let
2.232 - val flist = [(is_NL, TOKEN_NL),
2.233 - (is_blank, TOKEN_BLANK),
2.234 - (is_num, TOKEN_NUM),
2.235 - (is_delimiter, TOKEN_DELIMITER),
2.236 - (is_cmp, TOKEN_CMP),
2.237 - (is_symbol, TOKEN_SYMBOL)]
2.238 - fun match_helper [] s = (fn x => false, TOKEN_ERROR)
2.239 - | match_helper (f::fs) s =
2.240 - if ((fst f) s) then f else match_helper fs s
2.241 - fun match s = match_helper flist s
2.242 - fun tok s =
2.243 - if s = "" then [] else
2.244 - let
2.245 - val h = String.substring (s,0,1)
2.246 - val (f, j) = match h
2.247 - fun len i =
2.248 - if size s = i then i
2.249 - else if f (String.substring (s,0,i+1)) then
2.250 - len (i+1)
2.251 - else i
2.252 - in
2.253 - if j < 0 then
2.254 - (if h = "\\" then []
2.255 - else raise (Load_cplexFile ("token expected, found: "
2.256 - ^s)))
2.257 - else
2.258 - let
2.259 - val l = len 1
2.260 - val u = String.substring (s,0,l)
2.261 - val v = String.extract (s,l,NONE)
2.262 - in
2.263 - if j = 0 then tok v else (j, u) :: tok v
2.264 - end
2.265 - end
2.266 - in
2.267 - tok s
2.268 - end
2.269 -
2.270 -exception Tokenize of string;
2.271 -
2.272 -fun tokenize_general flist s =
2.273 - let
2.274 - fun match_helper [] s = raise (Tokenize s)
2.275 - | match_helper (f::fs) s =
2.276 - if ((fst f) s) then f else match_helper fs s
2.277 - fun match s = match_helper flist s
2.278 - fun tok s =
2.279 - if s = "" then [] else
2.280 - let
2.281 - val h = String.substring (s,0,1)
2.282 - val (f, j) = match h
2.283 - fun len i =
2.284 - if size s = i then i
2.285 - else if f (String.substring (s,0,i+1)) then
2.286 - len (i+1)
2.287 - else i
2.288 - val l = len 1
2.289 - in
2.290 - (j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
2.291 - end
2.292 - in
2.293 - tok s
2.294 - end
2.295 -
2.296 -fun load_cplexFile name =
2.297 - let
2.298 - val f = TextIO.openIn name
2.299 - val ignore_NL = ref true
2.300 - val rest = ref []
2.301 -
2.302 - fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
2.303 -
2.304 - fun readToken_helper () =
2.305 - if length (!rest) > 0 then
2.306 - let val u = hd (!rest) in
2.307 - (
2.308 - rest := tl (!rest);
2.309 - SOME u
2.310 - )
2.311 - end
2.312 - else
2.313 - let val s = TextIO.inputLine f in
2.314 - if s = "" then NONE else
2.315 - let val t = tokenize s in
2.316 - if (length t >= 2 andalso
2.317 - snd(hd (tl t)) = ":")
2.318 - then
2.319 - rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
2.320 - else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
2.321 - andalso is_symbol "TO" (hd (tl t))
2.322 - then
2.323 - rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
2.324 - else
2.325 - rest := t;
2.326 - readToken_helper ()
2.327 - end
2.328 - end
2.329 -
2.330 - fun readToken_helper2 () =
2.331 - let val c = readToken_helper () in
2.332 - if c = NONE then NONE
2.333 - else if !ignore_NL andalso fst (the c) = TOKEN_NL then
2.334 - readToken_helper2 ()
2.335 - else if fst (the c) = TOKEN_SYMBOL
2.336 - andalso keyword (snd (the c)) <> NONE
2.337 - then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
2.338 - else c
2.339 - end
2.340 -
2.341 - fun readToken () = readToken_helper2 ()
2.342 -
2.343 - fun pushToken a = rest := (a::(!rest))
2.344 -
2.345 - fun is_value token =
2.346 - fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
2.347 - andalso snd token = "INF")
2.348 -
2.349 - fun get_value token =
2.350 - if fst token = TOKEN_NUM then
2.351 - cplexNum (snd token)
2.352 - else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
2.353 - then
2.354 - cplexInf
2.355 - else
2.356 - raise (Load_cplexFile "num expected")
2.357 -
2.358 - fun readTerm_Product only_num =
2.359 - let val c = readToken () in
2.360 - if c = NONE then NONE
2.361 - else if fst (the c) = TOKEN_SYMBOL
2.362 - then (
2.363 - if only_num then (pushToken (the c); NONE)
2.364 - else SOME (cplexVar (snd (the c)))
2.365 - )
2.366 - else if only_num andalso is_value (the c) then
2.367 - SOME (get_value (the c))
2.368 - else if is_value (the c) then
2.369 - let val t1 = get_value (the c)
2.370 - val d = readToken ()
2.371 - in
2.372 - if d = NONE then SOME t1
2.373 - else if fst (the d) = TOKEN_SYMBOL then
2.374 - SOME (cplexProd (t1, cplexVar (snd (the d))))
2.375 - else
2.376 - (pushToken (the d); SOME t1)
2.377 - end
2.378 - else (pushToken (the c); NONE)
2.379 - end
2.380 -
2.381 - fun readTerm_Signed only_signed only_num =
2.382 - let
2.383 - val c = readToken ()
2.384 - in
2.385 - if c = NONE then NONE
2.386 - else
2.387 - let val d = the c in
2.388 - if d = (TOKEN_DELIMITER, "+") then
2.389 - readTerm_Product only_num
2.390 - else if d = (TOKEN_DELIMITER, "-") then
2.391 - SOME (cplexNeg (the (readTerm_Product
2.392 - only_num)))
2.393 - else (pushToken d;
2.394 - if only_signed then NONE
2.395 - else readTerm_Product only_num)
2.396 - end
2.397 - end
2.398 -
2.399 - fun readTerm_Sum first_signed =
2.400 - let val c = readTerm_Signed first_signed false in
2.401 - if c = NONE then [] else (the c)::(readTerm_Sum true)
2.402 - end
2.403 -
2.404 - fun readTerm () =
2.405 - let val c = readTerm_Sum false in
2.406 - if c = [] then NONE
2.407 - else if tl c = [] then SOME (hd c)
2.408 - else SOME (cplexSum c)
2.409 - end
2.410 -
2.411 - fun readLabeledTerm () =
2.412 - let val c = readToken () in
2.413 - if c = NONE then (NONE, NONE)
2.414 - else if fst (the c) = TOKEN_LABEL then
2.415 - let val t = readTerm () in
2.416 - if t = NONE then
2.417 - raise (Load_cplexFile ("term after label "^
2.418 - (snd (the c))^
2.419 - " expected"))
2.420 - else (SOME (snd (the c)), t)
2.421 - end
2.422 - else (pushToken (the c); (NONE, readTerm ()))
2.423 - end
2.424 -
2.425 - fun readGoal () =
2.426 - let
2.427 - val g = readToken ()
2.428 - in
2.429 - if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
2.430 - cplexMaximize (the (snd (readLabeledTerm ())))
2.431 - else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
2.432 - cplexMinimize (the (snd (readLabeledTerm ())))
2.433 - else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
2.434 - end
2.435 -
2.436 - fun str2cmp b =
2.437 - (case b of
2.438 - "<" => cplexLe
2.439 - | "<=" => cplexLeq
2.440 - | ">" => cplexGe
2.441 - | ">=" => cplexGeq
2.442 - | "=" => cplexEq
2.443 - | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
2.444 -
2.445 - fun readConstraint () =
2.446 - let
2.447 - val t = readLabeledTerm ()
2.448 - fun make_constraint b t1 t2 =
2.449 - cplexConstr
2.450 - (str2cmp b,
2.451 - (t1, t2))
2.452 - in
2.453 - if snd t = NONE then NONE
2.454 - else
2.455 - let val c = readToken () in
2.456 - if c = NONE orelse fst (the c) <> TOKEN_CMP
2.457 - then raise (Load_cplexFile "TOKEN_CMP expected")
2.458 - else
2.459 - let val n = readTerm_Signed false true in
2.460 - if n = NONE then
2.461 - raise (Load_cplexFile "num expected")
2.462 - else
2.463 - SOME (fst t,
2.464 - make_constraint (snd (the c))
2.465 - (the (snd t))
2.466 - (the n))
2.467 - end
2.468 - end
2.469 - end
2.470 -
2.471 - fun readST () =
2.472 - let
2.473 - fun readbody () =
2.474 - let val t = readConstraint () in
2.475 - if t = NONE then []
2.476 - else if (is_normed_Constr (snd (the t))) then
2.477 - (the t)::(readbody ())
2.478 - else if (fst (the t) <> NONE) then
2.479 - raise (Load_cplexFile
2.480 - ("constraint '"^(the (fst (the t)))^
2.481 - "'is not normed"))
2.482 - else
2.483 - raise (Load_cplexFile
2.484 - "constraint is not normed")
2.485 - end
2.486 - in
2.487 - if readToken () = SOME (TOKEN_KEYWORD, "ST")
2.488 - then
2.489 - readbody ()
2.490 - else
2.491 - raise (Load_cplexFile "ST expected")
2.492 - end
2.493 -
2.494 - fun readCmp () =
2.495 - let val c = readToken () in
2.496 - if c = NONE then NONE
2.497 - else if fst (the c) = TOKEN_CMP then
2.498 - SOME (str2cmp (snd (the c)))
2.499 - else (pushToken (the c); NONE)
2.500 - end
2.501 -
2.502 - fun skip_NL () =
2.503 - let val c = readToken () in
2.504 - if c <> NONE andalso fst (the c) = TOKEN_NL then
2.505 - skip_NL ()
2.506 - else
2.507 - (pushToken (the c); ())
2.508 - end
2.509 -
2.510 - fun is_var (cplexVar _) = true
2.511 - | is_var _ = false
2.512 -
2.513 - fun make_bounds c t1 t2 =
2.514 - cplexBound (t1, c, t2)
2.515 -
2.516 - fun readBound () =
2.517 - let
2.518 - val _ = skip_NL ()
2.519 - val t1 = readTerm ()
2.520 - in
2.521 - if t1 = NONE then NONE
2.522 - else
2.523 - let
2.524 - val c1 = readCmp ()
2.525 - in
2.526 - if c1 = NONE then
2.527 - let
2.528 - val c = readToken ()
2.529 - in
2.530 - if c = SOME (TOKEN_KEYWORD, "FREE") then
2.531 - SOME (
2.532 - cplexBounds (cplexNeg cplexInf,
2.533 - cplexLeq,
2.534 - the t1,
2.535 - cplexLeq,
2.536 - cplexInf))
2.537 - else
2.538 - raise (Load_cplexFile "FREE expected")
2.539 - end
2.540 - else
2.541 - let
2.542 - val t2 = readTerm ()
2.543 - in
2.544 - if t2 = NONE then
2.545 - raise (Load_cplexFile "term expected")
2.546 - else
2.547 - let val c2 = readCmp () in
2.548 - if c2 = NONE then
2.549 - SOME (make_bounds (the c1)
2.550 - (the t1)
2.551 - (the t2))
2.552 - else
2.553 - SOME (
2.554 - cplexBounds (the t1,
2.555 - the c1,
2.556 - the t2,
2.557 - the c2,
2.558 - the (readTerm())))
2.559 - end
2.560 - end
2.561 - end
2.562 - end
2.563 -
2.564 - fun readBounds () =
2.565 - let
2.566 - fun makestring b = "?"
2.567 - fun readbody () =
2.568 - let
2.569 - val b = readBound ()
2.570 - in
2.571 - if b = NONE then []
2.572 - else if (is_normed_Bounds (the b)) then
2.573 - (the b)::(readbody())
2.574 - else (
2.575 - raise (Load_cplexFile
2.576 - ("bounds are not normed in: "^
2.577 - (makestring (the b)))))
2.578 - end
2.579 - in
2.580 - if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
2.581 - readbody ()
2.582 - else raise (Load_cplexFile "BOUNDS expected")
2.583 - end
2.584 -
2.585 - fun readEnd () =
2.586 - if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
2.587 - else raise (Load_cplexFile "END expected")
2.588 -
2.589 - val result_Goal = readGoal ()
2.590 - val result_ST = readST ()
2.591 - val _ = ignore_NL := false
2.592 - val result_Bounds = readBounds ()
2.593 - val _ = ignore_NL := true
2.594 - val _ = readEnd ()
2.595 - val _ = TextIO.closeIn f
2.596 - in
2.597 - cplexProg (name, result_Goal, result_ST, result_Bounds)
2.598 - end
2.599 -
2.600 -fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
2.601 - let
2.602 - val f = TextIO.openOut filename
2.603 -
2.604 - fun basic_write s = TextIO.output(f, s)
2.605 -
2.606 - val linebuf = ref ""
2.607 - fun buf_flushline s =
2.608 - (basic_write (!linebuf);
2.609 - basic_write "\n";
2.610 - linebuf := s)
2.611 - fun buf_add s = linebuf := (!linebuf) ^ s
2.612 -
2.613 - fun write s =
2.614 - if (String.size s) + (String.size (!linebuf)) >= 250 then
2.615 - buf_flushline (" "^s)
2.616 - else
2.617 - buf_add s
2.618 -
2.619 - fun writeln s = (buf_add s; buf_flushline "")
2.620 -
2.621 - fun write_term (cplexVar x) = write x
2.622 - | write_term (cplexNum x) = write x
2.623 - | write_term cplexInf = write "inf"
2.624 - | write_term (cplexProd (cplexNum "1", b)) = write_term b
2.625 - | write_term (cplexProd (a, b)) =
2.626 - (write_term a; write " "; write_term b)
2.627 - | write_term (cplexNeg x) = (write " - "; write_term x)
2.628 - | write_term (cplexSum ts) = write_terms ts
2.629 - and write_terms [] = ()
2.630 - | write_terms (t::ts) =
2.631 - (if (not (is_Neg t)) then write " + " else ();
2.632 - write_term t; write_terms ts)
2.633 -
2.634 - fun write_goal (cplexMaximize term) =
2.635 - (writeln "MAXIMIZE"; write_term term; writeln "")
2.636 - | write_goal (cplexMinimize term) =
2.637 - (writeln "MINIMIZE"; write_term term; writeln "")
2.638 -
2.639 - fun write_cmp cplexLe = write "<"
2.640 - | write_cmp cplexLeq = write "<="
2.641 - | write_cmp cplexEq = write "="
2.642 - | write_cmp cplexGe = write ">"
2.643 - | write_cmp cplexGeq = write ">="
2.644 -
2.645 - fun write_constr (cplexConstr (cmp, (a,b))) =
2.646 - (write_term a;
2.647 - write " ";
2.648 - write_cmp cmp;
2.649 - write " ";
2.650 - write_term b)
2.651 -
2.652 - fun write_constraints [] = ()
2.653 - | write_constraints (c::cs) =
2.654 - (if (fst c <> NONE)
2.655 - then
2.656 - (write (the (fst c)); write ": ")
2.657 - else
2.658 - ();
2.659 - write_constr (snd c);
2.660 - writeln "";
2.661 - write_constraints cs)
2.662 -
2.663 - fun write_bounds [] = ()
2.664 - | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
2.665 - ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
2.666 - andalso (c1 = cplexLeq orelse c1 = cplexLe)
2.667 - andalso (c2 = cplexLeq orelse c2 = cplexLe)
2.668 - then
2.669 - (write_term t2; write " free")
2.670 - else
2.671 - (write_term t1; write " "; write_cmp c1; write " ";
2.672 - write_term t2; write " "; write_cmp c2; write " ";
2.673 - write_term t3)
2.674 - ); writeln ""; write_bounds bs)
2.675 - | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
2.676 - (write_term t1; write " ";
2.677 - write_cmp c; write " ";
2.678 - write_term t2; writeln ""; write_bounds bs)
2.679 -
2.680 - val _ = write_goal goal
2.681 - val _ = (writeln ""; writeln "ST")
2.682 - val _ = write_constraints constraints
2.683 - val _ = (writeln ""; writeln "BOUNDS")
2.684 - val _ = write_bounds bounds
2.685 - val _ = (writeln ""; writeln "END")
2.686 - val _ = TextIO.closeOut f
2.687 - in
2.688 - ()
2.689 - end
2.690 -
2.691 -fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
2.692 - if not (modulo_signed is_Num t2) andalso
2.693 - modulo_signed is_Num t1
2.694 - then
2.695 - [cplexConstr (rev_cmp c, (t2, t1))]
2.696 - else if (c = cplexLe orelse c = cplexLeq) andalso
2.697 - (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
2.698 - then
2.699 - []
2.700 - else if (c = cplexGe orelse c = cplexGeq) andalso
2.701 - (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
2.702 - then
2.703 - []
2.704 - else
2.705 - [constr]
2.706 -
2.707 -fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
2.708 - (norm_Constr(cplexConstr (c1, (t1, t2))))
2.709 - @ (norm_Constr(cplexConstr (c2, (t2, t3))))
2.710 - | bound2constr (cplexBound (t1, cplexEq, t2)) =
2.711 - (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
2.712 - @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
2.713 - | bound2constr (cplexBound (t1, c1, t2)) =
2.714 - norm_Constr(cplexConstr (c1, (t1,t2)))
2.715 -
2.716 -val emptyset = Symtab.empty
2.717 -
2.718 -fun singleton v = Symtab.update ((v, ()), emptyset)
2.719 -
2.720 -fun merge a b = Symtab.merge (op =) (a, b)
2.721 -
2.722 -fun mergemap f ts = Library.foldl
2.723 - (fn (table, x) => merge table (f x))
2.724 - (Symtab.empty, ts)
2.725 -
2.726 -fun diff a b = Symtab.foldl (fn (a, (k,v)) =>
2.727 - (Symtab.delete k a) handle UNDEF => a)
2.728 - (a, b)
2.729 -
2.730 -fun collect_vars (cplexVar v) = singleton v
2.731 - | collect_vars (cplexNeg t) = collect_vars t
2.732 - | collect_vars (cplexProd (t1, t2)) =
2.733 - merge (collect_vars t1) (collect_vars t2)
2.734 - | collect_vars (cplexSum ts) = mergemap collect_vars ts
2.735 - | collect_vars _ = emptyset
2.736 -
2.737 -(* Eliminates all nonfree bounds from the linear program and produces an
2.738 - equivalent program with only free bounds
2.739 - IF for the input program P holds: is_normed_cplexProg P *)
2.740 -fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
2.741 - let
2.742 - fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
2.743 - (collect_vars t1)
2.744 -
2.745 - val cvars = merge (collect_vars (term_of_goal goal))
2.746 - (mergemap collect_constr_vars constraints)
2.747 -
2.748 - fun collect_lower_bounded_vars
2.749 - (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
2.750 - singleton v
2.751 - | collect_lower_bounded_vars
2.752 - (cplexBound (_, cplexLe, cplexVar v)) =
2.753 - singleton v
2.754 - | collect_lower_bounded_vars
2.755 - (cplexBound (_, cplexLeq, cplexVar v)) =
2.756 - singleton v
2.757 - | collect_lower_bounded_vars
2.758 - (cplexBound (cplexVar v, cplexGe,_)) =
2.759 - singleton v
2.760 - | collect_lower_bounded_vars
2.761 - (cplexBound (cplexVar v, cplexGeq, _)) =
2.762 - singleton v
2.763 - | collect_lower_bounded_vars
2.764 - (cplexBound (cplexVar v, cplexEq, _)) =
2.765 - singleton v
2.766 - | collect_lower_bounded_vars _ = emptyset
2.767 -
2.768 - val lvars = mergemap collect_lower_bounded_vars bounds
2.769 - val positive_vars = diff cvars lvars
2.770 - val zero = cplexNum "0"
2.771 -
2.772 - fun make_pos_constr v =
2.773 - (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
2.774 -
2.775 - fun make_free_bound v =
2.776 - cplexBounds (cplexNeg cplexInf, cplexLeq,
2.777 - cplexVar v, cplexLeq,
2.778 - cplexInf)
2.779 -
2.780 - val pos_constrs = rev(Symtab.foldl
2.781 - (fn (l, (k,v)) => (make_pos_constr k) :: l)
2.782 - ([], positive_vars))
2.783 - val bound_constrs = map (fn x => (NONE, x))
2.784 - (List.concat (map bound2constr bounds))
2.785 - val constraints' = constraints @ pos_constrs @ bound_constrs
2.786 - val bounds' = rev(Symtab.foldl (fn (l, (v,_)) =>
2.787 - (make_free_bound v)::l)
2.788 - ([], cvars))
2.789 - in
2.790 - cplexProg (name, goal, constraints', bounds')
2.791 - end
2.792 -
2.793 -fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
2.794 - let
2.795 - fun relax cplexLe = cplexLeq
2.796 - | relax cplexGe = cplexGeq
2.797 - | relax x = x
2.798 -
2.799 - fun relax_constr (n, cplexConstr(c, (t1, t2))) =
2.800 - (n, cplexConstr(relax c, (t1, t2)))
2.801 -
2.802 - fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
2.803 - cplexBounds (t1, relax c1, t2, relax c2, t3)
2.804 - | relax_bounds (cplexBound (t1, c, t2)) =
2.805 - cplexBound (t1, relax c, t2)
2.806 - in
2.807 - cplexProg (name,
2.808 - goals,
2.809 - map relax_constr constrs,
2.810 - map relax_bounds bounds)
2.811 - end
2.812 -
2.813 -datatype cplexResult = Unbounded
2.814 - | Infeasible
2.815 - | Undefined
2.816 - | Optimal of string * ((string * string) list)
2.817 -
2.818 -fun is_separator x = forall (fn c => c = #"-") (String.explode x)
2.819 -
2.820 -fun is_sign x = (x = "+" orelse x = "-")
2.821 -
2.822 -fun is_colon x = (x = ":")
2.823 -
2.824 -fun is_resultsymbol a =
2.825 - let
2.826 - val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
2.827 - fun is_symbol_char c = Char.isAlphaNum c orelse
2.828 - exists (fn d => d=c) symbol_char
2.829 - fun is_symbol_start c = is_symbol_char c andalso
2.830 - not (Char.isDigit c) andalso
2.831 - not (c= #".") andalso
2.832 - not (c= #"-")
2.833 - val b = String.explode a
2.834 - in
2.835 - b <> [] andalso is_symbol_start (hd b) andalso
2.836 - forall is_symbol_char b
2.837 - end
2.838 -
2.839 -val TOKEN_SIGN = 100
2.840 -val TOKEN_COLON = 101
2.841 -val TOKEN_SEPARATOR = 102
2.842 -
2.843 -fun load_cplexResult name =
2.844 - let
2.845 - val flist = [(is_NL, TOKEN_NL),
2.846 - (is_blank, TOKEN_BLANK),
2.847 - (is_num, TOKEN_NUM),
2.848 - (is_sign, TOKEN_SIGN),
2.849 - (is_colon, TOKEN_COLON),
2.850 - (is_cmp, TOKEN_CMP),
2.851 - (is_resultsymbol, TOKEN_SYMBOL),
2.852 - (is_separator, TOKEN_SEPARATOR)]
2.853 -
2.854 - val tokenize = tokenize_general flist
2.855 -
2.856 - val f = TextIO.openIn name
2.857 -
2.858 - val rest = ref []
2.859 -
2.860 - fun readToken_helper () =
2.861 - if length (!rest) > 0 then
2.862 - let val u = hd (!rest) in
2.863 - (
2.864 - rest := tl (!rest);
2.865 - SOME u
2.866 - )
2.867 - end
2.868 - else
2.869 - let val s = TextIO.inputLine f in
2.870 - if s = "" then NONE else (rest := tokenize s; readToken_helper())
2.871 - end
2.872 -
2.873 - fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
2.874 -
2.875 - fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
2.876 -
2.877 - fun readToken () =
2.878 - let val t = readToken_helper () in
2.879 - if is_tt t TOKEN_BLANK then
2.880 - readToken ()
2.881 - else if is_tt t TOKEN_NL then
2.882 - let val t2 = readToken_helper () in
2.883 - if is_tt t2 TOKEN_SIGN then
2.884 - (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
2.885 - else
2.886 - (pushToken t2; t)
2.887 - end
2.888 - else if is_tt t TOKEN_SIGN then
2.889 - let val t2 = readToken_helper () in
2.890 - if is_tt t2 TOKEN_NUM then
2.891 - (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
2.892 - else
2.893 - (pushToken t2; t)
2.894 - end
2.895 - else
2.896 - t
2.897 - end
2.898 -
2.899 - fun readRestOfLine P =
2.900 - let
2.901 - val t = readToken ()
2.902 - in
2.903 - if is_tt t TOKEN_NL orelse t = NONE
2.904 - then P
2.905 - else readRestOfLine P
2.906 - end
2.907 -
2.908 - fun readHeader () =
2.909 - let
2.910 - fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
2.911 - fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
2.912 - val t1 = readToken ()
2.913 - val t2 = readToken ()
2.914 - in
2.915 - if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
2.916 - then
2.917 - case to_upper (snd (the t1)) of
2.918 - "STATUS" => (readStatus ())::(readHeader ())
2.919 - | "OBJECTIVE" => (readObjective())::(readHeader ())
2.920 - | _ => (readRestOfLine (); readHeader ())
2.921 - else
2.922 - (pushToken t2; pushToken t1; [])
2.923 - end
2.924 -
2.925 - fun skip_until_sep () =
2.926 - let val x = readToken () in
2.927 - if is_tt x TOKEN_SEPARATOR then
2.928 - readRestOfLine ()
2.929 - else
2.930 - skip_until_sep ()
2.931 - end
2.932 -
2.933 - fun load_value () =
2.934 - let
2.935 - val t1 = readToken ()
2.936 - val t2 = readToken ()
2.937 - in
2.938 - if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
2.939 - let
2.940 - val t = readToken ()
2.941 - val state = if is_tt t TOKEN_NL then readToken () else t
2.942 - val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
2.943 - val k = readToken ()
2.944 - in
2.945 - if is_tt k TOKEN_NUM then
2.946 - readRestOfLine (SOME (snd (the t2), snd (the k)))
2.947 - else
2.948 - raise (Load_cplexResult "number expected")
2.949 - end
2.950 - else
2.951 - (pushToken t2; pushToken t1; NONE)
2.952 - end
2.953 -
2.954 - fun load_values () =
2.955 - let val v = load_value () in
2.956 - if v = NONE then [] else (the v)::(load_values ())
2.957 - end
2.958 -
2.959 - val header = readHeader ()
2.960 -
2.961 - val result =
2.962 - case assoc (header, "STATUS") of
2.963 - SOME "INFEASIBLE" => Infeasible
2.964 - | SOME "UNBOUNDED" => Unbounded
2.965 - | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")),
2.966 - (skip_until_sep ();
2.967 - skip_until_sep ();
2.968 - load_values ()))
2.969 - | _ => Undefined
2.970 -
2.971 - val _ = TextIO.closeIn f
2.972 - in
2.973 - result
2.974 - end
2.975 - handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
2.976 - | OPTION => raise (Load_cplexResult "OPTION")
2.977 - | x => raise x
2.978 -
2.979 -exception Execute of string;
2.980 -
2.981 -fun execute_cplex lpname resultname =
2.982 -let
2.983 - fun wrap s = "\""^s^"\""
2.984 - val cplex_path = getenv "CPLEX"
2.985 - val cplex = if cplex_path = "" then "glpsol" else cplex_path
2.986 - val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
2.987 -in
2.988 - execute command
2.989 -end
2.990 -
2.991 -fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])))
2.992 -
2.993 -fun solve prog =
2.994 - let
2.995 - val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
2.996 - val lpname = tmp_file (name^".lp")
2.997 - val resultname = tmp_file (name^".result")
2.998 - val _ = save_cplexFile lpname prog
2.999 - val answer = execute_cplex lpname resultname
2.1000 - in
2.1001 - let
2.1002 - val result = load_cplexResult resultname
2.1003 - val _ = OS.FileSys.remove lpname
2.1004 - val _ = OS.FileSys.remove resultname
2.1005 - in
2.1006 - result
2.1007 - end
2.1008 - handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
2.1009 - | _ => raise (Execute answer)
2.1010 - end
2.1011 -end;
2.1012 -
2.1013 -val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
2.1014 -val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
2.1015 -val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
2.1016 -
2.1017 -fun loadcplex () = Cplex.relax_strict_ineqs
2.1018 - (Cplex.load_cplexFile demofile)
2.1019 -
2.1020 -fun writecplex lp = Cplex.save_cplexFile demoout lp
2.1021 -
2.1022 -fun test () =
2.1023 - let
2.1024 - val lp = loadcplex ()
2.1025 - val lp2 = Cplex.elim_nonfree_bounds lp
2.1026 - in
2.1027 - writecplex lp2
2.1028 - end
2.1029 -
2.1030 -fun loadresult () = Cplex.load_cplexResult demoresult;
3.1 --- a/src/HOL/Matrix/CplexMatrixConverter.ML Mon Mar 07 16:55:36 2005 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,132 +0,0 @@
3.4 -signature MATRIX_BUILDER =
3.5 -sig
3.6 - type vector
3.7 - type matrix
3.8 -
3.9 - val empty_vector : vector
3.10 - val empty_matrix : matrix
3.11 -
3.12 - exception Nat_expected of int
3.13 - val set_elem : vector -> int -> string -> vector
3.14 - val set_vector : matrix -> int -> vector -> matrix
3.15 -end;
3.16 -
3.17 -signature CPLEX_MATRIX_CONVERTER =
3.18 -sig
3.19 - structure cplex : CPLEX
3.20 - structure matrix_builder : MATRIX_BUILDER
3.21 - type vector = matrix_builder.vector
3.22 - type matrix = matrix_builder.matrix
3.23 - type naming = int * (int -> string) * (string -> int)
3.24 -
3.25 - exception Converter of string
3.26 -
3.27 - (* program must fulfill is_normed_cplexProg and must be an element of the image of elim_nonfree_bounds *)
3.28 - (* convert_prog maximize c A b naming *)
3.29 - val convert_prog : cplex.cplexProg -> bool * vector * matrix * vector * naming
3.30 -
3.31 - (* results must be optimal, converts_results returns the optimal value as string and the solution as vector *)
3.32 - (* convert_results results name2index *)
3.33 - val convert_results : cplex.cplexResult -> (string -> int) -> string * vector
3.34 -end;
3.35 -
3.36 -functor MAKE_CPLEX_MATRIX_CONVERTER (structure cplex: CPLEX and matrix_builder: MATRIX_BUILDER) : CPLEX_MATRIX_CONVERTER =
3.37 -struct
3.38 -
3.39 -structure cplex = cplex
3.40 -structure matrix_builder = matrix_builder
3.41 -type matrix = matrix_builder.matrix
3.42 -type vector = matrix_builder.vector
3.43 -type naming = int * (int -> string) * (string -> int)
3.44 -
3.45 -open matrix_builder
3.46 -open cplex
3.47 -
3.48 -exception Converter of string;
3.49 -
3.50 -structure Inttab = TableFun(type key = int val ord = int_ord);
3.51 -
3.52 -fun neg_term (cplexNeg t) = t
3.53 - | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
3.54 - | neg_term t = cplexNeg t
3.55 -
3.56 -fun convert_prog (cplexProg (s, goal, constrs, bounds)) =
3.57 - let
3.58 - fun build_naming index i2s s2i [] = (index, i2s, s2i)
3.59 - | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
3.60 - = build_naming (index+1) (Inttab.update ((index, v), i2s)) (Symtab.update_new ((v, index), s2i)) bounds
3.61 - | build_naming _ _ _ _ = raise (Converter "nonfree bound")
3.62 -
3.63 - val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds
3.64 -
3.65 - fun i2s i = case Inttab.lookup (i2s_tab, i) of NONE => raise (Converter "index not found")
3.66 - | SOME n => n
3.67 - fun s2i s = case Symtab.lookup (s2i_tab, s) of NONE => raise (Converter ("name not found: "^s))
3.68 - | SOME i => i
3.69 - fun num2str positive (cplexNeg t) = num2str (not positive) t
3.70 - | num2str positive (cplexNum num) = if positive then num else "-"^num
3.71 - | num2str _ _ = raise (Converter "term is not a (possibly signed) number")
3.72 -
3.73 - fun setprod vec positive (cplexNeg t) = setprod vec (not positive) t
3.74 - | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1")
3.75 - | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) =
3.76 - set_elem vec (s2i v) (if positive then num else "-"^num)
3.77 - | setprod _ _ _ = raise (Converter "term is not a normed product")
3.78 -
3.79 - fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts)
3.80 - | sum2vec t = setprod empty_vector true t
3.81 -
3.82 - fun constrs2Ab j A b [] = (A, b)
3.83 - | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) =
3.84 - constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs
3.85 - | constrs2Ab j A b ((_, cplexConstr (cplexGeq, (t1,t2)))::cs) =
3.86 - constrs2Ab (j+1) (set_vector A j (sum2vec (neg_term t1))) (set_elem b j (num2str true (neg_term t2))) cs
3.87 - | constrs2Ab j A b ((_, cplexConstr (cplexEq, (t1,t2)))::cs) =
3.88 - constrs2Ab j A b ((NONE, cplexConstr (cplexLeq, (t1,t2)))::
3.89 - (NONE, cplexConstr (cplexGeq, (t1, t2)))::cs)
3.90 - | constrs2Ab _ _ _ _ = raise (Converter "no strict constraints allowed")
3.91 -
3.92 - val (A, b) = constrs2Ab 0 empty_matrix empty_vector constrs
3.93 -
3.94 - val (goal_maximize, goal_term) =
3.95 - case goal of
3.96 - (cplexMaximize t) => (true, t)
3.97 - | (cplexMinimize t) => (false, t)
3.98 - in
3.99 - (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i))
3.100 - end
3.101 -
3.102 -fun convert_results (cplex.Optimal (opt, entries)) name2index =
3.103 - let
3.104 - fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value)
3.105 - in
3.106 - (opt, Library.foldl setv (matrix_builder.empty_vector, entries))
3.107 - end
3.108 - | convert_results _ _ = raise (Converter "No optimal result")
3.109 -
3.110 -
3.111 -end;
3.112 -
3.113 -structure SimpleMatrixBuilder : MATRIX_BUILDER =
3.114 -struct
3.115 -type vector = (int * string) list
3.116 -type matrix = (int * vector) list
3.117 -
3.118 -val empty_matrix = []
3.119 -val empty_vector = []
3.120 -
3.121 -exception Nat_expected of int;
3.122 -
3.123 -fun set_elem v i s = v @ [(i, s)]
3.124 -
3.125 -fun set_vector m i v = m @ [(i, v)]
3.126 -
3.127 -end;
3.128 -
3.129 -
3.130 -
3.131 -structure SimpleCplexMatrixConverter = MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder);
3.132 -
3.133 -
3.134 -
3.135 -
4.1 --- a/src/HOL/Matrix/ExactFloatingPoint.ML Mon Mar 07 16:55:36 2005 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,215 +0,0 @@
4.4 -structure ExactFloatingPoint :
4.5 -sig
4.6 - exception Destruct_floatstr of string
4.7 -
4.8 - val destruct_floatstr : (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
4.9 -
4.10 - exception Floating_point of string
4.11 -
4.12 - type floatrep = IntInf.int * IntInf.int
4.13 - val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
4.14 - val approx_decstr_by_bin : int -> string -> floatrep * floatrep
4.15 -end
4.16 -=
4.17 -struct
4.18 -
4.19 -fun fst (a,b) = a
4.20 -fun snd (a,b) = b
4.21 -
4.22 -val filter = List.filter;
4.23 -
4.24 -exception Destruct_floatstr of string;
4.25 -
4.26 -fun destruct_floatstr isDigit isExp number =
4.27 - let
4.28 - val numlist = filter (not o Char.isSpace) (String.explode number)
4.29 -
4.30 - fun countsigns ((#"+")::cs) = countsigns cs
4.31 - | countsigns ((#"-")::cs) =
4.32 - let
4.33 - val (positive, rest) = countsigns cs
4.34 - in
4.35 - (not positive, rest)
4.36 - end
4.37 - | countsigns cs = (true, cs)
4.38 -
4.39 - fun readdigits [] = ([], [])
4.40 - | readdigits (q as c::cs) =
4.41 - if (isDigit c) then
4.42 - let
4.43 - val (digits, rest) = readdigits cs
4.44 - in
4.45 - (c::digits, rest)
4.46 - end
4.47 - else
4.48 - ([], q)
4.49 -
4.50 - fun readfromexp_helper cs =
4.51 - let
4.52 - val (positive, rest) = countsigns cs
4.53 - val (digits, rest') = readdigits rest
4.54 - in
4.55 - case rest' of
4.56 - [] => (positive, digits)
4.57 - | _ => raise (Destruct_floatstr number)
4.58 - end
4.59 -
4.60 - fun readfromexp [] = (true, [])
4.61 - | readfromexp (c::cs) =
4.62 - if isExp c then
4.63 - readfromexp_helper cs
4.64 - else
4.65 - raise (Destruct_floatstr number)
4.66 -
4.67 - fun readfromdot [] = ([], readfromexp [])
4.68 - | readfromdot ((#".")::cs) =
4.69 - let
4.70 - val (digits, rest) = readdigits cs
4.71 - val exp = readfromexp rest
4.72 - in
4.73 - (digits, exp)
4.74 - end
4.75 - | readfromdot cs = readfromdot ((#".")::cs)
4.76 -
4.77 - val (positive, numlist) = countsigns numlist
4.78 - val (digits1, numlist) = readdigits numlist
4.79 - val (digits2, exp) = readfromdot numlist
4.80 - in
4.81 - (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
4.82 - end
4.83 -
4.84 -type floatrep = IntInf.int * IntInf.int
4.85 -
4.86 -exception Floating_point of string;
4.87 -
4.88 -val ln2_10 = (Math.ln 10.0)/(Math.ln 2.0)
4.89 -
4.90 -fun intmul a b = IntInf.* (a,b)
4.91 -fun intsub a b = IntInf.- (a,b)
4.92 -fun intadd a b = IntInf.+ (a,b)
4.93 -fun intpow a b = IntInf.pow (a, IntInf.toInt b);
4.94 -fun intle a b = IntInf.<= (a, b);
4.95 -fun intless a b = IntInf.< (a, b);
4.96 -fun intneg a = IntInf.~ a;
4.97 -val zero = IntInf.fromInt 0;
4.98 -val one = IntInf.fromInt 1;
4.99 -val two = IntInf.fromInt 2;
4.100 -val ten = IntInf.fromInt 10;
4.101 -val five = IntInf.fromInt 5;
4.102 -
4.103 -fun find_most_significant q r =
4.104 - let
4.105 - fun int2real i =
4.106 - case Real.fromString (IntInf.toString i) of
4.107 - SOME r => r
4.108 - | NONE => raise (Floating_point "int2real")
4.109 - fun subtract (q, r) (q', r') =
4.110 - if intle r r' then
4.111 - (intsub q (intmul q' (intpow ten (intsub r' r))), r)
4.112 - else
4.113 - (intsub (intmul q (intpow ten (intsub r r'))) q', r')
4.114 - fun bin2dec d =
4.115 - if intle zero d then
4.116 - (intpow two d, zero)
4.117 - else
4.118 - (intpow five (intneg d), d)
4.119 -
4.120 - val L = IntInf.fromInt (Real.floor (int2real (IntInf.fromInt (IntInf.log2 q)) + (int2real r) * ln2_10))
4.121 - val L1 = intadd L one
4.122 -
4.123 - val (q1, r1) = subtract (q, r) (bin2dec L1)
4.124 - in
4.125 - if intle zero q1 then
4.126 - let
4.127 - val (q2, r2) = subtract (q, r) (bin2dec (intadd L1 one))
4.128 - in
4.129 - if intle zero q2 then
4.130 - raise (Floating_point "find_most_significant")
4.131 - else
4.132 - (L1, (q1, r1))
4.133 - end
4.134 - else
4.135 - let
4.136 - val (q0, r0) = subtract (q, r) (bin2dec L)
4.137 - in
4.138 - if intle zero q0 then
4.139 - (L, (q0, r0))
4.140 - else
4.141 - raise (Floating_point "find_most_significant")
4.142 - end
4.143 - end
4.144 -
4.145 -fun approx_dec_by_bin n (q,r) =
4.146 - let
4.147 - fun addseq acc d' [] = acc
4.148 - | addseq acc d' (d::ds) = addseq (intadd acc (intpow two (intsub d d'))) d' ds
4.149 -
4.150 - fun seq2bin [] = (zero, zero)
4.151 - | seq2bin (d::ds) = (intadd (addseq zero d ds) one, d)
4.152 -
4.153 - fun approx d_seq d0 precision (q,r) =
4.154 - if q = zero then
4.155 - let val x = seq2bin d_seq in
4.156 - (x, x)
4.157 - end
4.158 - else
4.159 - let
4.160 - val (d, (q', r')) = find_most_significant q r
4.161 - in
4.162 - if intless precision (intsub d0 d) then
4.163 - let
4.164 - val d' = intsub d0 precision
4.165 - val x1 = seq2bin (d_seq)
4.166 - val x2 = (intadd (intmul (fst x1) (intpow two (intsub (snd x1) d'))) one, d') (* = seq2bin (d'::d_seq) *)
4.167 - in
4.168 - (x1, x2)
4.169 - end
4.170 - else
4.171 - approx (d::d_seq) d0 precision (q', r')
4.172 - end
4.173 -
4.174 - fun approx_start precision (q, r) =
4.175 - if q = zero then
4.176 - ((zero, zero), (zero, zero))
4.177 - else
4.178 - let
4.179 - val (d, (q', r')) = find_most_significant q r
4.180 - in
4.181 - if intle precision zero then
4.182 - let
4.183 - val x1 = seq2bin [d]
4.184 - in
4.185 - if q' = zero then
4.186 - (x1, x1)
4.187 - else
4.188 - (x1, seq2bin [intadd d one])
4.189 - end
4.190 - else
4.191 - approx [d] d precision (q', r')
4.192 - end
4.193 - in
4.194 - if intle zero q then
4.195 - approx_start n (q,r)
4.196 - else
4.197 - let
4.198 - val ((a1,b1), (a2, b2)) = approx_start n (intneg q, r)
4.199 - in
4.200 - ((intneg a2, b2), (intneg a1, b1))
4.201 - end
4.202 - end
4.203 -
4.204 -fun approx_decstr_by_bin n decstr =
4.205 - let
4.206 - fun str2int s = case IntInf.fromString s of SOME x => x | NONE => zero
4.207 - fun signint p x = if p then x else intneg x
4.208 -
4.209 - val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
4.210 - val s = IntInf.fromInt (size d2)
4.211 -
4.212 - val q = signint p (intadd (intmul (str2int d1) (intpow ten s)) (str2int d2))
4.213 - val r = intsub (signint ep (str2int e)) s
4.214 - in
4.215 - approx_dec_by_bin (IntInf.fromInt n) (q,r)
4.216 - end
4.217 -
4.218 -end;
5.1 --- a/src/HOL/Matrix/Float.thy Mon Mar 07 16:55:36 2005 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,508 +0,0 @@
5.4 -theory Float = Hyperreal:
5.5 -
5.6 -constdefs
5.7 - pow2 :: "int \<Rightarrow> real"
5.8 - "pow2 a == if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a))))"
5.9 - float :: "int * int \<Rightarrow> real"
5.10 - "float x == (real (fst x)) * (pow2 (snd x))"
5.11 -
5.12 -lemma pow2_0[simp]: "pow2 0 = 1"
5.13 -by (simp add: pow2_def)
5.14 -
5.15 -lemma pow2_1[simp]: "pow2 1 = 2"
5.16 -by (simp add: pow2_def)
5.17 -
5.18 -lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
5.19 -by (simp add: pow2_def)
5.20 -
5.21 -lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
5.22 -proof -
5.23 - have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
5.24 - have g: "! a b. a - -1 = a + (1::int)" by arith
5.25 - have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
5.26 - apply (auto, induct_tac n)
5.27 - apply (simp_all add: pow2_def)
5.28 - apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
5.29 - apply (auto simp add: h)
5.30 - apply arith
5.31 - done
5.32 - show ?thesis
5.33 - proof (induct a)
5.34 - case (1 n)
5.35 - from pos show ?case by (simp add: ring_eq_simps)
5.36 - next
5.37 - case (2 n)
5.38 - show ?case
5.39 - apply (auto)
5.40 - apply (subst pow2_neg[of "- int n"])
5.41 - apply (subst pow2_neg[of "-1 - int n"])
5.42 - apply (auto simp add: g pos)
5.43 - done
5.44 - qed
5.45 -qed
5.46 -
5.47 -lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
5.48 -proof (induct b)
5.49 - case (1 n)
5.50 - show ?case
5.51 - proof (induct n)
5.52 - case 0
5.53 - show ?case by simp
5.54 - next
5.55 - case (Suc m)
5.56 - show ?case by (auto simp add: ring_eq_simps pow2_add1 prems)
5.57 - qed
5.58 -next
5.59 - case (2 n)
5.60 - show ?case
5.61 - proof (induct n)
5.62 - case 0
5.63 - show ?case
5.64 - apply (auto)
5.65 - apply (subst pow2_neg[of "a + -1"])
5.66 - apply (subst pow2_neg[of "-1"])
5.67 - apply (simp)
5.68 - apply (insert pow2_add1[of "-a"])
5.69 - apply (simp add: ring_eq_simps)
5.70 - apply (subst pow2_neg[of "-a"])
5.71 - apply (simp)
5.72 - done
5.73 - case (Suc m)
5.74 - have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
5.75 - have b: "int m - -2 = 1 + (int m + 1)" by arith
5.76 - show ?case
5.77 - apply (auto)
5.78 - apply (subst pow2_neg[of "a + (-2 - int m)"])
5.79 - apply (subst pow2_neg[of "-2 - int m"])
5.80 - apply (auto simp add: ring_eq_simps)
5.81 - apply (subst a)
5.82 - apply (subst b)
5.83 - apply (simp only: pow2_add1)
5.84 - apply (subst pow2_neg[of "int m - a + 1"])
5.85 - apply (subst pow2_neg[of "int m + 1"])
5.86 - apply auto
5.87 - apply (insert prems)
5.88 - apply (auto simp add: ring_eq_simps)
5.89 - done
5.90 - qed
5.91 -qed
5.92 -
5.93 -lemma "float (a, e) + float (b, e) = float (a + b, e)"
5.94 -by (simp add: float_def ring_eq_simps)
5.95 -
5.96 -constdefs
5.97 - int_of_real :: "real \<Rightarrow> int"
5.98 - "int_of_real x == SOME y. real y = x"
5.99 - real_is_int :: "real \<Rightarrow> bool"
5.100 - "real_is_int x == ? (u::int). x = real u"
5.101 -
5.102 -lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
5.103 -by (auto simp add: real_is_int_def int_of_real_def)
5.104 -
5.105 -lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
5.106 -by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
5.107 -
5.108 -lemma pow2_int: "pow2 (int c) = (2::real)^c"
5.109 -by (simp add: pow2_def)
5.110 -
5.111 -lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
5.112 -by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
5.113 -
5.114 -lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
5.115 -by (auto simp add: real_is_int_def int_of_real_def)
5.116 -
5.117 -lemma int_of_real_real[simp]: "int_of_real (real x) = x"
5.118 -by (simp add: int_of_real_def)
5.119 -
5.120 -lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
5.121 -by (auto simp add: int_of_real_def real_is_int_def)
5.122 -
5.123 -lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
5.124 -by (auto simp add: int_of_real_def real_is_int_def)
5.125 -
5.126 -lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
5.127 -apply (subst real_is_int_def2)
5.128 -apply (simp add: real_is_int_add_int_of_real real_int_of_real)
5.129 -done
5.130 -
5.131 -lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
5.132 -by (auto simp add: int_of_real_def real_is_int_def)
5.133 -
5.134 -lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
5.135 -apply (subst real_is_int_def2)
5.136 -apply (simp add: int_of_real_sub real_int_of_real)
5.137 -done
5.138 -
5.139 -lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
5.140 -by (auto simp add: real_is_int_def)
5.141 -
5.142 -lemma int_of_real_mult:
5.143 - assumes "real_is_int a" "real_is_int b"
5.144 - shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
5.145 -proof -
5.146 - from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
5.147 - from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
5.148 - from a obtain a'::int where a':"a = real a'" by auto
5.149 - from b obtain b'::int where b':"b = real b'" by auto
5.150 - have r: "real a' * real b' = real (a' * b')" by auto
5.151 - show ?thesis
5.152 - apply (simp add: a' b')
5.153 - apply (subst r)
5.154 - apply (simp only: int_of_real_real)
5.155 - done
5.156 -qed
5.157 -
5.158 -lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
5.159 -apply (subst real_is_int_def2)
5.160 -apply (simp add: int_of_real_mult)
5.161 -done
5.162 -
5.163 -lemma real_is_int_0[simp]: "real_is_int (0::real)"
5.164 -by (simp add: real_is_int_def int_of_real_def)
5.165 -
5.166 -lemma real_is_int_1[simp]: "real_is_int (1::real)"
5.167 -proof -
5.168 - have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
5.169 - also have "\<dots> = True" by (simp only: real_is_int_real)
5.170 - ultimately show ?thesis by auto
5.171 -qed
5.172 -
5.173 -lemma real_is_int_n1: "real_is_int (-1::real)"
5.174 -proof -
5.175 - have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
5.176 - also have "\<dots> = True" by (simp only: real_is_int_real)
5.177 - ultimately show ?thesis by auto
5.178 -qed
5.179 -
5.180 -lemma real_is_int_number_of[simp]: "real_is_int ((number_of::bin\<Rightarrow>real) x)"
5.181 -proof -
5.182 - have neg1: "real_is_int (-1::real)"
5.183 - proof -
5.184 - have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
5.185 - also have "\<dots> = True" by (simp only: real_is_int_real)
5.186 - ultimately show ?thesis by auto
5.187 - qed
5.188 -
5.189 - {
5.190 - fix x::int
5.191 - have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
5.192 - apply (simp add: number_of_eq)
5.193 - apply (subst Abs_Bin_inverse)
5.194 - apply (simp add: Bin_def)
5.195 - apply (induct x)
5.196 - apply (induct_tac n)
5.197 - apply (simp)
5.198 - apply (simp)
5.199 - apply (induct_tac n)
5.200 - apply (simp add: neg1)
5.201 - proof -
5.202 - fix n :: nat
5.203 - assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
5.204 - have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
5.205 - show "real_is_int (of_int (- (int (Suc (Suc n)))))"
5.206 - apply (simp only: s of_int_add)
5.207 - apply (rule real_is_int_add)
5.208 - apply (simp add: neg1)
5.209 - apply (simp only: rn)
5.210 - done
5.211 - qed
5.212 - }
5.213 - note Abs_Bin = this
5.214 - {
5.215 - fix x :: bin
5.216 - have "? u. x = Abs_Bin u"
5.217 - apply (rule exI[where x = "Rep_Bin x"])
5.218 - apply (simp add: Rep_Bin_inverse)
5.219 - done
5.220 - }
5.221 - then obtain u::int where "x = Abs_Bin u" by auto
5.222 - with Abs_Bin show ?thesis by auto
5.223 -qed
5.224 -
5.225 -lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
5.226 -by (simp add: int_of_real_def)
5.227 -
5.228 -lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
5.229 -proof -
5.230 - have 1: "(1::real) = real (1::int)" by auto
5.231 - show ?thesis by (simp only: 1 int_of_real_real)
5.232 -qed
5.233 -
5.234 -lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
5.235 -proof -
5.236 - have "real_is_int (number_of b)" by simp
5.237 - then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
5.238 - then obtain u::int where u:"number_of b = real u" by auto
5.239 - have "number_of b = real ((number_of b)::int)"
5.240 - by (simp add: number_of_eq real_of_int_def)
5.241 - have ub: "number_of b = real ((number_of b)::int)"
5.242 - by (simp add: number_of_eq real_of_int_def)
5.243 - from uu u ub have unb: "u = number_of b"
5.244 - by blast
5.245 - have "int_of_real (number_of b) = u" by (simp add: u)
5.246 - with unb show ?thesis by simp
5.247 -qed
5.248 -
5.249 -lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
5.250 - apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
5.251 - apply (simp_all add: pow2_def even_def real_is_int_def ring_eq_simps)
5.252 - apply (auto)
5.253 -proof -
5.254 - fix q::int
5.255 - have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
5.256 - show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
5.257 - by (simp add: a)
5.258 -qed
5.259 -
5.260 -consts
5.261 - norm_float :: "int*int \<Rightarrow> int*int"
5.262 -
5.263 -lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
5.264 -apply (subst split_div, auto)
5.265 -apply (subst split_zdiv, auto)
5.266 -apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
5.267 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
5.268 -done
5.269 -
5.270 -lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
5.271 -apply (subst split_mod, auto)
5.272 -apply (subst split_zmod, auto)
5.273 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
5.274 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
5.275 -done
5.276 -
5.277 -lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
5.278 -by arith
5.279 -
5.280 -lemma terminating_norm_float: "\<forall>a. (a::int) \<noteq> 0 \<and> even a \<longrightarrow> a \<noteq> 0 \<and> \<bar>a div 2\<bar> < \<bar>a\<bar>"
5.281 -apply (auto)
5.282 -apply (rule abs_div_2_less)
5.283 -apply (auto)
5.284 -done
5.285 -
5.286 -ML {* simp_depth_limit := 2 *}
5.287 -recdef norm_float "measure (% (a,b). nat (abs a))"
5.288 - "norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
5.289 -(hints simp: terminating_norm_float)
5.290 -ML {* simp_depth_limit := 1000 *}
5.291 -
5.292 -
5.293 -lemma norm_float: "float x = float (norm_float x)"
5.294 -proof -
5.295 - {
5.296 - fix a b :: int
5.297 - have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
5.298 - proof (induct a b rule: norm_float.induct)
5.299 - case (1 u v)
5.300 - show ?case
5.301 - proof cases
5.302 - assume u: "u \<noteq> 0 \<and> even u"
5.303 - with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
5.304 - with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
5.305 - then show ?thesis
5.306 - apply (subst norm_float.simps)
5.307 - apply (simp add: ind)
5.308 - done
5.309 - next
5.310 - assume "~(u \<noteq> 0 \<and> even u)"
5.311 - then show ?thesis
5.312 - by (simp add: prems float_def)
5.313 - qed
5.314 - qed
5.315 - }
5.316 - note helper = this
5.317 - have "? a b. x = (a,b)" by auto
5.318 - then obtain a b where "x = (a, b)" by blast
5.319 - then show ?thesis by (simp only: helper)
5.320 -qed
5.321 -
5.322 -lemma pow2_int: "pow2 (int n) = 2^n"
5.323 - by (simp add: pow2_def)
5.324 -
5.325 -lemma float_add:
5.326 - "float (a1, e1) + float (a2, e2) =
5.327 - (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
5.328 - else float (a1*2^(nat (e1-e2))+a2, e2))"
5.329 - apply (simp add: float_def ring_eq_simps)
5.330 - apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
5.331 - done
5.332 -
5.333 -lemma float_mult:
5.334 - "float (a1, e1) * float (a2, e2) =
5.335 - (float (a1 * a2, e1 + e2))"
5.336 - by (simp add: float_def pow2_add)
5.337 -
5.338 -lemma float_minus:
5.339 - "- (float (a,b)) = float (-a, b)"
5.340 - by (simp add: float_def)
5.341 -
5.342 -lemma zero_less_pow2:
5.343 - "0 < pow2 x"
5.344 -proof -
5.345 - {
5.346 - fix y
5.347 - have "0 <= y \<Longrightarrow> 0 < pow2 y"
5.348 - by (induct y, induct_tac n, simp_all add: pow2_add)
5.349 - }
5.350 - note helper=this
5.351 - show ?thesis
5.352 - apply (case_tac "0 <= x")
5.353 - apply (simp add: helper)
5.354 - apply (subst pow2_neg)
5.355 - apply (simp add: helper)
5.356 - done
5.357 -qed
5.358 -
5.359 -lemma zero_le_float:
5.360 - "(0 <= float (a,b)) = (0 <= a)"
5.361 - apply (auto simp add: float_def)
5.362 - apply (auto simp add: zero_le_mult_iff zero_less_pow2)
5.363 - apply (insert zero_less_pow2[of b])
5.364 - apply (simp_all)
5.365 - done
5.366 -
5.367 -lemma float_abs:
5.368 - "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
5.369 - apply (auto simp add: abs_if)
5.370 - apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
5.371 - done
5.372 -
5.373 -lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
5.374 - by auto
5.375 -
5.376 -lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
5.377 - by simp
5.378 -
5.379 -lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
5.380 - by simp
5.381 -
5.382 -lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
5.383 - by simp
5.384 -
5.385 -lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
5.386 - by simp
5.387 -
5.388 -lemma int_pow_0: "(a::int)^(Numeral0) = 1"
5.389 - by simp
5.390 -
5.391 -lemma int_pow_1: "(a::int)^(Numeral1) = a"
5.392 - by simp
5.393 -
5.394 -lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
5.395 - by simp
5.396 -
5.397 -lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
5.398 - by simp
5.399 -
5.400 -lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
5.401 - by simp
5.402 -
5.403 -lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
5.404 - by simp
5.405 -
5.406 -lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
5.407 - by simp
5.408 -
5.409 -lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
5.410 -proof -
5.411 - have 1:"((-1)::nat) = 0"
5.412 - by simp
5.413 - show ?thesis by (simp add: 1)
5.414 -qed
5.415 -
5.416 -lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
5.417 - by simp
5.418 -
5.419 -lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
5.420 - by simp
5.421 -
5.422 -lemma lift_bool: "x \<Longrightarrow> x=True"
5.423 - by simp
5.424 -
5.425 -lemma nlift_bool: "~x \<Longrightarrow> x=False"
5.426 - by simp
5.427 -
5.428 -lemma not_false_eq_true: "(~ False) = True" by simp
5.429 -
5.430 -lemma not_true_eq_false: "(~ True) = False" by simp
5.431 -
5.432 -
5.433 -lemmas binarith =
5.434 - Pls_0_eq Min_1_eq
5.435 - bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
5.436 - bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
5.437 - bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
5.438 - bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
5.439 - bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
5.440 - bin_add_Pls_right bin_add_Min_right
5.441 -
5.442 -thm eq_number_of_eq
5.443 -
5.444 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
5.445 - by simp
5.446 -
5.447 -lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
5.448 - by (simp only: iszero_number_of_Pls)
5.449 -
5.450 -lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
5.451 - by simp
5.452 -thm iszero_number_of_1
5.453 -
5.454 -lemma int_iszero_number_of_0: "iszero ((number_of (w BIT False))::int) = iszero ((number_of w)::int)"
5.455 - by simp
5.456 -
5.457 -lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT True))::int)"
5.458 - by simp
5.459 -
5.460 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
5.461 - by simp
5.462 -
5.463 -lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
5.464 - by simp
5.465 -
5.466 -lemma int_neg_number_of_Min: "neg (-1::int)"
5.467 - by simp
5.468 -
5.469 -lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
5.470 - by simp
5.471 -
5.472 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
5.473 - by simp
5.474 -
5.475 -lemmas intarithrel =
5.476 - (*abs_zero abs_one*)
5.477 - int_eq_number_of_eq
5.478 - lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
5.479 - lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
5.480 - int_neg_number_of_BIT int_le_number_of_eq
5.481 -
5.482 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
5.483 - by simp
5.484 -
5.485 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
5.486 - by simp
5.487 -
5.488 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
5.489 - by simp
5.490 -
5.491 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
5.492 - by simp
5.493 -
5.494 -lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
5.495 -
5.496 -lemmas natarith = (*zero_eq_Numeral0_nat one_eq_Numeral1_nat*) add_nat_number_of
5.497 - diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
5.498 -
5.499 -lemmas powerarith = nat_number_of zpower_number_of_even
5.500 - zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
5.501 - zpower_Pls zpower_Min
5.502 -
5.503 -lemmas floatarith[simplified norm_0_1] = float_add float_mult float_minus float_abs zero_le_float
5.504 -
5.505 -lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
5.506 -
5.507 -(* needed for the verifying code generator *)
5.508 -lemmas arith_no_let = arith[simplified Let_def]
5.509 -
5.510 -end
5.511 -
6.1 --- a/src/HOL/Matrix/FloatArith.ML Mon Mar 07 16:55:36 2005 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,56 +0,0 @@
6.4 -structure FloatArith =
6.5 -struct
6.6 -
6.7 -type float = IntInf.int * IntInf.int
6.8 -
6.9 -val izero = IntInf.fromInt 0
6.10 -fun imul a b = IntInf.* (a,b)
6.11 -fun isub a b = IntInf.- (a,b)
6.12 -fun iadd a b = IntInf.+ (a,b)
6.13 -
6.14 -val floatzero = (izero, izero)
6.15 -
6.16 -fun positive_part (a,b) =
6.17 - (if IntInf.< (a,izero) then izero else a, b)
6.18 -
6.19 -fun negative_part (a,b) =
6.20 - (if IntInf.< (a,izero) then a else izero, b)
6.21 -
6.22 -fun is_negative (a,b) =
6.23 - if IntInf.< (a, izero) then true else false
6.24 -
6.25 -fun is_positive (a,b) =
6.26 - if IntInf.< (izero, a) then true else false
6.27 -
6.28 -fun is_zero (a,b) =
6.29 - if a = izero then true else false
6.30 -
6.31 -fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
6.32 -
6.33 -fun add (a1, b1) (a2, b2) =
6.34 - if IntInf.< (b1, b2) then
6.35 - (iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
6.36 - else
6.37 - (iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
6.38 -
6.39 -fun sub (a1, b1) (a2, b2) =
6.40 - if IntInf.< (b1, b2) then
6.41 - (isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
6.42 - else
6.43 - (isub (imul a1 (ipow2 (isub b1 b2))) a2, b2)
6.44 -
6.45 -fun neg (a, b) = (IntInf.~ a, b)
6.46 -
6.47 -fun is_equal a b = is_zero (sub a b)
6.48 -
6.49 -fun is_less a b = is_negative (sub a b)
6.50 -
6.51 -fun max a b = if is_less a b then b else a
6.52 -
6.53 -fun min a b = if is_less a b then a else b
6.54 -
6.55 -fun abs a = if is_negative a then neg a else a
6.56 -
6.57 -fun mul (a1, b1) (a2, b2) = (imul a1 a2, iadd b1 b2)
6.58 -
6.59 -end;
7.1 --- a/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Mon Mar 07 16:55:36 2005 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,388 +0,0 @@
7.4 -structure FloatSparseMatrixBuilder :
7.5 -sig
7.6 - include MATRIX_BUILDER
7.7 -
7.8 - structure cplex : CPLEX
7.9 -
7.10 - type float = IntInf.int*IntInf.int
7.11 - type floatfunc = float -> float
7.12 -
7.13 -
7.14 - val float2cterm : IntInf.int * IntInf.int -> cterm
7.15 -
7.16 - val approx_value : int -> floatfunc -> string -> cterm * cterm
7.17 - val approx_vector : int -> floatfunc -> vector -> cterm * cterm
7.18 - val approx_matrix : int -> floatfunc -> matrix -> cterm * cterm
7.19 -
7.20 - val mk_spvec_entry : int -> float -> term
7.21 - val empty_spvec : term
7.22 - val cons_spvec : term -> term -> term
7.23 - val empty_spmat : term
7.24 - val mk_spmat_entry : int -> term -> term
7.25 - val cons_spmat : term -> term -> term
7.26 - val sign_term : term -> cterm
7.27 -
7.28 - val v_elem_at : vector -> int -> string option
7.29 - val m_elem_at : matrix -> int -> vector option
7.30 - val v_only_elem : vector -> int option
7.31 - val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
7.32 - val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
7.33 -
7.34 - val transpose_matrix : matrix -> matrix
7.35 -
7.36 - val cut_vector : int -> vector -> vector
7.37 - val cut_matrix : vector -> (int option) -> matrix -> matrix
7.38 -
7.39 - (* cplexProg c A b *)
7.40 - val cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
7.41 - (* dual_cplexProg c A b *)
7.42 - val dual_cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
7.43 -
7.44 - val real_spmatT : typ
7.45 - val real_spvecT : typ
7.46 -end
7.47 -=
7.48 -struct
7.49 -
7.50 -
7.51 -structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
7.52 -
7.53 -type vector = string Inttab.table
7.54 -type matrix = vector Inttab.table
7.55 -type float = IntInf.int*IntInf.int
7.56 -type floatfunc = float -> float
7.57 -
7.58 -val th = theory "Float"
7.59 -val sg = sign_of th
7.60 -
7.61 -fun readtype s = Sign.intern_tycon sg s
7.62 -fun readterm s = Sign.intern_const sg s
7.63 -
7.64 -val ty_list = readtype "list"
7.65 -val term_Nil = readterm "Nil"
7.66 -val term_Cons = readterm "Cons"
7.67 -
7.68 -val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT)
7.69 -val spvecT = Type (ty_list, [spvec_elemT])
7.70 -val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT)
7.71 -val spmatT = Type (ty_list, [spmat_elemT])
7.72 -
7.73 -val real_spmatT = spmatT
7.74 -val real_spvecT = spvecT
7.75 -
7.76 -val empty_matrix_const = Const (term_Nil, spmatT)
7.77 -val empty_vector_const = Const (term_Nil, spvecT)
7.78 -
7.79 -val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
7.80 -val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT)
7.81 -
7.82 -val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
7.83 -
7.84 -val zero = IntInf.fromInt 0
7.85 -val minus_one = IntInf.fromInt ~1
7.86 -val two = IntInf.fromInt 2
7.87 -
7.88 -fun mk_intinf ty n =
7.89 - let
7.90 - fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
7.91 -
7.92 - fun bin_of n =
7.93 - if n = zero then HOLogic.pls_const
7.94 - else if n = minus_one then HOLogic.min_const
7.95 - else
7.96 - let
7.97 - (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
7.98 - val q = IntInf.div (n, two)
7.99 - val r = IntInf.mod (n, two)
7.100 - in
7.101 - HOLogic.bit_const $ bin_of q $ mk_bit r
7.102 - end
7.103 - in
7.104 - HOLogic.number_of_const ty $ (bin_of n)
7.105 - end
7.106 -
7.107 -fun mk_float (a,b) =
7.108 - float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))
7.109 -
7.110 -fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
7.111 -
7.112 -fun approx_value_term prec f value =
7.113 - let
7.114 - val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
7.115 - val (flower, fupper) = (f flower, f fupper)
7.116 - in
7.117 - (mk_float flower, mk_float fupper)
7.118 - end
7.119 -
7.120 -fun approx_value prec pprt value =
7.121 - let
7.122 - val (flower, fupper) = approx_value_term prec pprt value
7.123 - in
7.124 - (cterm_of sg flower, cterm_of sg fupper)
7.125 - end
7.126 -
7.127 -fun sign_term t = cterm_of sg t
7.128 -
7.129 -val empty_spvec = empty_vector_const
7.130 -
7.131 -val empty_spmat = empty_matrix_const
7.132 -
7.133 -fun mk_spvec_entry i f =
7.134 - let
7.135 - val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
7.136 - val term_f = mk_float f
7.137 - in
7.138 - HOLogic.mk_prod (term_i, term_f)
7.139 - end
7.140 -
7.141 -fun mk_spmat_entry i e =
7.142 - let
7.143 - val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
7.144 - in
7.145 - HOLogic.mk_prod (term_i, e)
7.146 - end
7.147 -
7.148 -fun cons_spvec h t = Cons_spvec_const $ h $ t
7.149 -
7.150 -fun cons_spmat h t = Cons_spmat_const $ h $ t
7.151 -
7.152 -fun approx_vector_term prec pprt vector =
7.153 - let
7.154 - fun app ((vlower, vupper), (index, s)) =
7.155 - let
7.156 - val (flower, fupper) = approx_value_term prec pprt s
7.157 - val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
7.158 - val elower = HOLogic.mk_prod (index, flower)
7.159 - val eupper = HOLogic.mk_prod (index, fupper)
7.160 - in
7.161 - (Cons_spvec_const $ elower $ vlower,
7.162 - Cons_spvec_const $ eupper $ vupper)
7.163 - end
7.164 - in
7.165 - Inttab.foldl app ((empty_vector_const, empty_vector_const), vector)
7.166 - end
7.167 -
7.168 -fun approx_matrix_term prec pprt matrix =
7.169 - let
7.170 - fun app ((mlower, mupper), (index, vector)) =
7.171 - let
7.172 - val (vlower, vupper) = approx_vector_term prec pprt vector
7.173 - val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
7.174 - val elower = HOLogic.mk_prod (index, vlower)
7.175 - val eupper = HOLogic.mk_prod (index, vupper)
7.176 - in
7.177 - (Cons_spmat_const $ elower $ mlower,
7.178 - Cons_spmat_const $ eupper $ mupper)
7.179 - end
7.180 -
7.181 - val (mlower, mupper) = Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)
7.182 - in
7.183 - Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)
7.184 - end
7.185 -
7.186 -fun approx_vector prec pprt vector =
7.187 - let
7.188 - val (l, u) = approx_vector_term prec pprt vector
7.189 - in
7.190 - (cterm_of sg l, cterm_of sg u)
7.191 - end
7.192 -
7.193 -fun approx_matrix prec pprt matrix =
7.194 - let
7.195 - val (l, u) = approx_matrix_term prec pprt matrix
7.196 - in
7.197 - (cterm_of sg l, cterm_of sg u)
7.198 - end
7.199 -
7.200 -
7.201 -exception Nat_expected of int;
7.202 -
7.203 -val zero_interval = approx_value_term 1 I "0"
7.204 -
7.205 -fun set_elem vector index str =
7.206 - if index < 0 then
7.207 - raise (Nat_expected index)
7.208 - else if (approx_value_term 1 I str) = zero_interval then
7.209 - vector
7.210 - else
7.211 - Inttab.update ((index, str), vector)
7.212 -
7.213 -fun set_vector matrix index vector =
7.214 - if index < 0 then
7.215 - raise (Nat_expected index)
7.216 - else if Inttab.is_empty vector then
7.217 - matrix
7.218 - else
7.219 - Inttab.update ((index, vector), matrix)
7.220 -
7.221 -val empty_matrix = Inttab.empty
7.222 -val empty_vector = Inttab.empty
7.223 -
7.224 -(* dual stuff *)
7.225 -
7.226 -structure cplex = Cplex
7.227 -
7.228 -fun transpose_matrix matrix =
7.229 - let
7.230 - fun upd m j i x =
7.231 - case Inttab.lookup (m, j) of
7.232 - SOME v => Inttab.update ((j, Inttab.update ((i, x), v)), m)
7.233 - | NONE => Inttab.update ((j, Inttab.update ((i, x), Inttab.empty)), m)
7.234 -
7.235 - fun updv j (m, (i, s)) = upd m i j s
7.236 -
7.237 - fun updm (m, (j, v)) = Inttab.foldl (updv j) (m, v)
7.238 - in
7.239 - Inttab.foldl updm (empty_matrix, matrix)
7.240 - end
7.241 -
7.242 -exception No_name of string;
7.243 -
7.244 -exception Superfluous_constr_right_hand_sides
7.245 -
7.246 -fun cplexProg c A b =
7.247 - let
7.248 - val ytable = ref Inttab.empty
7.249 - fun indexof s =
7.250 - if String.size s = 0 then raise (No_name s)
7.251 - else case Int.fromString (String.extract(s, 1, NONE)) of
7.252 - SOME i => i | NONE => raise (No_name s)
7.253 -
7.254 - fun nameof i =
7.255 - let
7.256 - val s = "x"^(Int.toString i)
7.257 - val _ = ytable := (Inttab.update ((i, s), !ytable))
7.258 - in
7.259 - s
7.260 - end
7.261 -
7.262 - fun split_numstr s =
7.263 - if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
7.264 - else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
7.265 - else (true, s)
7.266 -
7.267 - fun mk_term index s =
7.268 - let
7.269 - val (p, s) = split_numstr s
7.270 - val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
7.271 - in
7.272 - if p then prod else cplex.cplexNeg prod
7.273 - end
7.274 -
7.275 - fun vec2sum vector =
7.276 - cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
7.277 -
7.278 - fun mk_constr index vector c =
7.279 - let
7.280 - val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
7.281 - val (p, s) = split_numstr s
7.282 - val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
7.283 - in
7.284 - (NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
7.285 - end
7.286 -
7.287 - fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
7.288 -
7.289 - val (list, b) = Inttab.foldl
7.290 - (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
7.291 - (([], b), A)
7.292 - val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
7.293 -
7.294 - fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
7.295 - cplex.cplexVar y, cplex.cplexLeq,
7.296 - cplex.cplexInf)
7.297 -
7.298 - val yvars = Inttab.foldl (fn (l, (i, y)) => (mk_free y)::l) ([], !ytable)
7.299 -
7.300 - val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
7.301 - in
7.302 - (prog, indexof)
7.303 - end
7.304 -
7.305 -
7.306 -fun dual_cplexProg c A b =
7.307 - let
7.308 - fun indexof s =
7.309 - if String.size s = 0 then raise (No_name s)
7.310 - else case Int.fromString (String.extract(s, 1, NONE)) of
7.311 - SOME i => i | NONE => raise (No_name s)
7.312 -
7.313 - fun nameof i = "y"^(Int.toString i)
7.314 -
7.315 - fun split_numstr s =
7.316 - if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
7.317 - else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
7.318 - else (true, s)
7.319 -
7.320 - fun mk_term index s =
7.321 - let
7.322 - val (p, s) = split_numstr s
7.323 - val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
7.324 - in
7.325 - if p then prod else cplex.cplexNeg prod
7.326 - end
7.327 -
7.328 - fun vec2sum vector =
7.329 - cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
7.330 -
7.331 - fun mk_constr index vector c =
7.332 - let
7.333 - val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
7.334 - val (p, s) = split_numstr s
7.335 - val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
7.336 - in
7.337 - (NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
7.338 - end
7.339 -
7.340 - fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
7.341 -
7.342 - val (list, c) = Inttab.foldl
7.343 - (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
7.344 - (([], c), transpose_matrix A)
7.345 - val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
7.346 -
7.347 - val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
7.348 - in
7.349 - (prog, indexof)
7.350 - end
7.351 -
7.352 -fun cut_vector size v =
7.353 - let
7.354 - val count = ref 0
7.355 - fun app (v, (i, s)) =
7.356 - if (!count < size) then
7.357 - (count := !count +1 ; Inttab.update ((i,s),v))
7.358 - else
7.359 - v
7.360 - in
7.361 - Inttab.foldl app (empty_vector, v)
7.362 - end
7.363 -
7.364 -fun cut_matrix vfilter vsize m =
7.365 - let
7.366 - fun app (m, (i, v)) =
7.367 - if (Inttab.lookup (vfilter, i) = NONE) then
7.368 - m
7.369 - else
7.370 - case vsize of
7.371 - NONE => Inttab.update ((i,v), m)
7.372 - | SOME s => Inttab.update((i, cut_vector s v),m)
7.373 - in
7.374 - Inttab.foldl app (empty_matrix, m)
7.375 - end
7.376 -
7.377 -fun v_elem_at v i = Inttab.lookup (v,i)
7.378 -fun m_elem_at m i = Inttab.lookup (m,i)
7.379 -
7.380 -fun v_only_elem v =
7.381 - case Inttab.min_key v of
7.382 - NONE => NONE
7.383 - | SOME vmin => (case Inttab.max_key v of
7.384 - NONE => SOME vmin
7.385 - | SOME vmax => if vmin = vmax then SOME vmin else NONE)
7.386 -
7.387 -fun v_fold f a v = Inttab.foldl f (a,v)
7.388 -
7.389 -fun m_fold f a m = Inttab.foldl f (a,m)
7.390 -
7.391 -end;
8.1 --- a/src/HOL/Matrix/MatrixGeneral.thy Mon Mar 07 16:55:36 2005 +0100
8.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy Mon Mar 07 18:19:55 2005 +0100
8.3 @@ -41,7 +41,7 @@
8.4 from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
8.5 have "m \<notin> ?S"
8.6 proof -
8.7 - have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_ge[OF c b])
8.8 + have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge[OF c b])
8.9 moreover from d have "~(m <= Max ?S)" by (simp)
8.10 ultimately show "m \<notin> ?S" by (auto)
8.11 qed
8.12 @@ -537,12 +537,14 @@
8.13 and nm: "n <= m"
8.14 shows
8.15 "foldseq f s n = foldseq f s m"
8.16 +proof -
8.17 + show "foldseq f s n = foldseq f s m"
8.18 apply (simp add: foldseq_tail[OF nm, of f s])
8.19 apply (rule foldseq_significant_positions)
8.20 apply (auto)
8.21 apply (subst foldseq_zero)
8.22 by (simp add: fz sz)+
8.23 -
8.24 +qed
8.25
8.26 lemma foldseq_zerotail2:
8.27 assumes "! x. f x 0 = x"
8.28 @@ -663,7 +665,7 @@
8.29 assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
8.30 shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
8.31 proof -
8.32 - from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n[where n = n])
8.33 + from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
8.34 also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
8.35 finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
8.36 qed
8.37 @@ -759,7 +761,6 @@
8.38 qed
8.39 qed
8.40
8.41 -
8.42 instance matrix :: (zero) zero ..
8.43
8.44 defs(overloaded)
8.45 @@ -785,25 +786,23 @@
8.46 lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
8.47 by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
8.48
8.49 -
8.50 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
8.51 by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
8.52
8.53 lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
8.54 apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
8.55 - apply (simp add: foldseq_zero zero_matrix_def)
8.56 - done
8.57 -
8.58 + apply (auto)
8.59 + by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
8.60
8.61 lemma mult_matrix_n_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd A 0 = 0"
8.62 apply (simp add: mult_matrix_n_def)
8.63 - apply (simp add: foldseq_zero zero_matrix_def)
8.64 - done
8.65 + apply (subst foldseq_zero)
8.66 + by (simp_all add: zero_matrix_def)
8.67
8.68 lemma mult_matrix_n_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd 0 A = 0"
8.69 apply (simp add: mult_matrix_n_def)
8.70 - apply (simp add: foldseq_zero zero_matrix_def)
8.71 - done
8.72 + apply (subst foldseq_zero)
8.73 + by (simp_all add: zero_matrix_def)
8.74
8.75 lemma mult_matrix_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd 0 A = 0"
8.76 by (simp add: mult_matrix_def)
8.77 @@ -851,7 +850,7 @@
8.78 apply (subst RepAbs_matrix)
8.79 apply (rule exI[of _ "Suc m"], simp)
8.80 apply (rule exI[of _ "Suc n"], simp+)
8.81 -by (simplesubst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
8.82 +by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
8.83
8.84 lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
8.85 apply (subst Rep_matrix_inject[symmetric])
8.86 @@ -892,7 +891,7 @@
8.87
8.88 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"
8.89 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
8.90 -apply (simplesubst RepAbs_matrix)
8.91 +apply (subst RepAbs_matrix)
8.92 apply (rule exI[of _ "Suc j"], simp)
8.93 apply (rule exI[of _ "Suc i"], simp)
8.94 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
8.95 @@ -911,7 +910,7 @@
8.96 (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
8.97 apply (simp add: move_matrix_def)
8.98 apply (auto)
8.99 -by (simplesubst RepAbs_matrix,
8.100 +by (subst RepAbs_matrix,
8.101 rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
8.102 rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
8.103
9.1 --- a/src/HOL/Matrix/MatrixLP.ML Mon Mar 07 16:55:36 2005 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,83 +0,0 @@
9.4 -use "MatrixLP_gensimp.ML";
9.5 -
9.6 -signature MATRIX_LP =
9.7 -sig
9.8 - val lp_dual_estimate : string -> int -> thm
9.9 - val simplify : thm -> thm
9.10 -end
9.11 -
9.12 -structure MatrixLP : MATRIX_LP =
9.13 -struct
9.14 -
9.15 -val _ = SimprocsCodegen.use_simprocs_code sg geninput
9.16 -
9.17 -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'
9.18 -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'''''
9.19 -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'''''
9.20 -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'''''
9.21 -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'''''
9.22 -val simp_sorted_sparse_matrix = simp_SparseMatrix_sorted_sparse_matrix
9.23 -val simp_sorted_spvec = simp_SparseMatrix_sorted_spvec
9.24 -
9.25 -fun single_arg simp ct = snd (simp (snd (Thm.dest_comb ct)))
9.26 -
9.27 -fun double_arg simp ct =
9.28 - let
9.29 - val (a, y) = Thm.dest_comb ct
9.30 - val (_, x) = Thm.dest_comb a
9.31 - in
9.32 - snd (simp x y)
9.33 - end
9.34 -
9.35 -fun spmc ct =
9.36 - (case term_of ct of
9.37 - ((Const ("SparseMatrix.le_spmat", _)) $ _) =>
9.38 - single_arg simp_le_spmat ct
9.39 - | ((Const ("SparseMatrix.add_spmat", _)) $ _) =>
9.40 - single_arg simp_add_spmat ct
9.41 - | ((Const ("SparseMatrix.diff_spmat", _)) $ _ $ _) =>
9.42 - double_arg simp_diff_spmat ct
9.43 - | ((Const ("SparseMatrix.abs_spmat", _)) $ _) =>
9.44 - single_arg simp_abs_spmat ct
9.45 - | ((Const ("SparseMatrix.mult_spmat", _)) $ _ $ _) =>
9.46 - double_arg simp_mult_spmat ct
9.47 - | ((Const ("SparseMatrix.sorted_sparse_matrix", _)) $ _) =>
9.48 - single_arg simp_sorted_sparse_matrix ct
9.49 - | ((Const ("SparseMatrix.sorted_spvec", ty)) $ _) =>
9.50 - single_arg simp_sorted_spvec ct
9.51 - | _ => raise Fail_conv)
9.52 -
9.53 -fun lp_dual_estimate lptfile prec =
9.54 - let
9.55 - val th = inst_real (thm "SparseMatrix.spm_linprog_dual_estimate_1")
9.56 - val sg = sign_of (theory "MatrixLP")
9.57 - val (y, (A1, A2), (c1, c2), b, r) =
9.58 - let
9.59 - open fspmlp
9.60 - val l = load lptfile prec false
9.61 - in
9.62 - (y l, A l, c l, b l, r l)
9.63 - end
9.64 - fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
9.65 - 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
9.66 - in
9.67 - th
9.68 - end
9.69 -
9.70 -fun simplify th =
9.71 - let
9.72 - val simp_th = botc spmc (cprop_of th)
9.73 - val th = strip_shyps (equal_elim simp_th th)
9.74 - fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
9.75 - in
9.76 - removeTrue th
9.77 - end
9.78 -
9.79 -end
9.80 -
9.81 -fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
9.82 -
9.83 -val result = ref ([]:thm list)
9.84 -
9.85 -fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ()))
9.86 -
10.1 --- a/src/HOL/Matrix/MatrixLP.thy Mon Mar 07 16:55:36 2005 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,4 +0,0 @@
10.4 -theory MatrixLP = Float + SparseMatrix:
10.5 -
10.6 -end
10.7 -
11.1 --- a/src/HOL/Matrix/MatrixLP_gensimp.ML Mon Mar 07 16:55:36 2005 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,35 +0,0 @@
11.4 -open BasisLibrary;
11.5 -
11.6 -use "Cplex.ML";
11.7 -use "CplexMatrixConverter.ML";
11.8 -use "ExactFloatingPoint.ML";
11.9 -use "FloatArith.ML";
11.10 -use "FloatSparseMatrixBuilder.ML";
11.11 -use "fspmlp.ML";
11.12 -use "codegen_prep.ML";
11.13 -use "eq_codegen.ML";
11.14 -use "conv.ML";
11.15 -
11.16 -
11.17 -val th = theory "MatrixLP"
11.18 -val sg = sign_of th
11.19 -
11.20 -fun prep x = standard (mk_meta_eq x)
11.21 -
11.22 -fun inst_real thm = standard (Thm.instantiate ([(fst (hd (term_tvars (prop_of thm))),
11.23 - ctyp_of sg HOLogic.realT)], []) thm);
11.24 -
11.25 -val spm_lp_dual_estimate_simp =
11.26 - (thms "Float.arith_no_let") @
11.27 - (map inst_real (thms "SparseMatrix.sparse_row_matrix_arith_simps")) @
11.28 - (thms "SparseMatrix.sorted_sp_simps") @
11.29 - [thm "Product_Type.fst_conv", thm "Product_Type.snd_conv"] @
11.30 - (thms "SparseMatrix.boolarith")
11.31 -
11.32 -val simp_with = Simplifier.simplify (HOL_basic_ss addsimps [thm "SparseMatrix.if_case_eq", thm "Float.norm_0_1"])
11.33 -
11.34 -val spm_lp_dual_estimate_simp = map simp_with spm_lp_dual_estimate_simp
11.35 -
11.36 -val geninput = codegen_prep.prepare_thms spm_lp_dual_estimate_simp
11.37 -
11.38 -val _ = SimprocsCodegen.use_simprocs_code sg geninput
12.1 --- a/src/HOL/Matrix/ROOT.ML Mon Mar 07 16:55:36 2005 +0100
12.2 +++ b/src/HOL/Matrix/ROOT.ML Mon Mar 07 18:19:55 2005 +0100
12.3 @@ -1,1 +1,1 @@
12.4 -use_thy "MatrixLP"
12.5 +use_thy "SparseMatrix"
13.1 --- a/src/HOL/Matrix/SparseMatrix.thy Mon Mar 07 16:55:36 2005 +0100
13.2 +++ b/src/HOL/Matrix/SparseMatrix.thy Mon Mar 07 18:19:55 2005 +0100
13.3 @@ -138,6 +138,14 @@
13.4 apply (simp add: sorted_spvec.simps split:list.split_asm)
13.5 done
13.6
13.7 +lemma sorted_spvec_minus_spvec:
13.8 + "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
13.9 + apply (induct v)
13.10 + apply (simp)
13.11 + apply (frule sorted_spvec_cons1, simp)
13.12 + apply (simp add: sorted_spvec.simps split:list.split_asm)
13.13 + done
13.14 +
13.15 lemma sorted_spvec_abs_spvec:
13.16 "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
13.17 apply (induct v)
13.18 @@ -233,7 +241,6 @@
13.19 apply (frule_tac as=arr in sorted_spvec_cons1)
13.20 apply (frule_tac as=brr in sorted_spvec_cons1)
13.21 apply (simp)
13.22 - apply (case_tac "a=aa")
13.23 apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
13.24 done
13.25
13.26 @@ -590,6 +597,13 @@
13.27
13.28 ML {* simp_depth_limit := 2 *}
13.29
13.30 +lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
13.31 + by (simp add: disj_matrices_def)
13.32 +
13.33 +lemma disj_matrices_contr2: "disj_matrices A B \<Longrightarrow> Rep_matrix B j i \<noteq> 0 \<Longrightarrow> Rep_matrix A j i = 0"
13.34 + by (simp add: disj_matrices_def)
13.35 +
13.36 +
13.37 lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow>
13.38 (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
13.39 apply (auto)
13.40 @@ -800,7 +814,7 @@
13.41 apply (induct A)
13.42 apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
13.43 apply (frule_tac sorted_spvec_cons1, simp)
13.44 - apply (subst Rep_matrix_inject[symmetric])
13.45 + apply (simplesubst Rep_matrix_inject[symmetric])
13.46 apply (rule ext)+
13.47 apply auto
13.48 apply (case_tac "x=a")
13.49 @@ -858,27 +872,6 @@
13.50 lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A"
13.51 by (simp add: sorted_sparse_matrix_def)
13.52
13.53 -lemmas sparse_row_matrix_op_simps =
13.54 - sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
13.55 - sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
13.56 - sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
13.57 - sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
13.58 - sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
13.59 - sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
13.60 - le_spmat_iff_sparse_row_le
13.61 -
13.62 -lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
13.63 -
13.64 -lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] =
13.65 - mult_spmat.simps mult_spvec_spmat.simps
13.66 - addmult_spvec.simps
13.67 - smult_spvec_empty smult_spvec_cons
13.68 - add_spmat.simps add_spvec.simps
13.69 - minus_spmat.simps minus_spvec.simps
13.70 - abs_spmat.simps abs_spvec.simps
13.71 - diff_spmat_def
13.72 - le_spmat.simps le_spvec.simps
13.73 -
13.74 lemmas sorted_sp_simps =
13.75 sorted_spvec.simps
13.76 sorted_spmat.simps
13.77 @@ -898,7 +891,210 @@
13.78
13.79 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
13.80
13.81 -lemma spm_linprog_dual_estimate_1:
13.82 +consts
13.83 + pprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
13.84 + nprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
13.85 + pprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
13.86 + nprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
13.87 +
13.88 +primrec
13.89 + "pprt_spvec [] = []"
13.90 + "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
13.91 +
13.92 +primrec
13.93 + "nprt_spvec [] = []"
13.94 + "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
13.95 +
13.96 +primrec
13.97 + "pprt_spmat [] = []"
13.98 + "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
13.99 + (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
13.100 +
13.101 +primrec
13.102 + "nprt_spmat [] = []"
13.103 + "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
13.104 + (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
13.105 +
13.106 +
13.107 +lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
13.108 + apply (simp add: pprt_def join_matrix)
13.109 + apply (simp add: Rep_matrix_inject[symmetric])
13.110 + apply (rule ext)+
13.111 + apply simp
13.112 + apply (case_tac "Rep_matrix A x xa \<noteq> 0")
13.113 + apply (simp_all add: disj_matrices_contr1)
13.114 + done
13.115 +
13.116 +lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
13.117 + apply (simp add: nprt_def meet_matrix)
13.118 + apply (simp add: Rep_matrix_inject[symmetric])
13.119 + apply (rule ext)+
13.120 + apply simp
13.121 + apply (case_tac "Rep_matrix A x xa \<noteq> 0")
13.122 + apply (simp_all add: disj_matrices_contr1)
13.123 + done
13.124 +
13.125 +lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
13.126 + apply (simp add: pprt_def join_matrix)
13.127 + apply (simp add: Rep_matrix_inject[symmetric])
13.128 + apply (rule ext)+
13.129 + apply simp
13.130 + done
13.131 +
13.132 +lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
13.133 + apply (simp add: nprt_def meet_matrix)
13.134 + apply (simp add: Rep_matrix_inject[symmetric])
13.135 + apply (rule ext)+
13.136 + apply simp
13.137 + done
13.138 +
13.139 +lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
13.140 +
13.141 +lemma sparse_row_vector_pprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
13.142 + apply (induct v)
13.143 + apply (simp_all)
13.144 + apply (frule sorted_spvec_cons1, auto)
13.145 + apply (subst pprt_add)
13.146 + apply (subst disj_matrices_commute)
13.147 + apply (rule disj_sparse_row_singleton)
13.148 + apply auto
13.149 + done
13.150 +
13.151 +lemma sparse_row_vector_nprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
13.152 + apply (induct v)
13.153 + apply (simp_all)
13.154 + apply (frule sorted_spvec_cons1, auto)
13.155 + apply (subst nprt_add)
13.156 + apply (subst disj_matrices_commute)
13.157 + apply (rule disj_sparse_row_singleton)
13.158 + apply auto
13.159 + done
13.160 +
13.161 +
13.162 +lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
13.163 + apply (simp add: pprt_def)
13.164 + apply (simp add: join_matrix)
13.165 + apply (simp add: Rep_matrix_inject[symmetric])
13.166 + apply (rule ext)+
13.167 + apply (simp)
13.168 + done
13.169 +
13.170 +lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
13.171 + apply (simp add: nprt_def)
13.172 + apply (simp add: meet_matrix)
13.173 + apply (simp add: Rep_matrix_inject[symmetric])
13.174 + apply (rule ext)+
13.175 + apply (simp)
13.176 + done
13.177 +
13.178 +lemma sparse_row_matrix_pprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
13.179 + apply (induct m)
13.180 + apply simp
13.181 + apply simp
13.182 + apply (frule sorted_spvec_cons1)
13.183 + apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
13.184 + apply (subst pprt_add)
13.185 + apply (subst disj_matrices_commute)
13.186 + apply (rule disj_move_sparse_vec_mat)
13.187 + apply auto
13.188 + apply (simp add: sorted_spvec.simps)
13.189 + apply (simp split: list.split)
13.190 + apply auto
13.191 + apply (simp add: pprt_move_matrix)
13.192 + done
13.193 +
13.194 +lemma sparse_row_matrix_nprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
13.195 + apply (induct m)
13.196 + apply simp
13.197 + apply simp
13.198 + apply (frule sorted_spvec_cons1)
13.199 + apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
13.200 + apply (subst nprt_add)
13.201 + apply (subst disj_matrices_commute)
13.202 + apply (rule disj_move_sparse_vec_mat)
13.203 + apply auto
13.204 + apply (simp add: sorted_spvec.simps)
13.205 + apply (simp split: list.split)
13.206 + apply auto
13.207 + apply (simp add: nprt_move_matrix)
13.208 + done
13.209 +
13.210 +lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)"
13.211 + apply (induct v)
13.212 + apply (simp)
13.213 + apply (frule sorted_spvec_cons1)
13.214 + apply simp
13.215 + apply (simp add: sorted_spvec.simps split:list.split_asm)
13.216 + done
13.217 +
13.218 +lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
13.219 + apply (induct v)
13.220 + apply (simp)
13.221 + apply (frule sorted_spvec_cons1)
13.222 + apply simp
13.223 + apply (simp add: sorted_spvec.simps split:list.split_asm)
13.224 + done
13.225 +
13.226 +lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)"
13.227 + apply (induct m)
13.228 + apply (simp)
13.229 + apply (frule sorted_spvec_cons1)
13.230 + apply simp
13.231 + apply (simp add: sorted_spvec.simps split:list.split_asm)
13.232 + done
13.233 +
13.234 +lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)"
13.235 + apply (induct m)
13.236 + apply (simp)
13.237 + apply (frule sorted_spvec_cons1)
13.238 + apply simp
13.239 + apply (simp add: sorted_spvec.simps split:list.split_asm)
13.240 + done
13.241 +
13.242 +lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)"
13.243 + apply (induct m)
13.244 + apply (simp_all add: sorted_pprt_spvec)
13.245 + done
13.246 +
13.247 +lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)"
13.248 + apply (induct m)
13.249 + apply (simp_all add: sorted_nprt_spvec)
13.250 + done
13.251 +
13.252 +constdefs
13.253 + mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
13.254 + "mult_est_spmat r1 r2 s1 s2 ==
13.255 + add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2),
13.256 + add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"
13.257 +
13.258 +lemmas sparse_row_matrix_op_simps =
13.259 + sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
13.260 + sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
13.261 + sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
13.262 + sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
13.263 + sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
13.264 + sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
13.265 + le_spmat_iff_sparse_row_le
13.266 + sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat
13.267 + sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat
13.268 +
13.269 +lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
13.270 +
13.271 +lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] =
13.272 + mult_spmat.simps mult_spvec_spmat.simps
13.273 + addmult_spvec.simps
13.274 + smult_spvec_empty smult_spvec_cons
13.275 + add_spmat.simps add_spvec.simps
13.276 + minus_spmat.simps minus_spvec.simps
13.277 + abs_spmat.simps abs_spvec.simps
13.278 + diff_spmat_def
13.279 + le_spmat.simps le_spvec.simps
13.280 + pprt_spmat.simps pprt_spvec.simps
13.281 + nprt_spmat.simps nprt_spvec.simps
13.282 + mult_est_spmat_def
13.283 +
13.284 +
13.285 +(*lemma spm_linprog_dual_estimate_1:
13.286 assumes
13.287 "sorted_sparse_matrix A1"
13.288 "sorted_sparse_matrix A2"
13.289 @@ -918,5 +1114,59 @@
13.290 "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1),
13.291 abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
13.292 by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])
13.293 +*)
13.294
13.295 +lemma spm_mult_le_dual_prts:
13.296 + assumes
13.297 + "sorted_sparse_matrix A1"
13.298 + "sorted_sparse_matrix A2"
13.299 + "sorted_sparse_matrix c1"
13.300 + "sorted_sparse_matrix c2"
13.301 + "sorted_sparse_matrix y"
13.302 + "sorted_sparse_matrix r1"
13.303 + "sorted_sparse_matrix r2"
13.304 + "sorted_spvec b"
13.305 + "le_spmat ([], y)"
13.306 + "sparse_row_matrix A1 \<le> A"
13.307 + "A \<le> sparse_row_matrix A2"
13.308 + "sparse_row_matrix c1 \<le> c"
13.309 + "c \<le> sparse_row_matrix c2"
13.310 + "sparse_row_matrix r1 \<le> x"
13.311 + "x \<le> sparse_row_matrix r2"
13.312 + "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
13.313 + shows
13.314 + "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
13.315 + (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in
13.316 + add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2),
13.317 + add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
13.318 + apply (simp add: Let_def)
13.319 + apply (insert prems)
13.320 + apply (simp add: sparse_row_matrix_op_simps ring_eq_simps)
13.321 + apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_eq_simps])
13.322 + apply (auto)
13.323 + done
13.324 +
13.325 +lemma spm_mult_le_dual_prts_no_let:
13.326 + assumes
13.327 + "sorted_sparse_matrix A1"
13.328 + "sorted_sparse_matrix A2"
13.329 + "sorted_sparse_matrix c1"
13.330 + "sorted_sparse_matrix c2"
13.331 + "sorted_sparse_matrix y"
13.332 + "sorted_sparse_matrix r1"
13.333 + "sorted_sparse_matrix r2"
13.334 + "sorted_spvec b"
13.335 + "le_spmat ([], y)"
13.336 + "sparse_row_matrix A1 \<le> A"
13.337 + "A \<le> sparse_row_matrix A2"
13.338 + "sparse_row_matrix c1 \<le> c"
13.339 + "c \<le> sparse_row_matrix c2"
13.340 + "sparse_row_matrix r1 \<le> x"
13.341 + "x \<le> sparse_row_matrix r2"
13.342 + "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
13.343 + shows
13.344 + "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
13.345 + mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
13.346 + by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
13.347 +
13.348 end
14.1 --- a/src/HOL/Matrix/codegen_prep.ML Mon Mar 07 16:55:36 2005 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,110 +0,0 @@
14.4 -structure codegen_prep =
14.5 -struct
14.6 -
14.7 -exception Prepare_thms of string;
14.8 -
14.9 -fun is_meta_eq th =
14.10 - let
14.11 - fun check ((Const ("==", _)) $ _ $ _) = true
14.12 - | check _ = false
14.13 - in
14.14 - check (concl_of th)
14.15 - end
14.16 -
14.17 -fun printty ty =
14.18 - let
14.19 - fun immerse s [] = []
14.20 - | immerse s [x] = [x]
14.21 - | immerse s (x::xs) = x::s::(immerse s xs)
14.22 -
14.23 - fun py t =
14.24 - let
14.25 - val (name, args) = dest_Type t
14.26 - val args' = map printty args
14.27 - in
14.28 - concat (immerse "_" (name::args'))
14.29 - end
14.30 -
14.31 - val (args, res) = strip_type ty
14.32 - val tystrs = map py (args@[res])
14.33 -
14.34 - val s = "'"^(concat (immerse "_" tystrs))^"'"
14.35 - in
14.36 - s
14.37 - end
14.38 -
14.39 -fun head_name th =
14.40 - let val s =
14.41 - let
14.42 - val h = fst (strip_comb (hd (snd (strip_comb (concl_of th)))))
14.43 - val n = fst (dest_Const h)
14.44 - val ty = snd (dest_Const h)
14.45 - val hn = fst (dest_Const h)
14.46 - in
14.47 - hn^"_"^(printty ty) handle _ => (writeln ("warning: polymorphic "^hn); hn)
14.48 - end
14.49 - in
14.50 - s
14.51 - end
14.52 -
14.53 -val mangle_id =
14.54 - let
14.55 - fun tr #"=" = "_eq_"
14.56 - | tr #"." = "_"
14.57 - | tr #" " = "_"
14.58 - | tr #"<" = "_le_"
14.59 - | tr #">" = "_ge_"
14.60 - | tr #"(" = "_bro_"
14.61 - | tr #")" = "_brc_"
14.62 - | tr #"+" = "_plus_"
14.63 - | tr #"*" = "_mult_"
14.64 - | tr #"-" = "_minus_"
14.65 - | tr #"|" = "_or_"
14.66 - | tr #"&" = "_and_"
14.67 - | tr x = Char.toString x
14.68 - fun m s = "simp_"^(String.translate tr s)
14.69 - in
14.70 - m
14.71 - end
14.72 -
14.73 -fun group f [] = []
14.74 - | group f (x::xs) =
14.75 - let
14.76 - val g = group f xs
14.77 - val key = f x
14.78 - in
14.79 - case assoc (g, key) of
14.80 - NONE => (key, [x])::g
14.81 - | SOME l => overwrite (g, (key, x::l))
14.82 - end
14.83 -
14.84 -fun prepare_thms ths =
14.85 - let
14.86 - val ths = (List.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (filter_out is_meta_eq ths))
14.87 - val _ = if forall Thm.no_prems ths then () else raise (Prepare_thms "premisse found")
14.88 - val thmgroups = group head_name ths
14.89 - val test_clashgroups = group (fn (a,b) => mangle_id a) thmgroups
14.90 - val _ = if (length thmgroups <> length test_clashgroups) then raise (Prepare_thms "clash after name mangling") else ()
14.91 -
14.92 - fun prep (name, ths) =
14.93 - let
14.94 - val m = mangle_id name
14.95 -
14.96 - in
14.97 - (m, true, ths)
14.98 - end
14.99 -
14.100 - val thmgroups = map prep thmgroups
14.101 - in
14.102 - (thmgroups)
14.103 - end
14.104 -
14.105 -fun writestr filename s =
14.106 - let
14.107 - val f = TextIO.openOut filename
14.108 - val _ = TextIO.output(f, s)
14.109 - val _ = TextIO.closeOut f
14.110 - in
14.111 - ()
14.112 - end
14.113 -end
15.1 --- a/src/HOL/Matrix/conv.ML Mon Mar 07 16:55:36 2005 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,26 +0,0 @@
15.4 -exception Fail_conv;
15.5 -
15.6 -fun orelsec conv1 conv2 ct = conv1 ct handle Fail_conv => conv2 ct
15.7 -
15.8 -val allc = Thm.reflexive
15.9 -
15.10 -fun thenc conv1 conv2 ct =
15.11 - let
15.12 - fun rhs_of t = snd (Thm.dest_comb (strip_imp_concl (cprop_of t)))
15.13 -
15.14 - val eq = conv1 ct
15.15 - in
15.16 - Thm.transitive eq (conv2 (rhs_of eq))
15.17 - end
15.18 -
15.19 -fun subc conv ct =
15.20 - case term_of ct of
15.21 - _ $ _ =>
15.22 - let
15.23 - val (ct1, ct2) = Thm.dest_comb ct
15.24 - in
15.25 - Thm.combination (conv ct1) (conv ct2)
15.26 - end
15.27 - | _ => allc ct
15.28 -
15.29 -fun botc conv ct = thenc (subc (botc conv)) (orelsec conv allc) ct
15.30 \ No newline at end of file
16.1 --- a/src/HOL/Matrix/eq_codegen.ML Mon Mar 07 16:55:36 2005 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,493 +0,0 @@
16.4 -fun inst_cterm inst ct = fst (Drule.dest_equals
16.5 - (Thm.cprop_of (Thm.instantiate inst (reflexive ct))));
16.6 -fun tyinst_cterm tyinst = inst_cterm (tyinst, []);
16.7 -
16.8 -val bla = ref ([] : term list);
16.9 -
16.10 -(******************************************************)
16.11 -(* Code generator for equational proofs *)
16.12 -(******************************************************)
16.13 -fun my_mk_meta_eq thm =
16.14 - let
16.15 - val (_, eq) = Thm.dest_comb (cprop_of thm);
16.16 - val (ct, rhs) = Thm.dest_comb eq;
16.17 - val (_, lhs) = Thm.dest_comb ct
16.18 - in Thm.implies_elim (Drule.instantiate' [SOME (ctyp_of_term lhs)]
16.19 - [SOME lhs, SOME rhs] eq_reflection) thm
16.20 - end;
16.21 -
16.22 -structure SimprocsCodegen =
16.23 -struct
16.24 -
16.25 -val simp_thms = ref ([] : thm list);
16.26 -
16.27 -fun parens b = if b then Pretty.enclose "(" ")" else Pretty.block;
16.28 -
16.29 -fun gen_mk_val f xs ps = Pretty.block ([Pretty.str "val ",
16.30 - f (length xs > 1) (List.concat
16.31 - (separate [Pretty.str ",", Pretty.brk 1] (map (single o Pretty.str) xs))),
16.32 - Pretty.str " =", Pretty.brk 1] @ ps @ [Pretty.str ";"]);
16.33 -
16.34 -val mk_val = gen_mk_val parens;
16.35 -val mk_vall = gen_mk_val (K (Pretty.enclose "[" "]"));
16.36 -
16.37 -fun rename s = if s mem ThmDatabase.ml_reserved then s ^ "'" else s;
16.38 -
16.39 -fun mk_decomp_name (Var ((s, i), _)) = rename (if i=0 then s else s ^ string_of_int i)
16.40 - | mk_decomp_name (Const (s, _)) = rename (Codegen.mk_id (Sign.base_name s))
16.41 - | mk_decomp_name _ = "ct";
16.42 -
16.43 -fun decomp_term_code cn ((vs, bs, ps), (v, t)) =
16.44 - if exists (equal t o fst) bs then (vs, bs, ps)
16.45 - else (case t of
16.46 - Var _ => (vs, bs @ [(t, v)], ps)
16.47 - | Const _ => (vs, if cn then bs @ [(t, v)] else bs, ps)
16.48 - | Bound _ => (vs, bs, ps)
16.49 - | Abs (s, T, t) =>
16.50 - let
16.51 - val v1 = variant vs s;
16.52 - val v2 = variant (v1 :: vs) (mk_decomp_name t)
16.53 - in
16.54 - decomp_term_code cn ((v1 :: v2 :: vs,
16.55 - bs @ [(Free (s, T), v1)],
16.56 - ps @ [mk_val [v1, v2] [Pretty.str "Thm.dest_abs", Pretty.brk 1,
16.57 - Pretty.str "NONE", Pretty.brk 1, Pretty.str v]]), (v2, t))
16.58 - end
16.59 - | t $ u =>
16.60 - let
16.61 - val v1 = variant vs (mk_decomp_name t);
16.62 - val v2 = variant (v1 :: vs) (mk_decomp_name u);
16.63 - val (vs', bs', ps') = decomp_term_code cn ((v1 :: v2 :: vs, bs,
16.64 - ps @ [mk_val [v1, v2] [Pretty.str "Thm.dest_comb", Pretty.brk 1,
16.65 - Pretty.str v]]), (v1, t));
16.66 - val (vs'', bs'', ps'') = decomp_term_code cn ((vs', bs', ps'), (v2, u))
16.67 - in
16.68 - if bs'' = bs then (vs, bs, ps) else (vs'', bs'', ps'')
16.69 - end);
16.70 -
16.71 -val strip_tv = implode o tl o explode;
16.72 -
16.73 -fun mk_decomp_tname (TVar ((s, i), _)) =
16.74 - strip_tv ((if i=0 then s else s ^ string_of_int i) ^ "T")
16.75 - | mk_decomp_tname (Type (s, _)) = Codegen.mk_id (Sign.base_name s) ^ "T"
16.76 - | mk_decomp_tname _ = "cT";
16.77 -
16.78 -fun decomp_type_code ((vs, bs, ps), (v, TVar (ixn, _))) =
16.79 - if exists (equal ixn o fst) bs then (vs, bs, ps)
16.80 - else (vs, bs @ [(ixn, v)], ps)
16.81 - | decomp_type_code ((vs, bs, ps), (v, Type (_, Ts))) =
16.82 - let
16.83 - val vs' = variantlist (map mk_decomp_tname Ts, vs);
16.84 - val (vs'', bs', ps') =
16.85 - Library.foldl decomp_type_code ((vs @ vs', bs, ps @
16.86 - [mk_vall vs' [Pretty.str "Thm.dest_ctyp", Pretty.brk 1,
16.87 - Pretty.str v]]), vs' ~~ Ts)
16.88 - in
16.89 - if bs' = bs then (vs, bs, ps) else (vs'', bs', ps')
16.90 - end;
16.91 -
16.92 -fun gen_mk_bindings s dest decomp ((vs, bs, ps), (v, x)) =
16.93 - let
16.94 - val s' = variant vs s;
16.95 - val (vs', bs', ps') = decomp ((s' :: vs, bs, ps @
16.96 - [mk_val [s'] (dest v)]), (s', x))
16.97 - in
16.98 - if bs' = bs then (vs, bs, ps) else (vs', bs', ps')
16.99 - end;
16.100 -
16.101 -val mk_term_bindings = gen_mk_bindings "ct"
16.102 - (fn s => [Pretty.str "cprop_of", Pretty.brk 1, Pretty.str s])
16.103 - (decomp_term_code true);
16.104 -
16.105 -val mk_type_bindings = gen_mk_bindings "cT"
16.106 - (fn s => [Pretty.str "Thm.ctyp_of_term", Pretty.brk 1, Pretty.str s])
16.107 - decomp_type_code;
16.108 -
16.109 -fun pretty_pattern b (Const (s, _)) = Pretty.block [Pretty.str "Const",
16.110 - Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\", _)")]
16.111 - | pretty_pattern b (t as _ $ _) = parens b
16.112 - (List.concat (separate [Pretty.str " $", Pretty.brk 1]
16.113 - (map (single o pretty_pattern true) (op :: (strip_comb t)))))
16.114 - | pretty_pattern b _ = Pretty.str "_";
16.115 -
16.116 -fun term_consts' t = foldl_aterms
16.117 - (fn (cs, c as Const _) => c ins cs | (cs, _) => cs) ([], t);
16.118 -
16.119 -fun mk_apps s b p [] = p
16.120 - | mk_apps s b p (q :: qs) =
16.121 - mk_apps s b (parens (b orelse not (null qs))
16.122 - [Pretty.str s, Pretty.brk 1, p, Pretty.brk 1, q]) qs;
16.123 -
16.124 -fun mk_refleq eq ct = mk_val [eq] [Pretty.str ("Thm.reflexive " ^ ct)];
16.125 -
16.126 -fun mk_tyinst ((s, i), s') =
16.127 - Pretty.block [Pretty.str ("((" ^ quote s ^ ","), Pretty.brk 1,
16.128 - Pretty.str (string_of_int i ^ "),"), Pretty.brk 1,
16.129 - Pretty.str (s' ^ ")")];
16.130 -
16.131 -fun inst_ty b ty_bs t s = (case term_tvars t of
16.132 - [] => Pretty.str s
16.133 - | Ts => parens b [Pretty.str "tyinst_cterm", Pretty.brk 1,
16.134 - Pretty.list "[" "]" (map (fn (ixn, _) => mk_tyinst
16.135 - (ixn, valOf (assoc (ty_bs, ixn)))) Ts),
16.136 - Pretty.brk 1, Pretty.str s]);
16.137 -
16.138 -fun mk_cterm_code b ty_bs ts xs (vals, t $ u) =
16.139 - let
16.140 - val (vals', p1) = mk_cterm_code true ty_bs ts xs (vals, t);
16.141 - val (vals'', p2) = mk_cterm_code true ty_bs ts xs (vals', u)
16.142 - in
16.143 - (vals'', parens b [Pretty.str "Thm.capply", Pretty.brk 1,
16.144 - p1, Pretty.brk 1, p2])
16.145 - end
16.146 - | mk_cterm_code b ty_bs ts xs (vals, Abs (s, T, t)) =
16.147 - let
16.148 - val u = Free (s, T);
16.149 - val SOME s' = assoc (ts, u);
16.150 - val p = Pretty.str s';
16.151 - val (vals', p') = mk_cterm_code true ty_bs ts (p :: xs)
16.152 - (if null (typ_tvars T) then vals
16.153 - else vals @ [(u, (("", s'), [mk_val [s'] [inst_ty true ty_bs u s']]))], t)
16.154 - in (vals',
16.155 - parens b [Pretty.str "Thm.cabs", Pretty.brk 1, p, Pretty.brk 1, p'])
16.156 - end
16.157 - | mk_cterm_code b ty_bs ts xs (vals, Bound i) = (vals, List.nth (xs, i))
16.158 - | mk_cterm_code b ty_bs ts xs (vals, t) = (case assoc (vals, t) of
16.159 - NONE =>
16.160 - let val SOME s = assoc (ts, t)
16.161 - in (if is_Const t andalso not (null (term_tvars t)) then
16.162 - vals @ [(t, (("", s), [mk_val [s] [inst_ty true ty_bs t s]]))]
16.163 - else vals, Pretty.str s)
16.164 - end
16.165 - | SOME ((_, s), _) => (vals, Pretty.str s));
16.166 -
16.167 -fun get_cases sg =
16.168 - Symtab.foldl (fn (tab, (k, {case_rewrites, ...})) => Symtab.update_new
16.169 - ((fst (dest_Const (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
16.170 - (prop_of (hd case_rewrites))))))), map my_mk_meta_eq case_rewrites), tab))
16.171 - (Symtab.empty, DatatypePackage.get_datatypes_sg sg);
16.172 -
16.173 -fun decomp_case th =
16.174 - let
16.175 - val (lhs, _) = Logic.dest_equals (prop_of th);
16.176 - val (f, ts) = strip_comb lhs;
16.177 - val (us, u) = split_last ts;
16.178 - val (Const (s, _), vs) = strip_comb u
16.179 - in (us, s, vs, u) end;
16.180 -
16.181 -fun rename vs t =
16.182 - let
16.183 - fun mk_subst ((vs, subs), Var ((s, i), T)) =
16.184 - let val s' = variant vs s
16.185 - in if s = s' then (vs, subs)
16.186 - else (s' :: vs, ((s, i), Var ((s', i), T)) :: subs)
16.187 - end;
16.188 - val (vs', subs) = Library.foldl mk_subst ((vs, []), term_vars t)
16.189 - in (vs', subst_Vars subs t) end;
16.190 -
16.191 -fun is_instance sg t u = t = subst_TVars_Vartab
16.192 - (Type.typ_match (Sign.tsig_of sg) (Vartab.empty,
16.193 - (fastype_of u, fastype_of t))) u handle Type.TYPE_MATCH => false;
16.194 -
16.195 -(*
16.196 -fun lookup sg fs t = Option.map snd (Library.find_first
16.197 - (is_instance sg t o fst) fs);
16.198 -*)
16.199 -
16.200 -fun lookup sg fs t = (case Library.find_first (is_instance sg t o fst) fs of
16.201 - NONE => (bla := (t ins !bla); NONE)
16.202 - | SOME (_, x) => SOME x);
16.203 -
16.204 -fun unint sg fs t = forall (is_none o lookup sg fs) (term_consts' t);
16.205 -
16.206 -fun mk_let s i xs ys =
16.207 - Pretty.blk (0, [Pretty.blk (i, separate Pretty.fbrk (Pretty.str s :: xs)),
16.208 - Pretty.fbrk,
16.209 - Pretty.blk (i, ([Pretty.str "in", Pretty.fbrk] @ ys)),
16.210 - Pretty.fbrk, Pretty.str "end"]);
16.211 -
16.212 -(*****************************************************************************)
16.213 -(* Generate bindings for simplifying term t *)
16.214 -(* mkeq: whether to generate reflexivity theorem for uninterpreted terms *)
16.215 -(* fs: interpreted functions *)
16.216 -(* ts: atomic terms *)
16.217 -(* vs: used identifiers *)
16.218 -(* vals: list of bindings of the form ((eq, ct), ps) where *)
16.219 -(* eq: name of equational theorem *)
16.220 -(* ct: name of simplified cterm *)
16.221 -(* ps: ML code for creating the above two items *)
16.222 -(*****************************************************************************)
16.223 -
16.224 -fun mk_simpl_code sg case_tab mkeq fs ts ty_bs thm_bs ((vs, vals), t) =
16.225 - (case assoc (vals, t) of
16.226 - SOME ((eq, ct), ps) => (* binding already generated *)
16.227 - if mkeq andalso eq="" then
16.228 - let val eq' = variant vs "eq"
16.229 - in ((eq' :: vs, overwrite (vals,
16.230 - (t, ((eq', ct), ps @ [mk_refleq eq' ct])))), (eq', ct))
16.231 - end
16.232 - else ((vs, vals), (eq, ct))
16.233 - | NONE => (case assoc (ts, t) of
16.234 - SOME v => (* atomic term *)
16.235 - let val xs = if not (null (term_tvars t)) andalso is_Const t then
16.236 - [mk_val [v] [inst_ty false ty_bs t v]] else []
16.237 - in
16.238 - if mkeq then
16.239 - let val eq = variant vs "eq"
16.240 - in ((eq :: vs, vals @
16.241 - [(t, ((eq, v), xs @ [mk_refleq eq v]))]), (eq, v))
16.242 - end
16.243 - else ((vs, if null xs then vals else vals @
16.244 - [(t, (("", v), xs))]), ("", v))
16.245 - end
16.246 - | NONE => (* complex term *)
16.247 - let val (f as Const (cname, _), us) = strip_comb t
16.248 - in case Symtab.lookup (case_tab, cname) of
16.249 - SOME cases => (* case expression *)
16.250 - let
16.251 - val (us', u) = split_last us;
16.252 - val b = unint sg fs u;
16.253 - val ((vs1, vals1), (eq, ct)) =
16.254 - mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs ((vs, vals), u);
16.255 - val xs = variantlist (replicate (length us') "f", vs1);
16.256 - val (vals2, ps) = foldl_map
16.257 - (mk_cterm_code false ty_bs ts []) (vals1, us');
16.258 - val fvals = map (fn (x, p) => mk_val [x] [p]) (xs ~~ ps);
16.259 - val uT = fastype_of u;
16.260 - val (us'', _, _, u') = decomp_case (hd cases);
16.261 - val (vs2, ty_bs', ty_vals) = mk_type_bindings
16.262 - (mk_type_bindings ((vs1 @ xs, [], []),
16.263 - (hd xs, fastype_of (hd us''))), (ct, fastype_of u'));
16.264 - val insts1 = map mk_tyinst ty_bs';
16.265 - val i = length vals2;
16.266 -
16.267 - fun mk_case_code ((vs, vals), (f, (name, eqn))) =
16.268 - let
16.269 - val (fvs, cname, cvs, _) = decomp_case eqn;
16.270 - val Ts = binder_types (fastype_of f);
16.271 - val ys = variantlist (map (fst o fst o dest_Var) cvs, vs);
16.272 - val cvs' = map Var (map (rpair 0) ys ~~ Ts);
16.273 - val rs = cvs' ~~ cvs;
16.274 - val lhs = list_comb (Const (cname, Ts ---> uT), cvs');
16.275 - val rhs = Library.foldl betapply (f, cvs');
16.276 - val (vs', tm_bs, tm_vals) = decomp_term_code false
16.277 - ((vs @ ys, [], []), (ct, lhs));
16.278 - val ((vs'', all_vals), (eq', ct')) = mk_simpl_code sg case_tab
16.279 - false fs (tm_bs @ ts) ty_bs thm_bs ((vs', vals), rhs);
16.280 - val (old_vals, eq_vals) = splitAt (i, all_vals);
16.281 - val vs''' = vs @ List.filter (fn v => exists
16.282 - (fn (_, ((v', _), _)) => v = v') old_vals) (vs'' \\ vs');
16.283 - val insts2 = map (fn (t, s) => Pretty.block [Pretty.str "(",
16.284 - inst_ty false ty_bs' t (valOf (assoc (thm_bs, t))), Pretty.str ",",
16.285 - Pretty.brk 1, Pretty.str (s ^ ")")]) ((fvs ~~ xs) @
16.286 - (map (fn (v, s) => (valOf (assoc (rs, v)), s)) tm_bs));
16.287 - val eq'' = if null insts1 andalso null insts2 then Pretty.str name
16.288 - else parens (eq' <> "") [Pretty.str
16.289 - (if null cvs then "Thm.instantiate" else "Drule.instantiate"),
16.290 - Pretty.brk 1, Pretty.str "(", Pretty.list "[" "]" insts1,
16.291 - Pretty.str ",", Pretty.brk 1, Pretty.list "[" "]" insts2,
16.292 - Pretty.str ")", Pretty.brk 1, Pretty.str name];
16.293 - val eq''' = if eq' = "" then eq'' else
16.294 - Pretty.block [Pretty.str "Thm.transitive", Pretty.brk 1,
16.295 - eq'', Pretty.brk 1, Pretty.str eq']
16.296 - in
16.297 - ((vs''', old_vals), Pretty.block [pretty_pattern false lhs,
16.298 - Pretty.str " =>",
16.299 - Pretty.brk 1, mk_let "let" 2 (tm_vals @ List.concat (map (snd o snd) eq_vals))
16.300 - [Pretty.str ("(" ^ ct' ^ ","), Pretty.brk 1, eq''', Pretty.str ")"]])
16.301 - end;
16.302 -
16.303 - val case_names = map (fn i => Sign.base_name cname ^ "_" ^
16.304 - string_of_int i) (1 upto length cases);
16.305 - val ((vs3, vals3), case_ps) = foldl_map mk_case_code
16.306 - ((vs2, vals2), us' ~~ (case_names ~~ cases));
16.307 - val eq' = variant vs3 "eq";
16.308 - val ct' = variant (eq' :: vs3) "ct";
16.309 - val eq'' = variant (eq' :: ct' :: vs3) "eq";
16.310 - val case_vals =
16.311 - fvals @ ty_vals @
16.312 - [mk_val [ct', eq'] ([Pretty.str "(case", Pretty.brk 1,
16.313 - Pretty.str ("term_of " ^ ct ^ " of"), Pretty.brk 1] @
16.314 - List.concat (separate [Pretty.brk 1, Pretty.str "| "]
16.315 - (map single case_ps)) @ [Pretty.str ")"])]
16.316 - in
16.317 - if b then
16.318 - ((eq' :: ct' :: vs3, vals3 @
16.319 - [(t, ((eq', ct'), case_vals))]), (eq', ct'))
16.320 - else
16.321 - let val ((vs4, vals4), (_, ctcase)) = mk_simpl_code sg case_tab false
16.322 - fs ts ty_bs thm_bs ((eq' :: eq'' :: ct' :: vs3, vals3), f)
16.323 - in
16.324 - ((vs4, vals4 @ [(t, ((eq'', ct'), case_vals @
16.325 - [mk_val [eq''] [Pretty.str "Thm.transitive", Pretty.brk 1,
16.326 - Pretty.str "(Thm.combination", Pretty.brk 1,
16.327 - Pretty.str "(Thm.reflexive", Pretty.brk 1,
16.328 - mk_apps "Thm.capply" true (Pretty.str ctcase)
16.329 - (map Pretty.str xs),
16.330 - Pretty.str ")", Pretty.brk 1, Pretty.str (eq ^ ")"),
16.331 - Pretty.brk 1, Pretty.str eq']]))]), (eq'', ct'))
16.332 - end
16.333 - end
16.334 -
16.335 - | NONE =>
16.336 - let
16.337 - val b = forall (unint sg fs) us;
16.338 - val (q, eqs) = foldl_map
16.339 - (mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs) ((vs, vals), us);
16.340 - val ((vs', vals'), (eqf, ctf)) = if isSome (lookup sg fs f) andalso b
16.341 - then (q, ("", ""))
16.342 - else mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs (q, f);
16.343 - val ct = variant vs' "ct";
16.344 - val eq = variant (ct :: vs') "eq";
16.345 - val ctv = mk_val [ct] [mk_apps "Thm.capply" false
16.346 - (Pretty.str ctf) (map (Pretty.str o snd) eqs)];
16.347 - fun combp b = mk_apps "Thm.combination" b
16.348 - (Pretty.str eqf) (map (Pretty.str o fst) eqs)
16.349 - in
16.350 - case (lookup sg fs f, b) of
16.351 - (NONE, true) => (* completely uninterpreted *)
16.352 - if mkeq then ((ct :: eq :: vs', vals' @
16.353 - [(t, ((eq, ct), [ctv, mk_refleq eq ct]))]), (eq, ct))
16.354 - else ((ct :: vs', vals' @ [(t, (("", ct), [ctv]))]), ("", ct))
16.355 - | (NONE, false) => (* function uninterpreted *)
16.356 - ((eq :: ct :: vs', vals' @
16.357 - [(t, ((eq, ct), [ctv, mk_val [eq] [combp false]]))]), (eq, ct))
16.358 - | (SOME (s, _, _), true) => (* arguments uninterpreted *)
16.359 - ((eq :: ct :: vs', vals' @
16.360 - [(t, ((eq, ct), [mk_val [ct, eq] (separate (Pretty.brk 1)
16.361 - (Pretty.str s :: map (Pretty.str o snd) eqs))]))]), (eq, ct))
16.362 - | (SOME (s, _, _), false) => (* function and arguments interpreted *)
16.363 - let val eq' = variant (eq :: ct :: vs') "eq"
16.364 - in ((eq' :: eq :: ct :: vs', vals' @ [(t, ((eq', ct),
16.365 - [mk_val [ct, eq] (separate (Pretty.brk 1)
16.366 - (Pretty.str s :: map (Pretty.str o snd) eqs)),
16.367 - mk_val [eq'] [Pretty.str "Thm.transitive", Pretty.brk 1,
16.368 - combp true, Pretty.brk 1, Pretty.str eq]]))]), (eq', ct))
16.369 - end
16.370 - end
16.371 - end));
16.372 -
16.373 -fun lhs_of thm = fst (Logic.dest_equals (prop_of thm));
16.374 -fun rhs_of thm = snd (Logic.dest_equals (prop_of thm));
16.375 -
16.376 -fun mk_funs_code sg case_tab fs fs' =
16.377 - let
16.378 - val case_thms = List.mapPartial (fn s => (case Symtab.lookup (case_tab, s) of
16.379 - NONE => NONE
16.380 - | SOME thms => SOME (unsuffix "_case" (Sign.base_name s) ^ ".cases",
16.381 - map (fn i => Sign.base_name s ^ "_" ^ string_of_int i)
16.382 - (1 upto length thms) ~~ thms)))
16.383 - (foldr add_term_consts [] (map (prop_of o snd)
16.384 - (List.concat (map (#3 o snd) fs'))));
16.385 - val case_vals = map (fn (s, cs) => mk_vall (map fst cs)
16.386 - [Pretty.str "map my_mk_meta_eq", Pretty.brk 1,
16.387 - Pretty.str ("(thms \"" ^ s ^ "\")")]) case_thms;
16.388 - val (vs, thm_bs, thm_vals) = Library.foldl mk_term_bindings (([], [], []),
16.389 - List.concat (map (map (apsnd prop_of) o #3 o snd) fs') @
16.390 - map (apsnd prop_of) (List.concat (map snd case_thms)));
16.391 -
16.392 - fun mk_fun_code (prfx, (fname, d, eqns)) =
16.393 - let
16.394 - val (f, ts) = strip_comb (lhs_of (snd (hd eqns)));
16.395 - val args = variantlist (replicate (length ts) "ct", vs);
16.396 - val (vs', ty_bs, ty_vals) = Library.foldl mk_type_bindings
16.397 - ((vs @ args, [], []), args ~~ map fastype_of ts);
16.398 - val insts1 = map mk_tyinst ty_bs;
16.399 -
16.400 - fun mk_eqn_code (name, eqn) =
16.401 - let
16.402 - val (_, argts) = strip_comb (lhs_of eqn);
16.403 - val (vs'', tm_bs, tm_vals) = Library.foldl (decomp_term_code false)
16.404 - ((vs', [], []), args ~~ argts);
16.405 - val ((vs''', eq_vals), (eq, ct)) = mk_simpl_code sg case_tab false fs
16.406 - (tm_bs @ filter_out (is_Var o fst) thm_bs) ty_bs thm_bs
16.407 - ((vs'', []), rhs_of eqn);
16.408 - val insts2 = map (fn (t, s) => Pretty.block [Pretty.str "(",
16.409 - inst_ty false ty_bs t (valOf (assoc (thm_bs, t))), Pretty.str ",", Pretty.brk 1,
16.410 - Pretty.str (s ^ ")")]) tm_bs
16.411 - val eq' = if null insts1 andalso null insts2 then Pretty.str name
16.412 - else parens (eq <> "") [Pretty.str "Thm.instantiate",
16.413 - Pretty.brk 1, Pretty.str "(", Pretty.list "[" "]" insts1,
16.414 - Pretty.str ",", Pretty.brk 1, Pretty.list "[" "]" insts2,
16.415 - Pretty.str ")", Pretty.brk 1, Pretty.str name];
16.416 - val eq'' = if eq = "" then eq' else
16.417 - Pretty.block [Pretty.str "Thm.transitive", Pretty.brk 1,
16.418 - eq', Pretty.brk 1, Pretty.str eq]
16.419 - in
16.420 - Pretty.block [parens (length argts > 1)
16.421 - (Pretty.commas (map (pretty_pattern false) argts)),
16.422 - Pretty.str " =>",
16.423 - Pretty.brk 1, mk_let "let" 2 (ty_vals @ tm_vals @ List.concat (map (snd o snd) eq_vals))
16.424 - [Pretty.str ("(" ^ ct ^ ","), Pretty.brk 1, eq'', Pretty.str ")"]]
16.425 - end;
16.426 -
16.427 - val default = if d then
16.428 - let
16.429 - val SOME s = assoc (thm_bs, f);
16.430 - val ct = variant vs' "ct"
16.431 - in [Pretty.brk 1, Pretty.str "handle", Pretty.brk 1,
16.432 - Pretty.str "Match =>", Pretty.brk 1, mk_let "let" 2
16.433 - (ty_vals @ (if null (term_tvars f) then [] else
16.434 - [mk_val [s] [inst_ty false ty_bs f s]]) @
16.435 - [mk_val [ct] [mk_apps "Thm.capply" false (Pretty.str s)
16.436 - (map Pretty.str args)]])
16.437 - [Pretty.str ("(" ^ ct ^ ","), Pretty.brk 1,
16.438 - Pretty.str "Thm.reflexive", Pretty.brk 1, Pretty.str (ct ^ ")")]]
16.439 - end
16.440 - else []
16.441 - in
16.442 - ("and ", Pretty.block (separate (Pretty.brk 1)
16.443 - (Pretty.str (prfx ^ fname) :: map Pretty.str args) @
16.444 - [Pretty.str " =", Pretty.brk 1, Pretty.str "(case", Pretty.brk 1,
16.445 - Pretty.list "(" ")" (map (fn s => Pretty.str ("term_of " ^ s)) args),
16.446 - Pretty.str " of", Pretty.brk 1] @
16.447 - List.concat (separate [Pretty.brk 1, Pretty.str "| "]
16.448 - (map (single o mk_eqn_code) eqns)) @ [Pretty.str ")"] @ default))
16.449 - end;
16.450 -
16.451 - val (_, decls) = foldl_map mk_fun_code ("fun ", map snd fs')
16.452 - in
16.453 - mk_let "local" 2 (case_vals @ thm_vals) (separate Pretty.fbrk decls)
16.454 - end;
16.455 -
16.456 -fun mk_simprocs_code sg eqns =
16.457 - let
16.458 - val case_tab = get_cases sg;
16.459 - fun get_head th = head_of (fst (Logic.dest_equals (prop_of th)));
16.460 - fun attach_term (x as (_, _, (_, th) :: _)) = (get_head th, x);
16.461 - val eqns' = map attach_term eqns;
16.462 - fun mk_node (s, _, (_, th) :: _) = (s, get_head th);
16.463 - fun mk_edges (s, _, ths) = map (pair s) (distinct
16.464 - (List.mapPartial (fn t => Option.map #1 (lookup sg eqns' t))
16.465 - (List.concat (map (term_consts' o prop_of o snd) ths))));
16.466 - val gr = foldr (uncurry Graph.add_edge)
16.467 - (Library.foldr (uncurry Graph.new_node)
16.468 - (("", Bound 0) :: map mk_node eqns, Graph.empty))
16.469 - (map (pair "" o #1) eqns @ List.concat (map mk_edges eqns));
16.470 - val keys = rev (Graph.all_succs gr [""] \ "");
16.471 - fun gr_ord (x :: _, y :: _) =
16.472 - int_ord (find_index (equal x) keys, find_index (equal y) keys);
16.473 - val scc = map (fn xs => List.filter (fn (_, (s, _, _)) => s mem xs) eqns')
16.474 - (sort gr_ord (Graph.strong_conn gr \ [""]));
16.475 - in
16.476 - List.concat (separate [Pretty.str ";", Pretty.fbrk, Pretty.str " ", Pretty.fbrk]
16.477 - (map (fn eqns'' => [mk_funs_code sg case_tab eqns' eqns'']) scc)) @
16.478 - [Pretty.str ";", Pretty.fbrk]
16.479 - end;
16.480 -
16.481 -fun use_simprocs_code sg eqns =
16.482 - let
16.483 - fun attach_name (i, x) = (i+1, ("simp_thm_" ^ string_of_int i, x));
16.484 - fun attach_names (i, (s, b, eqs)) =
16.485 - let val (i', eqs') = foldl_map attach_name (i, eqs)
16.486 - in (i', (s, b, eqs')) end;
16.487 - val (_, eqns') = foldl_map attach_names (1, eqns);
16.488 - val (names, thms) = split_list (List.concat (map #3 eqns'));
16.489 - val s = setmp print_mode [] Pretty.string_of
16.490 - (mk_let "local" 2 [mk_vall names [Pretty.str "!SimprocsCodegen.simp_thms"]]
16.491 - (mk_simprocs_code sg eqns'))
16.492 - in
16.493 - (simp_thms := thms; use_text Context.ml_output false s)
16.494 - end;
16.495 -
16.496 -end;
17.1 --- a/src/HOL/Matrix/fspmlp.ML Mon Mar 07 16:55:36 2005 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,303 +0,0 @@
17.4 -signature FSPMLP =
17.5 -sig
17.6 - type linprog
17.7 -
17.8 - val y : linprog -> cterm
17.9 - val A : linprog -> cterm * cterm
17.10 - val b : linprog -> cterm
17.11 - val c : linprog -> cterm * cterm
17.12 - val r : linprog -> cterm
17.13 -
17.14 - exception Load of string
17.15 -
17.16 - val load : string -> int -> bool -> linprog
17.17 -end
17.18 -
17.19 -structure fspmlp : FSPMLP =
17.20 -struct
17.21 -
17.22 -type linprog = cterm * (cterm * cterm) * cterm * (cterm * cterm) * cterm
17.23 -
17.24 -fun y (c1, c2, c3, c4, c5) = c1
17.25 -fun A (c1, c2, c3, c4, c5) = c2
17.26 -fun b (c1, c2, c3, c4, c5) = c3
17.27 -fun c (c1, c2, c3, c4, c5) = c4
17.28 -fun r (c1, c2, c3, c4, c5) = c5
17.29 -
17.30 -structure CplexFloatSparseMatrixConverter =
17.31 -MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);
17.32 -
17.33 -datatype bound_type = LOWER | UPPER
17.34 -
17.35 -fun intbound_ord ((i1, b1),(i2,b2)) =
17.36 - if i1 < i2 then LESS
17.37 - else if i1 = i2 then
17.38 - (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
17.39 - else GREATER
17.40 -
17.41 -structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
17.42 -
17.43 -structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
17.44 -(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
17.45 -(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
17.46 -
17.47 -exception Internal of string;
17.48 -
17.49 -fun add_row_bound g dest_key row_index row_bound =
17.50 - let
17.51 - val x =
17.52 - case VarGraph.lookup (g, dest_key) of
17.53 - NONE => (NONE, Inttab.update ((row_index, (row_bound, [])), Inttab.empty))
17.54 - | SOME (sure_bound, f) =>
17.55 - (sure_bound,
17.56 - case Inttab.lookup (f, row_index) of
17.57 - NONE => Inttab.update ((row_index, (row_bound, [])), f)
17.58 - | SOME _ => raise (Internal "add_row_bound"))
17.59 - in
17.60 - VarGraph.update ((dest_key, x), g)
17.61 - end
17.62 -
17.63 -fun update_sure_bound g (key as (_, btype)) bound =
17.64 - let
17.65 - val x =
17.66 - case VarGraph.lookup (g, key) of
17.67 - NONE => (SOME bound, Inttab.empty)
17.68 - | SOME (NONE, f) => (SOME bound, f)
17.69 - | SOME (SOME old_bound, f) =>
17.70 - (SOME ((case btype of
17.71 - UPPER => FloatArith.min
17.72 - | LOWER => FloatArith.max)
17.73 - old_bound bound), f)
17.74 - in
17.75 - VarGraph.update ((key, x), g)
17.76 - end
17.77 -
17.78 -fun get_sure_bound g key =
17.79 - case VarGraph.lookup (g, key) of
17.80 - NONE => NONE
17.81 - | SOME (sure_bound, _) => sure_bound
17.82 -
17.83 -(*fun get_row_bound g key row_index =
17.84 - case VarGraph.lookup (g, key) of
17.85 - NONE => NONE
17.86 - | SOME (sure_bound, f) =>
17.87 - (case Inttab.lookup (f, row_index) of
17.88 - NONE => NONE
17.89 - | SOME (row_bound, _) => (sure_bound, row_bound))*)
17.90 -
17.91 -fun add_edge g src_key dest_key row_index coeff =
17.92 - case VarGraph.lookup (g, dest_key) of
17.93 - NONE => raise (Internal "add_edge: dest_key not found")
17.94 - | SOME (sure_bound, f) =>
17.95 - (case Inttab.lookup (f, row_index) of
17.96 - NONE => raise (Internal "add_edge: row_index not found")
17.97 - | SOME (row_bound, sources) =>
17.98 - VarGraph.update ((dest_key, (sure_bound, Inttab.update ((row_index, (row_bound, (coeff, src_key) :: sources)), f))), g))
17.99 -
17.100 -fun split_graph g =
17.101 - let
17.102 - fun split ((r1, r2), (key, (sure_bound, _))) =
17.103 - case sure_bound of
17.104 - NONE => (r1, r2)
17.105 - | SOME bound =>
17.106 - (case key of
17.107 - (u, UPPER) => (r1, Inttab.update ((u, bound), r2))
17.108 - | (u, LOWER) => (Inttab.update ((u, bound), r1), r2))
17.109 - in
17.110 - VarGraph.foldl split ((Inttab.empty, Inttab.empty), g)
17.111 - end
17.112 -
17.113 -fun it2list t =
17.114 - let
17.115 - fun tolist (l, a) = a::l
17.116 - in
17.117 - Inttab.foldl tolist ([], t)
17.118 - end
17.119 -
17.120 -(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
17.121 - If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
17.122 -fun propagate_sure_bounds safe names g =
17.123 - let
17.124 - (* returns NONE if no new sure bound could be calculated, otherwise the new sure bound is returned *)
17.125 - fun calc_sure_bound_from_sources g (key as (_, btype)) =
17.126 - let
17.127 - fun mult_upper x (lower, upper) =
17.128 - if FloatArith.is_negative x then
17.129 - FloatArith.mul x lower
17.130 - else
17.131 - FloatArith.mul x upper
17.132 -
17.133 - fun mult_lower x (lower, upper) =
17.134 - if FloatArith.is_negative x then
17.135 - FloatArith.mul x upper
17.136 - else
17.137 - FloatArith.mul x lower
17.138 -
17.139 - val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
17.140 -
17.141 - fun calc_sure_bound (sure_bound, (row_index, (row_bound, sources))) =
17.142 - let
17.143 - fun add_src_bound (sum, (coeff, src_key)) =
17.144 - case sum of
17.145 - NONE => NONE
17.146 - | SOME x =>
17.147 - (case get_sure_bound g src_key of
17.148 - NONE => NONE
17.149 - | SOME src_sure_bound => SOME (FloatArith.add x (mult_btype src_sure_bound coeff)))
17.150 - in
17.151 - case Library.foldl add_src_bound (SOME row_bound, sources) of
17.152 - NONE => sure_bound
17.153 - | new_sure_bound as (SOME new_bound) =>
17.154 - (case sure_bound of
17.155 - NONE => new_sure_bound
17.156 - | SOME old_bound =>
17.157 - SOME (case btype of
17.158 - UPPER => FloatArith.min old_bound new_bound
17.159 - | LOWER => FloatArith.max old_bound new_bound))
17.160 - end
17.161 - in
17.162 - case VarGraph.lookup (g, key) of
17.163 - NONE => NONE
17.164 - | SOME (sure_bound, f) =>
17.165 - let
17.166 - val x = Inttab.foldl calc_sure_bound (sure_bound, f)
17.167 - in
17.168 - if x = sure_bound then NONE else x
17.169 - end
17.170 - end
17.171 -
17.172 - fun propagate ((g, b), (key, _)) =
17.173 - case calc_sure_bound_from_sources g key of
17.174 - NONE => (g,b)
17.175 - | SOME bound => (update_sure_bound g key bound,
17.176 - if safe then
17.177 - case get_sure_bound g key of
17.178 - NONE => true
17.179 - | _ => b
17.180 - else
17.181 - true)
17.182 -
17.183 - val (g, b) = VarGraph.foldl propagate ((g, false), g)
17.184 - in
17.185 - if b then propagate_sure_bounds safe names g else g
17.186 - end
17.187 -
17.188 -exception Load of string;
17.189 -
17.190 -fun calcr safe_propagation xlen names prec A b =
17.191 - let
17.192 - val empty = Inttab.empty
17.193 -
17.194 - fun instab t i x = Inttab.update ((i,x), t)
17.195 -
17.196 - fun isnegstr x = String.isPrefix "-" x
17.197 - fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
17.198 -
17.199 - fun test_1 (lower, upper) =
17.200 - if lower = upper then
17.201 - (if FloatArith.is_equal lower (IntInf.fromInt ~1, FloatArith.izero) then ~1
17.202 - else if FloatArith.is_equal lower (IntInf.fromInt 1, FloatArith.izero) then 1
17.203 - else 0)
17.204 - else 0
17.205 -
17.206 - fun calcr (g, (row_index, a)) =
17.207 - let
17.208 - val b = FloatSparseMatrixBuilder.v_elem_at b row_index
17.209 - val (_, b2) = ExactFloatingPoint.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
17.210 - val approx_a = FloatSparseMatrixBuilder.v_fold (fn (l, (i,s)) =>
17.211 - (i, ExactFloatingPoint.approx_decstr_by_bin prec s)::l) [] a
17.212 -
17.213 - fun fold_dest_nodes (g, (dest_index, dest_value)) =
17.214 - let
17.215 - val dest_test = test_1 dest_value
17.216 - in
17.217 - if dest_test = 0 then
17.218 - g
17.219 - else let
17.220 - val (dest_key as (_, dest_btype), row_bound) =
17.221 - if dest_test = ~1 then
17.222 - ((dest_index, LOWER), FloatArith.neg b2)
17.223 - else
17.224 - ((dest_index, UPPER), b2)
17.225 -
17.226 - fun fold_src_nodes (g, (src_index, src_value as (src_lower, src_upper))) =
17.227 - if src_index = dest_index then g
17.228 - else
17.229 - let
17.230 - val coeff = case dest_btype of
17.231 - UPPER => (FloatArith.neg src_upper, FloatArith.neg src_lower)
17.232 - | LOWER => src_value
17.233 - in
17.234 - if FloatArith.is_negative src_lower then
17.235 - add_edge g (src_index, UPPER) dest_key row_index coeff
17.236 - else
17.237 - add_edge g (src_index, LOWER) dest_key row_index coeff
17.238 - end
17.239 - in
17.240 - Library.foldl fold_src_nodes ((add_row_bound g dest_key row_index row_bound), approx_a)
17.241 - end
17.242 - end
17.243 - in
17.244 - case approx_a of
17.245 - [] => g
17.246 - | [(u, a)] =>
17.247 - let
17.248 - val atest = test_1 a
17.249 - in
17.250 - if atest = ~1 then
17.251 - update_sure_bound g (u, LOWER) (FloatArith.neg b2)
17.252 - else if atest = 1 then
17.253 - update_sure_bound g (u, UPPER) b2
17.254 - else
17.255 - g
17.256 - end
17.257 - | _ => Library.foldl fold_dest_nodes (g, approx_a)
17.258 - end
17.259 -
17.260 - val g = FloatSparseMatrixBuilder.m_fold calcr VarGraph.empty A
17.261 - val g = propagate_sure_bounds safe_propagation names g
17.262 -
17.263 - val (r1, r2) = split_graph g
17.264 -
17.265 - fun abs_estimate i r1 r2 =
17.266 - if i = 0 then FloatSparseMatrixBuilder.empty_spmat
17.267 - else
17.268 - let
17.269 - val index = xlen-i
17.270 - val r = abs_estimate (i-1) r1 r2
17.271 - val b1 = case Inttab.lookup (r1, index) of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
17.272 - val b2 = case Inttab.lookup (r2, index) of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
17.273 - val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2)
17.274 - val vec = FloatSparseMatrixBuilder.cons_spvec (FloatSparseMatrixBuilder.mk_spvec_entry 0 abs_max) FloatSparseMatrixBuilder.empty_spvec
17.275 - in
17.276 - FloatSparseMatrixBuilder.cons_spmat (FloatSparseMatrixBuilder.mk_spmat_entry index vec) r
17.277 - end
17.278 - in
17.279 - FloatSparseMatrixBuilder.sign_term (abs_estimate xlen r1 r2)
17.280 - end
17.281 -
17.282 -fun load filename prec safe_propagation =
17.283 - let
17.284 - val prog = Cplex.load_cplexFile filename
17.285 - val prog = Cplex.elim_nonfree_bounds prog
17.286 - val prog = Cplex.relax_strict_ineqs prog
17.287 - val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog
17.288 - val r = calcr safe_propagation xlen names prec A b
17.289 - val _ = if maximize then () else raise Load "sorry, cannot handle minimization problems"
17.290 - val (dualprog, indexof) = FloatSparseMatrixBuilder.dual_cplexProg c A b
17.291 - val results = Cplex.solve dualprog
17.292 - val (optimal,v) = CplexFloatSparseMatrixConverter.convert_results results indexof
17.293 - val A = FloatSparseMatrixBuilder.cut_matrix v NONE A
17.294 - fun id x = x
17.295 - val v = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 v
17.296 - val b = FloatSparseMatrixBuilder.transpose_matrix (FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 b)
17.297 - val c = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 c
17.298 - val (y1, _) = FloatSparseMatrixBuilder.approx_matrix prec FloatArith.positive_part v
17.299 - val A = FloatSparseMatrixBuilder.approx_matrix prec id A
17.300 - val (_,b2) = FloatSparseMatrixBuilder.approx_matrix prec id b
17.301 - val c = FloatSparseMatrixBuilder.approx_matrix prec id c
17.302 - in
17.303 - (y1, A, b2, c, r)
17.304 - end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
17.305 -
17.306 -end
17.307 \ No newline at end of file
18.1 --- a/src/HOL/OrderedGroup.thy Mon Mar 07 16:55:36 2005 +0100
18.2 +++ b/src/HOL/OrderedGroup.thy Mon Mar 07 18:19:55 2005 +0100
18.3 @@ -594,6 +594,21 @@
18.4 from a b show ?thesis by blast
18.5 qed
18.6
18.7 +lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
18.8 +lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
18.9 +
18.10 +lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
18.11 + by (simp add: pprt_def le_def_join join_aci)
18.12 +
18.13 +lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
18.14 + by (simp add: nprt_def le_def_meet meet_aci)
18.15 +
18.16 +lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
18.17 + by (simp add: pprt_def le_def_join join_aci)
18.18 +
18.19 +lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
18.20 + by (simp add: nprt_def le_def_meet meet_aci)
18.21 +
18.22 lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
18.23 proof -
18.24 {
18.25 @@ -776,6 +791,12 @@
18.26 lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
18.27 by (simp add: le_def_meet nprt_def meet_comm)
18.28
18.29 +lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
18.30 + by (simp add: le_def_join pprt_def join_aci)
18.31 +
18.32 +lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
18.33 + by (simp add: le_def_meet nprt_def meet_aci)
18.34 +
18.35 lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
18.36 by (simp)
18.37
19.1 --- a/src/HOL/Ring_and_Field.thy Mon Mar 07 16:55:36 2005 +0100
19.2 +++ b/src/HOL/Ring_and_Field.thy Mon Mar 07 18:19:55 2005 +0100
19.3 @@ -1532,12 +1532,6 @@
19.4 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
19.5 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
19.6
19.7 -lemma abs_eq [simp]: "(0::'a::ordered_idom) \<le> a ==> abs a = a"
19.8 -by (simp add: abs_if linorder_not_less [symmetric])
19.9 -
19.10 -lemma abs_minus_eq [simp]: "a < (0::'a::ordered_idom) ==> abs a = -a"
19.11 -by (simp add: abs_if linorder_not_less [symmetric])
19.12 -
19.13 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
19.14 proof -
19.15 let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
19.16 @@ -1599,10 +1593,6 @@
19.17 assume "0 <= a * b"
19.18 then show ?thesis
19.19 apply (simp_all add: mulprts abs_prts)
19.20 - apply (simp add:
19.21 - iff2imp[OF zero_le_iff_zero_nprt]
19.22 - iff2imp[OF le_zero_iff_pprt_id]
19.23 - )
19.24 apply (insert prems)
19.25 apply (auto simp add:
19.26 ring_eq_simps
19.27 @@ -1617,8 +1607,7 @@
19.28 then show ?thesis
19.29 apply (simp_all add: mulprts abs_prts)
19.30 apply (insert prems)
19.31 - apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
19.32 - iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
19.33 + apply (auto simp add: ring_eq_simps)
19.34 apply(drule (1) mult_pos_le[of a b],simp)
19.35 apply(drule (1) mult_neg_le[of a b],simp)
19.36 done
19.37 @@ -1740,24 +1729,86 @@
19.38 with prems show "abs (A-A1) <= (A2-A1)" by simp
19.39 qed
19.40
19.41 -lemma linprog_dual_estimate_1:
19.42 +lemma mult_le_prts:
19.43 + assumes
19.44 + "a1 <= (a::'a::lordered_ring)"
19.45 + "a <= a2"
19.46 + "b1 <= b"
19.47 + "b <= b2"
19.48 + shows
19.49 + "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
19.50 +proof -
19.51 + have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
19.52 + apply (subst prts[symmetric])+
19.53 + apply simp
19.54 + done
19.55 + then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
19.56 + by (simp add: ring_eq_simps)
19.57 + moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
19.58 + by (simp_all add: prems mult_mono)
19.59 + moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
19.60 + proof -
19.61 + have "pprt a * nprt b <= pprt a * nprt b2"
19.62 + by (simp add: mult_left_mono prems)
19.63 + moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
19.64 + by (simp add: mult_right_mono_neg prems)
19.65 + ultimately show ?thesis
19.66 + by simp
19.67 + qed
19.68 + moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
19.69 + proof -
19.70 + have "nprt a * pprt b <= nprt a2 * pprt b"
19.71 + by (simp add: mult_right_mono prems)
19.72 + moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
19.73 + by (simp add: mult_left_mono_neg prems)
19.74 + ultimately show ?thesis
19.75 + by simp
19.76 + qed
19.77 + moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
19.78 + proof -
19.79 + have "nprt a * nprt b <= nprt a * nprt b1"
19.80 + by (simp add: mult_left_mono_neg prems)
19.81 + moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
19.82 + by (simp add: mult_right_mono_neg prems)
19.83 + ultimately show ?thesis
19.84 + by simp
19.85 + qed
19.86 + ultimately show ?thesis
19.87 + by - (rule add_mono | simp)+
19.88 +qed
19.89 +
19.90 +lemma mult_le_dual_prts:
19.91 assumes
19.92 "A * x \<le> (b::'a::lordered_ring)"
19.93 "0 \<le> y"
19.94 - "A1 <= A"
19.95 - "A <= A2"
19.96 - "c1 <= c"
19.97 - "c <= c2"
19.98 - "abs x \<le> r"
19.99 + "A1 \<le> A"
19.100 + "A \<le> A2"
19.101 + "c1 \<le> c"
19.102 + "c \<le> c2"
19.103 + "r1 \<le> x"
19.104 + "x \<le> r2"
19.105 shows
19.106 - "c * x \<le> y * b + (y * (A2 - A1) + abs (y * A1 - c1) + (c2 - c1)) * r"
19.107 + "c * x \<le> y * b + (let s1 = c1 - y * A2; s2 = c2 - y * A1 in pprt s2 * pprt r2 + pprt s1 * nprt r2 + nprt s2 * pprt r1 + nprt s1 * nprt r1)"
19.108 + (is "_ <= _ + ?C")
19.109 proof -
19.110 - from prems have delta_A: "abs (A-A1) <= (A2-A1)" by (simp add: le_ge_imp_abs_diff_1)
19.111 - from prems have delta_c: "abs (c-c1) <= (c2-c1)" by (simp add: le_ge_imp_abs_diff_1)
19.112 - show ?thesis
19.113 - apply (rule_tac linprog_dual_estimate)
19.114 - apply (auto intro: delta_A delta_c simp add: prems)
19.115 + from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono)
19.116 + moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_eq_simps)
19.117 + ultimately have "c * x + (y * A - c) * x <= y * b" by simp
19.118 + then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
19.119 + then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_eq_simps)
19.120 + have s2: "c - y * A <= c2 - y * A1"
19.121 + by (simp add: diff_def prems add_mono mult_left_mono)
19.122 + have s1: "c1 - y * A2 <= c - y * A"
19.123 + by (simp add: diff_def prems add_mono mult_left_mono)
19.124 + have prts: "(c - y * A) * x <= ?C"
19.125 + apply (simp add: Let_def)
19.126 + apply (rule mult_le_prts)
19.127 + apply (simp_all add: prems s1 s2)
19.128 done
19.129 + then have "y * b + (c - y * A) * x <= y * b + ?C"
19.130 + by simp
19.131 + with cx show ?thesis
19.132 + by(simp only:)
19.133 qed
19.134
19.135 ML {*