wneuper/isa: src/Tools/isac/Knowledge/Rational.thy@460c24a6a6ba

     1 (* rationals, i.e. fractions of multivariate polynomials over the real field

     2    author: isac team

     3    Copyright (c) isac team 2002

     4    Use is subject to license terms.

     6    depends on Poly (and not on Atools), because

     7    fractions with _normalized_ polynomials are canceled, added, etc.

     8 *)

    10 theory Rational imports Poly begin

    12 consts

    14   is'_expanded   :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)

    15   is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")

    17 axioms (*.not contained in Isabelle2002,

    18           stated as axioms, TODO?: prove as theorems*)

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

    21   mult_cross1:     "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)"

    22   mult_cross2:     "           d ~= 0    ==> (a     = c / d) = (a * d =     c)"

    24   add_minus:       "a + b - b = a"(*RL->Poly.thy*)

    25   add_minus1:      "a - b + b = a"(*RL->Poly.thy*)

    27   rat_mult:        "a / b * (c / d) = a * c / (b * d)"(*?Isa02*)

    28   rat_mult2:       "a / b *  c      = a * c /  b     "(*?Isa02*)

    30   rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a /  b"

    31   rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c /  b"

    33 (*real_times_divide1_eq .. Isa02*)

    34   real_times_divide_1_eq:  "-1    * (c / d) =-1 * c /      d "

    35   real_times_divide_num:   "a is_const ==>

    36 	          	   a     * (c / d) = a * c /      d "

    38   real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n"

    39 (*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)

    41   real_divide_divide1:     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"

    42   real_divide_divide1_mg:  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"

    43 (*real_divide_divide2_eq:  "x / y / z = x / (y * z)"..Isa02*)

    45   rat_power:               "(a / b)^^^n = (a^^^n) / (b^^^n)"

    48   rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==>

    49 	           a / c + b / d = (a * d + b * c) / (c * d)"

    50   rat_add_assoc:   "[| a is_const; b is_const; c is_const; d is_const |] ==>

    51 	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"

    52   rat_add1:        "[| a is_const; b is_const; c is_const |] ==>

    53 	           a / c + b / c = (a + b) / c"

    54   rat_add1_assoc:   "[| a is_const; b is_const; c is_const |] ==>

    55 	           a / c + (b / c + e) = (a + b) / c + e"

    56   rat_add2:        "[| a is_const; b is_const; c is_const |] ==>

    57 	           a / c + b = (a + b * c) / c"

    58   rat_add2_assoc:  "[| a is_const; b is_const; c is_const |] ==>

    59 	           a / c + (b + e) = (a + b * c) / c + e"

    60   rat_add3:        "[| a is_const; b is_const; c is_const |] ==>

    61 	           a + b / c = (a * c + b) / c"

    62   rat_add3_assoc:   "[| a is_const; b is_const; c is_const |] ==>

    63 	           a + (b / c + e) = (a * c + b) / c + e"

    65 text {*calculate in rationals: gcd, lcm, etc.

    66       (c) Stefan Karnel 2002

    67       Institute for Mathematics D and Institute for Software Technology,

    68       TU-Graz SS 2002 *}

    70 text {* Remark on notions in the documentation below:

    71     referring to the remark on 'polynomials' in Poly.sml we use

    72     [2] 'polynomial' normalform (Polynom)

    73     [3] 'expanded_term' normalform (Ausmultiplizierter Term),

    74     where normalform [2] is a special case of [3], i.e. [3] implies [2].

    75     Instead of

    76       'fraction with numerator and nominator both in normalform [2]'

    77       'fraction with numerator and nominator both in normalform [3]'

    78     we say:

    79       'fraction in normalform [2]'

    80       'fraction in normalform [3]'

    81     or

    82       'fraction [2]'

    83       'fraction [3]'.

    84     a 'simple fraction' is a term with '/' as outmost operator and

    85     numerator and nominator in normalform [2] or [3].

    86 *}

    88 ML {*

    89 val thy = @{theory};

    91 signature RATIONALI =

    92 sig

    93   type mv_monom

    94   type mv_poly

    95   val add_fraction_ : theory -> term -> (term * term list) option

    96   val add_fraction_p_ : theory -> term -> (term * term list) option

    97   val calculate_Rational : rls

    98   val calc_rat_erls:rls

    99   val cancel : rls

   100   val cancel_ : theory -> term -> (term * term list) option

   101   val cancel_p : rls

   102   val cancel_p_ : theory -> term -> (term * term list) option

   103   val common_nominator : rls

   104   val common_nominator_ : theory -> term -> (term * term list) option

   105   val common_nominator_p : rls

   106   val common_nominator_p_ : theory -> term -> (term * term list) option

   107   val eval_is_expanded : string -> 'a -> term -> theory ->

   108 			 (string * term) option

   109   val expanded2polynomial : term -> term option

   110   val factout_ : theory -> term -> (term * term list) option

   111   val factout_p_ : theory -> term -> (term * term list) option

   112   val is_expanded : term -> bool

   113   val is_polynomial : term -> bool

   115   val mv_gcd : (int * int list) list -> mv_poly -> mv_poly

   116   val mv_lcm : mv_poly -> mv_poly -> mv_poly

   118   val norm_expanded_rat_ : theory -> term -> (term * term list) option

   119 (*WN0602.2.6.pull into struct !!!

   120   val norm_Rational : rls(*.normalizes an arbitrary rational term without

   121                            roots into a simple and canceled fraction

   122                            with normalform [2].*)

   123 *)

   124 (*val norm_rational_p : 19.10.02 missing FIXXXXXXXXXXXXME

   125       rls               (*.normalizes an rational term [2] without

   126                            roots into a simple and canceled fraction

   127                            with normalform [2].*)

   128 *)

   129   val norm_rational_ : theory -> term -> (term * term list) option

   130   val polynomial2expanded : term -> term option

   131   val rational_erls :

   132       rls             (*.evaluates an arbitrary rational term with numerals.*)

   134 (*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)

   135 end

   137 (*.**************************************************************************

   138 survey on the functions

   139 ~~~~~~~~~~~~~~~~~~~~~~~

   140  [2] 'polynomial'   :rls               | [3]'expanded_term':rls

   141 --------------------:------------------+-------------------:-----------------

   142  factout_p_         :                  | factout_          :

   143  cancel_p_          :                  | cancel_           :

   144                     :cancel_p          |                   :cancel

   145 --------------------:------------------+-------------------:-----------------

   146  common_nominator_p_:                  | common_nominator_ :

   147                     :common_nominator_p|                   :common_nominator

   148  add_fraction_p_    :                  | add_fraction_     :

   149 --------------------:------------------+-------------------:-----------------

   150 ???SK                 :norm_rational_p   |                   :norm_rational

   152 This survey shows only the principal functions for reuse, and the identifiers

   153 of the rls exported. The list below shows some more useful functions.

   156 conversion from Isabelle-term to internal representation

   157 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   159 ... BITTE FORTSETZEN ...

   161 polynomial2expanded = ...

   162 expanded2polynomial = ...

   164 remark: polynomial2expanded o expanded2polynomial = I,

   165         where 'o' is function chaining, and 'I' is identity WN0210???SK

   167 functions for greatest common divisor and canceling

   168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   169 mv_gcd

   170 factout_

   171 factout_p_

   172 cancel_

   173 cancel_p_

   175 functions for least common multiple and addition of fractions

   176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   177 mv_lcm

   178 common_nominator_

   179 common_nominator_p_

   180 add_fraction_       (*.add 2 or more fractions.*)

   181 add_fraction_p_     (*.add 2 or more fractions.*)

   183 functions for normalform of rationals

   184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   185 WN0210???SK interne Funktionen f"ur norm_rational:

   186           schaffen diese SML-Funktionen wirklich ganz allgemeine Terme ?

   188 norm_rational_

   189 norm_expanded_rat_

   191 **************************************************************************.*)

   194 (*##*)

   195 structure RationalI : RATIONALI =

   196 struct

   197 (*##*)

   199 infix mem ins union; (*WN100819 updating to Isabelle2009-2*)

   200 fun x mem [] = false

   201   | x mem (y :: ys) = x = y orelse x mem ys;

   202 fun (x ins xs) = if x mem xs then xs else x :: xs;

   203 fun xs union [] = xs

   204   | [] union ys = ys

   205   | (x :: xs) union ys = xs union (x ins ys);

   207 (*. gcd of integers .*)

   208 (* die gcd Funktion von Isabelle funktioniert nicht richtig !!! *)

   209 fun gcd_int a b = if b=0 then a

   210 		  else gcd_int b (a mod b);

   212 (*. univariate polynomials (uv) .*)

   213 (*. univariate polynomials are represented as a list

   214     of the coefficent in reverse maximum degree order .*)

   215 (*. 5 * x^5 + 4 * x^3 + 2 * x^2 + x + 19 => [19,1,2,4,0,5] .*)

   216 type uv_poly = int list;

   218 (*. adds two uv polynomials .*)

   219 fun uv_mod_add_poly ([]:uv_poly,p2:uv_poly) = p2:uv_poly

   220   | uv_mod_add_poly (p1,[]) = p1

   221   | uv_mod_add_poly (x::p1,y::p2) = (x+y)::(uv_mod_add_poly(p1,p2));

   223 (*. multiplies a uv polynomial with a skalar s .*)

   224 fun uv_mod_smul_poly ([]:uv_poly,s:int) = []:uv_poly

   225   | uv_mod_smul_poly (x::p,s) = (x*s)::(uv_mod_smul_poly(p,s));

   227 (*. calculates the remainder of a polynomial divided by a skalar s .*)

   228 fun uv_mod_rem_poly ([]:uv_poly,s) = []:uv_poly

   229   | uv_mod_rem_poly (x::p,s) = (x mod s)::(uv_mod_smul_poly(p,s));

   231 (*. calculates the degree of a uv polynomial .*)

   232 fun uv_mod_deg ([]:uv_poly) = 0

   233   | uv_mod_deg p = length(p)-1;

   235 (*. calculates the remainder of x/p and represents it as

   236     value between -p/2 and p/2 .*)

   237 fun uv_mod_mod2(x,p)=

   238     let

   239 	val y=(x mod p);

   240     in

   241 	if (y)>(p div 2) then (y)-p else

   242 	    (

   243 	     if (y)<(~p div 2) then p+(y) else (y)

   244 	     )

   245     end;

   247 (*.calculates the remainder for each element of a integer list divided by p.*)

   248 fun uv_mod_list_modp [] p = []

   249   | uv_mod_list_modp (x::xs) p = (uv_mod_mod2(x,p))::(uv_mod_list_modp xs p);

   251 (*. appends an integer at the end of a integer list .*)

   252 fun uv_mod_null (p1:int list,0) = p1

   253   | uv_mod_null (p1:int list,n1:int) = uv_mod_null(p1,n1-1) @ [0];

   255 (*. uv polynomial division, result is (quotient, remainder) .*)

   256 (*. only for uv_mod_divides .*)

   257 (* FIXME: Division von x^9+x^5+1 durch x-1000 funktioniert nicht,

   258    integer zu klein  *)

   259 fun uv_mod_pdiv (p1:uv_poly) ([]:uv_poly) =

   260     error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")

   261   | uv_mod_pdiv p1 [x] =

   262     let

   263 	val xs= Unsynchronized.ref  [];

   264     in

   265 	if x<>0 then

   266 	    (

   267 	     xs:=(uv_mod_rem_poly(p1,x));

   268 	     while length(!xs)>0 andalso hd(!xs)=0 do xs:=tl(!xs)

   269 	     )

   270 	else error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");

   271 	([]:uv_poly,!xs:uv_poly)

   272     end

   273   | uv_mod_pdiv p1 p2 =

   274     let

   275 	val n= uv_mod_deg(p2);

   276 	val m= Unsynchronized.ref (uv_mod_deg(p1));

   277 	val p1'= Unsynchronized.ref  (rev(p1));

   278 	val p2'=(rev(p2));

   279 	val lc2=hd(p2');

   280 	val q= Unsynchronized.ref  [];

   281 	val c= Unsynchronized.ref  0;

   282 	val output= Unsynchronized.ref  ([],[]);

   283     in

   284 	(

   285 	 if (!m)=0 orelse p2=[0]

   286          then error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")

   287 	 else

   288 	     (

   289 	      if (!m)<n then

   290 		  (

   291 		   output:=([0],p1)

   292 		   )

   293 	      else

   294 		  (

   295 		   while (!m)>=n do

   296 		       (

   297 			c:=hd(!p1') div hd(p2');

   298 			if !c<>0 then

   299 			    (

   300 			     p1':=uv_mod_add_poly(!p1',uv_mod_null(uv_mod_smul_poly(p2',~(!c)),!m-n));

   301 			     while length(!p1')>0 andalso hd(!p1')=0  do p1':= tl(!p1');

   302 			     m:=uv_mod_deg(!p1')

   303 			     )

   304 			else m:=0

   305 			);

   306     		   output:=(rev(!q),rev(!p1'))

   307 		   )

   308 	      );

   309 	     !output

   310 	 )

   311     end;

   313 (*. divides p1 by p2 in Zp .*)

   314 fun uv_mod_pdivp (p1:uv_poly) (p2:uv_poly) p =

   315     let

   316 	val n=uv_mod_deg(p2);

   317 	val m= Unsynchronized.ref  (uv_mod_deg(uv_mod_list_modp p1 p));

   318 	val p1'= Unsynchronized.ref  (rev(p1));

   319 	val p2'=(rev(uv_mod_list_modp p2 p));

   320 	val lc2=hd(p2');

   321 	val q= Unsynchronized.ref  [];

   322 	val c= Unsynchronized.ref  0;

   323 	val output= Unsynchronized.ref  ([],[]);

   324     in

   325 	(

   326 	 if (!m)=0 orelse p2=[0] then error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")

   327 	 else

   328 	     (

   329 	      if (!m)<n then

   330 		  (

   331 		   output:=([0],p1)

   332 		   )

   333 	      else

   334 		  (

   335 		   while (!m)>=n do

   336 		       (

   337 			c:=uv_mod_mod2(hd(!p1')*(power lc2 1), p);

   338 			q:=(!c)::(!q);

   339 			p1':=uv_mod_list_modp(tl(uv_mod_add_poly(uv_mod_smul_poly(!p1',lc2),

   340 								  uv_mod_smul_poly(uv_mod_smul_poly(p2',hd(!p1')),~1)))) p;

   341 			m:=(!m)-1

   342 			);

   344 		   while !p1'<>[] andalso hd(!p1')=0 do

   345 		       (

   346 			p1':=tl(!p1')

   347 			);

   349     		   output:=(rev(uv_mod_list_modp (!q) (p)),rev(!p1'))

   350 		   )

   351 	      );

   352 	     !output:uv_poly * uv_poly

   353 	 )

   354     end;

   356 (*. calculates the remainder of p1/p2 .*)

   357 fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = error("UV_MOD_PREST_EXCEPTION: Division by zero")

   358   | uv_mod_prest [] p2 = []:uv_poly

   359   | uv_mod_prest p1 p2 = (#2(uv_mod_pdiv p1 p2));

   361 (*. calculates the remainder of p1/p2 in Zp .*)

   362 fun uv_mod_prestp (p1:uv_poly) ([]:uv_poly) p= error("UV_MOD_PRESTP_EXCEPTION: Division by zero")

   363   | uv_mod_prestp [] p2 p= []:uv_poly

   364   | uv_mod_prestp p1 p2 p = #2(uv_mod_pdivp p1 p2 p);

   366 (*. calculates the content of a uv polynomial .*)

   367 fun uv_mod_cont ([]:uv_poly) = 0

   368   | uv_mod_cont (x::p)= gcd_int x (uv_mod_cont(p));

   370 (*. divides each coefficient of a uv polynomial by y .*)

   371 fun uv_mod_div_list (p:uv_poly,0) = error("UV_MOD_DIV_LIST_EXCEPTION: Division by zero")

   372   | uv_mod_div_list ([],y)   = []:uv_poly

   373   | uv_mod_div_list (x::p,y) = (x div y)::uv_mod_div_list(p,y);

   375 (*. calculates the primitiv part of a uv polynomial .*)

   376 fun uv_mod_pp ([]:uv_poly) = []:uv_poly

   377   | uv_mod_pp p =

   378     let

   379 	val c= Unsynchronized.ref  0;

   380     in

   381 	(

   382 	 c:=uv_mod_cont(p);

   384 	 if !c=0 then error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")

   385 	 else uv_mod_div_list(p,!c)

   386 	)

   387     end;

   389 (*. gets the leading coefficient of a uv polynomial .*)

   390 fun uv_mod_lc ([]:uv_poly) = 0

   391   | uv_mod_lc p  = hd(rev(p));

   393 (*. calculates the euklidean polynomial remainder sequence in Zp .*)

   394 fun uv_mod_prs_euklid_p(p1:uv_poly,p2:uv_poly,p)=

   395     let

   396 	val f = Unsynchronized.ref  [];

   397 	val f'= Unsynchronized.ref  p2;

   398 	val fi= Unsynchronized.ref  [];

   399     in

   400 	(

   401 	 f:=p2::p1::[];

   402  	 while uv_mod_deg(!f')>0 do

   403 	     (

   404 	      f':=uv_mod_prestp (hd(tl(!f))) (hd(!f)) p;

   405 	      if (!f')<>[] then

   406 		  (

   407 		   fi:=(!f');

   408 		   f:=(!fi)::(!f)

   409 		   )

   410 	      else ()

   411 	      );

   412 	      (!f)

   414 	 )

   415     end;

   417 (*. calculates the gcd of p1 and p2 in Zp .*)

   418 fun uv_mod_gcd_modp ([]:uv_poly) (p2:uv_poly) p = p2:uv_poly

   419   | uv_mod_gcd_modp p1 [] p= p1

   420   | uv_mod_gcd_modp p1 p2 p=

   421     let

   422 	val p1'= Unsynchronized.ref [];

   423 	val p2'= Unsynchronized.ref [];

   424 	val pc= Unsynchronized.ref [];

   425 	val g= Unsynchronized.ref  [];

   426 	val d= Unsynchronized.ref  0;

   427 	val prs= Unsynchronized.ref  [];

   428     in

   429 	(

   430 	 if uv_mod_deg(p1)>=uv_mod_deg(p2) then

   431 	     (

   432 	      p1':=uv_mod_list_modp (uv_mod_pp(p1)) p;

   433 	      p2':=uv_mod_list_modp (uv_mod_pp(p2)) p

   434 	      )

   435 	 else

   436 	     (

   437 	      p1':=uv_mod_list_modp (uv_mod_pp(p2)) p;

   438 	      p2':=uv_mod_list_modp (uv_mod_pp(p1)) p

   439 	      );

   440 	 d:=uv_mod_mod2((gcd_int (uv_mod_cont(p1))) (uv_mod_cont(p2)), p) ;

   441 	 if !d>(p div 2) then d:=(!d)-p else ();

   443 	 prs:=uv_mod_prs_euklid_p(!p1',!p2',p);

   445 	 if hd(!prs)=[] then pc:=hd(tl(!prs))

   446 	 else pc:=hd(!prs);

   448 	 g:=uv_mod_smul_poly(uv_mod_pp(!pc),!d);

   449 	 !g

   450 	 )

   451     end;

   453 (*. calculates the minimum of two real values x and y .*)

   454 fun uv_mod_r_min(x,y):Real.real = if x>y then y else x;

   456 (*. calculates the minimum of two integer values x and y .*)

   457 fun uv_mod_min(x,y) = if x>y then y else x;

   459 (*. adds the squared values of a integer list .*)

   460 fun uv_mod_add_qu [] = 0.0

   461   | uv_mod_add_qu (x::p) =  Real.fromInt(x)*Real.fromInt(x) + uv_mod_add_qu p;

   463 (*. calculates the euklidean norm .*)

   464 fun uv_mod_norm ([]:uv_poly) = 0.0

   465   | uv_mod_norm p = Math.sqrt(uv_mod_add_qu(p));

   467 (*. multipies two values a and b .*)

   468 fun uv_mod_multi a b = a * b;

   470 (*. decides if x is a prim, the list contains all primes which are lower then x .*)

   471 fun uv_mod_prim(x,[])= false

   472   | uv_mod_prim(x,[y])=if ((x mod y) <> 0) then true

   473 		else false

   474   | uv_mod_prim(x,y::ys) = if uv_mod_prim(x,[y])

   475 			then

   476 			    if uv_mod_prim(x,ys) then true

   477 			    else false

   478 		    else false;

   480 (*. gets the first prime, which is greater than p and does not divide g .*)

   481 fun uv_mod_nextprime(g,p)=

   482     let

   483 	val list= Unsynchronized.ref  [2];

   484 	val exit= Unsynchronized.ref  0;

   485 	val i = Unsynchronized.ref 2

   486     in

   487 	while (!i<p) do (* calculates the primes lower then p *)

   488 	    (

   489 	     if uv_mod_prim(!i,!list) then

   490 		 (

   491 		  if (p mod !i <> 0)

   492 		      then

   493 			  (

   494 			   list:= (!i)::(!list);

   495 			   i:= (!i)+1

   496 			   )

   497 		  else i:=(!i)+1

   498 		  )

   499 	     else i:= (!i)+1

   500 		 );

   501 	    i:=(p+1);

   502 	    while (!exit=0) do   (* calculate next prime which does not divide g *)

   503 	    (

   504 	     if uv_mod_prim(!i,!list) then

   505 		 (

   506 		  if (g mod !i <> 0)

   507 		      then

   508 			  (

   509 			   list:= (!i)::(!list);

   510 			   exit:= (!i)

   511 			   )

   512 		  else i:=(!i)+1

   513 		      )

   514 	     else i:= (!i)+1

   515 		 );

   516 	    !exit

   517     end;

   519 (*. decides if p1 is a factor of p2 in Zp .*)

   520 fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= error("UV_MOD_DIVIDESP: Division by zero")

   521   | uv_mod_dividesp p1 p2 p= if uv_mod_prestp p2 p1 p = [] then true else false;

   523 (*. decides if p1 is a factor of p2 .*)

   524 fun uv_mod_divides ([]:uv_poly) (p2:uv_poly) = error("UV_MOD_DIVIDES: Division by zero")

   525   | uv_mod_divides p1 p2 = if uv_mod_prest p2 p1  = [] then true else false;

   527 (*. chinese remainder algorithm .*)

   528 fun uv_mod_cra2(r1,r2,m1,m2)=

   529     let

   530 	val c= Unsynchronized.ref  0;

   531 	val r1'= Unsynchronized.ref  0;

   532 	val d= Unsynchronized.ref  0;

   533 	val a= Unsynchronized.ref  0;

   534     in

   535 	(

   536 	 while (uv_mod_mod2((!c)*m1,m2))<>1 do

   537 	     (

   538 	      c:=(!c)+1

   539 	      );

   540 	 r1':= uv_mod_mod2(r1,m1);

   541 	 d:=uv_mod_mod2(((r2-(!r1'))*(!c)),m2);

   542 	 !r1'+(!d)*m1

   543 	 )

   544     end;

   546 (*. applies the chinese remainder algorithmen to the coefficients of x1 and x2 .*)

   547 fun uv_mod_cra_2 ([],[],m1,m2) = []

   548   | uv_mod_cra_2 ([],x2,m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")

   549   | uv_mod_cra_2 (x1,[],m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x2")

   550   | uv_mod_cra_2 (x1::x1s,x2::x2s,m1,m2) = (uv_mod_cra2(x1,x2,m1,m2))::(uv_mod_cra_2(x1s,x2s,m1,m2));

   552 (*. calculates the gcd of two uv polynomials p1' and p2' with the modular algorithm .*)

   553 fun uv_mod_gcd (p1':uv_poly) (p2':uv_poly) =

   554     let

   555 	val p1= Unsynchronized.ref  (uv_mod_pp(p1'));

   556 	val p2= Unsynchronized.ref  (uv_mod_pp(p2'));

   557 	val c=gcd_int (uv_mod_cont(p1')) (uv_mod_cont(p2'));

   558 	val temp= Unsynchronized.ref  [];

   559 	val cp= Unsynchronized.ref  [];

   560 	val qp= Unsynchronized.ref  [];

   561 	val q= Unsynchronized.ref [];

   562 	val pn= Unsynchronized.ref  0;

   563 	val d= Unsynchronized.ref  0;

   564 	val g1= Unsynchronized.ref  0;

   565 	val p= Unsynchronized.ref  0;

   566 	val m= Unsynchronized.ref  0;

   567 	val exit= Unsynchronized.ref  0;

   568 	val i= Unsynchronized.ref  1;

   569     in

   570 	if length(!p1)>length(!p2) then ()

   571 	else

   572 	    (

   573 	     temp:= !p1;

   574 	     p1:= !p2;

   575 	     p2:= !temp

   576 	     );

   579 	d:=gcd_int (uv_mod_lc(!p1)) (uv_mod_lc(!p2));

   580 	g1:=uv_mod_lc(!p1)*uv_mod_lc(!p2);

   581 	p:=4;

   583 	m:=Real.ceil(2.0 * Real.fromInt(!d) *

   584 	  Real.fromInt(power 2 (uv_mod_min(uv_mod_deg(!p2),uv_mod_deg(!p1)))) *

   585 	  Real.fromInt(!d) *

   586 	  uv_mod_r_min(uv_mod_norm(!p1) / Real.fromInt(abs(uv_mod_lc(!p1))),

   587 	  uv_mod_norm(!p2) / Real.fromInt(abs(uv_mod_lc(!p2)))));

   589 	while (!exit=0) do

   590 	    (

   591 	     p:=uv_mod_nextprime(!d,!p);

   592 	     cp:=(uv_mod_gcd_modp (uv_mod_list_modp(!p1) (!p)) (uv_mod_list_modp(!p2) (!p)) (!p)) ;

   593 	     if abs(uv_mod_lc(!cp))<>1 then  (* leading coefficient = 1 ? *)

   594 		 (

   595 		  i:=1;

   596 		  while (!i)<(!p) andalso (abs(uv_mod_mod2((uv_mod_lc(!cp)*(!i)),(!p)))<>1) do

   597 		      (

   598 		       i:=(!i)+1

   599 		       );

   600 		      cp:=uv_mod_list_modp (map (uv_mod_multi (!i)) (!cp)) (!p)

   601 		  )

   602 	     else ();

   604 	     qp:= ((map (uv_mod_multi (uv_mod_mod2(!d,!p)))) (!cp));

   606 	     if uv_mod_deg(!qp)=0 then (q:=[1]; exit:=1) else ();

   608 	     pn:=(!p);

   609 	     q:=(!qp);

   611 	     while !pn<= !m andalso !m>(!p) andalso !exit=0 do

   612 		 (

   613 		  p:=uv_mod_nextprime(!d,!p);

   614  		  cp:=(uv_mod_gcd_modp (uv_mod_list_modp(!p1) (!p)) (uv_mod_list_modp(!p2) (!p)) (!p));

   615  		  if uv_mod_lc(!cp)<>1 then  (* leading coefficient = 1 ? *)

   616  		      (

   617  		       i:=1;

   618  		       while (!i)<(!p) andalso ((uv_mod_mod2((uv_mod_lc(!q)*(!i)),(!p)))<>1) do

   619  			   (

   620  			    i:=(!i)+1

   621 		           );

   622 		       cp:=uv_mod_list_modp (map (uv_mod_multi (!i)) (!cp)) (!p)

   623  		      )

   624  		  else ();

   626 		  qp:=uv_mod_list_modp ((map (uv_mod_multi (uv_mod_mod2(!d,!p)))) (!cp)  ) (!p);

   627  		  if uv_mod_deg(!qp)>uv_mod_deg(!q) then

   628  		      (

   629  		       (*print("degree to high!!!\n")*)

   630  		       )

   631  		  else

   632  		      (

   633  		       if uv_mod_deg(!qp)=uv_mod_deg(!q) then

   634  			   (

   635  			    q:=uv_mod_cra_2(!q,!qp,!pn,!p);

   636 			    pn:=(!pn) * !p;

   637 			    q:=uv_mod_pp(uv_mod_list_modp (!q) (!pn)); (* found already gcd ? *)

   638 			    if (uv_mod_divides (!q) (p1')) andalso (uv_mod_divides (!q) (p2')) then (exit:=1) else ()

   639 		 	    )

   640 		       else

   641 			   (

   642 			    if  uv_mod_deg(!qp)<uv_mod_deg(!q) then

   643 				(

   644 				 pn:= !p;

   645 				 q:= !qp

   646 				 )

   647 			    else ()

   648 			    )

   649 		       )

   650 		  );

   651  	     q:=uv_mod_pp(uv_mod_list_modp (!q) (!pn));

   652 	     if (uv_mod_divides (!q) (p1')) andalso (uv_mod_divides (!q) (p2')) then exit:=1 else ()

   653 	     );

   654 	    uv_mod_smul_poly(!q,c):uv_poly

   655     end;

   657 (*. multivariate polynomials .*)

   658 (*. multivariate polynomials are represented as a list of the pairs,

   659  first is the coefficent and the second is a list of the exponents .*)

   660 (*. 5 * x^5 * y^3 + 4 * x^3 * z^2 + 2 * x^2 * y * z^3 - z - 19

   661  => [(5,[5,3,0]),(4,[3,0,2]),(2,[2,1,3]),(~1,[0,0,1]),(~19,[0,0,0])] .*)

   663 (*. global variables .*)

   664 (*. order indicators .*)

   665 val LEX_=0; (* lexicographical term order *)

   666 val GGO_=1; (* greatest degree order *)

   668 (*. datatypes for internal representation.*)

   669 type mv_monom = (int *      (*.coefficient or the monom.*)

   670 		 int list); (*.list of exponents)      .*)

   671 fun mv_monom2str (i, is) = "("^ int2str i^"," ^ ints2str' is ^ ")";

   673 type mv_poly = mv_monom list;

   674 fun mv_poly2str p = (strs2str' o (map mv_monom2str)) p;

   676 (*. help function for monom_greater and geq .*)

   677 fun mv_mg_hlp([]) = EQUAL

   678   | mv_mg_hlp(x::list)=if x<0 then LESS

   679 		    else if x>0 then GREATER

   680 			 else mv_mg_hlp(list);

   682 (*. adds a list of values .*)

   683 fun mv_addlist([]) = 0

   684   | mv_addlist(p1) = hd(p1)+mv_addlist(tl(p1));

   686 (*. tests if the monomial M1 is greater as the monomial M2 and returns a boolean value .*)

   687 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)

   688 fun mv_monom_greater((M1x,M1l):mv_monom,(M2x,M2l):mv_monom,order)=

   689     if order=LEX_ then

   690 	(

   691 	 if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")

   692 	 else if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true

   693 	     )

   694     else

   695 	if order=GGO_ then

   696 	    (

   697 	     if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")

   698 	     else

   699 		 if mv_addlist(M1l)=mv_addlist(M2l)  then if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true

   700 		 else if mv_addlist(M1l)>mv_addlist(M2l) then true else false

   701 	     )

   702 	else error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Wrong Order");

   704 (*. tests if the monomial X is greater as the monomial Y and returns a order value (GREATER,EQUAL,LESS) .*)

   705 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)

   706 fun mv_geq order ((x1,x):mv_monom,(x2,y):mv_monom) =

   707 let

   708     val temp= Unsynchronized.ref  EQUAL;

   709 in

   710     if order=LEX_ then

   711 	(

   712 	 if length(x)<>length(y) then

   713 	     error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")

   714 	 else

   715 	     (

   716 	      temp:=mv_mg_hlp((map op- (x~~y)));

   717 	      if !temp=EQUAL then

   718 		  ( if x1=x2 then EQUAL

   719 		    else if x1>x2 then GREATER

   720 			 else LESS

   721 			     )

   722 	      else (!temp)

   723 	      )

   724 	     )

   725     else

   726 	if order=GGO_ then

   727 	    (

   728 	     if length(x)<>length(y) then

   729 	      error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")

   730 	     else

   731 		 if mv_addlist(x)=mv_addlist(y) then

   732 		     (mv_mg_hlp((map op- (x~~y))))

   733 		 else if mv_addlist(x)>mv_addlist(y) then GREATER else LESS

   734 		     )

   735 	else error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")

   736 end;

   738 (*. cuts the first variable from a polynomial .*)

   739 fun mv_cut([]:mv_poly)=[]:mv_poly

   740   | mv_cut((x,[])::list) = error ("RATIONALS_MV_CUT_EXCEPTION: Invalid list ")

   741   | mv_cut((x,y::ys)::list)=(x,ys)::mv_cut(list);

   743 (*. leading power product .*)

   744 fun mv_lpp([]:mv_poly,order)  = []

   745   | mv_lpp([(x,y)],order) = y

   746   | mv_lpp(p1,order)  = #2(hd(rev(sort (mv_geq order) p1)));

   748 (*. leading monomial .*)

   749 fun mv_lm([]:mv_poly,order)  = (0,[]):mv_monom

   750   | mv_lm([x],order) = x

   751   | mv_lm(p1,order)  = hd(rev(sort (mv_geq order) p1));

   753 (*. leading coefficient in term order .*)

   754 fun mv_lc2([]:mv_poly,order)  = 0

   755   | mv_lc2([(x,y)],order) = x

   756   | mv_lc2(p1,order)  = #1(hd(rev(sort (mv_geq order) p1)));

   759 (*. reverse the coefficients in mv polynomial .*)

   760 fun mv_rev_to([]:mv_poly) = []:mv_poly

   761   | mv_rev_to((c,e)::xs) = (c,rev(e))::mv_rev_to(xs);

   763 (*. leading coefficient in reverse term order .*)

   764 fun mv_lc([]:mv_poly,order)  = []:mv_poly

   765   | mv_lc([(x,y)],order) = mv_rev_to(mv_cut(mv_rev_to([(x,y)])))

   766   | mv_lc(p1,order)  =

   767     let

   768 	val p1o= Unsynchronized.ref  (rev(sort (mv_geq order) (mv_rev_to(p1))));

   769 	val lp=hd(#2(hd(!p1o)));

   770 	val lc= Unsynchronized.ref  [];

   771     in

   772 	(

   773 	 while (length(!p1o)>0 andalso hd(#2(hd(!p1o)))=lp) do

   774 	     (

   775 	      lc:=hd(mv_cut([hd(!p1o)]))::(!lc);

   776 	      p1o:=tl(!p1o)

   777 	      );

   778 	 if !lc=[] then error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();

   779 	 mv_rev_to(!lc)

   780 	 )

   781     end;

   783 (*. compares two powerproducts .*)

   784 fun mv_monom_equal((_,xlist):mv_monom,(_,ylist):mv_monom) = (foldr and_) (((map op=) (xlist~~ylist)),true);

   786 (*. help function for mv_add .*)

   787 fun mv_madd([]:mv_poly,[]:mv_poly,order) = []:mv_poly

   788   | mv_madd([(0,_)],p2,order) = p2

   789   | mv_madd(p1,[(0,_)],order) = p1

   790   | mv_madd([],p2,order) = p2

   791   | mv_madd(p1,[],order) = p1

   792   | mv_madd(p1,p2,order) =

   793     (

   794      if mv_monom_greater(hd(p1),hd(p2),order)

   795 	 then hd(p1)::mv_madd(tl(p1),p2,order)

   796      else if mv_monom_equal(hd(p1),hd(p2))

   797 	      then if mv_lc2(p1,order)+mv_lc2(p2,order)<>0

   798 		       then (mv_lc2(p1,order)+mv_lc2(p2,order),mv_lpp(p1,order))::mv_madd(tl(p1),tl(p2),order)

   799 		   else mv_madd(tl(p1),tl(p2),order)

   800 	  else hd(p2)::mv_madd(p1,tl(p2),order)

   801 	      )

   803 (*. adds two multivariate polynomials .*)

   804 fun mv_add([]:mv_poly,p2:mv_poly,order) = p2

   805   | mv_add(p1,[],order) = p1

   806   | mv_add(p1,p2,order) = mv_madd(rev(sort (mv_geq order) p1),rev(sort (mv_geq order) p2), order);

   808 (*. monom multiplication .*)

   809 fun mv_mmul((x1,y1):mv_monom,(x2,y2):mv_monom)=(x1*x2,(map op+) (y1~~y2)):mv_monom;

   811 (*. deletes all monomials with coefficient 0 .*)

   812 fun mv_shorten([]:mv_poly,order) = []:mv_poly

   813   | mv_shorten(x::xs,order)=mv_madd([x],mv_shorten(xs,order),order);

   815 (*. zeros a list .*)

   816 fun mv_null2([])=[]

   817   | mv_null2(x::l)=0::mv_null2(l);

   819 (*. multiplies two multivariate polynomials .*)

   820 fun mv_mul([]:mv_poly,[]:mv_poly,_) = []:mv_poly

   821   | mv_mul([],y::p2,_) = [(0,mv_null2(#2(y)))]

   822   | mv_mul(x::p1,[],_) = [(0,mv_null2(#2(x)))]

   823   | mv_mul(x::p1,y::p2,order) = mv_shorten(rev(sort (mv_geq order) (mv_mmul(x,y) :: (mv_mul(p1,y::p2,order) @

   824 									    mv_mul([x],p2,order)))),order);

   826 (*. gets the maximum value of a list .*)

   827 fun mv_getmax([])=0

   828   | mv_getmax(x::p1)= let

   829 		       val m=mv_getmax(p1);

   830 		   in

   831 		       if m>x then m

   832 		       else x

   833 		   end;

   834 (*. calculates the maximum degree of an multivariate polynomial .*)

   835 fun mv_grad([]:mv_poly) = 0

   836   | mv_grad(p1:mv_poly)= mv_getmax((map mv_addlist) ((map #2) p1));

   838 (*. converts the sign of a value .*)

   839 fun mv_minus(x)=(~1) * x;

   841 (*. converts the sign of all coefficients of a polynomial .*)

   842 fun mv_minus2([]:mv_poly)=[]:mv_poly

   843   | mv_minus2(p1)=(mv_minus(#1(hd(p1))),#2(hd(p1)))::(mv_minus2(tl(p1)));

   845 (*. searches for a negativ value in a list .*)

   846 fun mv_is_negativ([])=false

   847   | mv_is_negativ(x::xs)=if x<0 then true else mv_is_negativ(xs);

   849 (*. division of monomials .*)

   850 fun mv_mdiv((0,[]):mv_monom,_:mv_monom)=(0,[]):mv_monom

   851   | mv_mdiv(_,(0,[]))= error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")

   852   | mv_mdiv(p1:mv_monom,p2:mv_monom)=

   853     let

   854 	val c= Unsynchronized.ref  (#1(p2));

   855 	val pp= Unsynchronized.ref  [];

   856     in

   857 	(

   858 	 if !c=0 then error("MV_MDIV_EXCEPTION Dividing by zero")

   859 	 else c:=(#1(p1) div #1(p2));

   860 	     if #1(p2)<>0 then

   861 		 (

   862 		  pp:=(#2(mv_mmul((1,#2(p1)),(1,(map mv_minus) (#2(p2))))));

   863 		  if mv_is_negativ(!pp) then (0,!pp)

   864 		  else (!c,!pp)

   865 		      )

   866 	     else error("MV_MDIV_EXCEPTION Dividing by empty Polynom")

   867 		 )

   868     end;

   870 (*. prints a polynom for (internal use only) .*)

   871 fun mv_print_poly([]:mv_poly)=tracing("[]\n")

   872   | mv_print_poly((x,y)::[])= tracing("("^Int.toString(x)^","^ints2str(y)^")\n")

   873   | mv_print_poly((x,y)::p1) = (tracing("("^Int.toString(x)^","^ints2str(y)^"),");mv_print_poly(p1));

   876 (*. division of two multivariate polynomials .*)

   877 fun mv_division([]:mv_poly,g:mv_poly,order)=([]:mv_poly,[]:mv_poly)

   878   | mv_division(f,[],order)= error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")

   879   | mv_division(f,g,order)=

   880     let

   881 	val r= Unsynchronized.ref  [];

   882 	val q= Unsynchronized.ref  [];

   883 	val g'= Unsynchronized.ref  ([] : mv_monom list);

   884 	val k= Unsynchronized.ref  0;

   885 	val m= Unsynchronized.ref  (0,[0]);

   886 	val exit= Unsynchronized.ref  0;

   887     in

   888 	r := rev(sort (mv_geq order) (mv_shorten(f,order)));

   889 	g':= rev(sort (mv_geq order) (mv_shorten(g,order)));

   890 	if #1(hd(!g'))=0 then error("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero") else ();

   891 	if  (mv_monom_greater (hd(!g'),hd(!r),order)) then ([(0,mv_null2(#2(hd(f))))],(!r))

   892 	else

   893 	    (

   894 	     exit:=0;

   895 	     while (if (!exit)=0 then not(mv_monom_greater (hd(!g'),hd(!r),order)) else false) do

   896 		 (

   897 		  if (#1(mv_lm(!g',order)))<>0 then m:=mv_mdiv(mv_lm(!r,order),mv_lm(!g',order))

   898 		  else error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");

   899 		  if #1(!m)<>0 then

   900 		      (

   901 		       q:=(!m)::(!q);

   902 		       r:=mv_add((!r),mv_minus2(mv_mul(!g',[!m],order)),order)

   903 		       )

   904 		  else exit:=1;

   905 		  if (if length(!r)<>0 then length(!g')<>0 else false) then ()

   906 		  else (exit:=1)

   907 		  );

   908 		 (rev(!q),!r)

   909 		 )

   910     end;

   912 (*. multiplies a polynomial with an integer .*)

   913 fun mv_skalar_mul([]:mv_poly,c) = []:mv_poly

   914   | mv_skalar_mul((x,y)::p1,c) = ((x * c),y)::mv_skalar_mul(p1,c);

   916 (*. inserts the a first variable into an polynomial with exponent v .*)

   917 fun mv_correct([]:mv_poly,v:int)=[]:mv_poly

   918   | mv_correct((x,y)::list,v:int)=(x,v::y)::mv_correct(list,v);

   920 (*. multivariate case .*)

   922 (*. decides if x is a factor of y .*)

   923 fun mv_divides([]:mv_poly,[]:mv_poly)=  error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")

   924   | mv_divides(x,[]) =  error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")

   925   | mv_divides(x:mv_poly,y:mv_poly) = #2(mv_division(y,x,LEX_))=[];

   927 (*. gets the maximum of a and b .*)

   928 fun mv_max(a,b) = if a>b then a else b;

   930 (*. gets the maximum exponent of a mv polynomial in the lexicographic term order .*)

   931 fun mv_deg([]:mv_poly) = 0

   932   | mv_deg(p1)=

   933     let

   934 	val p1'=mv_shorten(p1,LEX_);

   935     in

   936 	if length(p1')=0 then 0

   937 	else mv_max(hd(#2(hd(p1'))),mv_deg(tl(p1')))

   938     end;

   940 (*. gets the maximum exponent of a mv polynomial in the reverse lexicographic term order .*)

   941 fun mv_deg2([]:mv_poly) = 0

   942   | mv_deg2(p1)=

   943     let

   944 	val p1'=mv_shorten(p1,LEX_);

   945     in

   946 	if length(p1')=0 then 0

   947 	else mv_max(hd(rev(#2(hd(p1')))),mv_deg2(tl(p1')))

   948     end;

   950 (*. evaluates the mv polynomial at the value v of the main variable .*)

   951 fun mv_subs([]:mv_poly,v) = []:mv_poly

   952   | mv_subs((c,e)::p1:mv_poly,v) = mv_skalar_mul(mv_cut([(c,e)]),power v (hd(e))) @ mv_subs(p1,v);

   954 (*. calculates the content of a uv-polynomial in mv-representation .*)

   955 fun uv_content2([]:mv_poly) = 0

   956   | uv_content2((c,e)::p1) = (gcd_int c (uv_content2(p1)));

   958 (*. converts a uv-polynomial from mv-representation to  uv-representation .*)

   959 fun uv_to_list ([]:mv_poly)=[]:uv_poly

   960   | uv_to_list ((c1,e1)::others) =

   961     let

   962 	val count= Unsynchronized.ref  0;

   963 	val max=mv_grad((c1,e1)::others);

   964 	val help= Unsynchronized.ref  ((c1,e1)::others);

   965 	val list= Unsynchronized.ref  [];

   966     in

   967 	if length(e1)>1 then error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")

   968 	else if length(e1)=0 then [c1]

   969 	     else

   970 		 (

   971 		  count:=0;

   972 		  while (!count)<=max do

   973 		      (

   974 		       if length(!help)>0 andalso hd(#2(hd(!help)))=max-(!count) then

   975 			   (

   976 			    list:=(#1(hd(!help)))::(!list);

   977 			    help:=tl(!help)

   978 			    )

   979 		       else

   980 			   (

   981 			    list:= 0::(!list)

   982 			    );

   983 		       count := (!count) + 1

   984 		       );

   985 		      (!list)

   986 		      )

   987     end;

   989 (*. converts a uv-polynomial from uv-representation to mv-representation .*)

   990 fun uv_to_poly ([]:uv_poly) = []:mv_poly

   991   | uv_to_poly p1 =

   992     let

   993 	val count= Unsynchronized.ref  0;

   994 	val help= Unsynchronized.ref  p1;

   995 	val list= Unsynchronized.ref  [];

   996     in

   997 	while length(!help)>0 do

   998 	    (

   999 	     if hd(!help)=0 then ()

  1000 	     else list:=(hd(!help),[!count])::(!list);

  1001 	     count:=(!count)+1;

  1002 	     help:=tl(!help)

  1003 	     );

  1004 	    (!list)

  1005     end;

  1007 (*. univariate gcd calculation from polynomials in multivariate representation .*)

  1008 fun uv_gcd ([]:mv_poly) p2 = p2

  1009   | uv_gcd p1 ([]:mv_poly) = p1

  1010   | uv_gcd p1 [(c,[e])] =

  1011     let

  1012 	val list= Unsynchronized.ref  (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));

  1013 	val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));

  1014     in

  1015 	[(gcd_int (uv_content2(p1)) c,[min])]

  1016     end

  1017   | uv_gcd [(c,[e])] p2 =

  1018     let

  1019 	val list= Unsynchronized.ref  (rev(sort (mv_geq LEX_) (mv_shorten(p2,LEX_))));

  1020 	val min=uv_mod_min(e,(hd(#2(hd(rev(!list))))));

  1021     in

  1022 	[(gcd_int (uv_content2(p2)) c,[min])]

  1023     end

  1024   | uv_gcd p11 p22 = uv_to_poly(uv_mod_gcd (uv_to_list(mv_shorten(p11,LEX_))) (uv_to_list(mv_shorten(p22,LEX_))));

  1026 (*. help function for the newton interpolation .*)

  1027 fun mv_newton_help ([]:mv_poly list,k:int) = []:mv_poly list

  1028   | mv_newton_help (pl:mv_poly list,k) =

  1029     let

  1030 	val x= Unsynchronized.ref  (rev(pl));

  1031 	val t= Unsynchronized.ref  [];

  1032 	val y= Unsynchronized.ref  [];

  1033 	val n= Unsynchronized.ref  1;

  1034 	val n1= Unsynchronized.ref [];

  1035     in

  1036 	(

  1037 	 while length(!x)>1 do

  1038 	     (

  1039 	      if length(hd(!x))>0 then n1:=mv_null2(#2(hd(hd(!x))))

  1040 	      else if length(hd(tl(!x)))>0 then n1:=mv_null2(#2(hd(hd(tl(!x)))))

  1041 		   else n1:=[];

  1042 	      t:= #1(mv_division(mv_add(hd(!x),mv_skalar_mul(hd(tl(!x)),~1),LEX_),[(k,!n1)],LEX_));

  1043 	      y:=(!t)::(!y);

  1044 	      x:=tl(!x)

  1045 	      );

  1046 	 (!y)

  1047 	 )

  1048     end;

  1050 (*. help function for the newton interpolation .*)

  1051 fun mv_newton_add ([]:mv_poly list) t = []:mv_poly

  1052   | mv_newton_add [x:mv_poly] t = x

  1053   | mv_newton_add (pl:mv_poly list) t =

  1054     let

  1055 	val expos= Unsynchronized.ref  [];

  1056 	val pll= Unsynchronized.ref  pl;

  1057     in

  1058 	(

  1060 	 while length(!pll)>0 andalso hd(!pll)=[]  do

  1061 	     (

  1062 	      pll:=tl(!pll)

  1063 	      );

  1064 	 if length(!pll)>0 then expos:= #2(hd(hd(!pll))) else expos:=[];

  1065 	 mv_add(hd(pl),

  1066 		mv_mul(

  1067 		       mv_add(mv_correct(mv_cut([(1,mv_null2(!expos))]),1),[(~t,mv_null2(!expos))],LEX_),

  1068 		       mv_newton_add (tl(pl)) (t+1),

  1069 		       LEX_

  1070 		       ),

  1071 		LEX_)

  1072 	 )

  1073     end;

  1075 (*. calculates the newton interpolation with polynomial coefficients .*)

  1076 (*. step-depth is 1 and if the result is not an integerpolynomial .*)

  1077 (*. this function returns [] .*)

  1078 fun mv_newton ([]:(mv_poly) list) = []:mv_poly

  1079   | mv_newton ([mp]:(mv_poly) list) = mp:mv_poly

  1080   | mv_newton pl =

  1081     let

  1082 	val c= Unsynchronized.ref  pl;

  1083 	val c1= Unsynchronized.ref  [];

  1084 	val n=length(pl);

  1085 	val k= Unsynchronized.ref  1;

  1086 	val i= Unsynchronized.ref  n;

  1087 	val ppl= Unsynchronized.ref  [];

  1088     in

  1089 	c1:=hd(pl)::[];

  1090 	c:=mv_newton_help(!c,!k);

  1091 	c1:=(hd(!c))::(!c1);

  1092 	while(length(!c)>1 andalso !k<n) do

  1093 	    (

  1094 	     k:=(!k)+1;

  1095 	     while  length(!c)>0 andalso hd(!c)=[] do c:=tl(!c);

  1096 	     if !c=[] then () else c:=mv_newton_help(!c,!k);

  1097 	     ppl:= !c;

  1098 	     if !c=[] then () else  c1:=(hd(!c))::(!c1)

  1099 	     );

  1100 	while  hd(!c1)=[] do c1:=tl(!c1);

  1101 	c1:=rev(!c1);

  1102 	ppl:= !c1;

  1103 	mv_newton_add (!c1) 1

  1104     end;

  1106 (*. sets the exponents of the first variable to zero .*)

  1107 fun mv_null3([]:mv_poly)    = []:mv_poly

  1108   | mv_null3((x,y)::xs) = (x,0::tl(y))::mv_null3(xs);

  1110 (*. calculates the minimum exponents of a multivariate polynomial .*)

  1111 fun mv_min_pp([]:mv_poly)=[]

  1112   | mv_min_pp((c,e)::xs)=

  1113     let

  1114 	val y= Unsynchronized.ref  xs;

  1115 	val x= Unsynchronized.ref  [];

  1116     in

  1117 	(

  1118 	 x:=e;

  1119 	 while length(!y)>0 do

  1120 	     (

  1121 	      x:=(map uv_mod_min) ((!x) ~~ (#2(hd(!y))));

  1122 	      y:=tl(!y)

  1123 	      );

  1124 	 !x

  1125 	 )

  1126     end;

  1128 (*. checks if all elements of the list have value zero .*)

  1129 fun list_is_null [] = true

  1130   | list_is_null (x::xs) = (x=0 andalso list_is_null(xs));

  1132 (* check if main variable is zero*)

  1133 fun main_zero (ms : mv_poly) = (list_is_null o (map (hd o #2))) ms;

  1135 (*. calculates the content of an polynomial .*)

  1136 fun mv_content([]:mv_poly) = []:mv_poly

  1137   | mv_content(p1) =

  1138     let

  1139 	val list= Unsynchronized.ref  (rev(sort (mv_geq LEX_) (mv_shorten(p1,LEX_))));

  1140 	val test= Unsynchronized.ref  (hd(#2(hd(!list))));

  1141 	val result= Unsynchronized.ref  [];

  1142 	val min=(hd(#2(hd(rev(!list)))));

  1143     in

  1144 	(

  1145 	 if length(!list)>1 then

  1146 	     (

  1147 	      while (if length(!list)>0 then (hd(#2(hd(!list)))=(!test)) else false) do

  1148 		  (

  1149 		   result:=(#1(hd(!list)),tl(#2(hd(!list))))::(!result);

  1151 		   if length(!list)<1 then list:=[]

  1152 		   else list:=tl(!list)

  1154 		       );

  1155 		  if length(!list)>0 then

  1156 		   (

  1157 		    list:=mv_gcd (!result) (mv_cut(mv_content(!list)))

  1158 		    )

  1159 		  else list:=(!result);

  1160 		  list:=mv_correct(!list,0);

  1161 		  (!list)

  1162 		  )

  1163 	 else

  1164 	     (

  1165 	      mv_null3(!list)

  1166 	      )

  1167 	     )

  1168     end

  1170 (*. calculates the primitiv part of a polynomial .*)

  1171 and mv_pp([]:mv_poly) = []:mv_poly

  1172   | mv_pp(p1) = let

  1173 		    val cont= Unsynchronized.ref  [];

  1174 		    val pp= Unsynchronized.ref [];

  1175 		in

  1176 		    cont:=mv_content(p1);

  1177 		    pp:=(#1(mv_division(p1,!cont,LEX_)));

  1178 		    if !pp=[]

  1179 			then error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")

  1180 		    else (!pp)

  1181 		end

  1183 (*. calculates the gcd of two multivariate polynomials with a modular approach .*)

  1184 and mv_gcd ([]:mv_poly) ([]:mv_poly) :mv_poly= []:mv_poly

  1185   | mv_gcd ([]:mv_poly) (p2) :mv_poly= p2:mv_poly

  1186   | mv_gcd (p1:mv_poly) ([]) :mv_poly= p1:mv_poly

  1187   | mv_gcd ([(x,xs)]:mv_poly) ([(y,ys)]):mv_poly =

  1188      let

  1189       val xpoly:mv_poly = [(x,xs)];

  1190       val ypoly:mv_poly = [(y,ys)];

  1191      in

  1192 	(

  1193 	 if xs=ys then [((gcd_int x y),xs)]

  1194 	 else [((gcd_int x y),(map uv_mod_min)(xs~~ys))]:mv_poly

  1195         )

  1196     end

  1197   | mv_gcd (p1:mv_poly) ([(y,ys)]) :mv_poly=

  1198 	(

  1199 	 [(gcd_int (uv_content2(p1)) (y),(map  uv_mod_min)(mv_min_pp(p1)~~ys))]:mv_poly

  1200 	)

  1201   | mv_gcd ([(y,ys)]:mv_poly) (p2):mv_poly =

  1202 	(

  1203          [(gcd_int (uv_content2(p2)) (y),(map  uv_mod_min)(mv_min_pp(p2)~~ys))]:mv_poly

  1204         )

  1205   | mv_gcd (p1':mv_poly) (p2':mv_poly):mv_poly=

  1206     let

  1207 	val vc=length(#2(hd(p1')));

  1208 	val cont =

  1209 		  (

  1210                    if main_zero(mv_content(p1')) andalso

  1211                      (main_zero(mv_content(p2'))) then

  1212                      mv_correct((mv_gcd (mv_cut(mv_content(p1'))) (mv_cut(mv_content(p2')))),0)

  1213                    else

  1214                      mv_gcd (mv_content(p1')) (mv_content(p2'))

  1215                   );

  1216 	val p1= #1(mv_division(p1',mv_content(p1'),LEX_));

  1217 	val p2= #1(mv_division(p2',mv_content(p2'),LEX_));

  1218 	val gcd= Unsynchronized.ref  [];

  1219 	val candidate= Unsynchronized.ref  [];

  1220 	val interpolation_list= Unsynchronized.ref  [];

  1221 	val delta= Unsynchronized.ref  [];

  1222         val p1r = Unsynchronized.ref [];

  1223         val p2r = Unsynchronized.ref [];

  1224         val p1r' = Unsynchronized.ref [];

  1225         val p2r' = Unsynchronized.ref [];

  1226 	val factor= Unsynchronized.ref  [];

  1227 	val r= Unsynchronized.ref  0;

  1228 	val gcd_r= Unsynchronized.ref  [];

  1229 	val d= Unsynchronized.ref  0;

  1230 	val exit= Unsynchronized.ref  0;

  1231 	val current_degree= Unsynchronized.ref  99999; (*. FIXME: unlimited ! .*)

  1232     in

  1233 	(

  1234 	 if vc<2 then (* areUnivariate(p1',p2') *)

  1235 	     (

  1236 	      gcd:=uv_gcd (mv_shorten(p1',LEX_)) (mv_shorten(p2',LEX_))

  1237 	      )

  1238 	 else

  1239 	     (

  1240 	      while !exit=0 do

  1241 		  (

  1242 		   r:=(!r)+1;

  1243                    p1r := mv_lc(p1,LEX_);

  1244 		   p2r := mv_lc(p2,LEX_);

  1245                    if main_zero(!p1r) andalso

  1246                       main_zero(!p2r)

  1247                    then

  1248                        (

  1249                         delta := mv_correct((mv_gcd (mv_cut (!p1r)) (mv_cut (!p2r))),0)

  1250                        )

  1251                    else

  1252                        (

  1253 		        delta := mv_gcd (!p1r) (!p2r)

  1254                        );

  1255 		   (*if mv_shorten(mv_subs(!p1r,!r),LEX_)=[] andalso

  1256 		      mv_shorten(mv_subs(!p2r,!r),LEX_)=[] *)

  1257 		   if mv_lc2(mv_shorten(mv_subs(!p1r,!r),LEX_),LEX_)=0 andalso

  1258 		      mv_lc2(mv_shorten(mv_subs(!p2r,!r),LEX_),LEX_)=0

  1259                    then

  1260                        (

  1261 		       )

  1262 		   else

  1263 		       (

  1264 			gcd_r:=mv_shorten(mv_gcd (mv_shorten(mv_subs(p1,!r),LEX_))

  1265 					         (mv_shorten(mv_subs(p2,!r),LEX_)) ,LEX_);

  1266 			gcd_r:= #1(mv_division(mv_mul(mv_correct(mv_subs(!delta,!r),0),!gcd_r,LEX_),

  1267 					       mv_correct(mv_lc(!gcd_r,LEX_),0),LEX_));

  1268 			d:=mv_deg2(!gcd_r); (* deg(gcd_r,z) *)

  1269 			if (!d < !current_degree) then

  1270 			    (

  1271 			     current_degree:= !d;

  1272 			     interpolation_list:=mv_correct(!gcd_r,0)::(!interpolation_list)

  1273 			     )

  1274 			else

  1275 			    (

  1276 			     if (!d = !current_degree) then

  1277 				 (

  1278 				  interpolation_list:=mv_correct(!gcd_r,0)::(!interpolation_list)

  1279 				  )

  1280 			     else ()

  1281 				 )

  1282 			    );

  1283 		      if length(!interpolation_list)> uv_mod_min(mv_deg(p1),mv_deg(p2)) then

  1284 			  (

  1285 			   candidate := mv_newton(rev(!interpolation_list));

  1286 			   if !candidate=[] then ()

  1287 			   else

  1288 			       (

  1289 				candidate:=mv_pp(!candidate);

  1290 				if mv_divides(!candidate,p1) andalso mv_divides(!candidate,p2) then

  1291 				    (

  1292 				     gcd:= mv_mul(!candidate,cont,LEX_);

  1293 				     exit:=1

  1294 				     )

  1295 				else ()

  1296 				    );

  1297 			       interpolation_list:=[mv_correct(!gcd_r,0)]

  1298 			       )

  1299 		      else ()

  1300 			  )

  1301 	     );

  1302 	     (!gcd):mv_poly

  1303 	     )

  1304     end;

  1307 (*. calculates the least common divisor of two polynomials .*)

  1308 fun mv_lcm (p1:mv_poly) (p2:mv_poly) :mv_poly =

  1309     (

  1310      #1(mv_division(mv_mul(p1,p2,LEX_),mv_gcd p1 p2,LEX_))

  1311      );

  1313 (*. gets the variables (strings) of a term .*)

  1314 fun get_vars(term1) = (map free2str) (vars term1); (*["a","b","c"]; *)

  1316 (*. counts the negative coefficents in a polynomial .*)

  1317 fun count_neg ([]:mv_poly) = 0

  1318   | count_neg ((c,e)::xs) = if c<0 then 1+count_neg xs

  1319 			  else count_neg xs;

  1321 (*. help function for is_polynomial

  1322     checks the order of the operators .*)

  1323 fun test_polynomial (Const ("uminus",_) $ Free (str,_)) _ = true (*WN.13.3.03*)

  1324   | test_polynomial (t as Free(str,_)) v = true

  1325   | test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false

  1326 						     else (test_polynomial t1 "*") andalso (test_polynomial t2 "*")

  1327   | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false

  1328 							  else (test_polynomial t1 " ") andalso (test_polynomial t2 " ")

  1329   | test_polynomial (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_polynomial t1 "^") andalso (test_polynomial t2 "^")

  1330   | test_polynomial _ v = false;

  1332 (*. tests if a term is a polynomial .*)

  1333 fun is_polynomial t = test_polynomial t " ";

  1335 (*. help function for is_expanded

  1336     checks the order of the operators .*)

  1337 fun test_exp (t as Free(str,_)) v = true

  1338   | test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false

  1339 						     else (test_exp t1 "*") andalso (test_exp t2 "*")

  1340   | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false

  1341 							  else (test_exp t1 " ") andalso (test_exp t2 " ")

  1342   | test_exp (t as Const ("Groups.minus_class.minus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false

  1343 							  else (test_exp t1 " ") andalso (test_exp t2 " ")

  1344   | test_exp (t as Const ("Atools.pow",_) $ t1 $ t2) v = (test_exp t1 "^") andalso (test_exp t2 "^")

  1345   | test_exp  _ v = false;

  1348 (*. help function for check_coeff:

  1349     converts the term to a list of coefficients .*)

  1350 fun term2coef' (t as Free(str,_(*typ*))) v :mv_poly option =

  1351     let

  1352 	val x= Unsynchronized.ref  NONE;

  1353 	val len= Unsynchronized.ref  0;

  1354 	val vl= Unsynchronized.ref  [];

  1355 	val vh= Unsynchronized.ref  [];

  1356 	val i= Unsynchronized.ref  0;

  1357     in

  1358 	if is_numeral str then

  1359 	    (

  1360 	     SOME [(((the o int_of_str) str),mv_null2(v))] handle _ => NONE

  1361 		 )

  1362 	else (* variable *)

  1363 	    (

  1364 	     len:=length(v);

  1365 	     vh:=v;

  1366 	     while ((!len)>(!i)) do

  1367 		 (

  1368 		  if str=hd((!vh)) then

  1369 		      (

  1370 		       vl:=1::(!vl)

  1371 		       )

  1372 		  else

  1373 		      (

  1374 		       vl:=0::(!vl)

  1375 		       );

  1376 		      vh:=tl(!vh);

  1377 		      i:=(!i)+1

  1378 		      );

  1379 		 SOME [(1,rev(!vl))] handle _ => NONE

  1380 	    )

  1381     end

  1382   | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=

  1383     let

  1384 	val t1pp= Unsynchronized.ref  [];

  1385 	val t2pp= Unsynchronized.ref  [];

  1386 	val t1c= Unsynchronized.ref  0;

  1387 	val t2c= Unsynchronized.ref  0;

  1388     in

  1389 	(

  1390 	 t1pp:=(#2(hd(the(term2coef' t1 v))));

  1391 	 t2pp:=(#2(hd(the(term2coef' t2 v))));

  1392 	 t1c:=(#1(hd(the(term2coef' t1 v))));

  1393 	 t2c:=(#1(hd(the(term2coef' t2 v))));

  1395 	 SOME [( (!t1c)*(!t2c) ,( (map op+) ((!t1pp)~~(!t2pp)) ) )] handle _ => NONE

  1397 	 )

  1398     end

  1399   | term2coef' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $ (t2 as Free (str2,_))) v :mv_poly option=

  1400     let

  1401 	val x= Unsynchronized.ref  NONE;

  1402 	val len= Unsynchronized.ref  0;

  1403 	val vl= Unsynchronized.ref  [];

  1404 	val vh= Unsynchronized.ref  [];

  1405 	val vtemp= Unsynchronized.ref  [];

  1406 	val i= Unsynchronized.ref  0;

  1407     in

  1408     (

  1409      if (not o is_numeral) str1 andalso is_numeral str2 then

  1410 	 (

  1411 	  len:=length(v);

  1412 	  vh:=v;

  1414 	  while ((!len)>(!i)) do

  1415 	      (

  1416 	       if str1=hd((!vh)) then

  1417 		   (

  1418 		    vl:=((the o int_of_str) str2)::(!vl)

  1419 		    )

  1420 	       else

  1421 		   (

  1422 		    vl:=0::(!vl)

  1423 		    );

  1424 		   vh:=tl(!vh);

  1425 		   i:=(!i)+1

  1426 		   );

  1427 	      SOME [(1,rev(!vl))] handle _ => NONE

  1428 	      )

  1429      else error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")

  1430 	 )

  1431     end

  1432   | term2coef' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option=

  1433     (

  1434      SOME ((the(term2coef' t1 v)) @ (the(term2coef' t2 v))) handle _ => NONE

  1435 	 )

  1436   | term2coef' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option=

  1437     (

  1438      SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE

  1439 	 )

  1440   | term2coef' (term) v = error ("RATIONALS_TERM2COEF_EXCEPTION 2: Invalid term");

  1442 (*. checks if all coefficients of a polynomial are positiv (except the first) .*)

  1443 fun check_coeff t = (* erste Koeffizient kann <0 sein !!! *)

  1444     if count_neg(tl(the(term2coef' t (get_vars(t)))))=0 then true

  1445     else false;

  1447 (*. checks for expanded term [3] .*)

  1448 fun is_expanded t = test_exp t " " andalso check_coeff(t);

  1450 (*WN.7.3.03 Hilfsfunktion f"ur term2poly'*)

  1451 fun mk_monom v' p vs =

  1452     let fun conv p (v: string) = if v'= v then p else 0

  1453     in map (conv p) vs end;

  1454 (* mk_monom "y" 5 ["a","b","x","y","z"];

  1455 val it = [0,0,0,5,0] : int list*)

  1457 (*. this function converts the term representation into the internal representation mv_poly .*)

  1458 fun term2poly' (Const ("uminus",_) $ Free (str,_)) v = (*WN.7.3.03*)

  1459     if is_numeral str

  1460     then SOME [((the o int_of_str) ("-"^str), mk_monom "#" 0 v)]

  1461     else SOME [(~1, mk_monom str 1 v)]

  1463   | term2poly' (Free(str,_)) v :mv_poly option =

  1464     let

  1465 	val x= Unsynchronized.ref  NONE;

  1466 	val len= Unsynchronized.ref  0;

  1467 	val vl= Unsynchronized.ref  [];

  1468 	val vh= Unsynchronized.ref  [];

  1469 	val i= Unsynchronized.ref  0;

  1470     in

  1471 	if is_numeral str then

  1472 	    (

  1473 	     SOME [(((the o int_of_str) str),mv_null2 v)] handle _ => NONE

  1474 		 )

  1475 	else (* variable *)

  1476 	    (

  1477 	     len:=length v;

  1478 	     vh:= v;

  1479 	     while ((!len)>(!i)) do

  1480 		 (

  1481 		  if str=hd((!vh)) then

  1482 		      (

  1483 		       vl:=1::(!vl)

  1484 		       )

  1485 		  else

  1486 		      (

  1487 		       vl:=0::(!vl)

  1488 		       );

  1489 		      vh:=tl(!vh);

  1490 		      i:=(!i)+1

  1491 		      );

  1492 		 SOME [(1,rev(!vl))] handle _ => NONE

  1493 	    )

  1494     end

  1495   | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=

  1496     let

  1497 	val t1pp= Unsynchronized.ref  [];

  1498 	val t2pp= Unsynchronized.ref  [];

  1499 	val t1c= Unsynchronized.ref  0;

  1500 	val t2c= Unsynchronized.ref  0;

  1501     in

  1502 	(

  1503 	 t1pp:=(#2(hd(the(term2poly' t1 v))));

  1504 	 t2pp:=(#2(hd(the(term2poly' t2 v))));

  1505 	 t1c:=(#1(hd(the(term2poly' t1 v))));

  1506 	 t2c:=(#1(hd(the(term2poly' t2 v))));

  1508 	 SOME [( (!t1c)*(!t2c) ,( (map op+) ((!t1pp)~~(!t2pp)) ) )]

  1509 	 handle _ => NONE

  1511 	 )

  1512     end

  1513   | term2poly' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $

  1514 		      (t2 as Free (str2,_))) v :mv_poly option=

  1515     let

  1516 	val x= Unsynchronized.ref  NONE;

  1517 	val len= Unsynchronized.ref  0;

  1518 	val vl= Unsynchronized.ref  [];

  1519 	val vh= Unsynchronized.ref  [];

  1520 	val vtemp= Unsynchronized.ref  [];

  1521 	val i= Unsynchronized.ref  0;

  1522     in

  1523     (

  1524      if (not o is_numeral) str1 andalso is_numeral str2 then

  1525 	 (

  1526 	  len:=length(v);

  1527 	  vh:=v;

  1529 	  while ((!len)>(!i)) do

  1530 	      (

  1531 	       if str1=hd((!vh)) then

  1532 		   (

  1533 		    vl:=((the o int_of_str) str2)::(!vl)

  1534 		    )

  1535 	       else

  1536 		   (

  1537 		    vl:=0::(!vl)

  1538 		    );

  1539 		   vh:=tl(!vh);

  1540 		   i:=(!i)+1

  1541 		   );

  1542 	      SOME [(1,rev(!vl))] handle _ => NONE

  1543 	      )

  1544      else error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")

  1545 	 )

  1546     end

  1547   | term2poly' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option =

  1548     (

  1549      SOME ((the(term2poly' t1 v)) @ (the(term2poly' t2 v))) handle _ => NONE

  1550 	 )

  1551   | term2poly' (Const ("Groups.minus_class.minus",_) $ t1 $ t2) v :mv_poly option =

  1552     (

  1553      SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE

  1554 	 )

  1555   | term2poly' (term) v = error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");

  1557 (*. translates an Isabelle term into internal representation.

  1558     term2poly

  1559     fn : term ->              (*normalform [2]                    *)

  1560     	 string list ->       (*for ...!!! BITTE DIE ERKLÄRUNG,

  1561     			       DIE DU MIR LETZTES MAL GEGEBEN HAST*)

  1562     	 mv_monom list        (*internal representation           *)

  1563     		  option      (*the translation may fail with NONE*)

  1564 .*)

  1565 fun term2poly (t:term) v =

  1566      if is_polynomial t then term2poly' t v

  1567      else error ("term2poly: invalid = "^(term2str t));

  1569 (*. same as term2poly with automatic detection of the variables .*)

  1570 fun term2polyx t = term2poly t (((map free2str) o vars) t);

  1572 (*. checks if the term is in expanded polynomial form and converts it into the internal representation .*)

  1573 fun expanded2poly (t:term) v =

  1574     (*if is_expanded t then*) term2poly' t v

  1575     (*else error ("RATIONALS_EXPANDED2POLY_EXCEPTION: Invalid Polynomial")*);

  1577 (*. same as expanded2poly with automatic detection of the variables .*)

  1578 fun expanded2polyx t = expanded2poly t (((map free2str) o vars) t);

  1580 (*. converts a powerproduct into term representation .*)

  1581 fun powerproduct2term(xs,v) =

  1582     let

  1583 	val xss= Unsynchronized.ref  xs;

  1584 	val vv= Unsynchronized.ref  v;

  1585     in

  1586 	(

  1587 	 while hd(!xss)=0 do

  1588 	     (

  1589 	      xss:=tl(!xss);

  1590 	      vv:=tl(!vv)

  1591 	      );

  1593 	 if list_is_null(tl(!xss)) then

  1594 	     (

  1595 	      if hd(!xss)=1 then Free(hd(!vv), HOLogic.realT)

  1596 	      else

  1597 		  (

  1598 		   Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1599 		   Free(hd(!vv), HOLogic.realT) $  Free(str_of_int (hd(!xss)),HOLogic.realT)

  1600 		   )

  1601 	      )

  1602 	 else

  1603 	     (

  1604 	      if hd(!xss)=1 then

  1605 		  (

  1606 		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1607 		   Free(hd(!vv), HOLogic.realT) $

  1608 		   powerproduct2term(tl(!xss),tl(!vv))

  1609 		   )

  1610 	      else

  1611 		  (

  1612 		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1613 		   (

  1614 		    Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1615 		    Free(hd(!vv), HOLogic.realT) $  Free(str_of_int (hd(!xss)),HOLogic.realT)

  1616 		    ) $

  1617 		    powerproduct2term(tl(!xss),tl(!vv))

  1618 		   )

  1619 	      )

  1620 	 )

  1621     end;

  1623 (*. converts a monom into term representation .*)

  1624 (*fun monom2term ((c,e):mv_monom, v:string list) =

  1625     if c=0 then Free(str_of_int 0,HOLogic.realT)

  1626     else

  1627 	(

  1628 	 if list_is_null(e) then

  1629 	     (

  1630 	      Free(str_of_int c,HOLogic.realT)

  1631 	      )

  1632 	 else

  1633 	     (

  1634 	      if c=1 then

  1635 		  (

  1636 		   powerproduct2term(e,v)

  1637 		   )

  1638 	      else

  1639 		  (

  1640 		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1641 		   Free(str_of_int c,HOLogic.realT)  $

  1642 		   powerproduct2term(e,v)

  1643 		   )

  1644 		  )

  1645 	     );*)

  1648 (*fun monom2term ((i, is):mv_monom, v) =

  1649     if list_is_null is

  1650     then

  1651 	if i >= 0

  1652 	then Free (str_of_int i, HOLogic.realT)

  1653 	else Const ("uminus", HOLogic.realT --> HOLogic.realT) $

  1654 		   Free ((str_of_int o abs) i, HOLogic.realT)

  1655     else

  1656 	if i > 0

  1657 	then Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $

  1658 		   (Free (str_of_int i, HOLogic.realT)) $

  1659 		   powerproduct2term(is, v)

  1660 	else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $

  1661 		   (Const ("uminus", HOLogic.realT --> HOLogic.realT) $

  1662 		   Free ((str_of_int o abs) i, HOLogic.realT)) $

  1663 		   powerproduct2term(is, vs);---------------------------*)

  1664 fun monom2term ((i, is) : mv_monom, vs) =

  1665     if list_is_null is

  1666     then Free (str_of_int i, HOLogic.realT)

  1667     else if i = 1

  1668     then powerproduct2term (is, vs)

  1669     else Const ("op *", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $

  1670 	       (Free (str_of_int i, HOLogic.realT)) $

  1671 	       powerproduct2term (is, vs);

  1673 (*. converts the internal polynomial representation into an Isabelle term.*)

  1674 fun poly2term' ([] : mv_poly, vs) = Free(str_of_int 0, HOLogic.realT)

  1675   | poly2term' ([(c, e) : mv_monom], vs) = monom2term ((c, e), vs)

  1676   | poly2term' ((c, e) :: ces, vs) =

  1677     Const("Groups.plus_class.plus", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $

  1678          poly2term (ces, vs) $ monom2term ((c, e), vs)

  1679 and poly2term (xs, vs) = poly2term' (rev (sort (mv_geq LEX_) (xs)), vs);

  1682 (*. converts a monom into term representation .*)

  1683 (*. ignores the sign of the coefficients => use only for exp-poly functions .*)

  1684 fun monom2term2((c,e):mv_monom, v:string list) =

  1685     if c=0 then Free(str_of_int 0,HOLogic.realT)

  1686     else

  1687 	(

  1688 	 if list_is_null(e) then

  1689 	     (

  1690 	      Free(str_of_int (abs(c)),HOLogic.realT)

  1691 	      )

  1692 	 else

  1693 	     (

  1694 	      if abs(c)=1 then

  1695 		  (

  1696 		   powerproduct2term(e,v)

  1697 		   )

  1698 	      else

  1699 		  (

  1700 		   Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1701 		   Free(str_of_int (abs(c)),HOLogic.realT)  $

  1702 		   powerproduct2term(e,v)

  1703 		   )

  1704 		  )

  1705 	     );

  1707 (*. converts the expanded polynomial representation into the term representation .*)

  1708 fun exp2term' ([]:mv_poly,vars) =  Free(str_of_int 0,HOLogic.realT)

  1709   | exp2term' ([(c,e)],vars) =     monom2term((c,e),vars)

  1710   | exp2term' ((c1,e1)::others,vars) =

  1711     if c1<0 then

  1712 	Const("Groups.minus_class.minus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1713 	exp2term'(others,vars) $

  1714 	(

  1715 	 monom2term2((c1,e1),vars)

  1716 	 )

  1717     else

  1718 	Const("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1719 	exp2term'(others,vars) $

  1720 	(

  1721 	 monom2term2((c1,e1),vars)

  1722 	 );

  1724 (*. sorts the powerproduct by lexicographic termorder and converts them into

  1725     a term in polynomial representation .*)

  1726 fun poly2expanded (xs,vars) = exp2term'(rev(sort (mv_geq LEX_) (xs)),vars);

  1728 (*. converts a polynomial into expanded form .*)

  1729 fun polynomial2expanded t =

  1730     (let

  1731 	val vars=(((map free2str) o vars) t);

  1732     in

  1733 	SOME (poly2expanded (the (term2poly t vars), vars))

  1734     end) handle _ => NONE;

  1736 (*. converts a polynomial into polynomial form .*)

  1737 fun expanded2polynomial t =

  1738     (let

  1739 	val vars=(((map free2str) o vars) t);

  1740     in

  1741 	SOME (poly2term (the (expanded2poly t vars), vars))

  1742     end) handle _ => NONE;

  1745 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)

  1746 fun step_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =

  1747     let

  1748 	val p1' = Unsynchronized.ref [];

  1749 	val p2' = Unsynchronized.ref [];

  1750 	val p3  = Unsynchronized.ref []

  1751 	val vars = rev(get_vars(p1) union get_vars(p2));

  1752     in

  1753 	(

  1754          p1':= sort (mv_geq LEX_) (the (term2poly p1 vars ));

  1755        	 p2':= sort (mv_geq LEX_) (the (term2poly p2 vars ));

  1756 	 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));

  1757 	 if (!p3)=[(1,mv_null2(vars))] then

  1758 	     (

  1759 	      Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2

  1760 	      )

  1761 	 else

  1762 	     (

  1764 	      p1':=sort (mv_geq LEX_) (#1(mv_division((!p1'),(!p3),LEX_)));

  1765 	      p2':=sort (mv_geq LEX_) (#1(mv_division((!p2'),(!p3),LEX_)));

  1767 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then

  1768 	      (

  1769 	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1770 	       $

  1771 	       (

  1772 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1773 		poly2term(!p1',vars) $

  1774 		poly2term(!p3,vars)

  1775 		)

  1776 	       $

  1777 	       (

  1778 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1779 		poly2term(!p2',vars) $

  1780 		poly2term(!p3,vars)

  1781 		)

  1782 	       )

  1783 	      else

  1784 	      (

  1785 	       p1':=mv_skalar_mul(!p1',~1);

  1786 	       p2':=mv_skalar_mul(!p2',~1);

  1787 	       p3:=mv_skalar_mul(!p3,~1);

  1788 	       (

  1789 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1790 		$

  1791 		(

  1792 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1793 		 poly2term(!p1',vars) $

  1794 		 poly2term(!p3,vars)

  1795 		 )

  1796 		$

  1797 		(

  1798 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1799 		 poly2term(!p2',vars) $

  1800 		 poly2term(!p3,vars)

  1801 		 )

  1802 		)

  1803 	       )

  1804 	      )

  1805 	     )

  1806     end

  1807 | step_cancel _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");

  1810 (*. same as step_cancel, this time for expanded forms (input+output) .*)

  1811 fun step_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =

  1812     let

  1813 	val p1' = Unsynchronized.ref [];

  1814 	val p2' = Unsynchronized.ref [];

  1815 	val p3  = Unsynchronized.ref []

  1816 	val vars = rev(get_vars(p1) union get_vars(p2));

  1817     in

  1818 	(

  1819          p1':= sort (mv_geq LEX_) (the (expanded2poly p1 vars ));

  1820        	 p2':= sort (mv_geq LEX_) (the (expanded2poly p2 vars ));

  1821 	 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));

  1822 	 if (!p3)=[(1,mv_null2(vars))] then

  1823 	     (

  1824 	      Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2

  1825 	      )

  1826 	 else

  1827 	     (

  1829 	      p1':=sort (mv_geq LEX_) (#1(mv_division((!p1'),(!p3),LEX_)));

  1830 	      p2':=sort (mv_geq LEX_) (#1(mv_division((!p2'),(!p3),LEX_)));

  1832 	      if #1(hd(sort (mv_geq LEX_) (!p2')))(* mv_lc2(!p2',LEX_)*)>0 then

  1833 	      (

  1834 	       Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1835 	       $

  1836 	       (

  1837 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1838 		poly2expanded(!p1',vars) $

  1839 		poly2expanded(!p3,vars)

  1840 		)

  1841 	       $

  1842 	       (

  1843 		Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1844 		poly2expanded(!p2',vars) $

  1845 		poly2expanded(!p3,vars)

  1846 		)

  1847 	       )

  1848 	      else

  1849 	      (

  1850 	       p1':=mv_skalar_mul(!p1',~1);

  1851 	       p2':=mv_skalar_mul(!p2',~1);

  1852 	       p3:=mv_skalar_mul(!p3,~1);

  1853 	       (

  1854 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1855 		$

  1856 		(

  1857 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1858 		 poly2expanded(!p1',vars) $

  1859 		 poly2expanded(!p3,vars)

  1860 		 )

  1861 		$

  1862 		(

  1863 		 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  1864 		 poly2expanded(!p2',vars) $

  1865 		 poly2expanded(!p3,vars)

  1866 		 )

  1867 		)

  1868 	       )

  1869 	      )

  1870 	     )

  1871     end

  1872 | step_cancel_expanded _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");

  1874 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)

  1875 fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =

  1876     let

  1877 	val p1' = Unsynchronized.ref [];

  1878 	val p2' = Unsynchronized.ref [];

  1879 	val p3  = Unsynchronized.ref []

  1880 	val vars = rev(get_vars(p1) union get_vars(p2));

  1881     in

  1882 	(

  1883 	 p1':=sort (mv_geq LEX_) (mv_shorten((the (term2poly p1 vars )),LEX_));

  1884 	 p2':=sort (mv_geq LEX_) (mv_shorten((the (term2poly p2 vars )),LEX_));

  1885 	 p3 :=sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));

  1887 	 if (!p3)=[(1,mv_null2(vars))] then

  1888 	     (

  1889 	      (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])

  1890 	      )

  1891 	 else

  1892 	     (

  1893 	      p1':=sort (mv_geq LEX_) (#1(mv_division((!p1'),(!p3),LEX_)));

  1894 	      p2':=sort (mv_geq LEX_) (#1(mv_division((!p2'),(!p3),LEX_)));

  1895 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then

  1896 	      (

  1897 	       (

  1898 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1899 		$

  1900 		(

  1901 		 poly2term((!p1'),vars)

  1902 		 )

  1903 		$

  1904 		(

  1905 		 poly2term((!p2'),vars)

  1906 		 )

  1907 		)

  1908 	       ,

  1909 	       if mv_grad(!p3)>0 then

  1910 		   [

  1911 		    (

  1912 		     Const ("Not",[bool]--->bool) $

  1913 		     (

  1914 		      Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $

  1915 		      poly2term((!p3),vars) $

  1916 		      Free("0",HOLogic.realT)

  1917 		      )

  1918 		     )

  1919 		    ]

  1920 	       else

  1921 		   []

  1922 		   )

  1923 	      else

  1924 		  (

  1925 		   p1':=mv_skalar_mul(!p1',~1);

  1926 		   p2':=mv_skalar_mul(!p2',~1);

  1927 		   if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);

  1928 		       (

  1929 			Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1930 			$

  1931 			(

  1932 			 poly2term((!p1'),vars)

  1933 			 )

  1934 			$

  1935 			(

  1936 			 poly2term((!p2'),vars)

  1937 			 )

  1938 			,

  1939 			if mv_grad(!p3)>0 then

  1940 			    [

  1941 			     (

  1942 			      Const ("Not",[bool]--->bool) $

  1943 			      (

  1944 			       Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $

  1945 			       poly2term((!p3),vars) $

  1946 			       Free("0",HOLogic.realT)

  1947 			       )

  1948 			      )

  1949 			     ]

  1950 			else

  1951 			    []

  1952 			    )

  1953 		       )

  1954 		  )

  1955 	     )

  1956     end

  1957   | direct_cancel _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");

  1959 (*. same es direct_cancel, this time for expanded forms (input+output).*)

  1960 fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =

  1961     let

  1962 	val p1' = Unsynchronized.ref [];

  1963 	val p2' = Unsynchronized.ref [];

  1964 	val p3  = Unsynchronized.ref []

  1965 	val vars = rev(get_vars(p1) union get_vars(p2));

  1966     in

  1967 	(

  1968 	 p1':=sort (mv_geq LEX_) (mv_shorten((the (expanded2poly p1 vars )),LEX_));

  1969 	 p2':=sort (mv_geq LEX_) (mv_shorten((the (expanded2poly p2 vars )),LEX_));

  1970 	 p3 :=sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));

  1972 	 if (!p3)=[(1,mv_null2(vars))] then

  1973 	     (

  1974 	      (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])

  1975 	      )

  1976 	 else

  1977 	     (

  1978 	      p1':=sort (mv_geq LEX_) (#1(mv_division((!p1'),(!p3),LEX_)));

  1979 	      p2':=sort (mv_geq LEX_) (#1(mv_division((!p2'),(!p3),LEX_)));

  1980 	      if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then

  1981 	      (

  1982 	       (

  1983 		Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  1984 		$

  1985 		(

  1986 		 poly2expanded((!p1'),vars)

  1987 		 )

  1988 		$

  1989 		(

  1990 		 poly2expanded((!p2'),vars)

  1991 		 )

  1992 		)

  1993 	       ,

  1994 	       if mv_grad(!p3)>0 then

  1995 		   [

  1996 		    (

  1997 		     Const ("Not",[bool]--->bool) $

  1998 		     (

  1999 		      Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $

  2000 		      poly2expanded((!p3),vars) $

  2001 		      Free("0",HOLogic.realT)

  2002 		      )

  2003 		     )

  2004 		    ]

  2005 	       else

  2006 		   []

  2007 		   )

  2008 	      else

  2009 		  (

  2010 		   p1':=mv_skalar_mul(!p1',~1);

  2011 		   p2':=mv_skalar_mul(!p2',~1);

  2012 		   if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);

  2013 		       (

  2014 			Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2015 			$

  2016 			(

  2017 			 poly2expanded((!p1'),vars)

  2018 			 )

  2019 			$

  2020 			(

  2021 			 poly2expanded((!p2'),vars)

  2022 			 )

  2023 			,

  2024 			if mv_grad(!p3)>0 then

  2025 			    [

  2026 			     (

  2027 			      Const ("Not",[bool]--->bool) $

  2028 			      (

  2029 			       Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $

  2030 			       poly2expanded((!p3),vars) $

  2031 			       Free("0",HOLogic.realT)

  2032 			       )

  2033 			      )

  2034 			     ]

  2035 			else

  2036 			    []

  2037 			    )

  2038 		       )

  2039 		  )

  2040 	     )

  2041     end

  2042   | direct_cancel_expanded _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");

  2045 (*. adds two fractions .*)

  2046 fun add_fract ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =

  2047     let

  2048 	val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);

  2049 	val t11'= Unsynchronized.ref  (the(term2poly t11 vars));

  2050 val _= tracing"### add_fract: done t11"

  2051 	val t12'= Unsynchronized.ref  (the(term2poly t12 vars));

  2052 val _= tracing"### add_fract: done t12"

  2053 	val t21'= Unsynchronized.ref  (the(term2poly t21 vars));

  2054 val _= tracing"### add_fract: done t21"

  2055 	val t22'= Unsynchronized.ref  (the(term2poly t22 vars));

  2056 val _= tracing"### add_fract: done t22"

  2057 	val den= Unsynchronized.ref  [];

  2058 	val nom= Unsynchronized.ref  [];

  2059 	val m1= Unsynchronized.ref  [];

  2060 	val m2= Unsynchronized.ref  [];

  2061     in

  2063 	(

  2064 	 den :=sort (mv_geq LEX_) (mv_lcm (!t12') (!t22'));

  2065 tracing"### add_fract: done sort mv_lcm";

  2066 	 m1  :=sort (mv_geq LEX_) (#1(mv_division(!den,!t12',LEX_)));

  2067 tracing"### add_fract: done sort mv_division t12";

  2068 	 m2  :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));

  2069 tracing"### add_fract: done sort mv_division t22";

  2070 	 nom :=sort (mv_geq LEX_)

  2071 		    (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),

  2072 				       mv_mul(!t21',!m2,LEX_),

  2073 				       LEX_),

  2074 				LEX_));

  2075 tracing"### add_fract: done sort mv_add";

  2076 	 (

  2077 	  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2078 	  $

  2079 	  (

  2080 	   poly2term((!nom),vars)

  2081 	   )

  2082 	  $

  2083 	  (

  2084 	   poly2term((!den),vars)

  2085 	   )

  2086 	  )

  2087 	 )

  2088     end

  2089   | add_fract (_,_) = error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");

  2091 (*. adds two expanded fractions .*)

  2092 fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =

  2093     let

  2094 	val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);

  2095 	val t11'= Unsynchronized.ref  (the(expanded2poly t11 vars));

  2096 	val t12'= Unsynchronized.ref  (the(expanded2poly t12 vars));

  2097 	val t21'= Unsynchronized.ref  (the(expanded2poly t21 vars));

  2098 	val t22'= Unsynchronized.ref  (the(expanded2poly t22 vars));

  2099 	val den= Unsynchronized.ref  [];

  2100 	val nom= Unsynchronized.ref  [];

  2101 	val m1= Unsynchronized.ref  [];

  2102 	val m2= Unsynchronized.ref  [];

  2103     in

  2105 	(

  2106 	 den :=sort (mv_geq LEX_) (mv_lcm (!t12') (!t22'));

  2107 	 m1  :=sort (mv_geq LEX_) (#1(mv_division(!den,!t12',LEX_)));

  2108 	 m2  :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));

  2109 	 nom :=sort (mv_geq LEX_) (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),mv_mul(!t21',!m2,LEX_),LEX_),LEX_));

  2110 	 (

  2111 	  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2112 	  $

  2113 	  (

  2114 	   poly2expanded((!nom),vars)

  2115 	   )

  2116 	  $

  2117 	  (

  2118 	   poly2expanded((!den),vars)

  2119 	   )

  2120 	  )

  2121 	 )

  2122     end

  2123   | add_fract_exp (_,_) = error ("RATIONALS_ADD_FRACTION_EXP_EXCEPTION: Invalid add_fraction call");

  2125 (*. adds a list of terms .*)

  2126 fun add_list_of_fractions []= (Free("0",HOLogic.realT),[])

  2127   | add_list_of_fractions [x]= direct_cancel x

  2128   | add_list_of_fractions (x::y::xs) =

  2129     let

  2130 	val (t1a,rest1)=direct_cancel(x);

  2131 val _= tracing"### add_list_of_fractions xs: has done direct_cancel(x)";

  2132 	val (t2a,rest2)=direct_cancel(y);

  2133 val _= tracing"### add_list_of_fractions xs: has done direct_cancel(y)";

  2134 	val (t3a,rest3)=(add_list_of_fractions (add_fract(t1a,t2a)::xs));

  2135 val _= tracing"### add_list_of_fractions xs: has done add_list_of_fraction xs";

  2136 	val (t4a,rest4)=direct_cancel(t3a);

  2137 val _= tracing"### add_list_of_fractions xs: has done direct_cancel(t3a)";

  2138 	val rest=rest1 union rest2 union rest3 union rest4;

  2139     in

  2140 	(tracing"### add_list_of_fractions in";

  2141 	 (

  2142 	 (t4a,rest)

  2143 	 )

  2144 	 )

  2145     end;

  2147 (*. adds a list of expanded terms .*)

  2148 fun add_list_of_fractions_exp []= (Free("0",HOLogic.realT),[])

  2149   | add_list_of_fractions_exp [x]= direct_cancel_expanded x

  2150   | add_list_of_fractions_exp (x::y::xs) =

  2151     let

  2152 	val (t1a,rest1)=direct_cancel_expanded(x);

  2153 	val (t2a,rest2)=direct_cancel_expanded(y);

  2154 	val (t3a,rest3)=(add_list_of_fractions_exp (add_fract_exp(t1a,t2a)::xs));

  2155 	val (t4a,rest4)=direct_cancel_expanded(t3a);

  2156 	val rest=rest1 union rest2 union rest3 union rest4;

  2157     in

  2158 	(

  2159 	 (t4a,rest)

  2160 	 )

  2161     end;

  2163 (*. calculates the lcm of a list of mv_poly .*)

  2164 fun calc_lcm ([x],var)= (x,var)

  2165   | calc_lcm ((x::xs),var) = (mv_lcm x (#1(calc_lcm (xs,var))),var);

  2167 (*. converts a list of terms to a list of mv_poly .*)

  2168 fun t2d([],_)=[]

  2169   | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);

  2171 (*. same as t2d, this time for expanded forms .*)

  2172 fun t2d_exp([],_)=[]

  2173   | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);

  2175 (*. converts a list of fract terms to a list of their denominators .*)

  2176 fun termlist2denominators [] = ([],[])

  2177   | termlist2denominators xs =

  2178     let

  2179 	val xxs= Unsynchronized.ref  xs;

  2180 	val var= Unsynchronized.ref  [];

  2181     in

  2182 	var:=[];

  2183 	while length(!xxs)>0 do

  2184 	    (

  2185 	     let

  2186 		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);

  2187 	     in

  2188 		 (

  2189 		  xxs:=tl(!xxs);

  2190 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

  2191 		  )

  2192 	     end

  2193 	     );

  2194 	    (t2d(xs,!var),!var)

  2195     end;

  2197 (*. calculates the lcm of a list of mv_poly .*)

  2198 fun calc_lcm ([x],var)= (x,var)

  2199   | calc_lcm ((x::xs),var) = (mv_lcm x (#1(calc_lcm (xs,var))),var);

  2201 (*. converts a list of terms to a list of mv_poly .*)

  2202 fun t2d([],_)=[]

  2203   | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);

  2205 (*. same as t2d, this time for expanded forms .*)

  2206 fun t2d_exp([],_)=[]

  2207   | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);

  2209 (*. converts a list of fract terms to a list of their denominators .*)

  2210 fun termlist2denominators [] = ([],[])

  2211   | termlist2denominators xs =

  2212     let

  2213 	val xxs= Unsynchronized.ref  xs;

  2214 	val var= Unsynchronized.ref  [];

  2215     in

  2216 	var:=[];

  2217 	while length(!xxs)>0 do

  2218 	    (

  2219 	     let

  2220 		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);

  2221 	     in

  2222 		 (

  2223 		  xxs:=tl(!xxs);

  2224 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

  2225 		  )

  2226 	     end

  2227 	     );

  2228 	    (t2d(xs,!var),!var)

  2229     end;

  2231 (*. same as termlist2denminators, this time for expanded forms .*)

  2232 fun termlist2denominators_exp [] = ([],[])

  2233   | termlist2denominators_exp xs =

  2234     let

  2235 	val xxs= Unsynchronized.ref  xs;

  2236 	val var= Unsynchronized.ref  [];

  2237     in

  2238 	var:=[];

  2239 	while length(!xxs)>0 do

  2240 	    (

  2241 	     let

  2242 		 val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);

  2243 	     in

  2244 		 (

  2245 		  xxs:=tl(!xxs);

  2246 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

  2247 		  )

  2248 	     end

  2249 	     );

  2250 	    (t2d_exp(xs,!var),!var)

  2251     end;

  2253 (*. reduces all fractions to the least common denominator .*)

  2254 fun com_den(x::xs,denom,den,var)=

  2255     let

  2256 	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;

  2257 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

  2258 	val p3= #1(mv_division(denom,p2,LEX_));

  2259 	val p1var=get_vars(p1');

  2260     in

  2261 	if length(xs)>0 then

  2262 	    if p3=[(1,mv_null2(var))] then

  2263 		(

  2264 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2265 		 $

  2266 		 (

  2267 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2268 		  $

  2269 		  poly2term(the (term2poly p1' p1var),p1var)

  2270 		  $

  2271 		  den

  2272 		  )

  2273 		 $

  2274 		 #1(com_den(xs,denom,den,var))

  2275 		,

  2276 		[]

  2277 		)

  2278 	    else

  2279 		(

  2280 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2281 		 $

  2282 		 (

  2283 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2284 		  $

  2285 		  (

  2286 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2287 		   poly2term(the (term2poly p1' p1var),p1var) $

  2288 		   poly2term(p3,var)

  2289 		   )

  2290 		  $

  2291 		  (

  2292 		   den

  2293 		   )

  2294 		  )

  2295 		 $

  2296 		 #1(com_den(xs,denom,den,var))

  2297 		,

  2298 		[]

  2299 		)

  2300 	else

  2301 	    if p3=[(1,mv_null2(var))] then

  2302 		(

  2303 		 (

  2304 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2305 		  $

  2306 		  poly2term(the (term2poly p1' p1var),p1var)

  2307 		  $

  2308 		  den

  2309 		  )

  2310 		 ,

  2311 		 []

  2312 		 )

  2313 	     else

  2314 		 (

  2315 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2316 		  $

  2317 		  (

  2318 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2319 		   poly2term(the (term2poly p1' p1var),p1var) $

  2320 		   poly2term(p3,var)

  2321 		   )

  2322 		  $

  2323 		  den

  2324 		  ,

  2325 		  []

  2326 		  )

  2327     end;

  2329 (*. same as com_den, this time for expanded forms .*)

  2330 fun com_den_exp(x::xs,denom,den,var)=

  2331     let

  2332 	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;

  2333 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

  2334 	val p3= #1(mv_division(denom,p2,LEX_));

  2335 	val p1var=get_vars(p1');

  2336     in

  2337 	if length(xs)>0 then

  2338 	    if p3=[(1,mv_null2(var))] then

  2339 		(

  2340 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2341 		 $

  2342 		 (

  2343 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2344 		  $

  2345 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

  2346 		  $

  2347 		  den

  2348 		  )

  2349 		 $

  2350 		 #1(com_den_exp(xs,denom,den,var))

  2351 		,

  2352 		[]

  2353 		)

  2354 	    else

  2355 		(

  2356 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2357 		 $

  2358 		 (

  2359 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2360 		  $

  2361 		  (

  2362 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2363 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $

  2364 		   poly2expanded(p3,var)

  2365 		   )

  2366 		  $

  2367 		  (

  2368 		   den

  2369 		   )

  2370 		  )

  2371 		 $

  2372 		 #1(com_den_exp(xs,denom,den,var))

  2373 		,

  2374 		[]

  2375 		)

  2376 	else

  2377 	    if p3=[(1,mv_null2(var))] then

  2378 		(

  2379 		 (

  2380 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2381 		  $

  2382 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

  2383 		  $

  2384 		  den

  2385 		  )

  2386 		 ,

  2387 		 []

  2388 		 )

  2389 	     else

  2390 		 (

  2391 		  Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)

  2392 		  $

  2393 		  (

  2394 		   Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2395 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $

  2396 		   poly2expanded(p3,var)

  2397 		   )

  2398 		  $

  2399 		  den

  2400 		  ,

  2401 		  []

  2402 		  )

  2403     end;

  2405 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon

  2406 -------------------------------------------------------------

  2407 (* WN0210???SK brauch ma des überhaupt *)

  2408 fun com_den2(x::xs,denom,den,var)=

  2409     let

  2410 	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;

  2411 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

  2412 	val p3= #1(mv_division(denom,p2,LEX_));

  2413 	val p1var=get_vars(p1');

  2414     in

  2415 	if length(xs)>0 then

  2416 	    if p3=[(1,mv_null2(var))] then

  2417 		(

  2418 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2419 		 poly2term(the(term2poly p1' p1var),p1var) $

  2420 		 com_den2(xs,denom,den,var)

  2421 		)

  2422 	    else

  2423 		(

  2424 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2425 		 (

  2426 		   let

  2427 		       val p3'=poly2term(p3,var);

  2428 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

  2429 		   in

  2430 		       poly2term(sort (mv_geq LEX_) (mv_mul(the(term2poly p1' vars) ,the(term2poly p3' vars),LEX_)),vars)

  2431 		   end

  2432 		  ) $

  2433 		 com_den2(xs,denom,den,var)

  2434 		)

  2435 	else

  2436 	    if p3=[(1,mv_null2(var))] then

  2437 		(

  2438 		 poly2term(the(term2poly p1' p1var),p1var)

  2439 		 )

  2440 	     else

  2441 		 (

  2442 		   let

  2443 		       val p3'=poly2term(p3,var);

  2444 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

  2445 		   in

  2446 		       poly2term(sort (mv_geq LEX_) (mv_mul(the(term2poly p1' vars) ,the(term2poly p3' vars),LEX_)),vars)

  2447 		   end

  2448 		  )

  2449     end;

  2451 (* WN0210???SK brauch ma des überhaupt *)

  2452 fun com_den_exp2(x::xs,denom,den,var)=

  2453     let

  2454 	val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;

  2455 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

  2456 	val p3= #1(mv_division(denom,p2,LEX_));

  2457 	val p1var=get_vars p1';

  2458     in

  2459 	if length(xs)>0 then

  2460 	    if p3=[(1,mv_null2(var))] then

  2461 		(

  2462 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2463 		 poly2expanded(the (expanded2poly p1' p1var),p1var) $

  2464 		 com_den_exp2(xs,denom,den,var)

  2465 		)

  2466 	    else

  2467 		(

  2468 		 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2469 		 (

  2470 		   let

  2471 		       val p3'=poly2expanded(p3,var);

  2472 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

  2473 		   in

  2474 		       poly2expanded(sort (mv_geq LEX_) (mv_mul(the(expanded2poly p1' vars) ,the(expanded2poly p3' vars),LEX_)),vars)

  2475 		   end

  2476 		  ) $

  2477 		 com_den_exp2(xs,denom,den,var)

  2478 		)

  2479 	else

  2480 	    if p3=[(1,mv_null2(var))] then

  2481 		(

  2482 		 poly2expanded(the (expanded2poly p1' p1var),p1var)

  2483 		 )

  2484 	     else

  2485 		 (

  2486 		   let

  2487 		       val p3'=poly2expanded(p3,var);

  2488 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

  2489 		   in

  2490 		       poly2expanded(sort (mv_geq LEX_) (mv_mul(the(expanded2poly p1' vars) ,the(expanded2poly p3' vars),LEX_)),vars)

  2491 		   end

  2492 		  )

  2493     end;

  2494 ---------------------------------------------------------*)

  2497 (*. searches for an element y of a list ys, which has an gcd not 1 with x .*)

  2498 fun exists_gcd (x,[]) = false

  2499   | exists_gcd (x,y::ys) = if mv_gcd x y = [(1,mv_null2(#2(hd(x))))] then  exists_gcd (x,ys)

  2500 			   else true;

  2502 (*. divides each element of the list xs with y .*)

  2503 fun list_div ([],y) = []

  2504   | list_div (x::xs,y) =

  2505     let

  2506 	val (d,r)=mv_division(x,y,LEX_);

  2507     in

  2508 	if r=[] then

  2509 	    d::list_div(xs,y)

  2510 	else x::list_div(xs,y)

  2511     end;

  2513 (*. checks if x is in the list ys .*)

  2514 fun in_list (x,[]) = false

  2515   | in_list (x,y::ys) = if x=y then true

  2516 			else in_list(x,ys);

  2518 (*. deletes all equal elements of the list xs .*)

  2519 fun kill_equal [] = []

  2520   | kill_equal (x::xs) = if in_list(x,xs) orelse x=[(1,mv_null2(#2(hd(x))))] then kill_equal(xs)

  2521 			 else x::kill_equal(xs);

  2523 (*. searches for new factors .*)

  2524 fun new_factors [] = []

  2525   | new_factors (list:mv_poly list):mv_poly list =

  2526     let

  2527 	val l = kill_equal list;

  2528 	val len = length(l);

  2529     in

  2530 	if len>=2 then

  2531 	    (

  2532 	     let

  2533 		 val x::y::xs=l;

  2534 		 val gcd=mv_gcd x y;

  2535 	     in

  2536 		 if gcd=[(1,mv_null2(#2(hd(x))))] then

  2537 		     (

  2538 		      if exists_gcd(x,xs) then new_factors (y::xs @ [x])

  2539 		      else x::new_factors(y::xs)

  2540 	             )

  2541 		 else gcd::new_factors(kill_equal(list_div(x::y::xs,gcd)))

  2542 	     end

  2543 	     )

  2544 	else

  2545 	    if len=1 then [hd(l)]

  2546 	    else []

  2547     end;

  2549 (*. gets the factors of a list .*)

  2550 fun get_factors x = new_factors x;

  2552 (*. multiplies the elements of the list .*)

  2553 fun multi_list [] = []

  2554   | multi_list (x::xs) = if xs=[] then x

  2555 			 else mv_mul(x,multi_list xs,LEX_);

  2557 (*. makes a term out of the elements of the list (polynomial representation) .*)

  2558 fun make_term ([],vars) = Free(str_of_int 0,HOLogic.realT)

  2559   | make_term ((x::xs),vars) = if length(xs)=0 then poly2term(sort (mv_geq LEX_) (x),vars)

  2560 			       else

  2561 				   (

  2562 				    Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2563 				    poly2term(sort (mv_geq LEX_) (x),vars) $

  2564 				    make_term(xs,vars)

  2565 				    );

  2567 (*. factorizes the denominator (polynomial representation) .*)

  2568 fun factorize_den (l,den,vars) =

  2569     let

  2570 	val factor_list=kill_equal( (get_factors l));

  2571 	val mlist=multi_list(factor_list);

  2572 	val (last,rest)=mv_division(den,multi_list(factor_list),LEX_);

  2573     in

  2574 	if rest=[] then

  2575 	    (

  2576 	     if last=[(1,mv_null2(vars))] then make_term(factor_list,vars)

  2577 	     else make_term(last::factor_list,vars)

  2578 	     )

  2579 	else error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")

  2580     end;

  2582 (*. makes a term out of the elements of the list (expanded polynomial representation) .*)

  2583 fun make_exp ([],vars) = Free(str_of_int 0,HOLogic.realT)

  2584   | make_exp ((x::xs),vars) = if length(xs)=0 then poly2expanded(sort (mv_geq LEX_) (x),vars)

  2585 			       else

  2586 				   (

  2587 				    Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2588 				    poly2expanded(sort (mv_geq LEX_) (x),vars) $

  2589 				    make_exp(xs,vars)

  2590 				    );

  2592 (*. factorizes the denominator (expanded polynomial representation) .*)

  2593 fun factorize_den_exp (l,den,vars) =

  2594     let

  2595 	val factor_list=kill_equal( (get_factors l));

  2596 	val mlist=multi_list(factor_list);

  2597 	val (last,rest)=mv_division(den,multi_list(factor_list),LEX_);

  2598     in

  2599 	if rest=[] then

  2600 	    (

  2601 	     if last=[(1,mv_null2(vars))] then make_exp(factor_list,vars)

  2602 	     else make_exp(last::factor_list,vars)

  2603 	     )

  2604 	else error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")

  2605     end;

  2607 (*. calculates the common denominator of all elements of the list and multiplies .*)

  2608 (*. the nominators and denominators with the correct factor .*)

  2609 (*. (polynomial representation) .*)

  2610 fun step_add_list_of_fractions []=(Free("0",HOLogic.realT),[]:term list)

  2611   | step_add_list_of_fractions [x]= error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")

  2612   | step_add_list_of_fractions (xs) =

  2613     let

  2614         val den_list=termlist2denominators (xs); (* list of denominators *)

  2615 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

  2616 	val den=factorize_den(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)

  2617     in

  2618 	com_den(xs,denom,den,var)

  2619     end;

  2621 (*. calculates the common denominator of all elements of the list and multiplies .*)

  2622 (*. the nominators and denominators with the correct factor .*)

  2623 (*. (expanded polynomial representation) .*)

  2624 fun step_add_list_of_fractions_exp []  = (Free("0",HOLogic.realT),[]:term list)

  2625   | step_add_list_of_fractions_exp [x] = error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")

  2626   | step_add_list_of_fractions_exp (xs)=

  2627     let

  2628         val den_list=termlist2denominators_exp (xs); (* list of denominators *)

  2629 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

  2630 	val den=factorize_den_exp(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)

  2631     in

  2632 	com_den_exp(xs,denom,den,var)

  2633     end;

  2635 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon

  2636 -------------------------------------------------------------

  2637 (* WN0210???SK brauch ma des überhaupt *)

  2638 fun step_add_list_of_fractions2 []=(Free("0",HOLogic.realT),[]:term list)

  2639   | step_add_list_of_fractions2 [x]=(x,[])

  2640   | step_add_list_of_fractions2 (xs) =

  2641     let

  2642         val den_list=termlist2denominators (xs); (* list of denominators *)

  2643 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

  2644 	val den=factorize_den(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

  2645     in

  2646 	(

  2647 	 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2648 	 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $

  2649 	 poly2term(denom,var)

  2650 	,

  2651 	[]

  2652 	)

  2653     end;

  2655 (* WN0210???SK brauch ma des überhaupt *)

  2656 fun step_add_list_of_fractions2_exp []=(Free("0",HOLogic.realT),[]:term list)

  2657   | step_add_list_of_fractions2_exp [x]=(x,[])

  2658   | step_add_list_of_fractions2_exp (xs) =

  2659     let

  2660         val den_list=termlist2denominators_exp (xs); (* list of denominators *)

  2661 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

  2662 	val den=factorize_den_exp(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

  2663     in

  2664 	(

  2665 	 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2666 	 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $

  2667 	 poly2expanded(denom,var)

  2668 	,

  2669 	[]

  2670 	)

  2671     end;

  2672 ---------------------------------------------- *)

  2675 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)

  2676 fun term2list (t as (Const("Rings.inverse_class.divide",_) $ _ $ _)) = [t]

  2677   | term2list (t as (Const("Atools.pow",_) $ _ $ _)) =

  2678     [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2679 	  t $ Free("1",HOLogic.realT)

  2680      ]

  2681   | term2list (t as (Free(_,_))) =

  2682     [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2683 	  t $  Free("1",HOLogic.realT)

  2684      ]

  2685   | term2list (t as (Const("op *",_) $ _ $ _)) =

  2686     [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $

  2687 	  t $ Free("1",HOLogic.realT)

  2688      ]

  2689   | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)

  2690   | term2list (Const("Groups.minus_class.minus",_) $ t1 $ t2) =

  2691     error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")

  2692   | term2list _ = error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");

  2694 (*.factors out the gcd of nominator and denominator:

  2695    a/b = (a' * gcd)/(b' * gcd),  a,b,gcd  are poly[2].*)

  2696 fun factout_p_  (thy:theory) t = SOME (step_cancel t,[]:term list);

  2697 fun factout_ (thy:theory) t = SOME (step_cancel_expanded t,[]:term list);

  2699 (*.cancels a single fraction with normalform [2]

  2700    resulting in a canceled fraction [2], see factout_ .*)

  2701 fun cancel_p_ (thy:theory) t = (*WN.2.6.03 no rewrite -> NONE !*)

  2702     (let val (t',asm) = direct_cancel(*_expanded ... corrected MG.21.8.03*) t

  2703      in if t = t' then NONE else SOME (t',asm)

  2704      end) handle _ => NONE;

  2705 (*.the same as above with normalform [3]

  2706   val cancel_ :

  2707       theory ->        (*10.02 unused                                    *)

  2708       term -> 	       (*fraction in normalform [3]                      *)

  2709       (term * 	       (*fraction in normalform [3]                      *)

  2710        term list)      (*casual asumptions in normalform [3]             *)

  2711 	  option       (*NONE: the function is not applicable            *).*)

  2712 fun cancel_ (thy:theory) t = SOME (direct_cancel_expanded t) handle _ => NONE;

  2714 (*.transforms sums of at least 2 fractions [3] to

  2715    sums with the least common multiple as nominator.*)

  2716 fun common_nominator_p_ (thy:theory) t =

  2717 ((*tracing("### common_nominator_p_ called");*)

  2718     SOME (step_add_list_of_fractions(term2list(t))) handle _ => NONE

  2719 );

  2720 fun common_nominator_ (thy:theory) t =

  2721     SOME (step_add_list_of_fractions_exp(term2list(t))) handle _ => NONE;

  2723 (*.add 2 or more fractions

  2724 val add_fraction_p_ :

  2725       theory ->        (*10.02 unused                                    *)

  2726       term -> 	       (*2 or more fractions with normalform [2]         *)

  2727       (term * 	       (*one fraction with normalform [2]                *)

  2728        term list)      (*casual assumptions in normalform [2] WN0210???SK  *)

  2729 	  option       (*NONE: the function is not applicable            *).*)

  2730 fun add_fraction_p_ (thy:theory) t =

  2731 (tracing("### add_fraction_p_ called");

  2732     (let val ts = term2list t

  2733      in if 1 < length ts

  2734 	then SOME (add_list_of_fractions ts)

  2735 	else NONE (*error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)

  2736      end) handle _ => NONE

  2737 );

  2738 (*.same as add_fraction_p_ but with normalform [3].*)

  2739 (*SOME (step_add_list_of_fractions2(term2list(t))); *)

  2740 fun add_fraction_ (thy:theory) t =

  2741     if length(term2list(t))>1

  2742     then SOME (add_list_of_fractions_exp(term2list(t))) handle _ => NONE

  2743     else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)

  2744 	NONE;

  2745 fun add_fraction_ (thy:theory) t =

  2746     (if 1 < length (term2list t)

  2747      then SOME (add_list_of_fractions_exp (term2list t))

  2748      else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)

  2749 	 NONE) handle _ => NONE;

  2751 (*SOME (step_add_list_of_fractions2_exp(term2list(t))); *)

  2753 (*. brings the term into a normal form .*)

  2754 fun norm_rational_ (thy:theory) t =

  2755     SOME (add_list_of_fractions(term2list(t))) handle _ => NONE;

  2756 fun norm_expanded_rat_ (thy:theory) t =

  2757     SOME (add_list_of_fractions_exp(term2list(t))) handle _ => NONE;

  2760 (*.evaluates conditions in calculate_Rational.*)

  2761 (*make local with FIXX@ME result:term *term list*)

  2762 val calc_rat_erls = prep_rls(

  2763   Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  2764 	 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *)

  2765 	 rules =

  2766 	 [Calc ("op =",eval_equal "#equal_"),

  2767 	  Calc ("Atools.is'_const",eval_const "#is_const_"),

  2768 	  Thm ("not_true",num_str @{thm not_true}),

  2769 	  Thm ("not_false",num_str @{thm not_false})

  2770 	  ],

  2771 	 scr = EmptyScr});

  2774 (*.simplifies expressions with numerals;

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

  2776    need to have constants to be commuted together respectively.*)

  2777 val calculate_Rational = prep_rls(

  2778     merge_rls "calculate_Rational"

  2779 	(Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  2780 	      erls = calc_rat_erls, srls = Erls, (*asm_thm = [],*)

  2781 	      calc = [],

  2782 	      rules =

  2783 	      [Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),

  2785 	       Thm ("minus_divide_left",

  2786 		    num_str (@{thm minus_divide_left} RS @{thm sym})),

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

  2789 	       Thm ("rat_add",num_str @{thm rat_add}),

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

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

  2792 	       Thm ("rat_add1",num_str @{thm rat_add1}),

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

  2794 		 \"a / c + b / c = (a + b) / c"*)

  2795 	       Thm ("rat_add2",num_str @{thm rat_add2}),

  2796 	       (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> \

  2797 		 \?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)

  2798 	       Thm ("rat_add3",num_str @{thm rat_add3}),

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

  2800 		 \"a + b / c = (a * c) / c + b / c"\

  2801 		 \.... is_const to be omitted here FIXME*)

  2803 	       Thm ("rat_mult",num_str @{thm rat_mult}),

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

  2805 	       Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),

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

  2807 	       Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),

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

  2810 	       Thm ("real_divide_divide1",num_str @{thm real_divide_divide1}),

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

  2812 	       Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}),

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

  2815 	       Thm ("rat_power", num_str @{thm rat_power}),

  2816 	       (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

  2818 	       Thm ("mult_cross",num_str @{thm mult_cross}),

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

  2820 	       Thm ("mult_cross1",num_str @{thm mult_cross1}),

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

  2822 	       Thm ("mult_cross2",num_str @{thm mult_cross2})

  2823 	       (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)

  2824 	       ], scr = EmptyScr})

  2825 	calculate_Poly);

  2827 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)

  2828 fun eval_is_expanded (thmid:string) _

  2829 		       (t as (Const("Rational.is'_expanded", _) $ arg)) thy =

  2830     if is_expanded arg

  2831     then SOME (mk_thmid thmid ""

  2832 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

  2833 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))

  2834     else SOME (mk_thmid thmid ""

  2835 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

  2836 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))

  2837   | eval_is_expanded _ _ _ _ = NONE;

  2839 val rational_erls =

  2840     merge_rls "rational_erls" calculate_Rational

  2841 	      (append_rls "is_expanded" Atools_erls

  2842 			  [Calc ("Rational.is'_expanded", eval_is_expanded "")

  2843 			   ]);

  2846 (*.3 'reverse-rewrite-sets' for symbolic computation on rationals:

  2847  =================================================================

  2848  A[2] 'cancel_p': .

  2849  A[3] 'cancel': .

  2850  B[2] 'common_nominator_p': transforms summands in a term [2]

  2851          to fractions with the (least) common multiple as nominator.

  2852  B[3] 'norm_rational': normalizes arbitrary algebraic terms (without

  2853          radicals and transzendental functions) to one canceled fraction,

  2854 	 nominator and denominator in polynomial form.

  2856 In order to meet isac's requirements for interactive and stepwise calculation,

  2857 each 'reverse-rewerite-set' consists of an initialization for the interpreter

  2858 state and of 4 functions, each of which employs rewriting as much as possible.

  2859 The signature of these functions are the same in each 'reverse-rewrite-set'

  2860 respectively.*)

  2862 (* ************************************************************************* *)

  2864 local(*. cancel_p

  2865 ------------------------

  2866 cancels a single fraction consisting of two (uni- or multivariate)

  2867 polynomials WN0609???SK[2] into another such a fraction; examples:

  2869 	   a^2 + -1*b^2         a + b

  2870         -------------------- = ---------

  2871 	a^2 + -2*a*b + b^2     a + -1*b

  2873         a^2    a

  2874         --- = ---

  2875          a     1

  2877 Remark: the reverse ruleset does _NOT_ work properly with other input !.*)

  2878 (*WN020824 wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)

  2880 val {rules, rew_ord=(_,ro),...} =

  2881     rep_rls (assoc_rls "make_polynomial");

  2882 (*WN060829 ... make_deriv does not terminate with 1st expl above,

  2883            see rational.sml --- investigate rulesets for cancel_p ---*)

  2884 val {rules, rew_ord=(_,ro),...} =

  2885     rep_rls (assoc_rls "rev_rew_p");

  2887 (*.init_state = fn : term -> istate

  2888 initialzies the state of the script interpreter. The state is:

  2890 type rrlsstate =      (*state for reverse rewriting*)

  2891      (term *          (*the current formula*)

  2892       term *          (*the final term*)

  2893       rule list       (*'reverse rule list' (#)*)

  2894 	    list *    (*may be serveral, eg. in norm_rational*)

  2895       (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

  2896        (term *        (*... rewrite with ...*)

  2897 	term list))   (*... assumptions*)

  2898 	  list);      (*derivation from given term to normalform

  2899 		       in reverse order with sym_thm;

  2900                        (#) could be extracted from here by (map #1)*).*)

  2901 (* val {rules, rew_ord=(_,ro),...} =

  2902        rep_rls (assoc_rls "rev_rew_p")        (*USE ALWAYS, SEE val cancel_p*);

  2903    val (thy, eval_rls, ro) =(thy, Atools_erls, ro) (*..val cancel_p*);

  2904    val t = t;

  2905    *)

  2906 fun init_state thy eval_rls ro t =

  2907     let val SOME (t',_) = factout_p_ thy t

  2908         val SOME (t'',asm) = cancel_p_ thy t

  2909         val der = reverse_deriv thy eval_rls rules ro NONE t'

  2910         val der = der @ [(Thm ("real_mult_div_cancel2",

  2911 			       num_str @{thm real_mult_div_cancel2}),

  2912 			  (t'',asm))]

  2913         val rs = (distinct_Thm o (map #1)) der

  2914 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",

  2915 				      "sym_real_mult_0",

  2916 				      "sym_real_mult_1"

  2917 				      (*..insufficient,eg.make_Polynomial*)])rs

  2918     in (t,t'',[rs(*here only _ONE_ to ease locate_rule*)],der) end;

  2920 (*.locate_rule = fn : rule list -> term -> rule

  2921 		      -> (rule * (term * term list) option) list.

  2922   checks a rule R for being a cancel-rule, and if it is,

  2923   then return the list of rules (+ the terms they are rewriting to)

  2924   which need to be applied before R should be applied.

  2925   precondition: the rule is applicable to the argument-term.

  2926 arguments:

  2927   rule list: the reverse rule list

  2928   -> term  : ... to which the rule shall be applied

  2929   -> rule  : ... to be applied to term

  2930 value:

  2931   -> (rule           : a rule rewriting to ...

  2932       * (term        : ... the resulting term ...

  2933          * term list): ... with the assumptions ( //#0).

  2934       ) list         : there may be several such rules;

  2935 		       the list is empty, if the rule has nothing to do

  2936 		       with cancelation.*)

  2937 (* val () = ();

  2938    *)

  2939 fun locate_rule thy eval_rls ro [rs] t r =

  2940     if (id_of_thm r) mem (map (id_of_thm)) rs

  2941     then let val ropt =

  2942 		 rewrite_ thy ro eval_rls true (thm_of_thm r) t;

  2943 	 in case ropt of

  2944 		SOME ta => [(r, ta)]

  2945 	      | NONE => (tracing("### locate_rule:  rewrite "^

  2946 				 (id_of_thm r)^" "^(term2str t)^" = NONE");

  2947 			 []) end

  2948     else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])

  2949   | locate_rule _ _ _ _ _ _ =

  2950     error ("locate_rule: doesnt match rev-sets in istate");

  2952 (*.next_rule = fn : rule list -> term -> rule option

  2953   for a given term return the next rules to be done for cancelling.

  2954 arguments:

  2955   rule list     : the reverse rule list

  2956   term          : the term for which ...

  2957 value:

  2958   -> rule option: ... this rule is appropriate for cancellation;

  2959 		  there may be no such rule (if the term is canceled already.*)

  2960 (* val thy = thy;

  2961    val Rrls {rew_ord=(_,ro),...} = cancel;

  2962    val ([rs],t) = (rss,f);

  2963    next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)

  2965    val (thy, [rs]) = (thy, revsets);

  2966    val Rrls {rew_ord=(_,ro),...} = cancel;

  2967    nex [rs] t;

  2968    *)

  2969 fun next_rule thy eval_rls ro [rs] t =

  2970     let val der = make_deriv thy eval_rls rs ro NONE t;

  2971     in case der of

  2972 (* val (_,r,_)::_ = der;

  2973    *)

  2974 	   (_,r,_)::_ => SOME r

  2975 	 | _ => NONE

  2976     end

  2977   | next_rule _ _ _ _ _ =

  2978     error ("next_rule: doesnt match rev-sets in istate");

  2980 (*.val attach_form = f : rule list -> term -> term

  2981 			 -> (rule * (term * term list)) list

  2982   checks an input term TI, if it may belong to a current cancellation, by

  2983   trying to derive it from the given term TG.

  2984 arguments:

  2985   term   : TG, the last one in the cancellation agreed upon by user + math-eng

  2986   -> term: TI, the next one input by the user

  2987 value:

  2988   -> (rule           : the rule to be applied in order to reach TI

  2989       * (term        : ... obtained by applying the rule ...

  2990          * term list): ... and the respective assumptions.

  2991       ) list         : there may be several such rules;

  2992                        the list is empty, if the users term does not belong

  2993 		       to a cancellation of the term last agreed upon.*)

  2994 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)

  2995     []:(rule * (term * term list)) list;

  2997 in

  2999 val cancel_p =

  3000     Rrls {id = "cancel_p", prepat=[],

  3001 	  rew_ord=("ord_make_polynomial",

  3002 		   ord_make_polynomial false thy),

  3003 	  erls = rational_erls,

  3004 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

  3005 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

  3006 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),

  3007 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

  3008 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

  3009 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

  3010 		     normal_form = cancel_p_ thy,

  3011 		     locate_rule = locate_rule thy Atools_erls ro,

  3012 		     next_rule   = next_rule thy Atools_erls ro,

  3013 		     attach_form = attach_form}}

  3014 end;(*local*)

  3016 local(*.ad (1) 'cancel'

  3017 ------------------------------

  3018 cancels a single fraction consisting of two (uni- or multivariate)

  3019 polynomials WN0609???SK[3] into another such a fraction; examples:

  3021 	   a^2 - b^2           a + b

  3022         -------------------- = ---------

  3023 	a^2 - 2*a*b + b^2      a - *b

  3025 Remark: the reverse ruleset does _NOT_ work properly with other input !.*)

  3026 (*WN 24.8.02: wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)

  3028 (*

  3029 val SOME (Rls {rules=rules,rew_ord=(_,ro),...}) =

  3030     assoc'(!ruleset',"expand_binoms");

  3031 *)

  3032 val {rules=rules,rew_ord=(_,ro),...} =

  3033     rep_rls (assoc_rls "expand_binoms");

  3034 val thy = thy;

  3036 fun init_state thy eval_rls ro t =

  3037     let val SOME (t',_) = factout_ thy t;

  3038         val SOME (t'',asm) = cancel_ thy t;

  3039         val der = reverse_deriv thy eval_rls rules ro NONE t';

  3040         val der = der @ [(Thm ("real_mult_div_cancel2",

  3041 			       num_str @{thm real_mult_div_cancel2}),

  3042 			  (t'',asm))]

  3043         val rs = map #1 der;

  3044     in (t,t'',[rs],der) end;

  3046 fun locate_rule thy eval_rls ro [rs] t r =

  3047     if (id_of_thm r) mem (map (id_of_thm)) rs

  3048     then let val ropt =

  3049 		 rewrite_ thy ro eval_rls true (thm_of_thm r) t;

  3050 	 in case ropt of

  3051 		SOME ta => [(r, ta)]

  3052 	      | NONE => (tracing("### locate_rule:  rewrite "^

  3053 				 (id_of_thm r)^" "^(term2str t)^" = NONE");

  3054 			 []) end

  3055     else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])

  3056   | locate_rule _ _ _ _ _ _ =

  3057     error ("locate_rule: doesnt match rev-sets in istate");

  3059 fun next_rule thy eval_rls ro [rs] t =

  3060     let val der = make_deriv thy eval_rls rs ro NONE t;

  3061     in case der of

  3062 (* val (_,r,_)::_ = der;

  3063    *)

  3064 	   (_,r,_)::_ => SOME r

  3065 	 | _ => NONE

  3066     end

  3067   | next_rule _ _ _ _ _ =

  3068     error ("next_rule: doesnt match rev-sets in istate");

  3070 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)

  3071     []:(rule * (term * term list)) list;

  3073 val pat = parse_patt thy "?r/?s";

  3074 val pre1 = parse_patt thy "?r is_expanded";

  3075 val pre2 = parse_patt thy "?s is_expanded";

  3076 val prepat = [([pre1, pre2], pat)];

  3078 in

  3081 val cancel =

  3082     Rrls {id = "cancel", prepat=prepat,

  3083 	  rew_ord=("ord_make_polynomial",

  3084 		   ord_make_polynomial false thy),

  3085 	  erls = rational_erls,

  3086 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

  3087 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

  3088 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),

  3089 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

  3090 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

  3091 		     normal_form = cancel_ thy,

  3092 		     locate_rule = locate_rule thy Atools_erls ro,

  3093 		     next_rule   = next_rule thy Atools_erls ro,

  3094 		     attach_form = attach_form}}

  3095 end;(*local*)

  3097 local(*.ad [2] 'common_nominator_p'

  3098 ---------------------------------

  3099 FIXME Beschreibung .*)

  3102 val {rules=rules,rew_ord=(_,ro),...} =

  3103     rep_rls (assoc_rls "make_polynomial");

  3104 (*WN060829 ... make_deriv does not terminate with 1st expl above,

  3105            see rational.sml --- investigate rulesets for cancel_p ---*)

  3106 val {rules, rew_ord=(_,ro),...} =

  3107     rep_rls (assoc_rls "rev_rew_p");

  3108 val thy = thy;

  3111 (*.common_nominator_p_ = fn : theory -> term -> (term * term list) option

  3112   as defined above*)

  3114 (*.init_state = fn : term -> istate

  3115 initialzies the state of the interactive interpreter. The state is:

  3117 type rrlsstate =      (*state for reverse rewriting*)

  3118      (term *          (*the current formula*)

  3119       term *          (*the final term*)

  3120       rule list       (*'reverse rule list' (#)*)

  3121 	    list *    (*may be serveral, eg. in norm_rational*)

  3122       (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

  3123        (term *        (*... rewrite with ...*)

  3124 	term list))   (*... assumptions*)

  3125 	  list);      (*derivation from given term to normalform

  3126 		       in reverse order with sym_thm;

  3127                        (#) could be extracted from here by (map #1)*).*)

  3128 fun init_state thy eval_rls ro t =

  3129     let val SOME (t',_) = common_nominator_p_ thy t;

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

  3131         val der = reverse_deriv thy eval_rls rules ro NONE t';

  3132         val der = der @ [(Thm ("real_mult_div_cancel2",

  3133 			       num_str @{thm real_mult_div_cancel2}),

  3134 			  (t'',asm))]

  3135         val rs = (distinct_Thm o (map #1)) der;

  3136 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",

  3137 				      "sym_real_mult_0",

  3138 				      "sym_real_mult_1"]) rs;

  3139     in (t,t'',[rs(*here only _ONE_*)],der) end;

  3141 (* use"knowledge/Rational.ML";

  3142    *)

  3144 (*.locate_rule = fn : rule list -> term -> rule

  3145 		      -> (rule * (term * term list) option) list.

  3146   checks a rule R for being a cancel-rule, and if it is,

  3147   then return the list of rules (+ the terms they are rewriting to)

  3148   which need to be applied before R should be applied.

  3149   precondition: the rule is applicable to the argument-term.

  3150 arguments:

  3151   rule list: the reverse rule list

  3152   -> term  : ... to which the rule shall be applied

  3153   -> rule  : ... to be applied to term

  3154 value:

  3155   -> (rule           : a rule rewriting to ...

  3156       * (term        : ... the resulting term ...

  3157          * term list): ... with the assumptions ( //#0).

  3158       ) list         : there may be several such rules;

  3159 		       the list is empty, if the rule has nothing to do

  3160 		       with cancelation.*)

  3161 (* val () = ();

  3162    *)

  3163 fun locate_rule thy eval_rls ro [rs] t r =

  3164     if (id_of_thm r) mem (map (id_of_thm)) rs

  3165     then let val ropt =

  3166 		 rewrite_ thy ro eval_rls true (thm_of_thm r) t;

  3167 	 in case ropt of

  3168 		SOME ta => [(r, ta)]

  3169 	      | NONE => (tracing("### locate_rule:  rewrite "^

  3170 				 (id_of_thm r)^" "^(term2str t)^" = NONE");

  3171 			 []) end

  3172     else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])

  3173   | locate_rule _ _ _ _ _ _ =

  3174     error ("locate_rule: doesnt match rev-sets in istate");

  3176 (*.next_rule = fn : rule list -> term -> rule option

  3177   for a given term return the next rules to be done for cancelling.

  3178 arguments:

  3179   rule list     : the reverse rule list

  3180   term          : the term for which ...

  3181 value:

  3182   -> rule option: ... this rule is appropriate for cancellation;

  3183 		  there may be no such rule (if the term is canceled already.*)

  3184 (* val thy = thy;

  3185    val Rrls {rew_ord=(_,ro),...} = cancel;

  3186    val ([rs],t) = (rss,f);

  3187    next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)

  3189    val (thy, [rs]) = (thy, revsets);

  3190    val Rrls {rew_ord=(_,ro),...} = cancel;

  3191    nex [rs] t;

  3192    *)

  3193 fun next_rule thy eval_rls ro [rs] t =

  3194     let val der = make_deriv thy eval_rls rs ro NONE t;

  3195     in case der of

  3196 (* val (_,r,_)::_ = der;

  3197    *)

  3198 	   (_,r,_)::_ => SOME r

  3199 	 | _ => NONE

  3200     end

  3201   | next_rule _ _ _ _ _ =

  3202     error ("next_rule: doesnt match rev-sets in istate");

  3204 (*.val attach_form = f : rule list -> term -> term

  3205 			 -> (rule * (term * term list)) list

  3206   checks an input term TI, if it may belong to a current cancellation, by

  3207   trying to derive it from the given term TG.

  3208 arguments:

  3209   term   : TG, the last one in the cancellation agreed upon by user + math-eng

  3210   -> term: TI, the next one input by the user

  3211 value:

  3212   -> (rule           : the rule to be applied in order to reach TI

  3213       * (term        : ... obtained by applying the rule ...

  3214          * term list): ... and the respective assumptions.

  3215       ) list         : there may be several such rules;

  3216                        the list is empty, if the users term does not belong

  3217 		       to a cancellation of the term last agreed upon.*)

  3218 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)

  3219     []:(rule * (term * term list)) list;

  3221 val pat0 = parse_patt thy "?r/?s+?u/?v";

  3222 val pat1 = parse_patt thy "?r/?s+?u   ";

  3223 val pat2 = parse_patt thy "?r   +?u/?v";

  3224 val prepat = [([HOLogic.true_const], pat0),

  3225 	      ([HOLogic.true_const], pat1),

  3226 	      ([HOLogic.true_const], pat2)];

  3228 in

  3230 (*11.02 schnelle L"osung f"ur RL: Bruch auch gek"urzt;

  3231   besser w"are: auf 1 gemeinsamen Bruchstrich, Nenner und Z"ahler unvereinfacht

  3232   dh. wie common_nominator_p_, aber auf 1 Bruchstrich*)

  3233 val common_nominator_p =

  3234     Rrls {id = "common_nominator_p", prepat=prepat,

  3235 	  rew_ord=("ord_make_polynomial",

  3236 		   ord_make_polynomial false thy),

  3237 	  erls = rational_erls,

  3238 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

  3239 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

  3240 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),

  3241 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

  3242 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

  3243 		     normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)

  3244 		     locate_rule = locate_rule thy Atools_erls ro,

  3245 		     next_rule   = next_rule thy Atools_erls ro,

  3246 		     attach_form = attach_form}}

  3247 end;(*local*)

  3249 local(*.ad [2] 'common_nominator'

  3250 ---------------------------------

  3251 FIXME Beschreibung .*)

  3254 val {rules=rules,rew_ord=(_,ro),...} =

  3255     rep_rls (assoc_rls "make_polynomial");

  3256 val thy = thy;

  3259 (*.common_nominator_ = fn : theory -> term -> (term * term list) option

  3260   as defined above*)

  3262 (*.init_state = fn : term -> istate

  3263 initialzies the state of the interactive interpreter. The state is:

  3264 type rrlsstate =      (*state for reverse rewriting*)

  3265      (term *          (*the current formula*)

  3266       term *          (*the final term*)

  3267       rule list       (*'reverse rule list' (#)*)

  3268 	    list *    (*may be serveral, eg. in norm_rational*)

  3269       (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

  3270        (term *        (*... rewrite with ...*)

  3271 	term list))   (*... assumptions*)

  3272 	  list);      (*derivation from given term to normalform

  3273 		       in reverse order with sym_thm;

  3274                        (#) could be extracted from here by (map #1)*).*)

  3275 fun init_state thy eval_rls ro t =

  3276     let val SOME (t',_) = common_nominator_ thy t;

  3277         val SOME (t'',asm) = add_fraction_ thy t;

  3278         val der = reverse_deriv thy eval_rls rules ro NONE t';

  3279         val der = der @ [(Thm ("real_mult_div_cancel2",

  3280 			       num_str @{thm real_mult_div_cancel2}),

  3281 			  (t'',asm))]

  3282         val rs = (distinct_Thm o (map #1)) der;

  3283 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",

  3284 				      "sym_real_mult_0",

  3285 				      "sym_real_mult_1"]) rs;

  3286     in (t,t'',[rs(*here only _ONE_*)],der) end;

  3288 (*.locate_rule = fn : rule list -> term -> rule

  3289 		      -> (rule * (term * term list) option) list.

  3290   checks a rule R for being a cancel-rule, and if it is,

  3291   then return the list of rules (+ the terms they are rewriting to)

  3292   which need to be applied before R should be applied.

  3293   precondition: the rule is applicable to the argument-term.

  3294 arguments:

  3295   rule list: the reverse rule list

  3296   -> term  : ... to which the rule shall be applied

  3297   -> rule  : ... to be applied to term

  3298 value:

  3299   -> (rule           : a rule rewriting to ...

  3300       * (term        : ... the resulting term ...

  3301          * term list): ... with the assumptions ( //#0).

  3302       ) list         : there may be several such rules;

  3303 		       the list is empty, if the rule has nothing to do

  3304 		       with cancelation.*)

  3305 (* val () = ();

  3306    *)

  3307 fun locate_rule thy eval_rls ro [rs] t r =

  3308     if (id_of_thm r) mem (map (id_of_thm)) rs

  3309     then let val ropt =

  3310 		 rewrite_ thy ro eval_rls true (thm_of_thm r) t;

  3311 	 in case ropt of

  3312 		SOME ta => [(r, ta)]

  3313 	      | NONE => (tracing("### locate_rule:  rewrite "^

  3314 				 (id_of_thm r)^" "^(term2str t)^" = NONE");

  3315 			 []) end

  3316     else (tracing("### locate_rule:  "^(id_of_thm r)^" not mem rrls");[])

  3317   | locate_rule _ _ _ _ _ _ =

  3318     error ("locate_rule: doesnt match rev-sets in istate");

  3320 (*.next_rule = fn : rule list -> term -> rule option

  3321   for a given term return the next rules to be done for cancelling.

  3322 arguments:

  3323   rule list     : the reverse rule list

  3324   term          : the term for which ...

  3325 value:

  3326   -> rule option: ... this rule is appropriate for cancellation;

  3327 		  there may be no such rule (if the term is canceled already.*)

  3328 (* val thy = thy;

  3329    val Rrls {rew_ord=(_,ro),...} = cancel;

  3330    val ([rs],t) = (rss,f);

  3331    next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)

  3333    val (thy, [rs]) = (thy, revsets);

  3334    val Rrls {rew_ord=(_,ro),...} = cancel_p;

  3335    nex [rs] t;

  3336    *)

  3337 fun next_rule thy eval_rls ro [rs] t =

  3338     let val der = make_deriv thy eval_rls rs ro NONE t;

  3339     in case der of

  3340 (* val (_,r,_)::_ = der;

  3341    *)

  3342 	   (_,r,_)::_ => SOME r

  3343 	 | _ => NONE

  3344     end

  3345   | next_rule _ _ _ _ _ =

  3346     error ("next_rule: doesnt match rev-sets in istate");

  3348 (*.val attach_form = f : rule list -> term -> term

  3349 			 -> (rule * (term * term list)) list

  3350   checks an input term TI, if it may belong to a current cancellation, by

  3351   trying to derive it from the given term TG.

  3352 arguments:

  3353   term   : TG, the last one in the cancellation agreed upon by user + math-eng

  3354   -> term: TI, the next one input by the user

  3355 value:

  3356   -> (rule           : the rule to be applied in order to reach TI

  3357       * (term        : ... obtained by applying the rule ...

  3358          * term list): ... and the respective assumptions.

  3359       ) list         : there may be several such rules;

  3360                        the list is empty, if the users term does not belong

  3361 		       to a cancellation of the term last agreed upon.*)

  3362 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)

  3363     []:(rule * (term * term list)) list;

  3365 val pat0 =  parse_patt thy "?r/?s+?u/?v";

  3366 val pat01 = parse_patt thy "?r/?s-?u/?v";

  3367 val pat1 =  parse_patt thy "?r/?s+?u   ";

  3368 val pat11 = parse_patt thy "?r/?s-?u   ";

  3369 val pat2 =  parse_patt thy "?r   +?u/?v";

  3370 val pat21 = parse_patt thy "?r   -?u/?v";

  3371 val prepat = [([HOLogic.true_const], pat0),

  3372 	      ([HOLogic.true_const], pat01),

  3373 	      ([HOLogic.true_const], pat1),

  3374 	      ([HOLogic.true_const], pat11),

  3375 	      ([HOLogic.true_const], pat2),

  3376 	      ([HOLogic.true_const], pat21)];

  3379 in

  3381 val common_nominator =

  3382     Rrls {id = "common_nominator", prepat=prepat,

  3383 	  rew_ord=("ord_make_polynomial",

  3384 		   ord_make_polynomial false thy),

  3385 	  erls = rational_erls,

  3386 	  calc = [("PLUS"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

  3387 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

  3388 		  ("DIVIDE" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")),

  3389 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

  3390 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

  3391 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

  3392 		     normal_form = add_fraction_ (*NOT common_nominator_*) thy,

  3393 		     locate_rule = locate_rule thy Atools_erls ro,

  3394 		     next_rule   = next_rule thy Atools_erls ro,

  3395 		     attach_form = attach_form}}

  3397 end;(*local*)

  3398 end;(*struct*)

  3400 open RationalI;

  3401 (*##*)

  3403 (*.the expression contains + - * ^ / only ?.*)

  3404 fun is_ratpolyexp (Free _) = true

  3405   | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true

  3406   | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true

  3407   | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true

  3408   | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true

  3409   | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true

  3410   | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =

  3411                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  3412   | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =

  3413                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  3414   | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) =

  3415                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  3416   | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =

  3417                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  3418   | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) =

  3419                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  3420   | is_ratpolyexp _ = false;

  3422 (*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)

  3423 fun eval_is_ratpolyexp (thmid:string) _

  3424 		       (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =

  3425     if is_ratpolyexp arg

  3426     then SOME (mk_thmid thmid ""

  3427 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

  3428 	       Trueprop $ (mk_equality (t, HOLogic.true_const)))

  3429     else SOME (mk_thmid thmid ""

  3430 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

  3431 	       Trueprop $ (mk_equality (t, HOLogic.false_const)))

  3432   | eval_is_ratpolyexp _ _ _ _ = NONE;

  3436 (*-------------------18.3.03 --> struct <-----------vvv--*)

  3437 val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)

  3439 (*WN100906 removed in favour of discard_minus = discard_minus_ formerly

  3440    discard binary minus, shift unary minus into -1*;

  3441    unary minus before numerals are put into the numeral by parsing;

  3442    contains absolute minimum of thms for context in norm_Rational

  3443 val discard_minus = prep_rls(

  3444   Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  3445       erls = e_rls, srls = Erls, calc = [],

  3446       rules = [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),

  3447 	       (*"a - b = a + -1 * b"*)

  3448 	       Thm ("sym_real_mult_minus1",

  3449                      num_str (@{thm real_mult_minus1} RS @{thm sym}))

  3450 	       (*- ?z = "-1 * ?z"*)

  3451 	       ],

  3452       scr = EmptyScr

  3453       }):rls;

  3454  *)

  3456 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)

  3457 val powers_erls = prep_rls(

  3458   Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  3459       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

  3460       rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),

  3461 	       Calc ("Atools.is'_even",eval_is_even "#is_even_"),

  3462 	       Calc ("op <",eval_equ "#less_"),

  3463 	       Thm ("not_false", num_str @{thm not_false}),

  3464 	       Thm ("not_true", num_str @{thm not_true}),

  3465 	       Calc ("Groups.plus_class.plus",eval_binop "#add_")

  3466 	       ],

  3467       scr = EmptyScr

  3468       }:rls);

  3469 (*.all powers over + distributed; atoms over * collected, other distributed

  3470    contains absolute minimum of thms for context in norm_Rational .*)

  3471 val powers = prep_rls(

  3472   Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  3473       erls = powers_erls, srls = Erls, calc = [], (*asm_thm = [],*)

  3474       rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),

  3475 	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)

  3476 	       Thm ("realpow_pow",num_str @{thm realpow_pow}),

  3477 	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

  3478 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),

  3479 	       (*"r ^^^ 1 = r"*)

  3480 	       Thm ("realpow_minus_even",num_str @{thm realpow_minus_even}),

  3481 	       (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)

  3482 	       Thm ("realpow_minus_odd",num_str @{thm realpow_minus_odd}),

  3483 	       (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)

  3485 	       (*----- collect atoms over * -----*)

  3486 	       Thm ("realpow_two_atom",num_str @{thm realpow_two_atom}),

  3487 	       (*"r is_atom ==> r * r = r ^^^ 2"*)

  3488 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),

  3489 	       (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)

  3490 	       Thm ("realpow_addI_atom",num_str @{thm realpow_addI_atom}),

  3491 	       (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)

  3493 	       (*----- distribute none-atoms -----*)

  3494 	       Thm ("realpow_def_atom",num_str @{thm realpow_def_atom}),

  3495 	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)

  3496 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI}),

  3497 	       (*"1 ^^^ n = 1"*)

  3498 	       Calc ("Groups.plus_class.plus",eval_binop "#add_")

  3499 	       ],

  3500       scr = EmptyScr

  3501       }:rls);

  3502 (*.contains absolute minimum of thms for context in norm_Rational.*)

  3503 val rat_mult_divide = prep_rls(

  3504   Rls {id = "rat_mult_divide", preconds = [],

  3505        rew_ord = ("dummy_ord",dummy_ord),

  3506       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

  3507       rules = [Thm ("rat_mult",num_str @{thm rat_mult}),

  3508 	       (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

  3509 	       Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),

  3510 	       (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],

  3511 	       otherwise inv.to a / b / c = ...*)

  3512 	       Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),

  3513 	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much

  3514 		     and does not commute a / b * c ^^^ 2 !*)

  3516 	       Thm ("divide_divide_eq_right",

  3517                      num_str @{thm divide_divide_eq_right}),

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

  3519 	       Thm ("divide_divide_eq_left",

  3520                      num_str @{thm divide_divide_eq_left}),

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

  3522 	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")

  3523 	       ],

  3524       scr = EmptyScr

  3525       }:rls);

  3527 (*.contains absolute minimum of thms for context in norm_Rational.*)

  3528 val reduce_0_1_2 = prep_rls(

  3529   Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", dummy_ord),

  3530       erls = e_rls,srls = Erls,calc = [],(*asm_thm = [],*)

  3531       rules = [(*Thm ("divide_1",num_str @{thm divide_1}),

  3532 		 "?x / 1 = ?x" unnecess.for normalform*)

  3533 	       Thm ("mult_1_left",num_str @{thm mult_1_left}),

  3534 	       (*"1 * z = z"*)

  3535 	       (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),

  3536 	       "-1 * z = - z"*)

  3537 	       (*Thm ("real_minus_mult_cancel",num_str @{thm real_minus_mult_cancel}),

  3538 	       "- ?x * - ?y = ?x * ?y"*)

  3540 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),

  3541 	       (*"0 * z = 0"*)

  3542 	       Thm ("add_0_left",num_str @{thm add_0_left}),

  3543 	       (*"0 + z = z"*)

  3544 	       (*Thm ("right_minus",num_str @{thm right_minus}),

  3545 	       "?z + - ?z = 0"*)

  3547 	       Thm ("sym_real_mult_2",

  3548                      num_str (@{thm real_mult_2} RS @{thm sym})),

  3549 	       (*"z1 + z1 = 2 * z1"*)

  3550 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),

  3551 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

  3553 	       Thm ("divide_zero_left",num_str @{thm divide_zero_left})

  3554 	       (*"0 / ?x = 0"*)

  3555 	       ], scr = EmptyScr}:rls);

  3557 (*erls for calculate_Rational;

  3558   make local with FIXX@ME result:term *term list WN0609???SKMG*)

  3559 val norm_rat_erls = prep_rls(

  3560   Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  3561       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

  3562       rules = [Calc ("Atools.is'_const",eval_const "#is_const_")

  3563 	       ], scr = EmptyScr}:rls);

  3565 (*.consists of rls containing the absolute minimum of thms.*)

  3566 (*040209: this version has been used by RL for his equations,

  3567 which is now replaced by MGs version below

  3568 vvv OLD VERSION !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)

  3569 val norm_Rational = prep_rls(

  3570   Rls {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord",dummy_ord),

  3571       erls = norm_rat_erls, srls = Erls, calc = [],

  3572       rules = [(*sequence given by operator precedence*)

  3573 	       Rls_ discard_minus,

  3574 	       Rls_ powers,

  3575 	       Rls_ rat_mult_divide,

  3576 	       Rls_ expand,

  3577 	       Rls_ reduce_0_1_2,

  3578 	       (*^^^^^^^^^ from RL -- not the latest one vvvvvvvvv*)

  3579 	       Rls_ order_add_mult,

  3580 	       Rls_ collect_numerals,

  3581 	       Rls_ add_fractions_p,

  3582 	       Rls_ cancel_p

  3583 	       ],

  3584       scr = EmptyScr}:rls);

  3586 val norm_Rational_parenthesized = prep_rls(

  3587   Seq {id = "norm_Rational_parenthesized", preconds = []:term list,

  3588        rew_ord = ("dummy_ord", dummy_ord),

  3589       erls = Atools_erls, srls = Erls,

  3590       calc = [],

  3591       rules = [Rls_  norm_Rational, (*from RL -- not the latest one*)

  3592 	       Rls_ discard_parentheses

  3593 	       ],

  3594       scr = EmptyScr}:rls);

  3596 (*WN030318???SK: simplifies all but cancel and common_nominator*)

  3597 val simplify_rational =

  3598     merge_rls "simplify_rational" expand_binoms

  3599     (append_rls "divide" calculate_Rational

  3600 		[Thm ("divide_1",num_str @{thm divide_1}),

  3601 		 (*"?x / 1 = ?x"*)

  3602 		 Thm ("rat_mult",num_str @{thm rat_mult}),

  3603 		 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

  3604 		 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),

  3605 		 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],

  3606 		 otherwise inv.to a / b / c = ...*)

  3607 		 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),

  3608 		 (*"?a / ?b * ?c = ?a * ?c / ?b"*)

  3609 		 Thm ("add_minus",num_str @{thm add_minus}),

  3610 		 (*"?a + ?b - ?b = ?a"*)

  3611 		 Thm ("add_minus1",num_str @{thm add_minus1}),

  3612 		 (*"?a - ?b + ?b = ?a"*)

  3613 		 Thm ("divide_minus1",num_str @{thm divide_minus1})

  3614 		 (*"?x / -1 = - ?x"*)

  3615 (*

  3616 ,

  3617 		 Thm ("",num_str @{thm })

  3618 *)

  3619 		 ]);

  3621 (*---------vvv-------------MG ab 1.07.2003--------------vvv-----------*)

  3623 (* ------------------------------------------------------------------ *)

  3624 (*                  Simplifier für beliebige Buchterme                *)

  3625 (* ------------------------------------------------------------------ *)

  3626 (*----------------------- norm_Rational_mg ---------------------------*)

  3627 (*. description of the simplifier see MG-DA.p.56ff .*)

  3628 (* ------------------------------------------------------------------- *)

  3629 val common_nominator_p_rls = prep_rls(

  3630   Rls {id = "common_nominator_p_rls", preconds = [],

  3631        rew_ord = ("dummy_ord",dummy_ord),

  3632 	 erls = e_rls, srls = Erls, calc = [],

  3633 	 rules =

  3634 	 [Rls_ common_nominator_p

  3635 	  (*FIXME.WN0401 ? redesign Rrls - use exhaustively on a term ?

  3636 	    FIXME.WN0510 unnecessary nesting: introduce RRls_ : rls -> rule*)

  3637 	  ],

  3638 	 scr = EmptyScr});

  3639 (* ------------------------------------------------------------------- *)

  3640 val cancel_p_rls = prep_rls(

  3641   Rls {id = "cancel_p_rls", preconds = [],

  3642        rew_ord = ("dummy_ord",dummy_ord),

  3643 	 erls = e_rls, srls = Erls, calc = [],

  3644 	 rules =

  3645 	 [Rls_ cancel_p

  3646 	  (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*)

  3647 	  ],

  3648 	 scr = EmptyScr});

  3649 (* -------------------------------------------------------------------- *)

  3650 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;

  3651     used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)

  3652 val rat_mult_poly = prep_rls(

  3653   Rls {id = "rat_mult_poly", preconds = [],

  3654        rew_ord = ("dummy_ord",dummy_ord),

  3655 	 erls =  append_rls "e_rls-is_polyexp" e_rls

  3656 	         [Calc ("Poly.is'_polyexp", eval_is_polyexp "")],

  3657 	 srls = Erls, calc = [],

  3658 	 rules =

  3659 	 [Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}),

  3660 	  (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)

  3661 	  Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r})

  3662 	  (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)

  3663 	  ],

  3664 	 scr = EmptyScr});

  3666 (* ------------------------------------------------------------------ *)

  3667 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;

  3668     used in looping part norm_Rational_rls, see example DA-M02-main.p.60

  3669     .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = e_rls,

  3670     I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Thm APPLIED; WN051028

  3671     ... WN0609???MG.*)

  3672 val rat_mult_div_pow = prep_rls(

  3673   Rls {id = "rat_mult_div_pow", preconds = [],

  3674        rew_ord = ("dummy_ord",dummy_ord),

  3675        erls = e_rls,

  3676        (*FIXME.WN051028 append_rls "e_rls-is_polyexp" e_rls

  3677 			[Calc ("Poly.is'_polyexp", eval_is_polyexp "")],

  3678          with this correction ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ we get

  3679 	 error "rational.sml.sml: diff.behav. in norm_Rational_mg 29" etc.

  3680          thus we decided to go on with this flaw*)

  3681 		 srls = Erls, calc = [],

  3682       rules = [Thm ("rat_mult",num_str @{thm rat_mult}),

  3683 	       (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

  3684 	       Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}),

  3685 	       (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)

  3686 	       Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),

  3687 	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)

  3689 	       Thm ("real_divide_divide1_mg",

  3690                      num_str @{thm real_divide_divide1_mg}),

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

  3692 	       Thm ("divide_divide_eq_right",

  3693                      num_str @{thm divide_divide_eq_right}),

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

  3695 	       Thm ("divide_divide_eq_left",

  3696                      num_str @{thm divide_divide_eq_left}),

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

  3698 	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),

  3700 	       Thm ("rat_power", num_str @{thm rat_power})

  3701 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

  3702 	       ],

  3703       scr = EmptyScr}:rls);

  3704 (* ------------------------------------------------------------------ *)

  3705 val rat_reduce_1 = prep_rls(

  3706   Rls {id = "rat_reduce_1", preconds = [],

  3707        rew_ord = ("dummy_ord",dummy_ord),

  3708        erls = e_rls, srls = Erls, calc = [],

  3709        rules = [Thm ("divide_1",num_str @{thm divide_1}),

  3710 		(*"?x / 1 = ?x"*)

  3711 		Thm ("mult_1_left",num_str @{thm mult_1_left})

  3712 		(*"1 * z = z"*)

  3713 		],

  3714        scr = EmptyScr}:rls);

  3715 (* ------------------------------------------------------------------ *)

  3716 (*. looping part of norm_Rational(*_mg*) .*)

  3717 val norm_Rational_rls = prep_rls(

  3718    Rls {id = "norm_Rational_rls", preconds = [],

  3719        rew_ord = ("dummy_ord",dummy_ord),

  3720        erls = norm_rat_erls, srls = Erls, calc = [],

  3721        rules = [Rls_ common_nominator_p_rls,

  3722 		Rls_ rat_mult_div_pow,

  3723 		Rls_ make_rat_poly_with_parentheses,

  3724 		Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)

  3725 		Rls_ rat_reduce_1

  3726 		],

  3727        scr = EmptyScr}:rls);

  3728 (* ------------------------------------------------------------------ *)

  3729 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG)

  3730  just be renaming:*)

  3731 val norm_Rational(*_mg*) = prep_rls(

  3732    Seq {id = "norm_Rational"(*_mg*), preconds = [],

  3733        rew_ord = ("dummy_ord",dummy_ord),

  3734        erls = norm_rat_erls, srls = Erls, calc = [],

  3735        rules = [Rls_ discard_minus,

  3736 		Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)

  3737 		Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)

  3738 		Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)

  3739 		Rls_ norm_Rational_rls,   (* the main rls, looping (#)       *)

  3740 		Rls_ discard_parentheses1 (* mult only                       *)

  3741 		],

  3742        scr = EmptyScr}:rls);

  3743 (* ------------------------------------------------------------------ *)

  3745 ruleset' := overwritelthy @{theory} (!ruleset',

  3746   [("calculate_Rational", calculate_Rational),

  3747    ("calc_rat_erls",calc_rat_erls),

  3748    ("rational_erls", rational_erls),

  3749    ("cancel_p", cancel_p),

  3750    ("cancel", cancel),

  3751    ("common_nominator_p", common_nominator_p),

  3752    ("common_nominator_p_rls", common_nominator_p_rls),

  3753    ("common_nominator"  , common_nominator),

  3754    ("discard_minus", discard_minus),

  3755    ("powers_erls", powers_erls),

  3756    ("powers", powers),

  3757    ("rat_mult_divide", rat_mult_divide),

  3758    ("reduce_0_1_2", reduce_0_1_2),

  3759    ("rat_reduce_1", rat_reduce_1),

  3760    ("norm_rat_erls", norm_rat_erls),

  3761    ("norm_Rational", norm_Rational),

  3762    ("norm_Rational_rls", norm_Rational_rls),

  3763    ("norm_Rational_parenthesized", norm_Rational_parenthesized),

  3764    ("rat_mult_poly", rat_mult_poly),

  3765    ("rat_mult_div_pow", rat_mult_div_pow),

  3766    ("cancel_p_rls", cancel_p_rls)

  3767    ]);

  3769 calclist':= overwritel (!calclist',

  3770    [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))

  3771     ]);

  3773 (** problems **)

  3775 store_pbt

  3776  (prep_pbt thy "pbl_simp_rat" [] e_pblID

  3777  (["rational","simplification"],

  3778   [("#Given" ,["TERM t_t"]),

  3779    ("#Where" ,["t_t is_ratpolyexp"]),

  3780    ("#Find"  ,["normalform n_n"])

  3781   ],

  3782   append_rls "e_rls" e_rls [(*for preds in where_*)],

  3783   SOME "Simplifyt_t",

  3784   [["simplification","of_rationals"]]));

  3786 (** methods **)

  3787 val --------------------------------------------------+++++-+++++ = "00000";

  3789 (*WN061025 this methods script is copied from (auto-generated) script

  3790   of norm_Rational in order to ease repair on inform*)

  3791 store_met

  3792     (prep_met thy "met_simp_rat" [] e_metID

  3793 	      (["simplification","of_rationals"],

  3794 	       [("#Given" ,["TERM t_t"]),

  3795 		("#Where" ,["t_t is_ratpolyexp"]),

  3796 		("#Find"  ,["normalform n_n"])

  3797 		],

  3798 	       {rew_ord'="tless_true",

  3799 		rls' = e_rls,

  3800 		calc = [], srls = e_rls,

  3801 		prls = append_rls "simplification_of_rationals_prls" e_rls

  3802 				[(*for preds in where_*)

  3803 				 Calc ("Rational.is'_ratpolyexp",

  3804 				       eval_is_ratpolyexp "")],

  3805 		crls = e_rls, nrls = norm_Rational_rls},

  3806 "Script SimplifyScript (t_t::real) =                             " ^

  3807 "  ((Try (Rewrite_Set discard_minus False) @@                   " ^

  3808 "    Try (Rewrite_Set rat_mult_poly False) @@                    " ^

  3809 "    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^

  3810 "    Try (Rewrite_Set cancel_p_rls False) @@                     " ^

  3811 "    (Repeat                                                     " ^

  3812 "     ((Try (Rewrite_Set common_nominator_p_rls False) @@        " ^

  3813 "       Try (Rewrite_Set rat_mult_div_pow False) @@              " ^

  3814 "       Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^

  3815 "       Try (Rewrite_Set cancel_p_rls False) @@                  " ^

  3816 "       Try (Rewrite_Set rat_reduce_1 False)))) @@               " ^

  3817 "    Try (Rewrite_Set discard_parentheses1 False))               " ^

  3818 "   t_t)"

  3819 	       ));

  3821 *}

  3823 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 38034	928cebc9c4aa
permissions	-rw-r--r--