author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 36945  9bec62c10714 
child 38715  6513ea67d95d 
permissions  rwrr 
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 

36945  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  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  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  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)"}, 
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  81 
val fast_int_arith_simproc = 
31100  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  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 

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  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}) 

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  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; 