125 term2str fun3; (*fails on x^^^(-1) TODO*) |
126 term2str fun3; (*fails on x^^^(-1) TODO*) |
126 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2'; |
127 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2'; |
127 term2str fun3'; (*OK*) |
128 term2str fun3'; (*OK*) |
128 *} |
129 *} |
129 |
130 |
130 subsection {*build equation from given term*} |
131 subsubsection {*get argument of X': z is the variable the equation is solved for*} |
|
132 |
|
133 text{*grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,... |
|
134 |
|
135 grep -r "fun eva_" ... shows all functions witch can be used in a script. |
|
136 lookup this files how to build and handle such functions. |
|
137 |
|
138 the next section shows how to introduce such a function. |
|
139 *} |
|
140 |
|
141 |
|
142 text{*---------------------------begin partial fractions snip--------------------------*} |
|
143 |
|
144 subsubsection {*get the denominator out of a fraction*} |
|
145 |
|
146 text {*get denominator should become a constant for the isabelle parser: *} |
|
147 |
|
148 consts |
|
149 |
|
150 get_denominator :: "real => real" |
|
151 |
|
152 ML {* |
|
153 |
|
154 (*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*) |
|
155 fun eval_get_denominator (thmid:string) _ |
|
156 ( t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $ |
|
157 (Const ("Rings.inverse_class.divide", _) $ num $ |
|
158 denom)) thy = |
|
159 ( writeln "found"; |
|
160 SOME (mk_thmid thmid "" |
|
161 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", |
|
162 Trueprop $ (mk_equality (t, denom))) |
|
163 ) |
|
164 | eval_get_denominator _ _ _ _ = |
|
165 ( writeln "NOT found"; |
|
166 NONE); |
|
167 *} |
|
168 |
|
169 |
|
170 ML {* |
|
171 val t = @{term "get_denominator ((a +x)/b)"}; |
|
172 eval_get_denominator "" 0 t @{theory} |
|
173 *} |
|
174 |
|
175 |
|
176 ML {* |
|
177 val t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $ |
|
178 (Const ("Rings.inverse_class.divide", _) $ num $ |
|
179 denom) = t; |
|
180 *} |
|
181 |
|
182 |
|
183 ML {* |
|
184 (* |
|
185 if term2s t' = "(argument_in M_b x) = x" then () |
|
186 else error "atools.sml:(argument_in M_b x) = x ???"; |
|
187 *) |
|
188 *} |
|
189 |
|
190 |
|
191 |
|
192 |
|
193 subsubsection {*build equation from given term*} |
131 ML {* |
194 ML {* |
132 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr; |
195 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr; |
133 val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr; |
196 val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr; |
134 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2"; |
197 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2"; |
135 *} |
198 *} |
136 text {*we have rhs in the language, but we need a function |
199 text {*we have rhs in the language, but we need a function |
137 which gets the denominator of a fraction*} |
200 which gets the denominator of a fraction*} |
138 ML {* |
201 |
139 (*GOON ===================================================*) |
202 |
140 |
|
141 *} |
|
142 |
|
143 text{*---------------------------begin partial fractions snip--------------------------*} |
|
144 |
|
145 subsection {*get the denominator out of a fraction*} |
|
146 text {*this function can be put into rule sets*} |
|
147 ML {* |
|
148 (*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*) |
|
149 fun eval_get_denominator (thmid:string) _ |
|
150 (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = |
|
151 SOME (mk_thmid thmid "" |
|
152 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", |
|
153 Trueprop $ (mk_equality (t, denom))) |
|
154 | eval_get_denominator _ _ _ _ = NONE; |
|
155 *} |
|
156 text {*rule set for partial fractions*} |
|
157 ML {* |
|
158 val partial_fraction = |
|
159 Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), |
|
160 erls = Erls, srls = Erls, calc = [], |
|
161 rules = [ |
|
162 Calc ("Rings.inverse_class.divide", eval_get_denominator "#") |
|
163 ], |
|
164 scr = EmptyScr}; |
|
165 *} |
|
166 text {*store the rule set for math engine*} |
|
167 ML {* |
|
168 overwritelthy @{theory} (!ruleset', |
|
169 [("partial_fraction", prep_rls partial_fraction) |
|
170 ]); |
|
171 *} |
|
172 text{*---------------------------end partial fractions snip--------------------------*} |
203 text{*---------------------------end partial fractions snip--------------------------*} |
173 |
204 |
174 subsection {*solve equation*} |
205 subsection {*solve equation*} |
175 text {*this type of equation if too general for the present program*} |
206 text {*this type of equation if too general for the present program*} |
176 ML {* |
207 ML {* |
517 val str = |
548 val str = |
518 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
549 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
519 " (let X = Take X_eq;" ^ |
550 " (let X = Take X_eq;" ^ |
520 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
551 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
521 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
552 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
522 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
553 " (X'_z::real) = lhs X';" ^ |
523 " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*) |
554 " (z::real) = argument_in X'_z;" ^ |
524 " equ = (denom = (0::real));" ^ |
555 " (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*) |
525 " fun_arg = Take (lhs X');" ^ |
556 " (denom::real) = get_denominator funterm;" ^ (*get_denominator*) |
526 " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*) |
557 " (equ::bool) = (denom = (0::real));" ^ |
527 " (L_L::bool list) = " ^ |
558 " (L_L::bool list) = " ^ |
528 " (SubProblem (Test', " ^ |
559 " (SubProblem (Test', " ^ |
529 " [linear,univariate,equation,test]," ^ |
560 " [linear,univariate,equation,test]," ^ |
530 " [Test,solve_linear]) " ^ |
561 " [Test,solve_linear]) " ^ |
531 " [BOOL equ, REAL z]) " ^ |
562 " [BOOL equ, REAL z]) " ^ |
570 crls = e_rls, nrls = e_rls}, |
601 crls = e_rls, nrls = e_rls}, |
571 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
602 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) |
572 " (let X = Take X_eq;" ^ |
603 " (let X = Take X_eq;" ^ |
573 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
604 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*) |
574 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
605 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*) |
575 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) |
606 " (X'_z::real) = lhs X';" ^ (**) |
576 " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*) |
607 " (z::real) = argument_in X'_z;" ^ (**) |
577 " equ = (denom = (0::real));" ^ |
608 " (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*) |
578 " fun_arg = Take (lhs X');" ^ (*= get_argument (lhs X')*) |
609 " (denom::real) = get_denominator funterm;" ^ (*get_denominator*) |
579 " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*) |
610 " (equ::bool) = (denom = (0::real));" ^ |
580 " (L_L::bool list) = " ^ |
611 " (L_L::bool list) = " ^ |
581 " (SubProblem (Test', " ^ |
612 " (SubProblem (Test', " ^ |
582 " [linear,univariate,equation,test]," ^ |
613 " [linear,univariate,equation,test]," ^ |
583 " [Test,solve_linear]) " ^ |
614 " [Test,solve_linear]) " ^ |
584 " [BOOL equ, REAL z]) " ^ |
615 " [BOOL equ, REAL z]) " ^ |