checks the order of the operators .*)

     checks the order of the operators .*)

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

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

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

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

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

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

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

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

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

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

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

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

   | test_polynomial _ v = false;  

   | test_polynomial _ v = false;  

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

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

 (*. help function for is_expanded 

 (*. help function for is_expanded 

     checks the order of the operators .*)

     checks the order of the operators .*)

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

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

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

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

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

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

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

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

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

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

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

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

   | test_exp  _ v = false;

   | test_exp  _ v = false;

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

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

 	      )

 	      )

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

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

 	 )

 	 )

     end

     end

     (

     (

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

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

 	 )

 	 )

     (

     (

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

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

 	 )

 	 )

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

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

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

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

 	      )

 	      )

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

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

 	 )

 	 )

     end

     end

     (

     (

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

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

 	 )

 	 )

     (

     (

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

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

 	 )

 	 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     if c1<0 then 	

     if c1<0 then 	

 	exp2term'(others,vars) $

 	exp2term'(others,vars) $

 	( 

 	( 

 	 monom2term2((c1,e1),vars)

 	 monom2term2((c1,e1),vars)

 	 ) 

 	 ) 

     else

     else

 	exp2term'(others,vars) $

 	exp2term'(others,vars) $

 	( 

 	( 

 	 monom2term2((c1,e1),vars)

 	 monom2term2((c1,e1),vars)

 	 );

 	 );

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

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

     end) handle _ => NONE;

     end) handle _ => NONE;

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

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

     let

     let

 	val p1' = Unsynchronized.ref [];

 	val p1' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p3  = Unsynchronized.ref []

 	val p3  = Unsynchronized.ref []

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

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

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

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

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

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

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

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

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

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

 	     (

 	     (

 	      )

 	      )

 	 else

 	 else

 	     (

 	     (

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

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

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

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

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

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

 	      (

 	      (

 	       $ 

 	       $ 

 	       (

 	       (

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

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

 		poly2term(!p1',vars) $ 

 		poly2term(!p1',vars) $ 

 		poly2term(!p3,vars) 

 		poly2term(!p3,vars) 

 	      (

 	      (

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

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

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

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

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

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

 	       (

 	       (

 		$ 

 		$ 

 		(

 		(

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

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

 		 poly2term(!p1',vars) $ 

 		 poly2term(!p1',vars) $ 

 		 poly2term(!p3,vars) 

 		 poly2term(!p3,vars) 

     end

     end

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

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

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

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

     let

     let

 	val p1' = Unsynchronized.ref [];

 	val p1' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p3  = Unsynchronized.ref []

 	val p3  = Unsynchronized.ref []

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

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

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

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

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

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

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

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

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

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

 	     (

 	     (

 	      )

 	      )

 	 else

 	 else

 	     (

 	     (

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

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

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

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

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

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

 	      (

 	      (

 	       $ 

 	       $ 

 	       (

 	       (

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

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

 		poly2expanded(!p1',vars) $ 

 		poly2expanded(!p1',vars) $ 

 		poly2expanded(!p3,vars) 

 		poly2expanded(!p3,vars) 

 	      (

 	      (

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

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

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

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

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

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

 	       (

 	       (

 		$ 

 		$ 

 		(

 		(

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

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

 		 poly2expanded(!p1',vars) $ 

 		 poly2expanded(!p1',vars) $ 

 		 poly2expanded(!p3,vars) 

 		 poly2expanded(!p3,vars) 

 	     )

 	     )

     end

     end

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

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

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

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

     let

     let

 	val p1' = Unsynchronized.ref [];

 	val p1' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p3  = Unsynchronized.ref []

 	val p3  = Unsynchronized.ref []

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

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

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

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

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

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

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

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

 	     (

 	     (

 	      )

 	      )

 	 else

 	 else

 	     (

 	     (

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

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

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

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

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

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

 	      (

 	      (

 	       (

 	       (

 		$ 

 		$ 

 		(

 		(

 		 poly2term((!p1'),vars)

 		 poly2term((!p1'),vars)

 		 ) 

 		 ) 

 		$ 

 		$ 

 		  (

 		  (

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

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

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

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

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

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

 		       (

 		       (

 			$ 

 			$ 

 			(

 			(

 			 poly2term((!p1'),vars)

 			 poly2term((!p1'),vars)

 			 ) 

 			 ) 

 			$ 

 			$ 

 	     )

 	     )

     end

     end

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

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

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

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

     let

     let

 	val p1' = Unsynchronized.ref [];

 	val p1' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p2' = Unsynchronized.ref [];

 	val p3  = Unsynchronized.ref []

 	val p3  = Unsynchronized.ref []

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

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

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

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

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

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

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

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

 	     (

 	     (

 	      )

 	      )

 	 else

 	 else

 	     (

 	     (

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

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

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

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

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

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

 	      (

 	      (

 	       (

 	       (

 		$ 

 		$ 

 		(

 		(

 		 poly2expanded((!p1'),vars)

 		 poly2expanded((!p1'),vars)

 		 ) 

 		 ) 

 		$ 

 		$ 

 		  (

 		  (

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

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

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

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

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

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

 		       (

 		       (

 			$ 

 			$ 

 			(

 			(

 			 poly2expanded((!p1'),vars)

 			 poly2expanded((!p1'),vars)

 			 ) 

 			 ) 

 			$ 

 			$ 

     end

     end

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

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

 (*. adds two fractions .*)

 (*. adds two fractions .*)

     let

     let

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

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

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

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

 val _= writeln"### add_fract: done t11"

 val _= writeln"### add_fract: done t11"

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

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

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

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

 				       LEX_),

 				       LEX_),

 				LEX_));

 				LEX_));

 writeln"### add_fract: done sort mv_add";

 writeln"### add_fract: done sort mv_add";

 	 (

 	 (

 	  $ 

 	  $ 

 	  (

 	  (

 	   poly2term((!nom),vars)

 	   poly2term((!nom),vars)

 	   ) 

 	   ) 

 	  $ 

 	  $ 

 	 )	     

 	 )	     

     end 

     end 

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

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

 (*. adds two expanded fractions .*)

 (*. adds two expanded fractions .*)

     let

     let

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 	 (

 	 (

 	  $ 

 	  $ 

 	  (

 	  (

 	   poly2expanded((!nom),vars)

 	   poly2expanded((!nom),vars)

 	   ) 

 	   ) 

 	  $ 

 	  $ 

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

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

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

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

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

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

 fun t2d([],_)=[] 

 fun t2d([],_)=[] 

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

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

 fun t2d_exp([],_)=[]  

 fun t2d_exp([],_)=[]  

 (*. converts a list of fract terms to a list of their denominators .*)

 (*. converts a list of fract terms to a list of their denominators .*)

 fun termlist2denominators [] = ([],[])

 fun termlist2denominators [] = ([],[])

   | termlist2denominators xs = 

   | termlist2denominators xs = 

     let	

     let	

     in

     in

 	var:=[];

 	var:=[];

 	while length(!xxs)>0 do

 	while length(!xxs)>0 do

 	    (

 	    (

 	     let 

 	     let 

 	     in

 	     in

 		 (

 		 (

 		  xxs:=tl(!xxs);

 		  xxs:=tl(!xxs);

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  )

 		  )

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

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

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

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

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

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

 fun t2d([],_)=[] 

 fun t2d([],_)=[] 

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

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

 fun t2d_exp([],_)=[]  

 fun t2d_exp([],_)=[]  

 (*. converts a list of fract terms to a list of their denominators .*)

 (*. converts a list of fract terms to a list of their denominators .*)

 fun termlist2denominators [] = ([],[])

 fun termlist2denominators [] = ([],[])

   | termlist2denominators xs = 

   | termlist2denominators xs = 

     let	

     let	

     in

     in

 	var:=[];

 	var:=[];

 	while length(!xxs)>0 do

 	while length(!xxs)>0 do

 	    (

 	    (

 	     let 

 	     let 

 	     in

 	     in

 		 (

 		 (

 		  xxs:=tl(!xxs);

 		  xxs:=tl(!xxs);

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  )

 		  )

     in

     in

 	var:=[];

 	var:=[];

 	while length(!xxs)>0 do

 	while length(!xxs)>0 do

 	    (

 	    (

 	     let 

 	     let 

 	     in

 	     in

 		 (

 		 (

 		  xxs:=tl(!xxs);

 		  xxs:=tl(!xxs);

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  var:=((get_vars(p2x)) union (get_vars(p1x)) union (!var))

 		  )

 		  )

     end;

     end;

 (*. reduces all fractions to the least common denominator .*)

 (*. reduces all fractions to the least common denominator .*)

 fun com_den(x::xs,denom,den,var)=

 fun com_den(x::xs,denom,den,var)=

     let 

     let 

 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p1var=get_vars(p1');

 	val p1var=get_vars(p1');

     in     

     in     

 	if length(xs)>0 then 

 	if length(xs)>0 then 

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 $ 

 		 $ 

 		 (

 		 (

 		  $ 

 		  $ 

 		  poly2term(the (term2poly p1' p1var),p1var)

 		  poly2term(the (term2poly p1' p1var),p1var)

 		  $ 

 		  $ 

 		  den	

 		  den	

 		  )    

 		  )    

 		,

 		,

 		[]

 		[]

 		)

 		)

 	    else

 	    else

 		(

 		(

 		 $ 

 		 $ 

 		 (

 		 (

 		  $ 

 		  $ 

 		  (

 		  (

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

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

 		   poly2term(the (term2poly p1' p1var),p1var) $ 

 		   poly2term(the (term2poly p1' p1var),p1var) $ 

 		   poly2term(p3,var)

 		   poly2term(p3,var)

 		)

 		)

 	else

 	else

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 (

 		 (

 		  $ 

 		  $ 

 		  poly2term(the (term2poly p1' p1var),p1var)

 		  poly2term(the (term2poly p1' p1var),p1var)

 		  $ 

 		  $ 

 		  den	

 		  den	

 		  )

 		  )

 		 ,

 		 ,

 		 []

 		 []

 		 )

 		 )

 	     else

 	     else

 		 (

 		 (

 		  $ 

 		  $ 

 		  (

 		  (

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

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

 		   poly2term(the (term2poly p1' p1var),p1var) $ 

 		   poly2term(the (term2poly p1' p1var),p1var) $ 

 		   poly2term(p3,var)

 		   poly2term(p3,var)

     end;

     end;

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

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

 fun com_den_exp(x::xs,denom,den,var)=

 fun com_den_exp(x::xs,denom,den,var)=

     let 

     let 

 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p1var=get_vars(p1');

 	val p1var=get_vars(p1');

     in     

     in     

 	if length(xs)>0 then 

 	if length(xs)>0 then 

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 $ 

 		 $ 

 		 (

 		 (

 		  $ 

 		  $ 

 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

 		  $ 

 		  $ 

 		  den	

 		  den	

 		  )    

 		  )    

 		,

 		,

 		[]

 		[]

 		)

 		)

 	    else

 	    else

 		(

 		(

 		 $ 

 		 $ 

 		 (

 		 (

 		  $ 

 		  $ 

 		  (

 		  (

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

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

 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $ 

 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $ 

 		   poly2expanded(p3,var)

 		   poly2expanded(p3,var)

 		)

 		)

 	else

 	else

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 (

 		 (

 		  $ 

 		  $ 

 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

 		  poly2expanded(the(expanded2poly p1' p1var),p1var)

 		  $ 

 		  $ 

 		  den	

 		  den	

 		  )

 		  )

 		 ,

 		 ,

 		 []

 		 []

 		 )

 		 )

 	     else

 	     else

 		 (

 		 (

 		  $ 

 		  $ 

 		  (

 		  (

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

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

 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $ 

 		   poly2expanded(the(expanded2poly p1' p1var),p1var) $ 

 		   poly2expanded(p3,var)

 		   poly2expanded(p3,var)

 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon 

 (* wird aktuell nicht mehr gebraucht, bei rückänderung schon 

 -------------------------------------------------------------

 -------------------------------------------------------------

 (* WN0210???SK brauch ma des überhaupt *)

 (* WN0210???SK brauch ma des überhaupt *)

 fun com_den2(x::xs,denom,den,var)=

 fun com_den2(x::xs,denom,den,var)=

     let 

     let 

 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

 	val p2= sort (mv_geq LEX_) (the(term2poly p2' var));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p1var=get_vars(p1');

 	val p1var=get_vars(p1');

     in     

     in     

 	if length(xs)>0 then 

 	if length(xs)>0 then 

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 poly2term(the(term2poly p1' p1var),p1var) $ 

 		 poly2term(the(term2poly p1' p1var),p1var) $ 

 		 com_den2(xs,denom,den,var)

 		 com_den2(xs,denom,den,var)

 		)

 		)

 	    else

 	    else

 		(

 		(

 		 (

 		 (

 		   let 

 		   let 

 		       val p3'=poly2term(p3,var);

 		       val p3'=poly2term(p3,var);

 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

 		   in

 		   in

     end;

     end;

 (* WN0210???SK brauch ma des überhaupt *)

 (* WN0210???SK brauch ma des überhaupt *)

 fun com_den_exp2(x::xs,denom,den,var)=

 fun com_den_exp2(x::xs,denom,den,var)=

     let 

     let 

 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

 	val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p3= #1(mv_division(denom,p2,LEX_));

 	val p1var=get_vars p1';

 	val p1var=get_vars p1';

     in     

     in     

 	if length(xs)>0 then 

 	if length(xs)>0 then 

 	    if p3=[(1,mv_null2(var))] then

 	    if p3=[(1,mv_null2(var))] then

 		(

 		(

 		 poly2expanded(the (expanded2poly p1' p1var),p1var) $ 

 		 poly2expanded(the (expanded2poly p1' p1var),p1var) $ 

 		 com_den_exp2(xs,denom,den,var)

 		 com_den_exp2(xs,denom,den,var)

 		)

 		)

 	    else

 	    else

 		(

 		(

 		 (

 		 (

 		   let 

 		   let 

 		       val p3'=poly2expanded(p3,var);

 		       val p3'=poly2expanded(p3,var);

 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

 		       val vars= (((map free2str) o vars) p1') union (((map free2str) o vars) p3');

 		   in

 		   in

         val den_list=termlist2denominators (xs); (* list of denominators *)

         val den_list=termlist2denominators (xs); (* list of denominators *)

 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

 	val den=factorize_den(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

 	val den=factorize_den(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

     in

     in

 	(

 	(

 	 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $

 	 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $

 	 poly2term(denom,var)

 	 poly2term(denom,var)

 	,

 	,

 	[]

 	[]

 	)

 	)

         val den_list=termlist2denominators_exp (xs); (* list of denominators *)

         val den_list=termlist2denominators_exp (xs); (* list of denominators *)

 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

 	val (denom,var)=calc_lcm(den_list);      (* common denominator *)

 	val den=factorize_den_exp(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

 	val den=factorize_den_exp(#1(den_list),denom,var);  (* faktorisierter Nenner !!! *)

     in

     in

 	(

 	(

 	 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $

 	 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $

 	 poly2expanded(denom,var)

 	 poly2expanded(denom,var)

 	,

 	,

 	[]

 	[]

 	)

 	)

     end;

     end;

 ---------------------------------------------- *)

 ---------------------------------------------- *)

 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)

 (*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)

   | term2list (t as (Const("Atools.pow",_) $ _ $ _)) = 

   | term2list (t as (Const("Atools.pow",_) $ _ $ _)) = 

 	  t $ Free("1",HOLogic.realT)

 	  t $ Free("1",HOLogic.realT)

      ]

      ]

   | term2list (t as (Free(_,_))) = 

   | term2list (t as (Free(_,_))) = 

 	  t $  Free("1",HOLogic.realT)

 	  t $  Free("1",HOLogic.realT)

      ]

      ]

   | term2list (t as (Const("op *",_) $ _ $ _)) = 

   | term2list (t as (Const("op *",_) $ _ $ _)) = 

 	  t $ Free("1",HOLogic.realT)

 	  t $ Free("1",HOLogic.realT)

      ]

      ]

     raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")

     raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")

   | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");

   | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");

 (*.factors out the gcd of nominator and denominator:

 (*.factors out the gcd of nominator and denominator:

    a/b = (a' * gcd)/(b' * gcd),  a,b,gcd  are poly[2].*)

    a/b = (a' * gcd)/(b' * gcd),  a,b,gcd  are poly[2].*)

     merge_rls "calculate_Rational"

     merge_rls "calculate_Rational"

 	(Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 

 	(Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 

 	      erls = calc_rat_erls, srls = Erls, (*asm_thm = [],*) 

 	      erls = calc_rat_erls, srls = Erls, (*asm_thm = [],*) 

 	      calc = [], 

 	      calc = [], 

 	      rules = 

 	      rules = 

 	       Thm ("minus_divide_left",

 	       Thm ("minus_divide_left",

 		    num_str (@{thm minus_divide_left} RS @{thm sym})),

 		    num_str (@{thm minus_divide_left} RS @{thm sym})),

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

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

 val cancel_p =

 val cancel_p =

     Rrls {id = "cancel_p", prepat=[],

     Rrls {id = "cancel_p", prepat=[],

 	  rew_ord=("ord_make_polynomial",

 	  rew_ord=("ord_make_polynomial",

 		   ord_make_polynomial false thy),

 		   ord_make_polynomial false thy),

 	  erls = rational_erls,

 	  erls = rational_erls,

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 		     normal_form = cancel_p_ thy,

 		     normal_form = cancel_p_ thy,

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     locate_rule = locate_rule thy Atools_erls ro,

 val cancel = 

 val cancel = 

     Rrls {id = "cancel", prepat=prepat,

     Rrls {id = "cancel", prepat=prepat,

 	  rew_ord=("ord_make_polynomial",

 	  rew_ord=("ord_make_polynomial",

 		   ord_make_polynomial false thy),

 		   ord_make_polynomial false thy),

 	  erls = rational_erls, 

 	  erls = rational_erls, 

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 		     normal_form = cancel_ thy, 

 		     normal_form = cancel_ thy, 

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     next_rule   = next_rule thy Atools_erls ro,

 		     next_rule   = next_rule thy Atools_erls ro,

 val common_nominator_p =

 val common_nominator_p =

     Rrls {id = "common_nominator_p", prepat=prepat,

     Rrls {id = "common_nominator_p", prepat=prepat,

 	  rew_ord=("ord_make_polynomial",

 	  rew_ord=("ord_make_polynomial",

 		   ord_make_polynomial false thy),

 		   ord_make_polynomial false thy),

 	  erls = rational_erls,

 	  erls = rational_erls,

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 		     normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)

 		     normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     next_rule   = next_rule thy Atools_erls ro,

 		     next_rule   = next_rule thy Atools_erls ro,

 val common_nominator =

 val common_nominator =

     Rrls {id = "common_nominator", prepat=prepat,

     Rrls {id = "common_nominator", prepat=prepat,

 	  rew_ord=("ord_make_polynomial",

 	  rew_ord=("ord_make_polynomial",

 		   ord_make_polynomial false thy),

 		   ord_make_polynomial false thy),

 	  erls = rational_erls,

 	  erls = rational_erls,

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 		  ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

 	  (*asm_thm=[("real_mult_div_cancel2","")],*)

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 	  scr=Rfuns {init_state  = init_state thy Atools_erls ro,

 		     normal_form = add_fraction_ (*NOT common_nominator_*) thy,

 		     normal_form = add_fraction_ (*NOT common_nominator_*) thy,

 		     locate_rule = locate_rule thy Atools_erls ro,

 		     locate_rule = locate_rule thy Atools_erls ro,

 open RationalI;

 open RationalI;

 (*##*)

 (*##*)

 (*.the expression contains + - * ^ / only ?.*)

 (*.the expression contains + - * ^ / only ?.*)

 fun is_ratpolyexp (Free _) = true

 fun is_ratpolyexp (Free _) = true

   | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true

   | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true

   | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true

   | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

   | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) = 

   | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) = 

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

   | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) = 

   | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) = 

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

   | is_ratpolyexp _ = false;

   | is_ratpolyexp _ = false;

 (*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)

 (*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)

 fun eval_is_ratpolyexp (thmid:string) _ 

 fun eval_is_ratpolyexp (thmid:string) _ 

       rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),

       rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),

 	       Calc ("Atools.is'_even",eval_is_even "#is_even_"),

 	       Calc ("Atools.is'_even",eval_is_even "#is_even_"),

 	       Calc ("op <",eval_equ "#less_"),

 	       Calc ("op <",eval_equ "#less_"),

 	       Thm ("not_false", num_str @{thm not_false}),

 	       Thm ("not_false", num_str @{thm not_false}),

 	       Thm ("not_true", num_str @{thm not_true}),

 	       Thm ("not_true", num_str @{thm not_true}),

 	       ],

 	       ],

       scr = EmptyScr

       scr = EmptyScr

       }:rls);

       }:rls);

 (*.all powers over + distributed; atoms over * collected, other distributed

 (*.all powers over + distributed; atoms over * collected, other distributed

    contains absolute minimum of thms for context in norm_Rational .*)

    contains absolute minimum of thms for context in norm_Rational .*)

 	       (*----- distribute none-atoms -----*)

 	       (*----- distribute none-atoms -----*)

 	       Thm ("realpow_def_atom",num_str @{thm realpow_def_atom}),

 	       Thm ("realpow_def_atom",num_str @{thm realpow_def_atom}),

 	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)

 	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)

 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI}),

 	       Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI}),

 	       (*"1 ^^^ n = 1"*)

 	       (*"1 ^^^ n = 1"*)

 	       ],

 	       ],

       scr = EmptyScr

       scr = EmptyScr

       }:rls);

       }:rls);

 (*.contains absolute minimum of thms for context in norm_Rational.*)

 (*.contains absolute minimum of thms for context in norm_Rational.*)

 val rat_mult_divide = prep_rls(

 val rat_mult_divide = prep_rls(

                      num_str @{thm divide_divide_eq_right}),

                      num_str @{thm divide_divide_eq_right}),

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

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

 	       Thm ("divide_divide_eq_left",

 	       Thm ("divide_divide_eq_left",

                      num_str @{thm divide_divide_eq_left}),

                      num_str @{thm divide_divide_eq_left}),

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

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

 	       ],

 	       ],

       scr = EmptyScr

       scr = EmptyScr

       }:rls);

       }:rls);

 (*.contains absolute minimum of thms for context in norm_Rational.*)

 (*.contains absolute minimum of thms for context in norm_Rational.*)

                      num_str @{thm divide_divide_eq_right}),

                      num_str @{thm divide_divide_eq_right}),

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

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

 	       Thm ("divide_divide_eq_left",

 	       Thm ("divide_divide_eq_left",

                      num_str @{thm divide_divide_eq_left}),

                      num_str @{thm divide_divide_eq_left}),

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

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

 	       Thm ("rat_power", num_str @{thm rat_power})

 	       Thm ("rat_power", num_str @{thm rat_power})

 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

 	       ],

 	       ],

       scr = EmptyScr}:rls);

       scr = EmptyScr}:rls);