| author | blanchet |
| Tue, 06 Jan 2015 09:59:43 +0100 | |
| changeset 59300 | 7009e5fa5cd3 |
| parent 55413 | a8e96847523c |
| child 59582 | 0fbed69ff081 |
| permissions | -rw-r--r-- |
| 47455 | 1 |
(* Title: HOL/Matrix_LP/matrixlp.ML |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Steven Obua |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
3 |
*) |
|
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 |
signature MATRIX_LP = |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
6 |
sig |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
7 |
val matrix_compute : cterm -> thm |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
8 |
val matrix_simplify : thm -> thm |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
9 |
end |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
10 |
|
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
11 |
structure MatrixLP : MATRIX_LP = |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
12 |
struct |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
13 |
|
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
53737
diff
changeset
|
14 |
val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_case_list" "ComputeHOL.compute_let"
|
| 46540 | 15 |
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" |
16 |
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair" |
|
| 46544 | 17 |
"SparseMatrix.sorted_sp_simps" |
18 |
"ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*) |
|
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
19 |
|
| 46540 | 20 |
val computer = PCompute.make Compute.SML @{theory} compute_thms []
|
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
21 |
|
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
22 |
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
|
23 |
|
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
24 |
fun matrix_simplify th = |
| 46540 | 25 |
let |
26 |
val simp_th = matrix_compute (cprop_of th) |
|
27 |
val th = Thm.strip_shyps (Thm.equal_elim simp_th th) |
|
28 |
fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th |
|
29 |
in |
|
30 |
removeTrue th |
|
31 |
end |
|
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
32 |
|
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
33 |
end |