src/HOL/Matrix_LP/matrixlp.ML
author haftmann
Thu Sep 19 18:03:54 2013 +0200 (2013-09-19)
changeset 53737 eab25a77af39
parent 51989 700693cb96f1
child 55413 a8e96847523c
permissions -rw-r--r--
dropped dead code
wenzelm@47455
     1
(*  Title:      HOL/Matrix_LP/matrixlp.ML
wenzelm@20787
     2
    Author:     Steven Obua
wenzelm@20787
     3
*)
wenzelm@20787
     4
wenzelm@20787
     5
signature MATRIX_LP =
wenzelm@20787
     6
sig
wenzelm@20787
     7
  val matrix_compute : cterm -> thm
wenzelm@20787
     8
  val matrix_simplify : thm -> thm
wenzelm@20787
     9
end
wenzelm@20787
    10
wenzelm@20787
    11
structure MatrixLP : MATRIX_LP =
wenzelm@20787
    12
struct
wenzelm@20787
    13
haftmann@46540
    14
val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
haftmann@46540
    15
  "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
haftmann@46540
    16
  "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
haftmann@46544
    17
  "SparseMatrix.sorted_sp_simps"
haftmann@46544
    18
  "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
obua@23665
    19
haftmann@46540
    20
val computer = PCompute.make Compute.SML @{theory} compute_thms []
wenzelm@20787
    21
obua@23665
    22
fun matrix_compute c = hd (PCompute.rewrite computer [c])
wenzelm@20787
    23
wenzelm@20787
    24
fun matrix_simplify th =
haftmann@46540
    25
  let
haftmann@46540
    26
    val simp_th = matrix_compute (cprop_of th)
haftmann@46540
    27
    val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
haftmann@46540
    28
    fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
haftmann@46540
    29
  in
haftmann@46540
    30
    removeTrue th
haftmann@46540
    31
  end
wenzelm@20787
    32
wenzelm@20787
    33
end