816 (revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))" |
816 (revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))" |
817 andalso |
817 andalso |
818 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso |
818 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso |
819 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso |
819 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso |
820 (revsets |> nth 1 |> nth 7 |> Rule.to_string) = |
820 (revsets |> nth 1 |> nth 7 |> Rule.to_string) = |
821 "Thm (\"sym_mult_assoc\",?a * (?b * ?c) = ?a * ?b * ?c)" |
821 "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)" |
822 then () else error "first 7 elements in revset changed" |
822 then () else error "first 7 elements in revset changed" |
823 |
823 |
824 (** find the rule 'r' to apply to term 't' **) |
824 (** find the rule 'r' to apply to term 't' **) |
825 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ |
825 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ |
826 for Isabelle2013, we don't get a working revset, but non-termination: |
826 for Isabelle2013, we don't get a working revset, but non-termination: |
828 val SOME (r as (Thm (str, thm))) = nex revsets t; |
828 val SOME (r as (Thm (str, thm))) = nex revsets t; |
829 : |
829 : |
830 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), |
830 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), |
831 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
831 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
832 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), |
832 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), |
833 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
833 Thm ("sym_mult.assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
834 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), |
834 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), |
835 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
835 Thm ("sym_mult.assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
836 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
836 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
837 : |
837 : |
838 ### Isabelle2002: |
838 ### Isabelle2002: |
839 Thm ("sym_#mult_2_3", "6 = 2 * 3") |
839 Thm ("sym_#mult_2_3", "6 = 2 * 3") |
840 ### Isabelle2009-2 for cancel_ (not cancel_p_): |
840 ### Isabelle2009-2 for cancel_ (not cancel_p_): |
914 |
914 |
915 (* WN.10.10.02: dieser Fall terminiert nicht |
915 (* WN.10.10.02: dieser Fall terminiert nicht |
916 (make_polynomial enth"alt zu viele rules) |
916 (make_polynomial enth"alt zu viele rules) |
917 WN060823 'init_state' requires rewriting on specified location in the term |
917 WN060823 'init_state' requires rewriting on specified location in the term |
918 default_print_depth 99; Rfuns; default_print_depth 3; |
918 default_print_depth 99; Rfuns; default_print_depth 3; |
919 WN060831 cycling "sym_order_mult_rls_" "sym_mult_assoc" |
919 WN060831 cycling "sym_order_mult_rls_" "sym_mult.assoc" |
920 as was with make_polynomial before ?!?*) |
920 as was with make_polynomial before ?!?*) |
921 |
921 |
922 val SOME r = nex revsets t; |
922 val SOME r = nex revsets t; |
923 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))", |
923 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))", |
924 mk_thm thy "9 = 3 ^^^ 2")); |
924 mk_thm thy "9 = 3 ^^^ 2")); |