(* Partial_Fractions

   author: Jan Rocnik, isac team

   Copyright (c) isac team 2011

   Use is subject to license terms.

1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80         90      100

*)

theory Partial_Fractions imports Rational begin

consts

  factors_from_solution   :: "bool list => real"

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

text {*this functions have been stored in Rationals.thy and 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; 

*}

subsubsection {*get solutions out of list*}

ML {*

fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)

fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)

  let val minus_1 = t |> type_of |> mk_minus_1

  in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;

fun fac_from_sol s =

  let val (lhs, rhs) = HOLogic.dest_eq s

  in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;

*}

ML {*

e_term

*}

ML {*

fun mk_prod prod [] =

      if prod = e_term then error "mk_prod called with []" else prod

  | mk_prod prod (t :: []) =

      if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)

  | mk_prod prod (t1 :: t2 :: ts) =

        if prod = e_term 

        then 

           let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)

           in mk_prod p ts end 

        else 

           let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)

           in mk_prod p (t2 :: ts) end 

*}

ML {*

fun factors_from_solution sol = 

  let val ts = HOLogic.dest_list sol

  in mk_prod e_term (map fac_from_sol ts) end;

*}

ML {*

(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)

fun eval_factors_from_solution (thmid:string) _

     (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =

       ((let val prod = factors_from_solution sol

         in SOME (mk_thmid thmid ""

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

               Trueprop $ (mk_equality (t, prod)))

         end)

       handle _ => NONE)

 | eval_factors_from_solution _ _ _ _ = 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