1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Sat Jul 17 14:05:28 2021 +0200
1.3 @@ -32,8 +32,8 @@
1.4 "-------- examples common denominator and multiplication from: Schalk --------";
1.5 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1.6 "-------- me Schalk I No.186 -------------------------------------------------";
1.7 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.8 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.9 +"-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.10 +"-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.11 "-------- investigate rulesets for cancel_p ----------------------------------";
1.12 "-------- fun eval_get_denominator -------------------------------------------";
1.13 "-------- several errpats in complicated term --------------------------------";
1.14 @@ -45,7 +45,7 @@
1.15 "-------- integration lev.1 fun factout_p_ -----------------------------------";
1.16 "-------- integration lev.1 fun factout_p_ -----------------------------------";
1.17 "-------- integration lev.1 fun factout_p_ -----------------------------------";
1.18 -val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"
1.19 +val t = TermC.str2term "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)"
1.20 val SOME (t', asm) = factout_p_ thy t;
1.21 if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))"
1.22 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t')
1.23 @@ -65,7 +65,7 @@
1.24 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
1.25 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
1.26 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
1.27 -val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"
1.28 +val t = TermC.str2term "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)"
1.29 val SOME (t', asm) = cancel_p_ thy t;
1.30 if (UnparseC.term t', UnparseC.terms asm) = ("(x + y) / x", "[\"x \<noteq> 0\"]")
1.31 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ UnparseC.term t')
1.32 @@ -96,7 +96,7 @@
1.33 then () else error "common_nominator_p_ asm 1 changed"
1.34
1.35 "-------- example in mail Nipkow";
1.36 -val t = TermC.str2term "x/(x \<up> 2 + -1*y \<up> 2) + y/(x \<up> 2 + -1*x*y)";
1.37 +val t = TermC.str2term "x/(x \<up> 2 + - 1*y \<up> 2) + y/(x \<up> 2 + - 1*x*y)";
1.38 val SOME (t', asm) = common_nominator_p_ thy t;
1.39 if UnparseC.term t' =
1.40 "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))"
1.41 @@ -109,7 +109,7 @@
1.42 val t = TermC.str2term "nothing / to_add";
1.43 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";
1.44 ;
1.45 -val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.46 +val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))";
1.47 val SOME (t', asm) = common_nominator_p_ thy t;
1.48 if UnparseC.term t' =
1.49 "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))"
1.50 @@ -119,7 +119,7 @@
1.51 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
1.52 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
1.53 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
1.54 -val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.55 +val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))";
1.56 val SOME (t', asm) = add_fraction_p_ thy t;
1.57 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)"
1.58 then () else error "add_fraction_p_ 3 changed";
1.59 @@ -130,7 +130,7 @@
1.60 val t = TermC.str2term "nothing / to_add";
1.61 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed";
1.62 ;
1.63 -val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.64 +val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))";
1.65 val SOME (t', asm) = add_fraction_p_ thy t;
1.66 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso
1.67 UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"
1.68 @@ -143,7 +143,7 @@
1.69 (which does not to work, because substitution is not done -- compare rew_sub!);
1.70 keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p
1.71 (again) get prepat = [] changed to <>[]. *)
1.72 -val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)";
1.73 +val t = TermC.str2term "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)";
1.74
1.75 (*rewrite_set_ @{theory Isac_Knowledge} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.76 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);
1.77 @@ -280,12 +280,12 @@
1.78 (* trace stops with ...: (and then jEdit hangs)..
1.79 rewrite_set_ thy false norm_Rational t;
1.80 :
1.81 -### rls: cancel_p on: (-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /
1.82 -(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)
1.83 +### rls: cancel_p on: (- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /
1.84 +(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)
1.85 *)
1.86 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
1.87 - ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1.88 - "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
1.89 + ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
1.90 + "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
1.91 (*cancel_p_ thy t;
1.92 exception Div raised*)
1.93
1.94 @@ -308,9 +308,9 @@
1.95 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.96 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.97 val thy = @{theory Isac_Knowledge};
1.98 -"----- SK060904-2a non-termination of add_fraction_p_";
1.99 -val t = TermC.str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1.100 - " (-1 * a + b * x) / (a + b * x) ");
1.101 +"----- SK060904- 2a non-termination of add_fraction_p_";
1.102 +val t = TermC.str2term (" (a + b * x) / (a + - 1 * (b * x)) + " ^
1.103 + " (- 1 * a + b * x) / (a + b * x) ");
1.104 (* rewrite_set_ thy false norm_Rational t
1.105 exception Div raised*)
1.106 (* rewrite_set_ thy false add_fractions_p t;
1.107 @@ -374,7 +374,7 @@
1.108 val ctxt = Proof_Context.init_global thy;
1.109
1.110 (*---------- (1) with Free A, B ----------------------------------------------------------------*)
1.111 -val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
1.112 +val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
1.113 (* required for applying thms in rewriting \<up> ^*)
1.114 (* we get details from here..*)
1.115
1.116 @@ -382,24 +382,24 @@
1.117 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
1.118 Rewrite.trace_on := false;
1.119 (* Rewrite.trace_on:
1.120 -add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.121 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.122 (* |||||||||||||||||||||||||||||||||||| *)
1.123
1.124 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
1.125 - "A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
1.126 + "A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
1.127 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.128 val NONE = (*case*) check_frac_sum t (*of*)
1.129
1.130 (* Rewrite.trace_on:
1.131 -add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.132 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.133 (* |||||||||||||||||||||||||||| *)
1.134 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
1.135 - "A / 4 + (B / 2 + -1 * B / (2::real))";
1.136 + "A / 4 + (B / 2 + - 1 * B / (2::real))";
1.137 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.138 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
1.139 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("A" , "4") andalso
1.140 (*+*) (UnparseC.term n2, UnparseC.term d2) = ("B / 2 + - 1 * B / 2", "1")
1.141 -(*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + -1 * B / (2::real))) changed";
1.142 +(*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + - 1 * B / (2::real))) changed";
1.143
1.144 val vs = TermC.vars_of t;
1.145 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
1.146 @@ -417,7 +417,7 @@
1.147 | _ => error "monom_of_term Free changed 2";
1.148
1.149 (*---------- (2) with Const AA, BB --------------------------------------------------------------*)
1.150 -val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
1.151 +val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
1.152 (*AA :: real*)
1.153 (* we get details from here..*)
1.154
1.155 @@ -425,23 +425,23 @@
1.156 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
1.157 Rewrite.trace_on := false;
1.158 (* Rewrite.trace_on:
1.159 -add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.160 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.161 (* |||||||||||||||||||||||||||||||||||| *)
1.162 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
1.163 - "AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
1.164 + "AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
1.165 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.166 val NONE = (*case*) check_frac_sum t (*of*)
1.167
1.168 (* Rewrite.trace_on:
1.169 -add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.170 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
1.171 (* |||||||||||||||||||||||||||| *)
1.172 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
1.173 - "AA / 4 + (BB / 2 + -1 * BB / 2)";
1.174 + "AA / 4 + (BB / 2 + - 1 * BB / 2)";
1.175 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
1.176 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
1.177 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("AA" , "4") andalso
1.178 (*+*) (UnparseC.term n2, UnparseC.term d2) = ("BB / 2 + - 1 * BB / 2", "1")
1.179 -(*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + -1 * BB / 2)) changed";
1.180 +(*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + - 1 * BB / 2)) changed";
1.181
1.182 val vs = TermC.vars_of t;
1.183 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
1.184 @@ -547,25 +547,25 @@
1.185 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
1.186 then () else error "rational.sml cancel Schalk 188a";
1.187
1.188 -val t = TermC.str2term "(8*((-1) + x))/(9*((-1) + x))";
1.189 +val t = TermC.str2term "(8*((- 1) + x))/(9*((- 1) + x))";
1.190 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.191 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
1.192 then () else error "rational.sml cancel Schalk make_polynomial 1";
1.193
1.194 "-------- example 188b";
1.195 -val t = TermC.str2term "(-15 + 5 * x) / (-18 + 6 * x)";
1.196 +val t = TermC.str2term "(- 15 + 5 * x) / (- 18 + 6 * x)";
1.197 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
1.198 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]")
1.199 then () else error "rational.sml cancel Schalk 188b";
1.200
1.201 "-------- example 188c";
1.202 -val t = TermC.str2term "(a + -1 * b) / (b + -1 * a)";
1.203 +val t = TermC.str2term "(a + - 1 * b) / (b + - 1 * a)";
1.204 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
1.205 if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]")
1.206 then () else error "rational.sml cancel Schalk 188c";
1.207
1.208 -is_expanded (TermC.str2term "a + -1 * b") = true;
1.209 -val t = TermC.str2term "((- 1)*(b + (-1) * a))/(1*(b + (- 1) * a))";
1.210 +is_expanded (TermC.str2term "a + - 1 * b") = true;
1.211 +val t = TermC.str2term "((- 1)*(b + (- 1) * a))/(1*(b + (- 1) * a))";
1.212 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.213 if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]")
1.214 then () else error "rational.sml cancel Schalk make_polynomial 2";
1.215 @@ -585,7 +585,7 @@
1.216 then () else error "rational.sml make_polynomial Schalk 190c";
1.217
1.218 "-------- example 191a";
1.219 -val t = TermC.str2term "( x \<up> 2 + -1 * y \<up> 2 ) / ( x + y )";
1.220 +val t = TermC.str2term "( x \<up> 2 + - 1 * y \<up> 2 ) / ( x + y )";
1.221 is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.222 is_expanded (TermC.str2term "x + y") = true;
1.223 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
1.224 @@ -599,10 +599,10 @@
1.225 then () else error "rational.sml make_polynomial Schalk 191b";
1.226
1.227 "-------- example 191c";
1.228 -val t = TermC.str2term "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + -25 )";
1.229 +val t = TermC.str2term "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + - 25 )";
1.230 is_expanded (TermC.str2term "9 * x \<up> 2 + -30 * x + 25") = true;
1.231 is_expanded (TermC.str2term "25 + -30*x + 9*x \<up> 2") = true;
1.232 - is_expanded (TermC.str2term "-25 + 9*x \<up> 2") = true;
1.233 + is_expanded (TermC.str2term "- 25 + 9*x \<up> 2") = true;
1.234
1.235 val t = TermC.str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
1.236 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.237 @@ -615,13 +615,13 @@
1.238 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]")
1.239 then () else error "rational.sml cancel_p Schalk 192b";
1.240
1.241 -val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
1.242 +val t = TermC.str2term "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))";
1.243 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.244 if (UnparseC.term t', UnparseC.terms asm) =
1.245 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
1.246 then () else error "rational.sml make_polynomial Schalk 192b";
1.247
1.248 -val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
1.249 +val t = TermC.str2term "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))";
1.250 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.251 if (UnparseC.term t', UnparseC.terms asm) =
1.252 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
1.253 @@ -640,14 +640,14 @@
1.254 then () else error "rational.sml cancel_p Schalk 193b";
1.255
1.256 "-------- example 193c";
1.257 -val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + -10 * x + 1 )";
1.258 +val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + - 10 * x + 1 )";
1.259 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
1.260 if (UnparseC.term t', UnparseC.terms asm) =
1.261 ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]")
1.262 then () else error "rational.sml cancel_p Schalk 193c";
1.263
1.264 (*WN: improved with new numerals*)
1.265 -val t = TermC.str2term "(-25 + 9*x \<up> 2)/(5 + 3*x)";
1.266 +val t = TermC.str2term "(- 25 + 9*x \<up> 2)/(5 + 3*x)";
1.267 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
1.268 if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]")
1.269 then () else error "rational.sml cancel WN 1";
1.270 @@ -733,7 +733,7 @@
1.271 "-------- reverse rewrite ----------------------------------------------------";
1.272 "-------- reverse rewrite ----------------------------------------------------";
1.273 (** the term for which reverse rewriting is demonstrated **)
1.274 -val t = TermC.str2term "(9 + -1 * x \<up> 2) / (9 + 6 * x + x \<up> 2)";
1.275 +val t = TermC.str2term "(9 + - 1 * x \<up> 2) / (9 + 6 * x + x \<up> 2)";
1.276 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,
1.277 next_rule = nex, normal_form = nor, ...},...} = cancel_p;
1.278
1.279 @@ -755,7 +755,7 @@
1.280 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\",9 = 3 \<up> 2)" andalso
1.281 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
1.282 andalso
1.283 -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"
1.284 +(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = - 1 * (3 * x)\",-3 * x = - 1 * (3 * x))"
1.285 andalso
1.286 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
1.287 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
1.288 @@ -770,17 +770,17 @@
1.289
1.290 val SOME (r as (Thm (str, thm))) = nex revsets t;
1.291 :
1.292 -((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
1.293 - Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "
1.294 -((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
1.295 - Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))", "
1.296 -((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
1.297 - Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))", "
1.298 -((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), []))", "
1.299 +((3 * 3 + - 1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
1.300 + Rls_ ("sym_order_mult_rls_"), ((3 * 3 + - 1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "
1.301 +((3 * 3 + - 1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
1.302 + Thm ("sym_mult.assoc", ""), ((3 * 3 + - 1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))", "
1.303 +((3 * 3 + - 1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
1.304 + Thm ("sym_mult.assoc", ""), ((3 * 3 + - 1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))", "
1.305 +((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), []))", "
1.306 :
1.307 ### Isabelle2002:
1.308 Thm ("sym_#mult_2_3", "6 = 2 * 3")
1.309 -### Isabelle2009-2 for cancel_ (not cancel_p_):
1.310 +### Isabelle2009- 2 for cancel_ (not cancel_p_):
1.311 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
1.312 andalso ThmC.string_of_thm thm =
1.313 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
1.314 @@ -841,7 +841,7 @@
1.315 special cases.*)
1.316
1.317 (*the term for which reverse rewriting is demonstrated*)
1.318 -val t = TermC.str2term "(9 + (-1)*x \<up> 2) / (9 + ((-6)*x + x \<up> 2))";
1.319 +val t = TermC.str2term "(9 + (- 1)*x \<up> 2) / (9 + ((-6)*x + x \<up> 2))";
1.320 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.321 next_rule=nex,normal_form=nor,...},...} = cancel_p;
1.322
1.323 @@ -894,7 +894,7 @@
1.324 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
1.325 else error "rational.sml powers_erls (6*x) \<up> 2";
1.326
1.327 -val t = TermC.str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1.328 +val t = TermC.str2term "- 1 * (- 2 * (5 / 2 * (13 * x / 2)))";
1.329 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1.330 if UnparseC.term t' = "65 * x / 2" then () else error "rational.sml 4";
1.331
1.332 @@ -929,11 +929,11 @@
1.333
1.334 (*WN130910 add_fractions_p exception Div raised + history:
1.335 ### WN.2.6.03 from rlang.sml 56a
1.336 -val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + -1 * b \<up> 2)";
1.337 +val t = TermC.str2term "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)";
1.338 val NONE = rewrite_set_ thy false add_fractions_p t;
1.339
1.340 THE ERROR ALREADY OCCURS IN THIS PART:
1.341 -val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.342 +val t = TermC.str2term "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x)";
1.343 val NONE = add_fraction_p_ thy t;
1.344
1.345 SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised ===
1.346 @@ -964,7 +964,7 @@
1.347 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1.348
1.349 (* e192b Stefan K.*)
1.350 -val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
1.351 +val t = TermC.str2term "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))";
1.352 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.353 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
1.354 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1.355 @@ -988,7 +988,7 @@
1.356 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1.357
1.358 (* e192b Stefan K.*)
1.359 -val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
1.360 +val t = TermC.str2term "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))";
1.361 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.362 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
1.363 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1.364 @@ -1007,12 +1007,12 @@
1.365
1.366 (* extreme example from somewhere *)
1.367 val t = TermC.str2term
1.368 - ("(a \<up> 4 * x + -1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^
1.369 + ("(a \<up> 4 * x + - 1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^
1.370 "6*a \<up> 2 * b \<up> 2 * x + -6*a \<up> 2 * b \<up> 2 * y + 4*a * b \<up> 3 * x + -4*a * b \<up> 3 * y + " ^
1.371 - "b \<up> 4 * x + -1*b \<up> 4 * y) " ^
1.372 - " / (a \<up> 2 * x \<up> 3 + -3*a \<up> 2 * x \<up> 2 * y + 3*a \<up> 2 * x * y \<up> 2 + -1*a \<up> 2 * y \<up> 3 + " ^
1.373 - "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + -2*a * b * y \<up> 3 + " ^
1.374 - "b \<up> 2 * x \<up> 3 + -3*b \<up> 2 * x \<up> 2 * y + 3*b \<up> 2 * x * y \<up> 2 + -1*b \<up> 2 * y \<up> 3)")
1.375 + "b \<up> 4 * x + - 1*b \<up> 4 * y) " ^
1.376 + " / (a \<up> 2 * x \<up> 3 + -3*a \<up> 2 * x \<up> 2 * y + 3*a \<up> 2 * x * y \<up> 2 + - 1*a \<up> 2 * y \<up> 3 + " ^
1.377 + "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + - 2*a * b * y \<up> 3 + " ^
1.378 + "b \<up> 2 * x \<up> 3 + -3*b \<up> 2 * x \<up> 2 * y + 3*b \<up> 2 * x * y \<up> 2 + - 1*b \<up> 2 * y \<up> 3)")
1.379 val SOME (t, _) = rewrite_set_ thy false cancel_p t;
1.380 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1.381 then () else error "with Isabelle2002: NONE -- now SOME changed";
1.382 @@ -1045,11 +1045,11 @@
1.383 "----- NOT TERMINATING ?: worked before 0707xx";
1.384 val t = TermC.str2term "(a \<up> 2 - 1)*(b + 1) / ((b \<up> 2 - 1)*(a+1))";
1.385 (* WN130911 "exception Div raised" by
1.386 - cancel_p_ thy (TermC.str2term ("(-1 + -1 * b + a \<up> 2 + a \<up> 2 * b) /" ^
1.387 - "(-1 + -1 * a + b \<up> 2 + a * b \<up> 2)"))
1.388 + cancel_p_ thy (TermC.str2term ("(- 1 + - 1 * b + a \<up> 2 + a \<up> 2 * b) /" ^
1.389 + "(- 1 + - 1 * a + b \<up> 2 + a * b \<up> 2)"))
1.390
1.391 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.392 -if UnparseC.term t = "(1 + -1 * a) / (1 + -1 * b)" then ()
1.393 +if UnparseC.term t = "(1 + - 1 * a) / (1 + - 1 * b)" then ()
1.394 else error "rational.sml MG tests 3e";
1.395 *)
1.396
1.397 @@ -1093,10 +1093,10 @@
1.398 val t = TermC.str2term
1.399 "1/(a - b) \<up> 2 + 1/(a + b) \<up> 2 - 2/(a \<up> 2 - b \<up> 2) - 4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2";
1.400 (* WN130911 non-termination due to non-termination of
1.401 - cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1.402 + cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1.403
1.404 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.405 -if UnparseC.term t = "4 / (a \<up> 4 + -2 * a \<up> 2 * b \<up> 2 + b \<up> 4)"
1.406 +if UnparseC.term t = "4 / (a \<up> 4 + - 2 * a \<up> 2 * b \<up> 2 + b \<up> 4)"
1.407 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";
1.408 *)
1.409
1.410 @@ -1143,14 +1143,14 @@
1.411 (* raises an exception for unclear reasons:
1.412 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.413 :
1.414 -### rls: cancel_p on: (9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /
1.415 -(9 * a \<up> 2 + -16 * b \<up> 2)
1.416 +### rls: cancel_p on: (9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) /
1.417 +(9 * a \<up> 2 + - 16 * b \<up> 2)
1.418 exception Div raised
1.419
1.420 BUT
1.421 val t = TermC.str2term
1.422 - ("(9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /" ^
1.423 - "(9 * a \<up> 2 + -16 * b \<up> 2)");
1.424 + ("(9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) /" ^
1.425 + "(9 * a \<up> 2 + - 16 * b \<up> 2)");
1.426 NONE = cancel_p_ thy t;
1.427
1.428 if UnparseC.term t = "1 / (4 * c + 3 * e)" then ()
1.429 @@ -1165,7 +1165,7 @@
1.430 then () else error "rational.sml: S.K.8..corrected 060904-6";
1.431
1.432 "----- S.K. corrected non-termination of cancel_p_";
1.433 -val t'' = TermC.str2term ("(9 * a \<up> 2 + -16 * b \<up> 2) /" ^
1.434 +val t'' = TermC.str2term ("(9 * a \<up> 2 + - 16 * b \<up> 2) /" ^
1.435 "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))");
1.436 (* /--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------\
1.437 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1.438 @@ -1177,10 +1177,10 @@
1.439 val t = TermC.str2term "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))";
1.440 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.441 :
1.442 -#### rls: cancel_p on: (a * x \<up> 2 + -2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 +
1.443 - -2 * (b * (x * y)) +
1.444 +#### rls: cancel_p on: (a * x \<up> 2 + - 2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 +
1.445 + - 2 * (b * (x * y)) +
1.446 b * y \<up> 2) /
1.447 -(a \<up> 2 * x \<up> 2 + -1 * (a \<up> 2 * y \<up> 2) + -1 * (b \<up> 2 * x \<up> 2) +
1.448 +(a \<up> 2 * x \<up> 2 + - 1 * (a \<up> 2 * y \<up> 2) + - 1 * (b \<up> 2 * x \<up> 2) +
1.449 b \<up> 2 * y \<up> 2)
1.450 exception Div raised
1.451 *)
1.452 @@ -1212,26 +1212,26 @@
1.453 :
1.454 ### rls: cancel_p on: (-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b +
1.455 a \<up> 4 * b \<up> 2) /
1.456 -(a \<up> 3 * b + -1 * (a * b \<up> 3)) /
1.457 +(a \<up> 3 * b + - 1 * (a * b \<up> 3)) /
1.458 (3 + a)
1.459 BUT THIS IS CORRECTLY RECOGNISED
1.460 val t = TermC.str2term
1.461 ("(-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + a \<up> 4 * b \<up> 2) /" ^
1.462 - "(a \<up> 3 * b + -1 * (a * b \<up> 3)) / (3 + (a::real))");
1.463 + "(a \<up> 3 * b + - 1 * (a * b \<up> 3)) / (3 + (a::real))");
1.464 AS
1.465 NONE = cancel_p_ thy t;
1.466
1.467 -if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()
1.468 +if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then ()
1.469 else error "rational.sml: diff.behav. in norm_Rational 27";
1.470 *)
1.471
1.472 "----- SK12 works since 0707xx";
1.473 val t = TermC.str2term "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2) / ((a \<up> 3*b - a*b \<up> 3) * (a+3))";
1.474 (* WN130911 non-termination due to non-termination of
1.475 - cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1.476 + cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1.477
1.478 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.479 -if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()
1.480 +if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then ()
1.481 else error "rational.sml: diff.behav. in norm_Rational 28";
1.482 *)
1.483
1.484 @@ -1266,7 +1266,7 @@
1.485 (*------- SRAM Schalk I, p.69 Nr. 446b *)
1.486 val t = TermC.str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)";
1.487 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.488 -if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + -20 * y \<up> 2" ..isabisac15 | Isabelle2017..*)
1.489 +if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + - 20 * y \<up> 2" ..isabisac15 | Isabelle2017..*)
1.490 "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1"
1.491 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";
1.492
1.493 @@ -1311,30 +1311,30 @@
1.494 "----- Schalk I, p.69 Nr. 455b";
1.495 val t = TermC.str2term "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))";
1.496 (* WN130911 non-termination due to non-termination of
1.497 - cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1.498 - "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1.499 + cancel_p_ thy (TermC.str2term ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
1.500 + "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1.501
1.502 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.503 -if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()
1.504 +if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then ()
1.505 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
1.506 *)
1.507
1.508 -"----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1.509 +"----- SK060904- 1a non-termination of cancel_p_ ?: worked before 0707xx";
1.510 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";
1.511 (* WN130911 non-termination due to non-termination of
1.512 - cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1.513 - "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1.514 + cancel_p_ thy (TermC.str2term ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
1.515 + "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1.516
1.517 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.518 -if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()
1.519 +if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then ()
1.520 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
1.521 *)
1.522
1.523 "----- ?: worked before 0707xx";
1.524 -val t = TermC.str2term "(3 + -1 * y) / (-9 + y \<up> 2)";
1.525 +val t = TermC.str2term "(3 + - 1 * y) / (-9 + y \<up> 2)";
1.526 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.527 if UnparseC.term t = "- 1 / (3 + y)"
1.528 -then () else error "rational.sml: -1 / (3 + y) norm_Rational";
1.529 +then () else error "rational.sml: - 1 / (3 + y) norm_Rational";
1.530
1.531 "----- SRD Schalk I, p.69 Nr. 456b";
1.532 val t = TermC.str2term "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)";
1.533 @@ -1352,14 +1352,14 @@
1.534 val t = TermC.str2term "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))";
1.535 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.536 :
1.537 -### rls: cancel_p on: (-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /
1.538 -((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))
1.539 +### rls: cancel_p on: (- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) /
1.540 +((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x)))
1.541 exception Div raised
1.542
1.543 BUT
1.544 val t = TermC.str2term
1.545 - ("(-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /" ^
1.546 - "((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))");
1.547 + ("(- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) /" ^
1.548 + "((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x)))");
1.549 NONE = cancel_p_ thy t;
1.550
1.551 if UnparseC.term t = "a \<up> 2 / b \<up> 2" then ()
1.552 @@ -1380,7 +1380,7 @@
1.553 BUT
1.554 val t = TermC.str2term
1.555 ("(144 + -72 * x + 9 * x \<up> 2) / (4 + -8 * y + 4 * y \<up> 2) /" ^
1.556 - "((-12 + 3 * x) / (-16 + 16 * y))");
1.557 + "((- 12 + 3 * x) / (- 16 + 16 * y))");
1.558 NONE = cancel_p_ thy t;
1.559
1.560 if UnparseC.term t = !!!!!!!!!!!!!!!!!!!!!!!!!
1.561 @@ -1422,7 +1422,7 @@
1.562 val t = TermC.str2term "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x)) / (x/9 + y/6 + z/4)";
1.563 (* WN130911 non-termination due to non-termination of
1.564 cancel_p_ thy (TermC.str2term
1.565 - ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + -2916 * z \<up> 2) /" ^
1.566 + ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + - 2916 * z \<up> 2) /" ^
1.567 "(576 * x \<up> 2 + 864 * (x * y) + 1296 * (x * z))"))
1.568
1.569 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.570 @@ -1470,9 +1470,9 @@
1.571 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.572
1.573 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.574 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.575 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.576 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.577 +"-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.578 +"-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.579 +"-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
1.580 reset_states ();
1.581 CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1.582 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.583 @@ -1485,11 +1485,11 @@
1.584 [
1.585 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1.586 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.587 -(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.588 -(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1.589 -(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1.590 -(([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),
1.591 -(([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]
1.592 +(([1], Res), (2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))),
1.593 +(([2], Res), (2 + - 1 * x) / (2 * a) / (2 * a / (- 2 + x))),
1.594 +(([3], Res), (2 + - 1 * x) * (- 2 + x) / (2 * a * (2 * a))),
1.595 +(([4], Res), (-4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)),
1.596 +(([], Res), (-4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2))]
1.597 *)
1.598 interSteps 1 ([1], Res);
1.599 val ((pt, p), _) = get_calc 1;
1.600 @@ -1498,29 +1498,29 @@
1.601 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1.602 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.603 (([1,1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.604 -(([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.605 -(([1,2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.606 -(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.607 -(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1.608 -(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1.609 -(([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),
1.610 -(([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]
1.611 +(([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + - 1 * 2))),
1.612 +(([1,2], Res), (2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))),
1.613 +(([1], Res), (2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))),
1.614 +(([2], Res), (2 + - 1 * x) / (2 * a) / (2 * a / (- 2 + x))),
1.615 +(([3], Res), (2 + - 1 * x) * (- 2 + x) / (2 * a * (2 * a))),
1.616 +(([4], Res), (-4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)),
1.617 +(([], Res), (-4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2))]
1.618 *)
1.619 val (t, asm) = get_obj g_result pt [1, 1];
1.620 -if UnparseC.term t = "(2 - x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"
1.621 -then () else error "2nd interSteps ..Simp_Rat_Double_No-1 changed on [1, 1]";
1.622 +if UnparseC.term t = "(2 - x) / (2 * a) / (2 * a / (x + - 1 * 2))" andalso UnparseC.terms asm = "[]"
1.623 +then () else error "2nd interSteps ..Simp_Rat_Double_No- 1 changed on [1, 1]";
1.624 val (t, asm) = get_obj g_result pt [1, 2];
1.625 -if UnparseC.term t = "(2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"
1.626 -then () else error "3rd interSteps ..Simp_Rat_Double_No-1 changed on [1, 2]";
1.627 +if UnparseC.term t = "(2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))" andalso UnparseC.terms asm = "[]"
1.628 +then () else error "3rd interSteps ..Simp_Rat_Double_No- 1 changed on [1, 2]";
1.629 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1.630
1.631
1.632 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1.633 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.634 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.635 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.636 +"-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.637 +"-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.638 +"-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
1.639 reset_states ();
1.640 -CalcTree [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1.641 +CalcTree [(["Term ((a^2 + - 1*b^2) / (a^2 + - 2*a*b + b^2))", "normalform N"],
1.642 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.643 Iterator 1;
1.644 moveActiveRoot 1;
1.645 @@ -1528,59 +1528,59 @@
1.646 val ((pt, p), _) = get_calc 1;
1.647 (*Test_Tool.show_pt pt;
1.648 [
1.649 -(([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1.650 -(([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1.651 -(([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.652 -(([2], Res), (a + b) / (a + -1 * b)),
1.653 -(([], Res), (a + b) / (a + -1 * b))]
1.654 +(([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
1.655 +(([1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2)),
1.656 +(([1], Res), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.657 +(([2], Res), (a + b) / (a + - 1 * b)),
1.658 +(([], Res), (a + b) / (a + - 1 * b))]
1.659 *)
1.660 interSteps 1 ([2], Res);
1.661 val ((pt, p), _) = get_calc 1;
1.662 (*Test_Tool.show_pt pt;
1.663 [
1.664 -(([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1.665 -(([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1.666 -(([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.667 -(([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.668 -(([2,1], Res), (a + b) / (a + -1 * b)),
1.669 -(([2], Res), (a + b) / (a + -1 * b)),
1.670 -(([], Res), (a + b) / (a + -1 * b))]
1.671 +(([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
1.672 +(([1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2)),
1.673 +(([1], Res), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.674 +(([2,1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.675 +(([2,1], Res), (a + b) / (a + - 1 * b)),
1.676 +(([2], Res), (a + b) / (a + - 1 * b)),
1.677 +(([], Res), (a + b) / (a + - 1 * b))]
1.678 *)
1.679 interSteps 1 ([2,1],Res);
1.680 val ((pt, p), _) = get_calc 1;
1.681 (*Test_Tool.show_pt pt;
1.682 [
1.683 -(([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1.684 -(([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1.685 -(([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.686 -(([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.687 -(([2,1,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1.688 -(([2,1,1], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1.689 -(a \<up> 2 + -2 * (a * b) + 1 * b \<up> 2)),
1.690 -(([2,1,2], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1.691 -(a \<up> 2 + -2 * (a * b) + -1 \<up> 2 * b \<up> 2)),
1.692 -(([2,1,3], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1.693 -(a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1.694 -(([2,1,4], Res), (a * a + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1.695 -(a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1.696 -(([2,1,5], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1.697 -(a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1.698 -(([2,1,6], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1.699 -(a \<up> 2 + -1 * (2 * (a * b)) + (-1 * b) \<up> 2)),
1.700 -(([2,1,7], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1.701 -(a \<up> 2 + 2 * (a * (-1 * b)) + (-1 * b) \<up> 2)),
1.702 -(([2,1,8], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1.703 -(a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1.704 -(([2,1,9], Res), (a * (a + -1 * b) + (b * a + b * (-1 * b))) /
1.705 -(a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1.706 -(([2,1,10], Res), (a * (a + -1 * b) + b * (a + -1 * b)) /
1.707 -(a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1.708 -(([2,1,11], Res), (a + b) * (a + -1 * b) / (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1.709 -(([2,1,12], Res), (a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))),
1.710 -(([2,1,13], Res), (a + b) / (a + -1 * b)),
1.711 -(([2,1], Res), (a + b) / (a + -1 * b)),
1.712 -(([2], Res), (a + b) / (a + -1 * b)),
1.713 -(([], Res), (a + b) / (a + -1 * b))]
1.714 +(([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
1.715 +(([1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2)),
1.716 +(([1], Res), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.717 +(([2,1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.718 +(([2,1,1], Frm), (a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * (a * b) + b \<up> 2)),
1.719 +(([2,1,1], Res), (a \<up> 2 + - 1 * (a * b) + a * b + - 1 * b \<up> 2) /
1.720 +(a \<up> 2 + - 2 * (a * b) + 1 * b \<up> 2)),
1.721 +(([2,1,2], Res), (a \<up> 2 + - 1 * (a * b) + a * b + - 1 * b \<up> 2) /
1.722 +(a \<up> 2 + - 2 * (a * b) + - 1 \<up> 2 * b \<up> 2)),
1.723 +(([2,1,3], Res), (a \<up> 2 + - 1 * (a * b) + a * b + - 1 * b \<up> 2) /
1.724 +(a \<up> 2 + - 2 * (a * b) + (- 1 * b) \<up> 2)),
1.725 +(([2,1,4], Res), (a * a + - 1 * (a * b) + a * b + - 1 * b \<up> 2) /
1.726 +(a \<up> 2 + - 2 * (a * b) + (- 1 * b) \<up> 2)),
1.727 +(([2,1,5], Res), (a * a + - 1 * (a * b) + a * b + - 1 * (b * b)) /
1.728 +(a \<up> 2 + - 2 * (a * b) + (- 1 * b) \<up> 2)),
1.729 +(([2,1,6], Res), (a * a + - 1 * (a * b) + a * b + - 1 * (b * b)) /
1.730 +(a \<up> 2 + - 1 * (2 * (a * b)) + (- 1 * b) \<up> 2)),
1.731 +(([2,1,7], Res), (a * a + a * (- 1 * b) + (b * a + b * (- 1 * b))) /
1.732 +(a \<up> 2 + 2 * (a * (- 1 * b)) + (- 1 * b) \<up> 2)),
1.733 +(([2,1,8], Res), (a * a + a * (- 1 * b) + (b * a + b * (- 1 * b))) /
1.734 +(a \<up> 2 + 2 * a * (- 1 * b) + (- 1 * b) \<up> 2)),
1.735 +(([2,1,9], Res), (a * (a + - 1 * b) + (b * a + b * (- 1 * b))) /
1.736 +(a \<up> 2 + 2 * a * (- 1 * b) + (- 1 * b) \<up> 2)),
1.737 +(([2,1,10], Res), (a * (a + - 1 * b) + b * (a + - 1 * b)) /
1.738 +(a \<up> 2 + 2 * a * (- 1 * b) + (- 1 * b) \<up> 2)),
1.739 +(([2,1,11], Res), (a + b) * (a + - 1 * b) / (a \<up> 2 + 2 * a * (- 1 * b) + (- 1 * b) \<up> 2)),
1.740 +(([2,1,12], Res), (a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))),
1.741 +(([2,1,13], Res), (a + b) / (a + - 1 * b)),
1.742 +(([2,1], Res), (a + b) / (a + - 1 * b)),
1.743 +(([2], Res), (a + b) / (a + - 1 * b)),
1.744 +(([], Res), (a + b) / (a + - 1 * b))]
1.745 *)
1.746 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1.747 if length newnds = 13 then () else error "rational.sml: interSteps cancel_p rev_rew_p";
1.748 @@ -1597,13 +1597,13 @@
1.749 "-------- investigate rulesets for cancel_p ----------------------------------";
1.750 "-------- investigate rulesets for cancel_p ----------------------------------";
1.751 val thy = @{theory "Rational"};
1.752 -val t = TermC.str2term "(a \<up> 2 + -1*b \<up> 2) / (a \<up> 2 + -2*a*b + b \<up> 2)";
1.753 -val tt = TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1.754 +val t = TermC.str2term "(a \<up> 2 + - 1*b \<up> 2) / (a \<up> 2 + - 2*a*b + b \<up> 2)";
1.755 +val tt = TermC.str2term "(1 * a + 1 * b) * (1 * a + - 1 * b)"(*numerator only*);
1.756
1.757 "----- with rewrite_set_";
1.758 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.759 if UnparseC.term tt'= "a \<up> 2 + - 1 * b \<up> 2" then () else error "rls chancel_p 1";
1.760 -val tt = TermC.str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1.761 +val tt = TermC.str2term "((1 * a + - 1 * b) * (1 * a + - 1 * b))"(*denominator only*);
1.762 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.763 if UnparseC.term tt' = "a \<up> 2 + - 2 * a * b + b \<up> 2" then () else error "rls chancel_p 2";
1.764
1.765 @@ -1619,17 +1619,17 @@
1.766 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1.767
1.768 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
1.769 -"...,(-1 * b \<up> 2 + a \<up> 2) / (-2 * (a * b) + a \<up> 2 + (-1 * b) \<up> 2) ]";
1.770 +"...,(- 1 * b \<up> 2 + a \<up> 2) / (- 2 * (a * b) + a \<up> 2 + (- 1 * b) \<up> 2) ]";
1.771 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
1.772 (*default_print_depth 99;*) map (UnparseC.term o #1 o #3) der; (*default_print_depth 3;*)
1.773
1.774 val der = Derive.do_one thy Atools_erls rules ro NONE
1.775 - (TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1.776 + (TermC.str2term "(1 * a + 1 * b) * (1 * a + - 1 * b)");
1.777 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1.778
1.779 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p");
1.780 val der = Derive.do_one thy Atools_erls rules ro NONE
1.781 - (TermC.str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1.782 + (TermC.str2term "(1 * a + - 1 * b) * (1 * a + - 1 * b)");
1.783 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1.784 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
1.785 (*WN060829 ...postponed*)
1.786 @@ -1661,9 +1661,9 @@
1.787 [
1.788 (([], Frm), Simplify ((5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b))),
1.789 (([1], Frm), (5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b)),
1.790 -(([1], Res), (5 * b + 25) / (a \<up> 2 + -1 * b \<up> 2) * (a + -1 * b) / (5 * b)),
1.791 -(([2], Res), (5 * b + 25) * (a + -1 * b) / (a \<up> 2 + -1 * b \<up> 2) / (5 * b)),
1.792 -(([3], Res), (25 * a + -25 * b + 5 * (a * b) + -5 * b \<up> 2) / (a \<up> 2 + -1 * b \<up> 2) /
1.793 +(([1], Res), (5 * b + 25) / (a \<up> 2 + - 1 * b \<up> 2) * (a + - 1 * b) / (5 * b)),
1.794 +(([2], Res), (5 * b + 25) * (a + - 1 * b) / (a \<up> 2 + - 1 * b \<up> 2) / (5 * b)),
1.795 +(([3], Res), (25 * a + - 25 * b + 5 * (a * b) + -5 * b \<up> 2) / (a \<up> 2 + - 1 * b \<up> 2) /
1.796 (5 * b)),
1.797 (([4], Res), (25 + 5 * b) / (a + b) / (5 * b)),
1.798 (([5], Res), (25 + 5 * b) / ((a + b) * (5 * b))),
1.799 @@ -1695,25 +1695,25 @@
1.800 (*val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.801 :
1.802 ### rls: cancel_p on: (a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /
1.803 -(b + -2 * y) /
1.804 -((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /
1.805 +(b + - 2 * y) /
1.806 +((b \<up> 2 + - 1 * y \<up> 2) / (b + 2 * y)) /
1.807 (b \<up> 2 * y + b * y \<up> 2) /
1.808 (a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +
1.809 - -16 * (a * (x * y \<up> 2)) +
1.810 + - 16 * (a * (x * y \<up> 2)) +
1.811 4 * (b \<up> 2 * x \<up> 2) +
1.812 - -16 * (x \<up> 2 * y \<up> 2))
1.813 + - 16 * (x \<up> 2 * y \<up> 2))
1.814 exception Div raised
1.815
1.816 BUT
1.817 val t = TermC.str2term
1.818 ("(a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /" ^
1.819 - "(b + -2 * y) /" ^
1.820 - "((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /" ^
1.821 + "(b + - 2 * y) /" ^
1.822 + "((b \<up> 2 + - 1 * y \<up> 2) / (b + 2 * y)) /" ^
1.823 "(b \<up> 2 * y + b * y \<up> 2) /" ^
1.824 "(a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +" ^
1.825 - "-16 * (a * (x * y \<up> 2)) +" ^
1.826 + "- 16 * (a * (x * y \<up> 2)) +" ^
1.827 "4 * (b \<up> 2 * x \<up> 2) +" ^
1.828 - "-16 * (x \<up> 2 * y \<up> 2))");
1.829 + "- 16 * (x \<up> 2 * y \<up> 2))");
1.830 NONE = cancel_p_ thy t;
1.831 *)
1.832
1.833 @@ -1735,9 +1735,9 @@
1.834 -4 * (a \<up> 4 * b \<up> 6) +
1.835 -4 * (a \<up> 3 * b \<up> 7) +
1.836 -4 * (a \<up> 2 * b \<up> 8) +
1.837 - -2 * (a * b \<up> 9))
1.838 + - 2 * (a * b \<up> 9))
1.839
1.840 -if UnparseC.term t = "1 / (a \<up> 2 + -1 * b \<up> 2)" then ()
1.841 +if UnparseC.term t = "1 / (a \<up> 2 + - 1 * b \<up> 2)" then ()
1.842 else error "rational.sml: diff.behav. in norm_Rational_mg 49";
1.843 *)
1.844
1.845 @@ -1749,14 +1749,14 @@
1.846 :
1.847 #### rls: cancel_p on: (2 * (x \<up> 6 * (y \<up> 2 * z)) + 2 * (x \<up> 6 * (y * z \<up> 2)) +
1.848 2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +
1.849 - -2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +
1.850 - -2 * (x \<up> 4 * (y * z \<up> 4)) +
1.851 - -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4))) /
1.852 -(-2 * (x \<up> 6 * (y \<up> 2 * z)) + -2 * (x \<up> 6 * (y * z \<up> 2)) +
1.853 + - 2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +
1.854 + - 2 * (x \<up> 4 * (y * z \<up> 4)) +
1.855 + - 2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4))) /
1.856 +(- 2 * (x \<up> 6 * (y \<up> 2 * z)) + - 2 * (x \<up> 6 * (y * z \<up> 2)) +
1.857 2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +
1.858 2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +
1.859 2 * (x \<up> 4 * (y * z \<up> 4)) +
1.860 - -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4)))
1.861 + - 2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4)))
1.862 *)
1.863
1.864 "-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate";
1.865 @@ -1766,11 +1766,11 @@
1.866 val t = TermC.str2term "(a-b) \<up> 3 * (x+y) \<up> 4";
1.867 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.868 UnparseC.term t;
1.869 -"a \<up> 3 * x \<up> 4 + 4 * a \<up> 3 * x \<up> 3 * y +6 * a \<up> 3 * x \<up> 2 * y \<up> 2 +4 * a \<up> 3 * x * y \<up> 3 +a \<up> 3 * y \<up> 4 +-3 * a \<up> 2 * b * x \<up> 4 +-12 * a \<up> 2 * b * x \<up> 3 * y +-18 * a \<up> 2 * b * x \<up> 2 * y \<up> 2 +-12 * a \<up> 2 * b * x * y \<up> 3 +-3 * a \<up> 2 * b * y \<up> 4 +3 * a * b \<up> 2 * x \<up> 4 +12 * a * b \<up> 2 * x \<up> 3 * y +18 * a * b \<up> 2 * x \<up> 2 * y \<up> 2 +12 * a * b \<up> 2 * x * y \<up> 3 +3 * a * b \<up> 2 * y \<up> 4 +-1 * b \<up> 3 * x \<up> 4 +-4 * b \<up> 3 * x \<up> 3 * y +-6 * b \<up> 3 * x \<up> 2 * y \<up> 2 +-4 * b \<up> 3 * x * y \<up> 3 +-1 * b \<up> 3 * y \<up> 4";
1.870 +"a \<up> 3 * x \<up> 4 + 4 * a \<up> 3 * x \<up> 3 * y +6 * a \<up> 3 * x \<up> 2 * y \<up> 2 +4 * a \<up> 3 * x * y \<up> 3 +a \<up> 3 * y \<up> 4 +-3 * a \<up> 2 * b * x \<up> 4 +- 12 * a \<up> 2 * b * x \<up> 3 * y +- 18 * a \<up> 2 * b * x \<up> 2 * y \<up> 2 +- 12 * a \<up> 2 * b * x * y \<up> 3 +-3 * a \<up> 2 * b * y \<up> 4 +3 * a * b \<up> 2 * x \<up> 4 +12 * a * b \<up> 2 * x \<up> 3 * y +18 * a * b \<up> 2 * x \<up> 2 * y \<up> 2 +12 * a * b \<up> 2 * x * y \<up> 3 +3 * a * b \<up> 2 * y \<up> 4 +- 1 * b \<up> 3 * x \<up> 4 +-4 * b \<up> 3 * x \<up> 3 * y +-6 * b \<up> 3 * x \<up> 2 * y \<up> 2 +-4 * b \<up> 3 * x * y \<up> 3 +- 1 * b \<up> 3 * y \<up> 4";
1.871 val t = TermC.str2term "((x+y) \<up> 2 * (a-b) \<up> 5)";
1.872 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.873 UnparseC.term t;
1.874 -"a \<up> 5 * x \<up> 2 + 2 * a \<up> 5 * x * y + a \<up> 5 * y \<up> 2 +-5 * a \<up> 4 * b * x \<up> 2 +-10 * a \<up> 4 * b * x * y +-5 * a \<up> 4 * b * y \<up> 2 +10 * a \<up> 3 * b \<up> 2 * x \<up> 2 +20 * a \<up> 3 * b \<up> 2 * x * y +10 * a \<up> 3 * b \<up> 2 * y \<up> 2 +-10 * a \<up> 2 * b \<up> 3 * x \<up> 2 +-20 * a \<up> 2 * b \<up> 3 * x * y +-10 * a \<up> 2 * b \<up> 3 * y \<up> 2 +5 * a * b \<up> 4 * x \<up> 2 +10 * a * b \<up> 4 * x * y +5 * a * b \<up> 4 * y \<up> 2 +-1 * b \<up> 5 * x \<up> 2 +-2 * b \<up> 5 * x * y +-1 * b \<up> 5 * y \<up> 2";
1.875 +"a \<up> 5 * x \<up> 2 + 2 * a \<up> 5 * x * y + a \<up> 5 * y \<up> 2 +-5 * a \<up> 4 * b * x \<up> 2 +- 10 * a \<up> 4 * b * x * y +-5 * a \<up> 4 * b * y \<up> 2 +10 * a \<up> 3 * b \<up> 2 * x \<up> 2 +20 * a \<up> 3 * b \<up> 2 * x * y +10 * a \<up> 3 * b \<up> 2 * y \<up> 2 +- 10 * a \<up> 2 * b \<up> 3 * x \<up> 2 +- 20 * a \<up> 2 * b \<up> 3 * x * y +- 10 * a \<up> 2 * b \<up> 3 * y \<up> 2 +5 * a * b \<up> 4 * x \<up> 2 +10 * a * b \<up> 4 * x * y +5 * a * b \<up> 4 * y \<up> 2 +- 1 * b \<up> 5 * x \<up> 2 +- 2 * b \<up> 5 * x * y +- 1 * b \<up> 5 * y \<up> 2";
1.876
1.877 anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1.878
1.879 @@ -1784,8 +1784,8 @@
1.880 #### rls: cancel_p on: (19440 * (x \<up> 8 * y \<up> 2) + -490320 * (x \<up> 6 * y \<up> 4) +
1.881 108240 * (x \<up> 4 * y \<up> 6) +
1.882 -6000 * (x \<up> 2 * y \<up> 8)) /
1.883 -(2160 * (x \<up> 8 * y \<up> 2) + -108240 * (x \<up> 6 * y \<up> 4) +
1.884 +(2160 * (x \<up> 8 * y \<up> 2) + - 108240 * (x \<up> 6 * y \<up> 4) +
1.885 1362000 * (x \<up> 4 * y \<up> 6) +
1.886 - -150000 * (x \<up> 2 * y \<up> 8))
1.887 + - 150000 * (x \<up> 2 * y \<up> 8))
1.888 *)
1.889