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@42353
|
12 |
ML {*Context.theory_name thy = "Isac"*}
|
jan@42353
|
13 |
|
jan@42353
|
14 |
ML{*
|
jan@42353
|
15 |
val thy = @{theory};
|
jan@42353
|
16 |
|
jan@42353
|
17 |
signature PARTFRAC =
|
jan@42353
|
18 |
sig
|
jan@42353
|
19 |
val ansatz_rls : rls
|
jan@42353
|
20 |
val ansatz_rls_ : theory -> term -> (term * term list) option
|
jan@42353
|
21 |
end
|
jan@42353
|
22 |
*}
|
jan@42353
|
23 |
|
jan@42344
|
24 |
consts
|
jan@42344
|
25 |
|
jan@42345
|
26 |
factors_from_solution :: "bool list => real"
|
jan@42344
|
27 |
|
neuper@42289
|
28 |
subsection {*get the denominator out of a fraction*}
|
jan@42344
|
29 |
text {*this functions have been stored in Rationals.thy and can be put into rule sets*}
|
jan@42344
|
30 |
|
jan@42345
|
31 |
ML {*
|
jan@42345
|
32 |
(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
|
jan@42345
|
33 |
fun eval_get_denominator (thmid:string) _
|
jan@42345
|
34 |
(t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy =
|
jan@42345
|
35 |
SOME (mk_thmid thmid ""
|
jan@42345
|
36 |
(Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
|
jan@42345
|
37 |
Trueprop $ (mk_equality (t, denom)))
|
jan@42345
|
38 |
| eval_get_denominator _ _ _ _ = NONE;
|
jan@42345
|
39 |
*}
|
jan@42345
|
40 |
|
jan@42345
|
41 |
|
jan@42344
|
42 |
subsubsection {*get solutions out of list*}
|
jan@42344
|
43 |
|
jan@42344
|
44 |
|
neuper@42289
|
45 |
ML {*
|
jan@42344
|
46 |
fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
|
jan@42344
|
47 |
fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
|
jan@42344
|
48 |
let val minus_1 = t |> type_of |> mk_minus_1
|
jan@42344
|
49 |
in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
|
jan@42344
|
50 |
fun fac_from_sol s =
|
jan@42344
|
51 |
let val (lhs, rhs) = HOLogic.dest_eq s
|
jan@42344
|
52 |
in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
|
neuper@42289
|
53 |
*}
|
jan@42344
|
54 |
|
jan@42344
|
55 |
ML {*
|
jan@42344
|
56 |
e_term
|
jan@42344
|
57 |
*}
|
jan@42344
|
58 |
|
jan@42344
|
59 |
ML {*
|
jan@42344
|
60 |
fun mk_prod prod [] =
|
jan@42344
|
61 |
if prod = e_term then error "mk_prod called with []" else prod
|
jan@42344
|
62 |
| mk_prod prod (t :: []) =
|
jan@42344
|
63 |
if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
|
jan@42344
|
64 |
| mk_prod prod (t1 :: t2 :: ts) =
|
jan@42344
|
65 |
if prod = e_term
|
jan@42344
|
66 |
then
|
jan@42344
|
67 |
let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
|
jan@42344
|
68 |
in mk_prod p ts end
|
jan@42344
|
69 |
else
|
jan@42344
|
70 |
let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
|
jan@42344
|
71 |
in mk_prod p (t2 :: ts) end
|
jan@42344
|
72 |
*}
|
jan@42344
|
73 |
|
jan@42344
|
74 |
ML {*
|
jan@42344
|
75 |
|
jan@42344
|
76 |
|
jan@42344
|
77 |
fun factors_from_solution sol =
|
jan@42344
|
78 |
let val ts = HOLogic.dest_list sol
|
jan@42344
|
79 |
in mk_prod e_term (map fac_from_sol ts) end;
|
jan@42344
|
80 |
|
jan@42344
|
81 |
*}
|
jan@42344
|
82 |
|
jan@42344
|
83 |
ML {*
|
jan@42352
|
84 |
(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
|
jan@42352
|
85 |
fun eval_factors_from_solution (thmid:string) _
|
jan@42352
|
86 |
(t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
|
jan@42352
|
87 |
((let val prod = factors_from_solution sol
|
jan@42352
|
88 |
in SOME (mk_thmid thmid ""
|
jan@42352
|
89 |
(Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
|
jan@42352
|
90 |
Trueprop $ (mk_equality (t, prod)))
|
jan@42352
|
91 |
end)
|
jan@42352
|
92 |
handle _ => NONE)
|
jan@42352
|
93 |
| eval_factors_from_solution _ _ _ _ = NONE;
|
jan@42344
|
94 |
*}
|
jan@42344
|
95 |
|
jan@42353
|
96 |
axiomatization where
|
jan@42354
|
97 |
ansatz_2nd_order: "n / (a*b) = A/a + B/(b::real)" and
|
jan@42354
|
98 |
equival_trans_2nd_order: "( n/(a*b) = A/a + B/(b::real) ) = ( n = A*b + B*(a::real) )"
|
jan@42353
|
99 |
|
jan@42353
|
100 |
|
jan@42353
|
101 |
ML {*
|
jan@42353
|
102 |
val ansatz_rls = prep_rls(
|
jan@42353
|
103 |
Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
jan@42353
|
104 |
erls = Erls, srls = Erls, calc = [],
|
jan@42353
|
105 |
rules =
|
jan@42354
|
106 |
[Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order})
|
jan@42353
|
107 |
],
|
jan@42353
|
108 |
scr = EmptyScr}:rls);
|
jan@42353
|
109 |
*}
|
jan@42353
|
110 |
|
jan@42353
|
111 |
ML {*
|
jan@42354
|
112 |
val equival_trans = prep_rls(
|
jan@42354
|
113 |
Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
jan@42354
|
114 |
erls = Erls, srls = Erls, calc = [],
|
jan@42354
|
115 |
rules =
|
jan@42354
|
116 |
[Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
|
jan@42354
|
117 |
],
|
jan@42354
|
118 |
scr = EmptyScr}:rls);
|
jan@42354
|
119 |
*}
|
jan@42354
|
120 |
|
jan@42354
|
121 |
|
jan@42354
|
122 |
text {*store the rule set for math engine*}
|
jan@42354
|
123 |
|
jan@42354
|
124 |
ML {*
|
jan@42353
|
125 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
jan@42354
|
126 |
[("ansatz_rls", ansatz_rls),
|
jan@42354
|
127 |
("equival_trans", equival_trans)
|
jan@42353
|
128 |
]);
|
jan@42353
|
129 |
*}
|
jan@42344
|
130 |
|
jan@42344
|
131 |
|
jan@42344
|
132 |
|
jan@42295
|
133 |
text {*rule set for partial fractions*}
|
neuper@42289
|
134 |
ML {*
|
neuper@42289
|
135 |
val partial_fraction =
|
neuper@42289
|
136 |
Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI),
|
neuper@42289
|
137 |
erls = Erls, srls = Erls, calc = [],
|
neuper@42289
|
138 |
rules = [
|
jan@42345
|
139 |
Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
|
neuper@42289
|
140 |
],
|
neuper@42289
|
141 |
scr = EmptyScr};
|
neuper@42289
|
142 |
*}
|
jan@42354
|
143 |
|
jan@42353
|
144 |
|
neuper@42289
|
145 |
|
jan@42295
|
146 |
|
neuper@42289
|
147 |
end |