File ‹Tools/int_arith.ML›

(* Author: Tobias Nipkow

A special simproc for the instantiation of the generic linear arithmetic package for int.
*)

signature INT_ARITH =
sig
  val zero_one_idom_simproc: simproc
end

structure Int_Arith : INT_ARITH =
struct

(* Update parameters of arithmetic prover *)

(* reduce contradictory =/</<= to False *)

(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
   and m and n are ground terms over rings (roughly speaking).
   That is, m and n consist only of 1s combined with "+", "-" and "*".
*)

val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});

val zero_to_of_int_zero_simproc =
  Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
   {lhss = [\<^term>‹0::'a::ring›],
    proc = fn _ => fn _ => fn ct =>
      let val T = Thm.ctyp_of_cterm ct in
        if Thm.typ_of T = \<^typ>‹int› then NONE
        else SOME (Thm.instantiate' [SOME T] [] zeroth)
      end};

val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});

val one_to_of_int_one_simproc =
  Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
   {lhss = [\<^term>‹1::'a::ring_1›],
    proc = fn _ => fn _ => fn ct =>
      let val T = Thm.ctyp_of_cterm ct in
        if Thm.typ_of T = \<^typ>‹int› then NONE
        else SOME (Thm.instantiate' [SOME T] [] oneth)
      end};

fun check (Const (\<^const_name>‹Groups.one›, \<^typ>‹int›)) = false
  | check (Const (\<^const_name>‹Groups.one›, _)) = true
  | check (Const (s, _)) = member (op =) [\<^const_name>‹HOL.eq›,
      \<^const_name>‹Groups.times›, \<^const_name>‹Groups.uminus›,
      \<^const_name>‹Groups.minus›, \<^const_name>‹Groups.plus›,
      \<^const_name>‹Groups.zero›,
      \<^const_name>‹Orderings.less›, \<^const_name>‹Orderings.less_eq›] s
  | check (a $ b) = check a andalso check b
  | check _ = false;

val conv_ss =
  \<^context>
  |> put_simpset HOL_basic_ss
  |> fold (Simplifier.add_simp o (fn th => th RS sym))
       @{thms of_int_add of_int_mult
         of_int_diff of_int_minus of_int_less_iff
         of_int_le_iff of_int_eq_iff}
  |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
  |> simpset_of;

val zero_one_idom_simproc =
  Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
   {lhss =
      [\<^term>‹(x::'a::ring_char_0) = y›,
       \<^term>‹(x::'a::linordered_idom) < y›,
       \<^term>‹(x::'a::linordered_idom) ≤ y›],
    proc = fn _ => fn ctxt => fn ct =>
      if check (Thm.term_of ct)
      then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
      else NONE};

end;