author | huffman |
Fri, 27 Jul 2012 17:59:18 +0200 | |
changeset 48560 | e0875d956a6b |
parent 48559 | 686cc7c47589 |
child 48561 | 12aa0cb2b447 |
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 |
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
2 |
Author: Brian Huffman |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
3 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
4 |
Basic arithmetic for natural numbers. |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
6 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
7 |
signature NAT_ARITH = |
26101 | 8 |
sig |
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
9 |
val cancel_diff_conv: conv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
10 |
val cancel_eq_conv: conv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
11 |
val cancel_le_conv: conv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
12 |
val cancel_less_conv: conv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
13 |
(* legacy functions: *) |
26101 | 14 |
val mk_sum: term list -> term |
15 |
val mk_norm_sum: term list -> term |
|
16 |
val dest_sum: term -> term list |
|
17 |
end; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
18 |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29302
diff
changeset
|
19 |
structure Nat_Arith: NAT_ARITH = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
20 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
21 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
22 |
(** abstract syntax of structure nat: 0, Suc, + **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
23 |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
24 |
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
|
25 |
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; |
26101 | 26 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
27 |
fun mk_sum [] = HOLogic.zero |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
28 |
| mk_sum [t] = t |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
29 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
30 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
31 |
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
32 |
fun mk_norm_sum ts = |
21621 | 33 |
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
|
34 |
funpow (length ones) HOLogic.mk_Suc (mk_sum sums) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
35 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
36 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
37 |
fun dest_sum tm = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
38 |
if HOLogic.is_zero tm then [] |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
39 |
else |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
40 |
(case try HOLogic.dest_Suc tm of |
21621 | 41 |
SOME t => HOLogic.Suc_zero :: dest_sum t |
15531 | 42 |
| NONE => |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
43 |
(case try dest_plus tm of |
15531 | 44 |
SOME (t, u) => dest_sum t @ dest_sum u |
45 |
| NONE => [tm])); |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
46 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
47 |
val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)" |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
48 |
by (simp only: add_ac)} |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
49 |
val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)" |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
50 |
by (simp only: add_ac)} |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
51 |
val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a" |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
52 |
by (simp only: add_Suc_right)} |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
53 |
val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0" |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
54 |
by (simp only: add_0_right)} |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
20044
diff
changeset
|
55 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
56 |
val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right} |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
57 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
58 |
fun move_to_front path = Conv.every_conv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
59 |
[Conv.rewr_conv (Library.foldl (op RS) (rule0, path)), |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
60 |
Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)] |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
61 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
62 |
fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) = |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
63 |
add_atoms (add1::path) x #> add_atoms (add2::path) y |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
64 |
| add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) = |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
65 |
add_atoms (suc1::path) x |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
66 |
| add_atoms _ (Const (@{const_name Groups.zero}, _)) = I |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
67 |
| add_atoms path x = cons (x, path) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
68 |
|
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
69 |
fun atoms t = add_atoms [] t [] |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
70 |
|
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
71 |
exception Cancel |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
72 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
73 |
fun find_common ord xs ys = |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
74 |
let |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
75 |
fun find (xs as (x, px)::xs') (ys as (y, py)::ys') = |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
76 |
(case ord (x, y) of |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
77 |
EQUAL => (px, py) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
78 |
| LESS => find xs' ys |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
79 |
| GREATER => find xs ys') |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
80 |
| find _ _ = raise Cancel |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
81 |
fun ord' ((x, _), (y, _)) = ord (x, y) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
82 |
in |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
83 |
find (sort ord' xs) (sort ord' ys) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
84 |
end |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
85 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
86 |
fun cancel_conv rule ct = |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
87 |
let |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
88 |
val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
89 |
val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
90 |
val lconv = move_to_front lpath |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
91 |
val rconv = move_to_front rpath |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
92 |
val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
93 |
val conv = conv1 then_conv Conv.rewr_conv rule |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
94 |
in conv ct handle Cancel => raise CTERM ("no_conversion", []) end |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
95 |
|
48560
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
96 |
val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel}) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
97 |
val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel}) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
98 |
val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left}) |
e0875d956a6b
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman
parents:
48559
diff
changeset
|
99 |
val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left}) |
24076 | 100 |
|
24095 | 101 |
end; |