15 "----------- calculate from script --requires 'setup'----"; |
15 "----------- calculate from script --requires 'setup'----"; |
16 "----------- calculate check test-root-equ --------------"; |
16 "----------- calculate check test-root-equ --------------"; |
17 "----------- check calculate bottom up -----------------"; |
17 "----------- check calculate bottom up -----------------"; |
18 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
18 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
19 "----------- fun cancel_int --------------------------------------------------------------------"; |
19 "----------- fun cancel_int --------------------------------------------------------------------"; |
20 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
20 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; |
21 "----------- get_pair with 3 args -----------------------"; |
21 "----------- get_pair with 3 args -----------------------"; |
22 "----------- calculate (2 * x is_num) -------------------"; |
22 "----------- calculate (2 * x is_num) -------------------"; |
23 "----------- fun get_pair: examples ------------------------------------------------------------"; |
23 "----------- fun get_pair: examples ------------------------------------------------------------"; |
24 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
24 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
25 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; |
25 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; |
47 "----------- fun calculate_ --------------------------------------------------------------------"; |
47 "----------- fun calculate_ --------------------------------------------------------------------"; |
48 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *) |
48 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *) |
49 val t = TermC.str2term "((1+2)*4/3) \<up> 2"; |
49 val t = TermC.str2term "((1+2)*4/3) \<up> 2"; |
50 val thy = @{theory}; |
50 val thy = @{theory}; |
51 val ctxt = Proof_Context.init_global @{theory} |
51 val ctxt = Proof_Context.init_global @{theory} |
52 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn; |
52 val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.eval_fn; |
53 val plus = ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn; |
53 val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn; |
54 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn; |
54 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn; |
55 val pow = (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn; |
55 val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn; |
56 |
56 |
57 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); |
57 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); |
58 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
58 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
59 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
59 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
60 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
60 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
277 case (op_, t) of |
277 case (op_, t) of |
278 (\<^const_name>\<open>realpow\<close>, |
278 (\<^const_name>\<open>realpow\<close>, |
279 Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $ |
279 Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $ |
280 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => () |
280 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => () |
281 | _ => error "3 \<up> 2 CHANGED"; |
281 | _ => error "3 \<up> 2 CHANGED"; |
282 val SOME (id, t') = eval_binop thmid op_ t ctxt; |
282 val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt; |
283 (*** calc: operator = pow not defined*) |
283 (*** calc: operator = pow not defined*) |
284 |
284 |
285 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
285 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
286 |
286 |
287 |
287 |
291 if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED"; |
291 if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED"; |
292 if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED"; |
292 if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED"; |
293 if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED"; |
293 if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED"; |
294 |
294 |
295 |
295 |
296 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
296 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; |
297 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
297 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; |
298 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
298 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; |
299 val t = @{term "2 + 3 ::real"}; |
299 val t = @{term "2 + 3 ::real"}; |
300 |
300 |
301 "~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t); |
301 "~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t); |
302 val simp_ctxt = |
302 val simp_ctxt = |
303 Proof_Context.init_global thy |
303 Proof_Context.init_global thy |
304 |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions}); |
304 |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions}); |
305 val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs); |
305 val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs); |
306 |
306 |