theory Partial_Fractions imports Rational begin

 subsection {*get the denominator out of a fraction*}

 text {*this function can be put into rule sets*}

 ML {*

 (*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)

 fun eval_get_denominator (thmid:string) _ 

 		      (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = 

     SOME (mk_thmid thmid "" 

             (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

 	          Trueprop $ (mk_equality (t, denom)))

   | eval_get_denominator _ _ _ _ = NONE; 

 *}

 subsection {*get the argument out of a fraction*}

 ML {*

 (*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*)

 (* 

 fun eval_get_argument "Atools.argument'_in" 

 		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =

     if is_Free arg (*could be something to be simplified before*)

     then SOME (term2str t ^ " = " ^ term2str arg,

 	       Trueprop $ (mk_equality (t, arg)))

     else NONE

   | eval_argument_in _ _ _ _ = NONE;

 *)

 *}

 subsection{*rule set for partial fractions*}

 ML {*

 val partial_fraction = 

   Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 

 	  erls = Erls, srls = Erls, calc = [],

 	  rules = [

 				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X")

 		  ],

 	 scr = EmptyScr};

 *}

 subsection{*store the rule set for math engine*}

 ML {*

   overwritelthy @{theory} (!ruleset', 

 	    [("partial_fraction", prep_rls partial_fraction)

 	     ]);

 *}

 end