wneuper/isa: comparison test/Tools/isac/Knowledge/rational.sml

equal deleted inserted replaced

-:83166e7c7e52
+:2786cc9704c8
 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
+"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
-"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
+"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
-"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
+"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
 "-------- reverse rewrite ----------------------------------------------------";
 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
 "-------- investigate rls norm_Rational --------------------------------------";
 "-------- examples: rls norm_Rational ----------------------------------------";
-"-------- numeral rationals -----------------------------";
+"-------- rational numerals --------------------------------------------------";
-"-------- cancellation ----------------------------------";
+"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
-"-------- common denominator ----------------------------";
+"-------- examples common denominator from: Mathematik 1 Schalk --------------";
-"-------- multiply and cancel ---------------------------";
+"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
-"-------- common denominator and multiplication ---------";
+"-------- examples common denominator and multiplication from: Schalk --------";
-"-------- double fractions ------------------------------";
+"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
-"-------- crucial examples ------------------------------";
+"-------- me Schalk I No.186 -------------------------------------------------";
-"-------- examples for Stefan Karnels thesis ------------";
+"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
-"-------- me Schalk I No.186 ----------------------------";
+"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
-"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
+"-------- investigate rulesets for cancel_p ----------------------------------";
-"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
+"-------- fun eval_get_denominator -------------------------------------------";
-"-------- investigate rulesets for cancel_p -------------";
+"-------- several errpats in complicated term --------------------------------";
-"-------- investigate format of factout_ and factout_p_ -";
+"-----------------------------------------------------------------------------";
-"-------- how to stepwise construct Scripts -------------";
+"-----------------------------------------------------------------------------";
-"----------- get_denominator ----------------------------";
-"--------- several errpats in complicated term -------------------";
-"--------------------------------------------------------";
-"-------- nonterminating cancel_p, norm_Rational 2002 ---";
-"--------------------------------------------------------";
-"--------------------------------------------------------";
 "-------- fun poly_of_term ---------------------------------------------------";
 "-------- fun poly_of_term ---------------------------------------------------";
 "-------- fun poly_of_term ---------------------------------------------------";
 if f pp then true else scan_ f pps;
 in scan_ chk prepat end;
 (* apply the normal_form of a rev-set *)
 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
 if chk_prepat thy erls prepat t
-then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
+then ((*tracing("### app_rev': t = "^term2str t);*) normal_form t)
 else NONE;
 (*  val opt = app_rev' thy rrls t  ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
 (thy, rrls, t);
 (* chk_prepat thy erls prepat t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
 val ((a', b'), c) = gcd_poly a b
 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
 *)
+"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
+"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
+"-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
+val thy =  @{theory Isac};
+"----- SK060904-2a non-termination of add_fraction_p_";
+val t = str2term (" (a + b * x) / (a + -1 * (b * x)) +  " ^
+		         " (-1 * a + b * x) / (a + b * x)      ");
+(* rewrite_set_ thy false norm_Rational t
+exception Div raised*)
+(* rewrite_set_ thy false add_fractions_p t;
+exception Div raised*)
+"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) =
+(@{theory Isac}, false, add_fractions_p, t);
+"~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
+(thy, 1, bool, [], rls, term);
+(* app_rev thy (i+1) rrls t;
+exception Div raised*)
+"~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
+fun chk_prepat thy erls [] t = true
+| chk_prepat thy erls prepat t =
+let
+fun chk (pres, pat) =
+(let
+val subst: Type.tyenv * Envir.tenv =
+Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
+in
+snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
+end) handle _ => false
+fun scan_ f [] = false (*scan_ NEVER called by []*)
+| scan_ f (pp::pps) =
+if f pp then true else scan_ f pps;
+in scan_ chk prepat end;
+(* apply the normal_form of a rev-set *)
+fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
+if chk_prepat thy erls prepat t
+then ((*tracing("### app_rev': t = "^term2str t);*) normal_form t)
+else NONE;
+(*  val opt = app_rev' thy rrls t;
+exception Div raised*)
+(*  val opt = app_rev' thy rrls t;
+exception Div raised*)
+"~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
+(thy, rrls, t);
+chk_prepat thy erls prepat t = true       = true;
+(*normal_form t
+exception Div raised*)
+(* lookup Rational.thy, val add_fractions_p: normal_form = add_fraction_p_ thy*)
+(*add_fraction_p_ thy t
+exception Div raised*)
+"~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t);
+val SOME ((n1, d1), (n2, d2)) = check_frac_sum t;
+term2str n1; term2str d1; term2str n2; term2str d2;
+val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+|> filter is_some |> map the |> sort string_ord;
+print_depth 3; (*999*)
+val (SOME _, SOME a, SOME _, SOME b) =
+(poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
+print_depth 3; (*999*)
+(*
+val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly
+val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly
+val ((a', b'), c) = gcd_poly a b
+*)
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 val thy  = @{theory "Rational"};
 "-------- WN";
 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
 if (term2str t', terms2str asm) = ("8 / 9", "[]")
 then () else error "rational.sml cancel Schalk 188a";
 val t = str2term "(8*((-1) + x))/(9*((-1) + x))";
-val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
+val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 if (term2str t', terms2str asm) = ("8 / 9", "[]")
 then () else error "rational.sml cancel Schalk make_polynomial 1";
 "-------- example 188b";
 val t = str2term "(-15 + 5 * x) / (-18 + 6 * x)";
 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
 if (term2str t', terms2str asm) =
 ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]")
 then () else error "rational.sml cancel_p heuberger";
-"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
+"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
-"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
+"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
-"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
+"-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
 (*deleted example 204 ... 236b at update Isabelle2012-->2013*)
-"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
+"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
-"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
+"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
-"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
+"-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
 "-------- gcd_poly integration level 1: works on exact term";
 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";
 "-------- gcd_poly integration level 3: rewrites all appropriate subterms";
 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
 if term2str t' = "123 = a / b + c / d + e / f"
 then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
-val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*)
+val SOME (t', asm) = rewrite_set_ thy false add_fractions_p_rls t; (*CREATE add_fractions_p_rls*)
 if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
 "-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";
 (* simpler variant *)
 val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p]
 val SOME (t', asm) = rewrite_set_ thy false testrls t;
 (*trace_rewrite := false;
 #  rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
 ##  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
-##  rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
+##  rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
 ##  rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f
-##  rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
+##  rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
 ##  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
-##  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
+##  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
 then () else error "level 4, rewrite_set_ *_p: changed";
 (* complicated variant *)
-val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls];
+val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ add_fractions_p_rls];
 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
 (*#  rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
 ##  rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
 ###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
 ###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
 ###  rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f
 ###  rls: cancel_p on: 123 = a / b + c / d + e / f
-##  rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f
+##  rls: add_fractions_p_rls on: 123 = a / b + c / d + e / f
-###  rls: common_nominator_p on: 123 = a / b + c / d + e / f
+###  rls: add_fractions_p on: 123 = a / b + c / d + e / f
-###  rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
+###  rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
-###  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
+###  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
 ##  rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
 ###  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
-##  rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
+##  rls: add_fractions_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
-###  rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
+###  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
 then () else error "level 4, rewrite_set_ *_p_rls: changed"
 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";
 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;
 (revsets |> nth 1 |> nth 7 |> rule2str) =
 "Thm (\"sym_mult_assoc\",Groups.semigroup_mult_class.mult_assoc)"
 then () else error "first 7 elements in revset changed"
 (** find the rule 'r' to apply to term 't' **)
-(*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
+(*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
 for Isabelle2013, we don't get a working revset, but non-termination:
 val SOME (r as (Thm (str, thm))) = nex revsets t;
 :
 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
 \--------------------------------------------------------------------------------------/*)
 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
-(*Isabelle2013: the example below shows, why "reverse rewriting" only worked for
+(*WN130909: the example below shows, why "reverse rewriting" only worked for
 special cases.*)
 (*the term for which reverse rewriting is demonstrated*)
 val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
 val SOME r = nex revsets t;
 val (r,(t,asm))::_ = loc revsets t r;
 term2str t;
 *)
-(*========== inhibit exn WN130824 TODO =======================================================
 "-------- examples: rls norm_Rational ----------------------------------------";
 "-------- examples: rls norm_Rational ----------------------------------------";
 "-------- examples: rls norm_Rational ----------------------------------------";
 val t = str2term "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 if term2str t' = "65 * x / 2" then () else error "rational.sml 4";
 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-(*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
 else error "rational.sml 5";
 (*SRAM Schalk I, p.92 Nr. 609a*)
 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
 (*SRAM Schalk I, p.92 Nr. 476a*)
 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) * (1 + x)";
 (*. a/b : c/d translated to a/b * d/c .*)
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-(*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
 if term2str t' = "1" then () else error "rational.sml 8";
-(*............................vvv---TODO: sollte gehen mit poly_order *)
 (*Schalk I, p.92 Nr. 472a*)
 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
-(*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
+(*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*)
-val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
-		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
+(*WN130910 add_fractions_p exception Div raised + history:
-		 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
+### WN.2.6.03 from rlang.sml 56a
-		 "(20*x*y/(x^^^2 - 25*y^^^2))");
-(*... nicht simpl, zerlegt ...*)
-val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
-		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))");
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-"(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
-(*                             ~~~~~~~~~~ poly_order notwendig!*)
-val t = str2term ("(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
-		 "(20*x*y/(x^^^2 - 25*y^^^2))");
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-if term2str t' = "1 / (x ^^^ 2 + -25 * y ^^^ 2)" then ()
-else error "rational.sml norm_Rational 1 / (x ^^^ 2 + -25 * y ^^^ 2)";
-"nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
-(*WN.2.6.03 from rlang.sml 56a
 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)";
-val NONE = rewrite_set_ thy false common_nominator_p t;
+val NONE = rewrite_set_ thy false add_fractions_p t;
-WN060831 nonterm.SK7
+THE ERROR ALREADY OCCURS IN THIS PART:
 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
 val NONE = add_fraction_p_ thy t;
-*)
+SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised ===
+*)
-(* ------------------------------------------------------------------- *)
-(*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
+"-------- rational numerals --------------------------------------------------";
-(*                 Simplifier fuer beliebige Buchterme                 *)
+"-------- rational numerals --------------------------------------------------";
-(* ------------------------------------------------------------------- *)
+"-------- rational numerals --------------------------------------------------";
-(*----------------------- norm_Rational_mg ----------------------------*)
-(* ------------------------------------------------------------------- *)
-"-------- numeral rationals -----------------------------";
-"-------- numeral rationals -----------------------------";
-"-------- numeral rationals -----------------------------";
 (*SRA Schalk I, p.40 Nr. 164b *)
 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 term2str t;
-if (term2str t) = "19 / 21" then ()
+if term2str t = "19 / 21" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 1";
 (*SRA Schalk I, p.40 Nr. 166a *)
 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 term2str t;
-if (term2str t) = "45 / 2" then ()
+if term2str t = "45 / 2" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 2";
+"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
-"-------- cancellation ----------------------------------";
+"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
-"-------- cancellation ----------------------------------";
+"-------- examples cancellation from: Mathematik 1 Schalk --------------------";
-"-------- cancellation ----------------------------------";
 (* e190c Stefan K.*)
-val t = str2term
+val t = str2term "((1 + 9*a^^^2) * (1 + 3*a)) / ((3*a + 9*a^^^2) * (1 + 3*a))";
-"((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
+(* e192b Stefan K.*)
+val t = str2term "(x^^^2 * (7*x + (-1)*y))  /  (y^^^2 * (7*x + (-1)*y))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "x ^^^ 2 / y ^^^ 2"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
+(*SRC Schalk I, p.66 Nr. 379c *)
+val t = str2term "(a - b)/(b - a)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 term2str t;
-if (term2str t) =
+if term2str t = "-1"
-"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 3";
-(* e192b Stefan K.*)
-val t = str2term
-"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"x ^^^ 2 / y ^^^ 2"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 4";
-(*SRC Schalk I, p.66 Nr. 379c *)
-val t = str2term
-"(a - b)/(b - a)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"-1"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 5";
 (*SRC Schalk I, p.66 Nr. 380b *)
-val t = str2term
+val t = str2term "15*(3*x + 3) * (4*x + 9)  /  (12*(2*x + 7) * (5*x + 5))";
-"15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(27 + 12 * x) / (28 + 8 * x)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
-if (term2str t) =
-"(27 + 12 * x) / (28 + 8 * x)"
+(*Schalk I, p.60 Nr. 215c: was not cancelled with Isabelle2002 *)
-then ()
+val t = str2term "(a + b)^^^4 * (x - y)  /  ((x - y)^^^3 * (a + b)^^^2)";
-else error "rational.sml: diff.behav. in norm_Rational_mg 6";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
-(*Schalk I, p.60 Nr. 215c *)
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
-(* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
-(* WN060831????MG1
-val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"(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)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 7";
-*)
-(*val t = str2term
-"(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)"
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;*)
-(* uncaught exception nonexhaustive binding failure
-raised at: stdIn:93.1-93.51 *)
-(*Schalk I, p.66 Nr. 381a *)
-(* ACHTUNG: rechnet ca. 2 Minuten !!! *)
-(* WN060831???MG2
-val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"(a + b) / (4 * a + -4 * b)"
-then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
-*)
 (*SRC Schalk I, p.66 Nr. 381b *)
 val t = str2term
 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "1 / (-5 + 2 * x)"
-if (term2str t) =
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
-"-1 / (5 + -2 * x)"
-then ()
+(* e190c Stefan K.*)
-else error "rational.sml: diff.behav. in norm_Rational_mg 9";
+val t = str2term "((1 + 9*a^^^2) * (1 + 3*a))  /  ((3*a + 9*a^^^2) * (1 + 3 * a))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t =  "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
+(* e192b Stefan K.*)
+val t = str2term "(x^^^2 * (7*x + (-1)*y))  /  (y^^^2 * (7*x + (-1)*y))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "x ^^^ 2 / y ^^^ 2"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
+(*SRC Schalk I, p.66 Nr. 379c *)
+val t = str2term "(a - b) / (b - a)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "-1"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
+(*SRC Schalk I, p.66 Nr. 380b *)
+val t = str2term "15*(3*x + 3) * (4*x + 9)  /  (12*(2*x + 7) * (5*x + 5))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(27 + 12 * x) / (28 + 8 * x)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
+(*Schalk I, p.60 Nr. 215c *)
+val t = str2term "(a + b)^^^4 * (x - y)  /  ((x - y)^^^3 * (a + b)^^^2)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
+then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
+(* extreme example from somewhere *)
+val t = str2term
+("(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)")
+val SOME (t, _) = rewrite_set_ thy false cancel_p t;
+if term2str t = "(a ^^^ 2 + 2 * a * b + b ^^^ 2) / (x ^^^ 2 + -2 * x * y + y ^^^ 2)"
+then () else error "with Isabelle2002: NONE -- now SOME changed";
+(*Schalk I, p.66 Nr. 381a *)
+(* ATTENTION: here the rls is very slow. In Isabelle2002 this required 2 min *)
+val t = str2term "18*(a + b)^^^3 * (a - b)^^^2 / (72*(a - b)^^^3 * (a + b)^^^2)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(a + b) / (4 * a + -4 * b)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
+(*SRC Schalk I, p.66 Nr. 381b *)
+val t = str2term "(4*x^^^2 - 20*x + 25) / (2*x - 5)^^^3";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "1 / (-5 + 2 * x)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
 (*SRC Schalk I, p.66 Nr. 381c *)
-val t = str2term
+val t = str2term "(27*a^^^3 + 9*a^^^2+3*a+1) / (27*a^^^3 + 18*a^^^2+3*a)";
-"(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 10";
-if (term2str t) =
-"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 10";
 (*SRC Schalk I, p.66 Nr. 383a *)
-val t = str2term
+val t = str2term "(5*a^^^2 - 5*a*b) / (a - b)^^^2";
-"(5*a^^^2 - 5*a*b)/(a - b)^^^2";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "-5 * a / (-1 * a + b)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 11";
-if (term2str t) =
-"5 * a / (a + -1 * b)"
+"----- NOT TERMINATING ?: worked before 0707xx";
-then ()
+val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
-else error "rational.sml: diff.behav. in norm_Rational_mg 11";
+(* WN130911 "exception Div raised" by
+cancel_p_ thy (str2term ("(-1 + -1 * b + a ^^^ 2 + a ^^^ 2 * b) /" ^
+"(-1 + -1 * a + b ^^^ 2 + a * b ^^^ 2)"))
-"-------- common denominator ----------------------------";
-"-------- common denominator ----------------------------";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-"-------- common denominator ----------------------------";
+if term2str t = "(1 + -1 * a) / (1 + -1 * b)" then ()
+else error "rational.sml MG tests 3e";
+*)
+"-------- examples common denominator from: Mathematik 1 Schalk --------------";
+"-------- examples common denominator from: Mathematik 1 Schalk --------------";
+"-------- examples common denominator from: Mathematik 1 Schalk --------------";
 (*SRA Schalk I, p.67 Nr. 403a *)
-val t = str2term
+val t = str2term "4/x - 3/y - 1";
-"4/x - 3/y - 1";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 12";
-if (term2str t) =
-"(-3 * x + 4 * y + -1 * x * y) / (x * y)"
+val t = str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
-then ()
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-else error "rational.sml: diff.behav. in norm_Rational_mg 12";
+if term2str t = "4 / c"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 13";
-(*SRA Schalk I, p.67 Nr. 407b *)
-val t = str2term
-"(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"4 / c"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 13";
 (*SRA Schalk I, p.67 Nr. 410b *)
-val t = str2term
+val t = str2term "1/(x+1) + 1/(x+2) - 2/(x+3)";
-"1/(x+1) + 1/(x+2) - 2/(x+3)";
+(* WN130911 non-termination due to non-termination of
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+cancel_p_ thy (str2term "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)")
-term2str t;
-if (term2str t) =
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-"(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
+if term2str t = "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
-then ()
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 14";
-else error "rational.sml: diff.behav. in norm_Rational_mg 14";
+*)
 (*SRA Schalk I, p.67 Nr. 413b *)
-val t = str2term
+val t = str2term "(1 + x)/(1 - x)  -  (1 - x)/(1 + x)  +  2*x/(1 - x^^^2)";
-"(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "6 * x / (1 + -1 * x ^^^ 2)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 15";
-if (term2str t) =
-"6 * x / (1 + -1 * x ^^^ 2)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 15";
 (*SRA Schalk I, p.68 Nr. 414a *)
-val t = str2term
+val t = str2term "(x + 2)/(x - 1)  +  (x - 3)/(x - 2)  -  (x + 1)/((x - 1)*(x - 2))";
-"(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t ="(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 16";
-if (term2str t) =
-"(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 16";
-(*SRA Schalk I, p.68 Nr. 423a *)
-val t = str2term
-"(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)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"1"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 17";
 (*SRA Schalk I, p.68 Nr. 428b *)
 val t = str2term
-"1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
+"1/(a - b)^^^2  +  1/(a + b)^^^2  -  2/(a^^^2 - b^^^2)  -  4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+(* WN130911 non-termination due to non-termination of
-term2str t;
+cancel_p_ thy (str2term "(4 + -4 * b ^^^ 2) / (a ^^^ 4 + -2 * (a ^^^ 2 * b ^^^ 2) + b ^^^ 4)")
-if (term2str t) =
-"4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-then ()
+if term2str t = "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
-else error "rational.sml: diff.behav. in norm_Rational_mg 18";
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";
+*)
 (*SRA Schalk I, p.68 Nr. 430b *)
 val t = str2term
 "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";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "a + 3 * b"
-if (term2str t) =
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 19";
-"a + 3 * b"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 19";
 (*SRA Schalk I, p.68 Nr. 432 *)
 val t = str2term
-"(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)";
+("(a^^^2 + a*b) / (a^^^2 - b^^^2)  -  (b^^^2 - a*b) / (b^^^2 - a^^^2)  +  " ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"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)");
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 term2str t;
-if (term2str t) =
+if term2str t = "0"
-"0"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 20";
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 20";
+(* some example *)
+val t = str2term "3*a / (a*b)  +  x/y";
-(*Eigenes*)
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(3 * y + b * x) / (b * y)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";
+"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
+"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
+"-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
+(*------- SRM Schalk I, p.68 Nr. 436a *)
+val t = str2term "3*(x+y) / (15*(x - y))  *   25*(x - y)^^^2 / (18*(x + y)^^^2)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(-5 * x + 5 * y) / (-18 * x + -18 * y)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";
+(*------- SRM.test Schalk I, p.68 Nr. 436b *)
+val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "5 * a / (a + -1 * b)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 23";
+(*------- Schalk I, p.68 Nr. 437a *)
+val t = str2term "(3*a - 4*b) / (4*c+3*e)  *  (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
+(* raises an exception for unclear reasons:
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+:
+###  rls: cancel_p on: (9 * a ^^^ 2 + -16 * b ^^^ 2) / (4 * c + 3 * e) /
+(9 * a ^^^ 2 + -16 * b ^^^ 2)
+exception Div raised
+BUT
 val t = str2term
-"3*a/(a*b) + x/y";
+("(9 * a ^^^ 2 + -16 * b ^^^ 2) / (4 * c + 3 * e) /" ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"(9 * a ^^^ 2 + -16 * b ^^^ 2)");
-term2str t;
+NONE = cancel_p_ thy t;
-if (term2str t) =
-"(3 * y + b * x) / (b * y)"
+if term2str t = "1 / (4 * c + 3 * e)" then ()
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 21";
-"-------- multiply and cancel ---------------------------";
-"-------- multiply and cancel ---------------------------";
-"-------- multiply and cancel ---------------------------";
-(*SRM Schalk I, p.68 Nr. 436a *)
-val t = str2term
-"3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"(5 * x + -5 * y) / (18 * x + 18 * y)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 22";
-(*SRM.test Schalk I, p.68 Nr. 436b *)
-(*WN060420???MG3 crashes with method 'simplify' in
-IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
-val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"5 * a / (a + -1 * b)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 23";
-(*Schalk I, p.68 Nr. 437a *)
-val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-if (term2str t) = "1 / (4 * c + 3 * e)" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
+*)
 "----- S.K. corrected non-termination 060904";
 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
-val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
+val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
-term2str t';
+if term2str t =
-if term2str t' =
 "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"
 (*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
 then () else error "rational.sml: S.K.8..corrected 060904-6";
 "----- S.K. corrected non-termination of cancel_p_";
 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
 "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
-if term2str t' = "1 / (4 * c + 3 * e)" then ()
+if term2str t' = "1 / (4 * c + 3 * e)"
-else error "rational.sml: diff.behav. in cancel_p S.K.8";
+then () else error "rational.sml: diff.behav. in cancel_p S.K.8";
-(*Schalk I, p.68 Nr. 437b *)
+(*------- Schalk I, p.68 Nr. 437b*)
-(* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
+val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
-val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
+(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-(* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
+:
-*)
+####  rls: cancel_p on: (a * x ^^^ 2 + -2 * (a * (x * y)) + a * y ^^^ 2 + b * x ^^^ 2 +
+-2 * (b * (x * y)) +
-"================delete===";
+b * y ^^^ 2) /
-(*a casual output from above*)
+(a ^^^ 2 * x ^^^ 2 + -1 * (a ^^^ 2 * y ^^^ 2) + -1 * (b ^^^ 2 * x ^^^ 2) +
+b ^^^ 2 * y ^^^ 2)
+exception Div raised
+*)
+(*------- SRM Schalk I, p.68 Nr. 438a *)
+val t = str2term "x*y / (x*y - y^^^2)  *  (x^^^2 - x*y)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "x ^^^ 2"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 24";
+(*------- SRM Schalk I, p.68 Nr. 439b *)
+val t = str2term "(4*x^^^2 + 4*x + 1)  *  ((x^^^2 - 2*x^^^3) / (4*x^^^2 + 2*x))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(x + -4 * x ^^^ 3) / 2"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 25";
+(*------- SRM Schalk I, p.68 Nr. 440a *)
+val t = str2term "(x^^^2 - 2*x) / (x^^^2 - 3*x)  *  (x - 3)^^^2 / (x^^^2 - 4)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(-3 + x) / (2 + x)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 26";
+"----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
+val t = str2term "(a^^^3 - 9*a) / (a^^^3*b - a*b^^^3)  *  (a^^^2*b + a*b^^^2) / (a+3)";
+(* WN130911 non-termination for unclear reasons:
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+... ENDS WITH THIS TRACE:
+:
+###  rls: cancel_p on: (-9 * (a ^^^ 3 * b) + -9 * (a ^^^ 2 * b ^^^ 2) + a ^^^ 5 * b +
+a ^^^ 4 * b ^^^ 2) /
+(a ^^^ 3 * b + -1 * (a * b ^^^ 3)) /
+(3 + a)
+BUT THIS IS CORRECTLY RECOGNISED
 val t = str2term
-"(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)";
+("(-9 * (a^^^3 * b) + -9 * (a^^^2 * b^^^2) + a^^^5 * b + a^^^4 * b^^^2)  /" ^
-(* WN060831 nonterm.SK10
+"(a^^^3 * b + -1 * (a * b^^^3))  /  (3 + (a::real))");
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
+AS
-term2str t;
+NONE = cancel_p_ thy t;
-*)
-(*SRM Schalk I, p.68 Nr. 438a *)
-val t = str2term
-"x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"x ^^^ 2"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 24";
-(*SRM Schalk I, p.68 Nr. 439b *)
-val t = str2term
-"(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"(x + -4 * x ^^^ 3) / 2"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 25";
-(*SRM Schalk I, p.68 Nr. 440a *)
-val t = str2term
-"(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"(-3 + x) / (2 + x)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 26";
-"----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
-val t = str2term
-"(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
 else error "rational.sml: diff.behav. in norm_Rational 27";
+*)
 "----- SK12 works since 0707xx";
-val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
+val t = str2term "(a^^^3 - 9*a) * (a^^^2*b+a*b^^^2)  /  ((a^^^3*b - a*b^^^3) * (a+3))";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
+(* WN130911 non-termination due to non-termination of
+cancel_p_ thy (str2term "(4 + -4 * b ^^^ 2) / (a ^^^ 4 + -2 * (a ^^^ 2 * b ^^^ 2) + b ^^^ 4)")
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
 else error "rational.sml: diff.behav. in norm_Rational 28";
+*)
-"-------- common denominator and multiplication ---------";
+"-------- examples common denominator and multiplication from: Schalk --------";
-"-------- common denominator and multiplication ---------";
+"-------- examples common denominator and multiplication from: Schalk --------";
-"-------- common denominator and multiplication ---------";
+"-------- examples common denominator and multiplication from: Schalk --------";
-(*SRAM Schalk I, p.69 Nr. 441b *)
+(*------- SRAM Schalk I, p.69 Nr. 441b *)
 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
-if (term2str t) =
-"(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
-(*SRAM Schalk I, p.69 Nr. 442b *)
+(*------- SRAM Schalk I, p.69 Nr. 442b *)
-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)";
+val t = str2term ("(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x) * " ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)");
-term2str t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-if (term2str t) =
+if term2str t = "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
-"5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
-(*SRAM Schalk I, p.69 Nr. 443b *)
+(*------- SRAM Schalk I, p.69 Nr. 443b *)
-val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
+val t = str2term "(a/2 + b/3) * (b/3 - a/2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
-if (term2str t) =
-"(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
-(*SRAM Schalk I, p.69 Nr. 445b *)
+(*------- SRAM Schalk I, p.69 Nr. 445b *)
 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "a ^^^ 3 / 27"
-if (term2str t) =
-"a ^^^ 3 / 27"
 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
-(*SRAM Schalk I, p.69 Nr. 446b *)
+(*------- SRAM Schalk I, p.69 Nr. 446b *)
 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
-if (term2str t) =
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";
-"30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
-then ()
+(*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
-else error "rational.sml: diff.behav. in norm_Rational_mg 32";
-(*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
 val t = str2term
 "(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)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
-if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
+(*------- SRAM Schalk I, p.69 Nr. 450a *)
-(*SRAM Schalk I, p.69 Nr. 450a *)
 val t = str2term
 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
-if (term2str t) =
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 34";
-"(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
-then ()
+(*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
-else error "rational.sml: diff.behav. in norm_Rational_mg 34";
-"-------- double fractions ------------------------------";
-"-------- double fractions ------------------------------";
-"-------- double fractions ------------------------------";
-(*SRD Schalk I, p.69 Nr. 454b *)
 val t = str2term
-"((2 - x)/(2*a)) / (2*a/(x - 2))";
+("(15*a^^^4/(a*x^^^3)  -  5*a*((b^^^4 - 5*c^^^2*x) / x^^^2))  *  " ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"(x^^^3/(5*a*b^^^3*c^^^3))   +   a/c^^^3 * (x*(b/a) - 3*b*(a/b^^^4))");
-term2str t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-if (term2str t) =
+if term2str t = "5 * x ^^^ 2 / (b ^^^ 3 * c)"
-"(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 35";
+"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
-(*SRD Schalk I, p.69 Nr. 455a *)
+"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
-val t = str2term
+"-------- examples double fractions from: Mathematik 1 Schalk ----------------";
-"(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
+"----- SRD Schalk I, p.69 Nr. 454b";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val t = str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
-term2str t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-if (term2str t) =
+if term2str t = "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
-"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 35";
+"----- SRD Schalk I, p.69 Nr. 455a";
+val t = str2term "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 36";
 "----- Schalk I, p.69 Nr. 455b";
 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+(* WN130911 non-termination due to non-termination of
+cancel_p_ thy (str2term ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
+"(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"))
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
+*)
 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
-val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
+val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
+(* WN130911 non-termination due to non-termination of
+cancel_p_ thy (str2term ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
+"(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"))
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
+*)
 "----- ?: worked before 0707xx";
 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-if term2str t = "-1 / (3 + y)" then ()
+if term2str t = "-1 / (3 + y)"
-else error "rational.sml: -1 / (3 + y) norm_Rational";
+then () else error "rational.sml: -1 / (3 + y) norm_Rational";
-(*SRD Schalk I, p.69 Nr. 456b *)
+"----- SRD Schalk I, p.69 Nr. 456b";
+val t = str2term "(b^^^3 - b^^^2) / (b^^^2+b) / (b^^^2 - 1)";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "b / (1 + 2 * b + b ^^^ 2)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 38";
+"----- SRD Schalk I, p.69 Nr. 457b";
+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))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
+"----- Schalk I, p.69 Nr. 458b works since 0707";
+val t = str2term "(2*a^^^2*x - a^^^2) / (a*x - b*x) / (b^^^2*(2*x - 1) / (x*(a - b)))";
+(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+:
+###  rls: cancel_p on: (-1 * a ^^^ 2 + 2 * (a ^^^ 2 * x)) / (a * x + -1 * (b * x)) /
+((-1 * b ^^^ 2 + 2 * (b ^^^ 2 * x)) / (a * x + -1 * (b * x)))
+exception Div raised
+BUT
 val t = str2term
-"(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
+("(-1 * a ^^^ 2 + 2 * (a ^^^ 2 * x)) / (a * x + -1 * (b * x)) /" ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"((-1 * b ^^^ 2 + 2 * (b ^^^ 2 * x)) / (a * x + -1 * (b * x)))");
-term2str t;
+NONE = cancel_p_ thy t;
-if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 38";
-(*SRD Schalk I, p.69 Nr. 457b *)
-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))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
-then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
-"----- Schalk I, p.69 Nr. 458b works since 0707";
-val t = str2term
-"(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
+*)
-(*SRD Schalk I, p.69 Nr. 459b *)
+"----- SRD Schalk I, p.69 Nr. 459b";
 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
 else error "rational.sml: diff.behav. in norm_Rational_mg 41";
+"----- Schalk I, p.69 Nr. 460b nonterm.SK";
-(*Schalk I, p.69 Nr. 460b nonterm.SK
+val t = str2term "(9*(x^^^2 - 8*x + 16) / (4*(y^^^2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))";
+(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+exception Div raised
+BUT
 val t = str2term
-"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
+("(144 + -72 * x + 9 * x ^^^ 2) / (4 + -8 * y + 4 * y ^^^ 2) /" ^
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+"((-12 + 3 * x) / (-16 + 16 * y))");
-if term2str t =
+NONE = cancel_p_ thy t;
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 42";
+if term2str t = !!!!!!!!!!!!!!!!!!!!!!!!!
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 42";
-val t = str2term
+*)
-"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
+"----- some variant of the above; was non-terminating before";
-... non terminating.
+val t = str2term "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
-val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
+val SOME (t , _) = rewrite_set_ thy false norm_Rational t;
-"(-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)";
+if term2str t = "(48 + -12 * x) / (1 + -1 * y)"
-val SOME (t,_) = rewrite_set_ thy false cancel_p t';
+then () else error "some variant of the above; was non-terminating before";
-... non terminating.*)
+"----- SRD Schalk I, p.70 Nr. 472a";
-(*SRD Schalk I, p.70 Nr. 472a *)
+val t = str2term ("((8*x^^^2 - 32*y^^^2) / (2*x + 4*y))  /  ((4*x - 8*y) / (x + y))");
-val t = str2term ("((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/" ^
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-		 "((4*x - 8*y)/(x + y))");
+if term2str t = "x + y"
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 43";
-term2str t;
-if (term2str t) =
+"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
-"x + y"
+val t = str2term ("(a - (a*b + b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
-then ()
+		 "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
-else error "rational.sml: diff.behav. in norm_Rational_mg 43";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
+if term2str t = "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 51";
-(*----------------------------------------------------------------------*)
-(*---------------------- Einfache Dppelbrche --------------------------*)
-(*----------------------------------------------------------------------*)
 (*SRD Schalk I, p.69 Nr. 461a *)
-val t = str2term
+val t = str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
-"(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "1 / 2"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 44";
-if (term2str t) =
-"1 / 2"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 44";
 (*SRD Schalk I, p.69 Nr. 464b *)
-val t = str2term
+val t = str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
-"(a - a/(a - 2)) / (a + a/(a - 2))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(-3 + a) / (-1 + a)"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 45";
-if (term2str t) =
-"(3 + -1 * a) / (1 + -1 * a)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 45";
 (*SRD Schalk I, p.69 Nr. 465b *)
-val t = str2term
+val t = str2term "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x))   /   (x/9 + y/6 + z/4)";
-"((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
+(* WN130911 non-termination due to non-termination of
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+cancel_p_ thy (str2term
-term2str t;
+("("(576 * x ^^^ 2 + 1728 * (x * y) + 1296 * y ^^^ 2 + -2916 * z ^^^ 2) /" ^
-if (term2str t) =
+"(576 * x ^^^ 2 + 864 * (x * y) + 1296 * (x * z))"))
-"(4 * x + 6 * y + -9 * z) / (4 * x)"
-then ()
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-else error "rational.sml: diff.behav. in norm_Rational_mg 46";
+if term2str t = "(4 * x + 6 * y + -9 * z) / (4 * x)"
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 46";
+*)
 (*SRD Schalk I, p.69 Nr. 466b *)
-val t = str2term
+val t = str2term "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
-"((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(25 + -10 * x + x ^^^ 2) / 18"
-term2str t;
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 47";
-if (term2str t) =
-"(25 + -10 * x + x ^^^ 2) / 18"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 47";
 (*SRD Schalk I, p.70 Nr. 469 *)
-val t = str2term
+val t = str2term ("3*b^^^2 / (4*a^^^2 - 8*a*b + 4*b^^^2) / " ^
-"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))";
+"(a / (a^^^2*b - b^^^3)  +  (a - b) / (4*a*b^^^2 + 4*b^^^3)  -  1 / (4*b^^^2))");
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "-3 * b ^^^ 3 / (-2 * a + 2 * b)"
-if (term2str t) =
+then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
-"3 * b ^^^ 3 / (2 * a + -2 * b)"
-then ()
+"-------- me Schalk I No.186 -------------------------------------------------";
-else error "rational.sml: diff.behav. in norm_Rational_mg 48";
+"-------- me Schalk I No.186 -------------------------------------------------";
+"-------- me Schalk I No.186 -------------------------------------------------";
-(*----------------------------------------------------------------------*)
+val fmz = ["Term ((14 * x * y) / ( x * y ))", "normalform N"];
-(*---------------------- Mehrfache Dppelbrueche ------------------------*)
-(*----------------------------------------------------------------------*)
-(*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
-(*WN060419 crashes with method 'simplify' ????SK*)
-val t = str2term
-"((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)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
-if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 49";
-"----- Schalk I, p.70 Nr. 477a";
-(* MG Achtung: terme explodieren; Bsp zu komplex;
-L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
-val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /" ^
-		 "(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
-val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / " ^
-		 "((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
-val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
-????SK ???MG*)
-"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
-val t = str2term ("(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
-		 "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
-val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-if term2str t' =
-"(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 51";
-(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
-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 ()
-else error "rational.sml: works again";
-re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
-(*Schalk I, p.70 Nr. 480a *)
-(* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
-val t = str2term
-"(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)))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 52";
-(*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
-val t = str2term
-"(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-"(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)";
-val t = str2term
-"2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-"1"
-(* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
-###  rls: cancel_p on:
-(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))
-GC #3.61.81.101.197.17503:   (0 ms)
-*** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
-val t = str2term
-"(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))";
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-(*uncaught exception nonexhaustive binding failure*)
-(* Das kann er aber krzen !!????: *)
-val t = str2term
-"(x^^^2 * (y^^^2 * z) +  x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-"(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
-*)
-"-------- crucial examples ------------------------------";
-"-------- crucial examples ------------------------------";
-"-------- crucial examples ------------------------------";
-(*Schalk I, p.60 Nr. 215d *)
-(* Achtung: rechnet ewig ...
-val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t; noterm.SK
-*)
-(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
-(*
-val t = str2term "(a-b)^^^3 * (x+y)^^^4";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-"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";
-val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-"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";
-*)
-(*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
-(*--------------------------------------------------------------------*)
-(*Schalk I, p.70 Nr. 480b
-val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
-		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
-		 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
-		 "(20*x*y/(x^^^2 - 25*y^^^2))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-SK.nonterm
-Kann nicht weiter vereinfacht werden !!!!?? *)
-(*--------------------------------------------------------------------*)
-"---- MGs test set";
-val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
-val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
-if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
-else error "";
-(*--------------------------------------------------------------------*)
-(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
----> Sortierung FALSCH !!  *)
-val t = str2term "b^^^3 * a^^^5/a ";
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-"1 * (a^^^4 * b^^^3) / 1"; (*OK*)
-val t = str2term "b^^^3 * a^^^5/b ";
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-"1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
-(* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
-(*
-val x = str2term "x"; val bdv = str2term "bdv";
-val t1 = str2term "b^^^2 * a^^^5";
-val t2 = str2term "a^^^5 * b^^^2 ";
-ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
-*)
-(* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
-(*--------------------------------------------------------------------*)
-(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
----> erzeugt berflssige "1 * ..."
-val t = str2term "-1 / (3 + y)";
-(*~~         *)
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-"-1 / (3 + 1 * y)";
-(********* Das ist das PROBLEM !!!!!!!??? *******************)
-(* -1 im Z???ler der Angabe verursacht das Problem !*)
-*)
-(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
-"----- MGs test set";
-val t = str2term "(a^^^2 + -1)/(a+1)";
-val SOME (t',_) = rewrite_set_ thy false cancel_p t;
-if term2str t' = "(-1 + a) / 1" then ()
-else error "rational.sml MG tests 3d";
-"----- NOT TERMINATING ?: worked before 0707xx";
-val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
-val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
-if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
-else error "rational.sml MG tests 3e";
-"----- corrected SK060905";
-val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-if term2str t' = "-1 / (5 + -2 * x)" then ()
-else error "rational.sml corrected SK060905";
-"-------- examples for Stefan Karnels thesis ------------";
-"-------- examples for Stefan Karnels thesis ------------";
-"-------- examples for Stefan Karnels thesis ------------";
-(*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
-val t = str2term
-"(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))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
-if (term2str t) =
-"5 * x ^^^ 2 / (b ^^^ 3 * c)"
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 53";
-"-------- me Schalk I No.186 ----------------------------";
-"-------- me Schalk I No.186 ----------------------------";
-"-------- me Schalk I No.186 ----------------------------";
-val fmz = ["Term ((14 * x * y) / ( x * y ))",
-	   "normalform N"];
 val (dI',pI',mI') =
 ("Rational",["rational","simplification"],
 ["simplification","of_rationals"]);
 val p = e_pos'; val c = [];
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
 case (f2str f, nxt) of
 ("14", ("End_Proof'", _)) => ()
 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
+"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
-"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
+"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
-"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
+"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
-"-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
 states:=[];
-CalcTree
+CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
-[(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
+("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
-("Rational",["rational","simplification"],
-["simplification","of_rationals"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt, p), _) = get_calc 1;
+(*
-interSteps 1 ([1],Res);
+show_pt pt;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+[
+(([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
+(([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
-"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
+(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
-"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
+(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
-"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
+(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
+(([4], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)),
+(([], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2))]
+*)
+interSteps 1 ([1], Res);
+val ((pt, p), _) = get_calc 1;
+(*show_pt pt;
+[
+(([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
+(([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
+(([1,1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
+(([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + -1 * 2))),
+(([1,2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
+(([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
+(([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
+(([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
+(([4], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)),
+(([], Res), (-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2))]
+*)
+val (t, asm) = get_obj g_result pt [1, 1];
+if term2str t = "(2 - x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso terms2str asm = "[]"
+then () else error "2nd interSteps ..Simp_Rat_Double_No-1 changed on [1, 1]";
+val (t, asm) = get_obj g_result pt [1, 2];
+if term2str t = "(2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso terms2str asm = "[]"
+then () else error "3rd interSteps ..Simp_Rat_Double_No-1 changed on [1, 2]";
+"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
+"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
+"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
 states:=[];
-CalcTree
+CalcTree [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
-[(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
+("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
-("Rational",["rational","simplification"],
-["simplification","of_rationals"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt, p), _) = get_calc 1;
-(*========== inhibit exn 110314 ================================================
+(*show_pt pt;
-(*with explicit script done already... and removed [1,..] at below...
+[
-interSteps 1 ([1],Res);
+(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
-val ((pt,p),_) = get_calc 1; show_pt pt;
+(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
-*)
+(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
-interSteps 1 ([2],Res);
+(([2], Res), (a + b) / (a + -1 * b)),
-val ((pt,p),_) = get_calc 1; show_pt pt;
+(([], Res), (a + b) / (a + -1 * b))]
+*)
+interSteps 1 ([2], Res);
+val ((pt, p), _) = get_calc 1;
+(*show_pt pt;
+[
+(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
+(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
+(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
+(([2,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
+(([2,1], Res), (a + b) / (a + -1 * b)),
+(([2], Res), (a + b) / (a + -1 * b)),
+(([], Res), (a + b) / (a + -1 * b))]
+*)
 interSteps 1 ([2,1],Res);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt, p), _) = get_calc 1;
+(*show_pt pt;
+[
+(([], Frm), Simplify ((a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2))),
+(([1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * a * b + b ^^^ 2)),
+(([1], Res), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
+(([2,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
+(([2,1,1], Frm), (a ^^^ 2 + -1 * b ^^^ 2) / (a ^^^ 2 + -2 * (a * b) + b ^^^ 2)),
+(([2,1,1], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
+(a ^^^ 2 + -2 * (a * b) + 1 * b ^^^ 2)),
+(([2,1,2], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
+(a ^^^ 2 + -2 * (a * b) + -1 ^^^ 2 * b ^^^ 2)),
+(([2,1,3], Res), (a ^^^ 2 + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
+(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
+(([2,1,4], Res), (a * a + -1 * (a * b) + a * b + -1 * b ^^^ 2) /
+(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
+(([2,1,5], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
+(a ^^^ 2 + -2 * (a * b) + (-1 * b) ^^^ 2)),
+(([2,1,6], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
+(a ^^^ 2 + -1 * (2 * (a * b)) + (-1 * b) ^^^ 2)),
+(([2,1,7], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
+(a ^^^ 2 + 2 * (a * (-1 * b)) + (-1 * b) ^^^ 2)),
+(([2,1,8], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
+(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
+(([2,1,9], Res), (a * (a + -1 * b) + (b * a + b * (-1 * b))) /
+(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
+(([2,1,10], Res), (a * (a + -1 * b) + b * (a + -1 * b)) /
+(a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
+(([2,1,11], Res), (a + b) * (a + -1 * b) / (a ^^^ 2 + 2 * a * (-1 * b) + (-1 * b) ^^^ 2)),
+(([2,1,12], Res), (a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))),
+(([2,1,13], Res), (a + b) / (a + -1 * b)),
+(([2,1], Res), (a + b) / (a + -1 * b)),
+(([2], Res), (a + b) / (a + -1 * b)),
+(([], Res), (a + b) / (a + -1 * b))]
+*)
 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
-(*if length newnds = 12 then () WN060905*)
+if length newnds = 13 then () else error "rational.sml: interSteps cancel_p rev_rew_p";
-if length newnds = 13 then ()
-else error "rational.sml: interSteps cancel_p rev_rew_p";
 val p = ([2,1,9],Res);
 getTactic 1 p;
 val (_, tac, _) = pt_extract (pt, p);
-(*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
+case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
-WN060905*)
-case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
-============ inhibit exn 110314 ==============================================*)
+"-------- investigate rulesets for cancel_p ----------------------------------";
-"-------- investigate rulesets for cancel_p -------------";
+"-------- investigate rulesets for cancel_p ----------------------------------";
-"-------- investigate rulesets for cancel_p -------------";
+"-------- investigate rulesets for cancel_p ----------------------------------";
-"-------- investigate rulesets for cancel_p -------------";
 val thy = @{theory "Rational"};
-"---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
 "----- with rewrite_set_";
 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
-term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
+if term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" then () else error "rls chancel_p 1";
 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
-term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
+if term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" then () else error "rls chancel_p 2";
-"----- with make_deriv";
+"----- with make_deriv; WN1130912 not investigated further, will be discontinued";
-val SOME (tt, _) = factout_p_ thy t; term2str tt =
+val SOME (tt, _) = factout_p_ thy t;
-"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
+if term2str tt = "(a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))"
-(*
+then () else error "rls chancel_p 3";
-"--- with ruleset as before 060829";
+term2str tt = "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
-val {rules, rew_ord=(_,ro),...} =
-rep_rls (assoc_rls "make_polynomial");
+"--- with simpler ruleset";
+val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p");
 val der = make_deriv thy Atools_erls rules ro NONE tt;
-print_depth 99; map (term2str o #1) der; print_depth 3;
+if length der = 12 then () else error "WN1130912 rls chancel_p 4";
-print_depth 99; map (rule2str o #2) der; print_depth 3;
-... did not terminate*)
-"--- with simpler ruleset";
-val {rules, rew_ord=(_,ro),...} =
-rep_rls (assoc_rls "rev_rew_p");
-val der = make_deriv thy Atools_erls rules ro NONE tt;
 print_depth 99; writeln (deriv2str der); print_depth 3;
 print_depth 99; map (term2str o #1) der; print_depth 3;
 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
 print_depth 99; map (rule2str o #2) der; print_depth 3;
 print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
 val der = make_deriv thy Atools_erls rules ro NONE
-		     (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
+	(str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
 print_depth 99; writeln (deriv2str der); print_depth 3;
-val {rules, rew_ord=(_,ro),...} =
+val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p");
-rep_rls (assoc_rls "rev_rew_p");
 val der = make_deriv thy Atools_erls rules ro NONE
-		     (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
+	(str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
 print_depth 99; writeln (deriv2str der); print_depth 3;
 print_depth 99; map (term2str o #1) der; print_depth 3;
 (*WN060829 ...postponed*)
-"-------- investigate format of factout_ and factout_p_ -";
+"-------- fun eval_get_denominator -------------------------------------------";
-"-------- investigate format of factout_ and factout_p_ -";
+"-------- fun eval_get_denominator -------------------------------------------";
-"-------- investigate format of factout_ and factout_p_ -";
+"-------- fun eval_get_denominator -------------------------------------------";
-val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
-val (thy, eval_rls) = (@{theory "Rational"}, Atools_erls)(*see 'fun init_state'*);
-val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
-"----- see Rational.ML, local cancel_p, fun init_state";
-val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
-val SOME (t',_) = factout_p_ thy t; term2str t';
-(*
-val rtas = reverse_deriv thy eval_rls rules ro NONE t';
-writeln(trtas2str rst);
-*)
-"----- see Rational.ML, local cancel_p, fun init_state";
-val t = str2term "a^^^2 / a";
-val SOME (t',_) = factout_p_ thy t;
-term2str t' = "a * a / (1 * a)" (*true*);
-(*... can be canceled with
-real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
-(* sml/ME/rewtools.sml:
-val rtas = reverse_deriv thy Atools_erls rules ro NONE t';
-writeln (deri2str rtas);
-*)
-"-------- SK 060904 ----------------------------------------------";
-"----- order on polynomials -- input + output";
-val thy = @{theory "Isac"};
-val t = str2term "(a + -1 * b) / (-1 * a + b)";
-val SOME (t', _) = factout_p_ thy t; term2str t';
-val SOME (t', _) = cancel_p_ thy t; term2str t';
-val t = str2term "a*b*c*d / (d*e*f*g)";
-val SOME (t', _) = cancel_p_ thy t; term2str t';
-val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
-val SOME (t', _) = cancel_p_ thy t; term2str t';
-(*???order.SK  ???*)
-"----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
-val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
-if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
-else error "rational.sml SK060904-1a worked since 0707xx";
-"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
-val t = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
-"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
-val SOME (t',_) = cancel_p_ thy t;
-if term2str t' = "1 / (4 * c + 3 * e)" then ()
-else error "rational.sml SK060904-1b";
-"----- SK060904-2a non-termination of add_fraction_p_";
-val t = str2term (" (a + b * x) / (a + -1 * (b * x)) +  " ^
-		  " (-1 * a + b * x) / (a + b * x)      ");
-(* nonterm.SK
-val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
-common_nominator_p_ thy t;
-" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) +  " ^
-" (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
-add_fraction_p_ thy t;
-" ((a + b * x)*(a + b * x)  +  (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
-" ((a + b * x)*(-1 * a + b * x))                                     ";
-*)
-"-------- how to stepwise construct Scripts -------------";
-"-------- how to stepwise construct Scripts -------------";
-"-------- how to stepwise construct Scripts -------------";
-val thy = @{theory "Rational"};
-(*no trailing _*)
-val p1 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  (Rewrite_Set discard_minus False                   " ^
-"   t_t)");
-(*required (): (Rewrite_Set discard_minus False)*)
-val p2 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  (Rewrite_Set discard_minus False                   " ^
-"   t_t)");
-val p3 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  ((Rewrite_Set discard_minus False)                   " ^
-"   t_t)");
-val p4 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  ((Rewrite_Set discard_minus False)                   " ^
-"   t_t)");
-val p5 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  ((Try (Rewrite_Set discard_minus False)                   " ^
-"    Try (Rewrite_Set discard_parentheses False))               " ^
-"   t_t)");
-val p6 = parse thy (
-"Script SimplifyScript (t_t::real) =                             " ^
-"  ((Try (Rewrite_Set discard_minus False) @@                   " ^
-"    Try (Rewrite_Set rat_mult_poly False) @@                    " ^
-"    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^
-"    Try (Rewrite_Set cancel_p_rls False) @@                     " ^
-"    (Repeat                                                     " ^
-"     ((Try (Rewrite_Set common_nominator_p_rls False) @@        " ^
-"       Try (Rewrite_Set rat_mult_div_pow False) @@              " ^
-"       Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
-"       Try (Rewrite_Set cancel_p_rls False) @@                  " ^
-"       Try (Rewrite_Set rat_reduce_1 False)))) @@               " ^
-"    Try (Rewrite_Set discard_parentheses False))               " ^
-"   t_t)"
-);
-"----------- get_denominator ----------------------------";
-"----------- get_denominator ----------------------------";
-"----------- get_denominator ----------------------------";
 val thy = @{theory Isac};
 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
 val SOME (_, t') = eval_get_denominator "" 0 t thy;
-if term2str t' = "get_denominator ((a + x) / b) = b" then ()
+if term2str t' = "get_denominator ((a + x) / b) = b"
-else error "get_denominator ((a + x) / b) = b"
+then () else error "get_denominator ((a + x) / b) = b"
-"--------- several errpats in complicated term -------------------";
+"-------- several errpats in complicated term --------------------------------";
-"--------- several errpats in complicated term -------------------";
+"-------- several errpats in complicated term --------------------------------";
-"--------- several errpats in complicated term -------------------";
+"-------- several errpats in complicated term --------------------------------";
-(*TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one*)
+(*WN12xxxx TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one
-states:=[];
+WN130912: kept this test, although not clear what for*)
-CalcTree
+states := [];
-[(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
+CalcTree [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
-("Rational",["rational","simplification"], ["simplification","of_rationals"]))];
+("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt, p), _) = get_calc 1;
+(*show_pt pt;
-"-------- nonterminating cancel_p, norm_Rational 2002 ---";
+[
-"-------- nonterminating cancel_p, norm_Rational 2002 ---";
+(([], Frm), Simplify ((5 * b + 25) / (a ^^^ 2 - b ^^^ 2) * (a - b) / (5 * b))),
-"-------- nonterminating cancel_p, norm_Rational 2002 ---";
+(([1], Frm), (5 * b + 25) / (a ^^^ 2 - b ^^^ 2) * (a - b) / (5 * b)),
-(*------------------------------------------------------------------------------------\
+(([1], Res), (5 * b + 25) / (a ^^^ 2 + -1 * b ^^^ 2) * (a + -1 * b) / (5 * b)),
-"--- WN121204: searched rational.sml for "nonterm", added new numbering" ^
+(([2], Res), (5 * b + 25) * (a + -1 * b) / (a ^^^ 2 + -1 * b ^^^ 2) / (5 * b)),
-"              and thoroughly tested with this numbering subsequently";
+(([3], Res), (25 * a + -25 * b + 5 * (a * b) + -5 * b ^^^ 2) / (a ^^^ 2 + -1 * b ^^^ 2) /
-"--- 1 ---";
+(5 * b)),
-WN.2.6.03 from rlang.sml 56a
+(([4], Res), (25 + 5 * b) / (a + b) / (5 * b)),
-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)";
+(([5], Res), (25 + 5 * b) / ((a + b) * (5 * b))),
-val NONE = rewrite_set_ thy false common_nominator_p t;
+(([6], Res), (25 + 5 * b) / (5 * (a * b) + 5 * b ^^^ 2)),
-"--- 2 ---";
+(([7], Res), (5 + b) / (a * b + b ^^^ 2)),
-WN060831 nonterm.SK7
+(([], Res), (5 + b) / (a * b + b ^^^ 2))] *)
-val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
-val NONE = add_fraction_p_ thy t;
-"--- 3 ---";
-nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
-val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
-"--- 4 ---";
-val t = str2term
-"(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)";
-WN060831 nonterm.SK10
-val SOME (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-"--- 5 ---";
-val t = str2term
-"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-if term2str t =
-then ()
-else error "rational.sml: diff.behav. in norm_Rational_mg 42";
-"--- 6 ---";
-val t = str2term
-"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
-val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
-... non terminating.
-"--- 7 ---";
-val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
-"(-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)";
-val SOME (t,_) = rewrite_set_ thy false cancel_p t';
-"--- 8 ---";
-val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-"--- 9 ---";
-val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
-		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
-		 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
-		 "(20*x*y/(x^^^2 - 25*y^^^2))";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-"--- 10 ---";
-SK060904-2a non-termination of add_fraction_p_";
-val t = str2term (" (a + b * x) / (a + -1 * (b * x)) +  " ^
-		  " (-1 * a + b * x) / (a + b * x)      ");
-(* nonterm.SK = WN130830
-val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
-"--- 11 ---";
-common_nominator_p_ thy t;
-" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) +  " ^
-" (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
-"--- 12 ---";
-add_fraction_p_ thy t;
-" ((a + b * x)*(a + b * x)  +  (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
-" ((a + b * x)*(-1 * a + b * x))                                     ";
---------------------------------------------------------------------------------------/*)
-(*------------------------------------------------------------------------------------\
-"WN121205: thoroughly tested with the above numbering.";
-"  errors in cancel_p: --- 4,5,6,7.";
-"  error in common_nominator_p, common_nominator_p_: --- 10; 1,2?.";
-"  errors caused by ruleset norm_Rational: --- 8,9.";
-trace_rewrite := false;
-"--- 1 ---: non-terminating with ### add_fract: done t22 "; = WN130830
-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)";
-trace_rewrite := false;
-rewrite_set_ thy false common_nominator_p t;
-"--- 2 ---: non-terminating with ### add_fract: done t22 ";
-val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
-add_fraction_p_ thy t;
-"--- 3 ---: norm_Rational calls Rrls cancel_p with non-normalised polys";
-val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
-rewrite_set_ thy false norm_Rational t;
-(*tracing end...####  rls: cancel_p on:
-(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) *)
-"--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
-val t = str2term (
-"(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)");
-rewrite_set_ thy false cancel_p t;
-(*#  rls: cancel_p on:
-(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) *)
-"--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
-val t = str2term "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
-rewrite_set_ thy false norm_Rational t;
-(*####  rls: cancel_p on:
-(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))  *)
-"--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
-val t = str2term
-"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
-rewrite_set_ thy false norm_Rational t;
-(*###  rls: cancel_p on: (-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)) *)
-"--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
-val t' = str2term (
-"(-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)");
-rewrite_set_ thy false cancel_p t';
-"--- 8 ---: bottom of output cannot be looked ad (due to looping?)";
-val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
-val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
-"--- 9 ---: probably error in norm_Rational";
-val t = str2term (
-"((12*x*y / (9*x^^^2 - y^^^2)) / (1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
-		"(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y/(x^^^2 - 25*y^^^2))");
-rewrite_set_ thy false norm_Rational t;
-(*####  rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +
-108240 * (x ^^^ 4 * y ^^^ 6) +
--6000 * (x ^^^ 2 * y ^^^ 8)) /
-(2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +
-1362000 * (x ^^^ 4 * y ^^^ 6) +
--150000 * (x ^^^ 2 * y ^^^ 8)) *)
-"--- 10 ---: non-terminating with ### add_fract: done t22: error in common_nominator_p ";
-val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)");
-rewrite_set_ thy false common_nominator_p t; (*### add_fract: done t22 *)
-common_nominator_p_ thy t;                   (*loops without output*)
-"--- reformulated 10:";
-val t = str2term "(a + -1 * (b * x)) / (a + b * x)";
-rewrite_set_ thy false cancel_p t = NONE;
-"--- 11 ---";
-"--- 12 ---";
-"...both are to be considered after common_nominator_p_ is improved";
---------------------------------------------------------------------------------------/*)
-============ inhibit exn WN130824 TODO ======================================================*)

changeset 52105	2786cc9704c8
parent 52104	83166e7c7e52
child 52106	7f3760f39bdc