1 (* rationals, i.e. fractions of multivariate polynomials over the real field
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.
10 theory Rational imports Poly begin
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,
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].
76 'fraction with numerator and nominator both in normalform [2]'
77 'fraction with numerator and nominator both in normalform [3]'
79 'fraction in normalform [2]'
80 'fraction in normalform [3]'
84 a 'simple fraction' is a term with '/' as outmost operator and
85 numerator and nominator in normalform [2] or [3].
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
100 val cancel_ : theory -> term -> (term * term list) option
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].*)
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].*)
129 val norm_rational_ : theory -> term -> (term * term list) option
130 val polynomial2expanded : term -> term option
132 rls (*.evaluates an arbitrary rational term with numerals.*)
134 (*WN0210???SK: fehlen Funktionen, die exportiert werden sollen ? *)
137 (*.**************************************************************************
138 survey on the functions
139 ~~~~~~~~~~~~~~~~~~~~~~~
140 [2] 'polynomial' :rls | [3]'expanded_term':rls
141 --------------------:------------------+-------------------:-----------------
142 factout_p_ : | factout_ :
143 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
175 functions for least common multiple and addition of fractions
176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 ?
191 **************************************************************************.*)
195 structure RationalI : RATIONALI =
199 infix mem ins union; (*WN100819 updating to Isabelle2009-2*)
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;
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)=
241 if (y)>(p div 2) then (y)-p else
243 if (y)<(~p div 2) then p+(y) else (y)
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,
259 fun uv_mod_pdiv (p1:uv_poly) ([]:uv_poly) =
260 raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
261 | uv_mod_pdiv p1 [x] =
263 val xs= Unsynchronized.ref [];
267 xs:=(uv_mod_rem_poly(p1,x));
268 while length(!xs)>0 andalso hd(!xs)=0 do xs:=tl(!xs)
270 else raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");
271 ([]:uv_poly,!xs:uv_poly)
273 | uv_mod_pdiv p1 p2 =
275 val n= uv_mod_deg(p2);
276 val m= Unsynchronized.ref (uv_mod_deg(p1));
277 val p1'= Unsynchronized.ref (rev(p1));
280 val q= Unsynchronized.ref [];
281 val c= Unsynchronized.ref 0;
282 val output= Unsynchronized.ref ([],[]);
285 if (!m)=0 orelse p2=[0]
286 then raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")
297 c:=hd(!p1') div hd(p2');
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');
306 output:=(rev(!q),rev(!p1'))
313 (*. divides p1 by p2 in Zp .*)
314 fun uv_mod_pdivp (p1:uv_poly) (p2:uv_poly) p =
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));
321 val q= Unsynchronized.ref [];
322 val c= Unsynchronized.ref 0;
323 val output= Unsynchronized.ref ([],[]);
326 if (!m)=0 orelse p2=[0] then raise error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
337 c:=uv_mod_mod2(hd(!p1')*(power lc2 1), p);
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;
344 while !p1'<>[] andalso hd(!p1')=0 do
349 output:=(rev(uv_mod_list_modp (!q) (p)),rev(!p1'))
352 !output:uv_poly * uv_poly
356 (*. calculates the remainder of p1/p2 .*)
357 fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = raise 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= raise 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) = raise 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
379 val c= Unsynchronized.ref 0;
384 if !c=0 then raise error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")
385 else uv_mod_div_list(p,!c)
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)=
396 val f = Unsynchronized.ref [];
397 val f'= Unsynchronized.ref p2;
398 val fi= Unsynchronized.ref [];
402 while uv_mod_deg(!f')>0 do
404 f':=uv_mod_prestp (hd(tl(!f))) (hd(!f)) p;
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=
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 [];
430 if uv_mod_deg(p1)>=uv_mod_deg(p2) then
432 p1':=uv_mod_list_modp (uv_mod_pp(p1)) p;
433 p2':=uv_mod_list_modp (uv_mod_pp(p2)) p
437 p1':=uv_mod_list_modp (uv_mod_pp(p2)) p;
438 p2':=uv_mod_list_modp (uv_mod_pp(p1)) p
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))
448 g:=uv_mod_smul_poly(uv_mod_pp(!pc),!d);
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
474 | uv_mod_prim(x,y::ys) = if uv_mod_prim(x,[y])
476 if uv_mod_prim(x,ys) then true
480 (*. gets the first prime, which is greater than p and does not divide g .*)
481 fun uv_mod_nextprime(g,p)=
483 val list= Unsynchronized.ref [2];
484 val exit= Unsynchronized.ref 0;
485 val i = Unsynchronized.ref 2
487 while (!i<p) do (* calculates the primes lower then p *)
489 if uv_mod_prim(!i,!list) then
494 list:= (!i)::(!list);
502 while (!exit=0) do (* calculate next prime which does not divide g *)
504 if uv_mod_prim(!i,!list) then
509 list:= (!i)::(!list);
519 (*. decides if p1 is a factor of p2 in Zp .*)
520 fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= raise 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) = raise 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)=
530 val c= Unsynchronized.ref 0;
531 val r1'= Unsynchronized.ref 0;
532 val d= Unsynchronized.ref 0;
533 val a= Unsynchronized.ref 0;
536 while (uv_mod_mod2((!c)*m1,m2))<>1 do
540 r1':= uv_mod_mod2(r1,m1);
541 d:=uv_mod_mod2(((r2-(!r1'))*(!c)),m2);
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) = raise error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")
549 | uv_mod_cra_2 (x1,[],m1,m2) = raise 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) =
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;
570 if length(!p1)>length(!p2) then ()
579 d:=gcd_int (uv_mod_lc(!p1)) (uv_mod_lc(!p2));
580 g1:=uv_mod_lc(!p1)*uv_mod_lc(!p2);
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)))) *
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)))));
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 ? *)
596 while (!i)<(!p) andalso (abs(uv_mod_mod2((uv_mod_lc(!cp)*(!i)),(!p)))<>1) do
600 cp:=uv_mod_list_modp (map (uv_mod_multi (!i)) (!cp)) (!p)
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 ();
611 while !pn<= !m andalso !m>(!p) andalso !exit=0 do
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 ? *)
618 while (!i)<(!p) andalso ((uv_mod_mod2((uv_mod_lc(!q)*(!i)),(!p)))<>1) do
622 cp:=uv_mod_list_modp (map (uv_mod_multi (!i)) (!cp)) (!p)
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
629 (*print("degree to high!!!\n")*)
633 if uv_mod_deg(!qp)=uv_mod_deg(!q) then
635 q:=uv_mod_cra_2(!q,!qp,!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 ()
642 if uv_mod_deg(!qp)<uv_mod_deg(!q) then
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 ()
654 uv_mod_smul_poly(!q,c):uv_poly
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)=
691 if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
692 else if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true
697 if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
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
702 else raise 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) =
708 val temp= Unsynchronized.ref EQUAL;
712 if length(x)<>length(y) then
713 raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
716 temp:=mv_mg_hlp((map op- (x~~y)));
718 ( if x1=x2 then EQUAL
719 else if x1>x2 then GREATER
728 if length(x)<>length(y) then
729 raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
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
735 else raise error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")
738 (*. cuts the first variable from a polynomial .*)
739 fun mv_cut([]:mv_poly)=[]:mv_poly
740 | mv_cut((x,[])::list) = raise 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)])))
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 [];
773 while (length(!p1o)>0 andalso hd(#2(hd(!p1o)))=lp) do
775 lc:=hd(mv_cut([hd(!p1o)]))::(!lc);
778 if !lc=[] then raise error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();
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) =
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)
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);
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 .*)
828 | mv_getmax(x::p1)= let
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,[]))= raise error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
852 | mv_mdiv(p1:mv_monom,p2:mv_monom)=
854 val c= Unsynchronized.ref (#1(p2));
855 val pp= Unsynchronized.ref [];
858 if !c=0 then raise error("MV_MDIV_EXCEPTION Dividing by zero")
859 else c:=(#1(p1) div #1(p2));
862 pp:=(#2(mv_mmul((1,#2(p1)),(1,(map mv_minus) (#2(p2))))));
863 if mv_is_negativ(!pp) then (0,!pp)
866 else raise error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
870 (*. prints a polynom for (internal use only) .*)
871 fun mv_print_poly([]:mv_poly)=writeln("[]\n")
872 | mv_print_poly((x,y)::[])= writeln("("^Int.toString(x)^","^ints2str(y)^")\n")
873 | mv_print_poly((x,y)::p1) = (writeln("("^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)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
879 | mv_division(f,g,order)=
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;
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 raise 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))
895 while (if (!exit)=0 then not(mv_monom_greater (hd(!g'),hd(!r),order)) else false) do
897 if (#1(mv_lm(!g',order)))<>0 then m:=mv_mdiv(mv_lm(!r,order),mv_lm(!g',order))
898 else raise error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");
902 r:=mv_add((!r),mv_minus2(mv_mul(!g',[!m],order)),order)
905 if (if length(!r)<>0 then length(!g')<>0 else false) then ()
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)= raise error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
924 | mv_divides(x,[]) = raise 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
934 val p1'=mv_shorten(p1,LEX_);
936 if length(p1')=0 then 0
937 else mv_max(hd(#2(hd(p1'))),mv_deg(tl(p1')))
940 (*. gets the maximum exponent of a mv polynomial in the reverse lexicographic term order .*)
941 fun mv_deg2([]:mv_poly) = 0
944 val p1'=mv_shorten(p1,LEX_);
946 if length(p1')=0 then 0
947 else mv_max(hd(rev(#2(hd(p1')))),mv_deg2(tl(p1')))
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) =
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 [];
967 if length(e1)>1 then raise error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
968 else if length(e1)=0 then [c1]
972 while (!count)<=max do
974 if length(!help)>0 andalso hd(#2(hd(!help)))=max-(!count) then
976 list:=(#1(hd(!help)))::(!list);
983 count := (!count) + 1
989 (*. converts a uv-polynomial from uv-representation to mv-representation .*)
990 fun uv_to_poly ([]:uv_poly) = []:mv_poly
993 val count= Unsynchronized.ref 0;
994 val help= Unsynchronized.ref p1;
995 val list= Unsynchronized.ref [];
997 while length(!help)>0 do
999 if hd(!help)=0 then ()
1000 else list:=(hd(!help),[!count])::(!list);
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])] =
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))))));
1015 [(gcd_int (uv_content2(p1)) c,[min])]
1017 | uv_gcd [(c,[e])] p2 =
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))))));
1022 [(gcd_int (uv_content2(p2)) c,[min])]
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) =
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 [];
1037 while length(!x)>1 do
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)))))
1042 t:= #1(mv_division(mv_add(hd(!x),mv_skalar_mul(hd(tl(!x)),~1),LEX_),[(k,!n1)],LEX_));
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 =
1055 val expos= Unsynchronized.ref [];
1056 val pll= Unsynchronized.ref pl;
1060 while length(!pll)>0 andalso hd(!pll)=[] do
1064 if length(!pll)>0 then expos:= #2(hd(hd(!pll))) else expos:=[];
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),
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
1082 val c= Unsynchronized.ref pl;
1083 val c1= Unsynchronized.ref [];
1085 val k= Unsynchronized.ref 1;
1086 val i= Unsynchronized.ref n;
1087 val ppl= Unsynchronized.ref [];
1090 c:=mv_newton_help(!c,!k);
1091 c1:=(hd(!c))::(!c1);
1092 while(length(!c)>1 andalso !k<n) do
1095 while length(!c)>0 andalso hd(!c)=[] do c:=tl(!c);
1096 if !c=[] then () else c:=mv_newton_help(!c,!k);
1098 if !c=[] then () else c1:=(hd(!c))::(!c1)
1100 while hd(!c1)=[] do c1:=tl(!c1);
1103 mv_newton_add (!c1) 1
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)=
1114 val y= Unsynchronized.ref xs;
1115 val x= Unsynchronized.ref [];
1119 while length(!y)>0 do
1121 x:=(map uv_mod_min) ((!x) ~~ (#2(hd(!y))));
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
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)))));
1145 if length(!list)>1 then
1147 while (if length(!list)>0 then (hd(#2(hd(!list)))=(!test)) else false) do
1149 result:=(#1(hd(!list)),tl(#2(hd(!list))))::(!result);
1151 if length(!list)<1 then list:=[]
1152 else list:=tl(!list)
1155 if length(!list)>0 then
1157 list:=mv_gcd (!result) (mv_cut(mv_content(!list)))
1159 else list:=(!result);
1160 list:=mv_correct(!list,0);
1170 (*. calculates the primitiv part of a polynomial .*)
1171 and mv_pp([]:mv_poly) = []:mv_poly
1173 val cont= Unsynchronized.ref [];
1174 val pp= Unsynchronized.ref [];
1176 cont:=mv_content(p1);
1177 pp:=(#1(mv_division(p1,!cont,LEX_)));
1179 then raise error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")
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 =
1189 val xpoly:mv_poly = [(x,xs)];
1190 val ypoly:mv_poly = [(y,ys)];
1193 if xs=ys then [((gcd_int x y),xs)]
1194 else [((gcd_int x y),(map uv_mod_min)(xs~~ys))]:mv_poly
1197 | mv_gcd (p1:mv_poly) ([(y,ys)]) :mv_poly=
1199 [(gcd_int (uv_content2(p1)) (y),(map uv_mod_min)(mv_min_pp(p1)~~ys))]:mv_poly
1201 | mv_gcd ([(y,ys)]:mv_poly) (p2):mv_poly =
1203 [(gcd_int (uv_content2(p2)) (y),(map uv_mod_min)(mv_min_pp(p2)~~ys))]:mv_poly
1205 | mv_gcd (p1':mv_poly) (p2':mv_poly):mv_poly=
1207 val vc=length(#2(hd(p1')));
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)
1214 mv_gcd (mv_content(p1')) (mv_content(p2'))
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 ! .*)
1234 if vc<2 then (* areUnivariate(p1',p2') *)
1236 gcd:=uv_gcd (mv_shorten(p1',LEX_)) (mv_shorten(p2',LEX_))
1243 p1r := mv_lc(p1,LEX_);
1244 p2r := mv_lc(p2,LEX_);
1245 if main_zero(!p1r) andalso
1249 delta := mv_correct((mv_gcd (mv_cut (!p1r)) (mv_cut (!p2r))),0)
1253 delta := mv_gcd (!p1r) (!p2r)
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
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
1271 current_degree:= !d;
1272 interpolation_list:=mv_correct(!gcd_r,0)::(!interpolation_list)
1276 if (!d = !current_degree) then
1278 interpolation_list:=mv_correct(!gcd_r,0)::(!interpolation_list)
1283 if length(!interpolation_list)> uv_mod_min(mv_deg(p1),mv_deg(p2)) then
1285 candidate := mv_newton(rev(!interpolation_list));
1286 if !candidate=[] then ()
1289 candidate:=mv_pp(!candidate);
1290 if mv_divides(!candidate,p1) andalso mv_divides(!candidate,p2) then
1292 gcd:= mv_mul(!candidate,cont,LEX_);
1297 interpolation_list:=[mv_correct(!gcd_r,0)]
1307 (*. calculates the least common divisor of two polynomials .*)
1308 fun mv_lcm (p1:mv_poly) (p2:mv_poly) :mv_poly =
1310 #1(mv_division(mv_mul(p1,p2,LEX_),mv_gcd p1 p2,LEX_))
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
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 ("op +",_) $ 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 ("op +",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
1341 else (test_exp t1 " ") andalso (test_exp t2 " ")
1342 | test_exp (t as Const ("op -",_) $ 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 =
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;
1358 if is_numeral str then
1360 SOME [(((the o int_of_str) str),mv_null2(v))] handle _ => NONE
1366 while ((!len)>(!i)) do
1368 if str=hd((!vh)) then
1379 SOME [(1,rev(!vl))] handle _ => NONE
1382 | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
1384 val t1pp= Unsynchronized.ref [];
1385 val t2pp= Unsynchronized.ref [];
1386 val t1c= Unsynchronized.ref 0;
1387 val t2c= Unsynchronized.ref 0;
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
1399 | term2coef' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $ (t2 as Free (str2,_))) v :mv_poly option=
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;
1409 if (not o is_numeral) str1 andalso is_numeral str2 then
1414 while ((!len)>(!i)) do
1416 if str1=hd((!vh)) then
1418 vl:=((the o int_of_str) str2)::(!vl)
1427 SOME [(1,rev(!vl))] handle _ => NONE
1429 else raise error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
1432 | term2coef' (Const ("op +",_) $ t1 $ t2) v :mv_poly option=
1434 SOME ((the(term2coef' t1 v)) @ (the(term2coef' t2 v))) handle _ => NONE
1436 | term2coef' (Const ("op -",_) $ t1 $ t2) v :mv_poly option=
1438 SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE
1440 | term2coef' (term) v = raise 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
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*)
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 =
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;
1471 if is_numeral str then
1473 SOME [(((the o int_of_str) str),mv_null2 v)] handle _ => NONE
1479 while ((!len)>(!i)) do
1481 if str=hd((!vh)) then
1492 SOME [(1,rev(!vl))] handle _ => NONE
1495 | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
1497 val t1pp= Unsynchronized.ref [];
1498 val t2pp= Unsynchronized.ref [];
1499 val t1c= Unsynchronized.ref 0;
1500 val t2c= Unsynchronized.ref 0;
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)) ) )]
1513 | term2poly' (Const ("Atools.pow",_) $ (t1 as Free (str1,_)) $
1514 (t2 as Free (str2,_))) v :mv_poly option=
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;
1524 if (not o is_numeral) str1 andalso is_numeral str2 then
1529 while ((!len)>(!i)) do
1531 if str1=hd((!vh)) then
1533 vl:=((the o int_of_str) str2)::(!vl)
1542 SOME [(1,rev(!vl))] handle _ => NONE
1544 else raise error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
1547 | term2poly' (Const ("op +",_) $ t1 $ t2) v :mv_poly option =
1549 SOME ((the(term2poly' t1 v)) @ (the(term2poly' t2 v))) handle _ => NONE
1551 | term2poly' (Const ("op -",_) $ t1 $ t2) v :mv_poly option =
1553 SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE
1555 | term2poly' (term) v = raise error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");
1557 (*. translates an Isabelle term into internal representation.
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*)
1565 fun term2poly (t:term) v =
1566 if is_polynomial t then term2poly' t v
1567 else raise 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 raise 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) =
1583 val xss= Unsynchronized.ref xs;
1584 val vv= Unsynchronized.ref v;
1593 if list_is_null(tl(!xss)) then
1595 if hd(!xss)=1 then Free(hd(!vv), HOLogic.realT)
1598 Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1599 Free(hd(!vv), HOLogic.realT) $ Free(str_of_int (hd(!xss)),HOLogic.realT)
1606 Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1607 Free(hd(!vv), HOLogic.realT) $
1608 powerproduct2term(tl(!xss),tl(!vv))
1612 Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1614 Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1615 Free(hd(!vv), HOLogic.realT) $ Free(str_of_int (hd(!xss)),HOLogic.realT)
1617 powerproduct2term(tl(!xss),tl(!vv))
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)
1628 if list_is_null(e) then
1630 Free(str_of_int c,HOLogic.realT)
1636 powerproduct2term(e,v)
1640 Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1641 Free(str_of_int c,HOLogic.realT) $
1642 powerproduct2term(e,v)
1648 (*fun monom2term ((i, is):mv_monom, v) =
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)
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) =
1666 then Free (str_of_int i, HOLogic.realT)
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("op +", [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)
1688 if list_is_null(e) then
1690 Free(str_of_int (abs(c)),HOLogic.realT)
1696 powerproduct2term(e,v)
1700 Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1701 Free(str_of_int (abs(c)),HOLogic.realT) $
1702 powerproduct2term(e,v)
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) =
1712 Const("op -",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1713 exp2term'(others,vars) $
1715 monom2term2((c1,e1),vars)
1718 Const("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1719 exp2term'(others,vars) $
1721 monom2term2((c1,e1),vars)
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 =
1731 val vars=(((map free2str) o vars) t);
1733 SOME (poly2expanded (the (term2poly t vars), vars))
1734 end) handle _ => NONE;
1736 (*. converts a polynomial into polynomial form .*)
1737 fun expanded2polynomial t =
1739 val vars=(((map free2str) o vars) t);
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 ("HOL.divide",_) $ p1 $ p2) =
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));
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
1759 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
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
1769 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1772 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1773 poly2term(!p1',vars) $
1778 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1779 poly2term(!p2',vars) $
1785 p1':=mv_skalar_mul(!p1',~1);
1786 p2':=mv_skalar_mul(!p2',~1);
1787 p3:=mv_skalar_mul(!p3,~1);
1789 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1792 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1793 poly2term(!p1',vars) $
1798 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1799 poly2term(!p2',vars) $
1807 | step_cancel _ = raise 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 ("HOL.divide",_) $ p1 $ p2) =
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));
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
1824 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
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
1834 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1837 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1838 poly2expanded(!p1',vars) $
1839 poly2expanded(!p3,vars)
1843 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1844 poly2expanded(!p2',vars) $
1845 poly2expanded(!p3,vars)
1850 p1':=mv_skalar_mul(!p1',~1);
1851 p2':=mv_skalar_mul(!p2',~1);
1852 p3:=mv_skalar_mul(!p3,~1);
1854 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1857 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1858 poly2expanded(!p1',vars) $
1859 poly2expanded(!p3,vars)
1863 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
1864 poly2expanded(!p2',vars) $
1865 poly2expanded(!p3,vars)
1872 | step_cancel_expanded _ = raise 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 ("HOL.divide",_) $ p1 $ p2) =
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));
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
1889 (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
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
1898 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1901 poly2term((!p1'),vars)
1905 poly2term((!p2'),vars)
1909 if mv_grad(!p3)>0 then
1912 Const ("Not",[bool]--->bool) $
1914 Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
1915 poly2term((!p3),vars) $
1916 Free("0",HOLogic.realT)
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);
1929 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1932 poly2term((!p1'),vars)
1936 poly2term((!p2'),vars)
1939 if mv_grad(!p3)>0 then
1942 Const ("Not",[bool]--->bool) $
1944 Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
1945 poly2term((!p3),vars) $
1946 Free("0",HOLogic.realT)
1957 | direct_cancel _ = raise 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 ("HOL.divide",_) $ p1 $ p2) =
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));
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
1974 (Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
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
1983 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1986 poly2expanded((!p1'),vars)
1990 poly2expanded((!p2'),vars)
1994 if mv_grad(!p3)>0 then
1997 Const ("Not",[bool]--->bool) $
1999 Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
2000 poly2expanded((!p3),vars) $
2001 Free("0",HOLogic.realT)
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);
2014 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2017 poly2expanded((!p1'),vars)
2021 poly2expanded((!p2'),vars)
2024 if mv_grad(!p3)>0 then
2027 Const ("Not",[bool]--->bool) $
2029 Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
2030 poly2expanded((!p3),vars) $
2031 Free("0",HOLogic.realT)
2042 | direct_cancel_expanded _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
2045 (*. adds two fractions .*)
2046 fun add_fract ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
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 _= writeln"### add_fract: done t11"
2051 val t12'= Unsynchronized.ref (the(term2poly t12 vars));
2052 val _= writeln"### add_fract: done t12"
2053 val t21'= Unsynchronized.ref (the(term2poly t21 vars));
2054 val _= writeln"### add_fract: done t21"
2055 val t22'= Unsynchronized.ref (the(term2poly t22 vars));
2056 val _= writeln"### add_fract: done t22"
2057 val den= Unsynchronized.ref [];
2058 val nom= Unsynchronized.ref [];
2059 val m1= Unsynchronized.ref [];
2060 val m2= Unsynchronized.ref [];
2064 den :=sort (mv_geq LEX_) (mv_lcm (!t12') (!t22'));
2065 writeln"### add_fract: done sort mv_lcm";
2066 m1 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t12',LEX_)));
2067 writeln"### add_fract: done sort mv_division t12";
2068 m2 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));
2069 writeln"### 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_),
2075 writeln"### add_fract: done sort mv_add";
2077 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2080 poly2term((!nom),vars)
2084 poly2term((!den),vars)
2089 | add_fract (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
2091 (*. adds two expanded fractions .*)
2092 fun add_fract_exp ((Const("HOL.divide",_) $ t11 $ t12),(Const("HOL.divide",_) $ t21 $ t22)) =
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 [];
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_));
2111 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2114 poly2expanded((!nom),vars)
2118 poly2expanded((!den),vars)
2123 | add_fract_exp (_,_) = raise 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) =
2130 val (t1a,rest1)=direct_cancel(x);
2131 val _= writeln"### add_list_of_fractions xs: has done direct_cancel(x)";
2132 val (t2a,rest2)=direct_cancel(y);
2133 val _= writeln"### 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 _= writeln"### add_list_of_fractions xs: has done add_list_of_fraction xs";
2136 val (t4a,rest4)=direct_cancel(t3a);
2137 val _= writeln"### add_list_of_fractions xs: has done direct_cancel(t3a)";
2138 val rest=rest1 union rest2 union rest3 union rest4;
2140 (writeln"### add_list_of_fractions in";
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) =
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;
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 .*)
2169 | t2d((t as (Const("HOL.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("HOL.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 =
2179 val xxs= Unsynchronized.ref xs;
2180 val var= Unsynchronized.ref [];
2183 while length(!xxs)>0 do
2186 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
2190 var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))
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 .*)
2203 | t2d((t as (Const("HOL.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("HOL.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 =
2213 val xxs= Unsynchronized.ref xs;
2214 val var= Unsynchronized.ref [];
2217 while length(!xxs)>0 do
2220 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
2224 var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))
2231 (*. same as termlist2denminators, this time for expanded forms .*)
2232 fun termlist2denominators_exp [] = ([],[])
2233 | termlist2denominators_exp xs =
2235 val xxs= Unsynchronized.ref xs;
2236 val var= Unsynchronized.ref [];
2239 while length(!xxs)>0 do
2242 val (t as Const ("HOL.divide",_) $ p1x $ p2x)=hd(!xxs);
2246 var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))
2250 (t2d_exp(xs,!var),!var)
2253 (*. reduces all fractions to the least common denominator .*)
2254 fun com_den(x::xs,denom,den,var)=
2256 val (t as Const ("HOL.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');
2261 if length(xs)>0 then
2262 if p3=[(1,mv_null2(var))] then
2264 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2267 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2269 poly2term(the (term2poly p1' p1var),p1var)
2274 #1(com_den(xs,denom,den,var))
2280 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2283 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2286 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2287 poly2term(the (term2poly p1' p1var),p1var) $
2296 #1(com_den(xs,denom,den,var))
2301 if p3=[(1,mv_null2(var))] then
2304 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2306 poly2term(the (term2poly p1' p1var),p1var)
2315 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2318 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2319 poly2term(the (term2poly p1' p1var),p1var) $
2329 (*. same as com_den, this time for expanded forms .*)
2330 fun com_den_exp(x::xs,denom,den,var)=
2332 val (t as Const ("HOL.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');
2337 if length(xs)>0 then
2338 if p3=[(1,mv_null2(var))] then
2340 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2343 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2345 poly2expanded(the(expanded2poly p1' p1var),p1var)
2350 #1(com_den_exp(xs,denom,den,var))
2356 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2359 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2362 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2363 poly2expanded(the(expanded2poly p1' p1var),p1var) $
2364 poly2expanded(p3,var)
2372 #1(com_den_exp(xs,denom,den,var))
2377 if p3=[(1,mv_null2(var))] then
2380 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2382 poly2expanded(the(expanded2poly p1' p1var),p1var)
2391 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
2394 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2395 poly2expanded(the(expanded2poly p1' p1var),p1var) $
2396 poly2expanded(p3,var)
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)=
2410 val (t as Const ("HOL.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');
2415 if length(xs)>0 then
2416 if p3=[(1,mv_null2(var))] then
2418 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2419 poly2term(the(term2poly p1' p1var),p1var) $
2420 com_den2(xs,denom,den,var)
2424 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2427 val p3'=poly2term(p3,var);
2428 val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');
2430 poly2term(sort (mv_geq LEX_) (mv_mul(the(term2poly p1' vars) ,the(term2poly p3' vars),LEX_)),vars)
2433 com_den2(xs,denom,den,var)
2436 if p3=[(1,mv_null2(var))] then
2438 poly2term(the(term2poly p1' p1var),p1var)
2443 val p3'=poly2term(p3,var);
2444 val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');
2446 poly2term(sort (mv_geq LEX_) (mv_mul(the(term2poly p1' vars) ,the(term2poly p3' vars),LEX_)),vars)
2451 (* WN0210???SK brauch ma des überhaupt *)
2452 fun com_den_exp2(x::xs,denom,den,var)=
2454 val (t as Const ("HOL.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';
2459 if length(xs)>0 then
2460 if p3=[(1,mv_null2(var))] then
2462 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2463 poly2expanded(the (expanded2poly p1' p1var),p1var) $
2464 com_den_exp2(xs,denom,den,var)
2468 Const ("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2471 val p3'=poly2expanded(p3,var);
2472 val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');
2474 poly2expanded(sort (mv_geq LEX_) (mv_mul(the(expanded2poly p1' vars) ,the(expanded2poly p3' vars),LEX_)),vars)
2477 com_den_exp2(xs,denom,den,var)
2480 if p3=[(1,mv_null2(var))] then
2482 poly2expanded(the (expanded2poly p1' p1var),p1var)
2487 val p3'=poly2expanded(p3,var);
2488 val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');
2490 poly2expanded(sort (mv_geq LEX_) (mv_mul(the(expanded2poly p1' vars) ,the(expanded2poly p3' vars),LEX_)),vars)
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)
2502 (*. divides each element of the list xs with y .*)
2503 fun list_div ([],y) = []
2504 | list_div (x::xs,y) =
2506 val (d,r)=mv_division(x,y,LEX_);
2510 else x::list_div(xs,y)
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
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 =
2527 val l = kill_equal list;
2528 val len = length(l);
2536 if gcd=[(1,mv_null2(#2(hd(x))))] then
2538 if exists_gcd(x,xs) then new_factors (y::xs @ [x])
2539 else x::new_factors(y::xs)
2541 else gcd::new_factors(kill_equal(list_div(x::y::xs,gcd)))
2545 if len=1 then [hd(l)]
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)
2562 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2563 poly2term(sort (mv_geq LEX_) (x),vars) $
2567 (*. factorizes the denominator (polynomial representation) .*)
2568 fun factorize_den (l,den,vars) =
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_);
2576 if last=[(1,mv_null2(vars))] then make_term(factor_list,vars)
2577 else make_term(last::factor_list,vars)
2579 else raise error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")
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)
2587 Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2588 poly2expanded(sort (mv_geq LEX_) (x),vars) $
2592 (*. factorizes the denominator (expanded polynomial representation) .*)
2593 fun factorize_den_exp (l,den,vars) =
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_);
2601 if last=[(1,mv_null2(vars))] then make_exp(factor_list,vars)
2602 else make_exp(last::factor_list,vars)
2604 else raise error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")
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]= raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")
2612 | step_add_list_of_fractions (xs) =
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 !!! *)
2618 com_den(xs,denom,den,var)
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] = raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")
2626 | step_add_list_of_fractions_exp (xs)=
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 !!! *)
2632 com_den_exp(xs,denom,den,var)
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) =
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 !!! *)
2647 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2648 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $
2649 poly2term(denom,var)
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) =
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 !!! *)
2665 Const ("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2666 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $
2667 poly2expanded(denom,var)
2672 ---------------------------------------------- *)
2675 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)
2676 fun term2list (t as (Const("HOL.divide",_) $ _ $ _)) = [t]
2677 | term2list (t as (Const("Atools.pow",_) $ _ $ _)) =
2678 [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2679 t $ Free("1",HOLogic.realT)
2681 | term2list (t as (Free(_,_))) =
2682 [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2683 t $ Free("1",HOLogic.realT)
2685 | term2list (t as (Const("op *",_) $ _ $ _)) =
2686 [Const("HOL.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2687 t $ Free("1",HOLogic.realT)
2689 | term2list (Const("op +",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
2690 | term2list (Const("op -",_) $ t1 $ t2) =
2691 raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
2692 | term2list _ = raise 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]
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 ((*writeln("### common_nominator_p_ called");*)
2718 SOME (step_add_list_of_fractions(term2list(t))) handle _ => NONE
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 (writeln("### add_fraction_p_ called");
2732 (let val ts = term2list t
2734 then SOME (add_list_of_fractions ts)
2735 else NONE (*raise error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
2736 end) handle _ => NONE
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 (*raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
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 (*raise 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 = [], *)
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})
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 = [],*)
2783 [Calc ("HOL.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)*)
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 =
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;
2840 merge_rls "rational_erls" calculate_Rational
2841 (append_rls "is_expanded" Atools_erls
2842 [Calc ("Rational.is'_expanded", eval_is_expanded "")
2846 (*.3 'reverse-rewrite-sets' for symbolic computation on rationals:
2847 =================================================================
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'
2862 (* ************************************************************************* *)
2865 ------------------------
2866 cancels a single fraction consisting of two (uni- or multivariate)
2867 polynomials WN0609???SK[2] into another such a fraction; examples:
2870 -------------------- = ---------
2871 a^2 + -2*a*b + b^2 a + -1*b
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*);
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}),
2913 val rs = (distinct_Thm o (map #1)) der
2914 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
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.
2927 rule list: the reverse rule list
2928 -> term : ... to which the rule shall be applied
2929 -> rule : ... to be applied to term
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
2939 fun locate_rule thy eval_rls ro [rs] t r =
2940 if (id_of_thm r) mem (map (id_of_thm)) rs
2942 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
2944 SOME ta => [(r, ta)]
2945 | NONE => (writeln("### locate_rule: rewrite "^
2946 (id_of_thm r)^" "^(term2str t)^" = NONE");
2948 else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
2949 | locate_rule _ _ _ _ _ _ =
2950 raise 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.
2955 rule list : the reverse rule list
2956 term : the term for which ...
2958 -> rule option: ... this rule is appropriate for cancellation;
2959 there may be no such rule (if the term is canceled already.*)
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;
2969 fun next_rule thy eval_rls ro [rs] t =
2970 let val der = make_deriv thy eval_rls rs ro NONE t;
2972 (* val (_,r,_)::_ = der;
2974 (_,r,_)::_ => SOME r
2977 | next_rule _ _ _ _ _ =
2978 raise 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.
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
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;
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" ,("op +" ,eval_binop "#add_")),
3005 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3006 ("DIVIDE" ,("HOL.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}}
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:
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*)
3029 val SOME (Rls {rules=rules,rew_ord=(_,ro),...}) =
3030 assoc'(!ruleset',"expand_binoms");
3032 val {rules=rules,rew_ord=(_,ro),...} =
3033 rep_rls (assoc_rls "expand_binoms");
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}),
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
3049 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
3051 SOME ta => [(r, ta)]
3052 | NONE => (writeln("### locate_rule: rewrite "^
3053 (id_of_thm r)^" "^(term2str t)^" = NONE");
3055 else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
3056 | locate_rule _ _ _ _ _ _ =
3057 raise 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;
3062 (* val (_,r,_)::_ = der;
3064 (_,r,_)::_ => SOME r
3067 | next_rule _ _ _ _ _ =
3068 raise 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)];
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" ,("op +" ,eval_binop "#add_")),
3087 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3088 ("DIVIDE" ,("HOL.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}}
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");
3111 (*.common_nominator_p_ = fn : theory -> term -> (term * term list) option
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}),
3135 val rs = (distinct_Thm o (map #1)) der;
3136 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
3138 "sym_real_mult_1"]) rs;
3139 in (t,t'',[rs(*here only _ONE_*)],der) end;
3141 (* use"knowledge/Rational.ML";
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.
3151 rule list: the reverse rule list
3152 -> term : ... to which the rule shall be applied
3153 -> rule : ... to be applied to term
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
3163 fun locate_rule thy eval_rls ro [rs] t r =
3164 if (id_of_thm r) mem (map (id_of_thm)) rs
3166 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
3168 SOME ta => [(r, ta)]
3169 | NONE => (writeln("### locate_rule: rewrite "^
3170 (id_of_thm r)^" "^(term2str t)^" = NONE");
3172 else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
3173 | locate_rule _ _ _ _ _ _ =
3174 raise 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.
3179 rule list : the reverse rule list
3180 term : the term for which ...
3182 -> rule option: ... this rule is appropriate for cancellation;
3183 there may be no such rule (if the term is canceled already.*)
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;
3193 fun next_rule thy eval_rls ro [rs] t =
3194 let val der = make_deriv thy eval_rls rs ro NONE t;
3196 (* val (_,r,_)::_ = der;
3198 (_,r,_)::_ => SOME r
3201 | next_rule _ _ _ _ _ =
3202 raise 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.
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
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)];
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" ,("op +" ,eval_binop "#add_")),
3239 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3240 ("DIVIDE" ,("HOL.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}}
3249 local(*.ad [2] 'common_nominator'
3250 ---------------------------------
3251 FIXME Beschreibung .*)
3254 val {rules=rules,rew_ord=(_,ro),...} =
3255 rep_rls (assoc_rls "make_polynomial");
3259 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
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}),
3282 val rs = (distinct_Thm o (map #1)) der;
3283 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
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.
3295 rule list: the reverse rule list
3296 -> term : ... to which the rule shall be applied
3297 -> rule : ... to be applied to term
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
3307 fun locate_rule thy eval_rls ro [rs] t r =
3308 if (id_of_thm r) mem (map (id_of_thm)) rs
3310 rewrite_ thy ro eval_rls true (thm_of_thm r) t;
3312 SOME ta => [(r, ta)]
3313 | NONE => (writeln("### locate_rule: rewrite "^
3314 (id_of_thm r)^" "^(term2str t)^" = NONE");
3316 else (writeln("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
3317 | locate_rule _ _ _ _ _ _ =
3318 raise 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.
3323 rule list : the reverse rule list
3324 term : the term for which ...
3326 -> rule option: ... this rule is appropriate for cancellation;
3327 there may be no such rule (if the term is canceled already.*)
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;
3337 fun next_rule thy eval_rls ro [rs] t =
3338 let val der = make_deriv thy eval_rls rs ro NONE t;
3340 (* val (_,r,_)::_ = der;
3342 (_,r,_)::_ => SOME r
3345 | next_rule _ _ _ _ _ =
3346 raise 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.
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
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)];
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" ,("op +" ,eval_binop "#add_")),
3387 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3388 ("DIVIDE" ,("HOL.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}}
3403 (*.the expression contains + - * ^ / only ?.*)
3404 fun is_ratpolyexp (Free _) = true
3405 | is_ratpolyexp (Const ("op +",_) $ Free _ $ Free _) = true
3406 | is_ratpolyexp (Const ("op -",_) $ Free _ $ Free _) = true
3407 | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true
3408 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
3409 | is_ratpolyexp (Const ("HOL.divide",_) $ Free _ $ Free _) = true
3410 | is_ratpolyexp (Const ("op +",_) $ t1 $ t2) =
3411 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
3412 | is_ratpolyexp (Const ("op -",_) $ 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 ("HOL.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"*)
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 ("op +",eval_binop "#add_")
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}),
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}),
3498 Calc ("op +",eval_binop "#add_")
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 ("HOL.divide" ,eval_cancel "#divide_e")
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}),
3535 (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),
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}),
3542 Thm ("add_0_left",num_str @{thm add_0_left}),
3544 (*Thm ("right_minus",num_str @{thm right_minus}),
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})
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*)
3575 Rls_ rat_mult_divide,
3578 (*^^^^^^^^^ from RL -- not the latest one vvvvvvvvv*)
3579 Rls_ order_add_mult,
3580 Rls_ collect_numerals,
3581 Rls_ add_fractions_p,
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,
3591 rules = [Rls_ norm_Rational, (*from RL -- not the latest one*)
3592 Rls_ discard_parentheses
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}),
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"*)
3617 Thm ("",num_str @{thm })
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 = [],
3634 [Rls_ common_nominator_p
3635 (*FIXME.WN0401 ? redesign Rrls - use exhaustively on a term ?
3636 FIXME.WN0510 unnecessary nesting: introduce RRls_ : rls -> rule*)
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 = [],
3646 (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*)
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 = [],
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"*)
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
3672 val rat_mult_div_pow = prep_rls(
3673 Rls {id = "rat_mult_div_pow", preconds = [],
3674 rew_ord = ("dummy_ord",dummy_ord),
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 ("HOL.divide" ,eval_cancel "#divide_e"),
3700 Thm ("rat_power", num_str @{thm rat_power})
3701 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
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}),
3711 Thm ("mult_1_left",num_str @{thm mult_1_left})
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*)
3727 scr = EmptyScr}:rls);
3728 (* ------------------------------------------------------------------ *)
3729 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG)
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 *)
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),
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),
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)
3769 calclist':= overwritel (!calclist',
3770 [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))
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"])
3782 append_rls "e_rls" e_rls [(*for preds in where_*)],
3784 [["simplification","of_rationals"]]));
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*)
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"])
3798 {rew_ord'="tless_true",
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) @@ " ^
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)) " ^