agriesma@338
|
1 |
(* use"../tests/test-root-equ.sml";
|
agriesma@338
|
2 |
use"tests/test-root-equ.sml";
|
agriesma@338
|
3 |
use"test-root-equ.sml";
|
agriesma@338
|
4 |
trace_rewrite:= true;
|
agriesma@338
|
5 |
trace_rewrite:= false;
|
agriesma@338
|
6 |
|
agriesma@338
|
7 |
method "sqrt-equ-test", _NOT_ "square-equation"
|
agriesma@338
|
8 |
*)
|
agriesma@338
|
9 |
|
agriesma@338
|
10 |
|
agriesma@338
|
11 |
" ================= equation with x =(-12)/5, but L ={} ======= ";
|
agriesma@338
|
12 |
" _________________ rewrite _________________ ";
|
agriesma@338
|
13 |
|
agriesma@338
|
14 |
|
agriesma@338
|
15 |
" ================= equation with result={4} ================== ";
|
agriesma@338
|
16 |
" -------------- model, specify ------------ ";
|
agriesma@338
|
17 |
" ________________ rewrite _________________";
|
agriesma@338
|
18 |
" _________________ rewrite_ x=4_________________ ";
|
agriesma@338
|
19 |
" _________________ rewrite + cappend _________________ ";
|
agriesma@338
|
20 |
" _________________ me Free_Solve _________________ ";
|
agriesma@338
|
21 |
" _________________ me + msteps input _________________ ";
|
agriesma@338
|
22 |
(*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
|
agriesma@338
|
23 |
(*" _________________ me + nxt_step from script (check_elementwise..)______
|
agriesma@338
|
24 |
... L_a = Mstep subproblem_equation_dummy; ";*)
|
agriesma@338
|
25 |
(*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*)
|
agriesma@338
|
26 |
|
agriesma@338
|
27 |
(*
|
agriesma@338
|
28 |
> val t = (term_of o the o (parse thy)) "#2^^^#3";
|
agriesma@338
|
29 |
> val eval_fn = the (assoc (!eval_list, "pow"));
|
agriesma@338
|
30 |
> val (Some (id,t')) = get_pair thy "pow" eval_fn t;
|
agriesma@338
|
31 |
> Sign.string_of_term (sign_of thy) t';
|
agriesma@338
|
32 |
*)
|
agriesma@338
|
33 |
(******************************************************************)
|
agriesma@338
|
34 |
(* ------------------------------------- *)
|
agriesma@338
|
35 |
" _________________ equation with x =(-12)/5, but L ={} ------- ";
|
agriesma@338
|
36 |
(* ------------------------------------- *)
|
agriesma@338
|
37 |
" _________________ rewrite _________________ ";
|
agriesma@338
|
38 |
val thy' = "Test.thy";
|
agriesma@338
|
39 |
val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
|
agriesma@338
|
40 |
val thm = ("square_equation_left","");
|
agriesma@338
|
41 |
val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
agriesma@338
|
42 |
(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
|
agriesma@338
|
43 |
val rls = ("Test_simplify");
|
agriesma@338
|
44 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
45 |
(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)
|
agriesma@338
|
46 |
val rls = ("rearrange_assoc");
|
agriesma@338
|
47 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
48 |
(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)
|
agriesma@338
|
49 |
val rls = ("isolate_root");
|
agriesma@338
|
50 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
51 |
(*"sqrt (x ^^^ 2 + -3 * x) =
|
agriesma@338
|
52 |
(-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
|
agriesma@338
|
53 |
val rls = ("Test_simplify");
|
agriesma@338
|
54 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
55 |
(*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
|
agriesma@338
|
56 |
val thm = ("square_equation_left","");
|
agriesma@338
|
57 |
val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
agriesma@338
|
58 |
val asm = asm union asm';
|
agriesma@338
|
59 |
(*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
|
agriesma@338
|
60 |
val rls = ("Test_simplify");
|
agriesma@338
|
61 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
62 |
(*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)
|
agriesma@338
|
63 |
val rls = ("norm_equation");
|
agriesma@338
|
64 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
65 |
(*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)
|
agriesma@338
|
66 |
val rls = ("Test_simplify");
|
agriesma@338
|
67 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
68 |
(*"-36 + -15 * x = 0"*)
|
agriesma@338
|
69 |
val rls = ("isolate_bdv");
|
agriesma@338
|
70 |
val (ct,_) = the (rewrite_set_inst thy' false
|
agriesma@338
|
71 |
[("bdv","x::real")] rls ct);
|
agriesma@338
|
72 |
(*"x = (0 + -1 * -36) // -15"*)
|
agriesma@338
|
73 |
val rls = ("Test_simplify");
|
agriesma@338
|
74 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
75 |
if ct<>"x = -12 / 5"then raise error "new behaviour in testexample"else ();
|
agriesma@338
|
76 |
|
agriesma@338
|
77 |
(*
|
agriesma@338
|
78 |
val ct = "x = (-12) / 5" : cterm'
|
agriesma@338
|
79 |
> asm;
|
agriesma@338
|
80 |
val it =
|
agriesma@338
|
81 |
["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
|
agriesma@338
|
82 |
"(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list
|
agriesma@338
|
83 |
*)
|
agriesma@338
|
84 |
|
agriesma@338
|
85 |
|
agriesma@338
|
86 |
|
agriesma@338
|
87 |
|
agriesma@338
|
88 |
|
agriesma@338
|
89 |
" ================== equation with result={4} ================== ";
|
agriesma@338
|
90 |
" ================== equation with result={4} ================== ";
|
agriesma@338
|
91 |
" ================== equation with result={4} ================== ";
|
agriesma@338
|
92 |
|
agriesma@338
|
93 |
" -------------- model, specify ------------ ";
|
agriesma@338
|
94 |
" -------------- model, specify ------------ ";
|
agriesma@338
|
95 |
" -------------- model, specify ------------ ";
|
agriesma@338
|
96 |
" --- subproblem 1: linear-equation --- ";
|
agriesma@338
|
97 |
val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
agriesma@338
|
98 |
"bound_variable x","error_bound 0"(*,
|
agriesma@338
|
99 |
"solutions L::real set" ,
|
agriesma@338
|
100 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
agriesma@338
|
101 |
val thy = Isac.thy;
|
agriesma@338
|
102 |
val formals = map (the o (parse thy)) origin;
|
agriesma@338
|
103 |
|
agriesma@338
|
104 |
val given = ["equation (l=(r::real))",
|
agriesma@338
|
105 |
"bound_variable bdv", (* TODO type *)
|
agriesma@338
|
106 |
"error_bound eps"];
|
agriesma@338
|
107 |
val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.*)
|
agriesma@338
|
108 |
"bdv is_var",
|
agriesma@338
|
109 |
"eps is_const_expr"];
|
agriesma@338
|
110 |
val find = ["solutions (L::bool list)"];
|
agriesma@338
|
111 |
val with_ = [(* parseold ...
|
agriesma@338
|
112 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
agriesma@338
|
113 |
val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
|
agriesma@338
|
114 |
val givens = map (the o (parse thy)) given;
|
agriesma@338
|
115 |
parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
|
agriesma@338
|
116 |
(* 31.1.00
|
agriesma@338
|
117 |
val tag__forms = chktyps thy (formals, givens);
|
agriesma@338
|
118 |
map ((atomty thy) o term_of) tag__forms; *)
|
agriesma@338
|
119 |
|
agriesma@338
|
120 |
" --- subproblem 2: linear-equation --- ";
|
agriesma@338
|
121 |
val origin = ["x + 4 = (0::real)","x::real"];
|
agriesma@338
|
122 |
val formals = map (the o (parse thy)) origin;
|
agriesma@338
|
123 |
|
agriesma@338
|
124 |
val given = ["equation (l=(0::real))",
|
agriesma@338
|
125 |
"bound_variable bdv"];
|
agriesma@338
|
126 |
val where_ = ["l is_linear_in bdv","bdv is_const"];
|
agriesma@338
|
127 |
val find = ["l::real"];
|
agriesma@338
|
128 |
val with_ = ["l = (%x. l) bdv"];
|
agriesma@338
|
129 |
val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
|
agriesma@338
|
130 |
val givens = map (the o (parse thy)) given;
|
agriesma@338
|
131 |
|
agriesma@338
|
132 |
val tag__forms = chktyps thy (formals, givens);
|
agriesma@338
|
133 |
map ((atomty thy) o term_of) tag__forms;
|
agriesma@338
|
134 |
|
agriesma@338
|
135 |
|
agriesma@338
|
136 |
|
agriesma@338
|
137 |
" _________________ rewrite_ x+4_________________ ";
|
agriesma@338
|
138 |
" _________________ rewrite_ x+4_________________ ";
|
agriesma@338
|
139 |
" _________________ rewrite_ x+4_________________ ";
|
agriesma@338
|
140 |
val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
agriesma@338
|
141 |
val thm = num_str square_equation_left;
|
agriesma@338
|
142 |
val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
|
agriesma@338
|
143 |
val rls = Test_simplify;
|
agriesma@338
|
144 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
145 |
val rls = rearrange_assoc;
|
agriesma@338
|
146 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
147 |
val rls = isolate_root;
|
agriesma@338
|
148 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
149 |
|
agriesma@338
|
150 |
val rls = Test_simplify;
|
agriesma@338
|
151 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
152 |
(*
|
agriesma@338
|
153 |
sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
154 |
(5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
|
agriesma@338
|
155 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
agriesma@338
|
156 |
### trying thm 'rdistr_div_right'
|
agriesma@338
|
157 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
158 |
(5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
|
agriesma@338
|
159 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
160 |
(5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
agriesma@338
|
161 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
162 |
5 / (-1 * 2) + 2 * x / (-1 * 2) +
|
agriesma@338
|
163 |
(-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
agriesma@338
|
164 |
|
agriesma@338
|
165 |
### trying thm 'radd_left_commute'
|
agriesma@338
|
166 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
167 |
-1 * 9 / (-1 * 2) +
|
agriesma@338
|
168 |
(5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
agriesma@338
|
169 |
### trying thm 'radd_assoc'
|
agriesma@338
|
170 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
171 |
-1 * 9 / (-1 * 2) +
|
agriesma@338
|
172 |
(5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
|
agriesma@338
|
173 |
|
agriesma@338
|
174 |
### trying thm 'radd_real_const_eq'
|
agriesma@338
|
175 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
176 |
-1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
|
agriesma@338
|
177 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
178 |
-1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
|
agriesma@338
|
179 |
### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
|
agriesma@338
|
180 |
(-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
|
agriesma@338
|
181 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
agriesma@338
|
182 |
|
agriesma@338
|
183 |
28.8.02: ruleset besser zusammenstellen !!!
|
agriesma@338
|
184 |
*)
|
agriesma@338
|
185 |
val thm = num_str square_equation_left;
|
agriesma@338
|
186 |
val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
|
agriesma@338
|
187 |
val asm = asm union asm';
|
agriesma@338
|
188 |
val rls = Test_simplify;
|
agriesma@338
|
189 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
190 |
val rls = norm_equation;
|
agriesma@338
|
191 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
192 |
val rls = Test_simplify;
|
agriesma@338
|
193 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
194 |
val rls = isolate_bdv;
|
agriesma@338
|
195 |
val subst = [(str2term "bdv", str2term "x")];
|
agriesma@338
|
196 |
val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
|
agriesma@338
|
197 |
val rls = Test_simplify;
|
agriesma@338
|
198 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
agriesma@338
|
199 |
val t' = term2str t;
|
agriesma@338
|
200 |
if t' = "x = 4" then ()
|
agriesma@338
|
201 |
else raise error "root-equ.sml: new behav. in rewrite_ x+4";
|
agriesma@338
|
202 |
|
agriesma@338
|
203 |
" _________________ rewrite x=4_________________ ";
|
agriesma@338
|
204 |
" _________________ rewrite x=4_________________ ";
|
agriesma@338
|
205 |
" _________________ rewrite x=4_________________ ";
|
agriesma@338
|
206 |
(*
|
agriesma@338
|
207 |
rewrite thy' "tless_true" "tval_rls" true (num_str rbinom_power_2) ct;
|
agriesma@338
|
208 |
atomty thy ((#prop o rep_thm) (!tthm));
|
agriesma@338
|
209 |
atomty thy (term_of (!tct));
|
agriesma@338
|
210 |
*)
|
agriesma@338
|
211 |
val thy' = "Test.thy";
|
agriesma@338
|
212 |
val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
agriesma@338
|
213 |
(*1*)val thm = ("square_equation_left","");
|
agriesma@338
|
214 |
val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
agriesma@338
|
215 |
"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
|
agriesma@338
|
216 |
(*2*)val rls = "Test_simplify";
|
agriesma@338
|
217 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
218 |
"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
|
agriesma@338
|
219 |
(*3*)val rls = "rearrange_assoc";
|
agriesma@338
|
220 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
221 |
"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
|
agriesma@338
|
222 |
(*4*)val rls = "isolate_root";
|
agriesma@338
|
223 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
224 |
"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
|
agriesma@338
|
225 |
(*5*)val rls = "Test_simplify";
|
agriesma@338
|
226 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
227 |
"sqrt (x ^^^ 2 + 5 * x) = 2 + x";
|
agriesma@338
|
228 |
(*6*)val thm = ("square_equation_left","");
|
agriesma@338
|
229 |
val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
agriesma@338
|
230 |
val asm = asm union asm';
|
agriesma@338
|
231 |
"x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
|
agriesma@338
|
232 |
(*7*)val rls = "Test_simplify";
|
agriesma@338
|
233 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
234 |
"x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
|
agriesma@338
|
235 |
(*8*)val rls = "norm_equation";
|
agriesma@338
|
236 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
237 |
"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
|
agriesma@338
|
238 |
(*9*)val rls = "Test_simplify";
|
agriesma@338
|
239 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
240 |
"-4 + x = 0";
|
agriesma@338
|
241 |
(*10*)val rls = "isolate_bdv";
|
agriesma@338
|
242 |
val (ct,_) = the (rewrite_set_inst thy' false
|
agriesma@338
|
243 |
[("bdv","x")] rls ct);
|
agriesma@338
|
244 |
"x = 0 + -1 * -4";
|
agriesma@338
|
245 |
(*11*)val rls = "Test_simplify";
|
agriesma@338
|
246 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
247 |
if ct="x = 4" then () else raise error "new behaviour in test-example";
|
agriesma@338
|
248 |
|
agriesma@338
|
249 |
|
agriesma@338
|
250 |
|
agriesma@338
|
251 |
|
agriesma@338
|
252 |
" _________________ rewrite + cappend _________________ ";
|
agriesma@338
|
253 |
" _________________ rewrite + cappend _________________ ";
|
agriesma@338
|
254 |
" _________________ rewrite + cappend _________________ ";
|
agriesma@338
|
255 |
val thy' = "Test.thy";
|
agriesma@338
|
256 |
val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
agriesma@338
|
257 |
val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
|
agriesma@338
|
258 |
val oris = prep_ori ctl thy ((#ppc o get_pbt)
|
agriesma@338
|
259 |
["sqroot-test","univariate","equation","test"]);
|
agriesma@338
|
260 |
val loc = e_istate;
|
agriesma@338
|
261 |
val (pt,pos) = (e_ptree,[]);
|
agriesma@338
|
262 |
val (pt,_) = cappend_problem pt pos loc (oris,empty_spec);
|
agriesma@338
|
263 |
val pt = update_branch pt [] Transitive;
|
agriesma@338
|
264 |
(*
|
agriesma@338
|
265 |
val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
|
agriesma@338
|
266 |
*)
|
agriesma@338
|
267 |
(*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
|
agriesma@338
|
268 |
val pt = update_domID pt [] "Test";
|
agriesma@338
|
269 |
val pt = update_pblID pt [] ["Test",
|
agriesma@338
|
270 |
"equations","univariate","square-root"];
|
agriesma@338
|
271 |
val pt = update_metID pt [] ("Test","sqrt-equ-test");
|
agriesma@338
|
272 |
val pt = update_pbl pt [] [];
|
agriesma@338
|
273 |
val pt = update_met pt [] [];
|
agriesma@338
|
274 |
(*
|
agriesma@338
|
275 |
> get_obj g_spec pt [];
|
agriesma@338
|
276 |
val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec
|
agriesma@338
|
277 |
> val pt = update_domID pt [] "RatArith";
|
agriesma@338
|
278 |
> get_obj g_spec pt [];
|
agriesma@338
|
279 |
val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec
|
agriesma@338
|
280 |
> val pt = update_pblID pt [] ["RatArith",
|
agriesma@338
|
281 |
"equations","univariate","square-root"];
|
agriesma@338
|
282 |
> get_obj g_spec pt [];
|
agriesma@338
|
283 |
("RatArith",["RatArith","equations","univariate","square-root"],
|
agriesma@338
|
284 |
("e_domID","e_metID")) : spec
|
agriesma@338
|
285 |
> val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
|
agriesma@338
|
286 |
> get_obj g_spec pt [];
|
agriesma@338
|
287 |
("RatArith",["RatArith","equations","univariate","square-root"],
|
agriesma@338
|
288 |
("RatArith","sqrt-equ-test")) : spec
|
agriesma@338
|
289 |
*)
|
agriesma@338
|
290 |
|
agriesma@338
|
291 |
val pos = [1];
|
agriesma@338
|
292 |
val (pt,_) = cappend_parent pt pos loc ct (Mstep "repeat") Transitive;
|
agriesma@338
|
293 |
|
agriesma@338
|
294 |
val pos = (lev_on o lev_dn) pos;
|
agriesma@338
|
295 |
val thm = ("square_equation_left",""); val ctold = ct;
|
agriesma@338
|
296 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm ct);
|
agriesma@338
|
297 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep (fst thm)) ct Complete;
|
agriesma@338
|
298 |
val pt = union_asm pt [] (map (rpair []) asm);
|
agriesma@338
|
299 |
|
agriesma@338
|
300 |
val pos = lev_on pos;
|
agriesma@338
|
301 |
val rls = ("Test_simplify"); val ctold = ct;
|
agriesma@338
|
302 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
303 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
304 |
|
agriesma@338
|
305 |
val pos = lev_on pos;
|
agriesma@338
|
306 |
val rls = ("rearrange_assoc"); val ctold = ct;
|
agriesma@338
|
307 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
308 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
309 |
|
agriesma@338
|
310 |
val pos = lev_on pos;
|
agriesma@338
|
311 |
val rls = ("isolate_root"); val ctold = ct;
|
agriesma@338
|
312 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
313 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
314 |
|
agriesma@338
|
315 |
val pos = lev_on pos;
|
agriesma@338
|
316 |
val rls = ("Test_simplify"); val ctold = ct;
|
agriesma@338
|
317 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
318 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
319 |
|
agriesma@338
|
320 |
val pos = lev_on pos;
|
agriesma@338
|
321 |
val thm = ("square_equation_left",""); val ctold = ct;
|
agriesma@338
|
322 |
val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
agriesma@338
|
323 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
324 |
val pt = union_asm pt [] (map (rpair []) asm);
|
agriesma@338
|
325 |
|
agriesma@338
|
326 |
val pos = lev_up pos;
|
agriesma@338
|
327 |
val (pt,_) = append_result pt pos e_istate ct Complete;
|
agriesma@338
|
328 |
|
agriesma@338
|
329 |
val pos = lev_on pos;
|
agriesma@338
|
330 |
val rls = ("Test_simplify"); val ctold = ct;
|
agriesma@338
|
331 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
332 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
333 |
|
agriesma@338
|
334 |
val pos = lev_on pos;
|
agriesma@338
|
335 |
val rls = ("norm_equation"); val ctold = ct;
|
agriesma@338
|
336 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
337 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
338 |
|
agriesma@338
|
339 |
val pos = lev_on pos;
|
agriesma@338
|
340 |
val rls = ("Test_simplify"); val ctold = ct;
|
agriesma@338
|
341 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
342 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
343 |
|
agriesma@338
|
344 |
(* --- see comments in interface_ME_ISA/instantiate''
|
agriesma@338
|
345 |
val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");
|
agriesma@338
|
346 |
val (ct,_) = the (rewrite_set thy' false
|
agriesma@338
|
347 |
("#isolate_bdv",rlsdat') ct); *)
|
agriesma@338
|
348 |
val pos = lev_on pos;
|
agriesma@338
|
349 |
val rls = ("isolate_bdv"); val ctold = ct;
|
agriesma@338
|
350 |
val (ct,_) = the (rewrite_set_inst thy' false
|
agriesma@338
|
351 |
[("bdv","x")] rls ct);
|
agriesma@338
|
352 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
353 |
|
agriesma@338
|
354 |
val pos = lev_on pos;
|
agriesma@338
|
355 |
val rls = ("Test_simplify"); val ctold = ct;
|
agriesma@338
|
356 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
agriesma@338
|
357 |
val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete;
|
agriesma@338
|
358 |
|
agriesma@338
|
359 |
val pos = lev_up pos;
|
agriesma@338
|
360 |
val (pt,pos) = append_result pt pos e_istate ct Complete;
|
agriesma@338
|
361 |
get_obj g_asm pt [];
|
agriesma@338
|
362 |
|
agriesma@338
|
363 |
writeln (pr_ptree pr_short pt);
|
agriesma@338
|
364 |
(* aus src.24-11-99:
|
agriesma@338
|
365 |
. sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
|
agriesma@338
|
366 |
1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
|
agriesma@338
|
367 |
1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
|
agriesma@338
|
368 |
1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2
|
agriesma@338
|
369 |
1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
|
agriesma@338
|
370 |
1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2)
|
agriesma@338
|
371 |
1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
|
agriesma@338
|
372 |
1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x
|
agriesma@338
|
373 |
2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
|
agriesma@338
|
374 |
3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?!
|
agriesma@338
|
375 |
4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
|
agriesma@338
|
376 |
5. (-4) + x = (+0)
|
agriesma@338
|
377 |
6. x = (+0) + (-1) * (-4)
|
agriesma@338
|
378 |
*)
|
agriesma@338
|
379 |
|
agriesma@338
|
380 |
(*
|
agriesma@338
|
381 |
val t = (term_of o the o (parse thy)) "solutions (L::real set)";
|
agriesma@338
|
382 |
atomty thy t;
|
agriesma@338
|
383 |
*)
|
agriesma@338
|
384 |
|
agriesma@338
|
385 |
|
agriesma@338
|
386 |
(*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
|
agriesma@338
|
387 |
from thy ???, i.e. together with the *_simplify ?!!!? ----------
|
agriesma@338
|
388 |
" _________________ me Free_Solve _________________ ";
|
agriesma@338
|
389 |
" _________________ me Free_Solve _________________ ";
|
agriesma@338
|
390 |
" _________________ me Free_Solve _________________ ";
|
agriesma@338
|
391 |
val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
agriesma@338
|
392 |
"solveFor x","errorBound (eps=0)",
|
agriesma@338
|
393 |
"solutions L"(*,
|
agriesma@338
|
394 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
agriesma@338
|
395 |
val (dI',pI',mI') =
|
agriesma@338
|
396 |
("Test.thy",["sqroot-test","univariate","equation","test"],
|
agriesma@338
|
397 |
("Test.thy","sqrt-equ-test"));
|
agriesma@338
|
398 |
val p = e_pos'; val c = [];
|
agriesma@338
|
399 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
agriesma@338
|
400 |
|
agriesma@338
|
401 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
|
agriesma@338
|
402 |
(*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
|
agriesma@338
|
403 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
404 |
(* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
|
agriesma@338
|
405 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
406 |
(* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
|
agriesma@338
|
407 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
408 |
(* val nxt = ("Add_Find",Add_Find "solutions L"); *)
|
agriesma@338
|
409 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
410 |
(* val nxt = ("Specify_Domain",Specify_Domain "DiffAppl.thy");
|
agriesma@338
|
411 |
> get_obj g_spec pt (fst p);
|
agriesma@338
|
412 |
val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
|
agriesma@338
|
413 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
414 |
(*val nxt = ("Specify_Problem", Specify_Problem *)
|
agriesma@338
|
415 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
416 |
(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*)
|
agriesma@338
|
417 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
418 |
(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*)
|
agriesma@338
|
419 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
420 |
val nxt = ("Free_Solve",Free_Solve);
|
agriesma@338
|
421 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
agriesma@338
|
422 |
get_obj g_spec pt [];
|
agriesma@338
|
423 |
|
agriesma@338
|
424 |
"--- -2 ---";
|
agriesma@338
|
425 |
get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
|
agriesma@338
|
426 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
427 |
me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
|
agriesma@338
|
428 |
(* 15.4.
|
agriesma@338
|
429 |
"--- -1 ---";
|
agriesma@338
|
430 |
get_form ("Begin_Trans",Begin_Trans) p pt;
|
agriesma@338
|
431 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
432 |
me ("Begin_Trans",Begin_Trans) p [4] pt; *)
|
agriesma@338
|
433 |
|
agriesma@338
|
434 |
"--- 1 ---";
|
agriesma@338
|
435 |
get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
|
agriesma@338
|
436 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
437 |
me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;
|
agriesma@338
|
438 |
"--- 2 ---";
|
agriesma@338
|
439 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
|
agriesma@338
|
440 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
441 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
|
agriesma@338
|
442 |
"--- 3 ---";
|
agriesma@338
|
443 |
get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
|
agriesma@338
|
444 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
445 |
me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
|
agriesma@338
|
446 |
"--- 4 ---";
|
agriesma@338
|
447 |
get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
|
agriesma@338
|
448 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
449 |
me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
|
agriesma@338
|
450 |
"--- 5 ---";
|
agriesma@338
|
451 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
agriesma@338
|
452 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
453 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
|
agriesma@338
|
454 |
"--- 6 ---";
|
agriesma@338
|
455 |
get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
|
agriesma@338
|
456 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
457 |
me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;
|
agriesma@338
|
458 |
(* 15.4.
|
agriesma@338
|
459 |
"--- ---";
|
agriesma@338
|
460 |
get_form ("End_Trans",End_Trans) p pt;
|
agriesma@338
|
461 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
462 |
me ("End_Trans",End_Trans) p [11] pt; *)
|
agriesma@338
|
463 |
"--- 7 ---";
|
agriesma@338
|
464 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
agriesma@338
|
465 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
466 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
|
agriesma@338
|
467 |
"--- 8 ---";
|
agriesma@338
|
468 |
get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
|
agriesma@338
|
469 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
470 |
me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
|
agriesma@338
|
471 |
"--- 9 ---";
|
agriesma@338
|
472 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
agriesma@338
|
473 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
474 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
|
agriesma@338
|
475 |
"--- 10 ---.";
|
agriesma@338
|
476 |
get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt;
|
agriesma@338
|
477 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
478 |
me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt;
|
agriesma@338
|
479 |
"--- 11 ---";
|
agriesma@338
|
480 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
agriesma@338
|
481 |
val ((p,p_),_,f,nxt,_,pt)=
|
agriesma@338
|
482 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
|
agriesma@338
|
483 |
(* 5.4.00.: ---
|
agriesma@338
|
484 |
get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt;
|
agriesma@338
|
485 |
val (p,_,f,nxt,_,pt)=
|
agriesma@338
|
486 |
me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt;
|
agriesma@338
|
487 |
--- *)
|
agriesma@338
|
488 |
writeln (pr_ptree pr_short pt);
|
agriesma@338
|
489 |
writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
|
agriesma@338
|
490 |
*)
|
agriesma@338
|
491 |
|
agriesma@338
|
492 |
|
agriesma@338
|
493 |
" _________________ me + msteps input _________________ ";
|
agriesma@338
|
494 |
" _________________ me + msteps input _________________ ";
|
agriesma@338
|
495 |
" _________________ me + msteps input _________________ ";
|
agriesma@338
|
496 |
val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
agriesma@338
|
497 |
"solveFor x","errorBound (eps=0)",
|
agriesma@338
|
498 |
"solutions L"];
|
agriesma@338
|
499 |
val (dI',pI',mI') =
|
agriesma@338
|
500 |
("Test.thy",["sqroot-test","univariate","equation","test"],
|
agriesma@338
|
501 |
("Test.thy","sqrt-equ-test"));
|
agriesma@338
|
502 |
val p = e_pos'; val c = [];
|
agriesma@338
|
503 |
"--- s1 ---";
|
agriesma@338
|
504 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
agriesma@338
|
505 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
|
agriesma@338
|
506 |
"--- s2 ---";
|
agriesma@338
|
507 |
val nxt = ("Add_Given",
|
agriesma@338
|
508 |
Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
|
agriesma@338
|
509 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
510 |
"--- s3 ---";
|
agriesma@338
|
511 |
val nxt = ("Add_Given",Add_Given "solveFor x");
|
agriesma@338
|
512 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
513 |
"--- s4 ---";
|
agriesma@338
|
514 |
val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
|
agriesma@338
|
515 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
516 |
"--- s5 ---";
|
agriesma@338
|
517 |
val nxt = ("Add_Find",Add_Find "solutions L");
|
agriesma@338
|
518 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
519 |
"--- s6 ---";
|
agriesma@338
|
520 |
val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
|
agriesma@338
|
521 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
522 |
"--- s7 ---";
|
agriesma@338
|
523 |
val nxt = ("Specify_Problem",
|
agriesma@338
|
524 |
Specify_Problem ["sqroot-test","univariate","equation","test"]);
|
agriesma@338
|
525 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
526 |
"--- s8 ---";
|
agriesma@338
|
527 |
val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));
|
agriesma@338
|
528 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
529 |
"--- s9 ---";
|
agriesma@338
|
530 |
val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));
|
agriesma@338
|
531 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
532 |
"--- 1 ---";
|
agriesma@338
|
533 |
val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
|
agriesma@338
|
534 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
535 |
|
agriesma@338
|
536 |
(*me------------
|
agriesma@338
|
537 |
val (mI,m) = nxt; val pos' as (p,p_) = p;
|
agriesma@338
|
538 |
|
agriesma@338
|
539 |
val Appl m = applicable_in (p,p_) pt m;
|
agriesma@338
|
540 |
(*solve*)
|
agriesma@338
|
541 |
val pp = par_pblobj pt p;
|
agriesma@338
|
542 |
val metID = get_obj g_metID pt pp;
|
agriesma@338
|
543 |
val sc = (#scr o get_met) metID;
|
agriesma@338
|
544 |
val is = get_istate pt (p,p_);
|
agriesma@338
|
545 |
val thy' = get_obj g_domID pt pp;
|
agriesma@338
|
546 |
val thy = assoc_thy thy';
|
agriesma@338
|
547 |
val d = e_rls;
|
agriesma@338
|
548 |
val Steps [(m',f',pt',p',c',s')] =
|
agriesma@338
|
549 |
locate_gen thy' m (pt,(p,p_)) (sc,d) is;
|
agriesma@338
|
550 |
val is' = get_istate pt' p';
|
agriesma@338
|
551 |
next_tac thy' (pt'(*'*),p') sc is';
|
agriesma@338
|
552 |
|
agriesma@338
|
553 |
|
agriesma@338
|
554 |
|
agriesma@338
|
555 |
|
agriesma@338
|
556 |
val ttt = (term_of o the o (parse Test.thy))
|
agriesma@338
|
557 |
"Let (((While contains_root e_ Do\
|
agriesma@338
|
558 |
\Rewrite square_equation_left True @@\
|
agriesma@338
|
559 |
\Try (Rewrite_Set Test_simplify False) @@\
|
agriesma@338
|
560 |
\Try (Rewrite_Set rearrange_assoc False) @@\
|
agriesma@338
|
561 |
\Try (Rewrite_Set Test_simplify False)) @@\
|
agriesma@338
|
562 |
\Try (Rewrite_Set norm_equation False) @@\
|
agriesma@338
|
563 |
\Try (Rewrite_Set Test_simplify False) @@\
|
agriesma@338
|
564 |
\Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False @@\
|
agriesma@338
|
565 |
\Try (Rewrite_Set Test_simplify False))\
|
agriesma@338
|
566 |
\e_)";
|
agriesma@338
|
567 |
|
agriesma@338
|
568 |
-------------------------*)
|
agriesma@338
|
569 |
|
agriesma@338
|
570 |
|
agriesma@338
|
571 |
"--- 2 ---";
|
agriesma@338
|
572 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
573 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
574 |
"--- 3 ---";
|
agriesma@338
|
575 |
val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
|
agriesma@338
|
576 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
577 |
"--- 4 ---";
|
agriesma@338
|
578 |
val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
|
agriesma@338
|
579 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
580 |
"--- 5 ---";
|
agriesma@338
|
581 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
582 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
583 |
"--- 6 ---";
|
agriesma@338
|
584 |
val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
|
agriesma@338
|
585 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
586 |
"--- 7 ---";
|
agriesma@338
|
587 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
588 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
589 |
"--- 8<> ---";
|
agriesma@338
|
590 |
val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
|
agriesma@338
|
591 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
592 |
"--- 9<> ---";
|
agriesma@338
|
593 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
594 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
595 |
"--- 10<> ---";
|
agriesma@338
|
596 |
val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
|
agriesma@338
|
597 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
598 |
"--- 11<> ---.";
|
agriesma@338
|
599 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
600 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
601 |
"--- 12<> ---";
|
agriesma@338
|
602 |
val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));
|
agriesma@338
|
603 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
604 |
"--- 13<> ---";
|
agriesma@338
|
605 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
agriesma@338
|
606 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
agriesma@338
|
607 |
"--- 1<> ---";
|
agriesma@338
|
608 |
val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);
|
agriesma@338
|
609 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
agriesma@338
|
610 |
(* val nxt = ("End_Proof'",End_Proof');*)
|
agriesma@338
|
611 |
if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
|
agriesma@338
|
612 |
then raise error "me + msteps input: not finished correctly"
|
agriesma@338
|
613 |
else "root-equation, me + msteps input: OK";
|
agriesma@338
|
614 |
|
agriesma@338
|
615 |
writeln (pr_ptree pr_short pt);
|
agriesma@338
|
616 |
writeln("result: "^(get_obj g_result pt [])^
|
agriesma@338
|
617 |
"\n==============================================================");
|
agriesma@338
|
618 |
|
agriesma@338
|
619 |
|
agriesma@338
|
620 |
|