(* 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

ML {*Context.theory_name thy = "Isac"*}

ML{*

val thy = @{theory};

signature PARTFRAC =

sig

  val ansatz_rls : rls

  val ansatz_rls_ : theory -> term -> (term * term list) option

end

*}

consts

  factors_from_solution :: "bool list => real"

  drop_questionmarks    :: "'a => 'a"

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", ("Partial_Fractions.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;

*}

ML {*

(*("drop_questionmarks", ("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks ""))*)

fun eval_drop_questionmarks (thmid:string) _

     (t as Const ("Partial_Fractions.drop_questionmarks", _) $ tm) thy =

        if contains_Var tm

        then

          let

            val tm' = var2free tm

            in SOME (mk_thmid thmid ""

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

                Trueprop $ (mk_equality (t, tm')))

            end

        else NONE

  | eval_drop_questionmarks _ _ _ _ = NONE;

calclist':= overwritel (!calclist',

  [("drop_questionmarks", ("Partial_Fractions.drop'_questionmarks", eval_drop_questionmarks ""))

  ]);

*}

text {* this definition's scope is all Isac; so no equation etc with "A" would be possible:

consts

  A :: "real"

  B :: "real"

*}

axiomatization where

  ansatz_2nd_order: "n / (a*b) = A/a + B/b" and

  equival_trans_2nd_order: "( n/(a*b) = A/a + B/b ) = ( n = A*b + B*a )"

ML {*

val ansatz_rls = prep_rls(

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

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

	  rules = 

	   [Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order})

	   ], 

	 scr = EmptyScr}:rls);

*}

ML {*

val equival_trans = prep_rls(

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

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

	  rules = 

	   [Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})

	   ], 

	 scr = EmptyScr}:rls);

*}

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

ML {*

ruleset' := overwritelthy @{theory} (!ruleset',

  [("ansatz_rls", ansatz_rls),

   ("equival_trans", equival_trans)

   ]);

*}

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};

*}

end