39 fun find_first_numeral past (t::terms) = |
39 fun find_first_numeral past (t::terms) = |
40 ((dest_number t, t, rev past @ terms) |
40 ((dest_number t, t, rev past @ terms) |
41 handle TERM _ => find_first_numeral (t::past) terms) |
41 handle TERM _ => find_first_numeral (t::past) terms) |
42 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
42 | find_first_numeral past [] = raise TERM("find_first_numeral", []); |
43 |
43 |
44 val zero = mk_number 0; |
44 val mk_sum = Arith_Data.mk_sum HOLogic.natT; |
45 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
45 |
46 |
46 val long_mk_sum = Arith_Data.long_mk_sum HOLogic.natT; |
47 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
|
48 fun mk_sum [] = zero |
|
49 | mk_sum [t,u] = mk_plus (t, u) |
|
50 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
51 |
|
52 (*this version ALWAYS includes a trailing zero*) |
|
53 fun long_mk_sum [] = HOLogic.zero |
|
54 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
55 |
47 |
56 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; |
48 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; |
57 |
49 |
58 |
50 |
59 (** Other simproc items **) |
51 (** Other simproc items **) |