src/HOL/Tools/int_arith.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36945 9bec62c10714
child 38715 6513ea67d95d
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
     1
(* Author: Tobias Nipkow
30802
f9e9e800d27e simplify theorem references
huffman
parents: 30732
diff changeset
     2
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     3
Instantiation of the generic linear arithmetic package for int.
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     4
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     5
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
     6
signature INT_ARITH =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
     7
sig
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
     8
  val setup: Context.generic -> Context.generic
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
     9
  val global_setup: theory -> theory
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
    10
end
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
    11
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31024
diff changeset
    12
structure Int_Arith : INT_ARITH =
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    13
struct
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    14
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    15
(* Update parameters of arithmetic prover *)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    16
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    17
(* reduce contradictory =/</<= to False *)
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    18
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    19
(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    20
   and m and n are ground terms over rings (roughly speaking).
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    21
   That is, m and n consist only of 1s combined with "+", "-" and "*".
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    22
*)
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    23
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35267
diff changeset
    24
val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    25
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    26
val lhss0 = [@{cpat "0::?'a::ring"}];
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    27
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    28
fun proc0 phi ss ct =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    29
  let val T = ctyp_of_term ct
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    30
  in if typ_of T = @{typ int} then NONE else
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    31
     SOME (instantiate' [SOME T] [] zeroth)
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    32
  end;
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    33
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    34
val zero_to_of_int_zero_simproc =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    35
  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    36
  proc = proc0, identifier = []};
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    37
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35267
diff changeset
    38
val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    39
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    40
val lhss1 = [@{cpat "1::?'a::ring_1"}];
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    41
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    42
fun proc1 phi ss ct =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    43
  let val T = ctyp_of_term ct
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    44
  in if typ_of T = @{typ int} then NONE else
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    45
     SOME (instantiate' [SOME T] [] oneth)
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    46
  end;
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    47
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    48
val one_to_of_int_one_simproc =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    49
  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    50
  proc = proc1, identifier = []};
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    51
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    52
fun check (Const (@{const_name Groups.one}, @{typ int})) = false
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    53
  | check (Const (@{const_name Groups.one}, _)) = true
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    54
  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    55
      @{const_name Groups.times}, @{const_name Groups.uminus},
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    56
      @{const_name Groups.minus}, @{const_name Groups.plus},
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    57
      @{const_name Groups.zero},
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35028
diff changeset
    58
      @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    59
  | check (a $ b) = check a andalso check b
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    60
  | check _ = false;
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    61
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    62
val conv =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    63
  Simplifier.rewrite
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    64
   (HOL_basic_ss addsimps
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    65
     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    66
             @{thm of_int_diff},  @{thm of_int_minus}])@
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    67
      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    68
     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    69
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    70
fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    71
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    72
val lhss' =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    73
  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
    74
   @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"},
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
    75
   @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}]
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    76
24266
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    77
val zero_one_idom_simproc =
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    78
  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    79
  proc = sproc, identifier = []}
bdb48fd8fbdd extended linear arith capabilities with code by Amine
nipkow
parents: 24196
diff changeset
    80
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    81
val fast_int_arith_simproc =
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    82
  Simplifier.simproc @{theory} "fast_int_arith"
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
    83
     ["(m::'a::{linordered_idom,number_ring}) < n",
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
    84
      "(m::'a::{linordered_idom,number_ring}) <= n",
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
    85
      "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    86
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    87
val global_setup = Simplifier.map_simpset
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    88
  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    89
31510
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    90
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    91
fun number_of thy T n =
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    92
  if not (Sign.of_sort thy (T, @{sort number}))
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    93
  then raise CTERM ("number_of", [])
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    94
  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
    95
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    96
val setup =
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    97
  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    98
  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
    99
  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
   100
      @ @{thms arith_special} @ @{thms int_arith_rules})
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 32603
diff changeset
   101
  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
31510
e0f2bb4b0021 fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents: 31101
diff changeset
   102
  #> Lin_Arith.set_number_of number_of
31100
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
   103
  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
   104
  #> Lin_Arith.add_discrete_type @{type_name Int.int}
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
   105
6a2e67fe4488 tuned interface of Lin_Arith
haftmann
parents: 31082
diff changeset
   106
end;