author  wenzelm 
Thu, 20 Mar 2008 00:20:44 +0100  
changeset 26343  0dd2eab7b296 
parent 26336  a0e2b706ce73 
child 27484  dbb9981c3d18 
permissions  rwrr 
24584  1 
(* Title: HOL/Matrix/cplex/matrixlp.ML 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

3 
Author: Steven Obua 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

4 
*) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

5 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

6 
signature MATRIX_LP = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

7 
sig 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

8 
val lp_dual_estimate_prt : string > int > thm 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

9 
val lp_dual_estimate_prt_primitive : 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

10 
cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) > thm 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

11 
val matrix_compute : cterm > thm 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

12 
val matrix_simplify : thm > thm 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

13 
val prove_bound : string > int > thm 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

14 
val float2real : string * string > Real.real 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

15 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

16 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

17 
structure MatrixLP : MATRIX_LP = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

18 
struct 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

19 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

20 
fun inst_real thm = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

21 
let val certT = ctyp_of (Thm.theory_of_thm thm) in 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

22 
standard (Thm.instantiate 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

23 
([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

24 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

25 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

26 
local 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

27 

825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

28 
val cert = cterm_of @{theory "Cplex"} 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

29 

825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

30 
in 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

31 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

32 
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

33 
let 
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

34 
val th = inst_real @{thm "SparseMatrix.spm_mult_le_dual_prts_no_let"} 
22964  35 
fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x) 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

36 
val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

37 
var "r1" r1, var "r2" r2, var "b" b]) th 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

38 
in th end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

39 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

40 
fun lp_dual_estimate_prt lptfile prec = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

41 
let 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

42 
val certificate = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

43 
let 
22964  44 
open Fspmlp 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

45 
val l = load lptfile prec false 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

46 
in 
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

47 
(y l > cert, A l > pairself cert, c l > pairself cert, b l > cert, r12 l > pairself cert) 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

48 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

49 
in 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

50 
lp_dual_estimate_prt_primitive certificate 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

51 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

52 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

53 
end 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

54 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

55 
fun prep ths = ComputeHOL.prep_thms ths 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

56 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

57 
fun inst_tvar ty thm = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

58 
let 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

59 
val certT = Thm.ctyp_of (Thm.theory_of_thm thm); 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

60 
val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

61 
val v = TVar (hd (sort ord (term_tvars (prop_of thm)))) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

62 
in 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

63 
standard (Thm.instantiate ([(certT v, certT ty)], []) thm) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

64 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

65 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

66 
fun inst_tvars [] thms = thms 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

67 
 inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

68 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

69 
local 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

70 
val matrix_lemmas = [ 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

71 
"ComputeHOL.compute_list_case", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

72 
"ComputeHOL.compute_let", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

73 
"ComputeHOL.compute_if", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

74 
"Float.arith", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

75 
"SparseMatrix.sparse_row_matrix_arith_simps", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

76 
"ComputeHOL.compute_bool", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

77 
"ComputeHOL.compute_pair", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

78 
"SparseMatrix.sorted_sp_simps", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

79 
"ComputeNumeral.number_norm", 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

80 
"ComputeNumeral.natnorm"] 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

81 
fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n) 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

82 
val ths = maps get_thms matrix_lemmas 
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

83 
val computer = PCompute.make Compute.SML @{theory "Cplex"} ths [] 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

84 
in 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

85 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

86 
fun matrix_compute c = hd (PCompute.rewrite computer [c]) 
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

87 

23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

88 
end 
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset

89 

20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

90 
fun matrix_simplify th = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

91 
let 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

92 
val simp_th = matrix_compute (cprop_of th) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

93 
val th = strip_shyps (equal_elim simp_th th) 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

94 
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

95 
in 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

96 
removeTrue th 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

97 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

98 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

99 
fun prove_bound lptfile prec = 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

100 
let 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

101 
val th = lp_dual_estimate_prt lptfile prec 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

102 
in 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

103 
matrix_simplify th 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

104 
end 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

105 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

106 
val realFromStr = the o Real.fromString; 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

107 
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y); 
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

108 

406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset

109 
end 