57 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
57 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
58 ["Test", "squ-equ-test-subpbl1"]))]; |
58 ["Test", "squ-equ-test-subpbl1"]))]; |
59 Iterator 1; moveActiveRoot 1; |
59 Iterator 1; moveActiveRoot 1; |
60 autoCalculate 1 CompleteCalcHead; |
60 autoCalculate 1 CompleteCalcHead; |
61 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
61 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
62 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
62 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
63 |
63 |
64 appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1); |
64 appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1); |
65 val ((pt,_),_) = get_calc 1; |
65 val ((pt,_),_) = get_calc 1; |
66 val str = pr_ctree pr_short pt; |
66 val str = pr_ctree pr_short pt; |
67 if str = |
67 if str = |
68 (". ----- pblobj -----\n" ^ |
68 (". ----- pblobj -----\n" ^ |
69 "1. x + 1 = 2\n" ^ |
69 "1. x + 1 = 2\n" ^ |
70 "2. x + 1 + -1 * 2 = 0\n" ^ |
70 "2. x + 1 + - 1 * 2 = 0\n" ^ |
71 "2.1. x + 1 + -1 * 2 = 0\n" ^ |
71 "2.1. x + 1 + - 1 * 2 = 0\n" ^ |
72 "2.2. 1 + x + -1 * 2 = 0\n" ^ |
72 "2.2. 1 + x + - 1 * 2 = 0\n" ^ |
73 "2.3. 1 + (x + -1 * 2) = 0\n" ^ |
73 "2.3. 1 + (x + - 1 * 2) = 0\n" ^ |
74 "2.4. 1 + (x + -2) = 0\n" ^ |
74 "2.4. 1 + (x + - 2) = 0\n" ^ |
75 "2.5. 1 + (x + -2 * 1) = 0\n" ^ |
75 "2.5. 1 + (x + - 2 * 1) = 0\n" ^ |
76 "2.6. 1 + x + -2 * 1 = 0\n" ) then () |
76 "2.6. 1 + x + - 2 * 1 = 0\n" ) then () |
77 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1"; |
77 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1"; |
78 |
78 |
79 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*) |
79 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*) |
80 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*) |
80 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + - 1 * 2 = 0*) |
81 |
81 |
82 (*the seven steps of detailed derivation*) |
82 (*the seven steps of detailed derivation*) |
83 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm); |
83 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm); |
84 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res); |
84 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res); |
85 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res); |
85 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res); |
86 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res); |
86 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res); |
87 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res); |
87 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res); |
88 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res); |
88 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res); |
89 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res); |
89 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res); |
90 val ((pt,_),_) = get_calc 1; |
90 val ((pt,_),_) = get_calc 1; |
91 if "-2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then() |
91 if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then() |
92 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2"; |
92 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2"; |
93 |
93 |
94 fetchProposedTactic 1; (*takes Iterator 1 _1_*) |
94 fetchProposedTactic 1; (*takes Iterator 1 _1_*) |
95 (* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*) |
95 (* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*) |
96 (*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============= |
96 (*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============= |
117 "----------------------------------------------------------"; |
117 "----------------------------------------------------------"; |
118 |
118 |
119 val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
119 val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
120 ((#rules o Rule_Set.rep) Test_simplify) |
120 ((#rules o Rule_Set.rep) Test_simplify) |
121 (sqrt_right false (@{theory "Pure"})) NONE |
121 (sqrt_right false (@{theory "Pure"})) NONE |
122 (TermC.str2term "x + 1 + -1 * 2 = 0"); |
122 (TermC.str2term "x + 1 + - 1 * 2 = 0"); |
123 (writeln o Derive.trtas2str) fod; |
123 (writeln o Derive.trtas2str) fod; |
124 |
124 |
125 val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
125 val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls |
126 ((#rules o Rule_Set.rep) Test_simplify) |
126 ((#rules o Rule_Set.rep) Test_simplify) |
127 (sqrt_right false (@{theory "Pure"})) NONE |
127 (sqrt_right false (@{theory "Pure"})) NONE |
128 (TermC.str2term "-2 * 1 + (1 + x) = 0"); |
128 (TermC.str2term "- 2 * 1 + (1 + x) = 0"); |
129 (writeln o Derive.trtas2str) ifod; |
129 (writeln o Derive.trtas2str) ifod; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
131 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
131 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
132 val der = fod' @ (map Derive.rev_deriv' rifod'); |
132 val der = fod' @ (map Derive.rev_deriv' rifod'); |
133 (writeln o Derive.trtas2str) der; |
133 (writeln o Derive.trtas2str) der; |
142 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
142 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
143 ["Test", "squ-equ-test-subpbl1"]))]; |
143 ["Test", "squ-equ-test-subpbl1"]))]; |
144 Iterator 1; moveActiveRoot 1; |
144 Iterator 1; moveActiveRoot 1; |
145 autoCalculate 1 CompleteCalcHead; |
145 autoCalculate 1 CompleteCalcHead; |
146 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
146 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
147 appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1); |
147 appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1); |
148 |
148 |
149 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
149 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
150 |
150 |
151 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
151 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
152 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); |
152 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); |
154 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); |
154 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); |
155 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); |
155 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); |
156 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); |
156 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); |
157 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); |
157 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); |
158 val ((pt,_),_) = get_calc 1; |
158 val ((pt,_),_) = get_calc 1; |
159 if "2 + -1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then() |
159 if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then() |
160 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1"; |
160 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1"; |
161 |
161 |
162 fetchProposedTactic 1; (*takes Iterator 1 _1_*) |
162 fetchProposedTactic 1; (*takes Iterator 1 _1_*) |
163 val (_,(tac,_,_)::_) = get_calc 1; |
163 val (_,(tac,_,_)::_) = get_calc 1; |
164 case tac of Rewrite_Set "norm_equation" => () |
164 case tac of Rewrite_Set "norm_equation" => () |
177 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
177 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
178 ["Test", "squ-equ-test-subpbl1"]))]; |
178 ["Test", "squ-equ-test-subpbl1"]))]; |
179 Iterator 1; moveActiveRoot 1; |
179 Iterator 1; moveActiveRoot 1; |
180 autoCalculate 1 CompleteCalcHead; |
180 autoCalculate 1 CompleteCalcHead; |
181 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
181 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
182 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
182 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
183 |
183 |
184 appendFormula 1 "x = 2" (*|> Future.join*); |
184 appendFormula 1 "x = 2" (*|> Future.join*); |
185 val ((pt,p),_) = get_calc 1; |
185 val ((pt,p),_) = get_calc 1; |
186 val str = pr_ctree pr_short pt; |
186 val str = pr_ctree pr_short pt; |
187 writeln str; |
187 writeln str; |
210 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
210 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
211 ["Test", "squ-equ-test-subpbl1"]))]; |
211 ["Test", "squ-equ-test-subpbl1"]))]; |
212 Iterator 1; moveActiveRoot 1; |
212 Iterator 1; moveActiveRoot 1; |
213 autoCalculate 1 CompleteCalcHead; |
213 autoCalculate 1 CompleteCalcHead; |
214 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
214 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
215 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
215 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
216 |
216 |
217 appendFormula 1 "x = 1" (*|> Future.join*); |
217 appendFormula 1 "x = 1" (*|> Future.join*); |
218 val ((pt,p),_) = get_calc 1; |
218 val ((pt,p),_) = get_calc 1; |
219 val str = pr_ctree pr_short pt; |
219 val str = pr_ctree pr_short pt; |
220 writeln str; |
220 writeln str; |
221 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res) |
221 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res) |
222 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*) |
222 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*) |
223 else error "inform.sml: diff.behav.appendFormula: Res + late d 1"; |
223 else error "inform.sml: diff.behav.appendFormula: Res + late d 1"; |
224 |
224 |
225 fetchProposedTactic 1; |
225 fetchProposedTactic 1; |
226 val (_,(tac,_,_)::_) = get_calc 1; |
226 val (_,(tac,_,_)::_) = get_calc 1; |
230 val ((pt,_),_) = get_calc 1; |
230 val ((pt,_),_) = get_calc 1; |
231 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () |
231 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () |
232 else error "inform.sml: diff.behav.appendFormula: Res + late d 3"; |
232 else error "inform.sml: diff.behav.appendFormula: Res + late d 3"; |
233 DEconstrCalcTree 1; |
233 DEconstrCalcTree 1; |
234 |
234 |
235 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; |
235 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; |
236 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; |
236 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; |
237 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; |
237 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; |
238 reset_states (); |
238 reset_states (); |
239 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
239 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
240 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
240 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
241 ["Test", "squ-equ-test-subpbl1"]))]; |
241 ["Test", "squ-equ-test-subpbl1"]))]; |
242 Iterator 1; moveActiveRoot 1; |
242 Iterator 1; moveActiveRoot 1; |
243 autoCalculate 1 CompleteCalcHead; |
243 autoCalculate 1 CompleteCalcHead; |
244 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
244 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
245 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
245 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
246 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*); |
246 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*); |
247 val ((pt,p),_) = get_calc 1; |
247 val ((pt,p),_) = get_calc 1; |
248 val str = pr_ctree pr_short pt; |
248 val str = pr_ctree pr_short pt; |
249 writeln str; |
249 writeln str; |
250 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then () |
250 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then () |
251 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1"; |
251 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1"; |
252 autoCalculate 1 CompleteCalc; |
252 autoCalculate 1 CompleteCalc; |
253 val ((pt,p),_) = get_calc 1; |
253 val ((pt,p),_) = get_calc 1; |
254 if "[x = 3 + -2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () |
254 if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () |
255 (* ~~~~~~~~~~ simplify as last step in any script ?!*) |
255 (* ~~~~~~~~~~ simplify as last step in any script ?!*) |
256 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2"; |
256 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2"; |
257 DEconstrCalcTree 1; |
257 DEconstrCalcTree 1; |
258 |
258 |
259 "--------- replaceFormula: on Res + = ----------------------------"; |
259 "--------- replaceFormula: on Res + = ----------------------------"; |
264 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
264 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
265 ["Test", "squ-equ-test-subpbl1"]))]; |
265 ["Test", "squ-equ-test-subpbl1"]))]; |
266 Iterator 1; moveActiveRoot 1; |
266 Iterator 1; moveActiveRoot 1; |
267 autoCalculate 1 CompleteCalcHead; |
267 autoCalculate 1 CompleteCalcHead; |
268 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
268 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
269 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
269 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
270 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*-1 + x*); |
270 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*- 1 + x*); |
271 |
271 |
272 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); |
272 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); |
273 val ((pt,_),_) = get_calc 1; |
273 val ((pt,_),_) = get_calc 1; |
274 val str = pr_ctree pr_short pt; |
274 val str = pr_ctree pr_short pt; |
275 |
275 |
276 (* before AK110725 this was |
276 (* before AK110725 this was |
277 ". ----- pblobj -----\n |
277 ". ----- pblobj -----\n |
278 1. x + 1 = 2\n |
278 1. x + 1 = 2\n |
279 2. x + 1 + -1 * 2 = 0\n |
279 2. x + 1 + - 1 * 2 = 0\n |
280 2.1. x + 1 + -1 * 2 = 0\n |
280 2.1. x + 1 + - 1 * 2 = 0\n |
281 2.2. 1 + x + -1 * 2 = 0\n |
281 2.2. 1 + x + - 1 * 2 = 0\n |
282 2.3. 1 + (x + -1 * 2) = 0\n |
282 2.3. 1 + (x + - 1 * 2) = 0\n |
283 2.4. 1 + (x + -2) = 0\n |
283 2.4. 1 + (x + -2) = 0\n |
284 2.5. 1 + (x + -2 * 1) = 0\n |
284 2.5. 1 + (x + -2 * 1) = 0\n |
285 2.6. 1 + x + -2 * 1 = 0\n"; |
285 2.6. 1 + x + -2 * 1 = 0\n"; |
286 *) |
286 *) |
287 if str = |
287 if str = |
288 ". ----- pblobj -----\n"^ |
288 ". ----- pblobj -----\n"^ |
289 "1. x + 1 = 2\n"^ |
289 "1. x + 1 = 2\n"^ |
290 "2. x + 1 + -1 * 2 = 0\n"^ |
290 "2. x + 1 + - 1 * 2 = 0\n"^ |
291 "2.1. x + 1 + -1 * 2 = 0\n"^ |
291 "2.1. x + 1 + - 1 * 2 = 0\n"^ |
292 "2.2. 1 + x + -1 * 2 = 0\n"^ |
292 "2.2. 1 + x + - 1 * 2 = 0\n"^ |
293 "2.3. 1 + (x + -1 * 2) = 0\n"^ |
293 "2.3. 1 + (x + - 1 * 2) = 0\n"^ |
294 "2.4. 1 + (x + -2) = 0\n"^ |
294 "2.4. 1 + (x + - 2) = 0\n"^ |
295 "2.5. 1 + (x + -2 * 1) = 0\n"^ |
295 "2.5. 1 + (x + - 2 * 1) = 0\n"^ |
296 "2.6. 1 + x + -2 * 1 = 0\n" then() |
296 "2.6. 1 + x + - 2 * 1 = 0\n" then() |
297 else error "inform.sml: diff.behav.replaceFormula: on Res += 1"; |
297 else error "inform.sml: diff.behav.replaceFormula: on Res += 1"; |
298 |
298 |
299 autoCalculate 1 CompleteCalc; |
299 autoCalculate 1 CompleteCalc; |
300 val ((pt,pos as (p,_)),_) = get_calc 1; |
300 val ((pt,pos as (p,_)),_) = get_calc 1; |
301 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then() |
301 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then() |
310 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
310 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
311 ["Test", "squ-equ-test-subpbl1"]))]; |
311 ["Test", "squ-equ-test-subpbl1"]))]; |
312 Iterator 1; moveActiveRoot 1; |
312 Iterator 1; moveActiveRoot 1; |
313 autoCalculate 1 CompleteCalcHead; |
313 autoCalculate 1 CompleteCalcHead; |
314 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
314 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
315 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
315 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
316 |
316 |
317 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); |
317 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); |
318 val ((pt,_),_) = get_calc 1; |
318 val ((pt,_),_) = get_calc 1; |
319 val str = pr_ctree pr_short pt; |
319 val str = pr_ctree pr_short pt; |
320 writeln str; |
320 writeln str; |
321 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then () |
321 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then () |
322 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; |
322 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; |
323 autoCalculate 1 CompleteCalc; |
323 autoCalculate 1 CompleteCalc; |
324 val ((pt,pos as (p,_)),_) = get_calc 1; |
324 val ((pt,pos as (p,_)),_) = get_calc 1; |
325 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() |
325 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() |
326 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
326 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
339 |
339 |
340 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); |
340 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); |
341 val ((pt,_),_) = get_calc 1; |
341 val ((pt,_),_) = get_calc 1; |
342 val str = pr_ctree pr_short pt; |
342 val str = pr_ctree pr_short pt; |
343 writeln str; |
343 writeln str; |
344 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then () |
344 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then () |
345 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1"; |
345 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1"; |
346 autoCalculate 1 CompleteCalc; |
346 autoCalculate 1 CompleteCalc; |
347 val ((pt,pos as (p,_)),_) = get_calc 1; |
347 val ((pt,pos as (p,_)),_) = get_calc 1; |
348 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() |
348 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() |
349 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2"; |
349 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2"; |
454 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
454 ("Test", ["sqroot-test", "univariate", "equation", "test"], |
455 ["Test", "squ-equ-test-subpbl1"]))]; |
455 ["Test", "squ-equ-test-subpbl1"]))]; |
456 Iterator 1; moveActiveRoot 1; |
456 Iterator 1; moveActiveRoot 1; |
457 autoCalculate 1 CompleteCalcHead; |
457 autoCalculate 1 CompleteCalcHead; |
458 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
458 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*) |
459 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); |
459 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); |
460 |
460 |
461 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*) |
461 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*) |
462 val ((pt,_),_) = get_calc 1; |
462 val ((pt,_),_) = get_calc 1; |
463 val str = pr_ctree pr_short pt; |
463 val str = pr_ctree pr_short pt; |
464 writeln str; |
464 writeln str; |
510 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"], |
510 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"], |
511 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))]; |
511 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))]; |
512 Iterator 1; moveActiveRoot 1; |
512 Iterator 1; moveActiveRoot 1; |
513 autoCalculate 1 CompleteCalcHead; |
513 autoCalculate 1 CompleteCalcHead; |
514 |
514 |
515 "--- (-1) give a preview on the calculation without any input"; |
515 "--- (- 1) give a preview on the calculation without any input"; |
516 (* |
516 (* |
517 autoCalculate 1 CompleteCalc; |
517 autoCalculate 1 CompleteCalc; |
518 val ((pt, p), _) = get_calc 1; |
518 val ((pt, p), _) = get_calc 1; |
519 Test_Tool.show_pt pt; |
519 Test_Tool.show_pt pt; |
520 [ |
520 [ |
1275 "--------- fun concat_deriv --------------------------------------"; |
1275 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |
1277 "--------- fun concat_deriv --------------------------------------"; |
1277 "--------- fun concat_deriv --------------------------------------"; |
1278 (* |
1278 (* |
1279 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1279 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1280 (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ -1*2=0", TermC.str2term "-2*1+(x+1)=0"); |
1280 (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ - 1*2=0", TermC.str2term "-2*1+(x+1)=0"); |
1281 (tracing o Derive.trtas2str) fod'; |
1281 (tracing o Derive.trtas2str) fod'; |
1282 > [" |
1282 > [" |
1283 (x + 1 + -1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))", " |
1283 (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", " |
1284 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))", " |
1284 (- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", " |
1285 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))", " |
1285 (- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", " |
1286 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] |
1286 (1 + (- 1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "- 1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] |
1287 val it = () : unit |
1287 val it = () : unit |
1288 (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod'); |
1288 (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod'); |
1289 > [" |
1289 > [" |
1290 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))", "-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))", " |
1290 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))", "-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))", " |
1291 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))", " |
1291 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))", " |
1325 ------------------------------------------------------------------------------ |
1325 ------------------------------------------------------------------------------ |
1326 "Schalk I s.87 Bsp 55b (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)"; |
1326 "Schalk I s.87 Bsp 55b (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)"; |
1327 ------------------------------------------------------------------------------ |
1327 ------------------------------------------------------------------------------ |
1328 1. "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x" |
1328 1. "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x" |
1329 ... |
1329 ... |
1330 4. "(3 + (-1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))" |
1330 4. "(3 + (- 1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))" |
1331 Subproblem["normalise", "polynomial", "univariate".. |
1331 Subproblem["normalise", "polynomial", "univariate".. |
1332 ... |
1332 ... |
1333 4.4. "-6 * x + 5 * x \<up> 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. |
1333 4.4. "-6 * x + 5 * x \<up> 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. |
1334 ... |
1334 ... |
1335 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" |
1335 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" |