neuper@37906: (* tests for ME/script.sml neuper@37906: WN.13.3.00 neuper@37906: neuper@37906: WN050908 OLD FILE, MERGE WITH smltest/ME/script.sml neuper@37906: neuper@37906: use"systest/script.sml"; neuper@37906: use"script.sml"; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: " scripts: Variante 'funktional' "; neuper@37906: "############## Make_fun_by_new_variable ##############"; neuper@37906: "############## Make_fun_by_explicit ##############"; neuper@37906: "################ Solve_root_equation #################"; neuper@37906: "------- Notlocatable: Free_Solve -------"; neuper@37906: neuper@37906: " --- test100: nxt_tac order------------------------------------ "; neuper@37906: " --- test100: order 1 3 1 2 ----------------------------------- "; neuper@37906: " --- test200: nxt_tac order ------------------------------------- "; neuper@37906: " --- test200: order 3 1 1 2 --------------------------------- "; neuper@37906: neuper@37906: " --- root-equation: nxt_tac order------------------------------ "; neuper@37906: " --- root-equation: 1.norm_equation ------------------------------ "; neuper@37906: (* --- test200: calculate -----------------------------------------*) neuper@37906: " --- check_elementwise ------------------------------ "; neuper@37906: neuper@37906: " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; neuper@37906: " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; neuper@37906: neuper@37906: "--------- sel_rules ---------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: " ################################################# 6.5.03"; neuper@37906: " scripts: Variante 'funktional' 6.5.03"; neuper@37906: " ################################################# 6.5.03 "; neuper@37906: neuper@37906: val c = (the o (parse DiffApp.thy)) neuper@37906: "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ neuper@37906: \ (v_::real) (itv_::real set) (err_::bool) = \ neuper@37981: \ (let e_e = (hd o (filterVar m_)) rs_; \ neuper@37906: \ t_ = (if 1 < length_ rs_ \ neuper@37906: \ then (SubProblem (Reals_,[make,function],[no_met])\ neuper@37981: \ [real_ m_, real_ v_v, bool_list_ rs_])\ neuper@37906: \ else (hd rs_)); \ neuper@37906: \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \ neuper@37906: \ [Isac,maximum_on_interval])\ neuper@37981: \ [bool_ t_, real_ v_v, real_set_ itv_]\ neuper@37906: \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \ neuper@37981: \ [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_, \ neuper@37981: \ bool_list_ (dropWhile (ident e_e) rs_)])::bool list))"; neuper@37906: neuper@37906: neuper@37906: "################################################### 6.5.03"; neuper@37906: "############## Make_fun_by_new_variable ########### 6.5.03"; neuper@37906: "################################################### 6.5.03"; neuper@37906: neuper@37906: val sc = (the o (parse DiffApp.thy)) (*start interpretieren*) neuper@37906: "Script Make_fun_by_new_variable (f_::real) (v_::real) \ neuper@37906: \ (eqs_::bool list) = \ neuper@37906: \(let h_ = (hd o (filterVar f_)) eqs_; \ neuper@37906: \ es_ = dropWhile (ident h_) eqs_; \ neuper@37906: \ vs_ = dropWhile (ident f_) (Vars h_); \ neuper@37906: \ v_1 = nth_ 1 vs_; \ neuper@37906: \ v_2 = nth_ 2 vs_; \ neuper@37906: \ e_1 = (hd o (filterVar v_1)) es_; \ neuper@37906: \ e_2 = (hd o (filterVar v_2)) es_; \ neuper@37906: \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ neuper@37906: \ [bool_ e_1, real_ v_1]);\ neuper@37906: \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ neuper@37906: \ [bool_ e_2, real_ v_2])\ neuper@37906: \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; neuper@37906: neuper@37906: val ags = map (term_of o the o (parse DiffApp.thy)) neuper@37906: ["A::real", "alpha::real", neuper@37906: "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; neuper@37906: val ll = [](*:loc_*); neuper@37906: (* problem with exn PTREE + eval_to ------------------------- neuper@37906: "-------------- subproblem with empty formalizaton -------"; neuper@37906: val (mI1,m1) = neuper@37906: ("Subproblem", tac2tac_ pt p neuper@37906: (Subproblem (("Reals",["univar","equation","test"], neuper@37906: (""(*"ANDERN !!!!!!!*),"no_met")),[]))); neuper@37906: val (mI2,m2) = (mI1,m1); neuper@37906: val (mI3,m3) = neuper@37906: ("Substitute", tac2tac_ pt p neuper@37906: (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); neuper@37906: "------- same_tacpbl + eval_to -------"; neuper@37926: val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); neuper@37906: loc_2str l1; neuper@37906: (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) neuper@37934: Syntax.string_of_term (thy2ctxt' "DiffApp") t1; neuper@37906: (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) neuper@37906: neuper@37926: val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2); neuper@37906: loc_2str l2; neuper@37906: (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) neuper@37934: Syntax.string_of_term (thy2ctxt' "DiffApp") t2; neuper@37906: (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) neuper@37906: neuper@37926: val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3); neuper@37906: loc_2str l3; neuper@37906: (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) neuper@37934: Syntax.string_of_term (thy2ctxt' "DiffApp") t3; neuper@37906: (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) neuper@37906: neuper@37906: neuper@37906: "------- eq_tacIDs + eq_consts + eval_args -------"; neuper@37906: val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; neuper@37906: val eq_cons = filter (eq_consts m) eq_ids; neuper@37906: val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; neuper@37906: "------- locate -------"; neuper@37906: neuper@37906: neuper@37906: "-------------- subproblem with formalizaton -------"; neuper@37906: val (mI,m) = neuper@37906: ("Subproblem", tac2tac_ pt [] neuper@37906: (Subproblem (("Reals",["univar","equation","test"], neuper@37906: (""(*"ANDERN !!!!!!!*),"no_met")), neuper@37906: ["a//#2=r*sin alpha","a"]))); neuper@37906: "------- same_tacpbl + eval_to -------"; neuper@37906: neuper@37906: neuper@37906: "------- eq_tacIDs + eq_consts + eval_args -------"; neuper@37906: val eq_ids = eq_tacIDs [] sc (mI,m) []; neuper@37906: val eq_cons = filter (eq_consts m) eq_ids; neuper@37906: val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; neuper@37906: neuper@37906: neuper@37906: "------- locate -------"; neuper@37906: -------------------------------------------------------*) neuper@37906: (* use"ME/script.sml"; neuper@37906: use"test-script.sml"; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: "############## Make_fun_by_explicit ############## 6.5.03"; neuper@37906: "############## Make_fun_by_explicit ############## 6.5.03"; neuper@37906: "############## Make_fun_by_explicit ############## 6.5.03"; neuper@37906: val c = (the o (parse DiffApp.thy)) neuper@37906: "Script Make_fun_by_explicit (f_::real) (v_::real) \ neuper@37906: \ (eqs_::bool list) = \ neuper@37906: \ (let h_ = (hd o (filterVar f_)) eqs_; \ neuper@37906: \ e_1 = hd (dropWhile (ident h_) eqs_); \ neuper@37906: \ vs_ = dropWhile (ident f_) (Vars h_); \ neuper@37981: \ v_1 = hd (dropWhile (ident v_v) vs_); \ neuper@37906: \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\ neuper@37906: \ [bool_ e_1, real_ v_1])\ neuper@37906: \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; neuper@37906: neuper@37906: neuper@37906: (*#####################################################--------11.5.02 neuper@37906: "################ Solve_root_equation #################"; neuper@37906: (*#####################################################*) neuper@37906: val sc = (term_of o the o (parse Test.thy)) neuper@37906: "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ neuper@37981: \ (let e_e = Rewrite square_equation_left True eq_; \ neuper@37981: \ e_e = Rewrite_Set Test_simplify False e_; \ neuper@37981: \ e_e = Rewrite_Set rearrange_assoc False e_; \ neuper@37981: \ e_e = Rewrite_Set isolate_root False e_; \ neuper@37981: \ e_e = Rewrite_Set Test_simplify False e_; \ neuper@37906: neuper@37981: \ e_e = Rewrite square_equation_left True e_; \ neuper@37981: \ e_e = Rewrite_Set Test_simplify False e_; \ neuper@37906: neuper@37981: \ e_e = Rewrite_Set norm_equation False e_; \ neuper@37981: \ e_e = Rewrite_Set Test_simplify False e_; \ neuper@37981: \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ neuper@37981: \ e_e = Rewrite_Set Test_simplify False e_e \ neuper@37906: \ in [e_::bool])"; neuper@37906: val ags = map (term_of o the o (parse Test.thy)) neuper@37906: ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; neuper@37906: val fmz = neuper@37906: ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", neuper@37906: "solveFor x","errorBound (eps = #0)","solutions v_i_"]; neuper@37906: ----------------------------------------------------------------11.5.02...*) neuper@37906: neuper@37906: neuper@37906: (*################################# meNEW raises exception with not-locatable neuper@37906: "--------------------- Notlocatable: Free_Solve ---------------------"; neuper@37906: "--------------------- Notlocatable: Free_Solve ---------------------"; neuper@37906: "--------------------- Notlocatable: Free_Solve ---------------------"; neuper@37906: val fmz = []; neuper@37906: val (dI',pI',mI') = neuper@37906: ("Test.thy",["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","sqrt-equ-test"]); neuper@37906: (*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*) neuper@37906: neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@37906: val nxt = ("Model_Problem", neuper@37906: Model_Problem ["sqroot-test","univariate","equation","test"]); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = neuper@37906: ("Add_Given", neuper@37906: Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = ("Add_Given",Add_Given "solveFor x"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = ("Add_Find",Add_Find "solutions v_i_"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = ("Specify_Theory",Specify_Theory "Test.thy"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = neuper@37906: ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@37906: neuper@37906: "--- -1 ---"; neuper@37906: val nxt = ("Free_Solve",Free_Solve); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: neuper@37906: "--- 0 ---"; neuper@37906: val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: (*me ("Begin_Trans" ////*) neuper@37906: neuper@37906: "--- 1 ---"; neuper@37906: val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: neuper@37906: "--- 2 ---"; neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: neuper@37906: "--- 3 ---"; neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: if f = Form' neuper@37906: (FormKF neuper@37906: (~1,EdUndef,1,Nundef, neuper@37906: "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) neuper@37906: then () else raise error "behaviour in root-expl. Free_Solve changed"; neuper@37906: writeln (pr_ptree pr_short pt); neuper@37906: ---------------------------------meNEW raises exception with not-locatable*) neuper@37906: neuper@37906: neuper@37906: val d = e_rls; neuper@37906: neuper@37906: " --- test100: nxt_tac order------------------------------------ "; neuper@37906: " --- test100: nxt_tac order------------------------------------ "; neuper@37906: neuper@37906: val scr as (Script sc) = Script (((inst_abs Test.thy) neuper@37906: o term_of o the o (parse thy)) neuper@37906: "Script Testeq (e_::bool) = \ neuper@37981: \(While (contains_root e_e) Do \ neuper@37906: \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ neuper@37906: \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ neuper@37906: \ (Try (Repeat (Rewrite radd_0 False)))))\ neuper@37981: \ e_e "); neuper@37906: atomty sc; neuper@37906: val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","sqrt-equ-test"]); neuper@37906: val p = e_pos'; val c = []; neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); neuper@37906: val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; neuper@37906: val nxt = ("Specify_Theory",Specify_Theory "Test.thy"); neuper@37906: val (p,_,_,_,_,pt) = me nxt p c pt; neuper@37906: val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) neuper@37906: val (p,_,_,_,_,pt) = me nxt p c pt; neuper@37906: val p = ([1],Res):pos'; neuper@37906: val eq_ = (term_of o the o (parse thy))"e_::bool"; neuper@37906: neuper@37906: val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; neuper@37906: val ve0_= (term_of o the o (parse thy)) ct; neuper@37906: val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], neuper@37906: e_term,e_term,Safe)), neuper@37906: ([],(User', [], [], e_term, e_term,Sundef))]:ets; neuper@37906: val l0 = []; neuper@37906: " --------------- 1. ---------------------------------------------"; neuper@37906: val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete; neuper@37906: (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" neuper@37906: val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: val scr as (Script sc) = neuper@37906: Script (((inst_abs Test.thy) o term_of o the o (parse thy)) neuper@37906: "Script Testterm (g_::real) = (Calculate cancel g_)"); neuper@37906: (* neuper@37906: val scr as (Script sc) = neuper@37906: Script (((inst_abs Test.thy) o term_of o the o (parse thy)) neuper@37906: "Script Testterm (g_::real) = (Calculate power g_)"); neuper@37906: val scr as (Script sc) = neuper@37906: Script (((inst_abs Test.thy) o term_of o the o (parse thy)) neuper@37906: "Script Testterm (g_::real) = (Calculate pow g_)"); neuper@37906: ..............................................................*) neuper@37906: writeln neuper@37906: "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ neuper@37906: \ (Repeat (Calculate cancel g_)) Or \n\ neuper@37906: \ (Repeat (Calculate power g_)) Or \n\ neuper@37906: \%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\ neuper@37906: \%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set"; neuper@37906: neuper@37906: neuper@37906: "--------- sel_rules ---------------------------------------------"; neuper@37906: "--------- sel_rules ---------------------------------------------"; neuper@37906: "--------- sel_rules ---------------------------------------------"; neuper@37906: states:=[]; neuper@37906: CalcTree neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], neuper@37906: ("Test.thy", neuper@37906: ["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; neuper@37906: autoCalculate 1 CompleteCalc; neuper@37906: val ((pt,_),_) = get_calc 1; neuper@37906: show_pt pt; neuper@37906: neuper@37906: val tacs = sel_rules pt ([],Pbl); neuper@37906: if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)"; neuper@37906: neuper@37906: val tacs = sel_rules pt ([1],Res); neuper@37906: if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", neuper@37906: Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), neuper@37906: Check_elementwise "Assumptions"] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([1],Res)"; neuper@37906: neuper@37906: val tacs = sel_rules pt ([3],Pbl); neuper@37906: if tacs = [Apply_Method ["Test", "solve_linear"]] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)"; neuper@37906: neuper@37906: val tacs = sel_rules pt ([3,1],Res); neuper@37906: if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), neuper@37906: Rewrite_Set "Test_simplify"] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)"; neuper@37906: neuper@37906: val tacs = sel_rules pt ([3],Res); neuper@37906: if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", neuper@37906: Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), neuper@37906: Check_elementwise "Assumptions"] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([3],Res)"; neuper@37906: neuper@37906: val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str]; neuper@37906: if tacs = [Tac "no tactics applicable at the end of a calculation"] then () neuper@37906: else raise error "script.sml: diff.behav. in sel_rules ([],Res)";