376 \<^rule_thm>\<open>or_commute\<close>, |
376 \<^rule_thm>\<open>or_commute\<close>, |
377 |
377 |
378 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
378 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
379 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
379 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
380 |
380 |
381 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
381 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
382 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
382 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
383 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
383 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
384 |
384 |
385 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
385 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
386 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
386 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
387 |
387 |
388 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
388 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
419 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
419 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
420 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"), |
420 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"), |
421 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
421 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
422 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"), |
422 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"), |
423 |
423 |
424 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
424 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
425 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
425 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
426 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
426 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
427 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
427 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
428 |
428 |
429 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
429 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
430 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
430 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
431 |
431 |
432 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
432 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
492 |
492 |
493 \<^rule_thm>\<open>radd_real_const_eq\<close>, |
493 \<^rule_thm>\<open>radd_real_const_eq\<close>, |
494 \<^rule_thm>\<open>radd_real_const\<close>, |
494 \<^rule_thm>\<open>radd_real_const\<close>, |
495 (* these 2 rules are invers to distr_div_right wrt. termination. |
495 (* these 2 rules are invers to distr_div_right wrt. termination. |
496 thus they MUST be done IMMEDIATELY before calc *) |
496 thus they MUST be done IMMEDIATELY before calc *) |
497 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
497 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
498 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
498 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
499 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
499 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
500 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
500 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
501 |
501 |
502 \<^rule_thm>\<open>rcollect_right\<close>, |
502 \<^rule_thm>\<open>rcollect_right\<close>, |
503 \<^rule_thm>\<open>rcollect_one_left\<close>, |
503 \<^rule_thm>\<open>rcollect_one_left\<close>, |
504 \<^rule_thm>\<open>rcollect_one_left_assoc\<close>, |
504 \<^rule_thm>\<open>rcollect_one_left_assoc\<close>, |
505 \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>, |
505 \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>, |
597 val make_polytest = |
597 val make_polytest = |
598 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
598 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
599 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
599 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
600 erls = testerls, srls = Rule_Set.Empty, |
600 erls = testerls, srls = Rule_Set.Empty, |
601 calc = [ |
601 calc = [ |
602 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
602 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), |
603 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
603 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")), |
604 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))], |
604 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))], |
605 errpatts = [], |
605 errpatts = [], |
606 rules = [ |
606 rules = [ |
607 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*) |
607 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*) |
608 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
608 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
609 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
609 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
628 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
628 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
629 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
629 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
630 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
630 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
631 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
631 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
632 |
632 |
633 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
633 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
634 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
634 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
635 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")], |
635 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")], |
636 scr = Rule.Empty_Prog}; |
636 scr = Rule.Empty_Prog}; |
637 |
637 |
638 val expand_binomtest = |
638 val expand_binomtest = |
639 Rule_Def.Repeat{id = "expand_binomtest", preconds = [], |
639 Rule_Def.Repeat{id = "expand_binomtest", preconds = [], |
640 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty, |
640 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty, |
641 calc = [ |
641 calc = [ |
642 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
642 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), |
643 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
643 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")), |
644 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_")) |
644 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_")) |
645 ], |
645 ], |
646 errpatts = [], |
646 errpatts = [], |
647 rules = [ |
647 rules = [ |
648 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
648 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
649 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*) |
649 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*) |
662 |
662 |
663 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
663 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
664 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
664 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
665 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
665 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
666 |
666 |
667 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
667 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
668 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
668 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
669 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
669 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
670 |
670 |
671 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
671 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
672 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
672 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
673 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*) |
673 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*) |
674 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
674 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
676 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*) |
676 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*) |
677 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
677 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
678 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
678 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
679 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
679 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
680 |
680 |
681 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
681 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
682 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
682 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
683 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")], |
683 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")], |
684 scr = Rule.Empty_Prog}; |
684 scr = Rule.Empty_Prog}; |
685 \<close> |
685 \<close> |
686 rule_set_knowledge |
686 rule_set_knowledge |
687 make_polytest = \<open>prep_rls' make_polytest\<close> and |
687 make_polytest = \<open>prep_rls' make_polytest\<close> and |
688 expand_binomtest = \<open>prep_rls' expand_binomtest\<close> |
688 expand_binomtest = \<open>prep_rls' expand_binomtest\<close> |