(* Title: HOL/Matrix_LP/matrixlp.ML
Author: Steven Obua
*)
signature MATRIX_LP =
sig
val matrix_compute : cterm -> thm
val matrix_simplify : thm -> thm
end
structure MatrixLP : MATRIX_LP =
struct
val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
"SparseMatrix.sorted_sp_simps"
"ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
val computer = PCompute.make Compute.SML @{theory} compute_thms []
fun matrix_compute c = hd (PCompute.rewrite computer [c])
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)
val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
in
removeTrue th
end
end