169 | (NONE, NONE) => NONE, |
169 | (NONE, NONE) => NONE, |
170 Rat.mult m' (Rat.inv p)) |
170 Rat.mult m' (Rat.inv p)) |
171 end |
171 end |
172 else (SOME atom, m) |
172 else (SOME atom, m) |
173 (* terms that evaluate to numeric constants *) |
173 (* terms that evaluate to numeric constants *) |
174 | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m) |
174 | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m) |
175 | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0) |
175 | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0) |
176 | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m) |
176 | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m) |
177 (*Warning: in rare cases (neg_)numeral encloses a non-numeral, |
177 (*Warning: in rare cases (neg_)numeral encloses a non-numeral, |
178 in which case dest_numeral raises TERM; hence all the handles below. |
178 in which case dest_numeral raises TERM; hence all the handles below. |
179 Same for Suc-terms that turn out not to be numerals - |
179 Same for Suc-terms that turn out not to be numerals - |
198 summands and associated multiplicities, plus a constant 'i' (with implicit |
198 summands and associated multiplicities, plus a constant 'i' (with implicit |
199 multiplicity 1) *) |
199 multiplicity 1) *) |
200 fun poly (Const (@{const_name Groups.plus}, _) $ s $ t, |
200 fun poly (Const (@{const_name Groups.plus}, _) $ s $ t, |
201 m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) |
201 m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) |
202 | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) = |
202 | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) = |
203 if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi)) |
203 if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi)) |
204 | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) = |
204 | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) = |
205 if nT T then add_atom all m pi else poly (t, Rat.neg m, pi) |
205 if nT T then add_atom all m pi else poly (t, ~ m, pi) |
206 | poly (Const (@{const_name Groups.zero}, _), _, pi) = |
206 | poly (Const (@{const_name Groups.zero}, _), _, pi) = |
207 pi |
207 pi |
208 | poly (Const (@{const_name Groups.one}, _), m, (p, i)) = |
208 | poly (Const (@{const_name Groups.one}, _), m, (p, i)) = |
209 (p, Rat.add i m) |
209 (p, Rat.add i m) |
210 | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) = |
210 | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) = |