1 theory Partial_Fractions imports Rational begin |
|
2 |
|
3 subsection {*get the denominator out of a fraction*} |
|
4 text {*this function can be put into rule sets*} |
|
5 ML {* |
|
6 (*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*) |
|
7 fun eval_get_denominator (thmid:string) _ |
|
8 (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = |
|
9 SOME (mk_thmid thmid "" |
|
10 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", |
|
11 Trueprop $ (mk_equality (t, denom))) |
|
12 | eval_get_denominator _ _ _ _ = NONE; |
|
13 |
|
14 |
|
15 |
|
16 *} |
|
17 |
|
18 |
|
19 |
|
20 subsection {*get the argument out of a fraction*} |
|
21 |
|
22 ML {*(* |
|
23 (*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*) |
|
24 |
|
25 |
|
26 fun eval_get_argument "Atools.argument'_in" |
|
27 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ = |
|
28 if is_Free arg (*could be something to be simplified before*) |
|
29 then SOME (term2str t ^ " = " ^ term2str arg, |
|
30 Trueprop $ (mk_equality (t, arg))) |
|
31 else NONE |
|
32 | eval_get_argument_in _ _ _ _ = NONE; |
|
33 *) |
|
34 *} |
|
35 |
|
36 |
|
37 subsection {*store the function for fetching from script*} |
|
38 |
|
39 ML {* |
|
40 calclist' := overwritel (!calclist', |
|
41 [ |
|
42 ("get_denominator", ("Rational.get'_denominator", eval_get_denominator "")), |
|
43 ("get_argument", ("Rational.get'_argument", eval_get_argument "")) |
|
44 ]); |
|
45 *} |
|
46 |
|
47 subsection{*rule set for partial fractions*} |
|
48 ML {* |
|
49 val partial_fraction = |
|
50 Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), |
|
51 erls = Erls, srls = Erls, calc = [], |
|
52 rules = [ |
|
53 Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X") |
|
54 ], |
|
55 scr = EmptyScr}; |
|
56 *} |
|
57 |
|
58 subsection{*store the rule set for math engine*} |
|
59 ML {* |
|
60 overwritelthy @{theory} (!ruleset', |
|
61 [("partial_fraction", prep_rls partial_fraction) |
|
62 ]); |
|
63 *} |
|
64 |
|
65 end |
|