isabelle: src/HOL/Matrix_LP/matrixlp.ML@ca16b657901f (annotated)

47455 26315a545e26 updated headers; wenzelm parents: 46988 diff changeset	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 5522e28a566e tuned code haftmann parents: 46531 diff changeset	15	"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
5522e28a566e tuned code haftmann parents: 46531 diff changeset	16	"ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
46544 460b0d81d486 brute-force adjustion haftmann parents: 46541 diff changeset	17	"SparseMatrix.sorted_sp_simps"
460b0d81d486 brute-force adjustion haftmann parents: 46541 diff changeset	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 5522e28a566e tuned code haftmann parents: 46531 diff changeset	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 5522e28a566e tuned code haftmann parents: 46531 diff changeset	25	let
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 55413 diff changeset	26	val simp_th = matrix_compute (Thm.cprop_of th)
46540 5522e28a566e tuned code haftmann parents: 46531 diff changeset	27	val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
5522e28a566e tuned code haftmann parents: 46531 diff changeset	28	fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
5522e28a566e tuned code haftmann parents: 46531 diff changeset	29	in
5522e28a566e tuned code haftmann parents: 46531 diff changeset	30	removeTrue th
5522e28a566e tuned code haftmann parents: 46531 diff changeset	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

author	wenzelm
	Wed, 01 Apr 2015 17:58:23 +0200
changeset 59894	ca16b657901f
parent 59582	0fbed69ff081
child 69597	ff784d5a5bfb
permissions	-rw-r--r--