23 end; |
23 end; |
24 |
24 |
25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = |
25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = |
26 struct |
26 struct |
27 |
27 |
28 (*Maps n to #n for n = 0, 1, 2*) |
28 (*Maps n to #n for n = 1, 2*) |
29 val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; |
29 val numeral_syms = [@{thm numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; |
30 val numeral_sym_ss = HOL_basic_ss addsimps numeral_syms; |
30 val numeral_sym_ss = HOL_basic_ss addsimps numeral_syms; |
31 |
31 |
32 val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory}; |
32 val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory}; |
33 |
33 |
34 (*Utilities*) |
34 (*Utilities*) |
35 |
35 |
36 fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; |
36 fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const |
|
37 | mk_number n = HOLogic.mk_number HOLogic.natT n; |
37 fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); |
38 fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); |
38 |
39 |
39 fun find_first_numeral past (t::terms) = |
40 fun find_first_numeral past (t::terms) = |
40 ((dest_number t, t, rev past @ terms) |
41 ((dest_number t, t, rev past @ terms) |
41 handle TERM _ => find_first_numeral (t::past) terms) |
42 handle TERM _ => find_first_numeral (t::past) terms) |
57 |
58 |
58 |
59 |
59 (** Other simproc items **) |
60 (** Other simproc items **) |
60 |
61 |
61 val bin_simps = |
62 val bin_simps = |
62 [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, |
63 [@{thm numeral_1_eq_1} RS sym, |
63 @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, |
64 @{thm numeral_plus_numeral}, @{thm add_numeral_left}, |
64 @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, |
65 @{thm diff_nat_numeral}, @{thm diff_0_eq_0}, @{thm diff_0}, |
65 @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, |
66 @{thm numeral_times_numeral}, @{thm mult_numeral_left(1)}, |
66 @{thm less_nat_number_of}, |
|
67 @{thm if_True}, @{thm if_False}, @{thm not_False_eq_True}, |
67 @{thm if_True}, @{thm if_False}, @{thm not_False_eq_True}, |
68 @{thm Let_number_of}, @{thm nat_number_of}] @ |
68 @{thm nat_0}, @{thm nat_numeral}, @{thm nat_neg_numeral}] @ |
69 @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; |
69 @{thms arith_simps} @ @{thms rel_simps}; |
70 |
70 |
71 |
71 |
72 (*** CancelNumerals simprocs ***) |
72 (*** CancelNumerals simprocs ***) |
73 |
73 |
74 val one = mk_number 1; |
74 val one = mk_number 1; |
113 let val (t1,t2) = dest_plus t |
113 let val (t1,t2) = dest_plus t |
114 in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end |
114 in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end |
115 handle TERM _ => (k, t::ts); |
115 handle TERM _ => (k, t::ts); |
116 |
116 |
117 (*Code for testing whether numerals are already used in the goal*) |
117 (*Code for testing whether numerals are already used in the goal*) |
118 fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true |
118 fun is_numeral (Const(@{const_name Num.numeral}, _) $ w) = true |
119 | is_numeral _ = false; |
119 | is_numeral _ = false; |
120 |
120 |
121 fun prod_has_numeral t = exists is_numeral (dest_prod t); |
121 fun prod_has_numeral t = exists is_numeral (dest_prod t); |
122 |
122 |
123 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false, |
123 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false, |
145 val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, |
145 val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, |
146 @{thm Suc_not_Zero}, @{thm le_0_eq}]; |
146 @{thm Suc_not_Zero}, @{thm le_0_eq}]; |
147 |
147 |
148 val simplify_meta_eq = |
148 val simplify_meta_eq = |
149 Arith_Data.simplify_meta_eq |
149 Arith_Data.simplify_meta_eq |
150 ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right}, |
150 ([@{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right}, |
151 @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); |
151 @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); |
152 |
152 |
153 |
153 |
154 (*** Applying CancelNumeralsFun ***) |
154 (*** Applying CancelNumeralsFun ***) |
155 |
155 |