13 end; |
13 end; |
14 |
14 |
15 structure Nat_Arith: NAT_ARITH = |
15 structure Nat_Arith: NAT_ARITH = |
16 struct |
16 struct |
17 |
17 |
18 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)" |
|
19 by (simp only: ac_simps)} |
|
20 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)" |
|
21 by (simp only: ac_simps)} |
|
22 val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a" |
|
23 by (simp only: add_Suc_right)} |
|
24 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0" |
|
25 by (simp only: add_0_right)} |
|
26 |
|
27 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right} |
18 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right} |
28 |
19 |
29 fun move_to_front ctxt path = Conv.every_conv |
20 fun move_to_front ctxt path = Conv.every_conv |
30 [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)), |
21 [Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)), |
31 Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)] |
22 Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)] |
32 |
23 |
33 fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) = |
24 fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) = |
34 add_atoms (add1::path) x #> add_atoms (add2::path) y |
25 add_atoms (@{thm nat_arith.add1}::path) x #> |
|
26 add_atoms (@{thm nat_arith.add2}::path) y |
35 | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) = |
27 | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) = |
36 add_atoms (suc1::path) x |
28 add_atoms (@{thm nat_arith.suc1}::path) x |
37 | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I |
29 | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I |
38 | add_atoms path x = cons (x, path) |
30 | add_atoms path x = cons (x, path) |
39 |
31 |
40 fun atoms t = add_atoms [] t [] |
32 fun atoms t = add_atoms [] t [] |
41 |
33 |