1.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 11:28:43 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 12:20:00 2013 +0200
1.3 @@ -17,33 +17,28 @@
1.4 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
1.5 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
1.6 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
1.7 +"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.8 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.9 -"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
1.10 -"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
1.11 +"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
1.12 +"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
1.13 "-------- reverse rewrite ----------------------------------------------------";
1.14 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
1.15 "-------- investigate rls norm_Rational --------------------------------------";
1.16 "-------- examples: rls norm_Rational ----------------------------------------";
1.17 -"-------- numeral rationals -----------------------------";
1.18 -"-------- cancellation ----------------------------------";
1.19 -"-------- common denominator ----------------------------";
1.20 -"-------- multiply and cancel ---------------------------";
1.21 -"-------- common denominator and multiplication ---------";
1.22 -"-------- double fractions ------------------------------";
1.23 -"-------- crucial examples ------------------------------";
1.24 -"-------- examples for Stefan Karnels thesis ------------";
1.25 -"-------- me Schalk I No.186 ----------------------------";
1.26 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1.27 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1.28 -"-------- investigate rulesets for cancel_p -------------";
1.29 -"-------- investigate format of factout_ and factout_p_ -";
1.30 -"-------- how to stepwise construct Scripts -------------";
1.31 -"----------- get_denominator ----------------------------";
1.32 -"--------- several errpats in complicated term -------------------";
1.33 -"--------------------------------------------------------";
1.34 -"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.35 -"--------------------------------------------------------";
1.36 -"--------------------------------------------------------";
1.37 +"-------- rational numerals --------------------------------------------------";
1.38 +"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1.39 +"-------- examples common denominator from: Mathematik 1 Schalk --------------";
1.40 +"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1.41 +"-------- examples common denominator and multiplication from: Schalk --------";
1.42 +"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1.43 +"-------- me Schalk I No.186 -------------------------------------------------";
1.44 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.45 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.46 +"-------- investigate rulesets for cancel_p ----------------------------------";
1.47 +"-------- fun eval_get_denominator -------------------------------------------";
1.48 +"-------- several errpats in complicated term --------------------------------";
1.49 +"-----------------------------------------------------------------------------";
1.50 +"-----------------------------------------------------------------------------";
1.51
1.52
1.53 "-------- fun poly_of_term ---------------------------------------------------";
1.54 @@ -227,7 +222,7 @@
1.55 (* apply the normal_form of a rev-set *)
1.56 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.57 if chk_prepat thy erls prepat t
1.58 - then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
1.59 + then ((*tracing("### app_rev': t = "^term2str t);*) normal_form t)
1.60 else NONE;
1.61 (* val opt = app_rev' thy rrls t ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.62 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
1.63 @@ -363,6 +358,70 @@
1.64 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
1.65 *)
1.66
1.67 +"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.68 +"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.69 +"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
1.70 +val thy = @{theory Isac};
1.71 +"----- SK060904-2a non-termination of add_fraction_p_";
1.72 +val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1.73 + " (-1 * a + b * x) / (a + b * x) ");
1.74 +(* rewrite_set_ thy false norm_Rational t
1.75 +exception Div raised*)
1.76 +(* rewrite_set_ thy false add_fractions_p t;
1.77 +exception Div raised*)
1.78 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) =
1.79 + (@{theory Isac}, false, add_fractions_p, t);
1.80 +"~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
1.81 + (thy, 1, bool, [], rls, term);
1.82 +(* app_rev thy (i+1) rrls t;
1.83 +exception Div raised*)
1.84 +"~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.85 + fun chk_prepat thy erls [] t = true
1.86 + | chk_prepat thy erls prepat t =
1.87 + let
1.88 + fun chk (pres, pat) =
1.89 + (let
1.90 + val subst: Type.tyenv * Envir.tenv =
1.91 + Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
1.92 + in
1.93 + snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
1.94 + end) handle _ => false
1.95 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.96 + | scan_ f (pp::pps) =
1.97 + if f pp then true else scan_ f pps;
1.98 + in scan_ chk prepat end;
1.99 + (* apply the normal_form of a rev-set *)
1.100 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.101 + if chk_prepat thy erls prepat t
1.102 + then ((*tracing("### app_rev': t = "^term2str t);*) normal_form t)
1.103 + else NONE;
1.104 +(* val opt = app_rev' thy rrls t;
1.105 +exception Div raised*)
1.106 +(* val opt = app_rev' thy rrls t;
1.107 +exception Div raised*)
1.108 +"~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
1.109 + (thy, rrls, t);
1.110 +chk_prepat thy erls prepat t = true = true;
1.111 +(*normal_form t
1.112 +exception Div raised*)
1.113 +(* lookup Rational.thy, val add_fractions_p: normal_form = add_fraction_p_ thy*)
1.114 +(*add_fraction_p_ thy t
1.115 +exception Div raised*)
1.116 +"~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t);
1.117 +val SOME ((n1, d1), (n2, d2)) = check_frac_sum t;
1.118 +term2str n1; term2str d1; term2str n2; term2str d2;
1.119 + val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
1.120 + |> filter is_some |> map the |> sort string_ord;
1.121 +print_depth 3; (*999*)
1.122 +val (SOME _, SOME a, SOME _, SOME b) =
1.123 + (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
1.124 +print_depth 3; (*999*)
1.125 +(*
1.126 +val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly
1.127 +val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly
1.128 + val ((a', b'), c) = gcd_poly a b
1.129 +*)
1.130 +
1.131 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.132 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.133 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
1.134 @@ -428,7 +487,7 @@
1.135 then () else error "rational.sml cancel Schalk 188a";
1.136
1.137 val t = str2term "(8*((-1) + x))/(9*((-1) + x))";
1.138 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.139 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.140 if (term2str t', terms2str asm) = ("8 / 9", "[]")
1.141 then () else error "rational.sml cancel Schalk make_polynomial 1";
1.142
1.143 @@ -540,14 +599,14 @@
1.144 ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]")
1.145 then () else error "rational.sml cancel_p heuberger";
1.146
1.147 -"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
1.148 -"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
1.149 -"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
1.150 +"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
1.151 +"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
1.152 +"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
1.153 (*deleted example 204 ... 236b at update Isabelle2012-->2013*)
1.154
1.155 -"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
1.156 -"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
1.157 -"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
1.158 +"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
1.159 +"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
1.160 +"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
1.161 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
1.162 "-------- gcd_poly integration level 1: works on exact term";
1.163 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
1.164 @@ -565,7 +624,7 @@
1.165 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
1.166 if term2str t' = "123 = a / b + c / d + e / f"
1.167 then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
1.168 -val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*)
1.169 +val SOME (t', asm) = rewrite_set_ thy false add_fractions_p_rls t; (*CREATE add_fractions_p_rls*)
1.170 if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
1.171 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
1.172
1.173 @@ -576,16 +635,16 @@
1.174 (*trace_rewrite := false;
1.175 # rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
1.176 ## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
1.177 -## rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
1.178 +## rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
1.179 ## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f
1.180 -## rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
1.181 +## rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
1.182 ## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.183 -## rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
1.184 +## rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
1.185 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
1.186 then () else error "level 4, rewrite_set_ *_p: changed";
1.187
1.188 (* complicated variant *)
1.189 -val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls];
1.190 +val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ add_fractions_p_rls];
1.191 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
1.192 (*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
1.193 ## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
1.194 @@ -593,14 +652,14 @@
1.195 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
1.196 ### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f
1.197 ### rls: cancel_p on: 123 = a / b + c / d + e / f
1.198 -## rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f
1.199 -### rls: common_nominator_p on: 123 = a / b + c / d + e / f
1.200 -### rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
1.201 -### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.202 +## rls: add_fractions_p_rls on: 123 = a / b + c / d + e / f
1.203 +### rls: add_fractions_p on: 123 = a / b + c / d + e / f
1.204 +### rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
1.205 +### rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.206 ## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.207 ### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.208 -## rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.209 -### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
1.210 +## rls: add_fractions_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
1.211 +### rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
1.212 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
1.213 then () else error "level 4, rewrite_set_ *_p_rls: changed"
1.214
1.215 @@ -645,7 +704,7 @@
1.216 then () else error "first 7 elements in revset changed"
1.217
1.218 (** find the rule 'r' to apply to term 't' **)
1.219 -(*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
1.220 +(*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
1.221 for Isabelle2013, we don't get a working revset, but non-termination:
1.222
1.223 val SOME (r as (Thm (str, thm))) = nex revsets t;
1.224 @@ -717,7 +776,7 @@
1.225 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
1.226 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
1.227 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
1.228 -(*Isabelle2013: the example below shows, why "reverse rewriting" only worked for
1.229 +(*WN130909: the example below shows, why "reverse rewriting" only worked for
1.230 special cases.*)
1.231
1.232 (*the term for which reverse rewriting is demonstrated*)
1.233 @@ -755,7 +814,6 @@
1.234 term2str t;
1.235 *)
1.236
1.237 -(*========== inhibit exn WN130824 TODO =======================================================
1.238 "-------- examples: rls norm_Rational ----------------------------------------";
1.239 "-------- examples: rls norm_Rational ----------------------------------------";
1.240 "-------- examples: rls norm_Rational ----------------------------------------";
1.241 @@ -793,7 +851,6 @@
1.242
1.243 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
1.244 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.245 -(*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
1.246 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
1.247 else error "rational.sml 5";
1.248
1.249 @@ -812,801 +869,555 @@
1.250 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) * (1 + x)";
1.251 (*. a/b : c/d translated to a/b * d/c .*)
1.252 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.253 -(*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
1.254 if term2str t' = "1" then () else error "rational.sml 8";
1.255
1.256 -(*............................vvv---TODO: sollte gehen mit poly_order *)
1.257 (*Schalk I, p.92 Nr. 472a*)
1.258 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1.259 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.260 if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
1.261
1.262 -(*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.263 -val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.264 - "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.265 - "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.266 - "(20*x*y/(x^^^2 - 25*y^^^2))");
1.267 -(*... nicht simpl, zerlegt ...*)
1.268 -val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.269 - "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))");
1.270 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.271 -"(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
1.272 -(* ~~~~~~~~~~ poly_order notwendig!*)
1.273 -val t = str2term ("(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.274 - "(20*x*y/(x^^^2 - 25*y^^^2))");
1.275 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.276 -if term2str t' = "1 / (x ^^^ 2 + -25 * y ^^^ 2)" then ()
1.277 -else error "rational.sml norm_Rational 1 / (x ^^^ 2 + -25 * y ^^^ 2)";
1.278 +(*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*)
1.279
1.280 -"nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
1.281 -(*WN.2.6.03 from rlang.sml 56a
1.282 +(*WN130910 add_fractions_p exception Div raised + history:
1.283 +### WN.2.6.03 from rlang.sml 56a
1.284 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.285 -val NONE = rewrite_set_ thy false common_nominator_p t;
1.286 +val NONE = rewrite_set_ thy false add_fractions_p t;
1.287
1.288 -WN060831 nonterm.SK7
1.289 +THE ERROR ALREADY OCCURS IN THIS PART:
1.290 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.291 -val NONE = add_fraction_p_ thy t;
1.292 +val NONE = add_fraction_p_ thy t;
1.293 +
1.294 +SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised ===
1.295 *)
1.296
1.297 -
1.298 -(* ------------------------------------------------------------------- *)
1.299 -(*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
1.300 -(* Simplifier fuer beliebige Buchterme *)
1.301 -(* ------------------------------------------------------------------- *)
1.302 -(*----------------------- norm_Rational_mg ----------------------------*)
1.303 -(* ------------------------------------------------------------------- *)
1.304 -
1.305 -"-------- numeral rationals -----------------------------";
1.306 -"-------- numeral rationals -----------------------------";
1.307 -"-------- numeral rationals -----------------------------";
1.308 +"-------- rational numerals --------------------------------------------------";
1.309 +"-------- rational numerals --------------------------------------------------";
1.310 +"-------- rational numerals --------------------------------------------------";
1.311 (*SRA Schalk I, p.40 Nr. 164b *)
1.312 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
1.313 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.314 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.315 term2str t;
1.316 -if (term2str t) = "19 / 21" then ()
1.317 +if term2str t = "19 / 21" then ()
1.318 else error "rational.sml: diff.behav. in norm_Rational_mg 1";
1.319
1.320 (*SRA Schalk I, p.40 Nr. 166a *)
1.321 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1.322 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.323 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.324 term2str t;
1.325 -if (term2str t) = "45 / 2" then ()
1.326 +if term2str t = "45 / 2" then ()
1.327 else error "rational.sml: diff.behav. in norm_Rational_mg 2";
1.328
1.329 -
1.330 -"-------- cancellation ----------------------------------";
1.331 -"-------- cancellation ----------------------------------";
1.332 -"-------- cancellation ----------------------------------";
1.333 +"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1.334 +"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1.335 +"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1.336 (* e190c Stefan K.*)
1.337 -val t = str2term
1.338 -"((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.339 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.340 -term2str t;
1.341 -if (term2str t) =
1.342 -"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.343 -then ()
1.344 -else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1.345 +val t = str2term "((1 + 9*a^^^2) * (1 + 3*a)) / ((3*a + 9*a^^^2) * (1 + 3*a))";
1.346 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.347 +if term2str t = "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.348 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1.349
1.350 (* e192b Stefan K.*)
1.351 -val t = str2term
1.352 -"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.353 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.354 -term2str t;
1.355 -if (term2str t) =
1.356 -"x ^^^ 2 / y ^^^ 2"
1.357 -then ()
1.358 -else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1.359 +val t = str2term "(x^^^2 * (7*x + (-1)*y)) / (y^^^2 * (7*x + (-1)*y))";
1.360 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.361 +if term2str t = "x ^^^ 2 / y ^^^ 2"
1.362 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1.363
1.364 (*SRC Schalk I, p.66 Nr. 379c *)
1.365 -val t = str2term
1.366 -"(a - b)/(b - a)";
1.367 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.368 +val t = str2term "(a - b)/(b - a)";
1.369 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.370 term2str t;
1.371 -if (term2str t) =
1.372 -"-1"
1.373 -then ()
1.374 -else error "rational.sml: diff.behav. in norm_Rational_mg 5";
1.375 +if term2str t = "-1"
1.376 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
1.377
1.378 (*SRC Schalk I, p.66 Nr. 380b *)
1.379 -val t = str2term
1.380 -"15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
1.381 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.382 -term2str t;
1.383 -if (term2str t) =
1.384 -"(27 + 12 * x) / (28 + 8 * x)"
1.385 -then ()
1.386 -else error "rational.sml: diff.behav. in norm_Rational_mg 6";
1.387 +val t = str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
1.388 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.389 +if term2str t = "(27 + 12 * x) / (28 + 8 * x)"
1.390 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
1.391
1.392 -(*Schalk I, p.60 Nr. 215c *)
1.393 -(* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
1.394 -(* WN060831????MG1
1.395 -val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1.396 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.397 -term2str t;
1.398 -if (term2str t) =
1.399 -"(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.400 -then ()
1.401 -else error "rational.sml: diff.behav. in norm_Rational_mg 7";
1.402 -*)
1.403 -(*val t = str2term
1.404 -"(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.405 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.406 -term2str t;*)
1.407 -(* uncaught exception nonexhaustive binding failure
1.408 - raised at: stdIn:93.1-93.51 *)
1.409 -
1.410 -(*Schalk I, p.66 Nr. 381a *)
1.411 -(* ACHTUNG: rechnet ca. 2 Minuten !!! *)
1.412 -(* WN060831???MG2
1.413 -val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1.414 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.415 -term2str t;
1.416 -if (term2str t) =
1.417 -"(a + b) / (4 * a + -4 * b)"
1.418 -then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
1.419 -*)
1.420 +(*Schalk I, p.60 Nr. 215c: was not cancelled with Isabelle2002 *)
1.421 +val t = str2term "(a + b)^^^4 * (x - y) / ((x - y)^^^3 * (a + b)^^^2)";
1.422 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.423 +if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
1.424 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
1.425
1.426 (*SRC Schalk I, p.66 Nr. 381b *)
1.427 val t = str2term
1.428 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1.429 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.430 -term2str t;
1.431 -if (term2str t) =
1.432 -"-1 / (5 + -2 * x)"
1.433 -then ()
1.434 -else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1.435 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.436 +if term2str t = "1 / (-5 + 2 * x)"
1.437 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1.438 +
1.439 +(* e190c Stefan K.*)
1.440 +val t = str2term "((1 + 9*a^^^2) * (1 + 3*a)) / ((3*a + 9*a^^^2) * (1 + 3 * a))";
1.441 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.442 +if term2str t = "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.443 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1.444 +
1.445 +(* e192b Stefan K.*)
1.446 +val t = str2term "(x^^^2 * (7*x + (-1)*y)) / (y^^^2 * (7*x + (-1)*y))";
1.447 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.448 +if term2str t = "x ^^^ 2 / y ^^^ 2"
1.449 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1.450 +
1.451 +(*SRC Schalk I, p.66 Nr. 379c *)
1.452 +val t = str2term "(a - b) / (b - a)";
1.453 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.454 +if term2str t = "-1"
1.455 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
1.456 +
1.457 +(*SRC Schalk I, p.66 Nr. 380b *)
1.458 +val t = str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
1.459 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.460 +if term2str t = "(27 + 12 * x) / (28 + 8 * x)"
1.461 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
1.462 +
1.463 +(*Schalk I, p.60 Nr. 215c *)
1.464 +val t = str2term "(a + b)^^^4 * (x - y) / ((x - y)^^^3 * (a + b)^^^2)";
1.465 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.466 +if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
1.467 +then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
1.468 +
1.469 +(* extreme example from somewhere *)
1.470 +val t = str2term
1.471 + ("(a^^^4 * x + -1*a^^^4 * y + 4*a^^^3 * b * x + -4*a^^^3 * b * y + " ^
1.472 + "6*a^^^2 * b^^^2 * x + -6*a^^^2 * b^^^2 * y + 4*a * b^^^3 * x + -4*a * b^^^3 * y + " ^
1.473 + "b^^^4 * x + -1*b^^^4 * y) " ^
1.474 + " / (a^^^2 * x^^^3 + -3*a^^^2 * x^^^2 * y + 3*a^^^2 * x * y^^^2 + -1*a^^^2 * y^^^3 + " ^
1.475 + "2*a * b * x^^^3 + -6*a * b * x^^^2 * y + 6*a * b * x * y^^^2 + -2*a * b * y^^^3 + " ^
1.476 + "b^^^2 * x^^^3 + -3*b^^^2 * x^^^2 * y + 3*b^^^2 * x * y^^^2 + -1*b ^^^ 2 * y ^^^ 3)")
1.477 +val SOME (t, _) = rewrite_set_ thy false cancel_p t;
1.478 +if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
1.479 +then () else error "with Isabelle2002: NONE -- now SOME changed";
1.480 +
1.481 +(*Schalk I, p.66 Nr. 381a *)
1.482 +(* ATTENTION: here the rls is very slow. In Isabelle2002 this required 2 min *)
1.483 +val t = str2term "18*(a + b)^^^3 * (a - b)^^^2 / (72*(a - b)^^^3 * (a + b)^^^2)";
1.484 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.485 +if term2str t = "(a + b) / (4 * a + -4 * b)"
1.486 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
1.487 +
1.488 +(*SRC Schalk I, p.66 Nr. 381b *)
1.489 +val t = str2term "(4*x^^^2 - 20*x + 25) / (2*x - 5)^^^3";
1.490 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.491 +if term2str t = "1 / (-5 + 2 * x)"
1.492 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1.493
1.494 (*SRC Schalk I, p.66 Nr. 381c *)
1.495 -val t = str2term
1.496 -"(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
1.497 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.498 -term2str t;
1.499 -if (term2str t) =
1.500 -"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.501 -then ()
1.502 -else error "rational.sml: diff.behav. in norm_Rational_mg 10";
1.503 +val t = str2term "(27*a^^^3 + 9*a^^^2+3*a+1) / (27*a^^^3 + 18*a^^^2+3*a)";
1.504 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.505 +if term2str t = "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.506 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 10";
1.507
1.508 (*SRC Schalk I, p.66 Nr. 383a *)
1.509 -val t = str2term
1.510 -"(5*a^^^2 - 5*a*b)/(a - b)^^^2";
1.511 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.512 -term2str t;
1.513 -if (term2str t) =
1.514 -"5 * a / (a + -1 * b)"
1.515 -then ()
1.516 -else error "rational.sml: diff.behav. in norm_Rational_mg 11";
1.517 +val t = str2term "(5*a^^^2 - 5*a*b) / (a - b)^^^2";
1.518 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.519 +if term2str t = "-5 * a / (-1 * a + b)"
1.520 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 11";
1.521
1.522 +"----- NOT TERMINATING ?: worked before 0707xx";
1.523 +val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.524 +(* WN130911 "exception Div raised" by
1.525 + cancel_p_ thy (str2term ("(-1 + -1 * b + a ^^^ 2 + a ^^^ 2 * b) /" ^
1.526 + "(-1 + -1 * a + b ^^^ 2 + a * b ^^^ 2)"))
1.527
1.528 -"-------- common denominator ----------------------------";
1.529 -"-------- common denominator ----------------------------";
1.530 -"-------- common denominator ----------------------------";
1.531 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.532 +if term2str t = "(1 + -1 * a) / (1 + -1 * b)" then ()
1.533 +else error "rational.sml MG tests 3e";
1.534 +*)
1.535 +
1.536 +"-------- examples common denominator from: Mathematik 1 Schalk --------------";
1.537 +"-------- examples common denominator from: Mathematik 1 Schalk --------------";
1.538 +"-------- examples common denominator from: Mathematik 1 Schalk --------------";
1.539 (*SRA Schalk I, p.67 Nr. 403a *)
1.540 -val t = str2term
1.541 -"4/x - 3/y - 1";
1.542 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.543 -term2str t;
1.544 -if (term2str t) =
1.545 -"(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1.546 -then ()
1.547 -else error "rational.sml: diff.behav. in norm_Rational_mg 12";
1.548 +val t = str2term "4/x - 3/y - 1";
1.549 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.550 +if term2str t = "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1.551 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 12";
1.552
1.553 -(*SRA Schalk I, p.67 Nr. 407b *)
1.554 -val t = str2term
1.555 -"(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
1.556 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.557 -term2str t;
1.558 -if (term2str t) =
1.559 -"4 / c"
1.560 -then ()
1.561 -else error "rational.sml: diff.behav. in norm_Rational_mg 13";
1.562 +val t = str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
1.563 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.564 +if term2str t = "4 / c"
1.565 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 13";
1.566
1.567 (*SRA Schalk I, p.67 Nr. 410b *)
1.568 -val t = str2term
1.569 -"1/(x+1) + 1/(x+2) - 2/(x+3)";
1.570 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.571 -term2str t;
1.572 -if (term2str t) =
1.573 -"(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1.574 -then ()
1.575 -else error "rational.sml: diff.behav. in norm_Rational_mg 14";
1.576 +val t = str2term "1/(x+1) + 1/(x+2) - 2/(x+3)";
1.577 +(* WN130911 non-termination due to non-termination of
1.578 + cancel_p_ thy (str2term "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)")
1.579 +
1.580 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.581 +if term2str t = "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1.582 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 14";
1.583 +*)
1.584
1.585 (*SRA Schalk I, p.67 Nr. 413b *)
1.586 -val t = str2term
1.587 -"(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
1.588 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.589 -term2str t;
1.590 -if (term2str t) =
1.591 -"6 * x / (1 + -1 * x ^^^ 2)"
1.592 -then ()
1.593 -else error "rational.sml: diff.behav. in norm_Rational_mg 15";
1.594 +val t = str2term "(1 + x)/(1 - x) - (1 - x)/(1 + x) + 2*x/(1 - x^^^2)";
1.595 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.596 +if term2str t = "6 * x / (1 + -1 * x ^^^ 2)"
1.597 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 15";
1.598
1.599 (*SRA Schalk I, p.68 Nr. 414a *)
1.600 -val t = str2term
1.601 -"(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1.602 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.603 -term2str t;
1.604 -if (term2str t) =
1.605 -"(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1.606 -then ()
1.607 -else error "rational.sml: diff.behav. in norm_Rational_mg 16";
1.608 -
1.609 -(*SRA Schalk I, p.68 Nr. 423a *)
1.610 -val t = str2term
1.611 -"(2*x+3*y)/x + (4*x^^^3 - x*y^^^2 - 3*y^^^3)/(x^^^3 - 2*x^^^2*y+x*y^^^2) - (5*x+6*y)/(x - y)";
1.612 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.613 -term2str t;
1.614 -if (term2str t) =
1.615 -"1"
1.616 -then ()
1.617 -else error "rational.sml: diff.behav. in norm_Rational_mg 17";
1.618 +val t = str2term "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1.619 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.620 +if term2str t ="(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1.621 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 16";
1.622
1.623 (*SRA Schalk I, p.68 Nr. 428b *)
1.624 val t = str2term
1.625 -"1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1.626 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.627 -term2str t;
1.628 -if (term2str t) =
1.629 -"4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1.630 -then ()
1.631 -else error "rational.sml: diff.behav. in norm_Rational_mg 18";
1.632 + "1/(a - b)^^^2 + 1/(a + b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1.633 +(* WN130911 non-termination due to non-termination of
1.634 + cancel_p_ thy (str2term "(4 + -4 * b ^^^ 2) / (a ^^^ 4 + -2 * (a ^^^ 2 * b ^^^ 2) + b ^^^ 4)")
1.635 +
1.636 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.637 +if term2str t = "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1.638 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";
1.639 +*)
1.640
1.641 (*SRA Schalk I, p.68 Nr. 430b *)
1.642 val t = str2term
1.643 -"a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2";
1.644 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.645 -term2str t;
1.646 -if (term2str t) =
1.647 -"a + 3 * b"
1.648 -then ()
1.649 -else error "rational.sml: diff.behav. in norm_Rational_mg 19";
1.650 -
1.651 + "a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2";
1.652 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.653 +if term2str t = "a + 3 * b"
1.654 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 19";
1.655
1.656 (*SRA Schalk I, p.68 Nr. 432 *)
1.657 val t = str2term
1.658 -"(a^^^2+a*b)/(a^^^2 - b^^^2) - (b^^^2 - a*b)/(b^^^2 - a^^^2) + a^^^2*(a - b)/(a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2)/(a^^^3 - a*b^^^2) - 2*b^^^2/(a^^^2 - b^^^2)";
1.659 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.660 + ("(a^^^2 + a*b) / (a^^^2 - b^^^2) - (b^^^2 - a*b) / (b^^^2 - a^^^2) + " ^
1.661 + "a^^^2*(a - b) / (a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2) / (a^^^3 - a*b^^^2) - " ^
1.662 + "2*b^^^2 / (a^^^2 - b^^^2)");
1.663 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.664 term2str t;
1.665 -if (term2str t) =
1.666 -"0"
1.667 -then ()
1.668 -else error "rational.sml: diff.behav. in norm_Rational_mg 20";
1.669 +if term2str t = "0"
1.670 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 20";
1.671
1.672 -(*Eigenes*)
1.673 +(* some example *)
1.674 +val t = str2term "3*a / (a*b) + x/y";
1.675 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.676 +if term2str t = "(3 * y + b * x) / (b * y)"
1.677 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";
1.678 +
1.679 +"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1.680 +"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1.681 +"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1.682 +(*------- SRM Schalk I, p.68 Nr. 436a *)
1.683 +val t = str2term "3*(x+y) / (15*(x - y)) * 25*(x - y)^^^2 / (18*(x + y)^^^2)";
1.684 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.685 +if term2str t = "(-5 * x + 5 * y) / (-18 * x + -18 * y)"
1.686 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";
1.687 +
1.688 +(*------- SRM.test Schalk I, p.68 Nr. 436b *)
1.689 +val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1.690 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.691 +if term2str t = "5 * a / (a + -1 * b)"
1.692 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 23";
1.693 +
1.694 +(*------- Schalk I, p.68 Nr. 437a *)
1.695 +val t = str2term "(3*a - 4*b) / (4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.696 +(* raises an exception for unclear reasons:
1.697 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.698 +:
1.699 +### rls: cancel_p on: (9 * a ^^^ 2 + -16 * b ^^^ 2) / (4 * c + 3 * e) /
1.700 +(9 * a ^^^ 2 + -16 * b ^^^ 2)
1.701 +exception Div raised
1.702 +
1.703 +BUT
1.704 val t = str2term
1.705 -"3*a/(a*b) + x/y";
1.706 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.707 -term2str t;
1.708 -if (term2str t) =
1.709 -"(3 * y + b * x) / (b * y)"
1.710 -then ()
1.711 -else error "rational.sml: diff.behav. in norm_Rational_mg 21";
1.712 + ("(9 * a ^^^ 2 + -16 * b ^^^ 2) / (4 * c + 3 * e) /" ^
1.713 + "(9 * a ^^^ 2 + -16 * b ^^^ 2)");
1.714 +NONE = cancel_p_ thy t;
1.715
1.716 -
1.717 -"-------- multiply and cancel ---------------------------";
1.718 -"-------- multiply and cancel ---------------------------";
1.719 -"-------- multiply and cancel ---------------------------";
1.720 -(*SRM Schalk I, p.68 Nr. 436a *)
1.721 -val t = str2term
1.722 -"3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
1.723 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.724 -term2str t;
1.725 -if (term2str t) =
1.726 -"(5 * x + -5 * y) / (18 * x + 18 * y)"
1.727 -then ()
1.728 -else error "rational.sml: diff.behav. in norm_Rational_mg 22";
1.729 -
1.730 -(*SRM.test Schalk I, p.68 Nr. 436b *)
1.731 -(*WN060420???MG3 crashes with method 'simplify' in
1.732 - IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1.733 -val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1.734 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.735 -term2str t;
1.736 -if (term2str t) =
1.737 -"5 * a / (a + -1 * b)"
1.738 -then ()
1.739 -else error "rational.sml: diff.behav. in norm_Rational_mg 23";
1.740 -
1.741 -(*Schalk I, p.68 Nr. 437a *)
1.742 -val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.743 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.744 -if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1.745 +if term2str t = "1 / (4 * c + 3 * e)" then ()
1.746 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1.747 +*)
1.748
1.749 "----- S.K. corrected non-termination 060904";
1.750 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.751 -val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.752 -term2str t';
1.753 -if term2str t' =
1.754 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.755 +if term2str t =
1.756 "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"
1.757 (*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
1.758 then () else error "rational.sml: S.K.8..corrected 060904-6";
1.759
1.760 "----- S.K. corrected non-termination of cancel_p_";
1.761 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
1.762 -"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
1.763 + "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
1.764 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1.765 -if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.766 -else error "rational.sml: diff.behav. in cancel_p S.K.8";
1.767 +if term2str t' = "1 / (4 * c + 3 * e)"
1.768 +then () else error "rational.sml: diff.behav. in cancel_p S.K.8";
1.769
1.770 -(*Schalk I, p.68 Nr. 437b *)
1.771 -(* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1.772 -val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.773 -(* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1.774 - *)
1.775 -
1.776 -"================delete===";
1.777 -(*a casual output from above*)
1.778 -val t = str2term
1.779 -"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.780 -(* WN060831 nonterm.SK10
1.781 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.782 -term2str t;
1.783 +(*------- Schalk I, p.68 Nr. 437b*)
1.784 +val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.785 +(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.786 +:
1.787 +#### rls: cancel_p on: (a * x ^^^ 2 + -2 * (a * (x * y)) + a * y ^^^ 2 + b * x ^^^ 2 +
1.788 + -2 * (b * (x * y)) +
1.789 + b * y ^^^ 2) /
1.790 +(a ^^^ 2 * x ^^^ 2 + -1 * (a ^^^ 2 * y ^^^ 2) + -1 * (b ^^^ 2 * x ^^^ 2) +
1.791 + b ^^^ 2 * y ^^^ 2)
1.792 +exception Div raised
1.793 *)
1.794
1.795 -(*SRM Schalk I, p.68 Nr. 438a *)
1.796 -val t = str2term
1.797 -"x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
1.798 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.799 -term2str t;
1.800 -if (term2str t) =
1.801 -"x ^^^ 2"
1.802 -then ()
1.803 -else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1.804 +(*------- SRM Schalk I, p.68 Nr. 438a *)
1.805 +val t = str2term "x*y / (x*y - y^^^2) * (x^^^2 - x*y)";
1.806 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.807 +if term2str t = "x ^^^ 2"
1.808 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1.809
1.810 -(*SRM Schalk I, p.68 Nr. 439b *)
1.811 -val t = str2term
1.812 -"(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
1.813 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.814 -term2str t;
1.815 -if (term2str t) =
1.816 -"(x + -4 * x ^^^ 3) / 2"
1.817 -then ()
1.818 -else error "rational.sml: diff.behav. in norm_Rational_mg 25";
1.819 +(*------- SRM Schalk I, p.68 Nr. 439b *)
1.820 +val t = str2term "(4*x^^^2 + 4*x + 1) * ((x^^^2 - 2*x^^^3) / (4*x^^^2 + 2*x))";
1.821 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.822 +if term2str t = "(x + -4 * x ^^^ 3) / 2"
1.823 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 25";
1.824
1.825 -(*SRM Schalk I, p.68 Nr. 440a *)
1.826 -val t = str2term
1.827 -"(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
1.828 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.829 -term2str t;
1.830 -if (term2str t) =
1.831 -"(-3 + x) / (2 + x)"
1.832 -then ()
1.833 -else error "rational.sml: diff.behav. in norm_Rational_mg 26";
1.834 +(*------- SRM Schalk I, p.68 Nr. 440a *)
1.835 +val t = str2term "(x^^^2 - 2*x) / (x^^^2 - 3*x) * (x - 3)^^^2 / (x^^^2 - 4)";
1.836 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.837 +if term2str t = "(-3 + x) / (2 + x)"
1.838 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 26";
1.839
1.840 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1.841 +val t = str2term "(a^^^3 - 9*a) / (a^^^3*b - a*b^^^3) * (a^^^2*b + a*b^^^2) / (a+3)";
1.842 +(* WN130911 non-termination for unclear reasons:
1.843 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.844 +
1.845 +... ENDS WITH THIS TRACE:
1.846 +:
1.847 +### rls: cancel_p on: (-9 * (a ^^^ 3 * b) + -9 * (a ^^^ 2 * b ^^^ 2) + a ^^^ 5 * b +
1.848 + a ^^^ 4 * b ^^^ 2) /
1.849 +(a ^^^ 3 * b + -1 * (a * b ^^^ 3)) /
1.850 +(3 + a)
1.851 +BUT THIS IS CORRECTLY RECOGNISED
1.852 val t = str2term
1.853 -"(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.854 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.855 + ("(-9 * (a^^^3 * b) + -9 * (a^^^2 * b^^^2) + a^^^5 * b + a^^^4 * b^^^2) /" ^
1.856 + "(a^^^3 * b + -1 * (a * b^^^3)) / (3 + (a::real))");
1.857 +AS
1.858 +NONE = cancel_p_ thy t;
1.859 +
1.860 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.861 else error "rational.sml: diff.behav. in norm_Rational 27";
1.862 +*)
1.863
1.864 "----- SK12 works since 0707xx";
1.865 -val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.866 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.867 +val t = str2term "(a^^^3 - 9*a) * (a^^^2*b+a*b^^^2) / ((a^^^3*b - a*b^^^3) * (a+3))";
1.868 +(* WN130911 non-termination due to non-termination of
1.869 + cancel_p_ thy (str2term "(4 + -4 * b ^^^ 2) / (a ^^^ 4 + -2 * (a ^^^ 2 * b ^^^ 2) + b ^^^ 4)")
1.870 +
1.871 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.872 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.873 else error "rational.sml: diff.behav. in norm_Rational 28";
1.874 +*)
1.875
1.876 -
1.877 -"-------- common denominator and multiplication ---------";
1.878 -"-------- common denominator and multiplication ---------";
1.879 -"-------- common denominator and multiplication ---------";
1.880 -(*SRAM Schalk I, p.69 Nr. 441b *)
1.881 +"-------- examples common denominator and multiplication from: Schalk --------";
1.882 +"-------- examples common denominator and multiplication from: Schalk --------";
1.883 +"-------- examples common denominator and multiplication from: Schalk --------";
1.884 +(*------- SRAM Schalk I, p.69 Nr. 441b *)
1.885 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1.886 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.887 -term2str t;
1.888 -if (term2str t) =
1.889 - "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.890 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.891 +if term2str t = "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.892 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
1.893
1.894 -(*SRAM Schalk I, p.69 Nr. 442b *)
1.895 -val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)";
1.896 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.897 -term2str t;
1.898 -if (term2str t) =
1.899 -"5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.900 +(*------- SRAM Schalk I, p.69 Nr. 442b *)
1.901 +val t = str2term ("(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x) * " ^
1.902 + "(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)");
1.903 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.904 +if term2str t = "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.905 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
1.906
1.907 -(*SRAM Schalk I, p.69 Nr. 443b *)
1.908 -val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.909 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.910 -term2str t;
1.911 -if (term2str t) =
1.912 -"(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.913 +(*------- SRAM Schalk I, p.69 Nr. 443b *)
1.914 +val t = str2term "(a/2 + b/3) * (b/3 - a/2)";
1.915 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.916 +if term2str t = "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.917 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
1.918
1.919 -(*SRAM Schalk I, p.69 Nr. 445b *)
1.920 +(*------- SRAM Schalk I, p.69 Nr. 445b *)
1.921 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.922 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.923 -term2str t;
1.924 -if (term2str t) =
1.925 -"a ^^^ 3 / 27"
1.926 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.927 +if term2str t = "a ^^^ 3 / 27"
1.928 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
1.929
1.930 -(*SRAM Schalk I, p.69 Nr. 446b *)
1.931 +(*------- SRAM Schalk I, p.69 Nr. 446b *)
1.932 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.933 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.934 -term2str t;
1.935 -if (term2str t) =
1.936 -"30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.937 -then ()
1.938 -else error "rational.sml: diff.behav. in norm_Rational_mg 32";
1.939 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.940 +if term2str t = "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.941 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";
1.942
1.943 -(*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.944 +(*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.945 val t = str2term
1.946 "(2*x^^^2/(3*y)+x/y^^^2)*(4*x^^^4/(9*y^^^2)+x^^^2/y^^^4)*(2*x^^^2/(3*y) - x/y^^^2)";
1.947 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.948 -term2str t;
1.949 -if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.950 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.951 +if term2str t = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.952 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
1.953
1.954 -
1.955 -(*SRAM Schalk I, p.69 Nr. 450a *)
1.956 +(*------- SRAM Schalk I, p.69 Nr. 450a *)
1.957 val t = str2term
1.958 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1.959 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.960 -term2str t;
1.961 -if (term2str t) =
1.962 -"(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.963 -then ()
1.964 -else error "rational.sml: diff.behav. in norm_Rational_mg 34";
1.965 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.966 +if term2str t = "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.967 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 34";
1.968
1.969 +(*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1.970 +val t = str2term
1.971 + ("(15*a^^^4/(a*x^^^3) - 5*a*((b^^^4 - 5*c^^^2*x) / x^^^2)) * " ^
1.972 + "(x^^^3/(5*a*b^^^3*c^^^3)) + a/c^^^3 * (x*(b/a) - 3*b*(a/b^^^4))");
1.973 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.974 +if term2str t = "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1.975 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";
1.976
1.977 -"-------- double fractions ------------------------------";
1.978 -"-------- double fractions ------------------------------";
1.979 -"-------- double fractions ------------------------------";
1.980 -(*SRD Schalk I, p.69 Nr. 454b *)
1.981 -val t = str2term
1.982 -"((2 - x)/(2*a)) / (2*a/(x - 2))";
1.983 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.984 -term2str t;
1.985 -if (term2str t) =
1.986 -"(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.987 -then ()
1.988 -else error "rational.sml: diff.behav. in norm_Rational_mg 35";
1.989
1.990 -(*SRD Schalk I, p.69 Nr. 455a *)
1.991 -val t = str2term
1.992 -"(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.993 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.994 -term2str t;
1.995 -if (term2str t) =
1.996 -"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.997 +"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1.998 +"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1.999 +"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1.1000 +"----- SRD Schalk I, p.69 Nr. 454b";
1.1001 +val t = str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
1.1002 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1003 +if term2str t = "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.1004 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 35";
1.1005 +
1.1006 +"----- SRD Schalk I, p.69 Nr. 455a";
1.1007 +val t = str2term "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.1008 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1009 +if term2str t = "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.1010 else error "rational.sml: diff.behav. in norm_Rational_mg 36";
1.1011
1.1012 -
1.1013 "----- Schalk I, p.69 Nr. 455b";
1.1014 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.1015 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1016 +(* WN130911 non-termination due to non-termination of
1.1017 + cancel_p_ thy (str2term ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
1.1018 + "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"))
1.1019 +
1.1020 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1021 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.1022 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
1.1023 +*)
1.1024
1.1025 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1.1026 -val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.1027 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1028 +val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1.1029 +(* WN130911 non-termination due to non-termination of
1.1030 + cancel_p_ thy (str2term ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
1.1031 + "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"))
1.1032 +
1.1033 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1034 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.1035 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
1.1036 +*)
1.1037
1.1038 "----- ?: worked before 0707xx";
1.1039 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1.1040 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1041 -if term2str t = "-1 / (3 + y)" then ()
1.1042 -else error "rational.sml: -1 / (3 + y) norm_Rational";
1.1043 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1044 +if term2str t = "-1 / (3 + y)"
1.1045 +then () else error "rational.sml: -1 / (3 + y) norm_Rational";
1.1046
1.1047 -(*SRD Schalk I, p.69 Nr. 456b *)
1.1048 -val t = str2term
1.1049 -"(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.1050 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1051 -term2str t;
1.1052 -if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1.1053 -else error "rational.sml: diff.behav. in norm_Rational_mg 38";
1.1054 +"----- SRD Schalk I, p.69 Nr. 456b";
1.1055 +val t = str2term "(b^^^3 - b^^^2) / (b^^^2+b) / (b^^^2 - 1)";
1.1056 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1057 +if term2str t = "b / (1 + 2 * b + b ^^^ 2)"
1.1058 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 38";
1.1059
1.1060 -(*SRD Schalk I, p.69 Nr. 457b *)
1.1061 -val t = str2term
1.1062 -"(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1.1063 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1064 -term2str t;
1.1065 -if (term2str t) =
1.1066 - "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.1067 +"----- SRD Schalk I, p.69 Nr. 457b";
1.1068 +val t = str2term "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1.1069 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1070 +if term2str t = "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.1071 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
1.1072
1.1073 "----- Schalk I, p.69 Nr. 458b works since 0707";
1.1074 +val t = str2term "(2*a^^^2*x - a^^^2) / (a*x - b*x) / (b^^^2*(2*x - 1) / (x*(a - b)))";
1.1075 +(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1076 +:
1.1077 +### rls: cancel_p on: (-1 * a ^^^ 2 + 2 * (a ^^^ 2 * x)) / (a * x + -1 * (b * x)) /
1.1078 +((-1 * b ^^^ 2 + 2 * (b ^^^ 2 * x)) / (a * x + -1 * (b * x)))
1.1079 +exception Div raised
1.1080 +
1.1081 +BUT
1.1082 val t = str2term
1.1083 -"(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.1084 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1085 + ("(-1 * a ^^^ 2 + 2 * (a ^^^ 2 * x)) / (a * x + -1 * (b * x)) /" ^
1.1086 + "((-1 * b ^^^ 2 + 2 * (b ^^^ 2 * x)) / (a * x + -1 * (b * x)))");
1.1087 +NONE = cancel_p_ thy t;
1.1088 +
1.1089 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
1.1090 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
1.1091 +*)
1.1092
1.1093 -(*SRD Schalk I, p.69 Nr. 459b *)
1.1094 +"----- SRD Schalk I, p.69 Nr. 459b";
1.1095 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.1096 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1097 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1098 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
1.1099 else error "rational.sml: diff.behav. in norm_Rational_mg 41";
1.1100
1.1101 +"----- Schalk I, p.69 Nr. 460b nonterm.SK";
1.1102 +val t = str2term "(9*(x^^^2 - 8*x + 16) / (4*(y^^^2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))";
1.1103 +(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1104 +exception Div raised
1.1105
1.1106 -(*Schalk I, p.69 Nr. 460b nonterm.SK
1.1107 +BUT
1.1108 val t = str2term
1.1109 -"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.1110 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1111 -if term2str t =
1.1112 -then ()
1.1113 -else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1.1114 + ("(144 + -72 * x + 9 * x ^^^ 2) / (4 + -8 * y + 4 * y ^^^ 2) /" ^
1.1115 + "((-12 + 3 * x) / (-16 + 16 * y))");
1.1116 +NONE = cancel_p_ thy t;
1.1117
1.1118 -val t = str2term
1.1119 -"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.1120 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1121 -... non terminating.
1.1122 -val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.1123 -"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.1124 -val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1.1125 -... non terminating.*)
1.1126 +if term2str t = !!!!!!!!!!!!!!!!!!!!!!!!!
1.1127 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1.1128 +*)
1.1129
1.1130 -(*SRD Schalk I, p.70 Nr. 472a *)
1.1131 -val t = str2term ("((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/" ^
1.1132 - "((4*x - 8*y)/(x + y))");
1.1133 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1134 -term2str t;
1.1135 -if (term2str t) =
1.1136 -"x + y"
1.1137 -then ()
1.1138 -else error "rational.sml: diff.behav. in norm_Rational_mg 43";
1.1139 +"----- some variant of the above; was non-terminating before";
1.1140 +val t = str2term "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.1141 +val SOME (t , _) = rewrite_set_ thy false norm_Rational t;
1.1142 +if term2str t = "(48 + -12 * x) / (1 + -1 * y)"
1.1143 +then () else error "some variant of the above; was non-terminating before";
1.1144
1.1145 +"----- SRD Schalk I, p.70 Nr. 472a";
1.1146 +val t = str2term ("((8*x^^^2 - 32*y^^^2) / (2*x + 4*y)) / ((4*x - 8*y) / (x + y))");
1.1147 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1148 +if term2str t = "x + y"
1.1149 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 43";
1.1150
1.1151 -(*----------------------------------------------------------------------*)
1.1152 -(*---------------------- Einfache Dppelbrche --------------------------*)
1.1153 -(*----------------------------------------------------------------------*)
1.1154 +"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1.1155 +val t = str2term ("(a - (a*b + b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
1.1156 + "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
1.1157 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1158 +if term2str t = "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.1159 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 51";
1.1160
1.1161 (*SRD Schalk I, p.69 Nr. 461a *)
1.1162 -val t = str2term
1.1163 -"(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.1164 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1165 -term2str t;
1.1166 -if (term2str t) =
1.1167 -"1 / 2"
1.1168 -then ()
1.1169 -else error "rational.sml: diff.behav. in norm_Rational_mg 44";
1.1170 +val t = str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.1171 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1172 +if term2str t = "1 / 2"
1.1173 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 44";
1.1174
1.1175 (*SRD Schalk I, p.69 Nr. 464b *)
1.1176 -val t = str2term
1.1177 -"(a - a/(a - 2)) / (a + a/(a - 2))";
1.1178 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1179 -term2str t;
1.1180 -if (term2str t) =
1.1181 -"(3 + -1 * a) / (1 + -1 * a)"
1.1182 -then ()
1.1183 -else error "rational.sml: diff.behav. in norm_Rational_mg 45";
1.1184 +val t = str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
1.1185 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1186 +if term2str t = "(-3 + a) / (-1 + a)"
1.1187 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 45";
1.1188
1.1189 (*SRD Schalk I, p.69 Nr. 465b *)
1.1190 -val t = str2term
1.1191 -"((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.1192 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1193 -term2str t;
1.1194 -if (term2str t) =
1.1195 -"(4 * x + 6 * y + -9 * z) / (4 * x)"
1.1196 -then ()
1.1197 -else error "rational.sml: diff.behav. in norm_Rational_mg 46";
1.1198 +val t = str2term "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) / (x/9 + y/6 + z/4)";
1.1199 +(* WN130911 non-termination due to non-termination of
1.1200 + cancel_p_ thy (str2term
1.1201 + ("("(576 * x ^^^ 2 + 1728 * (x * y) + 1296 * y ^^^ 2 + -2916 * z ^^^ 2) /" ^
1.1202 + "(576 * x ^^^ 2 + 864 * (x * y) + 1296 * (x * z))"))
1.1203 +
1.1204 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1205 +if term2str t = "(4 * x + 6 * y + -9 * z) / (4 * x)"
1.1206 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 46";
1.1207 +*)
1.1208
1.1209 (*SRD Schalk I, p.69 Nr. 466b *)
1.1210 -val t = str2term
1.1211 -"((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1.1212 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1213 -term2str t;
1.1214 -if (term2str t) =
1.1215 -"(25 + -10 * x + x ^^^ 2) / 18"
1.1216 -then ()
1.1217 -else error "rational.sml: diff.behav. in norm_Rational_mg 47";
1.1218 +val t = str2term "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1.1219 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1220 +if term2str t = "(25 + -10 * x + x ^^^ 2) / 18"
1.1221 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 47";
1.1222
1.1223 (*SRD Schalk I, p.70 Nr. 469 *)
1.1224 -val t = str2term
1.1225 -"3*b^^^2/(4*a^^^2 - 8*a*b + 4*b^^^2)/(a/(a^^^2*b - b^^^3) + (a - b)/(4*a*b^^^2+4*b^^^3) - 1/(4*b^^^2))";
1.1226 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1227 -term2str t;
1.1228 -if (term2str t) =
1.1229 -"3 * b ^^^ 3 / (2 * a + -2 * b)"
1.1230 -then ()
1.1231 -else error "rational.sml: diff.behav. in norm_Rational_mg 48";
1.1232 +val t = str2term ("3*b^^^2 / (4*a^^^2 - 8*a*b + 4*b^^^2) / " ^
1.1233 + "(a / (a^^^2*b - b^^^3) + (a - b) / (4*a*b^^^2 + 4*b^^^3) - 1 / (4*b^^^2))");
1.1234 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.1235 +if term2str t = "-3 * b ^^^ 3 / (-2 * a + 2 * b)"
1.1236 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
1.1237
1.1238 -(*----------------------------------------------------------------------*)
1.1239 -(*---------------------- Mehrfache Dppelbrueche ------------------------*)
1.1240 -(*----------------------------------------------------------------------*)
1.1241 -
1.1242 -(*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1.1243 -(*WN060419 crashes with method 'simplify' ????SK*)
1.1244 -val t = str2term
1.1245 -"((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
1.1246 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1247 -if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1.1248 -else error "rational.sml: diff.behav. in norm_Rational_mg 49";
1.1249 -
1.1250 -"----- Schalk I, p.70 Nr. 477a";
1.1251 -(* MG Achtung: terme explodieren; Bsp zu komplex;
1.1252 - L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.1253 -val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /" ^
1.1254 - "(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1.1255 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1256 -
1.1257 -
1.1258 -val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / " ^
1.1259 - "((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1.1260 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.1261 -????SK ???MG*)
1.1262 -
1.1263 -
1.1264 -"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1.1265 -val t = str2term ("(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
1.1266 - "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
1.1267 -val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1268 -if term2str t' =
1.1269 -"(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.1270 -then ()
1.1271 -else error "rational.sml: diff.behav. in norm_Rational_mg 51";
1.1272 -
1.1273 -(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1.1274 -if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) * (a + -1 * b))" then ()
1.1275 -else error "rational.sml: works again";
1.1276 -re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1.1277 -
1.1278 -
1.1279 -
1.1280 -(*Schalk I, p.70 Nr. 480a *)
1.1281 -(* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
1.1282 -val t = str2term
1.1283 -"(1/x+1/y+1/z)/(1/x - 1/y - 1/z) / (2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z)))";
1.1284 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1285 -term2str t;
1.1286 -if (term2str t) =
1.1287 -
1.1288 -then ()
1.1289 -else error "rational.sml: diff.behav. in norm_Rational_mg 52";
1.1290 -
1.1291 -(*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
1.1292 -val t = str2term
1.1293 -"(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1.1294 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1295 -term2str t;
1.1296 -"(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
1.1297 -(-1 * x ^^^ 2 * y ^^^ 2 * z + -1 * x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2)";
1.1298 -val t = str2term
1.1299 -"2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
1.1300 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1301 -term2str t;
1.1302 -"1"
1.1303 -
1.1304 -(* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
1.1305 -### rls: cancel_p on:
1.1306 -(x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1.1307 -(-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1.1308 -GC #3.61.81.101.197.17503: (0 ms)
1.1309 -*** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
1.1310 -
1.1311 -val t = str2term
1.1312 -"(x^^^2 * (y^^^2 * z) + x^^^2 * (y * z^^^2) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y^^^2 * z)) + -1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.1313 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1314 -term2str t;
1.1315 -(*uncaught exception nonexhaustive binding failure*)
1.1316 -
1.1317 -(* Das kann er aber krzen !!????: *)
1.1318 -val t = str2term
1.1319 -"(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.1320 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1321 -term2str t;
1.1322 -"(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1.1323 -*)
1.1324 -
1.1325 -
1.1326 -"-------- crucial examples ------------------------------";
1.1327 -"-------- crucial examples ------------------------------";
1.1328 -"-------- crucial examples ------------------------------";
1.1329 -(*Schalk I, p.60 Nr. 215d *)
1.1330 -(* Achtung: rechnet ewig ...
1.1331 -val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.1332 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1333 -term2str t; noterm.SK
1.1334 -*)
1.1335 -
1.1336 -(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
1.1337 -(*
1.1338 -val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1.1339 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1340 -term2str t;
1.1341 -"a^^^3 * x^^^4 + 4 * a^^^3 * x^^^3 * y +6 * a^^^3 * x^^^2 * y^^^2 +4 * a^^^3 * x * y^^^3 +a^^^3 * y^^^4 +-3 * a^^^2 * b * x^^^4 +-12 * a^^^2 * b * x^^^3 * y +-18 * a^^^2 * b * x^^^2 * y^^^2 +-12 * a^^^2 * b * x * y^^^3 +-3 * a^^^2 * b * y^^^4 +3 * a * b^^^2 * x^^^4 +12 * a * b^^^2 * x^^^3 * y +18 * a * b^^^2 * x^^^2 * y^^^2 +12 * a * b^^^2 * x * y^^^3 +3 * a * b^^^2 * y^^^4 +-1 * b^^^3 * x^^^4 +-4 * b^^^3 * x^^^3 * y +-6 * b^^^3 * x^^^2 * y^^^2 +-4 * b^^^3 * x * y^^^3 +-1 * b^^^3 * y^^^4";
1.1342 -val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1.1343 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1344 -term2str t;
1.1345 -"a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +-5 * a^^^4 * b * x^^^2 +-10 * a^^^4 * b * x * y +-5 * a^^^4 * b * y^^^2 +10 * a^^^3 * b^^^2 * x^^^2 +20 * a^^^3 * b^^^2 * x * y +10 * a^^^3 * b^^^2 * y^^^2 +-10 * a^^^2 * b^^^3 * x^^^2 +-20 * a^^^2 * b^^^3 * x * y +-10 * a^^^2 * b^^^3 * y^^^2 +5 * a * b^^^4 * x^^^2 +10 * a * b^^^4 * x * y +5 * a * b^^^4 * y^^^2 +-1 * b^^^5 * x^^^2 +-2 * b^^^5 * x * y +-1 * b^^^5 * y^^^2";
1.1346 -*)
1.1347 -(*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1.1348 -
1.1349 -(*--------------------------------------------------------------------*)
1.1350 -(*Schalk I, p.70 Nr. 480b
1.1351 -val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.1352 - "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.1353 - "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.1354 - "(20*x*y/(x^^^2 - 25*y^^^2))";
1.1355 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1356 -SK.nonterm
1.1357 -Kann nicht weiter vereinfacht werden !!!!?? *)
1.1358 -
1.1359 -(*--------------------------------------------------------------------*)
1.1360 -"---- MGs test set";
1.1361 -val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1.1362 -val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
1.1363 -if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
1.1364 -else error "";
1.1365 -
1.1366 -(*--------------------------------------------------------------------*)
1.1367 -(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1.1368 - ---> Sortierung FALSCH !! *)
1.1369 -val t = str2term "b^^^3 * a^^^5/a ";
1.1370 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1371 -term2str t;
1.1372 -"1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1.1373 -
1.1374 -val t = str2term "b^^^3 * a^^^5/b ";
1.1375 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1376 -term2str t;
1.1377 -"1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1.1378 -
1.1379 -(* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
1.1380 -(*
1.1381 -val x = str2term "x"; val bdv = str2term "bdv";
1.1382 -val t1 = str2term "b^^^2 * a^^^5";
1.1383 -val t2 = str2term "a^^^5 * b^^^2 ";
1.1384 -ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
1.1385 -*)
1.1386 -(* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1.1387 -
1.1388 -(*--------------------------------------------------------------------*)
1.1389 -(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1.1390 - ---> erzeugt berflssige "1 * ..."
1.1391 -
1.1392 -val t = str2term "-1 / (3 + y)";
1.1393 -(*~~ *)
1.1394 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1395 -term2str t;
1.1396 -"-1 / (3 + 1 * y)";
1.1397 -(********* Das ist das PROBLEM !!!!!!!??? *******************)
1.1398 -(* -1 im Z???ler der Angabe verursacht das Problem !*)
1.1399 -*)
1.1400 -
1.1401 -(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1.1402 -"----- MGs test set";
1.1403 -val t = str2term "(a^^^2 + -1)/(a+1)";
1.1404 -val SOME (t',_) = rewrite_set_ thy false cancel_p t;
1.1405 -if term2str t' = "(-1 + a) / 1" then ()
1.1406 -else error "rational.sml MG tests 3d";
1.1407 -
1.1408 -"----- NOT TERMINATING ?: worked before 0707xx";
1.1409 -val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.1410 -val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
1.1411 -if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
1.1412 -else error "rational.sml MG tests 3e";
1.1413 -
1.1414 -"----- corrected SK060905";
1.1415 -val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1.1416 -val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1417 -if term2str t' = "-1 / (5 + -2 * x)" then ()
1.1418 -else error "rational.sml corrected SK060905";
1.1419 -
1.1420 -
1.1421 -"-------- examples for Stefan Karnels thesis ------------";
1.1422 -"-------- examples for Stefan Karnels thesis ------------";
1.1423 -"-------- examples for Stefan Karnels thesis ------------";
1.1424 -(*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1.1425 -val t = str2term
1.1426 -"(15*a^^^4/(a*x^^^3) - 5*a*((b^^^4 - 5*c^^^2*x)/x^^^2))*(x^^^3/(5*a*b^^^3*c^^^3)) + a/c^^^3 * (x*(b/a) - 3*b*(a/b^^^4))";
1.1427 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1428 -term2str t;
1.1429 -if (term2str t) =
1.1430 -"5 * x ^^^ 2 / (b ^^^ 3 * c)"
1.1431 -then ()
1.1432 -else error "rational.sml: diff.behav. in norm_Rational_mg 53";
1.1433 -
1.1434 -
1.1435 -"-------- me Schalk I No.186 ----------------------------";
1.1436 -"-------- me Schalk I No.186 ----------------------------";
1.1437 -"-------- me Schalk I No.186 ----------------------------";
1.1438 -val fmz = ["Term ((14 * x * y) / ( x * y ))",
1.1439 - "normalform N"];
1.1440 +"-------- me Schalk I No.186 -------------------------------------------------";
1.1441 +"-------- me Schalk I No.186 -------------------------------------------------";
1.1442 +"-------- me Schalk I No.186 -------------------------------------------------";
1.1443 +val fmz = ["Term ((14 * x * y) / ( x * y ))", "normalform N"];
1.1444 val (dI',pI',mI') =
1.1445 ("Rational",["rational","simplification"],
1.1446 ["simplification","of_rationals"]);
1.1447 @@ -1627,90 +1438,150 @@
1.1448 ("14", ("End_Proof'", _)) => ()
1.1449 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
1.1450
1.1451 -
1.1452 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1.1453 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1.1454 -"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1.1455 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.1456 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.1457 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1.1458 states:=[];
1.1459 -CalcTree
1.1460 -[(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1.1461 - ("Rational",["rational","simplification"],
1.1462 - ["simplification","of_rationals"]))];
1.1463 +CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1.1464 + ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.1465 Iterator 1;
1.1466 moveActiveRoot 1;
1.1467 autoCalculate 1 CompleteCalc;
1.1468 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1469 +val ((pt, p), _) = get_calc 1;
1.1470 +(*
1.1471 +show_pt pt;
1.1472 +[
1.1473 +(([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1.1474 +(([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.1475 +(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.1476 +(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1.1477 +(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1.1478 +(([4], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)),
1.1479 +(([], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2))]
1.1480 +*)
1.1481 +interSteps 1 ([1], Res);
1.1482 +val ((pt, p), _) = get_calc 1;
1.1483 +(*show_pt pt;
1.1484 +[
1.1485 +(([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1.1486 +(([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.1487 +(([1,1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1.1488 +(([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.1489 +(([1,2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.1490 +(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1.1491 +(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1.1492 +(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1.1493 +(([4], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)),
1.1494 +(([], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2))]
1.1495 +*)
1.1496 +val (t, asm) = get_obj g_result pt [1, 1];
1.1497 +if term2str t = "(2 - x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso terms2str asm = "[]"
1.1498 +then () else error "2nd interSteps ..Simp_Rat_Double_No-1 changed on [1, 1]";
1.1499 +val (t, asm) = get_obj g_result pt [1, 2];
1.1500 +if term2str t = "(2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso terms2str asm = "[]"
1.1501 +then () else error "3rd interSteps ..Simp_Rat_Double_No-1 changed on [1, 2]";
1.1502
1.1503 -interSteps 1 ([1],Res);
1.1504 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1505
1.1506 -
1.1507 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1.1508 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1.1509 -"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1.1510 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.1511 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.1512 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1.1513 states:=[];
1.1514 -CalcTree
1.1515 -[(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1.1516 - ("Rational",["rational","simplification"],
1.1517 - ["simplification","of_rationals"]))];
1.1518 +CalcTree [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1.1519 + ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.1520 Iterator 1;
1.1521 moveActiveRoot 1;
1.1522 autoCalculate 1 CompleteCalc;
1.1523 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1524 -(*========== inhibit exn 110314 ================================================
1.1525 -(*with explicit script done already... and removed [1,..] at below...
1.1526 -interSteps 1 ([1],Res);
1.1527 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1528 +val ((pt, p), _) = get_calc 1;
1.1529 +(*show_pt pt;
1.1530 +[
1.1531 +(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
1.1532 +(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
1.1533 +(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1534 +(([2], Res), (a + b) / (a + -1 * b)),
1.1535 +(([], Res), (a + b) / (a + -1 * b))]
1.1536 *)
1.1537 -interSteps 1 ([2],Res);
1.1538 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1539 -
1.1540 +interSteps 1 ([2], Res);
1.1541 +val ((pt, p), _) = get_calc 1;
1.1542 +(*show_pt pt;
1.1543 +[
1.1544 +(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
1.1545 +(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
1.1546 +(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1547 +(([2,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1548 +(([2,1], Res), (a + b) / (a + -1 * b)),
1.1549 +(([2], Res), (a + b) / (a + -1 * b)),
1.1550 +(([], Res), (a + b) / (a + -1 * b))]
1.1551 +*)
1.1552 interSteps 1 ([2,1],Res);
1.1553 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1554 +val ((pt, p), _) = get_calc 1;
1.1555 +(*show_pt pt;
1.1556 +[
1.1557 +(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
1.1558 +(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
1.1559 +(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1560 +(([2,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1561 +(([2,1,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
1.1562 +(([2,1,1], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
1.1563 +(a ^^^ 2 + -2 * (a * b) + 1 * b ^^^ 2)),
1.1564 +(([2,1,2], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
1.1565 +(a ^^^ 2 + -2 * (a * b) + -1 ^^^ 2 * b ^^^ 2)),
1.1566 +(([2,1,3], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
1.1567 +(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
1.1568 +(([2,1,4], Res), (a * a + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
1.1569 +(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
1.1570 +(([2,1,5], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1.1571 +(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
1.1572 +(([2,1,6], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1.1573 +(a ^^^ 2 + -1 * (2 * (a * b)) + (-1 * b) ^^^ 2)),
1.1574 +(([2,1,7], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1.1575 +(a ^^^ 2 + 2 * (a * (-1 * b)) + (-1 * b) ^^^ 2)),
1.1576 +(([2,1,8], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1.1577 +(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
1.1578 +(([2,1,9], Res), (a * (a + -1 * b) + (b * a + b * (-1 * b))) /
1.1579 +(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
1.1580 +(([2,1,10], Res), (a * (a + -1 * b) + b * (a + -1 * b)) /
1.1581 +(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
1.1582 +(([2,1,11], Res), (a + b) * (a + -1 * b) / (a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
1.1583 +(([2,1,12], Res), (a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))),
1.1584 +(([2,1,13], Res), (a + b) / (a + -1 * b)),
1.1585 +(([2,1], Res), (a + b) / (a + -1 * b)),
1.1586 +(([2], Res), (a + b) / (a + -1 * b)),
1.1587 +(([], Res), (a + b) / (a + -1 * b))]
1.1588 +*)
1.1589 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1.1590 -(*if length newnds = 12 then () WN060905*)
1.1591 -if length newnds = 13 then ()
1.1592 -else error "rational.sml: interSteps cancel_p rev_rew_p";
1.1593 +if length newnds = 13 then () else error "rational.sml: interSteps cancel_p rev_rew_p";
1.1594
1.1595 val p = ([2,1,9],Res);
1.1596 getTactic 1 p;
1.1597 val (_, tac, _) = pt_extract (pt, p);
1.1598 -(*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
1.1599 -WN060905*)
1.1600 -case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
1.1601 +case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
1.1602 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
1.1603 -============ inhibit exn 110314 ==============================================*)
1.1604
1.1605
1.1606 -"-------- investigate rulesets for cancel_p -------------";
1.1607 -"-------- investigate rulesets for cancel_p -------------";
1.1608 -"-------- investigate rulesets for cancel_p -------------";
1.1609 +"-------- investigate rulesets for cancel_p ----------------------------------";
1.1610 +"-------- investigate rulesets for cancel_p ----------------------------------";
1.1611 +"-------- investigate rulesets for cancel_p ----------------------------------";
1.1612 val thy = @{theory "Rational"};
1.1613 -"---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1.1614 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1.1615 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1.1616 +
1.1617 "----- with rewrite_set_";
1.1618 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.1619 -term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
1.1620 +if term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" then () else error "rls chancel_p 1";
1.1621 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1.1622 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.1623 -term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
1.1624 +if term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" then () else error "rls chancel_p 2";
1.1625
1.1626 -"----- with make_deriv";
1.1627 -val SOME (tt, _) = factout_p_ thy t; term2str tt =
1.1628 -"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
1.1629 -(*
1.1630 -"--- with ruleset as before 060829";
1.1631 -val {rules, rew_ord=(_,ro),...} =
1.1632 - rep_rls (assoc_rls "make_polynomial");
1.1633 +"----- with make_deriv; WN1130912 not investigated further, will be discontinued";
1.1634 +val SOME (tt, _) = factout_p_ thy t;
1.1635 +if term2str tt = "(a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))"
1.1636 +then () else error "rls chancel_p 3";
1.1637 +term2str tt = "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
1.1638 +
1.1639 +"--- with simpler ruleset";
1.1640 +val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p");
1.1641 val der = make_deriv thy Atools_erls rules ro NONE tt;
1.1642 -print_depth 99; map (term2str o #1) der; print_depth 3;
1.1643 -print_depth 99; map (rule2str o #2) der; print_depth 3;
1.1644 -... did not terminate*)
1.1645 -"--- with simpler ruleset";
1.1646 -val {rules, rew_ord=(_,ro),...} =
1.1647 - rep_rls (assoc_rls "rev_rew_p");
1.1648 -val der = make_deriv thy Atools_erls rules ro NONE tt;
1.1649 +if length der = 12 then () else error "WN1130912 rls chancel_p 4";
1.1650 print_depth 99; writeln (deriv2str der); print_depth 3;
1.1651
1.1652 print_depth 99; map (term2str o #1) der; print_depth 3;
1.1653 @@ -1719,305 +1590,52 @@
1.1654 print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
1.1655
1.1656 val der = make_deriv thy Atools_erls rules ro NONE
1.1657 - (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1.1658 + (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1.1659 print_depth 99; writeln (deriv2str der); print_depth 3;
1.1660
1.1661 -val {rules, rew_ord=(_,ro),...} =
1.1662 - rep_rls (assoc_rls "rev_rew_p");
1.1663 +val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p");
1.1664 val der = make_deriv thy Atools_erls rules ro NONE
1.1665 - (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1.1666 + (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1.1667 print_depth 99; writeln (deriv2str der); print_depth 3;
1.1668 print_depth 99; map (term2str o #1) der; print_depth 3;
1.1669 (*WN060829 ...postponed*)
1.1670
1.1671
1.1672 -"-------- investigate format of factout_ and factout_p_ -";
1.1673 -"-------- investigate format of factout_ and factout_p_ -";
1.1674 -"-------- investigate format of factout_ and factout_p_ -";
1.1675 -val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
1.1676 -val (thy, eval_rls) = (@{theory "Rational"}, Atools_erls)(*see 'fun init_state'*);
1.1677 -val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
1.1678 -
1.1679 -"----- see Rational.ML, local cancel_p, fun init_state";
1.1680 -val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
1.1681 -val SOME (t',_) = factout_p_ thy t; term2str t';
1.1682 -(*
1.1683 -val rtas = reverse_deriv thy eval_rls rules ro NONE t';
1.1684 -writeln(trtas2str rst);
1.1685 -*)
1.1686 -
1.1687 -
1.1688 -"----- see Rational.ML, local cancel_p, fun init_state";
1.1689 -val t = str2term "a^^^2 / a";
1.1690 -val SOME (t',_) = factout_p_ thy t;
1.1691 -term2str t' = "a * a / (1 * a)" (*true*);
1.1692 -(*... can be canceled with
1.1693 -real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1.1694 -(* sml/ME/rewtools.sml:
1.1695 -val rtas = reverse_deriv thy Atools_erls rules ro NONE t';
1.1696 -writeln (deri2str rtas);
1.1697 -*)
1.1698 -
1.1699 -
1.1700 -"-------- SK 060904 ----------------------------------------------";
1.1701 -"----- order on polynomials -- input + output";
1.1702 -val thy = @{theory "Isac"};
1.1703 -val t = str2term "(a + -1 * b) / (-1 * a + b)";
1.1704 -val SOME (t', _) = factout_p_ thy t; term2str t';
1.1705 -val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1706 -
1.1707 -val t = str2term "a*b*c*d / (d*e*f*g)";
1.1708 -val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1709 -
1.1710 -val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
1.1711 -val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1712 -(*???order.SK ???*)
1.1713 -
1.1714 -"----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
1.1715 -val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1.1716 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1717 -if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
1.1718 -else error "rational.sml SK060904-1a worked since 0707xx";
1.1719 -
1.1720 -"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1.1721 -val t = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
1.1722 -"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
1.1723 -val SOME (t',_) = cancel_p_ thy t;
1.1724 -if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.1725 -else error "rational.sml SK060904-1b";
1.1726 -
1.1727 -
1.1728 -"----- SK060904-2a non-termination of add_fraction_p_";
1.1729 -val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1.1730 - " (-1 * a + b * x) / (a + b * x) ");
1.1731 -(* nonterm.SK
1.1732 -val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1.1733 -
1.1734 -common_nominator_p_ thy t;
1.1735 -" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + " ^
1.1736 -" (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1.1737 -
1.1738 -add_fraction_p_ thy t;
1.1739 -" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
1.1740 -" ((a + b * x)*(-1 * a + b * x)) ";
1.1741 -*)
1.1742 -
1.1743 -
1.1744 -"-------- how to stepwise construct Scripts -------------";
1.1745 -"-------- how to stepwise construct Scripts -------------";
1.1746 -"-------- how to stepwise construct Scripts -------------";
1.1747 -val thy = @{theory "Rational"};
1.1748 -(*no trailing _*)
1.1749 -val p1 = parse thy (
1.1750 -"Script SimplifyScript (t_t::real) = " ^
1.1751 -" (Rewrite_Set discard_minus False " ^
1.1752 -" t_t)");
1.1753 -
1.1754 -(*required (): (Rewrite_Set discard_minus False)*)
1.1755 -val p2 = parse thy (
1.1756 -"Script SimplifyScript (t_t::real) = " ^
1.1757 -" (Rewrite_Set discard_minus False " ^
1.1758 -" t_t)");
1.1759 -
1.1760 -val p3 = parse thy (
1.1761 -"Script SimplifyScript (t_t::real) = " ^
1.1762 -" ((Rewrite_Set discard_minus False) " ^
1.1763 -" t_t)");
1.1764 -
1.1765 -val p4 = parse thy (
1.1766 -"Script SimplifyScript (t_t::real) = " ^
1.1767 -" ((Rewrite_Set discard_minus False) " ^
1.1768 -" t_t)");
1.1769 -
1.1770 -val p5 = parse thy (
1.1771 -"Script SimplifyScript (t_t::real) = " ^
1.1772 -" ((Try (Rewrite_Set discard_minus False) " ^
1.1773 -" Try (Rewrite_Set discard_parentheses False)) " ^
1.1774 -" t_t)");
1.1775 -
1.1776 -val p6 = parse thy (
1.1777 -"Script SimplifyScript (t_t::real) = " ^
1.1778 -" ((Try (Rewrite_Set discard_minus False) @@ " ^
1.1779 -" Try (Rewrite_Set rat_mult_poly False) @@ " ^
1.1780 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
1.1781 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
1.1782 -" (Repeat " ^
1.1783 -" ((Try (Rewrite_Set common_nominator_p_rls False) @@ " ^
1.1784 -" Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
1.1785 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
1.1786 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
1.1787 -" Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
1.1788 -" Try (Rewrite_Set discard_parentheses False)) " ^
1.1789 -" t_t)"
1.1790 -);
1.1791 -
1.1792 -"----------- get_denominator ----------------------------";
1.1793 -"----------- get_denominator ----------------------------";
1.1794 -"----------- get_denominator ----------------------------";
1.1795 +"-------- fun eval_get_denominator -------------------------------------------";
1.1796 +"-------- fun eval_get_denominator -------------------------------------------";
1.1797 +"-------- fun eval_get_denominator -------------------------------------------";
1.1798 val thy = @{theory Isac};
1.1799 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1.1800 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1.1801 -if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1.1802 -else error "get_denominator ((a + x) / b) = b"
1.1803 +if term2str t' = "get_denominator ((a + x) / b) = b"
1.1804 +then () else error "get_denominator ((a + x) / b) = b"
1.1805
1.1806
1.1807 -"--------- several errpats in complicated term -------------------";
1.1808 -"--------- several errpats in complicated term -------------------";
1.1809 -"--------- several errpats in complicated term -------------------";
1.1810 -(*TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one*)
1.1811 -states:=[];
1.1812 -CalcTree
1.1813 -[(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
1.1814 - ("Rational",["rational","simplification"], ["simplification","of_rationals"]))];
1.1815 +"-------- several errpats in complicated term --------------------------------";
1.1816 +"-------- several errpats in complicated term --------------------------------";
1.1817 +"-------- several errpats in complicated term --------------------------------";
1.1818 +(*WN12xxxx TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one
1.1819 + WN130912: kept this test, although not clear what for*)
1.1820 +states := [];
1.1821 +CalcTree [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
1.1822 + ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.1823 Iterator 1;
1.1824 moveActiveRoot 1;
1.1825 autoCalculate 1 CompleteCalc;
1.1826 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1827 +val ((pt, p), _) = get_calc 1;
1.1828 +(*show_pt pt;
1.1829 +[
1.1830 +(([], Frm), Simplify ((5 * b + 25) / (a ^^^ 2 - b ^^^ 2) * (a - b) / (5 * b))),
1.1831 +(([1], Frm), (5 * b + 25) / (a ^^^ 2 - b ^^^ 2) * (a - b) / (5 * b)),
1.1832 +(([1], Res), (5 * b + 25) / (a ^^^ 2 + -1 * b ^^^ 2) * (a + -1 * b) / (5 * b)),
1.1833 +(([2], Res), (5 * b + 25) * (a + -1 * b) / (a ^^^ 2 + -1 * b ^^^ 2) / (5 * b)),
1.1834 +(([3], Res), (25 * a + -25 * b + 5 * (a * b) + -5 * b ^^^ 2) / (a ^^^ 2 + -1 * b ^^^ 2) /
1.1835 +(5 * b)),
1.1836 +(([4], Res), (25 + 5 * b) / (a + b) / (5 * b)),
1.1837 +(([5], Res), (25 + 5 * b) / ((a + b) * (5 * b))),
1.1838 +(([6], Res), (25 + 5 * b) / (5 * (a * b) + 5 * b ^^^ 2)),
1.1839 +(([7], Res), (5 + b) / (a * b + b ^^^ 2)),
1.1840 +(([], Res), (5 + b) / (a * b + b ^^^ 2))] *)
1.1841
1.1842 -"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.1843 -"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.1844 -"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.1845 -(*------------------------------------------------------------------------------------\
1.1846 -"--- WN121204: searched rational.sml for "nonterm", added new numbering" ^
1.1847 -" and thoroughly tested with this numbering subsequently";
1.1848 -"--- 1 ---";
1.1849 -WN.2.6.03 from rlang.sml 56a
1.1850 -val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.1851 -val NONE = rewrite_set_ thy false common_nominator_p t;
1.1852 -"--- 2 ---";
1.1853 -WN060831 nonterm.SK7
1.1854 -val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.1855 -val NONE = add_fraction_p_ thy t;
1.1856 -"--- 3 ---";
1.1857 -nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1.1858 -val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.1859 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1.1860 -"--- 4 ---";
1.1861 -val t = str2term
1.1862 -"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.1863 -WN060831 nonterm.SK10
1.1864 -val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1865 -term2str t;
1.1866 -"--- 5 ---";
1.1867 -val t = str2term
1.1868 -"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.1869 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1870 -if term2str t =
1.1871 -then ()
1.1872 -else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1.1873 -"--- 6 ---";
1.1874 -val t = str2term
1.1875 -"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.1876 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1877 -... non terminating.
1.1878 -"--- 7 ---";
1.1879 -val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.1880 -"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.1881 -val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1.1882 -"--- 8 ---";
1.1883 -val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.1884 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1885 -"--- 9 ---";
1.1886 -val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.1887 - "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.1888 - "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.1889 - "(20*x*y/(x^^^2 - 25*y^^^2))";
1.1890 -val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1891 -"--- 10 ---";
1.1892 -SK060904-2a non-termination of add_fraction_p_";
1.1893 -val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1.1894 - " (-1 * a + b * x) / (a + b * x) ");
1.1895 -(* nonterm.SK = WN130830
1.1896 -val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1.1897 -"--- 11 ---";
1.1898 -common_nominator_p_ thy t;
1.1899 -" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + " ^
1.1900 -" (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1.1901 -"--- 12 ---";
1.1902 -add_fraction_p_ thy t;
1.1903 -" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
1.1904 -" ((a + b * x)*(-1 * a + b * x)) ";
1.1905 ---------------------------------------------------------------------------------------/*)
1.1906
1.1907 -(*------------------------------------------------------------------------------------\
1.1908 -"WN121205: thoroughly tested with the above numbering.";
1.1909 -" errors in cancel_p: --- 4,5,6,7.";
1.1910 -" error in common_nominator_p, common_nominator_p_: --- 10; 1,2?.";
1.1911 -" errors caused by ruleset norm_Rational: --- 8,9.";
1.1912 -trace_rewrite := false;
1.1913
1.1914 -"--- 1 ---: non-terminating with ### add_fract: done t22 "; = WN130830
1.1915 -val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.1916 -trace_rewrite := false;
1.1917 -rewrite_set_ thy false common_nominator_p t;
1.1918 -
1.1919 -"--- 2 ---: non-terminating with ### add_fract: done t22 ";
1.1920 -val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.1921 -add_fraction_p_ thy t;
1.1922 -
1.1923 -"--- 3 ---: norm_Rational calls Rrls cancel_p with non-normalised polys";
1.1924 -val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.1925 -rewrite_set_ thy false norm_Rational t;
1.1926 -(*tracing end...#### rls: cancel_p on:
1.1927 -(a * x ^^^ 2 + -2 * (a * (x * y)) + a * y ^^^ 2 + b * x ^^^ 2 + -2 * (b * (x * y)) + b * y ^^^ 2) /
1.1928 -(a ^^^ 2 * x ^^^ 2 + -1 * (a ^^^ 2 * y ^^^ 2) + -1 * (b ^^^ 2 * x ^^^ 2) + b ^^^ 2 * y ^^^ 2) *)
1.1929 -
1.1930 -"--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
1.1931 -val t = str2term (
1.1932 -"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /"^
1.1933 -"(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)");
1.1934 -rewrite_set_ thy false cancel_p t;
1.1935 -(*# rls: cancel_p on:
1.1936 -(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /
1.1937 -(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2) *)
1.1938 -
1.1939 -"--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
1.1940 -val t = str2term "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.1941 -rewrite_set_ thy false norm_Rational t;
1.1942 -(*#### rls: cancel_p on:
1.1943 -(2304 + -1152 * x + -2304 * y + 144 * x ^^^ 2 + 1152 * (x * y) + -144 * (x ^^^ 2 * y)) /
1.1944 -(48 + -12 * x + -96 * y + 24 * (x * y) + 48 * y ^^^ 2 + -12 * (x * y ^^^ 2)) *)
1.1945 -
1.1946 -"--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
1.1947 -val t = str2term
1.1948 -"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.1949 -rewrite_set_ thy false norm_Rational t;
1.1950 -(*### rls: cancel_p on: (-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * (x * y) +
1.1951 - 144 * (x ^^^ 2 * y)) /
1.1952 -(-48 + 12 * x + 96 * y + -24 * (x * y) + -48 * y ^^^ 2 + 12 * (x * y ^^^ 2)) *)
1.1953 -
1.1954 -"--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
1.1955 -val t' = str2term (
1.1956 -"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /"^
1.1957 -"(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)");
1.1958 -rewrite_set_ thy false cancel_p t';
1.1959 -
1.1960 -"--- 8 ---: bottom of output cannot be looked ad (due to looping?)";
1.1961 -val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.1962 -val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1963 -
1.1964 -"--- 9 ---: probably error in norm_Rational";
1.1965 -val t = str2term (
1.1966 -"((12*x*y / (9*x^^^2 - y^^^2)) / (1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.1967 - "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y/(x^^^2 - 25*y^^^2))");
1.1968 -rewrite_set_ thy false norm_Rational t;
1.1969 -(*#### rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +
1.1970 - 108240 * (x ^^^ 4 * y ^^^ 6) +
1.1971 - -6000 * (x ^^^ 2 * y ^^^ 8)) /
1.1972 -(2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +
1.1973 - 1362000 * (x ^^^ 4 * y ^^^ 6) +
1.1974 - -150000 * (x ^^^ 2 * y ^^^ 8)) *)
1.1975 -
1.1976 -"--- 10 ---: non-terminating with ### add_fract: done t22: error in common_nominator_p ";
1.1977 -val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)");
1.1978 -rewrite_set_ thy false common_nominator_p t; (*### add_fract: done t22 *)
1.1979 -common_nominator_p_ thy t; (*loops without output*)
1.1980 -"--- reformulated 10:";
1.1981 -val t = str2term "(a + -1 * (b * x)) / (a + b * x)";
1.1982 -rewrite_set_ thy false cancel_p t = NONE;
1.1983 -"--- 11 ---";
1.1984 -"--- 12 ---";
1.1985 -"...both are to be considered after common_nominator_p_ is improved";
1.1986 ---------------------------------------------------------------------------------------/*)
1.1987 -============ inhibit exn WN130824 TODO ======================================================*)
1.1988 -