348 val opt = check_fraction t; |
348 val opt = check_fraction t; |
349 val SOME (numerator, denominator) = opt |
349 val SOME (numerator, denominator) = opt |
350 val vs = t |> vars |> map free2str |> sort string_ord |
350 val vs = t |> vars |> map free2str |> sort string_ord |
351 val baseT = type_of numerator |
351 val baseT = type_of numerator |
352 val expT = HOLogic.realT; |
352 val expT = HOLogic.realT; |
353 default_print_depth 3; (*999*) |
353 (*default_print_depth 3; 999*) |
354 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator); |
354 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator); |
355 default_print_depth 3; (*999*) |
355 (*default_print_depth 3; 999*) |
356 (* does not terminate instead of returning ?: |
356 (* does not terminate instead of returning ?: |
357 val ((a', b'), c) = gcd_poly a b |
357 val ((a', b'), c) = gcd_poly a b |
358 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly |
358 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly |
359 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly |
359 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly |
360 *) |
360 *) |
411 "~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t); |
411 "~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t); |
412 val SOME ((n1, d1), (n2, d2)) = check_frac_sum t; |
412 val SOME ((n1, d1), (n2, d2)) = check_frac_sum t; |
413 term2str n1; term2str d1; term2str n2; term2str d2; |
413 term2str n1; term2str d1; term2str n2; term2str d2; |
414 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
414 val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *) |
415 |> filter is_some |> map the |> sort string_ord; |
415 |> filter is_some |> map the |> sort string_ord; |
416 default_print_depth 3; (*999*) |
416 (*default_print_depth 3; 999*) |
417 val (SOME _, SOME a, SOME _, SOME b) = |
417 val (SOME _, SOME a, SOME _, SOME b) = |
418 (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2); |
418 (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2); |
419 default_print_depth 3; (*999*) |
419 (*default_print_depth 3; 999*) |
420 (* |
420 (* |
421 val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly |
421 val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly |
422 val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly |
422 val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly |
423 val ((a', b'), c) = gcd_poly a b |
423 val ((a', b'), c) = gcd_poly a b |
424 *) |
424 *) |
1579 |
1579 |
1580 "--- with simpler ruleset"; |
1580 "--- with simpler ruleset"; |
1581 val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p"); |
1581 val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p"); |
1582 val der = make_deriv thy Atools_erls rules ro NONE tt; |
1582 val der = make_deriv thy Atools_erls rules ro NONE tt; |
1583 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1583 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1584 default_print_depth 99; writeln (deriv2str der); default_print_depth 3; |
1584 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*) |
1585 |
1585 |
1586 default_print_depth 99; map (term2str o #1) der; default_print_depth 3; |
1586 (*default_print_depth 99;*) map (term2str o #1) der; (*default_print_depth 3;*) |
1587 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]"; |
1587 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]"; |
1588 default_print_depth 99; map (rule2str o #2) der; default_print_depth 3; |
1588 (*default_print_depth 99;*) map (rule2str o #2) der; (*default_print_depth 3;*) |
1589 default_print_depth 99; map (term2str o #1 o #3) der; default_print_depth 3; |
1589 (*default_print_depth 99;*) map (term2str o #1 o #3) der; (*default_print_depth 3;*) |
1590 |
1590 |
1591 val der = make_deriv thy Atools_erls rules ro NONE |
1591 val der = make_deriv thy Atools_erls rules ro NONE |
1592 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"); |
1592 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"); |
1593 default_print_depth 99; writeln (deriv2str der); default_print_depth 3; |
1593 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*) |
1594 |
1594 |
1595 val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p"); |
1595 val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p"); |
1596 val der = make_deriv thy Atools_erls rules ro NONE |
1596 val der = make_deriv thy Atools_erls rules ro NONE |
1597 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)"); |
1597 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)"); |
1598 default_print_depth 99; writeln (deriv2str der); default_print_depth 3; |
1598 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*) |
1599 default_print_depth 99; map (term2str o #1) der; default_print_depth 3; |
1599 (*default_print_depth 99;*) map (term2str o #1) der; (*default_print_depth 3;*) |
1600 (*WN060829 ...postponed*) |
1600 (*WN060829 ...postponed*) |
1601 |
1601 |
1602 |
1602 |
1603 "-------- fun eval_get_denominator -------------------------------------------"; |
1603 "-------- fun eval_get_denominator -------------------------------------------"; |
1604 "-------- fun eval_get_denominator -------------------------------------------"; |
1604 "-------- fun eval_get_denominator -------------------------------------------"; |