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