src/HOL/Tools/int_arith.ML
author haftmann
Mon Nov 04 20:10:06 2013 +0100 (2013-11-04)
changeset 54249 ce00f2fef556
parent 51717 9e7d1c139569
child 59582 0fbed69ff081
permissions -rw-r--r--
streamlined setup of linear arithmetic
haftmann@31068
     1
(* Author: Tobias Nipkow
huffman@30802
     2
wenzelm@23164
     3
Instantiation of the generic linear arithmetic package for int.
wenzelm@23164
     4
*)
wenzelm@23164
     5
haftmann@31068
     6
signature INT_ARITH =
haftmann@31068
     7
sig
haftmann@31068
     8
  val setup: Context.generic -> Context.generic
haftmann@31068
     9
end
haftmann@31068
    10
haftmann@31068
    11
structure Int_Arith : INT_ARITH =
haftmann@30496
    12
struct
haftmann@30496
    13
wenzelm@23164
    14
(* Update parameters of arithmetic prover *)
wenzelm@23164
    15
nipkow@24266
    16
(* reduce contradictory =/</<= to False *)
nipkow@24266
    17
nipkow@24266
    18
(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
nipkow@24266
    19
   and m and n are ground terms over rings (roughly speaking).
nipkow@24266
    20
   That is, m and n consist only of 1s combined with "+", "-" and "*".
nipkow@24266
    21
*)
haftmann@30496
    22
wenzelm@36945
    23
val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
haftmann@30496
    24
nipkow@24266
    25
val lhss0 = [@{cpat "0::?'a::ring"}];
haftmann@30496
    26
wenzelm@51717
    27
fun proc0 phi ctxt ct =
nipkow@24266
    28
  let val T = ctyp_of_term ct
nipkow@24266
    29
  in if typ_of T = @{typ int} then NONE else
nipkow@24266
    30
     SOME (instantiate' [SOME T] [] zeroth)
nipkow@24266
    31
  end;
haftmann@30496
    32
nipkow@24266
    33
val zero_to_of_int_zero_simproc =
nipkow@24266
    34
  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
nipkow@24266
    35
  proc = proc0, identifier = []};
nipkow@24266
    36
wenzelm@36945
    37
val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
haftmann@30496
    38
nipkow@24266
    39
val lhss1 = [@{cpat "1::?'a::ring_1"}];
haftmann@30496
    40
wenzelm@51717
    41
fun proc1 phi ctxt ct =
nipkow@24266
    42
  let val T = ctyp_of_term ct
nipkow@24266
    43
  in if typ_of T = @{typ int} then NONE else
nipkow@24266
    44
     SOME (instantiate' [SOME T] [] oneth)
nipkow@24266
    45
  end;
haftmann@30496
    46
nipkow@24266
    47
val one_to_of_int_one_simproc =
nipkow@24266
    48
  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
nipkow@24266
    49
  proc = proc1, identifier = []};
nipkow@24266
    50
haftmann@35267
    51
fun check (Const (@{const_name Groups.one}, @{typ int})) = false
haftmann@35267
    52
  | check (Const (@{const_name Groups.one}, _)) = true
haftmann@38864
    53
  | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
haftmann@35267
    54
      @{const_name Groups.times}, @{const_name Groups.uminus},
haftmann@35267
    55
      @{const_name Groups.minus}, @{const_name Groups.plus},
haftmann@35267
    56
      @{const_name Groups.zero},
haftmann@35092
    57
      @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
haftmann@31100
    58
  | check (a $ b) = check a andalso check b
haftmann@31100
    59
  | check _ = false;
nipkow@24266
    60
wenzelm@51717
    61
val conv_ss =
wenzelm@51717
    62
  simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
    63
    addsimps
nipkow@24266
    64
     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
nipkow@24266
    65
             @{thm of_int_diff},  @{thm of_int_minus}])@
nipkow@24266
    66
      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
nipkow@24266
    67
     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
nipkow@24266
    68
wenzelm@51717
    69
fun sproc phi ctxt ct =
wenzelm@51717
    70
  if check (term_of ct) then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
wenzelm@51717
    71
  else NONE;
haftmann@30496
    72
nipkow@24266
    73
val lhss' =
nipkow@24266
    74
  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
haftmann@35028
    75
   @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"},
haftmann@35028
    76
   @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}]
haftmann@30496
    77
nipkow@24266
    78
val zero_one_idom_simproc =
nipkow@24266
    79
  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
nipkow@24266
    80
  proc = sproc, identifier = []}
nipkow@24266
    81
boehmes@31510
    82
fun number_of thy T n =
huffman@47108
    83
  if not (Sign.of_sort thy (T, @{sort numeral}))
boehmes@31510
    84
  then raise CTERM ("number_of", [])
wenzelm@38763
    85
  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
boehmes@31510
    86
haftmann@31100
    87
val setup =
haftmann@31100
    88
  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
haftmann@31100
    89
  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
haftmann@54249
    90
  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
haftmann@54249
    91
  #> Lin_Arith.add_simps
haftmann@54249
    92
      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
haftmann@33296
    93
  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
boehmes@31510
    94
  #> Lin_Arith.set_number_of number_of
haftmann@31100
    95
  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
haftmann@31100
    96
  #> Lin_Arith.add_discrete_type @{type_name Int.int}
haftmann@31100
    97
haftmann@31100
    98
end;