src/HOL/Tools/int_arith.ML
author haftmann
Sat May 09 09:17:29 2009 +0200 (2009-05-09)
changeset 31082 54a442b2d727
parent 31068 f591144b0f17
child 31100 6a2e67fe4488
permissions -rw-r--r--
interface changes in linarith.ML
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 fast_int_arith_simproc: simproc
haftmann@31068
     9
  val setup: Context.generic -> Context.generic
haftmann@31068
    10
end
haftmann@31068
    11
haftmann@31068
    12
structure Int_Arith : INT_ARITH =
haftmann@30496
    13
struct
haftmann@30496
    14
wenzelm@23164
    15
(* Update parameters of arithmetic prover *)
wenzelm@23164
    16
nipkow@24266
    17
(* reduce contradictory =/</<= to False *)
nipkow@24266
    18
nipkow@24266
    19
(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
nipkow@24266
    20
   and m and n are ground terms over rings (roughly speaking).
nipkow@24266
    21
   That is, m and n consist only of 1s combined with "+", "-" and "*".
nipkow@24266
    22
*)
haftmann@30496
    23
nipkow@24266
    24
val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
haftmann@30496
    25
nipkow@24266
    26
val lhss0 = [@{cpat "0::?'a::ring"}];
haftmann@30496
    27
nipkow@24266
    28
fun proc0 phi ss ct =
nipkow@24266
    29
  let val T = ctyp_of_term ct
nipkow@24266
    30
  in if typ_of T = @{typ int} then NONE else
nipkow@24266
    31
     SOME (instantiate' [SOME T] [] zeroth)
nipkow@24266
    32
  end;
haftmann@30496
    33
nipkow@24266
    34
val zero_to_of_int_zero_simproc =
nipkow@24266
    35
  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
nipkow@24266
    36
  proc = proc0, identifier = []};
nipkow@24266
    37
nipkow@24266
    38
val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
haftmann@30496
    39
nipkow@24266
    40
val lhss1 = [@{cpat "1::?'a::ring_1"}];
haftmann@30496
    41
nipkow@24266
    42
fun proc1 phi ss ct =
nipkow@24266
    43
  let val T = ctyp_of_term ct
nipkow@24266
    44
  in if typ_of T = @{typ int} then NONE else
nipkow@24266
    45
     SOME (instantiate' [SOME T] [] oneth)
nipkow@24266
    46
  end;
haftmann@30496
    47
nipkow@24266
    48
val one_to_of_int_one_simproc =
nipkow@24266
    49
  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
nipkow@24266
    50
  proc = proc1, identifier = []};
nipkow@24266
    51
nipkow@24266
    52
val allowed_consts =
nipkow@24266
    53
  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
nipkow@24266
    54
   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
nipkow@24266
    55
   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
nipkow@24266
    56
   @{const_name "HOL.less_eq"}];
nipkow@24266
    57
nipkow@24266
    58
fun check t = case t of
nipkow@24266
    59
   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
nipkow@24266
    60
                else s mem_string allowed_consts
nipkow@24266
    61
 | a$b => check a andalso check b
nipkow@24266
    62
 | _ => false;
nipkow@24266
    63
nipkow@24266
    64
val conv =
nipkow@24266
    65
  Simplifier.rewrite
nipkow@24266
    66
   (HOL_basic_ss addsimps
nipkow@24266
    67
     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
nipkow@24266
    68
             @{thm of_int_diff},  @{thm of_int_minus}])@
nipkow@24266
    69
      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
nipkow@24266
    70
     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
nipkow@24266
    71
nipkow@24266
    72
fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
haftmann@30496
    73
nipkow@24266
    74
val lhss' =
nipkow@24266
    75
  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
nipkow@24266
    76
   @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
nipkow@24266
    77
   @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
haftmann@30496
    78
nipkow@24266
    79
val zero_one_idom_simproc =
nipkow@24266
    80
  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
nipkow@24266
    81
  proc = sproc, identifier = []}
nipkow@24266
    82
wenzelm@23164
    83
val add_rules =
haftmann@25481
    84
    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
huffman@30802
    85
    @{thms int_arith_rules}
wenzelm@23164
    86
huffman@23365
    87
val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
wenzelm@23164
    88
haftmann@31068
    89
val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
haftmann@31068
    90
  :: Numeral_Simprocs.combine_numerals
haftmann@31068
    91
  :: Numeral_Simprocs.cancel_numerals;
wenzelm@23164
    92
haftmann@30496
    93
val setup =
haftmann@30685
    94
  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
wenzelm@23164
    95
   {add_mono_thms = add_mono_thms,
haftmann@31082
    96
    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
wenzelm@23164
    97
    inj_thms = nat_inj_thms @ inj_thms,
haftmann@25481
    98
    lessD = lessD @ [@{thm zless_imp_add1_zle}],
wenzelm@23164
    99
    neqE = neqE,
wenzelm@23164
   100
    simpset = simpset addsimps add_rules
haftmann@31082
   101
                      addsimprocs numeral_base_simprocs}) #>
haftmann@31082
   102
  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
haftmann@31082
   103
  Lin_Arith.add_discrete_type @{type_name Int.int}
wenzelm@23164
   104
wenzelm@23164
   105
val fast_int_arith_simproc =
wenzelm@28262
   106
  Simplifier.simproc (the_context ())
wenzelm@23164
   107
  "fast_int_arith" 
wenzelm@23164
   108
     ["(m::'a::{ordered_idom,number_ring}) < n",
wenzelm@23164
   109
      "(m::'a::{ordered_idom,number_ring}) <= n",
haftmann@30685
   110
      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
wenzelm@23164
   111
haftmann@30496
   112
end;
haftmann@30496
   113
haftmann@30496
   114
Addsimprocs [Int_Arith.fast_int_arith_simproc];