73 |
73 |
74 (* some specialized syntactic operations *) |
74 (* some specialized syntactic operations *) |
75 |
75 |
76 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
76 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
77 |
77 |
78 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; |
78 val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus}; |
79 |
79 |
80 fun mk_minus t = |
80 fun mk_minus t = |
81 let val T = Term.fastype_of t |
81 let val T = Term.fastype_of t |
82 in Const (@{const_name HOL.uminus}, T --> T) $ t end; |
82 in Const (@{const_name Algebras.uminus}, T --> T) $ t end; |
83 |
83 |
84 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
84 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) |
85 fun mk_sum T [] = mk_number T 0 |
85 fun mk_sum T [] = mk_number T 0 |
86 | mk_sum T [t,u] = mk_plus (t, u) |
86 | mk_sum T [t,u] = mk_plus (t, u) |
87 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
87 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
89 (*this version ALWAYS includes a trailing zero*) |
89 (*this version ALWAYS includes a trailing zero*) |
90 fun long_mk_sum T [] = mk_number T 0 |
90 fun long_mk_sum T [] = mk_number T 0 |
91 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
91 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); |
92 |
92 |
93 (*decompose additions AND subtractions as a sum*) |
93 (*decompose additions AND subtractions as a sum*) |
94 fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = |
94 fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) = |
95 dest_summing (pos, t, dest_summing (pos, u, ts)) |
95 dest_summing (pos, t, dest_summing (pos, u, ts)) |
96 | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = |
96 | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) = |
97 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
97 dest_summing (pos, t, dest_summing (not pos, u, ts)) |
98 | dest_summing (pos, t, ts) = |
98 | dest_summing (pos, t, ts) = |
99 if pos then t::ts else mk_minus t :: ts; |
99 if pos then t::ts else mk_minus t :: ts; |
100 |
100 |
101 fun dest_sum t = dest_summing (true, t, []); |
101 fun dest_sum t = dest_summing (true, t, []); |