716 if length (hd revsets) = 11 then () else error "length of revset changed"; |
716 if length (hd revsets) = 11 then () else error "length of revset changed"; |
717 if (revsets |> nth 1 |> nth 1 |> Rule.id) = |
717 if (revsets |> nth 1 |> nth 1 |> Rule.id) = |
718 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id) |
718 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id) |
719 then () else error "first element of revset changed"; |
719 then () else error "first element of revset changed"; |
720 if |
720 if |
721 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso |
721 (revsets |> nth 1 |> nth 1 |> Rule.to_string ctxt) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso |
722 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso |
722 (revsets |> nth 1 |> nth 2 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso |
723 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))" |
723 (revsets |> nth 1 |> nth 3 |> Rule.to_string ctxt) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))" |
724 andalso |
724 andalso |
725 (revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))" |
725 (revsets |> nth 1 |> nth 4 |> Rule.to_string ctxt) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))" |
726 andalso |
726 andalso |
727 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso |
727 (revsets |> nth 1 |> nth 5 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso |
728 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso |
728 (revsets |> nth 1 |> nth 6 |> Rule.to_string ctxt) = "Rls_ (\"sym_order_mult_rls_\")" andalso |
729 (revsets |> nth 1 |> nth 7 |> Rule.to_string) = |
729 (revsets |> nth 1 |> nth 7 |> Rule.to_string ctxt) = |
730 "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)" |
730 "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)" |
731 then () else error "first 7 elements in revset changed" |
731 then () else error "first 7 elements in revset changed" |
732 |
732 |
733 (** find the rule 'r' to apply to term 't' **) |
733 (** find the rule 'r' to apply to term 't' **) |
734 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ |
734 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ |
1579 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1579 if length der = 12 then () else error "WN1130912 rls chancel_p 4"; |
1580 (*default_print_depth 99;*) writeln (Derive.deriv2str ctxt der); (*default_print_depth 3;*) |
1580 (*default_print_depth 99;*) writeln (Derive.deriv2str ctxt der); (*default_print_depth 3;*) |
1581 |
1581 |
1582 (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1) der; (*default_print_depth 3;*) |
1582 (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1) der; (*default_print_depth 3;*) |
1583 "...,(- 1 * b \<up> 2 + a \<up> 2) / (- 2 * (a * b) + a \<up> 2 + (- 1 * b) \<up> 2) ]"; |
1583 "...,(- 1 * b \<up> 2 + a \<up> 2) / (- 2 * (a * b) + a \<up> 2 + (- 1 * b) \<up> 2) ]"; |
1584 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*) |
1584 (*default_print_depth 99;*) map ((Rule.to_string ctxt) o #2) der; (*default_print_depth 3;*) |
1585 (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1 o #3) der; (*default_print_depth 3;*) |
1585 (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1 o #3) der; (*default_print_depth 3;*) |
1586 |
1586 |
1587 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1587 val der = Derive.do_one ctxt Atools_erls rules ro NONE |
1588 (TermC.parse_test @{context} "(1 * a + 1 * b) * (1 * a + - 1 * b)"); |
1588 (TermC.parse_test @{context} "(1 * a + 1 * b) * (1 * a + - 1 * b)"); |
1589 (*default_print_depth 99;*) writeln (Derive.deriv2str ctxt der); (*default_print_depth 3;*) |
1589 (*default_print_depth 99;*) writeln (Derive.deriv2str ctxt der); (*default_print_depth 3;*) |