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