author | bulwahn |
Fri, 03 Dec 2010 08:40:47 +0100 | |
changeset 40905 | 647142607448 |
parent 38864 | 4abe644fcea5 |
child 48372 | 868dc809c8a2 |
permissions | -rw-r--r-- |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
1 |
(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
2 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
3 |
Basic arithmetic for natural numbers. |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
4 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
6 |
signature NAT_ARITH = |
26101 | 7 |
sig |
8 |
val mk_sum: term list -> term |
|
9 |
val mk_norm_sum: term list -> term |
|
10 |
val dest_sum: term -> term list |
|
11 |
||
12 |
val nat_cancel_sums_add: simproc list |
|
13 |
val nat_cancel_sums: simproc list |
|
14 |
val setup: Context.generic -> Context.generic |
|
15 |
end; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
16 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
17 |
structure Nat_Arith: NAT_ARITH = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
18 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
19 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
20 |
(** abstract syntax of structure nat: 0, Suc, + **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
21 |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
22 |
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
23 |
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; |
26101 | 24 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
25 |
fun mk_sum [] = HOLogic.zero |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
26 |
| mk_sum [t] = t |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
27 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
28 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
29 |
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
30 |
fun mk_norm_sum ts = |
21621 | 31 |
let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
32 |
funpow (length ones) HOLogic.mk_Suc (mk_sum sums) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
33 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
34 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
35 |
fun dest_sum tm = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
36 |
if HOLogic.is_zero tm then [] |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
37 |
else |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
38 |
(case try HOLogic.dest_Suc tm of |
21621 | 39 |
SOME t => HOLogic.Suc_zero :: dest_sum t |
15531 | 40 |
| NONE => |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
41 |
(case try dest_plus tm of |
15531 | 42 |
SOME (t, u) => dest_sum t @ dest_sum u |
43 |
| NONE => [tm])); |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
44 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset
|
45 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
46 |
(** cancel common summands **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
47 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
48 |
structure CommonCancelSums = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
49 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
50 |
val mk_sum = mk_norm_sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
51 |
val dest_sum = dest_sum; |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
52 |
val prove_conv = Arith_Data.prove_conv2; |
35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
34974
diff
changeset
|
53 |
val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right}, |
35064
1bdef0c013d3
hide fact names clashing with fact names from Group.thy
haftmann
parents:
35047
diff
changeset
|
54 |
@{thm Nat.add_0}, @{thm Nat.add_0_right}]; |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
55 |
val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac}; |
18328 | 56 |
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
57 |
fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals} |
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
58 |
in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
59 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
60 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
61 |
structure EqCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
62 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
63 |
open CommonCancelSums; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
64 |
val mk_bal = HOLogic.mk_eq; |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38715
diff
changeset
|
65 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT; |
22838 | 66 |
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
67 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
68 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
69 |
structure LessCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
70 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
71 |
open CommonCancelSums; |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
72 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}; |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
73 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT; |
22838 | 74 |
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
75 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
76 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
77 |
structure LeCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
78 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
79 |
open CommonCancelSums; |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
80 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}; |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
81 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT; |
22838 | 82 |
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
83 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
84 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
85 |
structure DiffCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
86 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
87 |
open CommonCancelSums; |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
88 |
val mk_bal = HOLogic.mk_binop @{const_name Groups.minus}; |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
89 |
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; |
22838 | 90 |
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
91 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
92 |
|
26101 | 93 |
val nat_cancel_sums_add = |
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35267
diff
changeset
|
94 |
[Simplifier.simproc_global @{theory} "nateq_cancel_sums" |
26101 | 95 |
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"] |
96 |
(K EqCancelSums.proc), |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35267
diff
changeset
|
97 |
Simplifier.simproc_global @{theory} "natless_cancel_sums" |
26101 | 98 |
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"] |
99 |
(K LessCancelSums.proc), |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35267
diff
changeset
|
100 |
Simplifier.simproc_global @{theory} "natle_cancel_sums" |
26101 | 101 |
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"] |
102 |
(K LeCancelSums.proc)]; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
103 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
104 |
val nat_cancel_sums = nat_cancel_sums_add @ |
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35267
diff
changeset
|
105 |
[Simplifier.simproc_global @{theory} "natdiff_cancel_sums" |
26101 | 106 |
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"] |
107 |
(K DiffCancelSums.proc)]; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
108 |
|
26101 | 109 |
val setup = |
24095 | 110 |
Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |
24076 | 111 |
|
24095 | 112 |
end; |