jan@42344: (* Partial_Fractions
jan@42344:    author: Jan Rocnik, isac team
jan@42344:    Copyright (c) isac team 2011
jan@42344:    Use is subject to license terms.
jan@42344: 
jan@42344: 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
jan@42344:         10        20        30        40        50        60        70        80         90      100
jan@42344: *)
jan@42344: 
neuper@42289: theory Partial_Fractions imports Rational begin
neuper@42289: 
jan@42344: consts
jan@42344: 
jan@42344:   factors_from_solution   :: "real => real"
jan@42344: 
neuper@42289: subsection {*get the denominator out of a fraction*}
jan@42344: text {*this functions have been stored in Rationals.thy and can be put into rule sets*}
jan@42344: 
jan@42344: subsubsection {*get solutions out of list*}
jan@42344: 
jan@42344: 
neuper@42289: ML {*
jan@42344: fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
jan@42344: fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
jan@42344:   let val minus_1 = t |> type_of |> mk_minus_1
jan@42344:   in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
jan@42344: fun fac_from_sol s =
jan@42344:   let val (lhs, rhs) = HOLogic.dest_eq s
jan@42344:   in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
neuper@42289: *}
jan@42344: 
jan@42344: ML {*
jan@42344: e_term
jan@42344: *}
jan@42344: 
jan@42344: ML {*
jan@42344: fun mk_prod prod [] =
jan@42344:       if prod = e_term then error "mk_prod called with []" else prod
jan@42344:   | mk_prod prod (t :: []) =
jan@42344:       if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
jan@42344:   | mk_prod prod (t1 :: t2 :: ts) =
jan@42344:         if prod = e_term 
jan@42344:         then 
jan@42344:            let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
jan@42344:            in mk_prod p ts end 
jan@42344:         else 
jan@42344:            let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
jan@42344:            in mk_prod p (t2 :: ts) end 
jan@42344: *}
jan@42344: 
jan@42344: ML {*
jan@42344: 
jan@42344: 
jan@42344: fun factors_from_solution sol = 
jan@42344:   let val ts = HOLogic.dest_list sol
jan@42344:   in mk_prod e_term (map fac_from_sol ts) end;
jan@42344: 
jan@42344: *}
jan@42344: 
jan@42344: ML {*
jan@42344: (*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
jan@42344: fun eval_factors_from_solution (thmid:string) _ t thy =
jan@42344:     (let val prod = factors_from_solution t
jan@42344:      in SOME (mk_thmid thmid "" 
jan@42344:             (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "", 
jan@42344: 	          Trueprop $ (mk_equality (t, prod)))
jan@42344:      end)
jan@42344:      handle _ => NONE; 
jan@42344: *}
jan@42344: 
jan@42344: 
jan@42344: 
jan@42344: 
jan@42295: text {*rule set for partial fractions*}
neuper@42289: ML {*
neuper@42289: val partial_fraction = 
neuper@42289:   Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@42289: 	  erls = Erls, srls = Erls, calc = [],
neuper@42289: 	  rules = [
jan@42344: 				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#"),
jan@42344: 				    Calc ("Rings.inverse_class.divide", eval_get_numerator "#")
neuper@42289: 		  ],
neuper@42289: 	 scr = EmptyScr};
neuper@42289: *}
jan@42295: text {*store the rule set for math engine*}
neuper@42289: ML {*
neuper@42289:   overwritelthy @{theory} (!ruleset', 
neuper@42289: 	    [("partial_fraction", prep_rls partial_fraction)
neuper@42289: 	     ]);
neuper@42289: *}
neuper@42289: 
jan@42295: 
neuper@42289: end