4 Basic arithmetic for natural numbers. |
4 Basic arithmetic for natural numbers. |
5 *) |
5 *) |
6 |
6 |
7 signature NAT_ARITH = |
7 signature NAT_ARITH = |
8 sig |
8 sig |
9 val cancel_diff_conv: conv |
9 val cancel_diff_conv: Proof.context -> conv |
10 val cancel_eq_conv: conv |
10 val cancel_eq_conv: Proof.context -> conv |
11 val cancel_le_conv: conv |
11 val cancel_le_conv: Proof.context -> conv |
12 val cancel_less_conv: conv |
12 val cancel_less_conv: Proof.context -> conv |
13 end; |
13 end; |
14 |
14 |
15 structure Nat_Arith: NAT_ARITH = |
15 structure Nat_Arith: NAT_ARITH = |
16 struct |
16 struct |
17 |
17 |
24 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0" |
24 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0" |
25 by (simp only: add_0_right)} |
25 by (simp only: add_0_right)} |
26 |
26 |
27 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right} |
27 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right} |
28 |
28 |
29 fun move_to_front path = Conv.every_conv |
29 fun move_to_front ctxt path = Conv.every_conv |
30 [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)), |
30 [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)), |
31 Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)] |
31 Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)] |
32 |
32 |
33 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) = |
33 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) = |
34 add_atoms (add1::path) x #> add_atoms (add2::path) y |
34 add_atoms (add1::path) x #> add_atoms (add2::path) y |
35 | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) = |
35 | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) = |
36 add_atoms (suc1::path) x |
36 add_atoms (suc1::path) x |
52 fun ord' ((x, _), (y, _)) = ord (x, y) |
52 fun ord' ((x, _), (y, _)) = ord (x, y) |
53 in |
53 in |
54 find (sort ord' xs) (sort ord' ys) |
54 find (sort ord' xs) (sort ord' ys) |
55 end |
55 end |
56 |
56 |
57 fun cancel_conv rule ct = |
57 fun cancel_conv rule ctxt ct = |
58 let |
58 let |
59 val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct) |
59 val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct) |
60 val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs) |
60 val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs) |
61 val lconv = move_to_front lpath |
61 val lconv = move_to_front ctxt lpath |
62 val rconv = move_to_front rpath |
62 val rconv = move_to_front ctxt rpath |
63 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
63 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
64 val conv = conv1 then_conv Conv.rewr_conv rule |
64 val conv = conv1 then_conv Conv.rewr_conv rule |
65 in conv ct end |
65 in conv ct end |
66 handle Cancel => raise CTERM ("no_conversion", []) |
66 handle Cancel => raise CTERM ("no_conversion", []) |
67 |
67 |