author | huffman |
Fri, 27 Jul 2012 17:57:31 +0200 | |
changeset 48559 | 686cc7c47589 |
parent 48372 | 868dc809c8a2 |
child 48560 | e0875d956a6b |
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 |
|
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
11 |
val nateq_cancel_sums: simpset -> cterm -> thm option |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
12 |
val natless_cancel_sums: simpset -> cterm -> thm option |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
13 |
val natle_cancel_sums: simpset -> cterm -> thm option |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
14 |
val natdiff_cancel_sums: simpset -> cterm -> thm option |
26101 | 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; |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
38864
diff
changeset
|
52 |
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
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; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
57 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
58 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
59 |
structure EqCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
60 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
61 |
open CommonCancelSums; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
62 |
val mk_bal = HOLogic.mk_eq; |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38715
diff
changeset
|
63 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT; |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
38864
diff
changeset
|
64 |
val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
65 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
66 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
67 |
structure LessCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
68 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
69 |
open CommonCancelSums; |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
70 |
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
|
71 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT; |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
38864
diff
changeset
|
72 |
val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
73 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
74 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
75 |
structure LeCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
76 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
77 |
open CommonCancelSums; |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset
|
78 |
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
|
79 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT; |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
38864
diff
changeset
|
80 |
val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
81 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
82 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
83 |
structure DiffCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
84 |
(struct |
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
85 |
open CommonCancelSums; |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
86 |
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
|
87 |
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; |
48372
868dc809c8a2
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
huffman
parents:
38864
diff
changeset
|
88 |
val cancel_rule = mk_meta_eq @{thm diff_cancel}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
89 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
90 |
|
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
91 |
fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
92 |
fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
93 |
fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
48372
diff
changeset
|
94 |
fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of |
24076 | 95 |
|
24095 | 96 |
end; |