1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/root-equ.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,620 @@
1.4 +(* use"../tests/test-root-equ.sml";
1.5 + use"tests/test-root-equ.sml";
1.6 + use"test-root-equ.sml";
1.7 + trace_rewrite:= true;
1.8 + trace_rewrite:= false;
1.9 +
1.10 + method "sqrt-equ-test", _NOT_ "square-equation"
1.11 +*)
1.12 +
1.13 +
1.14 +" ================= equation with x =(-12)/5, but L ={} ======= ";
1.15 +" _________________ rewrite _________________ ";
1.16 +
1.17 +
1.18 +" ================= equation with result={4} ================== ";
1.19 +" -------------- model, specify ------------ ";
1.20 +" ________________ rewrite _________________";
1.21 +" _________________ rewrite_ x=4_________________ ";
1.22 +" _________________ rewrite + cappend _________________ ";
1.23 +" _________________ me Free_Solve _________________ ";
1.24 +" _________________ me + msteps input _________________ ";
1.25 +(*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
1.26 +(*" _________________ me + nxt_step from script (check_elementwise..)______
1.27 + ... L_a = Mstep subproblem_equation_dummy; ";*)
1.28 +(*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*)
1.29 +
1.30 +(*
1.31 +> val t = (term_of o the o (parse thy)) "#2^^^#3";
1.32 +> val eval_fn = the (assoc (!eval_list, "pow"));
1.33 +> val (Some (id,t')) = get_pair thy "pow" eval_fn t;
1.34 +> Sign.string_of_term (sign_of thy) t';
1.35 +*)
1.36 +(******************************************************************)
1.37 +(* ------------------------------------- *)
1.38 +" _________________ equation with x =(-12)/5, but L ={} ------- ";
1.39 +(* ------------------------------------- *)
1.40 +" _________________ rewrite _________________ ";
1.41 +val thy' = "Test.thy";
1.42 +val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
1.43 +val thm = ("square_equation_left","");
1.44 +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.45 +(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
1.46 +val rls = ("Test_simplify");
1.47 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.48 +(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)
1.49 +val rls = ("rearrange_assoc");
1.50 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.51 +(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)
1.52 +val rls = ("isolate_root");
1.53 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.54 +(*"sqrt (x ^^^ 2 + -3 * x) =
1.55 +(-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
1.56 +val rls = ("Test_simplify");
1.57 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.58 +(*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
1.59 +val thm = ("square_equation_left","");
1.60 +val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.61 +val asm = asm union asm';
1.62 +(*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
1.63 +val rls = ("Test_simplify");
1.64 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.65 +(*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)
1.66 +val rls = ("norm_equation");
1.67 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.68 +(*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)
1.69 +val rls = ("Test_simplify");
1.70 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.71 +(*"-36 + -15 * x = 0"*)
1.72 +val rls = ("isolate_bdv");
1.73 +val (ct,_) = the (rewrite_set_inst thy' false
1.74 + [("bdv","x::real")] rls ct);
1.75 +(*"x = (0 + -1 * -36) // -15"*)
1.76 +val rls = ("Test_simplify");
1.77 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.78 +if ct<>"x = -12 / 5"then raise error "new behaviour in testexample"else ();
1.79 +
1.80 +(*
1.81 +val ct = "x = (-12) / 5" : cterm'
1.82 +> asm;
1.83 +val it =
1.84 + ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
1.85 + "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list
1.86 +*)
1.87 +
1.88 +
1.89 +
1.90 +
1.91 +
1.92 +" ================== equation with result={4} ================== ";
1.93 +" ================== equation with result={4} ================== ";
1.94 +" ================== equation with result={4} ================== ";
1.95 +
1.96 +" -------------- model, specify ------------ ";
1.97 +" -------------- model, specify ------------ ";
1.98 +" -------------- model, specify ------------ ";
1.99 +" --- subproblem 1: linear-equation --- ";
1.100 +val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.101 + "bound_variable x","error_bound 0"(*,
1.102 + "solutions L::real set" ,
1.103 + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.104 +val thy = Isac.thy;
1.105 +val formals = map (the o (parse thy)) origin;
1.106 +
1.107 +val given = ["equation (l=(r::real))",
1.108 + "bound_variable bdv", (* TODO type *)
1.109 + "error_bound eps"];
1.110 +val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.*)
1.111 + "bdv is_var",
1.112 + "eps is_const_expr"];
1.113 +val find = ["solutions (L::bool list)"];
1.114 +val with_ = [(* parseold ...
1.115 + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.116 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.117 +val givens = map (the o (parse thy)) given;
1.118 +parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
1.119 +(* 31.1.00
1.120 +val tag__forms = chktyps thy (formals, givens);
1.121 +map ((atomty thy) o term_of) tag__forms; *)
1.122 +
1.123 +" --- subproblem 2: linear-equation --- ";
1.124 +val origin = ["x + 4 = (0::real)","x::real"];
1.125 +val formals = map (the o (parse thy)) origin;
1.126 +
1.127 +val given = ["equation (l=(0::real))",
1.128 + "bound_variable bdv"];
1.129 +val where_ = ["l is_linear_in bdv","bdv is_const"];
1.130 +val find = ["l::real"];
1.131 +val with_ = ["l = (%x. l) bdv"];
1.132 +val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
1.133 +val givens = map (the o (parse thy)) given;
1.134 +
1.135 +val tag__forms = chktyps thy (formals, givens);
1.136 +map ((atomty thy) o term_of) tag__forms;
1.137 +
1.138 +
1.139 +
1.140 +" _________________ rewrite_ x+4_________________ ";
1.141 +" _________________ rewrite_ x+4_________________ ";
1.142 +" _________________ rewrite_ x+4_________________ ";
1.143 +val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.144 +val thm = num_str square_equation_left;
1.145 +val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
1.146 +val rls = Test_simplify;
1.147 +val (t,_) = the (rewrite_set_ thy false rls t);
1.148 +val rls = rearrange_assoc;
1.149 +val (t,_) = the (rewrite_set_ thy false rls t);
1.150 +val rls = isolate_root;
1.151 +val (t,_) = the (rewrite_set_ thy false rls t);
1.152 +
1.153 +val rls = Test_simplify;
1.154 +val (t,_) = the (rewrite_set_ thy false rls t);
1.155 +(*
1.156 +sqrt (x ^^^ 2 + 5 * x) =
1.157 +(5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
1.158 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.159 +### trying thm 'rdistr_div_right'
1.160 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.161 +(5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
1.162 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.163 +(5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.164 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.165 +5 / (-1 * 2) + 2 * x / (-1 * 2) +
1.166 +(-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.167 +
1.168 +### trying thm 'radd_left_commute'
1.169 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.170 +-1 * 9 / (-1 * 2) +
1.171 +(5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.172 +### trying thm 'radd_assoc'
1.173 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.174 +-1 * 9 / (-1 * 2) +
1.175 +(5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
1.176 +
1.177 +### trying thm 'radd_real_const_eq'
1.178 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.179 +-1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
1.180 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.181 +-1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
1.182 +### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.183 +(-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
1.184 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.185 +
1.186 +28.8.02: ruleset besser zusammenstellen !!!
1.187 +*)
1.188 +val thm = num_str square_equation_left;
1.189 +val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
1.190 +val asm = asm union asm';
1.191 +val rls = Test_simplify;
1.192 +val (t,_) = the (rewrite_set_ thy false rls t);
1.193 +val rls = norm_equation;
1.194 +val (t,_) = the (rewrite_set_ thy false rls t);
1.195 +val rls = Test_simplify;
1.196 +val (t,_) = the (rewrite_set_ thy false rls t);
1.197 +val rls = isolate_bdv;
1.198 +val subst = [(str2term "bdv", str2term "x")];
1.199 +val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
1.200 +val rls = Test_simplify;
1.201 +val (t,_) = the (rewrite_set_ thy false rls t);
1.202 +val t' = term2str t;
1.203 +if t' = "x = 4" then ()
1.204 +else raise error "root-equ.sml: new behav. in rewrite_ x+4";
1.205 +
1.206 +" _________________ rewrite x=4_________________ ";
1.207 +" _________________ rewrite x=4_________________ ";
1.208 +" _________________ rewrite x=4_________________ ";
1.209 +(*
1.210 +rewrite thy' "tless_true" "tval_rls" true (num_str rbinom_power_2) ct;
1.211 +atomty thy ((#prop o rep_thm) (!tthm));
1.212 +atomty thy (term_of (!tct));
1.213 +*)
1.214 +val thy' = "Test.thy";
1.215 +val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.216 +(*1*)val thm = ("square_equation_left","");
1.217 +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.218 +"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
1.219 +(*2*)val rls = "Test_simplify";
1.220 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.221 +"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
1.222 +(*3*)val rls = "rearrange_assoc";
1.223 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.224 +"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
1.225 +(*4*)val rls = "isolate_root";
1.226 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.227 +"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
1.228 +(*5*)val rls = "Test_simplify";
1.229 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.230 +"sqrt (x ^^^ 2 + 5 * x) = 2 + x";
1.231 +(*6*)val thm = ("square_equation_left","");
1.232 +val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.233 +val asm = asm union asm';
1.234 +"x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
1.235 +(*7*)val rls = "Test_simplify";
1.236 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.237 +"x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
1.238 +(*8*)val rls = "norm_equation";
1.239 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.240 +"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
1.241 +(*9*)val rls = "Test_simplify";
1.242 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.243 +"-4 + x = 0";
1.244 +(*10*)val rls = "isolate_bdv";
1.245 +val (ct,_) = the (rewrite_set_inst thy' false
1.246 + [("bdv","x")] rls ct);
1.247 +"x = 0 + -1 * -4";
1.248 +(*11*)val rls = "Test_simplify";
1.249 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.250 +if ct="x = 4" then () else raise error "new behaviour in test-example";
1.251 +
1.252 +
1.253 +
1.254 +
1.255 +" _________________ rewrite + cappend _________________ ";
1.256 +" _________________ rewrite + cappend _________________ ";
1.257 +" _________________ rewrite + cappend _________________ ";
1.258 +val thy' = "Test.thy";
1.259 +val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.260 +val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
1.261 +val oris = prep_ori ctl thy ((#ppc o get_pbt)
1.262 + ["sqroot-test","univariate","equation","test"]);
1.263 +val loc = e_istate;
1.264 +val (pt,pos) = (e_ptree,[]);
1.265 +val (pt,_) = cappend_problem pt pos loc (oris,empty_spec);
1.266 +val pt = update_branch pt [] Transitive;
1.267 +(*
1.268 +val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
1.269 +*)
1.270 +(*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
1.271 +val pt = update_domID pt [] "Test";
1.272 +val pt = update_pblID pt [] ["Test",
1.273 + "equations","univariate","square-root"];
1.274 +val pt = update_metID pt [] ("Test","sqrt-equ-test");
1.275 +val pt = update_pbl pt [] [];
1.276 +val pt = update_met pt [] [];
1.277 +(*
1.278 +> get_obj g_spec pt [];
1.279 +val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec
1.280 +> val pt = update_domID pt [] "RatArith";
1.281 +> get_obj g_spec pt [];
1.282 +val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec
1.283 +> val pt = update_pblID pt [] ["RatArith",
1.284 + "equations","univariate","square-root"];
1.285 +> get_obj g_spec pt [];
1.286 +("RatArith",["RatArith","equations","univariate","square-root"],
1.287 + ("e_domID","e_metID")) : spec
1.288 +> val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
1.289 +> get_obj g_spec pt [];
1.290 + ("RatArith",["RatArith","equations","univariate","square-root"],
1.291 + ("RatArith","sqrt-equ-test")) : spec
1.292 +*)
1.293 +
1.294 +val pos = [1];
1.295 +val (pt,_) = cappend_parent pt pos loc ct (Mstep "repeat") Transitive;
1.296 +
1.297 +val pos = (lev_on o lev_dn) pos;
1.298 +val thm = ("square_equation_left",""); val ctold = ct;
1.299 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm ct);
1.300 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep (fst thm)) ct Complete;
1.301 +val pt = union_asm pt [] (map (rpair []) asm);
1.302 +
1.303 +val pos = lev_on pos;
1.304 +val rls = ("Test_simplify"); val ctold = ct;
1.305 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.306 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.307 +
1.308 +val pos = lev_on pos;
1.309 +val rls = ("rearrange_assoc"); val ctold = ct;
1.310 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.311 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.312 +
1.313 +val pos = lev_on pos;
1.314 +val rls = ("isolate_root"); val ctold = ct;
1.315 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.316 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.317 +
1.318 +val pos = lev_on pos;
1.319 +val rls = ("Test_simplify"); val ctold = ct;
1.320 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.321 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.322 +
1.323 +val pos = lev_on pos;
1.324 +val thm = ("square_equation_left",""); val ctold = ct;
1.325 +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.326 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.327 +val pt = union_asm pt [] (map (rpair []) asm);
1.328 +
1.329 +val pos = lev_up pos;
1.330 +val (pt,_) = append_result pt pos e_istate ct Complete;
1.331 +
1.332 +val pos = lev_on pos;
1.333 +val rls = ("Test_simplify"); val ctold = ct;
1.334 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.335 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.336 +
1.337 +val pos = lev_on pos;
1.338 +val rls = ("norm_equation"); val ctold = ct;
1.339 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.340 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.341 +
1.342 +val pos = lev_on pos;
1.343 +val rls = ("Test_simplify"); val ctold = ct;
1.344 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.345 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.346 +
1.347 +(* --- see comments in interface_ME_ISA/instantiate''
1.348 +val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");
1.349 +val (ct,_) = the (rewrite_set thy' false
1.350 + ("#isolate_bdv",rlsdat') ct); *)
1.351 +val pos = lev_on pos;
1.352 +val rls = ("isolate_bdv"); val ctold = ct;
1.353 +val (ct,_) = the (rewrite_set_inst thy' false
1.354 + [("bdv","x")] rls ct);
1.355 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.356 +
1.357 +val pos = lev_on pos;
1.358 +val rls = ("Test_simplify"); val ctold = ct;
1.359 +val (ct,_) = the (rewrite_set thy' false rls ct);
1.360 +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
1.361 +
1.362 +val pos = lev_up pos;
1.363 +val (pt,pos) = append_result pt pos e_istate ct Complete;
1.364 +get_obj g_asm pt [];
1.365 +
1.366 +writeln (pr_ptree pr_short pt);
1.367 +(* aus src.24-11-99:
1.368 +. sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
1.369 +1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
1.370 +1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
1.371 +1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2
1.372 +1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
1.373 +1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2)
1.374 +1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
1.375 +1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x
1.376 +2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
1.377 +3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?!
1.378 +4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
1.379 +5. (-4) + x = (+0)
1.380 +6. x = (+0) + (-1) * (-4)
1.381 +*)
1.382 +
1.383 +(*
1.384 +val t = (term_of o the o (parse thy)) "solutions (L::real set)";
1.385 +atomty thy t;
1.386 +*)
1.387 +
1.388 +
1.389 +(*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
1.390 + from thy ???, i.e. together with the *_simplify ?!!!? ----------
1.391 +" _________________ me Free_Solve _________________ ";
1.392 +" _________________ me Free_Solve _________________ ";
1.393 +" _________________ me Free_Solve _________________ ";
1.394 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.395 + "solveFor x","errorBound (eps=0)",
1.396 + "solutions L"(*,
1.397 + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
1.398 +val (dI',pI',mI') =
1.399 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.400 + ("Test.thy","sqrt-equ-test"));
1.401 +val p = e_pos'; val c = [];
1.402 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.403 +
1.404 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.405 +(*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
1.406 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.407 +(* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
1.408 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.409 +(* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
1.410 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.411 +(* val nxt = ("Add_Find",Add_Find "solutions L"); *)
1.412 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.413 +(* val nxt = ("Specify_Domain",Specify_Domain "DiffAppl.thy");
1.414 +> get_obj g_spec pt (fst p);
1.415 +val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
1.416 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.417 +(*val nxt = ("Specify_Problem", Specify_Problem *)
1.418 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.419 +(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*)
1.420 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.421 +(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*)
1.422 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.423 +val nxt = ("Free_Solve",Free_Solve);
1.424 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.425 +get_obj g_spec pt [];
1.426 +
1.427 +"--- -2 ---";
1.428 +get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
1.429 +val (p,_,f,nxt,_,pt)=
1.430 +me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
1.431 +(* 15.4.
1.432 +"--- -1 ---";
1.433 +get_form ("Begin_Trans",Begin_Trans) p pt;
1.434 +val (p,_,f,nxt,_,pt)=
1.435 +me ("Begin_Trans",Begin_Trans) p [4] pt; *)
1.436 +
1.437 +"--- 1 ---";
1.438 +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
1.439 +val (p,_,f,nxt,_,pt)=
1.440 +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;
1.441 +"--- 2 ---";
1.442 +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
1.443 +val (p,_,f,nxt,_,pt)=
1.444 +me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
1.445 +"--- 3 ---";
1.446 +get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
1.447 +val (p,_,f,nxt,_,pt)=
1.448 +me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
1.449 +"--- 4 ---";
1.450 +get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
1.451 +val (p,_,f,nxt,_,pt)=
1.452 +me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
1.453 +"--- 5 ---";
1.454 +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
1.455 +val (p,_,f,nxt,_,pt)=
1.456 +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
1.457 +"--- 6 ---";
1.458 +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
1.459 +val (p,_,f,nxt,_,pt)=
1.460 +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;
1.461 +(* 15.4.
1.462 +"--- ---";
1.463 +get_form ("End_Trans",End_Trans) p pt;
1.464 +val (p,_,f,nxt,_,pt)=
1.465 +me ("End_Trans",End_Trans) p [11] pt; *)
1.466 +"--- 7 ---";
1.467 +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
1.468 +val (p,_,f,nxt,_,pt)=
1.469 +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
1.470 +"--- 8 ---";
1.471 +get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
1.472 +val (p,_,f,nxt,_,pt)=
1.473 +me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
1.474 +"--- 9 ---";
1.475 +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
1.476 +val (p,_,f,nxt,_,pt)=
1.477 +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
1.478 +"--- 10 ---.";
1.479 +get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt;
1.480 +val (p,_,f,nxt,_,pt)=
1.481 +me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt;
1.482 +"--- 11 ---";
1.483 +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
1.484 +val ((p,p_),_,f,nxt,_,pt)=
1.485 +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
1.486 +(* 5.4.00.: ---
1.487 +get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt;
1.488 +val (p,_,f,nxt,_,pt)=
1.489 +me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt;
1.490 +--- *)
1.491 +writeln (pr_ptree pr_short pt);
1.492 +writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
1.493 +*)
1.494 +
1.495 +
1.496 +" _________________ me + msteps input _________________ ";
1.497 +" _________________ me + msteps input _________________ ";
1.498 +" _________________ me + msteps input _________________ ";
1.499 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.500 + "solveFor x","errorBound (eps=0)",
1.501 + "solutions L"];
1.502 +val (dI',pI',mI') =
1.503 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.504 + ("Test.thy","sqrt-equ-test"));
1.505 +val p = e_pos'; val c = [];
1.506 +"--- s1 ---";
1.507 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.508 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.509 +"--- s2 ---";
1.510 +val nxt = ("Add_Given",
1.511 +Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
1.512 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.513 +"--- s3 ---";
1.514 +val nxt = ("Add_Given",Add_Given "solveFor x");
1.515 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.516 +"--- s4 ---";
1.517 +val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
1.518 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.519 +"--- s5 ---";
1.520 +val nxt = ("Add_Find",Add_Find "solutions L");
1.521 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.522 +"--- s6 ---";
1.523 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.524 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.525 +"--- s7 ---";
1.526 +val nxt = ("Specify_Problem",
1.527 +Specify_Problem ["sqroot-test","univariate","equation","test"]);
1.528 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.529 +"--- s8 ---";
1.530 +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));
1.531 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.532 +"--- s9 ---";
1.533 +val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));
1.534 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.535 +"--- 1 ---";
1.536 +val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
1.537 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.538 +
1.539 +(*me------------
1.540 + val (mI,m) = nxt; val pos' as (p,p_) = p;
1.541 +
1.542 + val Appl m = applicable_in (p,p_) pt m;
1.543 +(*solve*)
1.544 + val pp = par_pblobj pt p;
1.545 + val metID = get_obj g_metID pt pp;
1.546 + val sc = (#scr o get_met) metID;
1.547 + val is = get_istate pt (p,p_);
1.548 + val thy' = get_obj g_domID pt pp;
1.549 + val thy = assoc_thy thy';
1.550 + val d = e_rls;
1.551 + val Steps [(m',f',pt',p',c',s')] =
1.552 + locate_gen thy' m (pt,(p,p_)) (sc,d) is;
1.553 + val is' = get_istate pt' p';
1.554 + next_tac thy' (pt'(*'*),p') sc is';
1.555 +
1.556 +
1.557 +
1.558 +
1.559 +val ttt = (term_of o the o (parse Test.thy))
1.560 +"Let (((While contains_root e_ Do\
1.561 +\Rewrite square_equation_left True @@\
1.562 +\Try (Rewrite_Set Test_simplify False) @@\
1.563 +\Try (Rewrite_Set rearrange_assoc False) @@\
1.564 +\Try (Rewrite_Set Test_simplify False)) @@\
1.565 +\Try (Rewrite_Set norm_equation False) @@\
1.566 +\Try (Rewrite_Set Test_simplify False) @@\
1.567 +\Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False @@\
1.568 +\Try (Rewrite_Set Test_simplify False))\
1.569 +\e_)";
1.570 +
1.571 +-------------------------*)
1.572 +
1.573 +
1.574 +"--- 2 ---";
1.575 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.576 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.577 +"--- 3 ---";
1.578 +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
1.579 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.580 +"--- 4 ---";
1.581 +val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
1.582 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.583 +"--- 5 ---";
1.584 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.585 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.586 +"--- 6 ---";
1.587 +val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
1.588 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.589 +"--- 7 ---";
1.590 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.591 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.592 +"--- 8<> ---";
1.593 +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
1.594 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.595 +"--- 9<> ---";
1.596 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.597 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.598 +"--- 10<> ---";
1.599 +val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
1.600 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.601 +"--- 11<> ---.";
1.602 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.603 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.604 +"--- 12<> ---";
1.605 +val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));
1.606 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.607 +"--- 13<> ---";
1.608 +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
1.609 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.610 +"--- 1<> ---";
1.611 +val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);
1.612 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.613 +(* val nxt = ("End_Proof'",End_Proof');*)
1.614 +if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
1.615 +then raise error "me + msteps input: not finished correctly"
1.616 +else "root-equation, me + msteps input: OK";
1.617 +
1.618 +writeln (pr_ptree pr_short pt);
1.619 +writeln("result: "^(get_obj g_result pt [])^
1.620 +"\n==============================================================");
1.621 +
1.622 +
1.623 +