Cleaning up HOL/Matrix
authorobua
Mon Mar 07 18:19:55 2005 +0100 (2005-03-07)
changeset 15580900291ee0af8
parent 15579 32bee18c675f
child 15581 f07e865d9d40
Cleaning up HOL/Matrix
src/HOL/IsaMakefile
src/HOL/Matrix/Cplex.ML
src/HOL/Matrix/CplexMatrixConverter.ML
src/HOL/Matrix/ExactFloatingPoint.ML
src/HOL/Matrix/Float.thy
src/HOL/Matrix/FloatArith.ML
src/HOL/Matrix/FloatSparseMatrixBuilder.ML
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Matrix/MatrixLP.ML
src/HOL/Matrix/MatrixLP.thy
src/HOL/Matrix/MatrixLP_gensimp.ML
src/HOL/Matrix/ROOT.ML
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Matrix/codegen_prep.ML
src/HOL/Matrix/conv.ML
src/HOL/Matrix/eq_codegen.ML
src/HOL/Matrix/fspmlp.ML
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
     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 {*