src/HOL/Tools/int_arith.ML
author haftmann
Thu Jan 28 11:48:49 2010 +0100 (2010-01-28)
changeset 34974 18b41bba42b5
parent 33296 a3924d1069e5
child 35028 108662d50512
permissions -rw-r--r--
new theory Algebras.thy for generic algebraic structures
     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 setup: Context.generic -> Context.generic
     9   val global_setup: theory -> theory
    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 fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
    53   | check (Const (@{const_name Algebras.one}, _)) = true
    54   | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    55       @{const_name Algebras.times}, @{const_name Algebras.uminus},
    56       @{const_name Algebras.minus}, @{const_name Algebras.plus},
    57       @{const_name Algebras.zero},
    58       @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
    59   | check (a $ b) = check a andalso check b
    60   | check _ = false;
    61 
    62 val conv =
    63   Simplifier.rewrite
    64    (HOL_basic_ss addsimps
    65      ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
    66              @{thm of_int_diff},  @{thm of_int_minus}])@
    67       [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
    68      addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
    69 
    70 fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
    71 
    72 val lhss' =
    73   [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
    74    @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
    75    @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
    76 
    77 val zero_one_idom_simproc =
    78   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    79   proc = sproc, identifier = []}
    80 
    81 val fast_int_arith_simproc =
    82   Simplifier.simproc @{theory} "fast_int_arith"
    83      ["(m::'a::{ordered_idom,number_ring}) < n",
    84       "(m::'a::{ordered_idom,number_ring}) <= n",
    85       "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    86 
    87 val global_setup = Simplifier.map_simpset
    88   (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
    89 
    90 
    91 fun number_of thy T n =
    92   if not (Sign.of_sort thy (T, @{sort number}))
    93   then raise CTERM ("number_of", [])
    94   else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
    95 
    96 val setup =
    97   Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    98   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    99   #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
   100       @ @{thms arith_special} @ @{thms int_arith_rules})
   101   #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
   102   #> Lin_Arith.set_number_of number_of
   103   #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
   104   #> Lin_Arith.add_discrete_type @{type_name Int.int}
   105 
   106 end;