src/HOL/Matrix_LP/matrixlp.ML
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 55413 a8e96847523c
child 59582 0fbed69ff081
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     1 (*  Title:      HOL/Matrix_LP/matrixlp.ML
     2     Author:     Steven Obua
     3 *)
     4 
     5 signature MATRIX_LP =
     6 sig
     7   val matrix_compute : cterm -> thm
     8   val matrix_simplify : thm -> thm
     9 end
    10 
    11 structure MatrixLP : MATRIX_LP =
    12 struct
    13 
    14 val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_case_list" "ComputeHOL.compute_let"
    15   "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
    16   "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    17   "SparseMatrix.sorted_sp_simps"
    18   "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
    19 
    20 val computer = PCompute.make Compute.SML @{theory} compute_thms []
    21 
    22 fun matrix_compute c = hd (PCompute.rewrite computer [c])
    23 
    24 fun matrix_simplify th =
    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
    32 
    33 end