1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/calculate.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,455 @@
1.4 +(* use"tests/calculate.sml";
1.5 + use"calculate.sml";
1.6 + *)
1.7 +(*contents
1.8 +" ================= calculate.sml: calculate_ ======================== ";
1.9 +" ================= calculate.sml: aus script ======================== ";
1.10 +" ================= calculate.sml: from test-root-equ.sml ================== ";
1.11 +" ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
1.12 +" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.13 +" ================= calculate.sml: calculate_ 2002 =================== ";
1.14 +" ================= eval_binop Float =================== ";
1.15 +*)
1.16 +
1.17 +(* [("Var",("Tools.Var",fn)),("Length",("Tools.Length",fn)),
1.18 + ("Nth",("Tools.Nth",fn)),
1.19 + ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),
1.20 + ("is_const",("Atools.is'_const",fn)),
1.21 + ("le",("op <",fn)),("leq",("op <=",fn)),
1.22 + ("ident",("Atools.ident",fn))] *)
1.23 +
1.24 +" ================= calculate.sml: calculate_ ======================== ";
1.25 +" ================= calculate.sml: calculate_ ======================== ";
1.26 +" ================= calculate.sml: calculate_ ======================== ";
1.27 +
1.28 +
1.29 +val thy = Test.thy;
1.30 +val t = (term_of o the o (parse thy)) "1+2";
1.31 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.32 +
1.33 +val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
1.34 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.35 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.36 +Sign.string_of_term (sign_of thy) t;
1.37 +(*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
1.38 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
1.39 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.40 +Sign.string_of_term (sign_of thy) t;
1.41 +(*val it = "(#12 // #3) ^^^ #2" : string*)
1.42 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.43 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.44 +Sign.string_of_term (sign_of thy) t;
1.45 +(*it = "#4 ^^^ #2" : string*)
1.46 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.47 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.48 +Sign.string_of_term (sign_of thy) t;
1.49 +(*val it = "#16" : string*)
1.50 +if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
1.51 +else ();
1.52 +
1.53 +" ================= calculate.sml: aus script ======================== ";
1.54 +" ================= calculate.sml: aus script ======================== ";
1.55 +" ================= calculate.sml: aus script ======================== ";
1.56 +
1.57 +store_pbt
1.58 + (prep_pbt Test.thy
1.59 + (["test"],
1.60 + [],
1.61 + e_rls, None, []));
1.62 +store_pbt
1.63 + (prep_pbt Test.thy
1.64 + (["calculate","test"],
1.65 + [("#Given" ,["realTestGiven t_"]),
1.66 + ("#Find" ,["realTestFind s_"])
1.67 + ],
1.68 + e_rls, None, [("Test.thy","test_calculate")]));
1.69 +
1.70 +methods:= overwritel (!methods,
1.71 +[
1.72 + prep_met
1.73 + (("Test.thy","test_calculate"):metID,
1.74 + [("#Given" ,["realTestGiven t_"]),
1.75 + ("#Find" ,["realTestFind s_"])
1.76 + ],
1.77 + {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
1.78 + calc=[("plus" ,("op +" ,eval_binop "#add_")),
1.79 + ("times" ,("op *" ,eval_binop "#mult_")),
1.80 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.81 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
1.82 + asm_rls=[],asm_thm=[]},
1.83 + "Script STest_simplify (t_::real) = \
1.84 + \(Repeat \
1.85 + \ ((Try (Repeat (Calculate plus))) @@ \
1.86 + \ (Try (Repeat (Calculate times))) @@ \
1.87 + \ (Try (Repeat (Calculate divide_))) @@ \
1.88 + \ (Try (Repeat (Calculate power_))))) t_"
1.89 + )
1.90 +]);
1.91 +
1.92 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
1.93 +val (dI',pI',mI') =
1.94 + ("Test.thy",["calculate","test"],("Test.thy","test_calculate"));
1.95 +val p = e_pos'; val c = [];
1.96 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.97 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.98 +(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
1.99 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.100 +(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * mstep*)
1.101 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 +(*nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)
1.103 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.104 +(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
1.105 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.106 +(*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)
1.107 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.108 +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)
1.109 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.110 +(*nxt = ("Calculate",Calculate "plus")*)
1.111 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.112 +(*nxt = ("Calculate",Calculate "times")*)
1.113 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.114 +(*nxt = ("Calculate",Calculate "divide_")*)
1.115 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.116 +(*nxt = ("Calculate",Calculate "power_")*)
1.117 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.118 +(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.120 +(*nxt = ("End_Proof'",End_Proof')*)
1.121 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
1.122 +else raise error "calculate.sml: script test_calculate changed behaviour";
1.123 +
1.124 +
1.125 +
1.126 +
1.127 +" ================= calculate.sml: from test-root-equ.sml ================== ";
1.128 +" ================= calculate.sml: from test-root-equ.sml ================== ";
1.129 +" ================= calculate.sml: from test-root-equ.sml ================== ";
1.130 +val thy' = "Test.thy";
1.131 +val ct = "1 + 2";
1.132 +val (ct,thm') = the (calculate thy' (the(assoc(calclist,"plus"))) ct);
1.133 +(*val ct = "#3" : string
1.134 +val thm' = ("#add_#1_#2","\"#1 + #2 = #3\"") : thm'*)
1.135 +
1.136 +"----- me -----";
1.137 +val (dI',pI',mI') = ("Test.thy",e_pblID,
1.138 + ("Test.thy","sqrt-equ-test"));
1.139 +val p = e_pos'; val c = [];
1.140 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.141 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.142 +val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
1.143 +val (p,_,_,_,_,pt) = me nxt p c pt;
1.144 +val (pt,_) = cappend_atomic pt [1] e_istate "1 + 2"
1.145 + (Calculate "test") ct Complete;
1.146 +val p = ([1],Frm):pos';
1.147 +val nxt = ("Calculate",Calculate "plus");
1.148 +val (p,_,f,nxt,_,pt)=me nxt p c pt;
1.149 +Compiler.Control.Print.printDepth:=9; (*4 default*)
1.150 +(* Nd (PblObj...
1.151 + [Nd (PrfObj
1.152 + {branch=NoBranch,cell=[],form="#1 + #2",loc=(([],None),([],None)),
1.153 + mstep=Calculate "plus",ostate=Complete,result="#3"},[])]) : squ*)
1.154 +Compiler.Control.Print.printDepth:=4; (*4 default*)
1.155 +
1.156 +val (pt,_) = cappend_atomic pt [1] e_istate "6/4"
1.157 + (Calculate "test") ct Complete;
1.158 +val p = ([1],Frm):pos';
1.159 +val nxt = ("Calculate",Calculate "divide_");
1.160 +val (p,_,f,nxt,_,pt)=me nxt p c pt;
1.161 +(*{branch=NoBranch,cell=[],form="#6 // #4",loc=(([],None),([],None)),
1.162 + mstep=Calculate "divide_",ostate=Complete,result="#3 // #2"},[])]) *)
1.163 +
1.164 +(*5.7.00: interne ops in calclist*)
1.165 +
1.166 +
1.167 +" ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
1.168 +" ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
1.169 +" ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
1.170 +(*(1): 2nd Test_simplify didn't work:
1.171 +val ct =
1.172 + "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.173 +> val rls = ("Test_simplify");
1.174 +> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
1.175 +val ct = "sqrt (x ^^^ 2 + -3 * x) =
1.176 +(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.177 +ie. cancel does not work properly
1.178 +*)
1.179 + val thy = "Test.thy";
1.180 + val op_ = "divide_";
1.181 + val ct = "sqrt (x ^^^ 2 + -3 * x) =\
1.182 + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.183 + val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
1.184 + writeln ct;
1.185 +(*
1.186 + sqrt (x ^^^ 2 + -3 * x) =\
1.187 + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
1.188 +............... does not work *)
1.189 +
1.190 +(*--------------(2): does divide work in Test_simplify ?: ------*)
1.191 + val thy = Test.thy;
1.192 + val t = (term_of o the o (parse thy)) "6 / 2";
1.193 + val rls = Test_simplify;
1.194 + val (t,_) = the (rewrite_set_ thy false rls t);
1.195 +(*val t = Free ("3","RealDef.real") : term*)
1.196 +
1.197 + val thy = "Test.thy";
1.198 + val t = "6 / 2";
1.199 + val rls = "Test_simplify";
1.200 + val (t,_) = the (rewrite_set thy false rls t);
1.201 +(*val t = "3" : string
1.202 + ....... works, thus: which rule in SqRoot_simplify works differently ?*)
1.203 +
1.204 +
1.205 +(*--------------(3): is_const works ?: -------------------------------------*)
1.206 + val t = (term_of o the o (parse Test.thy)) "2 is_const";
1.207 + atomty Test.thy t;
1.208 + rewrite_set_ Test.thy false tval_rls t;
1.209 +(*val it = Some (Const ("True","bool"),[]) ... works*)
1.210 +
1.211 +
1.212 +(*--------------(4): check bottom up: ---------------------------*)
1.213 +(*-------------- eval_cancel works: *)
1.214 + trace_rewrite:=true;
1.215 + val thy = Test.thy;
1.216 + val t = (term_of o the o (parse thy)) "(-4) / 2";
1.217 + val Some (_,t) = eval_cancel "xxx" 111 t thy;
1.218 + term2str t;
1.219 +"-4 / 2 = (-2)";
1.220 +(*-------------- but ... *)
1.221 + val ct = "x + (-4) / 2";
1.222 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.223 +"(-2) + x";
1.224 +(*-------------- while ... *)
1.225 + val ct = "(-4) / 2";
1.226 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.227 +"(-2)";
1.228 +
1.229 +(*--------------(5): reproduce (1) with simpler term: ------------*)
1.230 + val thy = "Test.thy";
1.231 + val t = "(3+5)/2";
1.232 + val (t,_) = the (rewrite_set thy false rls t);
1.233 +(*val t = "4" ... works*)
1.234 +
1.235 + val t = "(3+1+2*x)/2";
1.236 + val (t,_) = the (rewrite_set thy false rls t);
1.237 +(*val t = "2 + x" ... works*)
1.238 +
1.239 + val t = "(3+(1+2*x))/2";
1.240 + val (t,_) = the (rewrite_set thy false rls t);
1.241 +(*val t = "2 + x" ... works: give up----------------------------------------*)
1.242 +
1.243 +
1.244 +
1.245 +(*--- trace_rewrite before correction of ... --------------------
1.246 + val ct = "(-3 + 2 * x + -1) / 2";
1.247 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.248 +:
1.249 +### trying thm 'root_ge0_2'
1.250 +### rewrite_set_: x + (-1 + -3) / 2
1.251 +### trying thm 'radd_real_const_eq'
1.252 +### trying thm 'radd_real_const'
1.253 +### rewrite_set_: x + (-4) / 2
1.254 +### trying thm 'rcollect_right'
1.255 +:
1.256 +"x + (-4) / 2"
1.257 +-------------------------------------while before Isabelle20002:
1.258 + val ct = "(#-3 + #2 * x + #-1) // #2";
1.259 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.260 +:
1.261 +### trying thm 'root_ge0_2'
1.262 +### rewrite_set_: x + (#-1 + #-3) // #2
1.263 +### trying thm 'radd_real_const_eq'
1.264 +### trying thm 'radd_real_const'
1.265 +### rewrite_set_: x + #-4 // #2
1.266 +### rewrite_set_: x + #-2
1.267 +### trying thm 'rcollect_right'
1.268 +:
1.269 +"#-2 + x"
1.270 +-----------------------------------------------------------------*)
1.271 +
1.272 +
1.273 + toggle trace_rewrite;
1.274 +(*===================*)
1.275 + trace_rewrite:=true;
1.276 + val thy' = "Test.thy";
1.277 + val rls = "Test_simplify";
1.278 + val ct = "x + (-1 + -3) / 2";
1.279 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.280 +"x + (-4) / 2";
1.281 +(*
1.282 +### trying calc. 'cancel'
1.283 +@@@ get_pair: binop, t = x + (-4) / 2
1.284 +@@@ get_pair: t else
1.285 +@@@ get_pair: t else -> None
1.286 +@@@ get_pair: binop, t = (-4) / 2
1.287 +@@@ get_pair: then 1
1.288 +@@@ get_pair: t -> None
1.289 +@@@ get_pair: t1 -> None
1.290 +@@@ get_calculation: None
1.291 +### trying calc. 'pow'
1.292 +*)
1.293 +
1.294 + trace_rewrite:=true;
1.295 + val thy' = "Test.thy";
1.296 + val rls = "Test_simplify";
1.297 + val ct = "x + (-4) / 2";
1.298 + val (ct,_) = the (rewrite_set thy' false rls ct);
1.299 +"(-2) + x";
1.300 +(*
1.301 +### trying calc. 'cancel'
1.302 +@@@ get_pair: binop, t = x + -4 / 2
1.303 +@@@ get_pair: t else
1.304 +@@@ get_pair: t else -> None
1.305 +@@@ get_pair: binop, t = -4 / 2
1.306 +@@@ get_pair: then 1
1.307 +@@@ get_calculation: Some #cancel_-4_2
1.308 +### calc. to: x + (-2)
1.309 +### trying calc. 'cancel'
1.310 +*)
1.311 + trace_rewrite:=false;
1.312 +
1.313 +" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.314 +" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.315 +" ================= calculate.sml:10.8.02 2002:///->/ ======== ";
1.316 +" ----------------- rewriting works ? -----------------------";
1.317 + val thy = Isac.thy;
1.318 + val prop = (#prop o rep_thm) real_divide_1;
1.319 + atomty thy prop;
1.320 +(*** -------------
1.321 +*** Const ( Trueprop, bool => prop)
1.322 +*** . Const ( op =, [real, real] => bool)
1.323 +*** . . Const ( HOL.divide, [real, real] => real)
1.324 +*** . . . Var ((x, 0), real)
1.325 +*** . . . Const ( 1, real)
1.326 +*** . . Var ((x, 0), real) *)
1.327 + val prop' = (#prop o rep_thm o num_str) real_divide_1;
1.328 + atomty thy prop';
1.329 +(*** -------------
1.330 +*** Const ( Trueprop, bool => prop)
1.331 +*** . Const ( op =, [real, real] => bool)
1.332 +*** . . Const ( HOL.divide, [real, real] => real)
1.333 +*** . . . Var ((x, 0), real)
1.334 +*** . . . Free ( 1, real) (*app_num_tr'*)
1.335 +*** . . Var ((x, 0), real)*)
1.336 + val t = (term_of o the o (parseold thy)) "aaa/1";
1.337 + atomty thy t;
1.338 +(*** -------------
1.339 +*** Const ( HOL.divide, ['a, 'a] => 'a)
1.340 +*** . Free ( aaa, 'a)
1.341 +*** . Free ( 1, 'a) *)
1.342 + val t = (term_of o the o (parse thy)) "aaa/1";
1.343 + atomty thy t;
1.344 +(*** -------------
1.345 +*** Const ( HOL.divide, [real, real] => real)
1.346 +*** . Free ( aaa, real)
1.347 +*** . Free ( 1, real) *)
1.348 + val thm = num_str real_divide_1;
1.349 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.350 +(*val t = Free ("aaa","RealDef.real") : term*)
1.351 +
1.352 +
1.353 + val prop = (#prop o rep_thm) realpow_eq_one;
1.354 + atomty thy prop;
1.355 +(*** -------------
1.356 +*** Const ( Trueprop, bool => prop)
1.357 +*** . Const ( op =, [real, real] => bool)
1.358 +*** . . Const ( Nat.power, [real, nat] => real)
1.359 +*** . . . Const ( 1, real)
1.360 +*** . . . Var ((n, 0), nat)
1.361 +*** . . Const ( 1, real) *)
1.362 + val prop' = (#prop o rep_thm o num_str) realpow_eq_one;
1.363 + atomty thy prop';
1.364 +(*** -------------
1.365 +*** Const ( Trueprop, bool => prop)
1.366 +*** . Const ( op =, [real, real] => bool)
1.367 +*** . . Const ( Nat.power, [real, nat] => real)
1.368 +*** . . . Free ( 1, real)
1.369 +*** . . . Var ((n, 0), nat)
1.370 +*** . . Free ( 1, real)*)
1.371 + val t = (term_of o the o (parseold thy)) "1 ^ aaa";
1.372 + atomty thy t;
1.373 +(*** -------------
1.374 +*** Const ( Nat.power, ['a, nat] => 'a)
1.375 +*** . Free ( 1, 'a)
1.376 +*** . Free ( aaa, nat) *)
1.377 + val t = (term_of o the o (parse thy)) "1 ^ aaa";
1.378 + atomty thy t;
1.379 +(*** -------------
1.380 +*** Const ( Nat.power, [real, nat] => real)
1.381 +*** . Free ( 1, real)
1.382 +*** . Free ( aaa, nat) .......................... nat !!! *)
1.383 + val thm = num_str realpow_eq_one;
1.384 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.385 +(*val t = Free ("1","RealDef.real") : term*)
1.386 +
1.387 +" ================= calculate.sml: calculate_ 2002 =================== ";
1.388 +" ================= calculate.sml: calculate_ 2002 =================== ";
1.389 +" ================= calculate.sml: calculate_ 2002 =================== ";
1.390 +
1.391 +val thy = Test.thy;
1.392 +val t = (term_of o the o (parse thy)) "12 / 3";
1.393 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.394 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.395 +"12 / 3 = 4";
1.396 +val thy = Test.thy;
1.397 +val t = (term_of o the o (parse thy)) "4 ^^^ 2";
1.398 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
1.399 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.400 +"4 ^ 2 = 16";
1.401 +
1.402 + val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.403 + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
1.404 +"1 + 2 = 3";
1.405 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.406 + Sign.string_of_term (sign_of thy) t;
1.407 +"(3 * 4 / 3) ^^^ 2";
1.408 + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
1.409 +"3 * 4 = 12";
1.410 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.411 + Sign.string_of_term (sign_of thy) t;
1.412 +"(12 / 3) ^^^ 2";
1.413 + val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
1.414 +"12 / 3 = 4";
1.415 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.416 + Sign.string_of_term (sign_of thy) t;
1.417 +"4 ^^^ 2";
1.418 + val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
1.419 +"4 ^^^ 2 = 16";
1.420 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.421 + Sign.string_of_term (sign_of thy) t;
1.422 +"16";
1.423 + if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
1.424 + else ();
1.425 +
1.426 +(*13.9.02 *** calc: operator = pow not defined*)
1.427 + val t = (term_of o the o (parse thy)) "3^^^2";
1.428 + val Some (thmID,thm) =
1.429 + get_calculation_ thy (the(assoc(calclist,"power_"))) t;
1.430 +(*** calc: operator = pow not defined*)
1.431 +
1.432 + val (op_, eval_fn) = the (assoc(calclist,"power_"));
1.433 + (*
1.434 +val op_ = "Atools.pow" : string
1.435 +val eval_fn = fn : string -> term -> theory -> (string * term) option*)
1.436 +
1.437 + val Some (thmid,t') = get_pair thy op_ eval_fn t;
1.438 +(*** calc: operator = pow not defined*)
1.439 +
1.440 + val Some (id,t') = eval_fn op_ t thy;
1.441 +(*** calc: operator = pow not defined*)
1.442 +
1.443 + val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
1.444 + val Some (id,t') = eval_binop thmid op_ t thy;
1.445 +(*** calc: operator = pow not defined*)
1.446 +
1.447 +
1.448 +
1.449 +" ================= eval_binop Float =================== ";
1.450 +val t = str2term "Float ((1,2),(0,0))";
1.451 +atomty thy t;
1.452 +val Const ("Float.Float",_) $
1.453 + (Const ("Pair",_) $
1.454 + (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;
1.455 +
1.456 +val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))";
1.457 +atomty thy t;
1.458 +(*GOON.10.4.03*)
1.459 \ No newline at end of file