|
1 (* use"test-script.sml"; |
|
2 WN.13.3.00 |
|
3 *) |
|
4 |
|
5 " scripts: Variante 'funktional' "; |
|
6 "############## Make_fun_by_new_variable ##############"; |
|
7 "############## Make_fun_by_explicit ##############"; |
|
8 "################ Solve_root_equation #################"; |
|
9 "------- Notlocatable: Free_Solve -------"; |
|
10 |
|
11 " --- test100: nxt_tac order------------------------------------ "; |
|
12 " --- test100: order 1 3 1 2 ----------------------------------- "; |
|
13 " --- test200: nxt_tac order ------------------------------------- "; |
|
14 " --- test200: order 3 1 1 2 --------------------------------- "; |
|
15 |
|
16 " --- root-equation: nxt_tac order------------------------------ "; |
|
17 " --- root-equation: 1.norm_equation ------------------------------ "; |
|
18 (* --- test200: calculate -----------------------------------------*) |
|
19 " --- check_elementwise ------------------------------ "; |
|
20 |
|
21 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; |
|
22 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; |
|
23 |
|
24 |
|
25 |
|
26 |
|
27 |
|
28 |
|
29 " #################################################### "; |
|
30 " scripts: Variante 'funktional' "; |
|
31 " #################################################### "; |
|
32 |
|
33 val c = (the o (parse DiffApp.thy)) |
|
34 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ |
|
35 \ (v_::real) (itv_::real set) (err_::bool) = \ |
|
36 \ (let e_ = (hd o (filter (Testvar m_))) rs_; \ |
|
37 \ t_ = (if 1 < Length rs_ \ |
|
38 \ then (SubProblem (Reals_,[make,function],(Isac_,no_met))\ |
|
39 \ [real_ m_, real_ v_, bool_list_ rs_])\ |
|
40 \ else (hd rs_)); \ |
|
41 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \ |
|
42 \ (DiffAppl_,maximum_on_interval))\ |
|
43 \ [bool_ t_, real_ v_, real_set_ itv_]\ |
|
44 \ in ((SubProblem (Reals_,[find_values,tool],(DiffAppl_,find_values)) \ |
|
45 \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \ |
|
46 \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))"; |
|
47 |
|
48 |
|
49 "######################################################"; |
|
50 "############## Make_fun_by_new_variable ##############"; |
|
51 "######################################################"; |
|
52 |
|
53 val sc = (the o (parse DiffApp.thy)) (*start interpretieren*) |
|
54 "Script Make_fun_by_new_variable (f_::real) (v_::real) \ |
|
55 \ (eqs_::bool list) = \ |
|
56 \(let h_ = (hd o (filter (Testvar m_))) eqs_; \ |
|
57 \ es_ = dropWhile (ident h_) eqs_; \ |
|
58 \ vs_ = dropWhile (ident f_) (Var h_); \ |
|
59 \ v1_ = Nth 1 vs_; \ |
|
60 \ v2_ = Nth 2 vs_; \ |
|
61 \ e1_ = (hd o (filter (Testvar v1_))) es_; \ |
|
62 \ e2_ = (hd o (filter (Testvar v2_))) es_; \ |
|
63 \ (s_1::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\ |
|
64 \ [bool_ e1_, real_ v1_]);\ |
|
65 \ (s_2::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\ |
|
66 \ [bool_ e2_, real_ v2_])\ |
|
67 \in Substitute [(v_1, (Rhs o hd) s_1),(v_2, (Rhs o hd) s_2)] h_)"; |
|
68 val ags = map (term_of o the o (parse DiffApp.thy)) |
|
69 ["A::real", "alpha::real", |
|
70 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; |
|
71 val ll = []:loc_; |
|
72 (* problem with exn PTREE + eval_to ------------------------- |
|
73 "-------------- subproblem with empty formalizaton -------"; |
|
74 val (mI1,m1) = |
|
75 ("Subproblem", mstep2mstep' pt p |
|
76 (Subproblem (("Reals",["univar","equation","test"], |
|
77 (""(*"ANDERN !!!!!!!*),"no_met")),[]))); |
|
78 val (mI2,m2) = (mI1,m1); |
|
79 val (mI3,m3) = |
|
80 ("Substitute", mstep2mstep' pt p |
|
81 (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); |
|
82 "------- same_tacpbl + eval_to -------"; |
|
83 val Some(l1,t1) = same_tacpbl sc ll (mI1,m1); |
|
84 loc_2str l1; |
|
85 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
|
86 Sign.string_of_term (sign_of DiffApp.thy) t1; |
|
87 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) |
|
88 |
|
89 val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2); |
|
90 loc_2str l2; |
|
91 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
|
92 Sign.string_of_term (sign_of DiffApp.thy) t2; |
|
93 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) |
|
94 |
|
95 val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3); |
|
96 loc_2str l3; |
|
97 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) |
|
98 Sign.string_of_term (sign_of DiffApp.thy) t3; |
|
99 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) |
|
100 |
|
101 |
|
102 "------- eq_tacIDs + eq_consts + eval_args -------"; |
|
103 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; |
|
104 val eq_cons = filter (eq_consts m) eq_ids; |
|
105 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; |
|
106 "------- locate -------"; |
|
107 |
|
108 |
|
109 "-------------- subproblem with formalizaton -------"; |
|
110 val (mI,m) = |
|
111 ("Subproblem", mstep2mstep' pt [] |
|
112 (Subproblem (("Reals",["univar","equation","test"], |
|
113 (""(*"ANDERN !!!!!!!*),"no_met")), |
|
114 ["a//#2=r*sin alpha","a"]))); |
|
115 "------- same_tacpbl + eval_to -------"; |
|
116 |
|
117 |
|
118 "------- eq_tacIDs + eq_consts + eval_args -------"; |
|
119 val eq_ids = eq_tacIDs [] sc (mI,m) []; |
|
120 val eq_cons = filter (eq_consts m) eq_ids; |
|
121 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; |
|
122 |
|
123 |
|
124 "------- locate -------"; |
|
125 -------------------------------------------------------*) |
|
126 (* use"ME/script.sml"; |
|
127 use"test-script.sml"; |
|
128 *) |
|
129 |
|
130 |
|
131 |
|
132 (*#####################################################*) |
|
133 (*#####################################################*) |
|
134 "############## Make_fun_by_explicit ##############"; |
|
135 val c = (the o (parse DiffApp.thy)) |
|
136 "Script Make_fun_by_explicit (f_::real) (v_::real) \ |
|
137 \ (eqs_::bool list) = \ |
|
138 \ (let h_ = (hd o (filter (Testvar m_))) eqs_; \ |
|
139 \ e1_ = hd (dropWhile (ident h_) eqs_); \ |
|
140 \ vs_ = dropWhile (ident f_) (Var h_); \ |
|
141 \ v1_ = hd (dropWhile (ident v_) vs_); \ |
|
142 \ (s1::bool list) = (SubProblem (Reals_, [univar,equation],(Isac_,no_met))\ |
|
143 \ [bool_ e1_, real_ v1_])\ |
|
144 \ in Substitute [(v_1, (Rhs o hd) s_1)] h_)"; |
|
145 |
|
146 |
|
147 (*#####################################################--------11.5.02 |
|
148 "################ Solve_root_equation #################"; |
|
149 (*#####################################################*) |
|
150 val sc = (term_of o the o (parse Test.thy)) |
|
151 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ |
|
152 \ (let e_ = Rewrite square_equation_left True eq_; \ |
|
153 \ e_ = Rewrite_Set Test_simplify False e_; \ |
|
154 \ e_ = Rewrite_Set rearrange_assoc False e_; \ |
|
155 \ e_ = Rewrite_Set isolate_root False e_; \ |
|
156 \ e_ = Rewrite_Set Test_simplify False e_; \ |
|
157 |
|
158 \ e_ = Rewrite square_equation_left True e_; \ |
|
159 \ e_ = Rewrite_Set Test_simplify False e_; \ |
|
160 |
|
161 \ e_ = Rewrite_Set norm_equation False e_; \ |
|
162 \ e_ = Rewrite_Set Test_simplify False e_; \ |
|
163 \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ |
|
164 \ e_ = Rewrite_Set Test_simplify False e_ \ |
|
165 \ in [e_::bool])"; |
|
166 val ags = map (term_of o the o (parse Test.thy)) |
|
167 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; |
|
168 val fmz = |
|
169 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
|
170 "solveFor x","errorBound (eps = #0)","solutions v_i_"]; |
|
171 ----------------------------------------------------------------11.5.02...*) |
|
172 |
|
173 |
|
174 (*#####################################################*) |
|
175 "------- Notlocatable: Free_Solve -------"; |
|
176 "------- Notlocatable: Free_Solve -------"; |
|
177 "------- Notlocatable: Free_Solve -------"; |
|
178 val fmz = []; |
|
179 val (dI',pI',mI') = |
|
180 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
181 ("Test.thy","sqrt-equ-test")); |
|
182 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
183 val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree; |
|
184 val nxt = |
|
185 ("Add_Given", |
|
186 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); |
|
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
188 val nxt = ("Add_Given",Add_Given "solveFor x"); |
|
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
190 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)"); |
|
191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
192 val nxt = ("Add_Find",Add_Find "solutions v_i_"); |
|
193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
194 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
196 val nxt = |
|
197 ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]); |
|
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
199 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); |
|
200 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
201 |
|
202 "--- -1 ---"; |
|
203 val nxt = ("Free_Solve",Free_Solve); |
|
204 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
205 |
|
206 "--- 0 ---"; |
|
207 val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)"); |
|
208 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
209 (*me ("Begin_Trans" ////*) |
|
210 |
|
211 "--- 1 ---"; |
|
212 val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")); |
|
213 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
214 |
|
215 "--- 2 ---"; |
|
216 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
217 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
218 |
|
219 "--- 3 ---"; |
|
220 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); |
|
221 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
222 if f = Form' |
|
223 (FormKF |
|
224 (~1,EdUndef,1,Nundef, |
|
225 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) |
|
226 then () else raise error "behaviour in root-expl. Free_Solve changed"; |
|
227 writeln (pr_ptree pr_short pt); |
|
228 |
|
229 |
|
230 |
|
231 val d = e_rls; |
|
232 |
|
233 " --- test100: nxt_tac order------------------------------------ "; |
|
234 " --- test100: nxt_tac order------------------------------------ "; |
|
235 |
|
236 val scr as (Script sc) = Script (((inst_abs Test.thy) |
|
237 o term_of o the o (parse thy)) |
|
238 "Script Testeq (e_::bool) = \ |
|
239 \(While (contains_root e_) Do \ |
|
240 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
|
241 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
|
242 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
|
243 \ e_ "); |
|
244 atomty thy sc; |
|
245 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
246 ("Test.thy","sqrt-equ-test")); |
|
247 val p = e_pos'; val c = []; |
|
248 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
249 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
250 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
251 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
252 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
253 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
254 val p = ([1],Res):pos'; |
|
255 val eq_ = (term_of o the o (parse thy))"e_::bool"; |
|
256 |
|
257 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
|
258 val ve0_= (term_of o the o (parse thy)) ct; |
|
259 val ets0=[([],(Mstep'(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
|
260 e_term,e_term,Safe)), |
|
261 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
262 val l0 = []; |
|
263 " --------------- 1. ---------------------------------------------"; |
|
264 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; |
|
265 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
|
266 |
|
267 |
|
268 (*-----------11.5.02: ets disabolished ------------------ |
|
269 |
|
270 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; |
|
271 (*val l = [R,R,L,R,R,R] : loc_ |
|
272 val m' = Rewrite'...("rroot_square_inv",..(sqrt (sqrt (sqrt a)).. |
|
273 -> sqrt (sqrt a)*) |
|
274 |
|
275 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = |
|
276 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; |
|
277 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; |
|
278 writeln(ets2str ets1); |
|
279 " --------------- 2. ---------------------------------------------"; |
|
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
|
281 |
|
282 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
283 (*val l = [R,R,L,R,R,R] : loc_ |
|
284 val m' = Rewrite'...("rroot_square_inv",..,sqrt (sqrt a).. |
|
285 -> #0+ sqrt a =#0*) |
|
286 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
287 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
288 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
289 writeln(ets2str ets2); |
|
290 " --------------- 3. ---------------------------------------------"; |
|
291 val Appl m'=applicable_in p pt (Rewrite("radd_0","")); |
|
292 |
|
293 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
294 (*val l = [R,R,R,D,R,D,R,R] : loc_ |
|
295 val m' = Rewrite'...("radd_0","")..(#0 + sqrt a = #0)..-> sqrt a = #0*) |
|
296 |
|
297 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = |
|
298 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; |
|
299 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; |
|
300 writeln(ets2str ets3); |
|
301 " --------------- 4. ---------------------------------------------"; |
|
302 val Appl m'=applicable_in p pt (Rewrite("square_equation_left","")); |
|
303 |
|
304 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; |
|
305 (*val l = [R,R,R,D,L,R,R,R] : loc_ |
|
306 val m' = Rewrite'...("square_equation_left"..(sqrt a = #0)..a = #0^#2*) |
|
307 |
|
308 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = |
|
309 (*=====*) locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; |
|
310 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; |
|
311 |
|
312 " --------------- 5. ---------------------------------------------"; |
|
313 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; |
|
314 |
|
315 writeln (pr_ptree pr_short pt);writeln("result: "^res^ |
|
316 "\n==================================================================="); |
|
317 "--- test100 nxt_tac order: finished correctly ---------------"; |
|
318 "--- test100 nxt_tac order: finished correctly ---------------"; |
|
319 "--- test100 nxt_tac order: finished correctly ---------------"; |
|
320 |
|
321 |
|
322 |
|
323 |
|
324 " --- test100: order 1 3 1 2 ----------------------------------- "; |
|
325 " --- test100: order 1 3 1 2 ----------------------------------- "; |
|
326 val scr as (Script sc) = |
|
327 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
|
328 "Script Testeq (e_::bool) = \ |
|
329 \While (contains_root e_) Do \ |
|
330 \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \ |
|
331 \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \ |
|
332 \ in Try (Repeat (Rewrite radd_0 False e_))) "); |
|
333 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
334 ("Test.thy","sqrt-equ-test")); |
|
335 val p = e_pos'; val c = []; |
|
336 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
337 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
338 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
339 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
340 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
341 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
342 val p = ([1],Res):pos'; |
|
343 val eq_ = (term_of o the o (parse thy))"e_::bool"; |
|
344 |
|
345 val ct = "#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0"; |
|
346 val ve0_= (term_of o the o (parse thy)) ct; |
|
347 val ets0=[([],(Mstep'(Script.thy,"bS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
|
348 e_term,e_term,Safe)), |
|
349 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
350 val l0 = []; |
|
351 " --------------- 1. --- test100 order 1 3 1 2 --------------------"; |
|
352 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; |
|
353 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
|
354 |
|
355 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = |
|
356 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; |
|
357 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; |
|
358 writeln (ets2str ets1); |
|
359 " --------------- 2. --- test100 order 1 3 1 2 --------------------"; |
|
360 val Appl m'=applicable_in p pt (Rewrite("radd_0","")); |
|
361 val Rewrite'(_,_,_,_,("radd_0",""),f,(_,[])) = m'; |
|
362 Sign.string_of_term (sign_of (thy)) f; |
|
363 (*"#0 + sqrt (sqrt a) ^^^ #2 = #0" |
|
364 -> AssocWeak .. pt aus ass_up,ass_dn,assy _verworfen_.. nur letzte tac*) |
|
365 |
|
366 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
367 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
368 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
369 " --------------- 3. --- test100 order 1 3 1 2 --------------------"; |
|
370 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
|
371 |
|
372 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = |
|
373 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; |
|
374 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; |
|
375 " --------------- 4. --- test100 order 1 3 1 2 --------------------"; |
|
376 val Appl m'=applicable_in p pt (Rewrite("square_equation_left","")); |
|
377 |
|
378 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = |
|
379 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; |
|
380 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; |
|
381 if res="a = #0 ^^^ #2"then()else raise error "test100 order 1 3 1 2"; |
|
382 " --------------- 5. --- test100 order 1 3 1 2 --------------------"; |
|
383 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; |
|
384 writeln (pr_ptree pr_short pt);writeln("result: "^res^ |
|
385 "\n==================================================================="); |
|
386 "--- test100 order 1 3 1 2: finished correctly --------------"; |
|
387 "--- test100 order 1 3 1 2: finished correctly --------------"; |
|
388 |
|
389 |
|
390 |
|
391 |
|
392 " --- test200: nxt_tac order ------------------------------------- "; |
|
393 " --- test200: nxt_tac order ------------------------------------- "; |
|
394 |
|
395 val scr as (Script sc) = |
|
396 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
|
397 "Script Testterm (g_::real) = \ |
|
398 \Repeat \ |
|
399 \ ((Repeat (Rewrite rmult_1 False g_)) Or \ |
|
400 \ (Repeat (Rewrite rmult_0 False g_)) Or \ |
|
401 \ (Repeat (Rewrite radd_0 False g_))) "); |
|
402 val d = e_rls; (*domain-rls for assod*) |
|
403 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
404 ("Test.thy","sqrt-equ-test")); |
|
405 val p = e_pos'; val c = []; |
|
406 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
407 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
408 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
409 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
410 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
411 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
412 val p = ([1],Res):pos'; |
|
413 val g_ = (term_of o the o (parse thy)) "g_"; |
|
414 |
|
415 val ct = "(#0+#0)*(#1*(#1*a))"; |
|
416 val vg0_= (term_of o the o (parse thy)) ct; |
|
417 val ets0 = [([],(Mstep'(Script.thy,"sB","",""), [(g_,vg0_)], [(g_,vg0_)], |
|
418 e_term, e_term,Safe)), |
|
419 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
420 val l0 = []; |
|
421 " --------------- 1. ---------------------------------------------"; |
|
422 val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete; |
|
423 val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); |
|
424 |
|
425 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; |
|
426 (*val l = [R,R,L,R,L,R,R] : loc_ |
|
427 val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*(#1*a)*) |
|
428 |
|
429 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = |
|
430 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; |
|
431 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; |
|
432 |
|
433 " --------------- 2. ---------------------------------------------"; |
|
434 val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); |
|
435 |
|
436 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
437 (*val l = [R,R,L,R,L,R,R] : loc_ |
|
438 val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*a*) |
|
439 |
|
440 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
441 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
442 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
443 |
|
444 " --------------- 3. ---------------------------------------------"; |
|
445 val Appl m'=applicable_in p pt (Rewrite("radd_0","")); |
|
446 |
|
447 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
448 (*val l = [R,R,R,R] : loc_ |
|
449 val m' = Rewrite'...("radd_0","") (#0+#0)*a *) |
|
450 |
|
451 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = |
|
452 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; |
|
453 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; |
|
454 |
|
455 " --------------- 4. ---------------------------------------------"; |
|
456 val Appl m'=applicable_in p pt (Rewrite("rmult_0","")); |
|
457 |
|
458 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; |
|
459 (*al l = [R,R,L,R,R,R] : loc_ |
|
460 val m' = Rewrite'...("rmult_0","") #0*a *) |
|
461 |
|
462 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = |
|
463 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; |
|
464 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; |
|
465 |
|
466 " --------------- 5. ---------------------------------------------"; |
|
467 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; |
|
468 (*al l = [R,R,L,R,R,R] : loc_ |
|
469 val m' = Rewrite'...("rmult_0","") #0*a *) |
|
470 writeln (pr_ptree pr_short pt);writeln("result: "^res^ |
|
471 "\n==================================================================="); |
|
472 "--- test200 nxt_tac order: finished correctly ---------------"; |
|
473 "--- test200 nxt_tac order: finished correctly ---------------"; |
|
474 |
|
475 |
|
476 |
|
477 |
|
478 " --- test200: order 3 1 1 2 --------------------------------- "; |
|
479 " --- test200: order 3 1 1 2 --------------------------------- "; |
|
480 val p = e_pos'; val c = []; |
|
481 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
482 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
483 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
484 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
485 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
486 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
487 val p = ([1],Res):pos'; |
|
488 val g_ = (term_of o the o (parse thy)) "g_"; |
|
489 |
|
490 val ct = "(#0+#0)*(#1*(#1*a))"; |
|
491 val vg0_= (term_of o the o (parse thy)) ct; |
|
492 val ets0 = [([],(Mstep'(Script.thy,"sB","",""),[(g_,vg0_)],[(g_,vg0_)], |
|
493 e_term,e_term,Safe)), |
|
494 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
495 val l0 = []; |
|
496 " --------------- 1. --- test200: order 3 1 1 2 -----------------"; |
|
497 val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete; |
|
498 val Appl m'=applicable_in p pt (Rewrite("radd_0","")); |
|
499 |
|
500 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = |
|
501 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; |
|
502 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; |
|
503 |
|
504 " --------------- 2. --- test200: order 3 1 1 2 -----------------"; |
|
505 val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); |
|
506 |
|
507 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
508 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
509 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
510 if res="#0 * (#1 * a)"then()else raise error "error test200: order 3 1 1 2"; |
|
511 " --------------- 3. --- test200: order 3 1 1 2 -----------------"; |
|
512 val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); |
|
513 |
|
514 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = |
|
515 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; |
|
516 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; |
|
517 |
|
518 " --------------- 4. --- test200: order 3 1 1 2 -----------------"; |
|
519 val Appl m'=applicable_in p pt (Rewrite("rmult_0","")); |
|
520 |
|
521 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = |
|
522 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; |
|
523 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; |
|
524 |
|
525 if res="#0"then()else raise error "test200 order 3 1 1 2"; |
|
526 " --------------- 5. --- test200: order 3 1 1 2 -----------------"; |
|
527 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; |
|
528 writeln (pr_ptree pr_short pt);writeln("result: "^res^ |
|
529 "\n==================================================================="); |
|
530 "--- test200 order 3 1 1 2: finished correctly ---------------"; |
|
531 "--- test200 order 3 1 1 2: finished correctly ---------------"; |
|
532 |
|
533 |
|
534 ------------------------------------11.5.02: ets disabolished ---*) |
|
535 (* use"test-script-nxt_tac.sml"; |
|
536 *) |
|
537 |
|
538 (*---------11.5.02: |
|
539 ### Currently parsed expression could be extremely ambiguous. ---------- |
|
540 |
|
541 " --- root-equation: nxt_tac order------------------------------ "; |
|
542 " --- root-equation: nxt_tac order------------------------------ "; |
|
543 val scr as (Script sc) = |
|
544 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
|
545 "Script Solve_root_equation (e_::bool) (v_::real) (err_::bool) =\ |
|
546 \ (let e_ = \ |
|
547 \ (While (contains_root e_) Do \ |
|
548 \ (let \ |
|
549 \ e_ = Rewrite square_equation_left True e_; \ |
|
550 \ e_ = Try (Rewrite_Set Test_simplify False e_); \ |
|
551 \ e_ = Try (Rewrite_Set rearrange_assoc False e_); \ |
|
552 \ e_ = Try (Rewrite_Set isolate_root False e_) \ |
|
553 \ in Try (Rewrite_Set Test_simplify False e_))); \ |
|
554 \ e_ = Try (Rewrite_Set norm_equation False e_); \ |
|
555 \ e_ = Try (Rewrite_Set Test_simplify False e_); \ |
|
556 \ e_ = Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False e_;\ |
|
557 \ e_ = Try (Rewrite_Set Test_simplify False e_) \ |
|
558 \ in [e_::bool])"); |
|
559 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
560 ("Test.thy","sqrt-equ-test")); |
|
561 val p = e_pos'; val c = []; |
|
562 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
563 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
564 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
565 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
566 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
567 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
568 val p = ([1],Frm):pos'; |
|
569 |
|
570 val bdv_ =(term_of o the o (parse thy))"v_::real"; |
|
571 val v_ =(term_of o the o (parse thy))"x::real"; |
|
572 val eq_ = (term_of o the o (parse thy))"e_::bool"; |
|
573 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)"; |
|
574 val ve0_= (term_of o the o (parse thy)) ct; |
|
575 val env= [(bdv_, v_), (eq_, ve0_)]; |
|
576 val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)), |
|
577 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
578 val l1 = []; |
|
579 " -------root-equation--- 1.--- nxt_tac-order----------------------"; |
|
580 val (pt,_) = cappend_form pt[1]e_istate ct; |
|
581 |
|
582 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
583 (*square_equation_left*) |
|
584 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
585 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
586 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
587 if res = "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2" |
|
588 then () else raise error "new behaviour in test-example"; |
|
589 writeln (pr_ptree pr_short pt); |
|
590 " -------root-equation--- 2.--- nxt_tac-order----------------------"; |
|
591 val ets1 = ets2; val l1 = l2; |
|
592 (* |
|
593 > val eee = (hd) ets2; |
|
594 > val (_,(_,_,ennv,_,rees,_)) = eee; |
|
595 > subst2str ennv; |
|
596 > Sign.string_of_term (sign_of ( thy)) rees; |
|
597 *) |
|
598 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
599 (*Test_simplify*) |
|
600 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
601 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
602 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
603 if res = "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))" |
|
604 then () else raise error "new behaviour in test-example"; |
|
605 writeln (pr_ptree pr_short pt); |
|
606 " -------root-equation--- 3.--- nxt_tac-order----------------------"; |
|
607 val ets1 = ets2; val l1 = l2; |
|
608 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
609 (*rearrange_assoc*) |
|
610 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
611 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
612 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
613 if res = "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)" |
|
614 then () else raise error "new behaviour in test-example"; |
|
615 writeln (pr_ptree pr_short pt); |
|
616 " -------root-equation--- 4.--- nxt_tac-order----------------------"; |
|
617 val ets1 = ets2; val l1 = l2; |
|
618 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
619 (*isolate_root*) |
|
620 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
621 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
622 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
623 if res = "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 * #2)" |
|
624 then () else raise error "new behaviour in test-example"; |
|
625 writeln (pr_ptree pr_short pt); |
|
626 " -------root-equation--- 5.--- nxt_tac-order----------------------"; |
|
627 val ets1 = ets2; val l1 = l2; |
|
628 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
629 (*Test_simplify*) |
|
630 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
631 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
632 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
633 if res = "sqrt (x ^^^ #2 + #5 * x) = #2 + x" |
|
634 then () else raise error "new behaviour in test-example"; |
|
635 writeln (pr_ptree pr_short pt); |
|
636 " -------root-equation--- 6.--- nxt_tac-order----------------------"; |
|
637 val ets1 = ets2; val l1 = l2; |
|
638 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
639 (*square_equation_left*) |
|
640 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
641 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
642 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
643 if res = "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2" |
|
644 then () else raise error "new behaviour in test-example"; |
|
645 writeln (pr_ptree pr_short pt); |
|
646 " -------root-equation--- 7.--- nxt_tac-order----------------------"; |
|
647 val ets1 = ets2; val l1 = l2; |
|
648 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
649 (*Test_simplify*) |
|
650 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
651 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
652 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
653 if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)" |
|
654 then () else raise error "new behaviour in test-example"; |
|
655 writeln (pr_ptree pr_short pt); |
|
656 " -------root-equation--- 8.--- nxt_tac-order----------------------"; |
|
657 val ets1 = ets2; val l1 = l2; |
|
658 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
659 (*rearrange_assoc ...<> test-root-equ.sml: norm_equation*) |
|
660 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
661 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
662 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
663 if res = "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x" |
|
664 (* "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0" |
|
665 ...<> test-root-equ.sml*) |
|
666 then () else raise error "new behaviour in test-example"; |
|
667 writeln (pr_ptree pr_short pt); |
|
668 " -------root-equation--- 9.--- nxt_tac-order----------------------"; |
|
669 val ets1 = ets2; val l1 = l2; |
|
670 (*> Sign.string_of_term (sign_of thy) (go l2 sc); |
|
671 val it = "Rewrite_Set rearrange_assoc False e_" : string*) |
|
672 |
|
673 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
674 (*Test_simplify*) |
|
675 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
676 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
677 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
678 if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)" |
|
679 then () else raise error "new behaviour in test-example"; |
|
680 writeln (pr_ptree pr_short pt); |
|
681 " -------root-equation--- 10.--- nxt_tac-order----------------------"; |
|
682 val ets1 = ets2; val l1 = l2; |
|
683 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
684 (*norm_equation*) |
|
685 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
686 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
687 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
688 if res = "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0" |
|
689 then () else raise error "new behaviour in test-example"; |
|
690 writeln (pr_ptree pr_short pt); |
|
691 " -------root-equation--- 11.--- nxt_tac-order----------------------"; |
|
692 val ets1 = ets2; val l1 = l2; |
|
693 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
694 (*Test_simplify*) |
|
695 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
696 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
697 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
698 if res = "#-4 + x = #0" |
|
699 then () else raise error "new behaviour in test-example"; |
|
700 writeln (pr_ptree pr_short pt); |
|
701 " -------root-equation--- 12.--- nxt_tac-order----------------------"; |
|
702 val ets1 = ets2; val l1 = l2; |
|
703 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
704 (*isolate_bdv*) |
|
705 (*> val eee = (last_elem o drop_last) ets2; |
|
706 > val (_,(mmm,_,ennv,_,rees,_)) = eee; |
|
707 val mmm = Rewrite_Set' |
|
708 ("Test.thy","erls",false,"Test_simplify",# $ # $ Free #,(# $ #,[])) |
|
709 > writeln(subst2str ennv); |
|
710 ["(e_, x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0)"] |
|
711 > Sign.string_of_term (sign_of ( thy)) rees; |
|
712 val it = "#-4 + x = #0" : string*) |
|
713 |
|
714 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
715 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
716 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
717 if res = "x = #0 + #-1 * #-4" |
|
718 then () else raise error "new behaviour in test-example"; |
|
719 writeln (pr_ptree pr_short pt); |
|
720 " -------root-equation--- 13.--- nxt_tac-order----------------------"; |
|
721 val ets1 = ets2; val l1 = l2; |
|
722 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
723 (*Test_simplify*) |
|
724 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
725 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
726 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
727 if res = "x = #4" |
|
728 then () else raise error "new behaviour in test-example"; |
|
729 writeln (pr_ptree pr_short pt); |
|
730 " -------root-equation--- 14.--- nxt_tac-order----------------------"; |
|
731 val ets1 = ets2; val l1 = l2; |
|
732 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
733 |
|
734 writeln (pr_ptree pr_short pt); |
|
735 writeln("result: "^res^"\n==================================================================="); |
|
736 " --- root-equation: nxt_tac order .. finised correctly --------- "; |
|
737 " --- root-equation: nxt_tac order .. finised correctly --------- "; |
|
738 |
|
739 |
|
740 -------------------------------------11.5.02-----*) |
|
741 (*-----------------------------------11.5.02 ets disabolished ------- |
|
742 |
|
743 " --- root-equation: 1.norm_equation ------------------------------ "; |
|
744 " --- root-equation: 1.norm_equation ------------------------------ "; |
|
745 val p = e_pos'; val c = []; |
|
746 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
747 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
748 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
749 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
750 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
751 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
752 val p = ([1],Frm):pos'; |
|
753 val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)), |
|
754 user_interrupt]:ets; |
|
755 " -------root-equation--- 1.--- 1.norm_equation----------------------"; |
|
756 val (pt,_) = cappend_form pt[1]e_istate ct; |
|
757 val Appl m'= applicable_in p pt (Rewrite_Set "norm_equation"); |
|
758 |
|
759 val l1 = (fst o last_elem o drop_last) ets1; |
|
760 (*val l1 = [R,L,R,R,L,R];//////////////test-root_equ, me 11.10.00*) |
|
761 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
762 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
763 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
764 if res = "sqrt (#9 + #4 * x) + #-1 * (sqrt x + sqrt (#5 + x)) = #0" |
|
765 then () else raise error "new behaviour in test-example"; |
|
766 |
|
767 val l2 = (fst o last_elem o drop_last) ets2; |
|
768 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
769 val ets1 = ets2; |
|
770 " -------root-equation--- 2.--- 1.norm_equation----------------------"; |
|
771 (*m'=Rewrite_Set'...,"Test_simplify" *) |
|
772 val l1 = (fst o last_elem o drop_last) ets1; |
|
773 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
774 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
775 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
776 if res = "#-1 * sqrt x + (#-1 * sqrt (#5 + x) + sqrt (#9 + #4 * x)) = #0" |
|
777 then () else raise error "new behaviour in test-example"; |
|
778 |
|
779 val Notappl _ = |
|
780 applicable_in p pt (Rewrite_Set_Inst(["(bdv,v_)"],"isolate_bdv")); |
|
781 val Notappl _ = applicable_in p pt (Rewrite_Set "Test_simplify"); |
|
782 |
|
783 val l2 = (fst o last_elem o drop_last) ets2; |
|
784 val Helpless = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
785 (* ~~~~ because isolate_bdv goes without Try *) |
|
786 writeln (pr_ptree pr_short pt); |
|
787 val ets1 = ets2; |
|
788 " -------root-equation--- 3.--- 1.norm_equation----------------------"; |
|
789 val Appl m'= applicable_in p pt (Rewrite_Set "rearrange_assoc"); |
|
790 |
|
791 val l1 = (fst o last_elem o drop_last) ets1; |
|
792 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
793 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
794 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
795 |
|
796 val l2 = (fst o last_elem o drop_last) ets2; |
|
797 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
798 writeln (pr_ptree pr_short pt); |
|
799 val ets1 = ets2; |
|
800 " -------root-equation--- 4.--- 1.norm_equation----------------------"; |
|
801 (*m' = .. isolate_root*) |
|
802 val l1 = (fst o last_elem o drop_last) ets1; |
|
803 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
804 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
805 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
806 |
|
807 val l2 = (fst o last_elem o drop_last) ets2; |
|
808 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
809 writeln (pr_ptree pr_short pt); |
|
810 val ets1 = ets2; |
|
811 " -------root-equation--- 5.--- 1.norm_equation----------------------"; |
|
812 (*m' = .. Test_simplify*) |
|
813 val l1 = (fst o last_elem o drop_last) ets1; |
|
814 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
815 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
816 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
817 |
|
818 val l2 = (fst o last_elem o drop_last) ets2; |
|
819 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
820 writeln (pr_ptree pr_short pt); |
|
821 if res="sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)" then () |
|
822 else raise error "new behaviour in test-example"; |
|
823 |
|
824 -------------------------------------11.5.02-----*) |
|
825 |
|
826 |
|
827 (* use"test-script.sml"; |
|
828 *) |
|
829 |
|
830 |
|
831 |
|
832 |
|
833 |
|
834 |
|
835 |
|
836 (* --- test200: calculate ----------------------------------------- |
|
837 " --- test200: calculate -----------------------------------------"; |
|
838 val scr as (Script sc) = |
|
839 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
|
840 "Script Testterm (g_::real) = \ |
|
841 \Repeat (Calculate plus g_) "); |
|
842 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
843 ("Test.thy","sqrt-equ-test")); |
|
844 val p = e_pos'; val c = []; |
|
845 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
846 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
847 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
848 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
849 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
850 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
851 val p = ([1],Res):pos'; |
|
852 val g_ = (term_of o the o (parse thy)) "g_"; |
|
853 val vg_= (term_of o the o (parse thy)) "#1+#2"; |
|
854 val env = [(g_,vg_)]; |
|
855 |
|
856 val ets = []:ets; |
|
857 (* --------------- 1. ---------------------------------------------*) |
|
858 val (pt,_) = cappend_atomic pt [1] e_istate "" |
|
859 (Rewrite("test","")) "#1+#2" Complete; |
|
860 val Appl m'=applicable_in p pt (Calculate "plus"); |
|
861 |
|
862 val NextStep(l,m') = nxt_tac "Test.thy" (pt,p) scr ets l; |
|
863 (*val l = [R,R,R,R] : loc_ |
|
864 val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*) |
|
865 |
|
866 val ets = (l,mstep'2etac m')::ets; |
|
867 (* --------------- 2. ---------------------------------------------*) |
|
868 val (pt,_) = cappend_atomic pt [1] e_istate "" |
|
869 (Rewrite("test","")) "#3" Complete; |
|
870 |
|
871 val Helpless = nxt_tac "Test.thy" (pt,p) scr ets l; |
|
872 (*val l = [R,R,R,R] : loc_ |
|
873 val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*) |
|
874 ---*) |
|
875 |
|
876 |
|
877 (* --- test200: Test_simplify ----------------------------------- |
|
878 |
|
879 val scr as (Script sc) = |
|
880 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
|
881 "Script Testterm (g_::real) = \ |
|
882 \Repeat \ |
|
883 \ ((Repeat (Rewrite radd_mult_distrib2 False g_)) Or \ |
|
884 \ (Repeat (Rewrite rdistr_right_assoc False g_)) Or \ |
|
885 \ (Repeat (Rewrite rdistr_right_assoc_p False g_)) Or \ |
|
886 \ (Repeat (Rewrite rdistr_div_right False g_)) Or \ |
|
887 \ (Repeat (Rewrite rbinom_power_2 False g_)) Or \ |
|
888 \ (Repeat (Rewrite radd_commute False g_)) Or \ |
|
889 \ (Repeat (Rewrite radd_left_commute False g_)) Or \ |
|
890 \ (Repeat (Rewrite radd_assoc False g_)) Or \ |
|
891 \ (Repeat (Rewrite rmult_commute False g_)) Or \ |
|
892 \ (Repeat (Rewrite rmult_left_commute False g_)) Or \ |
|
893 \ (Repeat (Rewrite rmult_assoc False g_)) Or \ |
|
894 \ (Repeat (Rewrite radd_real_const_eq False g_)) Or \ |
|
895 \ (Repeat (Rewrite radd_real_const False g_)) Or \ |
|
896 \ (Repeat (Calculate plus g_)) Or \ |
|
897 \ (Repeat (Calculate times g_)) Or \ |
|
898 \ (Repeat (Rewrite rcollect_right False g_)) Or \ |
|
899 \ (Repeat (Rewrite rcollect_one_left False g_)) Or \ |
|
900 \ (Repeat (Rewrite rcollect_one_left_assoc False g_)) Or \ |
|
901 \ (Repeat (Rewrite rcollect_one_left_assoc_p False g_))) "); |
|
902 ---*) |
|
903 writeln |
|
904 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
|
905 \ (Repeat (Calculate cancel g_)) Or \n\ |
|
906 \ (Repeat (Calculate pow g_)) Or \n\ |
|
907 \%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\ |
|
908 \%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set"; |
|
909 |
|
910 |
|
911 (*-------------------------------------11.5.02 ets disablished ------- |
|
912 |
|
913 " --- check_elementwise ------------------------------ "; |
|
914 " --- check_elementwise ------------------------------ "; |
|
915 val d = e_rls; |
|
916 val scr as (Script sc) = Script (((inst_abs Test.thy) |
|
917 o term_of o the o (parse thy)) |
|
918 "Script Testchk (e_::bool) (v_::real) = \ |
|
919 \ (let e_ = Try (Rewrite_Set Test_simplify False e_); \ |
|
920 \ (L_::real list) = Mstep subproblem_equation_dummy; \ |
|
921 \ L_ = Mstep solve_equation_dummy \ |
|
922 \ in Check_elementwise L_ {(v_::real). Assumptions})"); |
|
923 val (dI',pI',mI') = ("Test.thy",e_pblID, |
|
924 ("Test.thy","sqrt-equ-test")); |
|
925 val p = e_pos'; val c = []; |
|
926 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
|
927 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
928 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
929 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
930 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) |
|
931 val (p,_,_,_,_,pt) = me nxt p c pt; |
|
932 val pt = union_asm pt [] [("#0 <= sqrt x + sqrt (#5 + x)",[11]), |
|
933 ("#0 <= #9 + #4 * x",[22]), |
|
934 ("#0 <= x ^^^ #2 + #5 * x",[33]), |
|
935 ("#0 <= #2 + x",[44])]; |
|
936 val p = ([1],Res):pos'; |
|
937 val eq_ = (term_of o the o (parse thy))"e_::bool"; |
|
938 val ct = "x=#1+#3"; |
|
939 val ve0_= (term_of o the o (parse thy)) ct; |
|
940 val v_ = (term_of o the o (parse thy))"v_::real"; |
|
941 val xx = (term_of o the o (parse thy))"x::real"; |
|
942 val env0= [(eq_,ve0_),(v_,xx)]; |
|
943 |
|
944 val ets0=[([],(Mstep'(Script.thy,"BS","",""),env0,env0,e_term,e_term,Safe)), |
|
945 ([],(User', [], [], e_term, e_term,Sundef))]:ets; |
|
946 val l0 = []; |
|
947 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; |
|
948 " --------------- 1. ---------------------------------------------"; |
|
949 val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify"); |
|
950 |
|
951 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; |
|
952 (*val l1 = [R,L,R,R] : loc_*) |
|
953 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = |
|
954 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; |
|
955 (*val ets1 = [([R,L,R,R],(Rewrite_Set' #,[#],[#],Free #,# $ #,Safe)),..*) |
|
956 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; |
|
957 writeln(ets2str ets1); |
|
958 " --------------- 2. ---------------------------------------------"; |
|
959 val Appl m'=applicable_in p pt (Mstep "subproblem_equation_dummy"); |
|
960 |
|
961 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; |
|
962 (*val l2 = [R,R,D,L,R] : loc_|| val m' = Mstep' ("x = #4",...*) |
|
963 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = |
|
964 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; |
|
965 (*val ets2 =[([R,R,D,L,R],(Mstep' ..subpbl..,[#],[#],Const #,# $ #,Safe)),..*) |
|
966 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; |
|
967 writeln(ets2str ets2); |
|
968 " --------------- 3. ---------------------------------------------"; |
|
969 val Appl m'=applicable_in p pt (Mstep "solve_equation_dummy"); |
|
970 |
|
971 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; |
|
972 (*val l3 = [R,R,D,R,D,L,R] : loc_ |
|
973 val m' = Mstep'("subproblem_equation_dummy (x = #4)",..*) |
|
974 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = (*@@@*) |
|
975 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; |
|
976 (*val ets3 = [([R,R,D,R,D,L,R], (Mstep' (..,"solve_equation_dummy",..*) |
|
977 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; |
|
978 writeln(ets2str ets3); |
|
979 " --------------- 4. ---------------------------------------------"; |
|
980 val Appl (m' as (Check_elementwise' (consts,"Assumptions",consts'))) = |
|
981 applicable_in p pt (Check_elementwise "Assumptions"); |
|
982 |
|
983 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; |
|
984 (*val l4 = [R,R,D,R,D,R,D] : loc_ val m' = Check_elementwise' (Const (#,#) $ ...*) |
|
985 |
|
986 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = |
|
987 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; |
|
988 (*val ets4 = [([R,R,D,R,D,R,D], (Check_elementwise' (# $ #,"Assumptions",Const #),..*) |
|
989 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; |
|
990 " --------------- 5. ---------------------------------------------"; |
|
991 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; |
|
992 |
|
993 writeln (pr_ptree pr_short pt);writeln("result: "^res^ |
|
994 "\n==================================================================="); |
|
995 |
|
996 -------------------------------------11.5.02-----*) |