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