wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              CalcTreeTEST;

    10   open LItool;                 arguments_from_model;

    11   open Sub_Problem;

    12   open Fetch_Tacs;

    13   open Step

    14   open Env;

    15   open LI;                     scan_dn;

    16   open Istate;

    17   open Error_Pattern;

    18   open Error_Pattern_Def;

    19   open Specification;

    20   open Ctree;                  append_problem;

    21   open Pos;

    22   open Program;

    23   open Prog_Tac;

    24   open Tactical;

    25   open Prog_Expr;

    26   open Auto_Prog;              rule2stac;

    27   open Input_Descript;

    28   open Specify;

    29   open Specify;

    30   open Step_Specify;

    31   open Step_Solve;

    32   open Step;

    33   open Solve;                  (* NONE *)

    34   open ContextC;               transfer_asms_from_to;

    35   open Tactic;                 (* NONE *)

    36   open I_Model;

    37   open O_Model;

    38   open P_Model;                (* NONE *)

    39   open Rewrite;

    40   open Eval;                   get_pair;

    41   open TermC;                  atomt;

    42   open Rule;

    43   open Rule_Set;               Sequence;

    44   open Eval_Def

    45   open ThyC

    46   open ThmC_Def

    47   open ThmC

    48   open Rewrite_Ord

    49   open UnparseC

    50 \<close>

    52 section \<open>code for copy & paste ===============================================================\<close>

    53 ML \<open>

    54 "~~~~~ fun xxx , args:"; val () = ();

    55 "~~~~~ and xxx , args:"; val () = ();

    56 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    57 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

    58 "xx"

    59 ^ "xxx"   (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)

    60 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)

    61 \<close> ML \<open>

    62 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)

    63 (*/------------------- step into XXXXX -----------------------------------------------------\*)

    64 (*-------------------- stop step into XXXXX -------------------------------------------------*)

    65 (*\------------------- step into XXXXX -----------------------------------------------------/*)

    66 (*-------------------- contiue step into XXXXX ----------------------------------------------*)

    67 (*/------------------- check entry to XXXXX ------------------------------------------------\*)

    68 (*\------------------- check entry to XXXXX ------------------------------------------------/*)

    69 (*/------------------- check within XXXXX --------------------------------------------------\*)

    70 (*\------------------- check within XXXXX --------------------------------------------------/*)

    71 (*/------------------- check result of XXXXX -----------------------------------------------\*)

    72 (*\------------------- check result of XXXXX -----------------------------------------------/*)

    73 (* final test ...*)

    74 (*/------------------- build new fun XXXXX -------------------------------------------------\*)

    75 (*\------------------- build new fun XXXXX -------------------------------------------------/*)

    76 \<close> ML \<open>

    77 \<close>

    78 ML \<open>

    79 \<close> ML \<open>

    80 \<close> ML \<open>

    81 \<close>

    82 text \<open>

    83   declare [[show_types]]

    84   declare [[show_sorts]]

    85   find_theorems "?a <= ?a"

    87   print_theorems

    88   print_facts

    89   print_statement ""

    90   print_theory

    91   ML_command \<open>Pretty.writeln prt\<close>

    92   declare [[ML_print_depth = 999]]

    93   declare [[ML_exception_trace]]

    94 \<close>

    96 section \<open>===================================================================================\<close>

    97 ML \<open>

    98 \<close> ML \<open>

    99 \<close> ML \<open>

   100 \<close> ML \<open>

   101 \<close>

   103 section \<open>3============== NEW src/../ "Knowledge/Poly.thy" ================================\<close>

   104 subsection \<open>auxiliary functions\<close>

   105 ML \<open>

   106 val thy = @{theory};

   107 val poly_consts =

   108   ["Groups.plus_class.plus", "Groups.minus_class.minus",

   109   "Rings.divide_class.divide", "Groups.times_class.times",

   110   "Transcendental.powr"];

   112 val int_ord_SAVE = int_ord;

   113 (*for tests on rewrite orders*)

   114 fun int_ord (i1, i2) =

   115 (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};

   116   Int.compare (i1, i2));

   117 (**)val int_ord = int_ord_SAVE; (*..outcomment for tests*)

   118 \<close>

   119 subsubsection \<open>for predicates in specifications (ML)\<close>

   120 ML \<open>

   121 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)

   122 (*. a "monomial t in variable v" is a term t with

   123   either (1) v NOT existent in t, or (2) v contained in t,

   124   if (1) then degree 0

   125   if (2) then v is a factor on the very right, casually with exponent.*)

   126 fun factor_right_deg (*case 2*)

   127 	    (Const ("Groups.times_class.times", _) $

   128         t1 $ (Const ("Transcendental.powr",_) $ vv $ num)) v =

   129 	  if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))

   130     else NONE

   131   | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ num) v =

   132 	   if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE

   133   | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =

   134 	   if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE

   135   | factor_right_deg vv v =

   136 	  if (vv = v) then SOME 1 else NONE;

   137 fun mono_deg_in m v =  (*case 1*)

   138 	if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;

   140 fun expand_deg_in t v =

   141 	let

   142     fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) =

   143           (case mono_deg_in t2 v of (* $ is left associative*)

   144             SOME d' => edi d' d' t1 | NONE => NONE)

   145       | edi ~1 ~1 (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =

   146           (case mono_deg_in t2 v of

   147             SOME d' => edi d' d' t1 | NONE => NONE)

   148       | edi d dmax (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =

   149           (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)

   150 	        SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

   151           | NONE => NONE)

   152       | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

   153           (case mono_deg_in t2 v of

   154             SOME d' =>    (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)

   155               if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

   156           | NONE => NONE)

   157       | edi ~1 ~1 t =

   158           (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)

   159       | edi d dmax t = (*basecase last*)

   160     	    (case mono_deg_in t v of

   161     	      SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE

   162 		      | NONE => NONE)

   163 	in edi ~1 ~1 t end;

   165 fun poly_deg_in t v =

   166 	let

   167     fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

   168 		    (case mono_deg_in t2 v of (* $ is left associative *)

   169 		      SOME d' => edi d' d' t1

   170         | NONE => NONE)

   171 	    | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

   172 		    (case mono_deg_in t2 v of

   173 	        SOME d' =>    (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)

   174             if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE

   175         | NONE => NONE)

   176 	    | edi ~1 ~1 t =

   177         (case mono_deg_in t v of

   178 		      d as SOME _ => d

   179         | NONE => NONE)

   180 	    | edi d dmax t = (* basecase last *)

   181 		    (case mono_deg_in t v of

   182 		      SOME d' =>

   183             if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE

   184         | NONE => NONE)

   185 	in edi ~1 ~1 t end;

   186 \<close>

   188 subsubsection \<open>for hard-coded AC rewriting (MG)\<close>

   189 ML \<open>

   190 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)

   192 (*FIXME.0401: make SML-order local to make_polynomial(_) *)

   193 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)

   194 (* Polynom --> List von Monomen *)

   195 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

   196     (poly2list t1) @ (poly2list t2)

   197   | poly2list t = [t];

   199 (* Monom --> Liste von Variablen *)

   200 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =

   201     (monom2list t1) @ (monom2list t2)

   202   | monom2list t = [t];

   204 \<close> text \<open> (* \<longrightarrow> libraryC.sml *)

   205 (* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)

   206 fun string_of_int' i =

   207     if i >= 0 then i |> string_of_int

   208     else (i * ~1) |> string_of_int |> curry op ^ "-"

   209 \<close> ML \<open>

   210 (* use this fun ONLY locally: makes negative numbers with "-" instead of "~" for poly-orders*)

   211 fun dest_number' t = t |> TermC.num_of_term |> string_of_int'

   212 \<close> ML \<open>

   213 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)

   214 \<close> ML \<open> (* orig.code *)

   215 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str

   216   | get_basStr (Free (str, _)) = str

   217   | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)

   218 (*| get_basStr t =

   219     raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)

   220 \<close> ML \<open> (* \<longrightarrow> Poly.thy *)

   221 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str

   222   | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = dest_number' n

   223   | get_basStr (Free (str, _)) = str

   224   | get_basStr t =

   225     if TermC.is_num t then dest_number' t

   226     else "|||"; (* gross gewichtet; für Brüche ect. *)

   227 \<close> ML \<open>

   229 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)

   230 \<close> ML \<open> (*original*)

   231 fun get_potStr (Const ("Transcendental.powr",_) $ Free _ $ Free (str, _)) = str

   232   | get_potStr (Const ("Transcendental.powr",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)

   233   | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)

   234   | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)

   235 (*| get_potStr t =

   236     raise ERROR("get_potStr: called with t= "^(UnparseC.term t));*)

   237 \<close> ML \<open> (* \<longrightarrow> Poly.thy *)

   238 fun get_potStr (Const ("Transcendental.powr", _) $ Free _ $ Free (str, _)) = str

   239   | get_potStr (Const ("Transcendental.powr", _) $ Free _ $ t) =

   240     if TermC.is_num t then dest_number' t else "|||"

   241   | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)

   242   | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)

   244 (* Umgekehrte string_ord *)

   245 val string_ord_rev =  rev_order o string_ord;

   247  (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)

   248     innerhalb eines Monomes:

   249     - zuerst lexikographisch nach Variablenname

   250     - wenn gleich: nach steigender Potenz *)

   251 fun var_ord (a, b) =

   252 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",

   253    sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

   254   prod_ord string_ord string_ord

   255   ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

   256 );

   257 fun var_ord (a,b: term) =

   258   prod_ord string_ord string_ord

   259     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));

   260 \<close> ML \<open>

   262 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);

   263    verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:

   264    - zuerst lexikographisch nach Variablenname

   265    - wenn gleich: nach sinkender Potenz*)

   266 fun var_ord_revPow (a, b: term) =

   267 (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",

   268     sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};

   269   prod_ord string_ord string_ord_rev

   270     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))

   271 );

   272 fun var_ord_revPow (a, b: term) =

   273   prod_ord string_ord string_ord_rev

   274     ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));

   276 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)

   277 fun sort_varList ts =

   278 (@{print} {a = "sort_varList", args = UnparseC.terms ts};

   279   sort var_ord ts);

   280 val sort_varList = sort var_ord;

   281 \<close> ML \<open>

   283 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt

   284    Argumente in eine Liste *)

   285 \<close> ML \<open> (* DONE Poly.thy *)

   286 fun args u : term list =

   287   let

   288     fun stripc (f $ t, ts) = stripc (f, t::ts)

   289   	  | stripc (t as Free _, ts) = (t::ts)

   290   	  | stripc (_, ts) = ts

   291   in stripc (u, []) end;

   293 (* liefert True, falls der Term (Liste von Termen) nur Zahlen

   294    (keine Variablen) enthaelt *)

   295 fun filter_num ts = fold (curry and_) (map TermC.is_num ts) true

   297 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt

   298    dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)

   299 fun is_nums t = filter_num [t];

   301 (* Berechnet den Gesamtgrad eines Monoms *)

   302 (**)local(**)

   303   fun counter (n, []) = n

   304     | counter (n, x :: xs) =

   305 	    if (is_nums x) then counter (n, xs)

   306 	    else

   307 	      (case x of

   308 		      (Const ("Transcendental.powr", _) $ Free _ $ t) =>

   309             if TermC.is_num t

   310             then counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs)

   311             else counter (n + 1000, xs) (*FIXME.MG?!*)

   312 	      | (Const ("Num.numeral_class.numeral", _) $ num) =>

   313             counter (n + 1 + HOLogic.dest_numeral num, xs)

   314 	      | _ => counter (n + 1, xs)) (*FIXME.MG?! ... Brüche ect.*)

   315 (**)in(**)

   316   fun monom_degree l = counter (0, l)

   317 (**)end;(*local*)

   318 \<close> ML \<open>

   320 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich

   321    der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,

   322    werden jedoch dabei ignoriert (uebersprungen)  *)

   323 fun dict_cond_ord _ _ ([], [])     = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

   324   | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)

   325   | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)

   326   | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =

   327     (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",

   328       is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};

   329      case (cond x, cond y) of

   330 	    (false, false) =>

   331         (case elem_ord (x, y) of

   332 				  EQUAL => dict_cond_ord elem_ord cond (xs, ys)

   333 			  | ord => ord)

   334     | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)

   335     | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)

   336     | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys) );

   337 fun dict_cond_ord _ _ ([], []) = EQUAL

   338   | dict_cond_ord _ _ ([], _ :: _) = LESS

   339   | dict_cond_ord _ _ (_ :: _, []) = GREATER

   340   | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =

   341     (case (cond x, cond y) of

   342 	    (false, false) =>

   343         (case elem_ord (x, y) of

   344 				  EQUAL => dict_cond_ord elem_ord cond (xs, ys)

   345 			  | ord => ord)

   346     | (false, true)  => dict_cond_ord elem_ord cond (x :: xs, ys)

   347     | (true, false)  => dict_cond_ord elem_ord cond (xs, y :: ys)

   348     | (true, true)  =>  dict_cond_ord elem_ord cond (xs, ys) );

   350 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):

   351    zuerst nach Gesamtgrad int_ord, bei gleichem Gesamtgrad lexikographisch ordnen -

   352    dabei werden Koeffizienten ignoriert (2*3*a \<up> 2*4*b gilt wie a \<up> 2*b) *)

   353 fun degree_ord (xs, ys) =

   354 	prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)

   355 	  ((monom_degree xs, xs), (monom_degree ys, ys));

   357 fun hd_str str = substring (str, 0, 1);

   358 fun tl_str str = substring (str, 1, (size str) - 1);

   360 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)

   361 \<close> ML \<open> (* DONE Poly.thy *)

   362 fun get_koeff_of_mon [] = raise ERROR "get_koeff_of_mon: called with l = []"

   363   | get_koeff_of_mon (x :: _) = if is_nums x then SOME x else NONE;

   365 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)

   366 fun koeff2ordStr (SOME t) =

   367     if TermC.is_num t

   368     then

   369       if (t |> HOLogic.dest_number |> snd) < 0

   370       then (t |> HOLogic.dest_number |> snd |> curry op * ~1 |> string_of_int) ^ "0"  (* 3 < -3 *)

   371       else (t |> HOLogic.dest_number |> snd |> string_of_int)

   372     else "aaa"                                                      (* "num.Ausdruck" --> gross *)

   373   | koeff2ordStr NONE = "---";                                     (* "kein Koeff" --> kleinste *)

   375 (* Order zum Vergleich von Koeffizienten (strings):

   376    "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)

   377 fun compare_koeff_ord (xs, ys) =

   378 (@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",

   379     sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};

   380   string_ord

   381   ((koeff2ordStr o get_koeff_of_mon) xs,

   382    (koeff2ordStr o get_koeff_of_mon) ys)

   383 );

   384 fun compare_koeff_ord (xs, ys) = string_ord

   385   ((koeff2ordStr o get_koeff_of_mon) xs,

   386    (koeff2ordStr o get_koeff_of_mon) ys);

   388 (* Gesamtgradordnung: falls degree_ord EQUAL + Ordnen nach Koeffizienten falls EQUAL *)

   389 fun koeff_degree_ord (xs, ys) =

   390 	    prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));

   392 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels

   393    Gesamtgradordnung *)

   394 val sort_monList = sort koeff_degree_ord;

   396 (* Alternativ zu degree_ord koennte auch die viel einfachere und

   397    kuerzere Ordnung simple_ord verwendet werden - ist aber nicht

   398    fuer unsere Zwecke geeignet!

   400 fun simple_ord (al,bl: term list) = dict_ord string_ord

   401 	 (map get_basStr al, map get_basStr bl);

   403 val sort_monList = sort simple_ord; *)

   405 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt

   406    (mit gewuenschtem Typen T) *)

   407 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);

   408 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);

   409 fun binop op_ t1 t2 = op_ $ t1 $ t2;

   410 fun create_prod T (a,b) = binop (mult T) a b;

   411 fun create_sum T (a,b) = binop (plus T) a b;

   413 (* löscht letztes Element einer Liste *)

   414 fun drop_last l = take ((length l)-1,l);

   416 (* Liste von Variablen --> Monom *)

   417 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);

   418 (* Bemerkung:

   419    foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei

   420    gleiche Monome zusammengefasst werden können (collect_numerals)!

   421    zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)

   423 (* Liste von Monomen --> Polynom *)

   424 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);

   425 (* Bemerkung:

   426    foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -

   427    bessere Darstellung, da keine Klammern sichtbar!

   428    (und discard_parentheses in make_polynomial hat weniger zu tun) *)

   430 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)

   431 fun sort_variables t =

   432   let

   433   	val ll = map monom2list (poly2list t);

   434   	val lls = map sort_varList ll;

   435   	val T = type_of t;

   436   	val ls = map (create_monom T) lls;

   437   in create_polynom T ls end;

   439 (* sorts the monoms of an expanded and variable-sorted polynomial

   440    by total_degree *)

   441 fun sort_monoms t =

   442   let

   443   	val ll =  map monom2list (poly2list t);

   444   	val lls = sort_monList ll;

   445   	val T = Term.type_of t;

   446   	val ls = map (create_monom T) lls;

   447   in create_polynom T ls end;

   448 \<close>

   450 subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>

   451 ML \<open>

   452 local (*. for make_polynomial .*)

   454 open Term;  (* for type order = EQUAL | LESS | GREATER *)

   456 fun pr_ord EQUAL = "EQUAL"

   457   | pr_ord LESS  = "LESS"

   458   | pr_ord GREATER = "GREATER";

   460 fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)

   461   (case a of

   462      "Transcendental.powr" => ((("|||||||||||||", 0), T), 0)    (*WN greatest string*)

   463    | _ => (((a, 0), T), 0))

   464   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)

   465   | dest_hd' (Var v) = (v, 2)

   466   | dest_hd' (Bound i) = ((("", i), dummyT), 3)

   467   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)

   468   | dest_hd' t = raise TERM ("dest_hd'", [t]);

   470 fun size_of_term' (Const(str,_) $ t) =

   471   if "Transcendental.powr"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)

   472   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body

   473   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t

   474   | size_of_term' _ = 1;

   476 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

   477     (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)

   478   | term_ord' pr thy (t, u) =

   479     (if pr then

   480 	   let

   481        val (f, ts) = strip_comb t and (g, us) = strip_comb u;

   482        val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^

   483          commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");

   484        val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^

   485          commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");

   486        val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^

   487          string_of_int (size_of_term' u) ^ ")");

   488        val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o hd_ord) (f,g));

   489        val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));

   490        val _ = tracing ("-------");

   491      in () end

   492        else ();

   493 	 case int_ord (size_of_term' t, size_of_term' u) of

   494 	   EQUAL =>

   495 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in

   496 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)

   497 	     | ord => ord)

   498 	     end

   499 	 | ord => ord)

   500 and hd_ord (f, g) =                                        (* ~ term.ML *)

   501   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)

   502 and terms_ord _ pr (ts, us) =

   503     list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);

   505 in

   507 fun ord_make_polynomial (pr:bool) thy (_: subst) tu =

   508     (term_ord' pr thy(***) tu = LESS );

   510 end;(*local*)

   512 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)

   513 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);

   514 \<close>

   516 subsection \<open>predicates\<close>

   517 subsubsection \<open>in specifications\<close>

   518 ML \<open>

   519 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)

   520 fun is_polyrat_in t v =

   521   let

   522    	fun finddivide (_ $ _ $ _ $ _) _ = raise ERROR("is_polyrat_in:")

   523 	    (* at the moment there is no term like this, but ....*)

   524 	  | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)

   525 	  | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v

   526 	  | finddivide (_ $ t1) v = finddivide t1 v

   527 	  | finddivide _ _ = false;

   528   in finddivide t v end;

   530 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;

   531 fun is_poly_in t v =     case poly_deg_in t v of SOME _ => true | NONE => false;

   532 fun has_degree_in t v =  case expand_deg_in t v of SOME d => d | NONE => ~1;

   534 (*.the expression contains + - * ^ only ?

   535    this is weaker than 'is_polynomial' !.*)

   536 fun is_polyexp (Free _) = true

   537   | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)

   538   | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ num) =

   539     if TermC.is_num num then true

   540     else if TermC.is_variable num then true

   541     else is_polyexp num

   542   | is_polyexp (Const ("Groups.plus_class.plus",_) $ num $ Free _) =

   543     if TermC.is_num num then true

   544     else if TermC.is_variable num then true

   545     else is_polyexp num

   546   | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ num) =

   547     if TermC.is_num num then true

   548     else if TermC.is_variable num then true

   549     else is_polyexp num

   550   | is_polyexp (Const ("Groups.times_class.times",_) $ num $ Free _) =

   551     if TermC.is_num num then true

   552     else if TermC.is_variable num then true

   553     else is_polyexp num

   554   | is_polyexp (Const ("Transcendental.powr",_) $ Free _ $ num) =

   555     if TermC.is_num num then true

   556     else if TermC.is_variable num then true

   557     else is_polyexp num

   558   | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

   559     ((is_polyexp t1) andalso (is_polyexp t2))

   560   | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =

   561     ((is_polyexp t1) andalso (is_polyexp t2))

   562   | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =

   563     ((is_polyexp t1) andalso (is_polyexp t2))

   564   | is_polyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =

   565     ((is_polyexp t1) andalso (is_polyexp t2))

   566   | is_polyexp num = TermC.is_num num;

   567 \<close>

   569 subsubsection \<open>for hard-coded AC rewriting\<close>

   570 ML \<open>

   571 (* auch Klammerung muss übereinstimmen;

   572    sort_variables klammert Produkte rechtslastig*)

   573 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));

   575 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));

   576 \<close>

   578 subsection \<open>evaluations functions\<close>

   579 subsubsection \<open>for predicates\<close>

   580 ML \<open>

   581 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is_polyrat_in",_) $ t $ v)) _  =

   582     if is_polyrat_in t v

   583     then SOME ((UnparseC.term p) ^ " = True",

   584 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   585     else SOME ((UnparseC.term p) ^ " = True",

   586 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

   587   | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);

   589 (*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)

   590 fun eval_is_expanded_in _ _

   591        (p as (Const ("Poly.is_expanded_in",_) $ t $ v)) _ =

   592     if is_expanded_in t v

   593     then SOME ((UnparseC.term p) ^ " = True",

   594 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   595     else SOME ((UnparseC.term p) ^ " = True",

   596 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

   597   | eval_is_expanded_in _ _ _ _ = NONE;

   599 (*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)

   600 fun eval_is_poly_in _ _

   601        (p as (Const ("Poly.is_poly_in",_) $ t $ v)) _ =

   602     if is_poly_in t v

   603     then SOME ((UnparseC.term p) ^ " = True",

   604 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

   605     else SOME ((UnparseC.term p) ^ " = True",

   606 	        HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

   607   | eval_is_poly_in _ _ _ _ = NONE;

   609 (*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)

   610 fun eval_has_degree_in _ _

   611 	     (p as (Const ("Poly.has_degree_in",_) $ t $ v)) _ =

   612     let val d = has_degree_in t v

   613 	val d' = TermC.term_of_num HOLogic.realT d

   614     in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),

   615 	      HOLogic.Trueprop $ (TermC.mk_equality (p, d')))

   616     end

   617   | eval_has_degree_in _ _ _ _ = NONE;

   619 (*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)

   620 fun eval_is_polyexp (thmid:string) _

   621 		       (t as (Const("Poly.is_polyexp", _) $ arg)) thy =

   622     if is_polyexp arg

   623     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   624 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   625     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   626 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   627   | eval_is_polyexp _ _ _ _ = NONE;

   628 \<close>

   630 subsubsection \<open>for hard-coded AC rewriting\<close>

   631 ML \<open>

   632 (*WN.18.6.03 *)

   633 (*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)

   634 fun eval_is_addUnordered (thmid:string) _

   635 		       (t as (Const("Poly.is_addUnordered", _) $ arg)) thy =

   636     if is_addUnordered arg

   637     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   638 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   639     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   640 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   641   | eval_is_addUnordered _ _ _ _ = NONE;

   643 fun eval_is_multUnordered (thmid:string) _

   644 		       (t as (Const("Poly.is_multUnordered", _) $ arg)) thy =

   645     if is_multUnordered arg

   646     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   647 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   648     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

   649 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

   650   | eval_is_multUnordered _ _ _ _ = NONE;

   651 \<close>

   654 section \<open>2============== NEW src/../"Knowledge/Rational.thy" ================= ==============\<close>

   655 section \<open>Cancellation and addition of fractions\<close>

   656 subsection \<open>Conversion term <--> poly\<close>

   657 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>

   658 ML \<open>

   659 val mon1 = (1, [1,2,3]): monom;

   660 val mon2 = (~4, [5,6,7]): monom;

   661 val poly = [mon1, mon2]: poly

   662 \<close> ML \<open>

   663 fun monom_uminus ((c, ps): monom) = (~1 * c, ps): monom;

   664 fun poly_uminus (ms: poly) = map monom_uminus ms: poly;

   665 \<close> ML \<open>

   666 poly_uminus poly = [(~1, [1, 2, 3]), (4, [5, 6, 7])]

   667 \<close> ML \<open>

   668 fun monom_of_term vs (c, es) (t as Const _) =

   669     (c, list_update es (find_index (curry op = t) vs) 1)

   670   | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =

   671     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)

   672   | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =

   673     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)

   674   | monom_of_term  vs (c, es) (t as Free _) =

   675     (c, list_update es (find_index (curry op = t) vs) 1)

   676   | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $

   677       (e as Const ("Num.numeral_class.numeral", _) $ _)) =

   678     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))

   679   | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $

   680       (e as Const ("Groups.uminus_class.uminus", _) $ _)) =

   681     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))

   682   | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =

   683     let val (c', es') = monom_of_term vs (c, es) m1

   684     in monom_of_term vs (c', es') m2 end

   685   | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)

   687 fun monom_of_term vs (c, es) (t as Const _) =

   688     (c, list_update es (find_index (curry op = t) vs) 1)

   689   | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =

   690     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)

   691   | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =

   692     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)

   693   | monom_of_term  vs (c, es) (t as Free _) =

   694     (c, list_update es (find_index (curry op = t) vs) 1)

   695   | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $

   696       (e as Const ("Num.numeral_class.numeral", _) $ _)) =

   697     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))

   698   | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $

   699       (e as Const ("Groups.uminus_class.uminus", _) $ _)) =

   700     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))

   701   | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =

   702     let val (c', es') = monom_of_term vs (c, es) m1

   703     in monom_of_term vs (c', es') m2 end

   704   | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)

   706 (*-------v------*)

   707 fun monoms_of_term vs (t as Const _) =

   708     [monom_of_term  vs (1, replicate (length vs) 0) t]

   709   | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =

   710     [monom_of_term  vs (1, replicate (length vs) 0) t]

   711   | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =

   712     [monom_of_term  vs (1, replicate (length vs) 0) t]

   713   | monoms_of_term vs (t as Free _) =

   714     [monom_of_term  vs (1, replicate (length vs) 0) t]

   715   | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $  _) =

   716     [monom_of_term  vs (1, replicate (length vs) 0) t]

   717   | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $  _) =

   718     [monom_of_term  vs (1, replicate (length vs) 0) t]

   719   | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =

   720     (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)

   721   | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)

   723 fun monoms_of_term vs (t as Const _) =

   724     [monom_of_term  vs (1, replicate (length vs) 0) t]

   725   | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =

   726     [monom_of_term  vs (1, replicate (length vs) 0) t]

   727   | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =

   728     [monom_of_term  vs (1, replicate (length vs) 0) t]

   729   | monoms_of_term vs (t as Free _) =

   730     [monom_of_term  vs (1, replicate (length vs) 0) t]

   731   | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $  _) =

   732     [monom_of_term  vs (1, replicate (length vs) 0) t]

   733   | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $  _) =

   734     [monom_of_term  vs (1, replicate (length vs) 0) t]

   735   | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =

   736     (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)

   737   | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)

   739 (* convert a term to the internal representation of a multivariate polynomial;

   740   the conversion is quite liberal, see test --- fun poly_of_term ---:

   741 * the order of variables and the parentheses within a monomial are arbitrary

   742 * the coefficient may be somewhere

   743 * he order and the parentheses within monomials are arbitrary

   744 But the term must be completely expand + over * (laws of distributivity are not applicable).

   746 The function requires the free variables as strings already given,

   747 because the gcd involves 2 polynomials (with the same length for their list of exponents).

   748 *)

   749 fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =

   750     (SOME (t |> monoms_of_term vs |> order)

   751       handle ERROR _ => NONE)

   752 (*| poly_of_term vs (t as Const ("Groups.minus_class.minus", _) $ _ $ _) =

   753     (SOME (t |> monoms_of_term vs |> order)

   754       handle ERROR _ => NONE)

   755 ------------------------------------------------------ this is handled ahead by rewriting *)

   756   | poly_of_term vs t =

   757     (SOME [monom_of_term vs (1, replicate (length vs) 0) t]

   758       handle ERROR _ => NONE)

   760 fun is_poly t =

   761   let

   762     val vs = TermC.vars_of t

   763   in

   764     case poly_of_term vs t of SOME _ => true | NONE => false

   765   end

   766 val is_expanded = is_poly   (* TODO: check names *)

   767 val is_polynomial = is_poly (* TODO: check names *)

   768 \<close>

   770 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>

   771 ML \<open>

   772 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)

   773   | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es

   774   | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es

   775   | term_of_es baseT expT (v :: vs) (e :: es) =

   776     Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)

   777     :: term_of_es baseT expT vs es

   778   | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"

   780 fun term_of_monom baseT expT vs ((c, es): monom) =

   781     let val es' = term_of_es baseT expT vs es

   782     in

   783       if c = 1

   784       then

   785         if es' = [] (*if es = [0,0,0,...]*)

   786         then HOLogic.mk_number baseT c

   787         else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')

   788       else foldl (HOLogic.mk_binop "Groups.times_class.times")

   789         (HOLogic.mk_number baseT c, es')

   790     end

   792 fun term_of_poly baseT expT vs p =

   793   let val monos = map (term_of_monom baseT expT vs) p

   794   in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end

   795 \<close>

   797 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>

   798 ML \<open>

   799 fun mk_noteq_0 baseT t =

   800   Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $

   801     (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)

   803 fun mk_asms baseT ts =

   804   let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)

   805   in map (mk_noteq_0 baseT) as' end

   806 \<close>

   808 subsubsection \<open>Factor out gcd for cancellation\<close>

   809 ML \<open>

   810 fun check_fraction t =

   811   case t of

   812     Const ("Rings.divide_class.divide", _) $ numerator $ denominator

   813       => SOME (numerator, denominator)

   814   | _ => NONE

   816 (* prepare a term for cancellation by factoring out the gcd

   817   assumes: is a fraction with outmost "/"*)

   818 fun factout_p_ (thy: theory) t =

   819   let val opt = check_fraction t

   820   in

   821     case opt of

   822       NONE => NONE

   823     | SOME (numerator, denominator) =>

   824       let

   825         val vs = TermC.vars_of t

   826         val baseT = type_of numerator

   827         val expT = HOLogic.realT

   828       in

   829         case (poly_of_term vs numerator, poly_of_term vs denominator) of

   830           (SOME a, SOME b) =>

   831             let

   832               val ((a', b'), c) = gcd_poly a b

   833               val es = replicate (length vs) 0

   834             in

   835               if c = [(1, es)] orelse c = [(~1, es)]

   836               then NONE

   837               else

   838                 let

   839                   val b't = term_of_poly baseT expT vs b'

   840                   val ct = term_of_poly baseT expT vs c

   841                   val t' =

   842                     HOLogic.mk_binop "Rings.divide_class.divide"

   843                       (HOLogic.mk_binop "Groups.times_class.times"

   844                         (term_of_poly baseT expT vs a', ct),

   845                        HOLogic.mk_binop "Groups.times_class.times" (b't, ct))

   846                 in SOME (t', mk_asms baseT [b't, ct]) end

   847             end

   848         | _ => NONE : (term * term list) option

   849       end

   850   end

   851 \<close>

   853 subsubsection \<open>Cancel a fraction\<close>

   854 ML \<open>

   855 (* cancel a term by the gcd ("" denote terms with internal algebraic structure)

   856   cancel_p_ :: theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option

   857   cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])

   858   assumes: a is_polynomial  \<and>  b is_polynomial  \<and>  b \<noteq> 0

   859   yields

   860     SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1  \<and>  gcd_poly a b \<noteq> -1  \<and>

   861       a' * gcd_poly a b = a  \<and>  b' * gcd_poly a b = b

   862     \<or> NONE *)

   863 fun cancel_p_ (_: theory) t =

   864   let val opt = check_fraction t

   865   in

   866     case opt of

   867       NONE => NONE

   868     | SOME (numerator, denominator) =>

   869       let

   870         val vs = TermC.vars_of t

   871         val baseT = type_of numerator

   872         val expT = HOLogic.realT

   873       in

   874         case (poly_of_term vs numerator, poly_of_term vs denominator) of

   875           (SOME a, SOME b) =>

   876             let

   877               val ((a', b'), c) = gcd_poly a b

   878               val es = replicate (length vs) 0

   879             in

   880               if c = [(1, es)] orelse c = [(~1, es)]

   881               then NONE

   882               else

   883                 let

   884                   val bt' = term_of_poly baseT expT vs b'

   885                   val ct = term_of_poly baseT expT vs c

   886                   val t' =

   887                     HOLogic.mk_binop "Rings.divide_class.divide"

   888                       (term_of_poly baseT expT vs a', bt')

   889                   val asm = mk_asms baseT [bt']

   890                 in SOME (t', asm) end

   891             end

   892         | _ => NONE : (term * term list) option

   893       end

   894   end

   895 \<close>

   897 subsubsection \<open>Factor out to a common denominator for addition\<close>

   898 ML \<open>

   899 (* addition of fractions allows (at most) one non-fraction (a monomial) *)

   900 fun check_frac_sum

   901     (Const ("Groups.plus_class.plus", _) $

   902       (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $

   903       (Const ("Rings.divide_class.divide", _) $ n2 $ d2))

   904     = SOME ((n1, d1), (n2, d2))

   905   | check_frac_sum

   906     (Const ("Groups.plus_class.plus", _) $

   907       nofrac $

   908       (Const ("Rings.divide_class.divide", _) $ n2 $ d2))

   909     = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))

   910   | check_frac_sum

   911     (Const ("Groups.plus_class.plus", _) $

   912       (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $

   913       nofrac)

   914     = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))

   915   | check_frac_sum _ = NONE

   917 (* prepare a term for addition by providing the least common denominator as a product

   918   assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)

   919 fun common_nominator_p_ (_: theory) t =

   920   let val opt = check_frac_sum t

   921   in

   922     case opt of

   923       NONE => NONE

   924     | SOME ((n1, d1), (n2, d2)) =>

   925       let

   926         val vs = TermC.vars_of t

   927       in

   928         case (poly_of_term vs d1, poly_of_term vs d2) of

   929           (SOME a, SOME b) =>

   930             let

   931               val ((a', b'), c) = gcd_poly a b

   932               val (baseT, expT) = (type_of n1, HOLogic.realT)

   933               val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]

   934               (*----- minimum of parentheses & nice result, but breaks tests: -------------

   935               val denom = HOLogic.mk_binop "Groups.times_class.times"

   936                 (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)

   937               val denom =

   938                 if c = [(1, replicate (length vs) 0)]

   939                 then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')

   940                 else

   941                   HOLogic.mk_binop "Groups.times_class.times" (c',

   942                   HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)

   943               val t' =

   944                 HOLogic.mk_binop "Groups.plus_class.plus"

   945                   (HOLogic.mk_binop "Rings.divide_class.divide"

   946                     (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),

   947                   HOLogic.mk_binop "Rings.divide_class.divide"

   948                     (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))

   949               val asm = mk_asms baseT [d1', d2', c']

   950             in SOME (t', asm) end

   951         | _ => NONE : (term * term list) option

   952       end

   953   end

   954 \<close>

   956 subsubsection \<open>Addition of at least one fraction within a sum\<close>

   957 ML \<open>

   958 (* add fractions

   959   assumes: is a term with outmost "+" and at least one outmost "/" in respective summands

   960   NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)

   961 fun add_fraction_p_ (_: theory) t =

   962   case check_frac_sum t of

   963     NONE => NONE

   964   | SOME ((n1, d1), (n2, d2)) =>

   965     let

   966       val vs = TermC.vars_of t

   967     in

   968       case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of

   969         (SOME _, SOME a, SOME _, SOME b) =>

   970           let

   971             val ((a', b'), c) = gcd_poly a b

   972             val (baseT, expT) = (type_of n1, HOLogic.realT)

   973             val nomin = term_of_poly baseT expT vs

   974               (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))

   975             val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')

   976             val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)

   977           in SOME (t', mk_asms baseT [denom]) end

   978       | _ => NONE : (term * term list) option

   979     end

   980 \<close>

   982 section \<open>Embed cancellation and addition into rewriting\<close>

   983 ML \<open>val thy = @{theory}\<close>

   984 subsection \<open>Rulesets and predicate for embedding\<close>

   985 ML \<open>

   986 (* evaluates conditions in calculate_Rational *)

   987 val calc_rat_erls =

   988   prep_rls'

   989     (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

   990       erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

   991       rules =

   992         [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

   993         Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),

   994         Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),

   995         Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],

   996       scr = Rule.Empty_Prog});

   998 (* simplifies expressions with numerals;

   999    does NOT rearrange the term by AC-rewriting; thus terms with variables

  1000    need to have constants to be commuted together respectively           *)

  1001 val calculate_Rational =

  1002   prep_rls' (Rule_Set.merge "calculate_Rational"

  1003     (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

  1004       erls = calc_rat_erls, srls = Rule_Set.Empty,

  1005       calc = [], errpatts = [],

  1006       rules =

  1007         [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),

  1009         Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),

  1010           (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)

  1011         Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),

  1012           (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \

  1013           \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)

  1014         Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),

  1015           (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)

  1016         Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),

  1017           (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)

  1018         Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),

  1019           (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\

  1020           .... is_const to be omitted here FIXME*)

  1022         Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),

  1023           (*a / b * (c / d) = a * c / (b * d)*)

  1024         Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),

  1025           (*?x * (?y / ?z) = ?x * ?y / ?z*)

  1026         Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),

  1027           (*?y / ?z * ?x = ?y * ?x / ?z*)

  1029         Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),

  1030           (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)

  1031         Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),

  1032           (*"?x / ?y / ?z = ?x / (?y * ?z)"*)

  1034         Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),

  1035           (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)

  1037         Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),

  1038           (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)

  1039         Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),

  1040           (*"   b ~= 0            ==> (a / b = c    ) = (a     = b * c)*)

  1041         Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})

  1042           (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)],

  1043       scr = Rule.Empty_Prog})

  1044     calculate_Poly);

  1046 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)

  1047 fun eval_is_expanded (thmid:string) _

  1048 		       (t as (Const("Rational.is_expanded", _) $ arg)) thy =

  1049     if is_expanded arg

  1050     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

  1051 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  1052     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",

  1053 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

  1054   | eval_is_expanded _ _ _ _ = NONE;

  1055 \<close> ML \<open>

  1056 \<close> ML \<open>

  1057 \<close>

  1059 section \<open>===================================================================================\<close>

  1060 ML \<open>

  1061 \<close> ML \<open>

  1062 \<close> ML \<open>

  1063 \<close> ML \<open>

  1064 \<close>

  1067 section \<open>====== check test/../rational.sml =================================================\<close>

  1068 ML \<open>

  1069 \<close> ML \<open>

  1070 (* Title: tests for rationals

  1071    Author: Walther Neuper

  1072    Use is subject to license terms.

  1073 *)

  1075 "-----------------------------------------------------------------------------";

  1076 "-----------------------------------------------------------------------------";

  1077 "table of contents -----------------------------------------------------------";

  1078 "-----------------------------------------------------------------------------";

  1079 "-------- fun poly_of_term ---------------------------------------------------";

  1080 "-------- fun is_poly --------------------------------------------------------";

  1081 "-------- fun term_of_poly ---------------------------------------------------";

  1082 "-------- integration lev.1 fun factout_p_ -----------------------------------";

  1083 "-------- integration lev.1 fun cancel_p_ ------------------------------------";

  1084 "-------- integration lev.1 fun common_nominator_p_ --------------------------";

  1085 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";

  1086 "Rfuns-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";

  1087 "Rfuns-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";

  1088 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";

  1089 "Rfuns-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";

  1090 "----------- rewrite_set_ Partial_Fractions norm_Rational --------------------------------------";

  1091 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";

  1092 "----------- fun cancel_p with Const AA --------------------------------------------------------";

  1093 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";

  1094 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";

  1095 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";

  1096 "Rfuns-------- reverse rewrite ----------------------------------------------------";

  1097 "Rfuns-------- 'reverse-ruleset' cancel_p -----------------------------------------";

  1098 "-------- investigate rls norm_Rational --------------------------------------";

  1099 "-------- examples: rls norm_Rational ----------------------------------------";

  1100 "-------- rational numerals --------------------------------------------------";

  1101 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";

  1102 "-------- examples common denominator from: Mathematik 1 Schalk --------------";

  1103 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";

  1104 "-------- examples common denominator and multiplication from: Schalk --------";

  1105 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";

  1106 "-------- me Schalk I No.186 -------------------------------------------------";

  1107 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";

  1108 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";

  1109 "-------- investigate rulesets for cancel_p ----------------------------------";

  1110 "-------- fun eval_get_denominator -------------------------------------------";

  1111 "-------- several errpats in complicated term --------------------------------";

  1112 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

  1113 "-----------------------------------------------------------------------------";

  1114 "-----------------------------------------------------------------------------";

  1117 \<close> ML \<open>

  1118 "-------- fun poly_of_term ---------------------------------------------------";

  1119 "-------- fun poly_of_term ---------------------------------------------------";

  1120 "-------- fun poly_of_term ---------------------------------------------------";

  1121 val thy = @{theory Partial_Fractions};

  1122 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");

  1124 val t = TermC.str2term "-3 + -2 * x ::real";

  1125 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]

  1126 then () else error "poly_of_term uminus changed";

  1128 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)

  1129 \<close> ML \<open>

  1130 val t = TermC.str2term "x/2 - -(3*x - 2)/9";

  1131 \<close> ML \<open>

  1132 val NONE = poly_of_term vs t; (*COMPARE norm_Rational: exception TERM dest_number  - 3 + 13 * x

  1133  BUT: this raises no exn ! ! !*)

  1134 \<close> ML \<open>

  1135 Rewrite.trace_on := false;

  1136 \<close> text \<open>

  1137 Rewrite.trace_on := true;

  1138 \<close> ML \<open> (*norm_Rational: exception TERM raised dest_number  - 2 + 3 * x*)

  1139 val SOME (t', _) = rewrite_set_ thy false norm_Rational t;

  1140 \<close> ML \<open>

  1141 @{thm real_mult_minus1}

  1142 \<close> ML \<open>

  1144 @{term 0};

  1145 \<close> ML \<open>

  1146 "----------- fun is_atom -----------------------------------------------------------------------";

  1147 "----------- fun is_atom -----------------------------------------------------------------------";

  1148 "----------- fun is_atom -----------------------------------------------------------------------";

  1149 \<close> ML \<open>

  1150 \<close> ML \<open>

  1151 if is_atom @{term 0} then () else error "is_atom 1 CHANGED";

  1152 val eval_t = @{term "1 is_atom"};

  1153 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  1154   SOME ("#is_atom__", _) => ()

  1155 | _ => error "eval_is_atom 1 CHANGED";

  1156 \<close> ML \<open>

  1157 Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()

  1158 \<close> ML \<open>

  1159 \<close> ML \<open>

  1160 \<close> ML \<open>

  1161 if is_atom @{term 1} then () else error "is_atom 1 CHANGED";

  1162 val eval_t = @{term "1 is_atom"};

  1163 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  1164   SOME ("#is_atom__", _) => ()

  1165 | _ => error "eval_is_atom 1 CHANGED";

  1166 \<close> ML \<open>

  1167 Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t ()

  1168 \<close> ML \<open>

  1169 \<close> ML \<open>

  1170 \<close> ML \<open>

  1171 val eval_t = @{term "0 is_atom"};

  1172 \<close> text \<open>

  1173 string_of_atom

  1174 \<close> ML \<open>

  1175 \<close> ML \<open>

  1176 \<close> ML \<open>

  1177 \<close> ML \<open>

  1178 \<close> ML \<open>

  1179 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)

  1181 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]

  1182 then () else error "poly_of_term 1 changed";

  1184 if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]

  1185 then () else error "poly_of_term 2 changed";

  1187 if         poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]

  1188 then () else error "poly_of_term 3 changed";

  1189 "~~~~~ fun poly_of_term , args:"; val (vs, t) =

  1190   (vs, (TermC.str2term "12 * x \<up> 3"));

  1192            monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)

  1193 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Groups.times_class.times", _) $ m1 $ m2)) =

  1194   (vs, (1, replicate (length vs) 0), t);

  1195     val (c', es') =

  1197            monom_of_term vs (c, es) m1;

  1198 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Transcendental.powr", _) $ (t as Free _) $ (Const ("Num.numeral_class.numeral", _) $ num)) ) =

  1199   (vs, (c', es'), m2);

  1200 (*+*)c = 12;

  1201 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];

  1203 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])

  1204 then () else error "monom_of_term (powr): return value CHANGED";

  1206 if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]

  1207 then () else error "poly_of_term 4 changed";

  1209 if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =

  1210   SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]

  1211 then () else error "poly_of_term 5 changed";

  1213 (*poly_of_term is quite liberal:*)

  1214 (*the coefficient may be somewhere, the order of variables and the parentheses

  1215   within a monomial are arbitrary*)

  1216 if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]

  1217 then () else error "poly_of_term 6 changed";

  1219 (*there may even be more than 1 coefficient:*)

  1220 if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]

  1221 then () else error "poly_of_term 7 changed";

  1223 (*the order and the parentheses within monomials are arbitrary:*)

  1224 if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")

  1225   = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]

  1226 then () else error "poly_of_term 8 changed";

  1228 (*from --- rls norm_Rational downto fun gcd_poly ---*)

  1229 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)

  1230   ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^

  1231   "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");

  1232 \<close> ML \<open>

  1233 "~~~~~ fun cancel_p_, args:"; val (t) = (t);

  1234 val opt = check_fraction t;

  1235 \<close> ML \<open>

  1236 val SOME (numerator, denominator) = opt

  1237 \<close> ML \<open>

  1238 (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*)

  1239 (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2";     (*isa -- isa2*)

  1240 \<close> ML \<open>

  1241         val vs = TermC.vars_of t

  1242 \<close> ML \<open>

  1243 UnparseC.terms vs = "[\"x\", \"y\"]";

  1244 \<close> ML \<open>

  1245         val baseT = type_of numerator

  1246         val expT = HOLogic.realT;

  1247 \<close> ML \<open>

  1248 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator);  (*isa <> isa2*)

  1250 \<close> ML \<open>

  1251 "-------- fun is_poly --------------------------------------------------------";

  1252 "-------- fun is_poly --------------------------------------------------------";

  1253 "-------- fun is_poly --------------------------------------------------------";

  1254 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")

  1255 then () else error "is_poly 1 changed";

  1256 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))

  1257 then () else error "is_poly 2 changed";

  1259 \<close> ML \<open>

  1260 "-------- fun term_of_poly ---------------------------------------------------";

  1261 "-------- fun term_of_poly ---------------------------------------------------";

  1262 "-------- fun term_of_poly ---------------------------------------------------";

  1263 val expT = HOLogic.realT

  1264 val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";

  1265 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]

  1266 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))

  1267 (*precondition for [(c, es),...]: legth es = length vs*)

  1268 ;

  1269 if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"

  1270 then () else error "term_of_poly 1 changed";

  1272 \<close> ML \<open>

  1273 "-------- integration lev.1 fun factout_p_ -----------------------------------";

  1274 "-------- integration lev.1 fun factout_p_ -----------------------------------";

  1275 "-------- integration lev.1 fun factout_p_ -----------------------------------";

  1276 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"

  1277 val SOME (t', asm) = factout_p_ thy t;

  1278 if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))"

  1279 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t')

  1280 ;

  1281 if UnparseC.terms asm = "[\"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"

  1282 then () else error "factout_p_ asm 1 changed"

  1283 ;

  1284 val t = TermC.str2term "nothing + to_cancel ::real";

  1285 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable";

  1286 ;

  1287 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";

  1288 val SOME (t', asm) = factout_p_ thy t;

  1289 if UnparseC.term t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso

  1290   UnparseC.terms asm = "[\"1 + x \<noteq> 0\"]"

  1291 then () else error "factout_p_ 1 changed";

  1293 \<close> ML \<open>

  1294 "-------- integration lev.1 fun cancel_p_ ------------------------------------";

  1295 "-------- integration lev.1 fun cancel_p_ ------------------------------------";

  1296 "-------- integration lev.1 fun cancel_p_ ------------------------------------";

  1297 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"

  1298 val SOME (t', asm) = cancel_p_ thy t;

  1299 if (UnparseC.term t', UnparseC.terms asm) = ("(x + y) / x", "[\"x \<noteq> 0\"]")

  1300 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ UnparseC.term t')

  1301 ;

  1302 val t = TermC.str2term "nothing + to_cancel ::real";

  1303 if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable";

  1304 ;

  1305 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";

  1306 val SOME (t', asm) = cancel_p_ thy t;

  1307 if UnparseC.term t' = "(3 + 3 * x) / 2" andalso UnparseC.terms asm = "[]"

  1308 then () else error "cancel_p_ 1 changed";

  1310 \<close> ML \<open>

  1311 "-------- integration lev.1 fun common_nominator_p_ --------------------------";

  1312 "-------- integration lev.1 fun common_nominator_p_ --------------------------";

  1313 "-------- integration lev.1 fun common_nominator_p_ --------------------------";

  1314 val t = TermC.str2term ("y / (a*x + b*x + c*x) " ^

  1315               (* n1    d1                   *)

  1316                 "+ a / (x*y)");

  1317               (* n2    d2                   *)

  1318 val SOME (t', asm) = common_nominator_p_ thy t;

  1319 if UnparseC.term t' =

  1320       ("y * y / (x * ((a + b + c) * y)) " ^

  1321   (*  n1  *d2'/ (c'* ( d1'        *d2')) *)

  1322      "+ a * (a + b + c) / (x * ((a + b + c) * y))")

  1323    (*  n2 * d1'         / (c'* ( d1'        *d2')) *)

  1324 then () else error "common_nominator_p_ term 1 changed";

  1325 if UnparseC.terms asm = "[\"a + b + c \<noteq> 0\", \"y \<noteq> 0\", \"x \<noteq> 0\"]"

  1326 then () else error "common_nominator_p_ asm 1 changed"

  1328 "-------- example in mail Nipkow";

  1329 val t = TermC.str2term "x/(x \<up> 2 + -1*y \<up> 2) + y/(x \<up> 2 + -1*x*y)";

  1330 val SOME (t', asm) = common_nominator_p_ thy t;

  1331 if UnparseC.term t' =

  1332   "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))"

  1333 then () else error "common_nominator_p_ term 2 changed"

  1334 ;

  1335 if UnparseC.terms asm = "[\"x + y \<noteq> 0\", \"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"

  1336 then () else error "common_nominator_p_ asm 2 changed"

  1338 "-------- example: applicable tested by SML code";

  1339 val t = TermC.str2term "nothing / to_add";

  1340 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";

  1341 ;

  1342 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";

  1343 val SOME (t', asm) = common_nominator_p_ thy t;

  1344 if UnparseC.term t' =

  1345   "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))"

  1346   andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\", \"- 1 + x \<noteq> 0\"]"

  1347 then () else error "common_nominator_p_ 3 changed";

  1349 \<close> ML \<open>

  1350 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";

  1351 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";

  1352 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";

  1353 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";

  1354 val SOME (t', asm) = add_fraction_p_ thy t;

  1355 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)"

  1356 then () else error "add_fraction_p_ 3 changed";

  1357 ;

  1358 if UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"

  1359 then () else error "add_fraction_p_ 3 changed";

  1360 ;

  1361 val t = TermC.str2term "nothing / to_add";

  1362 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed";

  1363 ;

  1364 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";

  1365 val SOME (t', asm) = add_fraction_p_ thy t;

  1366 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso

  1367   UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"

  1368 then () else error "add_fraction_p_ 3 changed";

  1370 \<close> ML \<open>

  1371 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";

  1372 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";

  1373 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";

  1374 (* trace down until prepats are evaluated

  1375   (which does not to work, because substitution is not done -- compare rew_sub!);

  1376   keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p

  1377   (again) get prepat = [] changed to <>[]. *)

  1378 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)";

  1380 (*rewrite_set_ @{theory Isac_Knowledge} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1381 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);

  1382 "~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =

  1383   (thy, 1, bool, [], rls, term);

  1384 (*val (t', asm, rew) = app_rev thy (i+1) rrls t; rew = false!!!!!!!!!!!!!!!!!!!!!*)

  1385 "~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);

  1386     fun chk_prepat thy erls [] t = true

  1387       | chk_prepat thy erls prepat t =

  1388         let

  1389           fun chk (pres, pat) =

  1390             (let

  1391               val subst: Type.tyenv * Envir.tenv =

  1392                 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

  1393              in

  1394               snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)

  1395              end) handle Pattern.MATCH => false

  1396            fun scan_ f [] = false (*scan_ NEVER called by []*)

  1397              | scan_ f (pp::pps) =

  1398                if f pp then true else scan_ f pps;

  1399         in scan_ chk prepat end;

  1400     (* apply the normal_form of a rev-set *)

  1401     fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =

  1402       if chk_prepat thy erls prepat t

  1403       then ((*tracing("### app_rev': t = "^UnparseC.term t);*) normal_form t)

  1404       else NONE;

  1405 (*  val opt = app_rev' thy rrls t  ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1406 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =

  1407   (thy, rrls, t);

  1408 (* chk_prepat thy erls prepat t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1409 (* app_sub thy i rrls t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1410 "~~~~~ fun chk_prepat, args:"; val (thy, erls, prepat, t) = (thy, erls, prepat, t);

  1411           fun chk (pres, pat) =

  1412             (let

  1413               val subst: Type.tyenv * Envir.tenv =

  1414                 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

  1415              in

  1416               snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)

  1417              end) handle Pattern.MATCH => false

  1418            fun scan_ f [] = false (*scan_ NEVER called by []*)

  1419              | scan_ f (pp::pps) =

  1420                if f pp then true else scan_ f pps;

  1422 (*========== inhibit exn WN130823: prepat is empty ====================================

  1423 (* scan_ chk prepat = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1424 "~~~~~ fun , args:"; val (f, (pp::pps)) = (chk, prepat);

  1425 f;

  1426 val ([t1, t2], t) = pp;

  1427 UnparseC.term t1 = "?r is_expanded";

  1428 UnparseC.term t2 = "?s is_expanded";

  1429 UnparseC.term t = "?r / ?s";

  1430 (* f pp = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1431 "~~~~~ fun chk, args:"; val (pres, pat) = (pp);

  1432               val subst: Type.tyenv * Envir.tenv =

  1433                 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

  1434 (*subst =

  1435   ({}, {(("r", 0), ("real", Var (("r", 0), "real"))),

  1436         (("s", 0), ("real", Var (("s", 0), "real")))}*)

  1437 ;

  1438               snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)

  1439 "~~~~~ fun eval__true, args:"; val (thy, i, asms, bdv, rls) =

  1440   (thy, (i + 1), (map (Envir.subst_term subst) pres), [], erls);

  1441 UnparseC.terms asms;                         (* = "[\"?r is_expanded\",\"?s is_expanded\"]"*)

  1442 asms = [@{term True}] orelse asms = []; (* = false*)

  1443 asms = [@{term False}]                ; (* = false*)

  1444 "~~~~~ fun chk, args:"; val (indets, (a::asms)) = ([], asms);

  1445 bdv (*= []: _a list*);

  1446 val bdv : (term * term) list = [];

  1447 rewrite__set_ thy (i+1) false;

  1448 UnparseC.term a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*)

  1449 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a

  1450 ============ inhibit exn WN130823: prepat is empty ===================================*)

  1452 \<close> ML \<open>

  1453 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";

  1454 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";

  1455 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";

  1456 val t = TermC.str2term "(12 * x * y) / (8 * y \<up> 2 )";

  1457 (* "-------- example 187a": exception Div raised...

  1458 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)

  1459 val t = TermC.str2term "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )";

  1460 (* "-------- example 187b": doesn't terminate...

  1461 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)

  1462 val t = TermC.str2term "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )";

  1463 (* "-------- example 187c": doesn't terminate...

  1464 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)

  1465 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac_Knowledge}, false, cancel_p, t);

  1466 (* WN130827: exception Div raised...

  1467 rewrite__set_ thy 1 bool [] rls term

  1468 *)

  1469 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =

  1470   (thy, 1, bool, [], rls, term);

  1471 (* WN130827: exception Div raised...

  1472 	val (t', asm, rew) = app_rev thy (i+1) rrls t

  1473 *)

  1474 "~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);

  1475 (* WN130827: exception Div raised...

  1476     val opt = app_rev' thy rrls t

  1477 *)

  1478 "~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =

  1479   (thy, rrls, t);

  1480 chk_prepat thy erls prepat t    = true;

  1481 (* WN130827: exception Div raised...

  1482 normal_form t

  1483 *)

  1484 (* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*)

  1485 "~~~~~ fun cancel_p_, args:"; val (t) = (t);

  1486 val opt = check_fraction t;

  1487 val SOME (numerator, denominator) = opt

  1488         val vs = TermC.vars_of t

  1489         val baseT = type_of numerator

  1490         val expT = HOLogic.realT

  1491 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);

  1492 (*"-------- example 187a": exception Div raised...

  1493 val a = [(12, [1, 1])]: poly

  1494 val b = [(8, [0, 2])]: poly

  1495               val ((a', b'), c) = gcd_poly a b

  1496 *)

  1497 (* "-------- example 187b": doesn't terminate...

  1498 val a = [(8, [2, 1, 1])]: poly

  1499 val b = [(18, [1, 2, 1])]: poly

  1500               val ((a', b'), c) = gcd_poly a b

  1501 *)

  1502 (* "-------- example 187c": doesn't terminate...

  1503 val a = [(9, [5, 2, 4])]: poly

  1504 val b = [(15, [6, 3, 1])]: poly

  1505               val ((a', b'), c) = gcd_poly a b

  1506 *)

  1508 \<close> ML \<open> (*poly_of_term \<longrightarrow> NONE*)

  1509 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";

  1510 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";

  1511 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";

  1512 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";

  1513 Rewrite.trace_on := false (*true false*);

  1514 (* trace stops with ...: (and then jEdit hangs)..

  1515 rewrite_set_ thy false norm_Rational t;

  1516 :

  1517 ###  rls: cancel_p on: (-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /

  1518 (-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)

  1519 *)

  1520 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)

  1521   ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^

  1522   "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");

  1523 (*cancel_p_ thy t;

  1524 exception Div raised*)

  1526 "~~~~~ fun cancel_p_, args:"; val (t) = (t);

  1527 val opt = check_fraction t;

  1528 val SOME (numerator, denominator) = opt

  1529         val vs = TermC.vars_of t

  1530         val baseT = type_of numerator

  1531         val expT = HOLogic.realT;

  1532 (*default_print_depth 3; 999*)

  1533 \<close> ML \<open> (*poly_of_term --> NONE*)

  1534 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);

  1535 (*default_print_depth 3; 999*)

  1536 (* does not terminate instead of returning ?:

  1537         val ((a', b'), c) = gcd_poly a b

  1538 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly

  1539 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly

  1540 *)

  1542 \<close> ML \<open> (*poly_of_term \<longrightarrow> (SOME, NONE, NONE, SOME*)

  1543 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";

  1544 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";

  1545 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";

  1546 val thy =  @{theory Isac_Knowledge};

  1547 "----- SK060904-2a non-termination of add_fraction_p_";

  1548 val t = TermC.str2term (" (a + b * x) / (a + -1 * (b * x)) +  " ^

  1549 		         " (-1 * a + b * x) / (a + b * x)      ");

  1550 (* rewrite_set_ thy false norm_Rational t

  1551 exception Div raised*)

  1552 (* rewrite_set_ thy false add_fractions_p t;

  1553 exception Div raised*)

  1554 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) =

  1555   (@{theory Isac_Knowledge}, false, add_fractions_p, t);

  1556 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =

  1557   (thy, 1, bool, [], rls, term);

  1558 (* app_rev thy (i+1) rrls t;

  1559 exception Div raised*)

  1560 "~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);

  1561     fun chk_prepat thy erls [] t = true

  1562       | chk_prepat thy erls prepat t =

  1563         let

  1564           fun chk (pres, pat) =

  1565             (let

  1566               val subst: Type.tyenv * Envir.tenv =

  1567                 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

  1568              in

  1569               snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)

  1570              end) handle Pattern.MATCH => false

  1571            fun scan_ f [] = false (*scan_ NEVER called by []*)

  1572              | scan_ f (pp::pps) =

  1573                if f pp then true else scan_ f pps;

  1574         in scan_ chk prepat end;

  1575     (* apply the normal_form of a rev-set *)

  1576     fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =

  1577       if chk_prepat thy erls prepat t

  1578       then ((*tracing("### app_rev': t = "^UnparseC.term t);*) normal_form t)

  1579       else NONE;

  1580 (*  val opt = app_rev' thy rrls t;

  1581 exception Div raised*)

  1582 (*  val opt = app_rev' thy rrls t;

  1583 exception Div raised*)

  1584 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =

  1585   (thy, rrls, t);

  1586 chk_prepat thy erls prepat t = true       = true;

  1587 (*normal_form t

  1588 exception Div raised*)

  1589 (* lookup Rational.thy, val add_fractions_p: normal_form = add_fraction_p_ thy*)

  1590 (*add_fraction_p_ thy t

  1591 exception Div raised*)

  1592 "~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t);

  1593 val SOME ((n1, d1), (n2, d2)) = check_frac_sum t;

  1594 UnparseC.term n1; UnparseC.term d1; UnparseC.term n2; UnparseC.term d2;

  1595       val vs = TermC.vars_of t;

  1596 (*default_print_depth 3; 999*)

  1597 \<close> ML \<open>

  1598 val (SOME _, SOME a, SOME _, SOME b) =

  1599   (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);

  1600 (*default_print_depth 3; 999*)

  1601 (*

  1602 val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly

  1603 val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly

  1604             val ((a', b'), c) = gcd_poly a b

  1605 *)

  1607 \<close> ML \<open>

  1608 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";

  1609 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";

  1610 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";

  1611 val thy = @{theory Isac_Knowledge(*Partial_Fractions*)}

  1612 val ctxt = Proof_Context.init_global thy;

  1614 (*---------- (1) with Free A, B  ----------------------------------------------------------------*)

  1615 val t = (the o (parseNEW  ctxt)) "3 = A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";

  1616                                 (* required for applying thms in rewriting  \<up> ^*)

  1617 (* we get details from here..*)

  1619 Rewrite.trace_on := false;

  1620 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;

  1621 Rewrite.trace_on := false;

  1622 (* Rewrite.trace_on:

  1623 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)

  1624                      (* |||||||||||||||||||||||||||||||||||| *)

  1626 val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)

  1627                        "A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";

  1628 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);

  1629 val NONE = (*case*) check_frac_sum t (*of*)

  1631 (* Rewrite.trace_on:

  1632 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)

  1633                      (*         |||||||||||||||||||||||||||| *)

  1634 val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)

  1635                                "A / 4 + (B / 2 + -1 * B / (2::real))";

  1636 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);

  1637 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);

  1638 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("A"                 , "4") andalso

  1639 (*+*)   (UnparseC.term n2, UnparseC.term d2) = ("B / 2 + - 1 * B / 2", "1")

  1640 (*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + -1 * B / (2::real))) changed";

  1642 \<close> ML \<open>

  1643       val vs = TermC.vars_of t;

  1644 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =

  1645   (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);

  1647 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);

  1648 val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];

  1649 (*+*)if xxx = 1 then () else error "monom_of_term changed"

  1651 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Free (id, _))) =

  1652   (vs, (1, replicate (length vs) 0), t);

  1653 case vs of [Free ("A", _), Free ("B", _)] =>

  1654   if c = 1 andalso id = "A"

  1655   then () else error "monom_of_term Free changed 1"

  1656 | _ => error "monom_of_term Free changed 2";

  1658 (*---------- (2) with Const AA, BB --------------------------------------------------------------*)

  1659 val t = (the o (parseNEW  ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";

  1660                                     (*AA :: real*)

  1661 (* we get details from here..*)

  1663 Rewrite.trace_on := false;

  1664 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;

  1665 Rewrite.trace_on := false;

  1666 (* Rewrite.trace_on:

  1667 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)

  1668                      (* |||||||||||||||||||||||||||||||||||| *)

  1669 val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| *)

  1670                    "AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";

  1671 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);

  1672 val NONE = (*case*) check_frac_sum t (*of*)

  1674 (* Rewrite.trace_on:

  1675 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)

  1676                      (*         |||||||||||||||||||||||||||| *)

  1677 val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| *)

  1678                                "AA / 4 + (BB / 2 + -1 * BB / 2)";

  1679 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);

  1680 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);

  1681 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("AA"                 , "4") andalso

  1682 (*+*)   (UnparseC.term n2, UnparseC.term d2) = ("BB / 2 + - 1 * BB / 2", "1")

  1683 (*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + -1 * BB / 2)) changed";

  1685       val vs = TermC.vars_of t;

  1686 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =

  1687   (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);

  1689 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);

  1690 val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];

  1691 (*+*)if xxx = 1 then () else error "monom_of_term changed"

  1693 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =

  1694   (vs, (1, replicate (length vs) 0), t);

  1695 case vs of [Const ("Partial_Fractions.AA", _), Const ("Partial_Fractions.BB", _)] =>

  1696   if c = 1 andalso id = "Partial_Fractions.AA"

  1697   then () else error "monom_of_term Const changed 1"

  1698 | _ => error "monom_of_term Const changed 2";

  1700 \<close> ML \<open>

  1701 "----------- fun cancel_p with Const AA --------------------------------------------------------";

  1702 "----------- fun cancel_p with Const AA --------------------------------------------------------";

  1703 "----------- fun cancel_p with Const AA --------------------------------------------------------";

  1704 val thy = @{theory Partial_Fractions};

  1705 val ctxt = Proof_Context.init_global @{theory}

  1706 val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const ("Free ("AA", "real") *)

  1708 val SOME (t', _) = rewrite_set_ thy true cancel_p t;

  1709 case t' of

  1710   Const ("Rings.divide_class.divide", _) $ Const ("Partial_Fractions.AA", _) $

  1711     Const ("Groups.one_class.one", _) => ()

  1712 | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";

  1714 "~~~~~ fun cancel_p , args:"; val (t) = (t);

  1715 val opt = check_fraction t

  1716 val SOME (numerator, denominator) = (*case*) opt (*of*);

  1718 if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"

  1719 then () else error "check_fraction (2 * AA / 2) changed";

  1720         val vs = TermC.vars_of t;

  1721 case vs of

  1722   [Const ("Partial_Fractions.AA", _)] => ()

  1723 | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1  changed";

  1726 \<close> ML \<open>

  1727 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";

  1728 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";

  1729 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";

  1730 val thy  = @{theory "Rational"};

  1731 "-------- WN";

  1732 val t = TermC.str2term "(2 + -3 * x) / 9";

  1733 if NONE = rewrite_set_ thy false cancel_p t then ()

  1734 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled";

  1736 "-------- example 186a";

  1737 val t = TermC.str2term "(14 * x * y) / (x * y)";

  1738   is_expanded (TermC.str2term "14 * x * y");

  1739   is_expanded (TermC.str2term "x * y");

  1740 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1741 if (UnparseC.term t', UnparseC.terms asm) = ("14 / 1", "[]")

  1742 then () else error "rational.sml cancel Schalk 186a";

  1744 "-------- example 186b";

  1745 val t = TermC.str2term "(60 * a * b) / ( 15 * a  * b )";

  1746 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1747 if (UnparseC.term t', UnparseC.terms asm) = ("4 / 1", "[]")

  1748 then () else error "rational.sml cancel Schalk 186b";

  1750 "-------- example 186c";

  1751 val t = TermC.str2term "(144 * a \<up> 2 * b * c) / (12 * a * b * c)";

  1752 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1753 if (UnparseC.term t', UnparseC.terms asm) = ("12 * a / 1", "[]")

  1754 then () else error "rational.sml cancel Schalk 186c";

  1756 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! exception Div raised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

  1757   see --- fun rewrite_set_ downto fun gcd_poly ---

  1758 "-------- example 187a";

  1759 val t = TermC.str2term "(12 * x * y) / (8 * y \<up> 2 )";

  1760 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1761 if (UnparseC.term t', UnparseC.terms asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]")

  1762 then () else error "rational.sml cancel Schalk 187a";

  1763 *)

  1765 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

  1766   see --- fun rewrite_set_ downto fun gcd_poly ---

  1767 "-------- example 187b";

  1768 val t = TermC.str2term "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )";

  1769 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1770 if (UnparseC.term t', UnparseC.terms asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]")

  1771 then () else error "rational.sml cancel Schalk 187b";

  1772 *)

  1774 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

  1775   see --- fun rewrite_set_ downto fun gcd_poly ---

  1776 "-------- example 187c";

  1777 val t = TermC.str2term "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )";

  1778 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1779 if (UnparseC.term t', UnparseC.terms asm) =

  1780   ("3 * z \<up> 3 / (5 * (y * x))", "[\"3 * (z * (y \<up> 2 * x \<up> 5)) ~= 0\"]")

  1781 then () else error "rational.sml cancel Schalk 187c";

  1782 *)

  1784 \<close> ML \<open>

  1785 "-------- example 188a";

  1786 val t = TermC.str2term "(-8 + 8 * x) / (-9 + 9 * x)";

  1787   is_expanded (TermC.str2term "8 * x + -8");

  1788 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1789 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")

  1790 then () else error "rational.sml cancel Schalk 188a";

  1792 \<close> ML \<open>

  1793 val t = TermC.str2term "(8*((-1) + x))/(9*((-1) + x))";

  1794 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

  1795 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")

  1796 then () else error "rational.sml cancel Schalk make_polynomial 1";

  1798 \<close> ML \<open>

  1799 "-------- example 188b";

  1800 val t = TermC.str2term "(-15 + 5 * x) / (-18 + 6 * x)";

  1801 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1802 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]")

  1803 then () else error "rational.sml cancel Schalk 188b";

  1805 "-------- example 188c";

  1806 val t = TermC.str2term "(a + -1 * b) / (b + -1 * a)";

  1807 val SOME (t', asm) = rewrite_set_ thy false  cancel_p t;

  1808 if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]")

  1809 then () else error "rational.sml cancel Schalk 188c";

  1811 \<close> ML \<open>

  1812 is_expanded (TermC.str2term "a + -1 * b") = true;

  1813 val t = TermC.str2term "((- 1)*(b + (-1) * a))/(1*(b + (- 1) * a))";

  1814 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1815 if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]")

  1816 then () else error "rational.sml cancel Schalk make_polynomial 2";

  1818 \<close> ML \<open>

  1819 "-------- example 190a";

  1820 val t = TermC.str2term "( 27 * a \<up> 3 + 9 * a \<up> 2 + 3 * a + 1 ) / ( 27 * a \<up> 3 + 18 * a \<up> 2 + 3 * a )";

  1821 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1822 if (UnparseC.term t', UnparseC.terms asm) =

  1823   ("(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)", "[\"3 * a + 9 * a \<up> 2 \<noteq> 0\"]")

  1824 then () else error "rational.sml cancel Schalk 190a";

  1826 "-------- example 190c";

  1827 val t = TermC.str2term "((1 + 9 * a \<up> 2)*(1 + 3 * a))/((3 * a + 9 * a \<up> 2)*(1 + 3 * a))";

  1828 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1829 if (UnparseC.term t', UnparseC.terms asm) =

  1830   ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]")

  1831 then () else error "rational.sml make_polynomial Schalk 190c";

  1833 \<close> ML \<open>

  1834 "-------- example 191a";

  1835 val t = TermC.str2term "( x \<up> 2 + -1 * y \<up> 2 ) / ( x + y )";

  1836   is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  1837   is_expanded (TermC.str2term "x + y") = true;

  1838 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1839 if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]")

  1840 then () else error "rational.sml make_polynomial Schalk 191a";

  1842 \<close> ML \<open>

  1843 "-------- example 191b";

  1844 val t = TermC.str2term "((x + (- 1) * y)*(x + y))/((1)*(x + y))";

  1845 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1846 if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + - 1 * y \<up> 2) / (x + y)", "[]")

  1847 then () else error "rational.sml make_polynomial Schalk 191b";

  1849 \<close> ML \<open>

  1850 "-------- example 191c";

  1851 val t = TermC.str2term "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + -25 )";

  1852   is_expanded (TermC.str2term "9 * x \<up> 2 + -30 * x + 25") = true;

  1853   is_expanded (TermC.str2term "25 + -30*x + 9*x \<up> 2") = true;

  1854   is_expanded (TermC.str2term "-25 + 9*x \<up> 2") = true;

  1856 \<close> ML \<open>

  1857 val t = TermC.str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";

  1858 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1859 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]")

  1860 then () else error "rational.sml make_polynomial Schalk 191c";

  1862 \<close> ML \<open>

  1863 "-------- example 192b";

  1864 val t = TermC.str2term "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 *  y \<up> 3 )";

  1865 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1866 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]")

  1867 then () else error "rational.sml cancel_p Schalk 192b";

  1869 \<close> ML \<open>

  1870 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";

  1871 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1872 if (UnparseC.term t', UnparseC.terms asm) =

  1873   ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")

  1874 then () else error "rational.sml make_polynomial Schalk 192b";

  1876 \<close> ML \<open>

  1877 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";

  1878 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;

  1879 if (UnparseC.term t', UnparseC.terms asm) =

  1880   ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")

  1881 then () else error "rational.sml make_polynomial Schalk WN050929 not working";

  1883 \<close> ML \<open>

  1884 val t = TermC.str2term "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )";

  1885 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1886 if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]")

  1887 then () else error "rational.sml cancel_p Schalk 193a";

  1889 \<close> ML \<open>

  1890 "-------- example 193b";

  1891 val t = TermC.str2term "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )";

  1892 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1893 if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]")

  1894 then () else error "rational.sml cancel_p Schalk 193b";

  1896 \<close> ML \<open>

  1897 "-------- example 193c";

  1898 val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + -10 * x + 1 )";

  1899 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1900 if (UnparseC.term t', UnparseC.terms asm) =

  1901   ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]")

  1902 then () else error "rational.sml cancel_p Schalk 193c";

  1904 \<close> ML \<open>

  1905 (*WN: improved with new numerals*)

  1906 val t = TermC.str2term "(-25 + 9*x \<up> 2)/(5 + 3*x)";

  1907 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1908 if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]")

  1909 then () else error "rational.sml cancel WN 1";

  1911 \<close> ML \<open>

  1912 "-------- example heuberger";

  1913 val t = TermC.str2term ("(x \<up> 4 + x * y + x \<up> 3 * y + y \<up> 2) / " ^

  1914   "(x + 5 * x \<up> 2 + y + 5 * x * y + x \<up> 2 * y \<up> 3 + x * y \<up> 4)");

  1915 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1916 if (UnparseC.term t', UnparseC.terms asm) =

  1917   ("(x \<up> 3 + y) / (1 + 5 * x + x * y \<up> 3)", "[\"1 + 5 * x + x * y \<up> 3 \<noteq> 0\"]")

  1918 then () else error "rational.sml cancel_p heuberger";

  1920 \<close> ML \<open>

  1921 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";

  1922 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";

  1923 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";

  1924 (*deleted example 204 ... 236b at update Isabelle2012-->2013*)

  1926 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";

  1927 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";

  1928 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";

  1929 val t = TermC.str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");

  1930 "-------- gcd_poly integration level 1: works on exact term";

  1931 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";

  1932 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";

  1934 "-------- gcd_poly integration level 2: picks out ONE appropriate subterm";

  1935 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;

  1936 if UnparseC.term t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f"

  1937 then () else error "level 2, rewrite_set_ cancel_p: changed";

  1938 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t;

  1939 if UnparseC.term t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)"

  1940 then () else error "level 2, rewrite_set_ add_fractions_p: changed";

  1942 "-------- gcd_poly integration level 3: rewrites all appropriate subterms";

  1943 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;

  1944 if UnparseC.term t' = "123 = a / b + c / d + e / f"

  1945 then () else error "level 3, rewrite_set_ cancel_p_rls: changed";

  1946 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p_rls t; (*CREATE add_fractions_p_rls*)

  1947 if UnparseC.term t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"

  1948 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";

  1950 "-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";

  1951 (* simpler variant *)

  1952 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty [Rls_ cancel_p, Rls_ add_fractions_p]

  1953 val SOME (t', asm) = rewrite_set_ thy false testrls t;

  1954 (*Rewrite.trace_on := false;

  1955 #  rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)

  1956 ##  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)

  1957 ##  rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f

  1958 ##  rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f

  1959 ##  rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f

  1960 ##  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)

  1961 ##  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)

  1962 if UnparseC.term t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"

  1963 then () else error "level 4, rewrite_set_ *_p: changed";

  1965 (* complicated variant *)

  1966 val testrls_rls = Rule_Set.append_rules "testrls_rls" Rule_Set.empty [Rls_ cancel_p_rls, Rls_ add_fractions_p_rls];

  1967 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;

  1968 (*#  rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)

  1969 ##  rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)

  1970 ###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)

  1971 ###  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f

  1972 ###  rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f

  1973 ###  rls: cancel_p on: 123 = a / b + c / d + e / f

  1974 ##  rls: add_fractions_p_rls on: 123 = a / b + c / d + e / f

  1975 ###  rls: add_fractions_p on: 123 = a / b + c / d + e / f

  1976 ###  rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f

  1977 ###  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)

  1978 ##  rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)

  1979 ###  rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)

  1980 ##  rls: add_fractions_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)

  1981 ###  rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)

  1982 if UnparseC.term t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"

  1983 then () else error "level 4, rewrite_set_ *_p_rls: changed"

  1985 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";

  1986 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;

  1987 if UnparseC.term t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"

  1988 then () else error "level 5, rewrite_set_ norm_Rational: changed"

  1990 \<close> ML \<open>

  1991 "-------- reverse rewrite ----------------------------------------------------";

  1992 "-------- reverse rewrite ----------------------------------------------------";

  1993 "-------- reverse rewrite ----------------------------------------------------";

  1994 (** the term for which reverse rewriting is demonstrated **)

  1995 val t = TermC.str2term "(9 + -1 * x \<up> 2) / (9 + 6 * x + x \<up> 2)";

  1996 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,

  1997   next_rule = nex, normal_form = nor, ...},...} = cancel_p;

  1999 \<close> ML \<open>

  2000 (** normal_form produces the result in ONE step **)

  2001   val SOME (t', _) = nor t;

  2002 \<close> ML \<open>

  2003 if UnparseC.term t' = "(3 + - 1 * x) / (3 + x)" then ()

  2004 else error "rational.sml normal_form (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";

  2006 (** initialize the interpreter state used by the 'me' **)

  2007   val (t, _, revsets, _) = ini t;

  2009 if length (hd revsets) = 11 then () else error "length of revset changed";

  2010 \<close> text \<open> (*Rfuns revsets \<longrightarrow> broken*)

  2011 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =

  2012   (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)

  2013 then () else error "first element of revset changed";

  2014 if

  2015 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 \<up> 2 = ?r1 * ?r1)" andalso

  2016 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\",9 = 3 \<up> 2)" andalso

  2017 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"

  2018 andalso

  2019 (revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"

  2020 andalso

  2021 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso

  2022 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso

  2023 (revsets |> nth 1 |> nth 7 |> Rule.to_string) =

  2024   "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"

  2025 then () else error "first 7 elements in revset changed"

  2027 \<close> ML \<open>

  2028 (** find the rule 'r' to apply to term 't' **)

  2029 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_

  2030   for Isabelle2013, we don't get a working revset, but non-termination:

  2032   val SOME (r as (Thm (str, thm))) = nex revsets t;

  2033   :

  2034 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),

  2035   Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "

  2036 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),

  2037   Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))", "

  2038 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),

  2039   Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))", "

  2040 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "

  2041  :

  2042 ### Isabelle2002:

  2043   Thm ("sym_#mult_2_3", "6 = 2 * 3")

  2044 ### Isabelle2009-2 for cancel_ (not cancel_p_):

  2045 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"

  2046    andalso ThmC.string_of_thm thm =

  2047            (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}

  2048                (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()

  2049 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";

  2050 \---------------------------------------------------------------------------------------/*)

  2052 (** check, if the rule 'r' applied by the user to 't' belongs to the ruleset;

  2053   if the rule is OK, the term resulting from applying the rule is returned,too;

  2054   there might be several rule applications inbetween,

  2055   which are listed after the head in reverse order **)

  2056 (*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm";

  2057   we don't repair this, because interaction within "reverse rewriting" never worked properly:

  2059   val (r, (t, asm))::_ = loc revsets t r;

  2060 if UnparseC.term t = "(9 - x \<up> 2) / (3 \<up> 2 + 6 * x + x \<up> 2)" andalso asm = []

  2061 then () else error "rational.sml locate_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";

  2063 (* find the next rule to apply *)

  2064   val SOME (r as (Thm (str, thm))) = nex revsets t;

  2065 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso

  2066    ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}

  2067                 (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()

  2068 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";

  2070 (*check the next rule*)

  2071   val (r, (t, asm)) :: _ = loc revsets t r;

  2072 if UnparseC.term t = "(3 \<up> 2 - x \<up> 2) / (3 \<up> 2 + 6 * x + x \<up> 2)" then ()

  2073 else error "rational.sml locate_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2) II";

  2075 (*find and check the next rules, rewrite*)

  2076   val SOME r = nex revsets t;

  2077   val (r,(t,asm))::_ = loc revsets t r;

  2078 if UnparseC.term t = "(3 \<up> 2 - x \<up> 2) / (3 \<up> 2 + 2 * 3 * x + x \<up> 2)" then ()

  2079 else error "rational.sml locate_rule II";

  2081   val SOME r = nex revsets t;

  2082   val (r,(t,asm))::_ = loc revsets t r;

  2083 if UnparseC.term t = "(3 - x) * (3 + x) / (3 \<up> 2 + 2 * 3 * x + x \<up> 2)" then ()

  2084 else error "rational.sml next_rule II";

  2086   val SOME r = nex revsets t;

  2087   val (r,(t,asm))::_ = loc revsets t r;

  2088 if UnparseC.term t = "(3 - x) * (3 + x) / ((3 + x) * (3 + x))" then ()

  2089 else error "rational.sml next_rule III";

  2091   val SOME r = nex revsets t;

  2092   val (r, (t, asm)) :: _ = loc revsets t r;

  2093   val ss = UnparseC.term t;

  2094 if ss = "(3 - x) / (3 + x)" andalso UnparseC.terms asm = "[\"3 + x ~= 0\"]" then ()

  2095 else error "rational.sml: new behav. in rev-set cancel";

  2096 \--------------------------------------------------------------------------------------/*)

  2098 \<close> ML \<open>

  2099 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";

  2100 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";

  2101 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";

  2102 (*WN130909: the example below shows, why "reverse rewriting" only worked for

  2103   special cases.*)

  2105 (*the term for which reverse rewriting is demonstrated*)

  2106 val t = TermC.str2term "(9 + (-1)*x \<up> 2) / (9 + ((-6)*x + x \<up> 2))";

  2107 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,

  2108 		       next_rule=nex,normal_form=nor,...},...} = cancel_p;

  2110 (*normal_form produces the result in ONE step*)

  2111 val SOME (t', _) = nor t;

  2112 if UnparseC.term t' = "(3 + x) / (3 + - 1 * x)"

  2113 then () else error "cancel_p normal_form CHANGED";;

  2115 \<close> ML \<open>

  2116 (*initialize the interpreter state used by the 'me'*)

  2117 val SOME (t', asm) = cancel_p_ thy t;

  2118 if (UnparseC.term t', UnparseC.terms asm) = ("(3 + x) / (3 + - 1 * x)", "[\"3 + - 1 * x \<noteq> 0\"]")

  2119 then () else error "cancel_p  CHANGED";;

  2121 val (t,_,revsets,_) = ini t;

  2123 (* WN.10.10.02: dieser Fall terminiert nicht

  2124            (make_polynomial enth"alt zu viele rules)

  2125 WN060823 'init_state' requires rewriting on specified location in the term

  2126 default_print_depth 99; Rfuns; default_print_depth 3;

  2127 WN060831 cycling "sym_order_mult_rls_" "sym_mult.assoc"

  2128          as was with make_polynomial before ?!?*)

  2130 val SOME r = nex revsets t;

  2131 (*

  2132 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",

  2133 		mk_thm thy "9 = 3 \<up> 2"));

  2134 *)

  2136 \<close> ML \<open>

  2137 "-------- examples: rls norm_Rational ----------------------------------------";

  2138 "-------- examples: rls norm_Rational ----------------------------------------";

  2139 "-------- examples: rls norm_Rational ----------------------------------------";

  2140 val t = TermC.str2term "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";

  2141 \<close> ML \<open>

  2142 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2143 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";

  2145 \<close> ML \<open>

  2146 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";

  2147 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2148 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()

  2149 else error "rational.sml 2";

  2151 \<close> ML \<open>

  2152 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";

  2153 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2154 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()

  2155 else error "rational.sml 3";

  2157 \<close> ML \<open>

  2158 (*Rewrite.trace_on:=true;*)

  2159 val t = TermC.str2term "Not (6*x is_atom)";

  2160 val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';

  2161 "HOL.True";

  2162 val t = TermC.str2term "1 < 2";

  2163 val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';

  2164 "HOL.True";

  2166 \<close> ML \<open>

  2167 val t = TermC.str2term "(6*x) \<up> 2";

  2168 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false

  2169 			   (ThmC.numerals_to_Free @{thm realpow_def_atom}) t;

  2170 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()

  2171 else error "rational.sml powers_erls (6*x) \<up> 2";

  2173 \<close> ML \<open>

  2174 val t = TermC.str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";

  2175 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2176 if UnparseC.term t' = "65 * x / 2" then () else error "rational.sml 4";

  2178 \<close> ML \<open>

  2179 val t = TermC.str2term "1 - ((13*x)/2 - 5/2) \<up> 2";

  2180 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2181 if UnparseC.term t' = "(- 21 + 130 * x + - 169 * x \<up> 2) / 4" then ()

  2182 else error "rational.sml 5";

  2184 \<close> ML \<open>

  2185 (*SRAM Schalk I, p.92 Nr. 609a*)

  2186 val t = TermC.str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";

  2187 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2188 if UnparseC.term t' = "(- 255 + 112 * x) / 135" then ()

  2189 else error "rational.sml 6";

  2191 \<close> ML \<open>

  2192 (*SRAM Schalk I, p.92 Nr. 610c*)

  2193 val t = TermC.str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";

  2194 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2195 if UnparseC.term t' = "(3 + x) / - 2" then () else error "rational.sml 7";

  2197 \<close> ML \<open>

  2198 (*SRAM Schalk I, p.92 Nr. 476a*)

  2199 val t = TermC.str2term "(x \<up> 2/(1 - x \<up> 2) + 1)/(x/(1 - x) + 1) * (1 + x)";

  2200 (*. a/b : c/d translated to a/b * d/c .*)

  2201 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2202 if UnparseC.term t' = "1" then () else error "rational.sml 8";

  2204 \<close> ML \<open>

  2205 (*Schalk I, p.92 Nr. 472a*)

  2206 val t = TermC.str2term "((8*x \<up> 2 - 32*y \<up> 2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";

  2207 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  2208 if UnparseC.term t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";

  2210 \<close> ML \<open>

  2211 (*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*)

  2213 (*WN130910 add_fractions_p exception Div raised + history:

  2214 ### WN.2.6.03 from rlang.sml 56a

  2215 val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + -1 * b \<up> 2)";

  2216 val NONE = rewrite_set_ thy false add_fractions_p t;

  2218 THE ERROR ALREADY OCCURS IN THIS PART:

  2219 val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";

  2220 val NONE = add_fraction_p_ thy t;

  2222 SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised ===

  2223 *)

  2225 \<close> ML \<open>

  2226 "-------- rational numerals --------------------------------------------------";

  2227 "-------- rational numerals --------------------------------------------------";

  2228 "-------- rational numerals --------------------------------------------------";

  2229 (*SRA Schalk I, p.40 Nr. 164b *)

  2230 val t = TermC.str2term "(47/6 - 76/9 + 13/4)/(35/12)";

  2231 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2232 if UnparseC.term t = "19 / 21" then ()

  2233 else error "rational.sml: diff.behav. in norm_Rational_mg 1";

  2235 \<close> ML \<open>

  2236 (*SRA Schalk I, p.40 Nr. 166a *)

  2237 val t = TermC.str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";

  2238 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2239 if UnparseC.term t = "45 / 2" then ()

  2240 else error "rational.sml: diff.behav. in norm_Rational_mg 2";

  2242 \<close> ML \<open>

  2243 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";

  2244 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";

  2245 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";

  2246 (* e190c Stefan K.*)

  2247 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3*a))";

  2248 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2249 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"

  2250 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";

  2252 \<close> ML \<open>

  2253 (* e192b Stefan K.*)

  2254 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y))  /  (y \<up> 2 * (7*x + (-1)*y))";

  2255 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2256 if UnparseC.term t = "x \<up> 2 / y \<up> 2"

  2257 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";

  2259 \<close> ML \<open>

  2260 (*SRC Schalk I, p.66 Nr. 379c *)

  2261 val t = TermC.str2term "(a - b)/(b - a)";

  2262 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2263 if UnparseC.term t = "- 1"

  2264 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";

  2266 \<close> ML \<open>

  2267 (*SRC Schalk I, p.66 Nr. 380b *)

  2268 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9)  /  (12*(2*x + 7) * (5*x + 5))";

  2269 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2270 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"

  2271 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";

  2273 \<close> ML \<open>

  2274 (*Schalk I, p.60 Nr. 215c: was not cancelled with Isabelle2002 *)

  2275 val t = TermC.str2term "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";

  2276 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2277 \<close> ML \<open>

  2278 UnparseC.term t = "(a \<up> 2 * x + - 1 * a \<up> 2 * y + 2 * a * b * x + - 2 * a * b * y +\n b \<up> 2 * x +\n - 1 * b \<up> 2 * y) /\n(x \<up> 3 + - 3 * x \<up> 2 * y + 3 * x * y \<up> 2 + y \<up> 3)"

  2279 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2280 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"

  2281 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";

  2283 \<close> ML \<open>

  2284 (*SRC Schalk I, p.66 Nr. 381b *)

  2285 val t = TermC.str2term

  2286 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";

  2287 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2288 \<close> ML \<open>

  2289 UnparseC.term t = "(25 + - 20 * x + 4 * x \<up> 2) /\n(125 + 150 * x + - 60 * x \<up> 2 + 8 * x \<up> 3)"

  2290 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2291 if UnparseC.term t = "1 / (- 5 + 2 * x)"

  2292 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";

  2294 \<close> ML \<open>

  2295 (* e190c Stefan K.*)

  2296 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a))  /  ((3*a + 9*a \<up> 2) * (1 + 3 * a))";

  2297 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2298 if UnparseC.term t =  "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"

  2299 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";

  2301 \<close> ML \<open>

  2302 (* e192b Stefan K.*)

  2303 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y))  /  (y \<up> 2 * (7*x + (-1)*y))";

  2304 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2305 if UnparseC.term t = "x \<up> 2 / y \<up> 2"

  2306 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";

  2308 \<close> ML \<open>

  2309 (*SRC Schalk I, p.66 Nr. 379c *)

  2310 val t = TermC.str2term "(a - b) / (b - a)";

  2311 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2312 if UnparseC.term t = "- 1"

  2313 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";

  2315 \<close> ML \<open>

  2316 (*SRC Schalk I, p.66 Nr. 380b *)

  2317 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9)  /  (12*(2*x + 7) * (5*x + 5))";

  2318 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2319 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"

  2320 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";

  2322 \<close> ML \<open>

  2323 (*Schalk I, p.60 Nr. 215c *)

  2324 val t = TermC.str2term "(a + b) \<up> 4 * (x - y)  /  ((x - y) \<up> 3 * (a + b) \<up> 2)";

  2325 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2326 \<close> ML \<open>

  2327 UnparseC.term t = "(a \<up> 2 * x + - 1 * a \<up> 2 * y + 2 * a * b * x + - 2 * a * b * y +\n b \<up> 2 * x +\n - 1 * b \<up> 2 * y) /\n(x \<up> 3 + - 3 * x \<up> 2 * y + 3 * x * y \<up> 2 + y \<up> 3)"

  2328 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2329 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"

  2330 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";

  2332 \<close> ML \<open>

  2333 (* extreme example from somewhere *)

  2334 val t = TermC.str2term

  2335     ("(a \<up> 4 * x  +  -1*a \<up> 4 * y  +  4*a \<up> 3 * b * x  +  -4*a \<up> 3 * b * y  + " ^

  2336       "6*a \<up> 2 * b \<up> 2 * x  +  -6*a \<up> 2 * b \<up> 2 * y  +  4*a * b \<up> 3 * x  +  -4*a * b \<up> 3 * y  + " ^

  2337       "b \<up> 4 * x  +  -1*b \<up> 4 * y) " ^

  2338   " / (a \<up> 2 * x \<up> 3  +  -3*a \<up> 2 * x \<up> 2 * y  +  3*a \<up> 2 * x * y \<up> 2  +  -1*a \<up> 2 * y \<up> 3 + " ^

  2339       "2*a * b * x \<up> 3  +  -6*a * b * x \<up> 2 * y  +  6*a * b * x * y \<up> 2  +  -2*a * b * y \<up> 3 + " ^

  2340       "b \<up> 2 * x \<up> 3  +  -3*b \<up> 2 * x \<up> 2 * y  +  3*b \<up> 2 * x * y \<up> 2  +  -1*b \<up> 2 * y \<up> 3)")

  2341 val SOME (t, _) = rewrite_set_ thy false cancel_p t;

  2342 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"

  2343 then () else error "with Isabelle2002: NONE -- now SOME changed";

  2345 \<close> ML \<open>

  2346 (*Schalk I, p.66 Nr. 381a *)

  2347 (* ATTENTION: here the rls is very slow. In Isabelle2002 this required 2 min *)

  2348 val t = TermC.str2term "18*(a + b) \<up> 3 * (a - b) \<up> 2 / (72*(a - b) \<up> 3 * (a + b) \<up> 2)";

  2349 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2350 \<close> ML \<open>

  2351 UnparseC.term t = "(a \<up> 3 + - 1 * a \<up> 2 * b + - 1 * a * b \<up> 2 + b \<up> 3) /\n(4 * a \<up> 3 + - 12 * a \<up> 2 * b + 12 * a * b \<up> 2 + 4 * b \<up> 3)"

  2352 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2353 if UnparseC.term t = "(a + b) / (4 * a + - 4 * b)"

  2354 then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";

  2356 \<close> ML \<open>

  2357 (*SRC Schalk I, p.66 Nr. 381b *)

  2358 val t = TermC.str2term "(4*x \<up> 2 - 20*x + 25) / (2*x - 5) \<up> 3";

  2359 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2360 \<close> ML \<open>

  2361 UnparseC.term t = "(25 + - 20 * x + 4 * x \<up> 2) /\n(125 + 150 * x + - 60 * x \<up> 2 + 8 * x \<up> 3)"

  2362 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2363 if UnparseC.term t = "1 / (- 5 + 2 * x)"

  2364 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";

  2366 \<close> ML \<open>

  2367 (*SRC Schalk I, p.66 Nr. 381c *)

  2368 val t = TermC.str2term "(27*a \<up> 3 + 9*a \<up> 2+3*a+1) / (27*a \<up> 3 + 18*a \<up> 2+3*a)";

  2369 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2370 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"

  2371 then () else error "rational.sml: diff.behav. in norm_Rational_mg 10";

  2373 \<close> ML \<open>

  2374 (*SRC Schalk I, p.66 Nr. 383a *)

  2375 val t = TermC.str2term "(5*a \<up> 2 - 5*a*b) / (a - b) \<up> 2";

  2376 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2377 if UnparseC.term t = "- 5 * a / (- 1 * a + b)"

  2378 then () else error "rational.sml: diff.behav. in norm_Rational_mg 11";

  2380 \<close> ML \<open>

  2381 "----- NOT TERMINATING ?: worked before 0707xx";

  2382 val t = TermC.str2term "(a \<up> 2 - 1)*(b + 1) / ((b \<up> 2 - 1)*(a+1))";

  2383 (* WN130911 "exception Div raised" by

  2384   cancel_p_ thy (TermC.str2term ("(-1 + -1 * b + a \<up> 2 + a \<up> 2 * b) /" ^

  2385                            "(-1 + -1 * a + b \<up> 2 + a * b \<up> 2)"))

  2387 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2388 if UnparseC.term t = "(1 + -1 * a) / (1 + -1 * b)" then ()

  2389 else error "rational.sml MG tests 3e";

  2390 *)

  2392 \<close> ML \<open>

  2393 "-------- examples common denominator from: Mathematik 1 Schalk --------------";

  2394 "-------- examples common denominator from: Mathematik 1 Schalk --------------";

  2395 "-------- examples common denominator from: Mathematik 1 Schalk --------------";

  2396 (*SRA Schalk I, p.67 Nr. 403a *)

  2397 val t = TermC.str2term "4/x - 3/y - 1";

  2398 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2399 if UnparseC.term t = "(- 3 * x + 4 * y + - 1 * x * y) / (x * y)"

  2400 then () else error "rational.sml: diff.behav. in norm_Rational_mg 12";

  2402 \<close> ML \<open>

  2403 val t = TermC.str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a \<up> 2+3*b*c)/(a*b*c)";

  2404 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2405 if UnparseC.term t = "4 / c"

  2406 then () else error "rational.sml: diff.behav. in norm_Rational_mg 13";

  2408 \<close> ML \<open>

  2409 (*SRA Schalk I, p.67 Nr. 410b *)

  2410 val t = TermC.str2term "1/(x+1) + 1/(x+2) - 2/(x+3)";

  2411 (* WN130911 non-termination due to non-termination of

  2412   cancel_p_ thy (TermC.str2term "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)")

  2414 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2415 if UnparseC.term t = "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)"

  2416 then () else error "rational.sml: diff.behav. in norm_Rational_mg 14";

  2417 *)

  2419 \<close> ML \<open>

  2420 (*SRA Schalk I, p.67 Nr. 413b *)

  2421 val t = TermC.str2term "(1 + x)/(1 - x)  -  (1 - x)/(1 + x)  +  2*x/(1 - x \<up> 2)";

  2422 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2423 if UnparseC.term t = "6 * x / (1 + - 1 * x \<up> 2)"

  2424 then () else error "rational.sml: diff.behav. in norm_Rational_mg 15";

  2426 \<close> ML \<open>

  2427 (*SRA Schalk I, p.68 Nr. 414a *)

  2428 val t = TermC.str2term "(x + 2)/(x - 1)  +  (x - 3)/(x - 2)  -  (x + 1)/((x - 1)*(x - 2))";

  2429 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2430 if UnparseC.term t ="(- 2 + - 5 * x + 2 * x \<up> 2) / (2 + - 3 * x + x \<up> 2)"

  2431 then () else error "rational.sml: diff.behav. in norm_Rational_mg 16";

  2433 \<close> ML \<open>

  2434 (*SRA Schalk I, p.68 Nr. 428b *)

  2435 val t = TermC.str2term

  2436   "1/(a - b) \<up> 2  +  1/(a + b) \<up> 2  -  2/(a \<up> 2 - b \<up> 2)  -  4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2";

  2437 (* WN130911 non-termination due to non-termination of

  2438   cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")

  2440 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2441 if UnparseC.term t = "4 / (a \<up> 4 + -2 * a \<up> 2 * b \<up> 2 + b \<up> 4)"

  2442 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";

  2443 *)

  2445 \<close> ML \<open>

  2446 (*SRA Schalk I, p.68 Nr. 430b *)

  2447 val t = TermC.str2term

  2448   "a \<up> 2/(a - 3*b) - 108*a*b \<up> 3/((a+3*b)*(a \<up> 2 - 9*b \<up> 2)) - 9*b \<up> 2*(a - 3*b)/(a+3*b) \<up> 2";

  2449 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2450 if UnparseC.term t = "a + 3 * b"

  2451 then () else error "rational.sml: diff.behav. in norm_Rational_mg 19";

  2453 \<close> ML \<open>

  2454 (*SRA Schalk I, p.68 Nr. 432 *)

  2455 val t = TermC.str2term

  2456   ("(a \<up> 2 + a*b) / (a \<up> 2 - b \<up> 2)  -  (b \<up> 2 - a*b) / (b \<up> 2 - a \<up> 2)  +  " ^

  2457   "a \<up> 2*(a - b) / (a \<up> 3 - a \<up> 2*b)  -  2*a*(a \<up> 2 - b \<up> 2) / (a \<up> 3 - a*b \<up> 2)  -  " ^

  2458   "2*b \<up> 2 / (a \<up> 2 - b \<up> 2)");

  2459 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2460 if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*)  "0 / (a \<up> 2 + - 1 * b \<up> 2)"

  2461 then () else error "rational.sml: diff.behav. in norm_Rational_mg 20";

  2463 \<close> ML \<open>

  2464 (* some example *)

  2465 val t = TermC.str2term "3*a / (a*b)  +  x/y";

  2466 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2467 if UnparseC.term t = "(3 * y + b * x) / (b * y)"

  2468 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";

  2471 \<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)

  2472 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";

  2473 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";

  2474 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";

  2475 (*------- SRM Schalk I, p.68 Nr. 436a *)

  2476 val t = TermC.str2term "3*(x+y) / (15*(x - y))  *   25*(x - y) \<up> 2 / (18*(x + y) \<up> 2)";

  2477 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2478 if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)"

  2479 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";

  2481 \<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)

  2482 (*------- SRM.test Schalk I, p.68 Nr. 436b *)

  2483 val t = TermC.str2term "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3";

  2484 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2485 \<close> ML \<open>

  2486  UnparseC.term t = "(5 * a \<up> 3 + - 10 * a \<up> 2 * b + 5 * a * b \<up> 2) /\n(a \<up> 3 + - 3 * a \<up> 2 * b + 3 * a * b \<up> 2 + b \<up> 3)"

  2487 \<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)

  2488 if UnparseC.term t = "5 * a / (a + - 1 * b)"

  2489 then () else error "rational.sml: diff.behav. in norm_Rational_mg 23";

  2491 \<close> ML \<open>

  2492 (*------- Schalk I, p.68 Nr. 437a *)

  2493 val t = TermC.str2term "(3*a - 4*b) / (4*c+3*e)  *  (3*a+4*b)/(9*a \<up> 2 - 16*b \<up> 2)";

  2494 (* raises an exception for unclear reasons:

  2495 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2496 :

  2497 ###  rls: cancel_p on: (9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /

  2498 (9 * a \<up> 2 + -16 * b \<up> 2)

  2499 exception Div raised

  2501 BUT

  2502 val t = TermC.str2term

  2503   ("(9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /" ^

  2504   "(9 * a \<up> 2 + -16 * b \<up> 2)");

  2505 NONE = cancel_p_ thy t;

  2507 if UnparseC.term t = "1 / (4 * c + 3 * e)" then ()

  2508 else error "rational.sml: diff.behav. in norm_Rational_mg 24";

  2509 *)

  2511 \<close> text \<open> (*cancel_p loops since "sym_real_mult_minus1"*)

  2512 "----- S.K. corrected non-termination 060904";

  2513 val t = TermC.str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))";

  2514 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

  2515 if UnparseC.term t =

  2516   "(9 * a \<up> 2 + - 16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + - 64 * b \<up> 2 * c +\n - 48 * b \<up> 2 * e)"

  2517 then () else error "rational.sml: S.K.8..corrected 060904-6";

  2519 \<close> ML \<open>

  2520 "----- S.K. corrected non-termination of cancel_p_";

  2521 val t'' = TermC.str2term ("(9 * a \<up> 2 + -16 * b \<up> 2) /" ^

  2522   "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))");

  2523 (* /--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------\

  2524 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';

  2525 if UnparseC.term t' = "1 / (4 * c + 3 * e)"

  2526 then () else error "rational.sml: diff.behav. in cancel_p S.K.8";

  2527    \--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------/*)

  2529 \<close> ML \<open>

  2530 (*------- Schalk I, p.68 Nr. 437b*)

  2531 val t = TermC.str2term "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))";

  2532 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2533 :

  2534 ####  rls: cancel_p on: (a * x \<up> 2 + -2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 +

  2535  -2 * (b * (x * y)) +

  2536  b * y \<up> 2) /

  2537 (a \<up> 2 * x \<up> 2 + -1 * (a \<up> 2 * y \<up> 2) + -1 * (b \<up> 2 * x \<up> 2) +

  2538  b \<up> 2 * y \<up> 2)

  2539 exception Div raised

  2540 *)

  2542 \<close> ML \<open>

  2543 (*------- SRM Schalk I, p.68 Nr. 438a *)

  2544 val t = TermC.str2term "x*y / (x*y - y \<up> 2)  *  (x \<up> 2 - x*y)";

  2545 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2546 if UnparseC.term t = "x \<up> 2"

  2547 then () else error "rational.sml: diff.behav. in norm_Rational_mg 24";

  2549 \<close> ML \<open>

  2550 (*------- SRM Schalk I, p.68 Nr. 439b *)

  2551 val t = TermC.str2term "(4*x \<up> 2 + 4*x + 1)  *  ((x \<up> 2 - 2*x \<up> 3) / (4*x \<up> 2 + 2*x))";

  2552 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2553 if UnparseC.term t = "(x + - 4 * x \<up> 3) / 2"

  2554 then () else error "rational.sml: diff.behav. in norm_Rational_mg 25";

  2556 \<close> ML \<open>

  2557 (*------- SRM Schalk I, p.68 Nr. 440a *)

  2558 val t = TermC.str2term "(x \<up> 2 - 2*x) / (x \<up> 2 - 3*x)  *  (x - 3) \<up> 2 / (x \<up> 2 - 4)";

  2559 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2560 if UnparseC.term t = "(- 3 + x) / (2 + x)"

  2561 then () else error "rational.sml: diff.behav. in norm_Rational_mg 26";

  2563 \<close> ML \<open>

  2564 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";

  2565 val t = TermC.str2term "(a \<up> 3 - 9*a) / (a \<up> 3*b - a*b \<up> 3)  *  (a \<up> 2*b + a*b \<up> 2) / (a+3)";

  2566 (* WN130911 non-termination for unclear reasons:

  2567 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2569 ... ENDS WITH THIS TRACE:

  2570 :

  2571 ###  rls: cancel_p on: (-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b +

  2572  a \<up> 4 * b \<up> 2) /

  2573 (a \<up> 3 * b + -1 * (a * b \<up> 3)) /

  2574 (3 + a)

  2575 BUT THIS IS CORRECTLY RECOGNISED

  2576 val t = TermC.str2term

  2577   ("(-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + a \<up> 4 * b \<up> 2)  /" ^

  2578   "(a \<up> 3 * b + -1 * (a * b \<up> 3))  /  (3 + (a::real))");

  2579 AS

  2580 NONE = cancel_p_ thy t;

  2582 if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()

  2583 else error "rational.sml: diff.behav. in norm_Rational 27";

  2584 *)

  2586 \<close> ML \<open>

  2587 "----- SK12 works since 0707xx";

  2588 val t = TermC.str2term "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2)  /  ((a \<up> 3*b - a*b \<up> 3) * (a+3))";

  2589 (* WN130911 non-termination due to non-termination of

  2590   cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")

  2592 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2593 if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()

  2594 else error "rational.sml: diff.behav. in norm_Rational 28";

  2595 *)

  2597 \<close> ML \<open> (*common denominator and multiplication MANY EXAMPLES*)

  2598 "-------- examples common denominator and multiplication from: Schalk --------";

  2599 "-------- examples common denominator and multiplication from: Schalk --------";

  2600 "-------- examples common denominator and multiplication from: Schalk --------";

  2601 (*------- SRAM Schalk I, p.69 Nr. 441b *)

  2602 val t = TermC.str2term "(4*a/3 + 3*b \<up> 2/a \<up> 3 + b/(4*a))*(4*b/(3*a))";

  2603 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2604 if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) /\n(9 * a \<up> 4)"

  2605 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";

  2607 \<close> ML \<open>

  2608 (*------- SRAM Schalk I, p.69 Nr. 442b *)

  2609 val t = TermC.str2term ("(15*a \<up> 2/x \<up> 3 - 5*b \<up> 4/x \<up> 2 + 25*c \<up> 2/x) * " ^

  2610   "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + 1/c \<up> 3 * (b*x/a - 3*a/b \<up> 3)");

  2611 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2612 if UnparseC.term t = "5 * x \<up> 2 / (a * b \<up> 3 * c)"

  2613 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";

  2615 \<close> ML \<open>

  2616 (*------- SRAM Schalk I, p.69 Nr. 443b *)

  2617 val t = TermC.str2term "(a/2 + b/3) * (b/3 - a/2)";

  2618 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2619 if UnparseC.term t = "(- 9 * a \<up> 2 + 4 * b \<up> 2) / 36"

  2620 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";

  2622 \<close> ML \<open>

  2623 (*------- SRAM Schalk I, p.69 Nr. 445b *)

  2624 val t = TermC.str2term "(a \<up> 2/9 + 2*a/(3*b) + 4/b \<up> 2)*(a/3 - 2/b) + 8/b \<up> 3";

  2625 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2626 if UnparseC.term t = "a \<up> 3 / 27"

  2627 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";

  2629 \<close> ML \<open>

  2630 (*------- SRAM Schalk I, p.69 Nr. 446b *)

  2631 val t = TermC.str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)";

  2632 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2633 if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + -20 * y \<up> 2" ..isabisac15 | Isabelle2017..*)

  2634                   "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1"

  2635 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";

  2637 \<close> ML \<open>

  2638 (*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)

  2639 val t = TermC.str2term

  2640 "(2*x \<up> 2/(3*y)+x/y \<up> 2)*(4*x \<up> 4/(9*y \<up> 2)+x \<up> 2/y \<up> 4)*(2*x \<up> 2/(3*y) - x/y \<up> 2)";

  2641 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2642 if UnparseC.term t = "(- 81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)"

  2643 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";

  2645 \<close> ML \<open>

  2646 (*------- SRAM Schalk I, p.69 Nr. 450a *)

  2647 val t = TermC.str2term

  2648 "(4*x/(3*y)+2*y/(3*x)) \<up> 2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";

  2649 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2650 if UnparseC.term t = "(52 * x \<up> 2 + 16 * y \<up> 2) / (9 * y \<up> 2)"

  2651 then () else error "rational.sml: diff.behav. in norm_Rational_mg 34";

  2653 \<close> ML \<open>

  2654 (*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)

  2655 val t = TermC.str2term

  2656   ("(15*a \<up> 4/(a*x \<up> 3)  -  5*a*((b \<up> 4 - 5*c \<up> 2*x) / x \<up> 2))  *  " ^

  2657   "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3))   +   a/c \<up> 3 * (x*(b/a) - 3*b*(a/b \<up> 4))");

  2658 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2659 if UnparseC.term t = "5 * x \<up> 2 / (b \<up> 3 * c)"

  2660 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";

  2663 \<close> ML \<open>

  2664 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";

  2665 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";

  2666 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";

  2667 "----- SRD Schalk I, p.69 Nr. 454b";

  2668 val t = TermC.str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";

  2669 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2670 if UnparseC.term t = "(- 4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)"

  2671 then () else error "rational.sml: diff.behav. in norm_Rational_mg 35";

  2673 \<close> ML \<open>

  2674 "----- SRD Schalk I, p.69 Nr. 455a";

  2675 val t = TermC.str2term "(a \<up> 2 + 1)/(a \<up> 2 - 1) / ((a+1)/(a - 1))";

  2676 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2677 if UnparseC.term t = "(1 + a \<up> 2) / (1 + 2 * a + a \<up> 2)" then ()

  2678 else error "rational.sml: diff.behav. in norm_Rational_mg 36";

  2680 \<close> ML \<open>

  2681 "----- Schalk I, p.69 Nr. 455b";

  2682 val t = TermC.str2term "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))";

  2683 (* WN130911 non-termination due to non-termination of

  2684   cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^

  2685                            "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))

  2687 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2688 if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()

  2689 else error "rational.sml: diff.behav. in norm_Rational_mg 37";

  2690 *)

  2692 \<close> ML \<open>

  2693 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";

  2694 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";

  2695 (* WN130911 non-termination due to non-termination of

  2696   cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^

  2697                            "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))

  2699 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2700 if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()

  2701 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";

  2702 *)

  2704 \<close> ML \<open>

  2705 "----- ?: worked before 0707xx";

  2706 val t = TermC.str2term "(3 + -1 * y) / (-9 + y \<up> 2)";

  2707 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2708 if UnparseC.term t = "- 1 / (3 + y)"

  2709 then () else error "rational.sml: -1 / (3 + y) norm_Rational";

  2711 \<close> ML \<open>

  2712 "----- SRD Schalk I, p.69 Nr. 456b";

  2713 val t = TermC.str2term "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)";

  2714 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2715 if UnparseC.term t = "b / (1 + 2 * b + b \<up> 2)"

  2716 then () else error "rational.sml: diff.behav. in norm_Rational_mg 38";

  2718 \<close> ML \<open>

  2719 "----- SRD Schalk I, p.69 Nr. 457b";

  2720 val t = TermC.str2term "(16*a \<up> 2 - 9*b \<up> 2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a \<up> 2 - 9*a \<up> 2*b \<up> 2))";

  2721 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2722 if UnparseC.term t = "8 * a \<up> 2 + - 6 * a * b + - 12 * a \<up> 2 * b + 9 * a * b \<up> 2"

  2723 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";

  2725 \<close> ML \<open>

  2726 "----- Schalk I, p.69 Nr. 458b works since 0707";

  2727 val t = TermC.str2term "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))";

  2728 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2729 :

  2730 ###  rls: cancel_p on: (-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /

  2731 ((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))

  2732 exception Div raised

  2734 BUT

  2735 val t = TermC.str2term

  2736   ("(-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /" ^

  2737   "((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))");

  2738 NONE = cancel_p_ thy t;

  2740 if UnparseC.term t = "a \<up> 2 / b \<up> 2" then ()

  2741 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";

  2742 *)

  2744 \<close> ML \<open>

  2745 "----- SRD Schalk I, p.69 Nr. 459b";

  2746 val t = TermC.str2term "(a \<up> 2 - b \<up> 2)/(a*b) / (4*(a+b) \<up> 2/a)";

  2747 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2748 if UnparseC.term t = "(a + - 1 * b) / (4 * a * b + 4 * b \<up> 2)" then ()

  2749 else error "rational.sml: diff.behav. in norm_Rational_mg 41";

  2751 \<close> ML \<open>

  2752 "----- Schalk I, p.69 Nr. 460b nonterm.SK";

  2753 val t = TermC.str2term "(9*(x \<up> 2 - 8*x + 16) / (4*(y \<up> 2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))";

  2754 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2755 exception Div raised

  2757 BUT

  2758 val t = TermC.str2term

  2759   ("(144 + -72 * x + 9 * x \<up> 2) / (4 + -8 * y + 4 * y \<up> 2) /" ^

  2760   "((-12 + 3 * x) / (-16 + 16 * y))");

  2761 NONE = cancel_p_ thy t;

  2763 if UnparseC.term t = !!!!!!!!!!!!!!!!!!!!!!!!!

  2764 then () else error "rational.sml: diff.behav. in norm_Rational_mg 42";

  2765 *)

  2767 \<close> ML \<open>

  2768 "----- some variant of the above; was non-terminating before";

  2769 val t = TermC.str2term "9*(x \<up> 2 - 8*x+16)*(16*y - 16)/(4*(y \<up> 2 - 2*y+1)*(3*x - 12))";

  2770 val SOME (t , _) = rewrite_set_ thy false norm_Rational t;

  2771 if UnparseC.term t = "(48 + - 12 * x) / (1 + - 1 * y)"

  2772 then () else error "some variant of the above; was non-terminating before";

  2774 \<close> ML \<open>

  2775 "----- SRD Schalk I, p.70 Nr. 472a";

  2776 val t = TermC.str2term ("((8*x \<up> 2 - 32*y \<up> 2) / (2*x + 4*y))  /  ((4*x - 8*y) / (x + y))");

  2777 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2778 if UnparseC.term t = "x + y"

  2779 then () else error "rational.sml: diff.behav. in norm_Rational_mg 43";

  2781 \<close> ML \<open>

  2782 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";

  2783 val t = TermC.str2term ("(a - (a*b + b \<up> 2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^

  2784 		 "((a - a \<up> 2/(a+b))/(a+(a*b)/(a - b)))");

  2785 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2786 if UnparseC.term t = "(2 * a \<up> 3 + 2 * a \<up> 2 * b) / (a \<up> 2 * b + b \<up> 3)"

  2787 then () else error "rational.sml: diff.behav. in norm_Rational_mg 51";

  2789 \<close> ML \<open>

  2790 (*SRD Schalk I, p.69 Nr. 461a *)

  2791 val t = TermC.str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9))";

  2792 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2793 if UnparseC.term t = "1 / 2"

  2794 then () else error "rational.sml: diff.behav. in norm_Rational_mg 44";

  2796 \<close> ML \<open>

  2797 (*SRD Schalk I, p.69 Nr. 464b *)

  2798 val t = TermC.str2term "(a - a/(a - 2)) / (a + a/(a - 2))";

  2799 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2800 if UnparseC.term t = "(- 3 + a) / (- 1 + a)"

  2801 then () else error "rational.sml: diff.behav. in norm_Rational_mg 45";

  2803 \<close> ML \<open>

  2804 (*SRD Schalk I, p.69 Nr. 465b *)

  2805 val t = TermC.str2term "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x))   /   (x/9 + y/6 + z/4)";

  2806 (* WN130911 non-termination due to non-termination of

  2807   cancel_p_ thy (TermC.str2term

  2808     ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + -2916 * z \<up> 2) /" ^

  2809       "(576 * x \<up> 2 + 864 * (x * y) + 1296 * (x * z))"))

  2811 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2812 if UnparseC.term t = "(4 * x + 6 * y + -9 * z) / (4 * x)"

  2813 then () else error "rational.sml: diff.behav. in norm_Rational_mg 46";

  2814 *)

  2816 \<close> ML \<open>

  2817 (*SRD Schalk I, p.69 Nr. 466b *)

  2818 val t = TermC.str2term "((1 - 7*(x - 2)/(x \<up> 2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x \<up> 2 - 25))";

  2819 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2820 if UnparseC.term t = "(25 + - 10 * x + x \<up> 2) / 18"

  2821 then () else error "rational.sml: diff.behav. in norm_Rational_mg 47";

  2823 \<close> ML \<open>

  2824 (*SRD Schalk I, p.70 Nr. 469 *)

  2825 val t = TermC.str2term ("3*b \<up> 2 / (4*a \<up> 2 - 8*a*b + 4*b \<up> 2) / " ^

  2826   "(a / (a \<up> 2*b - b \<up> 3)  +  (a - b) / (4*a*b \<up> 2 + 4*b \<up> 3)  -  1 / (4*b \<up> 2))");

  2827 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  2828 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)"

  2829 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";

  2831 \<close> text \<open> (*me nxt (14 * x * y) / ( x * y )*)

  2832 "-------- me Schalk I No.186 -------------------------------------------------";

  2833 "-------- me Schalk I No.186 -------------------------------------------------";

  2834 "-------- me Schalk I No.186 -------------------------------------------------";

  2835 val fmz = ["Term ((14 * x * y) / ( x * y ))", "normalform N"];

  2836 val (dI',pI',mI') =

  2837   ("Rational",["rational", "simplification"],

  2838    ["simplification", "of_rationals"]);

  2839 val p = e_pos'; val c = [];

  2840 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

  2841 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2842 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2843 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2844 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2845 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2846 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2847 val (p,_,f,nxt,_,pt) = me nxt p c pt;

  2848 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

  2849 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

  2850 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)

  2851 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)

  2852 case (f2str f, nxt) of

  2853     ("14", ("End_Proof'", _)) => ()

  2854   | _ => error "rational.sml diff.behav. in me Schalk I No.186";

  2856 \<close> text \<open> (*interSteps ((2 - x)/(2*a)) / (2*a/(x - 2))*)

  2857 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";

  2858 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";

  2859 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";

  2860 reset_states ();

  2861 CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],

  2862   ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];

  2863 Iterator 1;

  2864 moveActiveRoot 1;

  2865 autoCalculate 1 CompleteCalc;

  2866 val ((pt, p), _) = get_calc 1;

  2867 (*

  2868 Test_Tool.show_pt pt;

  2869 [

  2870 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),

  2871 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),

  2872 (([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),

  2873 (([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),

  2874 (([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),

  2875 (([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),

  2876 (([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]

  2877 *)

  2878 interSteps 1 ([1], Res);

  2879 val ((pt, p), _) = get_calc 1;

  2880 (*Test_Tool.show_pt pt;

  2881 [

  2882 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),

  2883 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),

  2884 (([1,1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),

  2885 (([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + -1 * 2))),

  2886 (([1,2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),

  2887 (([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),

  2888 (([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),

  2889 (([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),

  2890 (([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),

  2891 (([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]

  2892 *)

  2893 val (t, asm) = get_obj g_result pt [1, 1];

  2894 if UnparseC.term t = "(2 - x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"

  2895 then () else error "2nd interSteps ..Simp_Rat_Double_No-1 changed on [1, 1]";

  2896 val (t, asm) = get_obj g_result pt [1, 2];

  2897 if UnparseC.term t = "(2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"

  2898 then () else error "3rd interSteps ..Simp_Rat_Double_No-1 changed on [1, 2]";

  2901 \<close> text \<open> (*interSteps (a^2 + -1*b^2) / (a^2 + -2*a*b + b^2)*)

  2902 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";

  2903 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";

  2904 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";

  2905 reset_states ();

  2906 CalcTree [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],

  2907   ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];

  2908 Iterator 1;

  2909 moveActiveRoot 1;

  2910 autoCalculate 1 CompleteCalc;

  2911 val ((pt, p), _) = get_calc 1;

  2912 (*Test_Tool.show_pt pt;

  2913 [

  2914 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),

  2915 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),

  2916 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2917 (([2], Res), (a + b) / (a + -1 * b)),

  2918 (([], Res), (a + b) / (a + -1 * b))]

  2919 *)

  2920 interSteps 1 ([2], Res);

  2921 val ((pt, p), _) = get_calc 1;

  2922 (*Test_Tool.show_pt pt;

  2923 [

  2924 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),

  2925 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),

  2926 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2927 (([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2928 (([2,1], Res), (a + b) / (a + -1 * b)),

  2929 (([2], Res), (a + b) / (a + -1 * b)),

  2930 (([], Res), (a + b) / (a + -1 * b))]

  2931 *)

  2932 interSteps 1 ([2,1],Res);

  2933 val ((pt, p), _) = get_calc 1;

  2934 (*Test_Tool.show_pt pt;

  2935 [

  2936 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),

  2937 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),

  2938 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2939 (([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2940 (([2,1,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),

  2941 (([2,1,1], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /

  2942 (a \<up> 2 + -2 * (a * b) + 1 * b \<up> 2)),

  2943 (([2,1,2], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /

  2944 (a \<up> 2 + -2 * (a * b) + -1 \<up> 2 * b \<up> 2)),

  2945 (([2,1,3], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /

  2946 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),

  2947 (([2,1,4], Res), (a * a + -1 * (a * b) + a * b + -1 * b \<up> 2) /

  2948 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),

  2949 (([2,1,5], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /

  2950 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),

  2951 (([2,1,6], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /

  2952 (a \<up> 2 + -1 * (2 * (a * b)) + (-1 * b) \<up> 2)),

  2953 (([2,1,7], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /

  2954 (a \<up> 2 + 2 * (a * (-1 * b)) + (-1 * b) \<up> 2)),

  2955 (([2,1,8], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /

  2956 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),

  2957 (([2,1,9], Res), (a * (a + -1 * b) + (b * a + b * (-1 * b))) /

  2958 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),

  2959 (([2,1,10], Res), (a * (a + -1 * b) + b * (a + -1 * b)) /

  2960 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),

  2961 (([2,1,11], Res), (a + b) * (a + -1 * b) / (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),

  2962 (([2,1,12], Res), (a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))),

  2963 (([2,1,13], Res), (a + b) / (a + -1 * b)),

  2964 (([2,1], Res), (a + b) / (a + -1 * b)),

  2965 (([2], Res), (a + b) / (a + -1 * b)),

  2966 (([], Res), (a + b) / (a + -1 * b))]

  2967 *)

  2968 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);

  2969 if length newnds = 13 then () else error "rational.sml: interSteps cancel_p rev_rew_p";

  2971 val p = ([2,1,9],Res);

  2972 getTactic 1 p;

  2973 val (_, tac, _) = ME_Misc.pt_extract (pt, p);

  2974 case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()

  2975 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";

  2978 \<close> text \<open> (*rulesets for cancel_p loops since "sym_real_mult_minus1"*)

  2979 "-------- investigate rulesets for cancel_p ----------------------------------";

  2980 "-------- investigate rulesets for cancel_p ----------------------------------";

  2981 "-------- investigate rulesets for cancel_p ----------------------------------";

  2982 val thy = @ {theory "Rational"};

  2983 val t = TermC.str2term "(a \<up> 2 + -1*b \<up> 2) / (a \<up> 2 + -2*a*b + b \<up> 2)";

  2984 val tt = TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);

  2986 "----- with rewrite_set_";

  2987 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;

  2988 if UnparseC.term tt' = "a \<up> 2 + - 1 * b \<up> 2" then () else error "rls chancel_p 1";

  2989 val tt = TermC.str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);

  2990 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;

  2991 if UnparseC.term tt' = "a \<up> 2 + - 2 * a * b + b \<up> 2" then () else error "rls chancel_p 2";

  2993 \<close> text \<open> (*factout_p_ ff*)

  2994 "----- with .make_deriv; WN1130912 not investigated further, will be discontinued";

  2995 val SOME (tt, _) = factout_p_ thy t;

  2996 if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))"

  2997 then () else error "rls chancel_p 3";

  2999 \<close> text \<open> (*factout_p_ ff*)

  3000 "--- with simpler ruleset";

  3001 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");

  3002 val der = Derive.do_one thy Atools_erls rules ro NONE tt;

  3004 if length der = 12 then () else error "WN1130912 rls chancel_p 4";

  3005 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)

  3006 \<close> text \<open> (*factout_p_ ff*)

  3008 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)

  3009 "...,(-1 * b \<up> 2 + a \<up> 2) / (-2 * (a * b) + a \<up> 2 + (-1 * b) \<up> 2) ]";

  3010 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)

  3011 (*default_print_depth 99;*) map (UnparseC.term o #1 o #3) der; (*default_print_depth 3;*)

  3013 \<close> text \<open> (*factout_p_ ff*)

  3014 val der = Derive.do_one thy Atools_erls rules ro NONE

  3015 	(TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");

  3016 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)

  3018 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p");

  3019 val der = Derive.do_one thy Atools_erls rules ro NONE

  3020 	(TermC.str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");

  3021 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)

  3022 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)

  3023 (*WN060829 ...postponed*)

  3026 \<close> ML \<open>

  3027 "-------- fun eval_get_denominator -------------------------------------------";

  3028 "-------- fun eval_get_denominator -------------------------------------------";

  3029 "-------- fun eval_get_denominator -------------------------------------------";

  3030 val thy = @{theory Isac_Knowledge};

  3031 val t = Thm.term_of (the (TermC.parse thy "get_denominator ((a +x)/b)"));

  3032 val SOME (_, t') = eval_get_denominator "" 0 t thy;

  3033 if UnparseC.term t' = "get_denominator ((a + x) / b) = b"

  3034 then () else error "get_denominator ((a + x) / b) = b"

  3037 \<close> text \<open> (*several errpats loops since "sym_real_mult_minus1"*)

  3038 "-------- several errpats in complicated term --------------------------------";

  3039 "-------- several errpats in complicated term --------------------------------";

  3040 "-------- several errpats in complicated term --------------------------------";

  3041 (*WN12xxxx TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one

  3042   WN130912: kept this test, although not clear what for*)

  3043 reset_states ();

  3044 CalcTree [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],

  3045   ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];

  3046 Iterator 1;

  3047 moveActiveRoot 1;

  3048 autoCalculate 1 CompleteCalc;

  3049 val ((pt, p), _) = get_calc 1;

  3050 (*Test_Tool.show_pt pt;

  3051 [

  3052 (([], Frm), Simplify ((5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b))),

  3053 (([1], Frm), (5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b)),

  3054 (([1], Res), (5 * b + 25) / (a \<up> 2 + -1 * b \<up> 2) * (a + -1 * b) / (5 * b)),

  3055 (([2], Res), (5 * b + 25) * (a + -1 * b) / (a \<up> 2 + -1 * b \<up> 2) / (5 * b)),

  3056 (([3], Res), (25 * a + -25 * b + 5 * (a * b) + -5 * b \<up> 2) / (a \<up> 2 + -1 * b \<up> 2) /

  3057 (5 * b)),

  3058 (([4], Res), (25 + 5 * b) / (a + b) / (5 * b)),

  3059 (([5], Res), (25 + 5 * b) / ((a + b) * (5 * b))),

  3060 (([6], Res), (25 + 5 * b) / (5 * (a * b) + 5 * b \<up> 2)),

  3061 (([7], Res), (5 + b) / (a * b + b \<up> 2)),

  3062 (([], Res), (5 + b) / (a * b + b \<up> 2))] *)

  3065 \<close> ML \<open>

  3066 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

  3067 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

  3068 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

  3069 (*------- Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)

  3070 val t = TermC.str2term

  3071   ("((12*x*y / (9*x \<up> 2 - y \<up> 2))  /  (1 / (3*x - y) \<up> 2 - 1 / (3*x + y) \<up> 2))  *  " ^

  3072 	"((1/(x - 5*y) \<up> 2  -  1/(x + 5*y) \<up> 2)  /  (20*x*y / (x \<up> 2 - 25*y \<up> 2)))");

  3074 (*1st factor separately simplified *)

  3075 val t = TermC.str2term "((12*x*y / (9*x \<up> 2 - y \<up> 2))  /  (1 / (3*x - y) \<up> 2 - 1 / (3*x + y) \<up> 2))";

  3076 val SOME (t', _) = rewrite_set_ thy false norm_Rational t;

  3077 if UnparseC.term t' = "(- 9 * x \<up> 2 + y \<up> 2) / - 1" then () else error "Nr. 480b lhs changed";

  3078 (*2nd factor separately simplified *)

  3079 val t = TermC.str2term "((1/(x - 5*y) \<up> 2  -  1/(x + 5*y) \<up> 2)  /  (20*x*y / (x \<up> 2 - 25*y \<up> 2)))";

  3080 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';

  3081 if UnparseC.term t' = "- 1 / (- 1 * x \<up> 2 + 25 * y \<up> 2)" then () else error "Nr. 480b rhs changed";

  3083 \<close> ML \<open>

  3084 "-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?";

  3085 val t = TermC.str2term ("b*y/(b - 2*y)/((b \<up> 2 - y \<up> 2)/(b+2*y))  /" ^

  3086 		 "(b \<up> 2*y + b*y \<up> 2) * (a+x) \<up> 2  /  ((b \<up> 2 - 4*y \<up> 2) * (a+2*x) \<up> 2)");

  3087 (*val SOME (t',_) = rewrite_set_ thy false norm_Rational t;

  3088 :

  3089 ###  rls: cancel_p on: (a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /

  3090 (b + -2 * y) /

  3091 ((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /

  3092 (b \<up> 2 * y + b * y \<up> 2) /

  3093 (a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +

  3094  -16 * (a * (x * y \<up> 2)) +

  3095  4 * (b \<up> 2 * x \<up> 2) +

  3096  -16 * (x \<up> 2 * y \<up> 2))

  3097 exception Div raised

  3099 BUT

  3100 val t = TermC.str2term

  3101   ("(a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /" ^

  3102   "(b + -2 * y) /" ^

  3103   "((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /" ^

  3104   "(b \<up> 2 * y + b * y \<up> 2) /" ^

  3105   "(a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +" ^

  3106   "-16 * (a * (x * y \<up> 2)) +" ^

  3107   "4 * (b \<up> 2 * x \<up> 2) +" ^

  3108   "-16 * (x \<up> 2 * y \<up> 2))");

  3109 NONE = cancel_p_ thy t;

  3110 *)

  3112 \<close> ML \<open>

  3113 (*------- Schalk I, p.70 Nr. 476b in 2003 this worked using 10 sec. *)

  3114 val t = TermC.str2term

  3115   ("((a \<up> 2 - b \<up> 2)/(2*a*b) + 2*a*b/(a \<up> 2 - b \<up> 2))  /  ((a \<up> 2 + b \<up> 2)/(2*a*b) + 1)    / " ^

  3116    "((a \<up> 2 + b \<up> 2) \<up> 2  /  (a + b) \<up> 2)");

  3117 (* Rewrite.trace_on := true;

  3118 rewrite_set_ thy false norm_Rational t;

  3119 :

  3120 ####  rls: cancel_p on: (2 * (a \<up> 7 * b) + 4 * (a \<up> 6 * b \<up> 2) + 6 * (a \<up> 5 * b \<up> 3) +

  3121  8 * (a \<up> 4 * b \<up> 4) +

  3122  6 * (a \<up> 3 * b \<up> 5) +

  3124 33

  3125 0.

  3127  4 * (a \<up> 2 * b \<up> 6) +

  3128  2 * (a * b \<up> 7)) /

  3129 (2 * (a \<up> 9 * b) + 4 * (a \<up> 8 * b \<up> 2) +

  3130  2 * (2 * (a \<up> 7 * b \<up> 3)) +

  3131  4 * (a \<up> 6 * b \<up> 4) +

  3132  -4 * (a \<up> 4 * b \<up> 6) +

  3133  -4 * (a \<up> 3 * b \<up> 7) +

  3134  -4 * (a \<up> 2 * b \<up> 8) +

  3135  -2 * (a * b \<up> 9))

  3137 if UnparseC.term t = "1 / (a \<up> 2 + -1 * b \<up> 2)" then ()

  3138 else error "rational.sml: diff.behav. in norm_Rational_mg 49";

  3139 *)

  3141 "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";

  3142 val t = TermC.str2term ("(1/x + 1/y + 1/z)  /  (1/x - 1/y - 1/z)  /  " ^

  3143   "(2*x \<up> 2 / (x \<up> 2 - z \<up> 2) / (x / (x + z)  +  x / (x - z)))");

  3144 (* Rewrite.trace_on := true;

  3145 rewrite_set_ thy false norm_Rational t;

  3146 :

  3147 ####  rls: cancel_p on: (2 * (x \<up> 6 * (y \<up> 2 * z)) + 2 * (x \<up> 6 * (y * z \<up> 2)) +

  3148  2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +

  3149  -2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +

  3150  -2 * (x \<up> 4 * (y * z \<up> 4)) +

  3151  -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4))) /

  3152 (-2 * (x \<up> 6 * (y \<up> 2 * z)) + -2 * (x \<up> 6 * (y * z \<up> 2)) +

  3153  2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +

  3154  2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +

  3155  2 * (x \<up> 4 * (y * z \<up> 4)) +

  3156  -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4)))

  3157 *)

  3159 "-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate";

  3160 val t = TermC.str2term "(a-b) \<up> 3 * (x+y) \<up> 4 / ((x+y) \<up> 2 * (a-b) \<up> 5)";

  3161 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:

  3163 val t = TermC.str2term "(a-b) \<up> 3 * (x+y) \<up> 4";

  3164 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  3165 UnparseC.term t;

  3166 "a \<up> 3 * x \<up> 4 + 4 * a \<up> 3 * x \<up> 3 * y +6 * a \<up> 3 * x \<up> 2 * y \<up> 2 +4 * a \<up> 3 * x * y \<up> 3 +a \<up> 3 * y \<up> 4 +-3 * a \<up> 2 * b * x \<up> 4 +-12 * a \<up> 2 * b * x \<up> 3 * y +-18 * a \<up> 2 * b * x \<up> 2 * y \<up> 2 +-12 * a \<up> 2 * b * x * y \<up> 3 +-3 * a \<up> 2 * b * y \<up> 4 +3 * a * b \<up> 2 * x \<up> 4 +12 * a * b \<up> 2 * x \<up> 3 * y +18 * a * b \<up> 2 * x \<up> 2 * y \<up> 2 +12 * a * b \<up> 2 * x * y \<up> 3 +3 * a * b \<up> 2 * y \<up> 4 +-1 * b \<up> 3 * x \<up> 4 +-4 * b \<up> 3 * x \<up> 3 * y +-6 * b \<up> 3 * x \<up> 2 * y \<up> 2 +-4 * b \<up> 3 * x * y \<up> 3 +-1 * b \<up> 3 * y \<up> 4";

  3167 val t = TermC.str2term "((x+y) \<up> 2 * (a-b) \<up> 5)";

  3168 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  3169 UnparseC.term t;

  3170 "a \<up> 5 * x \<up> 2 + 2 * a \<up> 5 * x * y + a \<up> 5 * y \<up> 2 +-5 * a \<up> 4 * b * x \<up> 2 +-10 * a \<up> 4 * b * x * y +-5 * a \<up> 4 * b * y \<up> 2 +10 * a \<up> 3 * b \<up> 2 * x \<up> 2 +20 * a \<up> 3 * b \<up> 2 * x * y +10 * a \<up> 3 * b \<up> 2 * y \<up> 2 +-10 * a \<up> 2 * b \<up> 3 * x \<up> 2 +-20 * a \<up> 2 * b \<up> 3 * x * y +-10 * a \<up> 2 * b \<up> 3 * y \<up> 2 +5 * a * b \<up> 4 * x \<up> 2 +10 * a * b \<up> 4 * x * y +5 * a * b \<up> 4 * y \<up> 2 +-1 * b \<up> 5 * x \<up> 2 +-2 * b \<up> 5 * x * y +-1 * b \<up> 5 * y \<up> 2";

  3172 anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)

  3174 "-------- Schalk I, p.70 Nr. 480b: terms are exploding, Rewrite.trace_on stops at";

  3175 val t = TermC.str2term ("((12*x*y/(9*x \<up> 2 - y \<up> 2))/" ^

  3176 		 "(1/(3*x - y) \<up> 2 - 1/(3*x + y) \<up> 2)) *" ^

  3177 		 "(1/(x - 5*y) \<up> 2 - 1/(x + 5*y) \<up> 2)/" ^

  3178 		 "(20*x*y/(x \<up> 2 - 25*y \<up> 2))");

  3179 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

  3180 :

  3181 ####  rls: cancel_p on: (19440 * (x \<up> 8 * y \<up> 2) + -490320 * (x \<up> 6 * y \<up> 4) +

  3182  108240 * (x \<up> 4 * y \<up> 6) +

  3183  -6000 * (x \<up> 2 * y \<up> 8)) /

  3184 (2160 * (x \<up> 8 * y \<up> 2) + -108240 * (x \<up> 6 * y \<up> 4) +

  3185  1362000 * (x \<up> 4 * y \<up> 6) +

  3186  -150000 * (x \<up> 2 * y \<up> 8))

  3187 *)

  3188 \<close> ML \<open>

  3189 \<close> ML \<open>

  3190 \<close>

  3192 section \<open>===================================================================================\<close>

  3193 ML \<open>

  3194 \<close> ML \<open>

  3195 \<close> ML \<open>

  3196 \<close> ML \<open>

  3197 \<close>

  3199 section \<open>===================================================================================\<close>

  3200 ML \<open>

  3201 \<close> ML \<open>

  3202 \<close> ML \<open>

  3203 \<close> ML \<open>

  3204 \<close>

  3206 section \<open>code for copy & paste ===============================================================\<close>

  3207 ML \<open>

  3208 "~~~~~ fun xxx , args:"; val () = ();

  3209 "~~~~~ and xxx , args:"; val () = ();

  3210 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

  3211 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

  3212 "xx"

  3213 ^ "xxx"   (*+*)

  3214 \<close>

  3216 ML_file \<open>MathEngBasic/rewrite.sml\<close>

  3217 ML_file \<open>Knowledge/poly.sml\<close>

  3218 end

author	wneuper <walther.neuper@jku.at>
	Tue, 13 Jul 2021 09:49:45 +0200
changeset 60321	66086b5d1b6e
parent 60320	02102eaa2021
child 60322	2220bafba61f
permissions	-rw-r--r--