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; 

*}

text {*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 "#")

		  ],

	 scr = EmptyScr};

*}

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

ML {*

  overwritelthy @{theory} (!ruleset', 

	    [("partial_fraction", prep_rls partial_fraction)

	     ]);

*}

end