192 else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es') |
192 else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es') |
193 else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (isastr_of_int c, baseT), es') |
193 else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (isastr_of_int c, baseT), es') |
194 end |
194 end |
195 |
195 |
196 fun term_of_poly baseT expT vs p = |
196 fun term_of_poly baseT expT vs p = |
197 let val monos = map (term_of_monom baseT expT vs) p |
197 let val monos = map (Thm.term_of_monom baseT expT vs) p |
198 in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end |
198 in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end |
199 *} |
199 *} |
200 |
200 |
201 subsection {* Apply gcd_poly for cancelling and adding fractions as terms *} |
201 subsection {* Apply gcd_poly for cancelling and adding fractions as terms *} |
202 ML {* |
202 ML {* |
243 val b't = term_of_poly baseT expT vs b' |
243 val b't = term_of_poly baseT expT vs b' |
244 val ct = term_of_poly baseT expT vs c |
244 val ct = term_of_poly baseT expT vs c |
245 val t' = |
245 val t' = |
246 HOLogic.mk_binop "Fields.inverse_class.divide" |
246 HOLogic.mk_binop "Fields.inverse_class.divide" |
247 (HOLogic.mk_binop "Groups.times_class.times" |
247 (HOLogic.mk_binop "Groups.times_class.times" |
248 (term_of_poly baseT expT vs a', ct), |
248 (Thm.term_of_poly baseT expT vs a', ct), |
249 HOLogic.mk_binop "Groups.times_class.times" (b't, ct)) |
249 HOLogic.mk_binop "Groups.times_class.times" (b't, ct)) |
250 in SOME (t', mk_asms baseT [b't, ct]) end |
250 in SOME (t', mk_asms baseT [b't, ct]) end |
251 end |
251 end |
252 | _ => NONE : (term * term list) option |
252 | _ => NONE : (term * term list) option |
253 end |
253 end |
288 let |
288 let |
289 val bt' = term_of_poly baseT expT vs b' |
289 val bt' = term_of_poly baseT expT vs b' |
290 val ct = term_of_poly baseT expT vs c |
290 val ct = term_of_poly baseT expT vs c |
291 val t' = |
291 val t' = |
292 HOLogic.mk_binop "Fields.inverse_class.divide" |
292 HOLogic.mk_binop "Fields.inverse_class.divide" |
293 (term_of_poly baseT expT vs a', bt') |
293 (Thm.term_of_poly baseT expT vs a', bt') |
294 val asm = mk_asms baseT [bt'] |
294 val asm = mk_asms baseT [bt'] |
295 in SOME (t', asm) end |
295 in SOME (t', asm) end |
296 end |
296 end |
297 | _ => NONE : (term * term list) option |
297 | _ => NONE : (term * term list) option |
298 end |
298 end |
334 case (poly_of_term vs d1, poly_of_term vs d2) of |
334 case (poly_of_term vs d1, poly_of_term vs d2) of |
335 (SOME a, SOME b) => |
335 (SOME a, SOME b) => |
336 let |
336 let |
337 val ((a', b'), c) = gcd_poly a b |
337 val ((a', b'), c) = gcd_poly a b |
338 val (baseT, expT) = (type_of n1, HOLogic.realT) |
338 val (baseT, expT) = (type_of n1, HOLogic.realT) |
339 val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c] |
339 val [d1', d2', c'] = map (Thm.term_of_poly baseT expT vs) [a', b', c] |
340 (*----- minimum of parentheses & nice result, but breaks tests: ------------- |
340 (*----- minimum of parentheses & nice result, but breaks tests: ------------- |
341 val denom = HOLogic.mk_binop "Groups.times_class.times" |
341 val denom = HOLogic.mk_binop "Groups.times_class.times" |
342 (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*) |
342 (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*) |
343 val denom = |
343 val denom = |
344 if c = [(1, replicate (length vs) 0)] |
344 if c = [(1, replicate (length vs) 0)] |