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