1 (* test calculation of values for function constants
2 (c) Walther Neuper 2000
4 use"../smltest/Scripts/calculate.sml";
8 " ================= calculate.sml: calculate_ ======================== ";
9 " ================= calculate.sml: aus script ======================== ";
10 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
11 "--------------(4): check bottom up: ---------------------------";
12 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
13 " ================= calculate.sml: calculate_ 2002 =================== ";
14 "----------- get_pair with 3 args --------------------------------";
15 " ================= eval_binop Float =================== ";
16 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
18 (* [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),
19 ("Nth",("Tools.Nth",fn)),
20 ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),
21 ("is_const",("Atools.is'_const",fn)),
22 ("le",("op <",fn)),("leq",("op <=",fn)),
23 ("ident",("Atools.ident",fn))] *)
25 val thy' = "Isac.thy";
27 " ================= calculate.sml: calculate_ ======================== ";
28 " ================= calculate.sml: calculate_ ======================== ";
29 " ================= calculate.sml: calculate_ ======================== ";
33 val t = (term_of o the o (parse thy)) "1+2";
34 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
36 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
37 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
38 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
39 Syntax.string_of_term (thy2ctxt thy) t;
40 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
41 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
42 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
43 Syntax.string_of_term (thy2ctxt thy) t;
44 (*val it = "(#12 // #3) ^^^ #2" : string*)
45 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
46 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
47 Syntax.string_of_term (thy2ctxt thy) t;
48 (*it = "#4 ^^^ #2" : string*)
49 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
50 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
51 Syntax.string_of_term (thy2ctxt thy) t;
52 (*val it = "#16" : string*)
53 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
56 " ================= calculate.sml: aus script ======================== ";
57 " ================= calculate.sml: aus script ======================== ";
58 " ================= calculate.sml: aus script ======================== ";
61 (prep_pbt Test.thy "pbl_ttest" [] e_pblID
66 (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID
67 (["calculate","test"],
68 [("#Given" ,["realTestGiven t_"]),
69 ("#Find" ,["realTestFind s_"])
71 e_rls, NONE, [["Test","test_calculate"]]));
74 (prep_met Test.thy "met_testcal" [] e_metID
75 (["Test","test_calculate"]:metID,
76 [("#Given" ,["realTestGiven t_"]),
77 ("#Find" ,["realTestFind s_"])
79 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
80 calc=[("plus" ,("op +" ,eval_binop "#add_")),
81 ("times" ,("op *" ,eval_binop "#mult_")),
82 ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
83 ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
84 crls=tval_rls, nrls=e_rls(*,
85 asm_rls=[],asm_thm=[]*)},
86 "Script STest_simplify (t_::real) = \
88 \ ((Try (Repeat (Calculate plus))) @@ \
89 \ (Try (Repeat (Calculate times))) @@ \
90 \ (Try (Repeat (Calculate divide_))) @@ \
91 \ (Try (Repeat (Calculate power_))))) t_"
94 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
96 ("Test.thy",["calculate","test"],["Test","test_calculate"]);
97 (*val p = e_pos'; val c = [];
98 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
99 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
100 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 (*nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 (*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
115 (*nxt = ("Calculate",Calculate "plus")*)
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
117 (*nxt = ("Calculate",Calculate "times")*)
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 (*nxt = ("Calculate",Calculate "divide_")*)
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 (*nxt = ("Calculate",Calculate "power_")*)
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 (*nxt = ("End_Proof'",End_Proof')*)
126 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
127 else raise error "calculate.sml: script test_calculate changed behaviour";
132 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
133 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
134 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
135 (*(1): 2nd Test_simplify didn't work:
137 "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
138 > val rls = ("Test_simplify");
139 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
140 val ct = "sqrt (x ^^^ 2 + -3 * x) =
141 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
142 ie. cancel does not work properly
144 val thy = "Test.thy";
146 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
147 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
148 val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
151 sqrt (x ^^^ 2 + -3 * x) =\
152 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
153 ............... does not work *)
155 (*--------------(2): does divide work in Test_simplify ?: ------*)
157 val t = (term_of o the o (parse thy)) "6 / 2";
158 val rls = Test_simplify;
159 val (t,_) = the (rewrite_set_ thy false rls t);
160 (*val t = Free ("3","RealDef.real") : term*)
162 val thy = "Test.thy";
164 val rls = "Test_simplify";
165 val (t,_) = the (rewrite_set thy false rls t);
166 (*val t = "3" : string
167 ....... works, thus: which rule in SqRoot_simplify works differently ?*)
170 (*--------------(3): is_const works ?: -------------------------------------*)
171 val t = (term_of o the o (parse Test.thy)) "2 is_const";
173 rewrite_set_ Test.thy false tval_rls t;
174 (*val it = SOME (Const ("True","bool"),[]) ... works*)
176 val t = str2term "2 * x is_const";
177 val SOME (str,t') = eval_const "" "" t Isac.thy;
183 "--------------(4): check bottom up: ---------------------------";
184 (*-------------- eval_cancel works: *)
187 val t = (term_of o the o (parse thy)) "(-4) / 2";
188 val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
191 (*-------------- but ... *)
192 val ct = "x + (-4) / 2";
193 val (ct,_) = the (rewrite_set thy' false rls ct);
195 (*-------------- while ... *)
197 val (ct,_) = the (rewrite_set thy' false rls ct);
200 (*--------------(5): reproduce (1) with simpler term: ------------*)
201 val thy = "Test.thy";
203 val (t,_) = the (rewrite_set thy false rls t);
204 (*val t = "4" ... works*)
206 val t = "(3+1+2*x)/2";
207 val (t,_) = the (rewrite_set thy false rls t);
208 (*val t = "2 + x" ... works*)
210 trace_rewrite:=true; (*3.6.03*)
211 val thy = "Test.thy";
212 val rls = "Test_simplify";
213 val t = "(3+(1+2*x))/2";
214 val (t,_) = the (rewrite_set thy false rls t);
215 (*val t = "2 + x" ... works: give up----------------------------------------*)
216 trace_rewrite:=false;
218 trace_rewrite:=true; (*3.6.03*)
220 val rls = Test_simplify;
221 val t = str2term "(3+(1+2*x))/2";
222 val SOME (t',asm) = rewrite_set_ thy false rls t;
224 (*val t = "2 + x" ... works: give up----------------------------------------*)
225 trace_rewrite:=false;
230 (*--- trace_rewrite before correction of ... --------------------
231 val ct = "(-3 + 2 * x + -1) / 2";
232 val (ct,_) = the (rewrite_set thy' false rls ct);
234 ### trying thm 'root_ge0_2'
235 ### rewrite_set_: x + (-1 + -3) / 2
236 ### trying thm 'radd_real_const_eq'
237 ### trying thm 'radd_real_const'
238 ### rewrite_set_: x + (-4) / 2
239 ### trying thm 'rcollect_right'
242 -------------------------------------while before Isabelle20002:
243 val ct = "(#-3 + #2 * x + #-1) // #2";
244 val (ct,_) = the (rewrite_set thy' false rls ct);
246 ### trying thm 'root_ge0_2'
247 ### rewrite_set_: x + (#-1 + #-3) // #2
248 ### trying thm 'radd_real_const_eq'
249 ### trying thm 'radd_real_const'
250 ### rewrite_set_: x + #-4 // #2
251 ### rewrite_set_: x + #-2
252 ### trying thm 'rcollect_right'
255 -----------------------------------------------------------------*)
258 toggle trace_rewrite;
259 (*===================*)
261 val thy' = "Test.thy";
262 val rls = "Test_simplify";
263 val ct = "x + (-1 + -3) / 2";
264 val (ct,_) = the (rewrite_set thy' false rls ct);
267 ### trying calc. 'cancel'
268 @@@ get_pair: binop, t = x + (-4) / 2
270 @@@ get_pair: t else -> NONE
271 @@@ get_pair: binop, t = (-4) / 2
273 @@@ get_pair: t -> NONE
274 @@@ get_pair: t1 -> NONE
275 @@@ get_calculation: NONE
276 ### trying calc. 'pow'
280 val thy' = "Test.thy";
281 val rls = "Test_simplify";
282 val ct = "x + (-4) / 2";
283 val (ct,_) = the (rewrite_set thy' false rls ct);
286 ### trying calc. 'cancel'
287 @@@ get_pair: binop, t = x + -4 / 2
289 @@@ get_pair: t else -> NONE
290 @@@ get_pair: binop, t = -4 / 2
292 @@@ get_calculation: SOME #cancel_-4_2
293 ### calc. to: x + (-2)
294 ### trying calc. 'cancel'
296 trace_rewrite:=false;
298 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
299 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
300 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
301 " ----------------- rewriting works ? -----------------------";
303 val prop = (#prop o rep_thm) real_divide_1;
306 *** Const ( Trueprop, bool => prop)
307 *** . Const ( op =, [real, real] => bool)
308 *** . . Const ( HOL.divide, [real, real] => real)
309 *** . . . Var ((x, 0), real)
310 *** . . . Const ( 1, real)
311 *** . . Var ((x, 0), real) *)
312 val prop' = (#prop o rep_thm o num_str) real_divide_1;
315 *** Const ( Trueprop, bool => prop)
316 *** . Const ( op =, [real, real] => bool)
317 *** . . Const ( HOL.divide, [real, real] => real)
318 *** . . . Var ((x, 0), real)
319 *** . . . Free ( 1, real) (*app_num_tr'*)
320 *** . . Var ((x, 0), real)*)
321 val t = (term_of o the o (parseold thy)) "aaa/1";
324 *** Const ( HOL.divide, ['a, 'a] => 'a)
325 *** . Free ( aaa, 'a)
326 *** . Free ( 1, 'a) *)
327 val t = (term_of o the o (parse thy)) "aaa/1";
330 *** Const ( HOL.divide, [real, real] => real)
331 *** . Free ( aaa, real)
332 *** . Free ( 1, real) *)
333 val thm = num_str @{thm divide_1};
334 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
335 (*val t = Free ("aaa","RealDef.real") : term*)
338 val prop = (#prop o rep_thm) realpow_eq_one;
341 *** Const ( Trueprop, bool => prop)
342 *** . Const ( op =, [real, real] => bool)
343 *** . . Const ( Nat.power, [real, nat] => real)
344 *** . . . Const ( 1, real)
345 *** . . . Var ((n, 0), nat)
346 *** . . Const ( 1, real) *)
347 val prop' = (#prop o rep_thm o num_str) realpow_eq_one;
350 *** Const ( Trueprop, bool => prop)
351 *** . Const ( op =, [real, real] => bool)
352 *** . . Const ( Nat.power, [real, nat] => real)
353 *** . . . Free ( 1, real)
354 *** . . . Var ((n, 0), nat)
355 *** . . Free ( 1, real)*)
356 val t = (term_of o the o (parseold thy)) "1 ^ aaa";
359 *** Const ( Nat.power, ['a, nat] => 'a)
361 *** . Free ( aaa, nat) *)
362 val t = (term_of o the o (parse thy)) "1 ^ aaa";
365 *** Const ( Nat.power, [real, nat] => real)
366 *** . Free ( 1, real)
367 *** . Free ( aaa, nat) .......................... nat !!! *)
368 val thm = num_str @{realpow_eq_one;
369 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
370 (*val t = Free ("1","RealDef.real") : term*)
372 " ================= calculate.sml: calculate_ 2002 =================== ";
373 " ================= calculate.sml: calculate_ 2002 =================== ";
374 " ================= calculate.sml: calculate_ 2002 =================== ";
377 val t = (term_of o the o (parse thy)) "12 / 3";
378 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
379 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
382 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
383 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
384 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
387 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
388 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
390 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
391 Syntax.string_of_term (thy2ctxt thy) t;
393 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
395 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
396 Syntax.string_of_term (thy2ctxt thy) t;
398 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
400 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
401 Syntax.string_of_term (thy2ctxt thy) t;
403 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
405 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
406 Syntax.string_of_term (thy2ctxt thy) t;
408 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
411 (*13.9.02 *** calc: operator = pow not defined*)
412 val t = (term_of o the o (parse thy)) "3^^^2";
413 val SOME (thmID,thm) =
414 get_calculation_ thy (the(assoc(calclist,"power_"))) t;
415 (*** calc: operator = pow not defined*)
417 val (op_, eval_fn) = the (assoc(calclist,"power_"));
419 val op_ = "Atools.pow" : string
420 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
422 val SOME (thmid,t') = get_pair thy op_ eval_fn t;
423 (*** calc: operator = pow not defined*)
425 val SOME (id,t') = eval_fn op_ t thy;
426 (*** calc: operator = pow not defined*)
428 val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
429 val SOME (id,t') = eval_binop thmid op_ t thy;
430 (*** calc: operator = pow not defined*)
433 "----------- get_pair with 3 args --------------------------------";
434 "----------- get_pair with 3 args --------------------------------";
435 "----------- get_pair with 3 args --------------------------------";
436 val (thy, op_, ef, arg) =
437 (thy, "EqSystem.occur'_exactly'_in",
438 snd (the (assoc(!calclist',"occur_exactly_in"))),
440 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
442 val SOME (str, simpl) = get_pair thy op_ ef arg;
444 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
445 then () else raise error "calculate.sml get_pair with 3 args:occur_exactly_in";
449 " ================= eval_binop Float =================== ";
450 val t = str2term "Float ((1,2),(0,0))";
452 val Const ("Float.Float",_) $
454 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;
456 val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))";
458 (*WN.10.4.03 eval_binop Float *)
461 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
462 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
463 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
464 val t = str2term "2 * x is_const";
465 val SOME (str, t') = eval_const "" "" t Test.thy;
467 "(2 * x is_const) = False";
469 val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;