15 " ================= eval_binop Float =================== "; |
15 " ================= eval_binop Float =================== "; |
16 "------------------ 3.6.03 (2 * x is_const) ---------------------------"; |
16 "------------------ 3.6.03 (2 * x is_const) ---------------------------"; |
17 |
17 |
18 (* [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)), |
18 (* [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)), |
19 ("Nth",("Tools.Nth",fn)), |
19 ("Nth",("Tools.Nth",fn)), |
20 ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)), |
20 ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)), |
21 ("is_const",("Atools.is'_const",fn)), |
21 ("is_const",("Atools.is'_const",fn)), |
22 ("le",("op <",fn)),("leq",("op <=",fn)), |
22 ("le",("op <",fn)),("leq",("op <=",fn)), |
23 ("ident",("Atools.ident",fn))] *) |
23 ("ident",("Atools.ident",fn))] *) |
24 |
24 |
25 val thy' = "Isac.thy"; |
25 val thy' = "Isac.thy"; |
75 (["Test","test_calculate"]:metID, |
75 (["Test","test_calculate"]:metID, |
76 [("#Given" ,["realTestGiven t_"]), |
76 [("#Given" ,["realTestGiven t_"]), |
77 ("#Find" ,["realTestFind s_"]) |
77 ("#Find" ,["realTestFind s_"]) |
78 ], |
78 ], |
79 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
79 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
80 calc=[("plus" ,("op +" ,eval_binop "#add_")), |
80 calc=[("plus" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
81 ("times" ,("op *" ,eval_binop "#mult_")), |
81 ("times" ,("op *" ,eval_binop "#mult_")), |
82 ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")), |
82 ("divide_" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_")), |
83 ("power_" ,("Atools.pow" ,eval_binop "#power_"))], |
83 ("power_" ,("Atools.pow" ,eval_binop "#power_"))], |
84 crls=tval_rls, nrls=e_rls(*, |
84 crls=tval_rls, nrls=e_rls(*, |
85 asm_rls=[],asm_thm=[]*)}, |
85 asm_rls=[],asm_thm=[]*)}, |
86 "Script STest_simplify (t_::real) = \ |
86 "Script STest_simplify (t_::real) = \ |
87 \(Repeat \ |
87 \(Repeat \ |
183 "--------------(4): check bottom up: ---------------------------"; |
183 "--------------(4): check bottom up: ---------------------------"; |
184 (*-------------- eval_cancel works: *) |
184 (*-------------- eval_cancel works: *) |
185 trace_rewrite:=true; |
185 trace_rewrite:=true; |
186 val thy = Test.thy; |
186 val thy = Test.thy; |
187 val t = (term_of o the o (parse thy)) "(-4) / 2"; |
187 val t = (term_of o the o (parse thy)) "(-4) / 2"; |
188 val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy; |
188 val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy; |
189 term2str t; |
189 term2str t; |
190 "-4 / 2 = (-2)"; |
190 "-4 / 2 = (-2)"; |
191 (*-------------- but ... *) |
191 (*-------------- but ... *) |
192 val ct = "x + (-4) / 2"; |
192 val ct = "x + (-4) / 2"; |
193 val (ct,_) = the (rewrite_set thy' false rls ct); |
193 val (ct,_) = the (rewrite_set thy' false rls ct); |