1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/script.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,996 @@
1.4 +(* use"test-script.sml";
1.5 + WN.13.3.00
1.6 + *)
1.7 +
1.8 +" scripts: Variante 'funktional' ";
1.9 +"############## Make_fun_by_new_variable ##############";
1.10 +"############## Make_fun_by_explicit ##############";
1.11 +"################ Solve_root_equation #################";
1.12 +"------- Notlocatable: Free_Solve -------";
1.13 +
1.14 +" --- test100: nxt_tac order------------------------------------ ";
1.15 +" --- test100: order 1 3 1 2 ----------------------------------- ";
1.16 +" --- test200: nxt_tac order ------------------------------------- ";
1.17 +" --- test200: order 3 1 1 2 --------------------------------- ";
1.18 +
1.19 +" --- root-equation: nxt_tac order------------------------------ ";
1.20 +" --- root-equation: 1.norm_equation ------------------------------ ";
1.21 +(* --- test200: calculate -----------------------------------------*)
1.22 +" --- check_elementwise ------------------------------ ";
1.23 +
1.24 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.25 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.26 +
1.27 +
1.28 +
1.29 +
1.30 +
1.31 +
1.32 +" #################################################### ";
1.33 +" scripts: Variante 'funktional' ";
1.34 +" #################################################### ";
1.35 +
1.36 +val c = (the o (parse DiffApp.thy))
1.37 + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.38 + \ (v_::real) (itv_::real set) (err_::bool) = \
1.39 + \ (let e_ = (hd o (filter (Testvar m_))) rs_; \
1.40 + \ t_ = (if 1 < Length rs_ \
1.41 + \ then (SubProblem (Reals_,[make,function],(Isac_,no_met))\
1.42 + \ [real_ m_, real_ v_, bool_list_ rs_])\
1.43 + \ else (hd rs_)); \
1.44 + \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.45 + \ (DiffAppl_,maximum_on_interval))\
1.46 + \ [bool_ t_, real_ v_, real_set_ itv_]\
1.47 + \ in ((SubProblem (Reals_,[find_values,tool],(DiffAppl_,find_values)) \
1.48 + \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.49 + \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
1.50 +
1.51 +
1.52 +"######################################################";
1.53 +"############## Make_fun_by_new_variable ##############";
1.54 +"######################################################";
1.55 +
1.56 +val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
1.57 + "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.58 + \ (eqs_::bool list) = \
1.59 + \(let h_ = (hd o (filter (Testvar m_))) eqs_; \
1.60 + \ es_ = dropWhile (ident h_) eqs_; \
1.61 + \ vs_ = dropWhile (ident f_) (Var h_); \
1.62 + \ v1_ = Nth 1 vs_; \
1.63 + \ v2_ = Nth 2 vs_; \
1.64 + \ e1_ = (hd o (filter (Testvar v1_))) es_; \
1.65 + \ e2_ = (hd o (filter (Testvar v2_))) es_; \
1.66 + \ (s_1::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\
1.67 + \ [bool_ e1_, real_ v1_]);\
1.68 + \ (s_2::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\
1.69 + \ [bool_ e2_, real_ v2_])\
1.70 + \in Substitute [(v_1, (Rhs o hd) s_1),(v_2, (Rhs o hd) s_2)] h_)";
1.71 +val ags = map (term_of o the o (parse DiffApp.thy))
1.72 + ["A::real", "alpha::real",
1.73 + "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
1.74 +val ll = []:loc_;
1.75 +(* problem with exn PTREE + eval_to -------------------------
1.76 +"-------------- subproblem with empty formalizaton -------";
1.77 +val (mI1,m1) =
1.78 + ("Subproblem", mstep2mstep' pt p
1.79 + (Subproblem (("Reals",["univar","equation","test"],
1.80 + (""(*"ANDERN !!!!!!!*),"no_met")),[])));
1.81 +val (mI2,m2) = (mI1,m1);
1.82 +val (mI3,m3) =
1.83 + ("Substitute", mstep2mstep' pt p
1.84 + (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));
1.85 +"------- same_tacpbl + eval_to -------";
1.86 +val Some(l1,t1) = same_tacpbl sc ll (mI1,m1);
1.87 +loc_2str l1;
1.88 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
1.89 +Sign.string_of_term (sign_of DiffApp.thy) t1;
1.90 +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
1.91 +
1.92 +val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2);
1.93 +loc_2str l2;
1.94 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
1.95 +Sign.string_of_term (sign_of DiffApp.thy) t2;
1.96 +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
1.97 +
1.98 +val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3);
1.99 +loc_2str l3;
1.100 +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
1.101 +Sign.string_of_term (sign_of DiffApp.thy) t3;
1.102 +(*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
1.103 +
1.104 +
1.105 +"------- eq_tacIDs + eq_consts + eval_args -------";
1.106 +val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];
1.107 +val eq_cons = filter (eq_consts m) eq_ids;
1.108 +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
1.109 +"------- locate -------";
1.110 +
1.111 +
1.112 +"-------------- subproblem with formalizaton -------";
1.113 +val (mI,m) =
1.114 + ("Subproblem", mstep2mstep' pt []
1.115 + (Subproblem (("Reals",["univar","equation","test"],
1.116 + (""(*"ANDERN !!!!!!!*),"no_met")),
1.117 + ["a//#2=r*sin alpha","a"])));
1.118 +"------- same_tacpbl + eval_to -------";
1.119 +
1.120 +
1.121 +"------- eq_tacIDs + eq_consts + eval_args -------";
1.122 +val eq_ids = eq_tacIDs [] sc (mI,m) [];
1.123 +val eq_cons = filter (eq_consts m) eq_ids;
1.124 +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
1.125 +
1.126 +
1.127 +"------- locate -------";
1.128 +-------------------------------------------------------*)
1.129 +(* use"ME/script.sml";
1.130 + use"test-script.sml";
1.131 + *)
1.132 +
1.133 +
1.134 +
1.135 +(*#####################################################*)
1.136 +(*#####################################################*)
1.137 +"############## Make_fun_by_explicit ##############";
1.138 +val c = (the o (parse DiffApp.thy))
1.139 + "Script Make_fun_by_explicit (f_::real) (v_::real) \
1.140 + \ (eqs_::bool list) = \
1.141 + \ (let h_ = (hd o (filter (Testvar m_))) eqs_; \
1.142 + \ e1_ = hd (dropWhile (ident h_) eqs_); \
1.143 + \ vs_ = dropWhile (ident f_) (Var h_); \
1.144 + \ v1_ = hd (dropWhile (ident v_) vs_); \
1.145 + \ (s1::bool list) = (SubProblem (Reals_, [univar,equation],(Isac_,no_met))\
1.146 + \ [bool_ e1_, real_ v1_])\
1.147 + \ in Substitute [(v_1, (Rhs o hd) s_1)] h_)";
1.148 +
1.149 +
1.150 +(*#####################################################--------11.5.02
1.151 +"################ Solve_root_equation #################";
1.152 +(*#####################################################*)
1.153 +val sc = (term_of o the o (parse Test.thy))
1.154 + "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
1.155 + \ (let e_ = Rewrite square_equation_left True eq_; \
1.156 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.157 + \ e_ = Rewrite_Set rearrange_assoc False e_; \
1.158 + \ e_ = Rewrite_Set isolate_root False e_; \
1.159 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.160 +
1.161 + \ e_ = Rewrite square_equation_left True e_; \
1.162 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.163 +
1.164 + \ e_ = Rewrite_Set norm_equation False e_; \
1.165 + \ e_ = Rewrite_Set Test_simplify False e_; \
1.166 + \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
1.167 + \ e_ = Rewrite_Set Test_simplify False e_ \
1.168 + \ in [e_::bool])";
1.169 +val ags = map (term_of o the o (parse Test.thy))
1.170 + ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
1.171 +val fmz =
1.172 + ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.173 + "solveFor x","errorBound (eps = #0)","solutions v_i_"];
1.174 +----------------------------------------------------------------11.5.02...*)
1.175 +
1.176 +
1.177 +(*#####################################################*)
1.178 +"------- Notlocatable: Free_Solve -------";
1.179 +"------- Notlocatable: Free_Solve -------";
1.180 +"------- Notlocatable: Free_Solve -------";
1.181 +val fmz = [];
1.182 +val (dI',pI',mI') =
1.183 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.184 + ("Test.thy","sqrt-equ-test"));
1.185 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.186 +val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;
1.187 +val nxt =
1.188 + ("Add_Given",
1.189 + Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
1.190 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.191 +val nxt = ("Add_Given",Add_Given "solveFor x");
1.192 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 +val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
1.194 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.195 +val nxt = ("Add_Find",Add_Find "solutions v_i_");
1.196 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.197 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.198 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.199 +val nxt =
1.200 + ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
1.201 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.202 +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));
1.203 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.204 +
1.205 +"--- -1 ---";
1.206 +val nxt = ("Free_Solve",Free_Solve);
1.207 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.208 +
1.209 +"--- 0 ---";
1.210 +val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");
1.211 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.212 +(*me ("Begin_Trans" ////*)
1.213 +
1.214 +"--- 1 ---";
1.215 +val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left",""));
1.216 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.217 +
1.218 +"--- 2 ---";
1.219 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.220 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.221 +
1.222 +"--- 3 ---";
1.223 +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
1.224 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.225 +if f = Form'
1.226 + (FormKF
1.227 + (~1,EdUndef,1,Nundef,
1.228 + "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))
1.229 +then () else raise error "behaviour in root-expl. Free_Solve changed";
1.230 +writeln (pr_ptree pr_short pt);
1.231 +
1.232 +
1.233 +
1.234 +val d = e_rls;
1.235 +
1.236 +" --- test100: nxt_tac order------------------------------------ ";
1.237 +" --- test100: nxt_tac order------------------------------------ ";
1.238 +
1.239 +val scr as (Script sc) = Script (((inst_abs Test.thy)
1.240 + o term_of o the o (parse thy))
1.241 + "Script Testeq (e_::bool) = \
1.242 + \(While (contains_root e_) Do \
1.243 + \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
1.244 + \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
1.245 + \ (Try (Repeat (Rewrite radd_0 False)))))\
1.246 + \ e_ ");
1.247 +atomty thy sc;
1.248 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.249 + ("Test.thy","sqrt-equ-test"));
1.250 +val p = e_pos'; val c = [];
1.251 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.252 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.253 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.254 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.255 +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.256 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.257 +val p = ([1],Res):pos';
1.258 +val eq_ = (term_of o the o (parse thy))"e_::bool";
1.259 +
1.260 +val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
1.261 +val ve0_= (term_of o the o (parse thy)) ct;
1.262 +val ets0=[([],(Mstep'(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
1.263 + e_term,e_term,Safe)),
1.264 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.265 +val l0 = [];
1.266 +" --------------- 1. ---------------------------------------------";
1.267 +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
1.268 +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
1.269 +
1.270 +
1.271 +(*-----------11.5.02: ets disabolished ------------------
1.272 +
1.273 +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
1.274 +(*val l = [R,R,L,R,R,R] : loc_
1.275 + val m' = Rewrite'...("rroot_square_inv",..(sqrt (sqrt (sqrt a))..
1.276 + -> sqrt (sqrt a)*)
1.277 +
1.278 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.279 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
1.280 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.281 +writeln(ets2str ets1);
1.282 +" --------------- 2. ---------------------------------------------";
1.283 +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
1.284 +
1.285 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.286 +(*val l = [R,R,L,R,R,R] : loc_
1.287 +val m' = Rewrite'...("rroot_square_inv",..,sqrt (sqrt a)..
1.288 + -> #0+ sqrt a =#0*)
1.289 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.290 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.291 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.292 +writeln(ets2str ets2);
1.293 +" --------------- 3. ---------------------------------------------";
1.294 +val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
1.295 +
1.296 +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.297 +(*val l = [R,R,R,D,R,D,R,R] : loc_
1.298 +val m' = Rewrite'...("radd_0","")..(#0 + sqrt a = #0)..-> sqrt a = #0*)
1.299 +
1.300 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
1.301 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
1.302 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.303 +writeln(ets2str ets3);
1.304 +" --------------- 4. ---------------------------------------------";
1.305 +val Appl m'=applicable_in p pt (Rewrite("square_equation_left",""));
1.306 +
1.307 +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
1.308 +(*val l = [R,R,R,D,L,R,R,R] : loc_
1.309 +val m' = Rewrite'...("square_equation_left"..(sqrt a = #0)..a = #0^#2*)
1.310 +
1.311 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.312 +(*=====*) locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
1.313 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.314 +
1.315 +" --------------- 5. ---------------------------------------------";
1.316 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
1.317 +
1.318 +writeln (pr_ptree pr_short pt);writeln("result: "^res^
1.319 +"\n===================================================================");
1.320 +"--- test100 nxt_tac order: finished correctly ---------------";
1.321 +"--- test100 nxt_tac order: finished correctly ---------------";
1.322 +"--- test100 nxt_tac order: finished correctly ---------------";
1.323 +
1.324 +
1.325 +
1.326 +
1.327 +" --- test100: order 1 3 1 2 ----------------------------------- ";
1.328 +" --- test100: order 1 3 1 2 ----------------------------------- ";
1.329 +val scr as (Script sc) =
1.330 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.331 + "Script Testeq (e_::bool) = \
1.332 + \While (contains_root e_) Do \
1.333 + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
1.334 + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
1.335 + \ in Try (Repeat (Rewrite radd_0 False e_))) ");
1.336 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.337 + ("Test.thy","sqrt-equ-test"));
1.338 +val p = e_pos'; val c = [];
1.339 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.340 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.341 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.342 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.343 +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.344 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.345 +val p = ([1],Res):pos';
1.346 +val eq_ = (term_of o the o (parse thy))"e_::bool";
1.347 +
1.348 +val ct = "#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
1.349 +val ve0_= (term_of o the o (parse thy)) ct;
1.350 +val ets0=[([],(Mstep'(Script.thy,"bS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
1.351 + e_term,e_term,Safe)),
1.352 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.353 +val l0 = [];
1.354 +" --------------- 1. --- test100 order 1 3 1 2 --------------------";
1.355 +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
1.356 +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
1.357 +
1.358 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.359 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
1.360 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.361 +writeln (ets2str ets1);
1.362 +" --------------- 2. --- test100 order 1 3 1 2 --------------------";
1.363 +val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
1.364 +val Rewrite'(_,_,_,_,("radd_0",""),f,(_,[])) = m';
1.365 +Sign.string_of_term (sign_of (thy)) f;
1.366 +(*"#0 + sqrt (sqrt a) ^^^ #2 = #0"
1.367 + -> AssocWeak .. pt aus ass_up,ass_dn,assy _verworfen_.. nur letzte tac*)
1.368 +
1.369 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.370 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.371 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.372 +" --------------- 3. --- test100 order 1 3 1 2 --------------------";
1.373 +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
1.374 +
1.375 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
1.376 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
1.377 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.378 +" --------------- 4. --- test100 order 1 3 1 2 --------------------";
1.379 +val Appl m'=applicable_in p pt (Rewrite("square_equation_left",""));
1.380 +
1.381 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.382 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
1.383 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.384 +if res="a = #0 ^^^ #2"then()else raise error "test100 order 1 3 1 2";
1.385 +" --------------- 5. --- test100 order 1 3 1 2 --------------------";
1.386 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
1.387 +writeln (pr_ptree pr_short pt);writeln("result: "^res^
1.388 +"\n===================================================================");
1.389 +"--- test100 order 1 3 1 2: finished correctly --------------";
1.390 +"--- test100 order 1 3 1 2: finished correctly --------------";
1.391 +
1.392 +
1.393 +
1.394 +
1.395 +" --- test200: nxt_tac order ------------------------------------- ";
1.396 +" --- test200: nxt_tac order ------------------------------------- ";
1.397 +
1.398 +val scr as (Script sc) =
1.399 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.400 + "Script Testterm (g_::real) = \
1.401 + \Repeat \
1.402 + \ ((Repeat (Rewrite rmult_1 False g_)) Or \
1.403 + \ (Repeat (Rewrite rmult_0 False g_)) Or \
1.404 + \ (Repeat (Rewrite radd_0 False g_))) ");
1.405 +val d = e_rls; (*domain-rls for assod*)
1.406 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.407 + ("Test.thy","sqrt-equ-test"));
1.408 +val p = e_pos'; val c = [];
1.409 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.410 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.411 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.412 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.413 +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.414 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.415 +val p = ([1],Res):pos';
1.416 +val g_ = (term_of o the o (parse thy)) "g_";
1.417 +
1.418 +val ct = "(#0+#0)*(#1*(#1*a))";
1.419 +val vg0_= (term_of o the o (parse thy)) ct;
1.420 +val ets0 = [([],(Mstep'(Script.thy,"sB","",""), [(g_,vg0_)], [(g_,vg0_)],
1.421 + e_term, e_term,Safe)),
1.422 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.423 +val l0 = [];
1.424 +" --------------- 1. ---------------------------------------------";
1.425 +val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete;
1.426 +val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
1.427 +
1.428 +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
1.429 +(*val l = [R,R,L,R,L,R,R] : loc_
1.430 +val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*(#1*a)*)
1.431 +
1.432 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.433 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
1.434 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.435 +
1.436 +" --------------- 2. ---------------------------------------------";
1.437 +val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
1.438 +
1.439 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.440 +(*val l = [R,R,L,R,L,R,R] : loc_
1.441 +val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*a*)
1.442 +
1.443 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.444 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.445 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.446 +
1.447 +" --------------- 3. ---------------------------------------------";
1.448 +val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
1.449 +
1.450 +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.451 +(*val l = [R,R,R,R] : loc_
1.452 +val m' = Rewrite'...("radd_0","") (#0+#0)*a *)
1.453 +
1.454 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
1.455 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
1.456 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.457 +
1.458 +" --------------- 4. ---------------------------------------------";
1.459 +val Appl m'=applicable_in p pt (Rewrite("rmult_0",""));
1.460 +
1.461 +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
1.462 +(*al l = [R,R,L,R,R,R] : loc_
1.463 +val m' = Rewrite'...("rmult_0","") #0*a *)
1.464 +
1.465 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.466 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
1.467 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.468 +
1.469 +" --------------- 5. ---------------------------------------------";
1.470 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
1.471 +(*al l = [R,R,L,R,R,R] : loc_
1.472 +val m' = Rewrite'...("rmult_0","") #0*a *)
1.473 +writeln (pr_ptree pr_short pt);writeln("result: "^res^
1.474 +"\n===================================================================");
1.475 +"--- test200 nxt_tac order: finished correctly ---------------";
1.476 +"--- test200 nxt_tac order: finished correctly ---------------";
1.477 +
1.478 +
1.479 +
1.480 +
1.481 +" --- test200: order 3 1 1 2 --------------------------------- ";
1.482 +" --- test200: order 3 1 1 2 --------------------------------- ";
1.483 +val p = e_pos'; val c = [];
1.484 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.485 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.486 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.487 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.488 +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.489 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.490 +val p = ([1],Res):pos';
1.491 +val g_ = (term_of o the o (parse thy)) "g_";
1.492 +
1.493 +val ct = "(#0+#0)*(#1*(#1*a))";
1.494 +val vg0_= (term_of o the o (parse thy)) ct;
1.495 +val ets0 = [([],(Mstep'(Script.thy,"sB","",""),[(g_,vg0_)],[(g_,vg0_)],
1.496 + e_term,e_term,Safe)),
1.497 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.498 +val l0 = [];
1.499 +" --------------- 1. --- test200: order 3 1 1 2 -----------------";
1.500 +val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete;
1.501 +val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
1.502 +
1.503 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.504 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
1.505 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.506 +
1.507 +" --------------- 2. --- test200: order 3 1 1 2 -----------------";
1.508 +val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
1.509 +
1.510 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.511 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.512 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.513 +if res="#0 * (#1 * a)"then()else raise error "error test200: order 3 1 1 2";
1.514 +" --------------- 3. --- test200: order 3 1 1 2 -----------------";
1.515 +val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
1.516 +
1.517 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
1.518 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
1.519 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.520 +
1.521 +" --------------- 4. --- test200: order 3 1 1 2 -----------------";
1.522 +val Appl m'=applicable_in p pt (Rewrite("rmult_0",""));
1.523 +
1.524 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.525 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
1.526 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.527 +
1.528 +if res="#0"then()else raise error "test200 order 3 1 1 2";
1.529 +" --------------- 5. --- test200: order 3 1 1 2 -----------------";
1.530 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
1.531 +writeln (pr_ptree pr_short pt);writeln("result: "^res^
1.532 +"\n===================================================================");
1.533 +"--- test200 order 3 1 1 2: finished correctly ---------------";
1.534 +"--- test200 order 3 1 1 2: finished correctly ---------------";
1.535 +
1.536 +
1.537 +------------------------------------11.5.02: ets disabolished ---*)
1.538 +(* use"test-script-nxt_tac.sml";
1.539 + *)
1.540 +
1.541 +(*---------11.5.02:
1.542 +### Currently parsed expression could be extremely ambiguous. ----------
1.543 +
1.544 +" --- root-equation: nxt_tac order------------------------------ ";
1.545 +" --- root-equation: nxt_tac order------------------------------ ";
1.546 +val scr as (Script sc) =
1.547 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.548 + "Script Solve_root_equation (e_::bool) (v_::real) (err_::bool) =\
1.549 + \ (let e_ = \
1.550 + \ (While (contains_root e_) Do \
1.551 + \ (let \
1.552 + \ e_ = Rewrite square_equation_left True e_; \
1.553 + \ e_ = Try (Rewrite_Set Test_simplify False e_); \
1.554 + \ e_ = Try (Rewrite_Set rearrange_assoc False e_); \
1.555 + \ e_ = Try (Rewrite_Set isolate_root False e_) \
1.556 + \ in Try (Rewrite_Set Test_simplify False e_))); \
1.557 + \ e_ = Try (Rewrite_Set norm_equation False e_); \
1.558 + \ e_ = Try (Rewrite_Set Test_simplify False e_); \
1.559 + \ e_ = Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False e_;\
1.560 + \ e_ = Try (Rewrite_Set Test_simplify False e_) \
1.561 + \ in [e_::bool])");
1.562 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.563 + ("Test.thy","sqrt-equ-test"));
1.564 +val p = e_pos'; val c = [];
1.565 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.566 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.567 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.568 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.569 +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.570 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.571 +val p = ([1],Frm):pos';
1.572 +
1.573 +val bdv_ =(term_of o the o (parse thy))"v_::real";
1.574 +val v_ =(term_of o the o (parse thy))"x::real";
1.575 +val eq_ = (term_of o the o (parse thy))"e_::bool";
1.576 +val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)";
1.577 +val ve0_= (term_of o the o (parse thy)) ct;
1.578 +val env= [(bdv_, v_), (eq_, ve0_)];
1.579 +val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)),
1.580 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.581 +val l1 = [];
1.582 +" -------root-equation--- 1.--- nxt_tac-order----------------------";
1.583 +val (pt,_) = cappend_form pt[1]e_istate ct;
1.584 +
1.585 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.586 +(*square_equation_left*)
1.587 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.588 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.589 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.590 +if res = "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"
1.591 +then () else raise error "new behaviour in test-example";
1.592 +writeln (pr_ptree pr_short pt);
1.593 +" -------root-equation--- 2.--- nxt_tac-order----------------------";
1.594 +val ets1 = ets2; val l1 = l2;
1.595 +(*
1.596 +> val eee = (hd) ets2;
1.597 +> val (_,(_,_,ennv,_,rees,_)) = eee;
1.598 +> subst2str ennv;
1.599 +> Sign.string_of_term (sign_of ( thy)) rees;
1.600 +*)
1.601 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.602 +(*Test_simplify*)
1.603 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.604 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.605 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.606 +if res = "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"
1.607 +then () else raise error "new behaviour in test-example";
1.608 +writeln (pr_ptree pr_short pt);
1.609 +" -------root-equation--- 3.--- nxt_tac-order----------------------";
1.610 +val ets1 = ets2; val l1 = l2;
1.611 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.612 +(*rearrange_assoc*)
1.613 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.614 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.615 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.616 +if res = "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"
1.617 +then () else raise error "new behaviour in test-example";
1.618 +writeln (pr_ptree pr_short pt);
1.619 +" -------root-equation--- 4.--- nxt_tac-order----------------------";
1.620 +val ets1 = ets2; val l1 = l2;
1.621 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.622 +(*isolate_root*)
1.623 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.624 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.625 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.626 +if res = "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 * #2)"
1.627 +then () else raise error "new behaviour in test-example";
1.628 +writeln (pr_ptree pr_short pt);
1.629 +" -------root-equation--- 5.--- nxt_tac-order----------------------";
1.630 +val ets1 = ets2; val l1 = l2;
1.631 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.632 +(*Test_simplify*)
1.633 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.634 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.635 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.636 +if res = "sqrt (x ^^^ #2 + #5 * x) = #2 + x"
1.637 +then () else raise error "new behaviour in test-example";
1.638 +writeln (pr_ptree pr_short pt);
1.639 +" -------root-equation--- 6.--- nxt_tac-order----------------------";
1.640 +val ets1 = ets2; val l1 = l2;
1.641 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.642 +(*square_equation_left*)
1.643 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.644 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.645 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.646 +if res = "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"
1.647 +then () else raise error "new behaviour in test-example";
1.648 +writeln (pr_ptree pr_short pt);
1.649 +" -------root-equation--- 7.--- nxt_tac-order----------------------";
1.650 +val ets1 = ets2; val l1 = l2;
1.651 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.652 +(*Test_simplify*)
1.653 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.654 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.655 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.656 +if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"
1.657 +then () else raise error "new behaviour in test-example";
1.658 +writeln (pr_ptree pr_short pt);
1.659 +" -------root-equation--- 8.--- nxt_tac-order----------------------";
1.660 +val ets1 = ets2; val l1 = l2;
1.661 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.662 +(*rearrange_assoc ...<> test-root-equ.sml: norm_equation*)
1.663 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.664 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.665 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.666 +if res = "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"
1.667 +(* "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"
1.668 + ...<> test-root-equ.sml*)
1.669 +then () else raise error "new behaviour in test-example";
1.670 +writeln (pr_ptree pr_short pt);
1.671 +" -------root-equation--- 9.--- nxt_tac-order----------------------";
1.672 +val ets1 = ets2; val l1 = l2;
1.673 +(*> Sign.string_of_term (sign_of thy) (go l2 sc);
1.674 +val it = "Rewrite_Set rearrange_assoc False e_" : string*)
1.675 +
1.676 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.677 +(*Test_simplify*)
1.678 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.679 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.680 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.681 +if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"
1.682 +then () else raise error "new behaviour in test-example";
1.683 +writeln (pr_ptree pr_short pt);
1.684 +" -------root-equation--- 10.--- nxt_tac-order----------------------";
1.685 +val ets1 = ets2; val l1 = l2;
1.686 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.687 +(*norm_equation*)
1.688 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.689 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.690 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.691 +if res = "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"
1.692 +then () else raise error "new behaviour in test-example";
1.693 +writeln (pr_ptree pr_short pt);
1.694 +" -------root-equation--- 11.--- nxt_tac-order----------------------";
1.695 +val ets1 = ets2; val l1 = l2;
1.696 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.697 +(*Test_simplify*)
1.698 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.699 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.700 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.701 +if res = "#-4 + x = #0"
1.702 +then () else raise error "new behaviour in test-example";
1.703 +writeln (pr_ptree pr_short pt);
1.704 +" -------root-equation--- 12.--- nxt_tac-order----------------------";
1.705 +val ets1 = ets2; val l1 = l2;
1.706 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.707 +(*isolate_bdv*)
1.708 +(*> val eee = (last_elem o drop_last) ets2;
1.709 +> val (_,(mmm,_,ennv,_,rees,_)) = eee;
1.710 +val mmm = Rewrite_Set'
1.711 + ("Test.thy","erls",false,"Test_simplify",# $ # $ Free #,(# $ #,[]))
1.712 +> writeln(subst2str ennv);
1.713 +["(e_, x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0)"]
1.714 +> Sign.string_of_term (sign_of ( thy)) rees;
1.715 +val it = "#-4 + x = #0" : string*)
1.716 +
1.717 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.718 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.719 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.720 +if res = "x = #0 + #-1 * #-4"
1.721 +then () else raise error "new behaviour in test-example";
1.722 +writeln (pr_ptree pr_short pt);
1.723 +" -------root-equation--- 13.--- nxt_tac-order----------------------";
1.724 +val ets1 = ets2; val l1 = l2;
1.725 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.726 +(*Test_simplify*)
1.727 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.728 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.729 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.730 +if res = "x = #4"
1.731 +then () else raise error "new behaviour in test-example";
1.732 +writeln (pr_ptree pr_short pt);
1.733 +" -------root-equation--- 14.--- nxt_tac-order----------------------";
1.734 +val ets1 = ets2; val l1 = l2;
1.735 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.736 +
1.737 +writeln (pr_ptree pr_short pt);
1.738 +writeln("result: "^res^"\n===================================================================");
1.739 +" --- root-equation: nxt_tac order .. finised correctly --------- ";
1.740 +" --- root-equation: nxt_tac order .. finised correctly --------- ";
1.741 +
1.742 +
1.743 +-------------------------------------11.5.02-----*)
1.744 +(*-----------------------------------11.5.02 ets disabolished -------
1.745 +
1.746 +" --- root-equation: 1.norm_equation ------------------------------ ";
1.747 +" --- root-equation: 1.norm_equation ------------------------------ ";
1.748 +val p = e_pos'; val c = [];
1.749 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.750 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.751 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.752 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.753 +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.754 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.755 +val p = ([1],Frm):pos';
1.756 +val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)),
1.757 + user_interrupt]:ets;
1.758 +" -------root-equation--- 1.--- 1.norm_equation----------------------";
1.759 +val (pt,_) = cappend_form pt[1]e_istate ct;
1.760 +val Appl m'= applicable_in p pt (Rewrite_Set "norm_equation");
1.761 +
1.762 +val l1 = (fst o last_elem o drop_last) ets1;
1.763 +(*val l1 = [R,L,R,R,L,R];//////////////test-root_equ, me 11.10.00*)
1.764 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.765 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.766 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.767 +if res = "sqrt (#9 + #4 * x) + #-1 * (sqrt x + sqrt (#5 + x)) = #0"
1.768 +then () else raise error "new behaviour in test-example";
1.769 +
1.770 +val l2 = (fst o last_elem o drop_last) ets2;
1.771 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.772 +val ets1 = ets2;
1.773 +" -------root-equation--- 2.--- 1.norm_equation----------------------";
1.774 +(*m'=Rewrite_Set'...,"Test_simplify" *)
1.775 +val l1 = (fst o last_elem o drop_last) ets1;
1.776 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.777 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.778 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.779 +if res = "#-1 * sqrt x + (#-1 * sqrt (#5 + x) + sqrt (#9 + #4 * x)) = #0"
1.780 +then () else raise error "new behaviour in test-example";
1.781 +
1.782 +val Notappl _ =
1.783 + applicable_in p pt (Rewrite_Set_Inst(["(bdv,v_)"],"isolate_bdv"));
1.784 +val Notappl _ = applicable_in p pt (Rewrite_Set "Test_simplify");
1.785 +
1.786 +val l2 = (fst o last_elem o drop_last) ets2;
1.787 +val Helpless = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.788 +(* ~~~~ because isolate_bdv goes without Try *)
1.789 +writeln (pr_ptree pr_short pt);
1.790 +val ets1 = ets2;
1.791 +" -------root-equation--- 3.--- 1.norm_equation----------------------";
1.792 +val Appl m'= applicable_in p pt (Rewrite_Set "rearrange_assoc");
1.793 +
1.794 +val l1 = (fst o last_elem o drop_last) ets1;
1.795 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.796 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.797 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.798 +
1.799 +val l2 = (fst o last_elem o drop_last) ets2;
1.800 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.801 +writeln (pr_ptree pr_short pt);
1.802 +val ets1 = ets2;
1.803 +" -------root-equation--- 4.--- 1.norm_equation----------------------";
1.804 +(*m' = .. isolate_root*)
1.805 +val l1 = (fst o last_elem o drop_last) ets1;
1.806 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.807 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.808 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.809 +
1.810 +val l2 = (fst o last_elem o drop_last) ets2;
1.811 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.812 +writeln (pr_ptree pr_short pt);
1.813 +val ets1 = ets2;
1.814 +" -------root-equation--- 5.--- 1.norm_equation----------------------";
1.815 +(*m' = .. Test_simplify*)
1.816 +val l1 = (fst o last_elem o drop_last) ets1;
1.817 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.818 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.819 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.820 +
1.821 +val l2 = (fst o last_elem o drop_last) ets2;
1.822 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.823 +writeln (pr_ptree pr_short pt);
1.824 +if res="sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)" then ()
1.825 +else raise error "new behaviour in test-example";
1.826 +
1.827 +-------------------------------------11.5.02-----*)
1.828 +
1.829 +
1.830 +(* use"test-script.sml";
1.831 + *)
1.832 +
1.833 +
1.834 +
1.835 +
1.836 +
1.837 +
1.838 +
1.839 +(* --- test200: calculate -----------------------------------------
1.840 +" --- test200: calculate -----------------------------------------";
1.841 +val scr as (Script sc) =
1.842 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.843 + "Script Testterm (g_::real) = \
1.844 + \Repeat (Calculate plus g_) ");
1.845 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.846 + ("Test.thy","sqrt-equ-test"));
1.847 +val p = e_pos'; val c = [];
1.848 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.849 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.850 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.851 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.852 +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.853 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.854 +val p = ([1],Res):pos';
1.855 +val g_ = (term_of o the o (parse thy)) "g_";
1.856 +val vg_= (term_of o the o (parse thy)) "#1+#2";
1.857 +val env = [(g_,vg_)];
1.858 +
1.859 +val ets = []:ets;
1.860 +(* --------------- 1. ---------------------------------------------*)
1.861 +val (pt,_) = cappend_atomic pt [1] e_istate ""
1.862 + (Rewrite("test","")) "#1+#2" Complete;
1.863 +val Appl m'=applicable_in p pt (Calculate "plus");
1.864 +
1.865 +val NextStep(l,m') = nxt_tac "Test.thy" (pt,p) scr ets l;
1.866 +(*val l = [R,R,R,R] : loc_
1.867 + val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*)
1.868 +
1.869 +val ets = (l,mstep'2etac m')::ets;
1.870 +(* --------------- 2. ---------------------------------------------*)
1.871 +val (pt,_) = cappend_atomic pt [1] e_istate ""
1.872 + (Rewrite("test","")) "#3" Complete;
1.873 +
1.874 +val Helpless = nxt_tac "Test.thy" (pt,p) scr ets l;
1.875 +(*val l = [R,R,R,R] : loc_
1.876 + val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*)
1.877 +---*)
1.878 +
1.879 +
1.880 +(* --- test200: Test_simplify -----------------------------------
1.881 +
1.882 +val scr as (Script sc) =
1.883 + Script (((inst_abs Test.thy) o term_of o the o (parse thy))
1.884 + "Script Testterm (g_::real) = \
1.885 + \Repeat \
1.886 + \ ((Repeat (Rewrite radd_mult_distrib2 False g_)) Or \
1.887 + \ (Repeat (Rewrite rdistr_right_assoc False g_)) Or \
1.888 + \ (Repeat (Rewrite rdistr_right_assoc_p False g_)) Or \
1.889 + \ (Repeat (Rewrite rdistr_div_right False g_)) Or \
1.890 + \ (Repeat (Rewrite rbinom_power_2 False g_)) Or \
1.891 + \ (Repeat (Rewrite radd_commute False g_)) Or \
1.892 + \ (Repeat (Rewrite radd_left_commute False g_)) Or \
1.893 + \ (Repeat (Rewrite radd_assoc False g_)) Or \
1.894 + \ (Repeat (Rewrite rmult_commute False g_)) Or \
1.895 + \ (Repeat (Rewrite rmult_left_commute False g_)) Or \
1.896 + \ (Repeat (Rewrite rmult_assoc False g_)) Or \
1.897 + \ (Repeat (Rewrite radd_real_const_eq False g_)) Or \
1.898 + \ (Repeat (Rewrite radd_real_const False g_)) Or \
1.899 + \ (Repeat (Calculate plus g_)) Or \
1.900 + \ (Repeat (Calculate times g_)) Or \
1.901 + \ (Repeat (Rewrite rcollect_right False g_)) Or \
1.902 + \ (Repeat (Rewrite rcollect_one_left False g_)) Or \
1.903 + \ (Repeat (Rewrite rcollect_one_left_assoc False g_)) Or \
1.904 + \ (Repeat (Rewrite rcollect_one_left_assoc_p False g_))) ");
1.905 +---*)
1.906 +writeln
1.907 +"%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\
1.908 +\ (Repeat (Calculate cancel g_)) Or \n\
1.909 +\ (Repeat (Calculate pow g_)) Or \n\
1.910 +\%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\
1.911 +\%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";
1.912 +
1.913 +
1.914 +(*-------------------------------------11.5.02 ets disablished -------
1.915 +
1.916 +" --- check_elementwise ------------------------------ ";
1.917 +" --- check_elementwise ------------------------------ ";
1.918 +val d = e_rls;
1.919 +val scr as (Script sc) = Script (((inst_abs Test.thy)
1.920 + o term_of o the o (parse thy))
1.921 + "Script Testchk (e_::bool) (v_::real) = \
1.922 + \ (let e_ = Try (Rewrite_Set Test_simplify False e_); \
1.923 + \ (L_::real list) = Mstep subproblem_equation_dummy; \
1.924 + \ L_ = Mstep solve_equation_dummy \
1.925 + \ in Check_elementwise L_ {(v_::real). Assumptions})");
1.926 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.927 + ("Test.thy","sqrt-equ-test"));
1.928 +val p = e_pos'; val c = [];
1.929 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.930 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.931 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.932 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.933 +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
1.934 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.935 +val pt = union_asm pt [] [("#0 <= sqrt x + sqrt (#5 + x)",[11]),
1.936 + ("#0 <= #9 + #4 * x",[22]),
1.937 + ("#0 <= x ^^^ #2 + #5 * x",[33]),
1.938 + ("#0 <= #2 + x",[44])];
1.939 +val p = ([1],Res):pos';
1.940 +val eq_ = (term_of o the o (parse thy))"e_::bool";
1.941 +val ct = "x=#1+#3";
1.942 +val ve0_= (term_of o the o (parse thy)) ct;
1.943 +val v_ = (term_of o the o (parse thy))"v_::real";
1.944 +val xx = (term_of o the o (parse thy))"x::real";
1.945 +val env0= [(eq_,ve0_),(v_,xx)];
1.946 +
1.947 +val ets0=[([],(Mstep'(Script.thy,"BS","",""),env0,env0,e_term,e_term,Safe)),
1.948 + ([],(User', [], [], e_term, e_term,Sundef))]:ets;
1.949 +val l0 = [];
1.950 +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
1.951 +" --------------- 1. ---------------------------------------------";
1.952 +val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
1.953 +
1.954 +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
1.955 +(*val l1 = [R,L,R,R] : loc_*)
1.956 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.957 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
1.958 +(*val ets1 = [([R,L,R,R],(Rewrite_Set' #,[#],[#],Free #,# $ #,Safe)),..*)
1.959 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.960 +writeln(ets2str ets1);
1.961 +" --------------- 2. ---------------------------------------------";
1.962 +val Appl m'=applicable_in p pt (Mstep "subproblem_equation_dummy");
1.963 +
1.964 +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
1.965 +(*val l2 = [R,R,D,L,R] : loc_|| val m' = Mstep' ("x = #4",...*)
1.966 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.967 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
1.968 +(*val ets2 =[([R,R,D,L,R],(Mstep' ..subpbl..,[#],[#],Const #,# $ #,Safe)),..*)
1.969 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.970 +writeln(ets2str ets2);
1.971 +" --------------- 3. ---------------------------------------------";
1.972 +val Appl m'=applicable_in p pt (Mstep "solve_equation_dummy");
1.973 +
1.974 +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
1.975 +(*val l3 = [R,R,D,R,D,L,R] : loc_
1.976 + val m' = Mstep'("subproblem_equation_dummy (x = #4)",..*)
1.977 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = (*@@@*)
1.978 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
1.979 +(*val ets3 = [([R,R,D,R,D,L,R], (Mstep' (..,"solve_equation_dummy",..*)
1.980 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.981 +writeln(ets2str ets3);
1.982 +" --------------- 4. ---------------------------------------------";
1.983 +val Appl (m' as (Check_elementwise' (consts,"Assumptions",consts'))) =
1.984 + applicable_in p pt (Check_elementwise "Assumptions");
1.985 +
1.986 +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
1.987 +(*val l4 = [R,R,D,R,D,R,D] : loc_ val m' = Check_elementwise' (Const (#,#) $ ...*)
1.988 +
1.989 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.990 + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
1.991 +(*val ets4 = [([R,R,D,R,D,R,D], (Check_elementwise' (# $ #,"Assumptions",Const #),..*)
1.992 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.993 +" --------------- 5. ---------------------------------------------";
1.994 +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
1.995 +
1.996 +writeln (pr_ptree pr_short pt);writeln("result: "^res^
1.997 +"\n===================================================================");
1.998 +
1.999 +-------------------------------------11.5.02-----*)