72 \ [BOOL e_1, REAL v_1]);\ |
72 \ [BOOL e_1, REAL v_1]);\ |
73 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
73 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
74 \ [BOOL e_2, REAL v_2])\ |
74 \ [BOOL e_2, REAL v_2])\ |
75 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
75 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
76 |
76 |
77 val ags = map (term_of o the o (parse DiffApp.thy)) |
77 val ags = map (Thm.term_of o the o (parse DiffApp.thy)) |
78 ["A::real", "alpha::real", |
78 ["A::real", "alpha::real", |
79 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; |
79 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; |
80 val ll = [](*:loc_*); |
80 val ll = [](*:loc_*); |
81 (* problem with exn PTREE + eval_to ------------------------- |
81 (* problem with exn PTREE + eval_to ------------------------- |
82 "-------------- subproblem with empty formalizaton -------"; |
82 "-------------- subproblem with empty formalizaton -------"; |
154 |
154 |
155 |
155 |
156 (*#####################################################--------11.5.02 |
156 (*#####################################################--------11.5.02 |
157 "################ Solve_root_equation #################"; |
157 "################ Solve_root_equation #################"; |
158 (*#####################################################*) |
158 (*#####################################################*) |
159 val sc = (term_of o the o (parse Test.thy)) |
159 val sc = (Thm.term_of o the o (parse Test.thy)) |
160 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ |
160 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ |
161 \ (let e_e = Rewrite square_equation_left True eq_; \ |
161 \ (let e_e = Rewrite square_equation_left True eq_; \ |
162 \ e_e = Rewrite_Set Test_simplify False e_; \ |
162 \ e_e = Rewrite_Set Test_simplify False e_; \ |
163 \ e_e = Rewrite_Set rearrange_assoc False e_; \ |
163 \ e_e = Rewrite_Set rearrange_assoc False e_; \ |
164 \ e_e = Rewrite_Set isolate_root False e_; \ |
164 \ e_e = Rewrite_Set isolate_root False e_; \ |
170 \ e_e = Rewrite_Set norm_equation False e_; \ |
170 \ e_e = Rewrite_Set norm_equation False e_; \ |
171 \ e_e = Rewrite_Set Test_simplify False e_; \ |
171 \ e_e = Rewrite_Set Test_simplify False e_; \ |
172 \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ |
172 \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ |
173 \ e_e = Rewrite_Set Test_simplify False e_e \ |
173 \ e_e = Rewrite_Set Test_simplify False e_e \ |
174 \ in [e_::bool])"; |
174 \ in [e_::bool])"; |
175 val ags = map (term_of o the o (parse Test.thy)) |
175 val ags = map (Thm.term_of o the o (parse Test.thy)) |
176 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; |
176 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; |
177 val fmz = |
177 val fmz = |
178 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
178 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
179 "solveFor x","errorBound (eps = #0)","solutions v_i_"]; |
179 "solveFor x","errorBound (eps = #0)","solutions v_i_"]; |
180 ----------------------------------------------------------------11.5.02...*) |
180 ----------------------------------------------------------------11.5.02...*) |
246 |
246 |
247 " --- test100: nxt_tac order------------------------------------ "; |
247 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
249 |
249 |
250 val scr as (Prog sc) = Prog (((inst_abs Test.thy) |
250 val scr as (Prog sc) = Prog (((inst_abs Test.thy) |
251 o term_of o the o (parse thy)) |
251 o Thm.term_of o the o (parse thy)) |
252 "Script Testeq (e_e::bool) = \ |
252 "Script Testeq (e_e::bool) = \ |
253 \(While (contains_root e_e) Do \ |
253 \(While (contains_root e_e) Do \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
256 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
256 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
264 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
264 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
265 val (p,_,_,_,_,pt) = me nxt p c pt; |
265 val (p,_,_,_,_,pt) = me nxt p c pt; |
266 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) |
266 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) |
267 val (p,_,_,_,_,pt) = me nxt p c pt; |
267 val (p,_,_,_,_,pt) = me nxt p c pt; |
268 val p = ([1],Res):pos'; |
268 val p = ([1],Res):pos'; |
269 val eq_ = (term_of o the o (parse thy))"e_::bool"; |
269 val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; |
270 |
270 |
271 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
271 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
272 val ve0_= (term_of o the o (parse thy)) ct; |
272 val ve0_= (Thm.term_of o the o (parse thy)) ct; |
273 val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
273 val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
274 e_term,e_term,Safe)), |
274 e_term,e_term,Safe)), |
275 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
275 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
276 val l0 = []; |
276 val l0 = []; |
277 " --------------- 1. ---------------------------------------------"; |
277 " --------------- 1. ---------------------------------------------"; |
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
281 *) |
281 *) |
282 |
282 |
283 |
283 |
284 val scr as (Prog sc) = |
284 val scr as (Prog sc) = |
285 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
285 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
286 "Script Testterm (g_::real) = (Calculate cancel g_)"); |
286 "Script Testterm (g_::real) = (Calculate cancel g_)"); |
287 (* |
287 (* |
288 val scr as (Prog sc) = |
288 val scr as (Prog sc) = |
289 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
289 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
290 "Script Testterm (g_::real) = (Calculate power g_)"); |
290 "Script Testterm (g_::real) = (Calculate power g_)"); |
291 val scr as (Prog sc) = |
291 val scr as (Prog sc) = |
292 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
292 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
293 "Script Testterm (g_::real) = (Calculate pow g_)"); |
293 "Script Testterm (g_::real) = (Calculate pow g_)"); |
294 ..............................................................*) |
294 ..............................................................*) |
295 writeln |
295 writeln |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |