jan@42344
|
1 |
(* Partial_Fractions
|
jan@42344
|
2 |
author: Jan Rocnik, isac team
|
jan@42344
|
3 |
Copyright (c) isac team 2011
|
jan@42344
|
4 |
Use is subject to license terms.
|
jan@42344
|
5 |
|
jan@42344
|
6 |
1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
|
jan@42344
|
7 |
10 20 30 40 50 60 70 80 90 100
|
jan@42344
|
8 |
*)
|
jan@42344
|
9 |
|
neuper@42289
|
10 |
theory Partial_Fractions imports Rational begin
|
neuper@42289
|
11 |
|
jan@42344
|
12 |
consts
|
jan@42344
|
13 |
|
jan@42344
|
14 |
factors_from_solution :: "real => real"
|
jan@42344
|
15 |
|
neuper@42289
|
16 |
subsection {*get the denominator out of a fraction*}
|
jan@42344
|
17 |
text {*this functions have been stored in Rationals.thy and can be put into rule sets*}
|
jan@42344
|
18 |
|
jan@42344
|
19 |
subsubsection {*get solutions out of list*}
|
jan@42344
|
20 |
|
jan@42344
|
21 |
|
neuper@42289
|
22 |
ML {*
|
jan@42344
|
23 |
fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
|
jan@42344
|
24 |
fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
|
jan@42344
|
25 |
let val minus_1 = t |> type_of |> mk_minus_1
|
jan@42344
|
26 |
in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
|
jan@42344
|
27 |
fun fac_from_sol s =
|
jan@42344
|
28 |
let val (lhs, rhs) = HOLogic.dest_eq s
|
jan@42344
|
29 |
in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
|
neuper@42289
|
30 |
*}
|
jan@42344
|
31 |
|
jan@42344
|
32 |
ML {*
|
jan@42344
|
33 |
e_term
|
jan@42344
|
34 |
*}
|
jan@42344
|
35 |
|
jan@42344
|
36 |
ML {*
|
jan@42344
|
37 |
fun mk_prod prod [] =
|
jan@42344
|
38 |
if prod = e_term then error "mk_prod called with []" else prod
|
jan@42344
|
39 |
| mk_prod prod (t :: []) =
|
jan@42344
|
40 |
if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
|
jan@42344
|
41 |
| mk_prod prod (t1 :: t2 :: ts) =
|
jan@42344
|
42 |
if prod = e_term
|
jan@42344
|
43 |
then
|
jan@42344
|
44 |
let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
|
jan@42344
|
45 |
in mk_prod p ts end
|
jan@42344
|
46 |
else
|
jan@42344
|
47 |
let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
|
jan@42344
|
48 |
in mk_prod p (t2 :: ts) end
|
jan@42344
|
49 |
*}
|
jan@42344
|
50 |
|
jan@42344
|
51 |
ML {*
|
jan@42344
|
52 |
|
jan@42344
|
53 |
|
jan@42344
|
54 |
fun factors_from_solution sol =
|
jan@42344
|
55 |
let val ts = HOLogic.dest_list sol
|
jan@42344
|
56 |
in mk_prod e_term (map fac_from_sol ts) end;
|
jan@42344
|
57 |
|
jan@42344
|
58 |
*}
|
jan@42344
|
59 |
|
jan@42344
|
60 |
ML {*
|
jan@42344
|
61 |
(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
|
jan@42344
|
62 |
fun eval_factors_from_solution (thmid:string) _ t thy =
|
jan@42344
|
63 |
(let val prod = factors_from_solution t
|
jan@42344
|
64 |
in SOME (mk_thmid thmid ""
|
jan@42344
|
65 |
(Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
|
jan@42344
|
66 |
Trueprop $ (mk_equality (t, prod)))
|
jan@42344
|
67 |
end)
|
jan@42344
|
68 |
handle _ => NONE;
|
jan@42344
|
69 |
*}
|
jan@42344
|
70 |
|
jan@42344
|
71 |
|
jan@42344
|
72 |
|
jan@42344
|
73 |
|
jan@42295
|
74 |
text {*rule set for partial fractions*}
|
neuper@42289
|
75 |
ML {*
|
neuper@42289
|
76 |
val partial_fraction =
|
neuper@42289
|
77 |
Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI),
|
neuper@42289
|
78 |
erls = Erls, srls = Erls, calc = [],
|
neuper@42289
|
79 |
rules = [
|
jan@42344
|
80 |
Calc ("Rings.inverse_class.divide", eval_get_denominator "#"),
|
jan@42344
|
81 |
Calc ("Rings.inverse_class.divide", eval_get_numerator "#")
|
neuper@42289
|
82 |
],
|
neuper@42289
|
83 |
scr = EmptyScr};
|
neuper@42289
|
84 |
*}
|
jan@42295
|
85 |
text {*store the rule set for math engine*}
|
neuper@42289
|
86 |
ML {*
|
neuper@42289
|
87 |
overwritelthy @{theory} (!ruleset',
|
neuper@42289
|
88 |
[("partial_fraction", prep_rls partial_fraction)
|
neuper@42289
|
89 |
]);
|
neuper@42289
|
90 |
*}
|
neuper@42289
|
91 |
|
jan@42295
|
92 |
|
neuper@42289
|
93 |
end |