equal
deleted
inserted
replaced
110 | poly_of_term vs t = |
110 | poly_of_term vs t = |
111 (SOME [monom_of_term vs (1, replicate (length vs) 0) t] |
111 (SOME [monom_of_term vs (1, replicate (length vs) 0) t] |
112 handle ERROR _ => NONE) |
112 handle ERROR _ => NONE) |
113 |
113 |
114 fun is_poly t = |
114 fun is_poly t = |
115 let val vs = t |> vars |> map free2str |> sort string_ord |
115 let |
|
116 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
|
117 |> filter is_some |> map the |> sort string_ord |
116 in |
118 in |
117 case poly_of_term vs t of SOME _ => true | NONE => false |
119 case poly_of_term vs t of SOME _ => true | NONE => false |
118 end |
120 end |
119 val is_expanded = is_poly |
121 val is_expanded = is_poly |
120 |
122 |
308 in |
310 in |
309 case opt of |
311 case opt of |
310 NONE => NONE |
312 NONE => NONE |
311 | SOME (numerator, denominator) => |
313 | SOME (numerator, denominator) => |
312 let |
314 let |
313 val vs = t |> vars |> map free2str |> sort string_ord |
315 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
|
316 |> filter is_some |> map the |> sort string_ord |
314 val baseT = type_of numerator |
317 val baseT = type_of numerator |
315 val expT = HOLogic.realT |
318 val expT = HOLogic.realT |
316 in |
319 in |
317 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
320 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
318 (SOME a, SOME b) => |
321 (SOME a, SOME b) => |
351 in |
354 in |
352 case opt of |
355 case opt of |
353 NONE => NONE |
356 NONE => NONE |
354 | SOME (numerator, denominator) => |
357 | SOME (numerator, denominator) => |
355 let |
358 let |
356 val vs = t |> vars |> map free2str |> sort string_ord |
359 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
|
360 |> filter is_some |> map the |> sort string_ord |
357 val baseT = type_of numerator |
361 val baseT = type_of numerator |
358 val expT = HOLogic.realT |
362 val expT = HOLogic.realT |
359 in |
363 in |
360 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
364 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
361 (SOME a, SOME b) => |
365 (SOME a, SOME b) => |
403 let val opt = check_frac_sum t |
407 let val opt = check_frac_sum t |
404 in |
408 in |
405 case opt of |
409 case opt of |
406 NONE => NONE |
410 NONE => NONE |
407 | SOME ((n1, d1), (n2, d2)) => |
411 | SOME ((n1, d1), (n2, d2)) => |
408 let val vs = t |> vars |> map free2str |> sort string_ord |
412 let |
|
413 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
|
414 |> filter is_some |> map the |> sort string_ord |
409 in |
415 in |
410 case (poly_of_term vs d1, poly_of_term vs d2) of |
416 case (poly_of_term vs d1, poly_of_term vs d2) of |
411 (SOME a, SOME b) => |
417 (SOME a, SOME b) => |
412 let |
418 let |
413 val ((a', b'), c) = gcd_poly a b |
419 val ((a', b'), c) = gcd_poly a b |
440 fun add_fraction_p_ (thy: theory) t = |
446 fun add_fraction_p_ (thy: theory) t = |
441 case check_frac_sum t of |
447 case check_frac_sum t of |
442 NONE => NONE |
448 NONE => NONE |
443 | SOME ((n1, d1), (n2, d2)) => |
449 | SOME ((n1, d1), (n2, d2)) => |
444 let |
450 let |
445 val vs = t |> vars |> map free2str |> sort string_ord |
451 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
|
452 |> filter is_some |> map the |> sort string_ord |
446 in |
453 in |
447 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of |
454 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of |
448 (SOME _, SOME a, SOME _, SOME b) => |
455 (SOME _, SOME a, SOME _, SOME b) => |
449 let |
456 let |
450 val ((a', b'), c) = gcd_poly a b |
457 val ((a', b'), c) = gcd_poly a b |