src/HOL/Tools/int_arith.ML
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 47209 4893907fe872 child 51717 9e7d1c139569 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
```     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 ss ct =
```
```    28   let val T = ctyp_of_term ct
```
```    29   in if 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 ss ct =
```
```    42   let val T = ctyp_of_term ct
```
```    43   in if 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 =
```
```    62   Simplifier.rewrite
```
```    63    (HOL_basic_ss 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 ss ct = if check (term_of ct) then SOME (conv ct) else NONE
```
```    70
```
```    71 val lhss' =
```
```    72   [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
```
```    73    @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"},
```
```    74    @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}]
```
```    75
```
```    76 val zero_one_idom_simproc =
```
```    77   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
```
```    78   proc = sproc, identifier = []}
```
```    79
```
```    80 fun number_of thy T n =
```
```    81   if not (Sign.of_sort thy (T, @{sort numeral}))
```
```    82   then raise CTERM ("number_of", [])
```
```    83   else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
```
```    84
```
```    85 val setup =
```
```    86   Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
```
```    87   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
```
```    88   #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
```
```    89       @ @{thms pred_numeral_simps}
```
```    90       @ @{thms arith_special} @ @{thms int_arith_rules})
```
```    91   #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
```
```    92   #> Lin_Arith.set_number_of number_of
```
```    93   #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
```
```    94   #> Lin_Arith.add_discrete_type @{type_name Int.int}
```
```    95
```
```    96 end;
```