172 *} |
172 *} |
173 text {* tests of eval_get_denominator see test/Knowledge/rational.sml*} |
173 text {* tests of eval_get_denominator see test/Knowledge/rational.sml*} |
174 |
174 |
175 |
175 |
176 text{*---------------------------end partial fractions snip--------------------------*} |
176 text{*---------------------------end partial fractions snip--------------------------*} |
|
177 |
|
178 subsubsection {*get the numerator out of a fraction*} |
|
179 text {*get dnumerator should also become a constant for the isabelle parser: *} |
|
180 |
|
181 consts |
|
182 get_numerator :: "real => real" |
|
183 |
|
184 ML {* |
|
185 fun eval_get_numerator (thmid:string) _ |
|
186 (t as Const ("Rational.get_numerator", _) $ |
|
187 (Const ("Rings.inverse_class.divide", _) numerator |
|
188 $ num $ )) thy = |
|
189 SOME (mk_thmid thmid "" |
|
190 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", |
|
191 Trueprop $ (mk_equality (t, denom))) |
|
192 | eval_get_numerator _ _ _ _ = NONE; |
|
193 |
|
194 *} |
177 |
195 |
178 subsection {*solve equation*} |
196 subsection {*solve equation*} |
179 text {*this type of equation if too general for the present program*} |
197 text {*this type of equation if too general for the present program*} |
180 ML {* |
198 ML {* |
181 "----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------"; |
199 "----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------"; |
338 subsubsection {*Ansatz - create partial fractions out of our expression*} |
356 subsubsection {*Ansatz - create partial fractions out of our expression*} |
339 ML {*Context.theory_name thy = "Isac"*} |
357 ML {*Context.theory_name thy = "Isac"*} |
340 |
358 |
341 axiomatization where |
359 axiomatization where |
342 ansatz2: "n / (a*b) = A/a + B/(b::real)" and |
360 ansatz2: "n / (a*b) = A/a + B/(b::real)" and |
343 multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))" |
361 multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))" and |
|
362 ansatz3: "n / (a * b * c) = (A/a) + (B/b) + (C/c)" and |
|
363 ansatz4: "n / (a * b * c * d) = (A/a) + (B/b) + (C/c) + (D/d)" |
344 |
364 |
345 ML {* |
365 ML {* |
346 (*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*) |
366 (*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*) |
347 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr'; |
367 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr'; |
348 term2str t1; atomty t1; |
368 term2str t1; atomty t1; |
661 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
681 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
662 " (X'_z::real) = lhs X';" ^ (**) |
682 " (X'_z::real) = lhs X';" ^ (**) |
663 " (zzz::real) = argument_in X'_z;" ^ (**) |
683 " (zzz::real) = argument_in X'_z;" ^ (**) |
664 " (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*) |
684 " (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*) |
665 " (denom::real) = get_denominator funterm;" ^ (*get_denominator*) |
685 " (denom::real) = get_denominator funterm;" ^ (*get_denominator*) |
|
686 " (numer::real) = get_numerator funterm;" ^ |
666 " (equ::bool) = (denom = (0::real));" ^ |
687 " (equ::bool) = (denom = (0::real));" ^ |
667 |
688 |
668 " (L_L::bool list) = (SubProblem (PolyEq'," ^ |
689 " (L_L::bool list) = (SubProblem (PolyEq'," ^ |
669 " [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^ |
690 " [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^ |
670 " [BOOL equ, REAL zzz]) " ^ |
691 " [BOOL equ, REAL zzz]) " ^ |
671 " in X)" |
692 " in X);" ^ |
|
693 |
|
694 " facs = factors_from_solution L_L;" ^ |
|
695 " (eq::real) = Take (funterm = (num / facs));" ^ |
|
696 " (eq::real) = (Try (Rewrite_Set ansatz False)) eq " ^ |
|
697 |
672 )); |
698 )); |
673 *} |
699 *} |
674 |
700 |
675 subsection {*Check the Program*} |
701 subsection {*Check the Program*} |
676 |
702 |