45 |
45 |
46 "----------- fun calculate_ --------------------------------------------------------------------"; |
46 "----------- fun calculate_ --------------------------------------------------------------------"; |
47 "----------- fun calculate_ --------------------------------------------------------------------"; |
47 "----------- fun calculate_ --------------------------------------------------------------------"; |
48 "----------- fun calculate_ --------------------------------------------------------------------"; |
48 "----------- fun calculate_ --------------------------------------------------------------------"; |
49 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *) |
49 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *) |
50 val t = TermC.str2term "((1+2)*4/3) \<up> 2"; |
50 val t = TermC.parse_test @{context} "((1+2)*4/3) \<up> 2"; |
51 val thy = @{theory}; |
51 val thy = @{theory}; |
52 val ctxt = Proof_Context.init_global @{theory} |
52 val ctxt = Proof_Context.init_global @{theory} |
53 val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun; |
53 val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun; |
54 val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun; |
54 val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun; |
55 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun; |
55 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun; |
143 val t = TermC.parseNEW' ctxt "2 is_num"; |
143 val t = TermC.parseNEW' ctxt "2 is_num"; |
144 TermC.atomty t; |
144 TermC.atomty t; |
145 rewrite_set_ ctxt false tval_rls t; |
145 rewrite_set_ ctxt false tval_rls t; |
146 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*) |
146 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*) |
147 |
147 |
148 val t = TermC.str2term "2 * x is_num"; |
148 val t = TermC.parse_test @{context} "2 * x is_num"; |
149 val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"}); |
149 val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"}); |
150 |
150 |
151 |
151 |
152 "----------- check calculate bottom up ------------------"; |
152 "----------- check calculate bottom up ------------------"; |
153 "----------- check calculate bottom up ------------------"; |
153 "----------- check calculate bottom up ------------------"; |
318 "----------- get_pair with 3 args --------------------------------"; |
318 "----------- get_pair with 3 args --------------------------------"; |
319 "----------- get_pair with 3 args --------------------------------"; |
319 "----------- get_pair with 3 args --------------------------------"; |
320 val (thy, op_, ef, arg) = |
320 val (thy, op_, ef, arg) = |
321 (thy, "EqSystem.occur_exactly_in", |
321 (thy, "EqSystem.occur_exactly_in", |
322 get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd, |
322 get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd, |
323 TermC.str2term |
323 TermC.parse_test @{context} |
324 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2" |
324 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2" |
325 ); |
325 ); |
326 val SOME (str, simpl) = get_pair ctxt op_ ef arg; |
326 val SOME (str, simpl) = get_pair ctxt op_ ef arg; |
327 if str = |
327 if str = |
328 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True" |
328 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True" |
330 |
330 |
331 |
331 |
332 "----------- calculate (2 * x is_num) -------------------"; |
332 "----------- calculate (2 * x is_num) -------------------"; |
333 "----------- calculate (2 * x is_num) -------------------"; |
333 "----------- calculate (2 * x is_num) -------------------"; |
334 "----------- calculate (2 * x is_num) -------------------"; |
334 "----------- calculate (2 * x is_num) -------------------"; |
335 val t = TermC.str2term "(2::real) * x is_num"; |
335 val t = TermC.parse_test @{context} "(2::real) * x is_num"; |
336 |
336 |
337 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test}; |
337 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test}; |
338 if UnparseC.term t' = "(2 * x is_num) = False" then () |
338 if UnparseC.term t' = "(2 * x is_num) = False" then () |
339 else error "is_num 2 * x is_num CHANGED"; |
339 else error "is_num 2 * x is_num CHANGED"; |
340 |
340 |
469 |
469 |
470 |
470 |
471 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
471 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
472 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
472 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
473 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
473 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
474 val t = TermC.str2term "sqrt 4"; |
474 val t = TermC.parse_test @{context} "sqrt 4"; |
475 Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t; |
475 Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t; |
476 |
476 |
477 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) = |
477 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) = |
478 ((ThyC.get_theory "Isac_Knowledge"), |
478 ((ThyC.get_theory "Isac_Knowledge"), |
479 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t); |
479 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t); |