130 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $ |
130 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $ |
131 s_2 $ Const ("List.list.Nil", _)) = solutions; |
131 s_2 $ Const ("List.list.Nil", _)) = solutions; |
132 term2str s_1; |
132 term2str s_1; |
133 term2str s_2; |
133 term2str s_2; |
134 *} |
134 *} |
135 ML {* |
135 |
|
136 ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*) |
136 val xx = HOLogic.dest_eq s_1; |
137 val xx = HOLogic.dest_eq s_1; |
137 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
138 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
138 val xx = HOLogic.dest_eq s_2; |
139 val xx = HOLogic.dest_eq s_2; |
139 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
140 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx; |
140 term2str s_1'; |
141 term2str s_1'; |
142 *} |
143 *} |
143 |
144 |
144 subsubsection {*build expression*} |
145 subsubsection {*build expression*} |
145 text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*} |
146 text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*} |
146 ML {* |
147 ML {* |
|
148 (*The Main Denominator is the multiplikation of the partial fraction denominators*) |
147 val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ; |
149 val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ; |
148 val SOME n3 = parseNEW ctxt "3::real"; |
150 val SOME numerator = parseNEW ctxt "3::real"; |
149 val expression' = HOLogic.mk_binop "Rings.inverse_class.divide" (n3, denominator'); |
151 |
|
152 val expression' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator'); |
150 term2str expression'; |
153 term2str expression'; |
151 *} |
154 *} |
152 |
155 |
153 subsubsection {*Ansatz*} |
156 subsubsection {*Ansatz - create partial fractions out of our expression*} |
|
157 |
154 axiomatization where |
158 axiomatization where |
155 ansatz2: "n / (a*b) = A/a + B/(b::real)" and |
159 ansatz2: "n / (a*b) = A/a + B/(b::real)" and |
156 multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))" |
160 multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n / (a*b)) = a*b*(A/a + B/b))" |
157 ML {* |
161 |
|
162 ML {* |
|
163 (*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*) |
158 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expression'; |
164 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expression'; |
159 term2str t1; |
165 term2str t1; |
160 atomty t1; |
166 atomty t1; |
161 val eq1 = HOLogic.mk_eq (expression', t1); |
167 val eq1 = HOLogic.mk_eq (expression', t1); |
162 term2str eq1; |
168 term2str eq1; |
163 *} |
169 *} |
164 ML {* |
170 ML {* |
|
171 (*eliminate the demoninators by multiplying the left and the right side with the main denominator*) |
165 val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1; |
172 val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1; |
166 term2str eq2; |
173 term2str eq2; |
167 *} |
174 *} |
168 ML {* |
175 ML {* |
|
176 (*simplificatoin*) |
169 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2; |
177 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2; |
170 term2str eq3; (*?A ?B not simplified*) |
178 term2str eq3; (*?A ?B not simplified*) |
171 *} |
179 *} |
172 ML {* |
180 ML {* |
173 val SOME fract1 = |
181 val SOME fract1 = |
187 *} |
195 *} |
188 |
196 |
189 subsubsection {*get first koeffizient*} |
197 subsubsection {*get first koeffizient*} |
190 |
198 |
191 ML {* |
199 ML {* |
|
200 (*substitude z with the first zeropoint to get A*) |
192 val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3''; |
201 val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3''; |
193 term2str eq4_1; |
202 term2str eq4_1; |
194 *} |
203 *} |
195 ML {* |
204 ML {* |
196 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1; |
205 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1; |
200 val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"]; |
209 val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"]; |
201 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
210 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
202 |
211 |
203 *} |
212 *} |
204 ML {* |
213 ML {* |
|
214 (*solve the simple linear equilation for A*) |
205 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
215 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
206 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
216 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
207 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
217 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
208 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
218 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
219 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
236 *} |
246 *} |
237 |
247 |
238 subsubsection {*get second koeffizient*} |
248 subsubsection {*get second koeffizient*} |
239 |
249 |
240 ML {* |
250 ML {* |
|
251 (*substitude z with the second zeropoint to get B*) |
241 val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3''; |
252 val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3''; |
242 term2str eq4_1; |
253 term2str eq4_1; |
243 *} |
254 *} |
244 |
255 |
245 ML {* |
256 ML {* |
246 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1; |
257 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1; |
247 term2str eq4b_2; |
258 term2str eq4b_2; |
248 *} |
259 *} |
249 |
260 |
250 ML {* |
261 ML {* |
|
262 (*solve the simple linear equilation for B*) |
|
263 |
251 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"]; |
264 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"]; |
252 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
265 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]); |
253 |
266 |
254 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
267 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
255 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |
268 val (p,_,fb,nxt,_,pt) = me nxt p [] pt; |