equal
deleted
inserted
replaced
9 structure Nat_Numeral_Simprocs = |
9 structure Nat_Numeral_Simprocs = |
10 struct |
10 struct |
11 |
11 |
12 (*Maps n to #n for n = 0, 1, 2*) |
12 (*Maps n to #n for n = 0, 1, 2*) |
13 val numeral_syms = |
13 val numeral_syms = |
14 [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym]; |
14 [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym]; |
15 val numeral_sym_ss = HOL_ss addsimps numeral_syms; |
15 val numeral_sym_ss = HOL_ss addsimps numeral_syms; |
16 |
16 |
17 fun rename_numerals th = |
17 fun rename_numerals th = |
18 simplify numeral_sym_ss (Thm.transfer (the_context ()) th); |
18 simplify numeral_sym_ss (Thm.transfer (the_context ()) th); |
19 |
19 |
63 |
63 |
64 (** Other simproc items **) |
64 (** Other simproc items **) |
65 |
65 |
66 val trans_tac = Int_Numeral_Simprocs.trans_tac; |
66 val trans_tac = Int_Numeral_Simprocs.trans_tac; |
67 |
67 |
68 val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym, |
68 val bin_simps = [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, |
69 add_nat_number_of, nat_number_of_add_left, |
69 add_nat_number_of, nat_number_of_add_left, |
70 diff_nat_number_of, le_number_of_eq_not_less, |
70 diff_nat_number_of, le_number_of_eq_not_less, |
71 less_nat_number_of, mult_nat_number_of, |
71 less_nat_number_of, mult_nat_number_of, |
72 thm "Let_number_of", nat_number_of] @ |
72 thm "Let_number_of", nat_number_of] @ |
73 bin_arith_simps @ bin_rel_simps; |
73 bin_arith_simps @ bin_rel_simps; |
124 val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero, |
124 val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero, |
125 le_0_eq]; |
125 le_0_eq]; |
126 |
126 |
127 val simplify_meta_eq = |
127 val simplify_meta_eq = |
128 Int_Numeral_Simprocs.simplify_meta_eq |
128 Int_Numeral_Simprocs.simplify_meta_eq |
129 ([numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right, |
129 ([nat_numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right, |
130 mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules); |
130 mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules); |
131 |
131 |
132 |
132 |
133 (** Restricted version of dest_Sucs_sum for nat_combine_numerals: |
133 (** Restricted version of dest_Sucs_sum for nat_combine_numerals: |
134 Simprocs never apply unless the original expression contains at least one |
134 Simprocs never apply unless the original expression contains at least one |
151 |
151 |
152 (*** Applying CancelNumeralsFun ***) |
152 (*** Applying CancelNumeralsFun ***) |
153 |
153 |
154 structure CancelNumeralsCommon = |
154 structure CancelNumeralsCommon = |
155 struct |
155 struct |
156 val mk_sum = mk_sum |
156 val mk_sum = (fn T:typ => mk_sum) |
157 val dest_sum = dest_Sucs_sum |
157 val dest_sum = dest_Sucs_sum |
158 val mk_coeff = mk_coeff |
158 val mk_coeff = mk_coeff |
159 val dest_coeff = dest_coeff |
159 val dest_coeff = dest_coeff |
160 val find_first_coeff = find_first_coeff [] |
160 val find_first_coeff = find_first_coeff [] |
161 val trans_tac = trans_tac |
161 val trans_tac = trans_tac |
234 (*** Applying CombineNumeralsFun ***) |
234 (*** Applying CombineNumeralsFun ***) |
235 |
235 |
236 structure CombineNumeralsData = |
236 structure CombineNumeralsData = |
237 struct |
237 struct |
238 val add = op + : int*int -> int |
238 val add = op + : int*int -> int |
239 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
239 val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) |
240 val dest_sum = restricted_dest_Sucs_sum |
240 val dest_sum = restricted_dest_Sucs_sum |
241 val mk_coeff = mk_coeff |
241 val mk_coeff = mk_coeff |
242 val dest_coeff = dest_coeff |
242 val dest_coeff = dest_coeff |
243 val left_distrib = left_add_mult_distrib RS trans |
243 val left_distrib = left_add_mult_distrib RS trans |
244 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
244 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
344 Int_Numeral_Simprocs.simplify_meta_eq [zmult_1, zmult_1_right] |
344 Int_Numeral_Simprocs.simplify_meta_eq [zmult_1, zmult_1_right] |
345 (([th, cancel_th]) MRS trans); |
345 (([th, cancel_th]) MRS trans); |
346 |
346 |
347 structure CancelFactorCommon = |
347 structure CancelFactorCommon = |
348 struct |
348 struct |
349 val mk_sum = long_mk_prod |
349 val mk_sum = (fn T:typ => long_mk_prod) |
350 val dest_sum = dest_prod |
350 val dest_sum = dest_prod |
351 val mk_coeff = mk_coeff |
351 val mk_coeff = mk_coeff |
352 val dest_coeff = dest_coeff |
352 val dest_coeff = dest_coeff |
353 val find_first = find_first [] |
353 val find_first = find_first [] |
354 val trans_tac = trans_tac |
354 val trans_tac = trans_tac |
512 Suc_eq_number_of,eq_number_of_Suc, |
512 Suc_eq_number_of,eq_number_of_Suc, |
513 mult_Suc, mult_Suc_right, |
513 mult_Suc, mult_Suc_right, |
514 eq_number_of_0, eq_0_number_of, less_0_number_of, |
514 eq_number_of_0, eq_0_number_of, less_0_number_of, |
515 nat_number_of, if_True, if_False]; |
515 nat_number_of, if_True, if_False]; |
516 |
516 |
517 val simprocs = [Nat_Times_Assoc.conv, |
517 val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@ |
518 Nat_Numeral_Simprocs.combine_numerals]@ |
|
519 Nat_Numeral_Simprocs.cancel_numerals; |
518 Nat_Numeral_Simprocs.cancel_numerals; |
520 |
519 |
521 in |
520 in |
522 |
521 |
523 val nat_simprocs_setup = |
522 val nat_simprocs_setup = |