author | haftmann |
Mon, 11 May 2009 15:18:32 +0200 | |
changeset 31100 | 6a2e67fe4488 |
parent 31082 | 54a442b2d727 |
child 31101 | 26c7bb764a38 |
permissions | -rw-r--r-- |
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31024
diff
changeset
|
1 |
(* Author: Tobias Nipkow |
30802 | 2 |
|
23164 | 3 |
Instantiation of the generic linear arithmetic package for int. |
4 |
*) |
|
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 | 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 | 15 |
(* Update parameters of arithmetic prover *) |
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 |
|
24266
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
24 |
val zeroth = (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 |
|
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
38 |
val oneth = (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 |
|
31100 | 52 |
fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false |
53 |
| check (Const (@{const_name "HOL.one"}, _)) = true |
|
54 |
| check (Const (s, _)) = member (op =) [@{const_name "op ="}, |
|
55 |
@{const_name "HOL.times"}, @{const_name "HOL.uminus"}, |
|
56 |
@{const_name "HOL.minus"}, @{const_name "HOL.plus"}, |
|
57 |
@{const_name "HOL.zero"}, |
|
58 |
@{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s |
|
59 |
| check (a $ b) = check a andalso check b |
|
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)"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
74 |
@{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"}, |
bdb48fd8fbdd
extended linear arith capabilities with code by Amine
nipkow
parents:
24196
diff
changeset
|
75 |
@{cpat "(?x::?'a::ordered_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 | 81 |
val fast_int_arith_simproc = |
31100 | 82 |
Simplifier.simproc @{theory} "fast_int_arith" |
23164 | 83 |
["(m::'a::{ordered_idom,number_ring}) < n", |
84 |
"(m::'a::{ordered_idom,number_ring}) <= n", |
|
30685 | 85 |
"(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc); |
23164 | 86 |
|
31100 | 87 |
val global_setup = Simplifier.map_simpset |
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 |
|
31100 | 90 |
val setup = |
91 |
Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] |
|
92 |
#> Lin_Arith.add_lessD @{thm zless_imp_add1_zle} |
|
93 |
#> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps} |
|
94 |
@ @{thms arith_special} @ @{thms int_arith_rules}) |
|
95 |
#> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc |
|
96 |
:: Numeral_Simprocs.combine_numerals |
|
97 |
:: Numeral_Simprocs.cancel_numerals) |
|
98 |
#> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) |
|
99 |
#> Lin_Arith.add_discrete_type @{type_name Int.int} |
|
100 |
||
101 |
end; |