407 subsection \<open>Rulesets and predicate for embedding\<close> |
407 subsection \<open>Rulesets and predicate for embedding\<close> |
408 ML \<open> |
408 ML \<open> |
409 (* evaluates conditions in calculate_Rational *) |
409 (* evaluates conditions in calculate_Rational *) |
410 val calc_rat_erls = |
410 val calc_rat_erls = |
411 prep_rls' |
411 prep_rls' |
412 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
412 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
413 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
413 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
414 rules = [ |
414 rules = [ |
415 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"), |
415 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"), |
416 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
416 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
417 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
417 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
422 (* simplifies expressions with numerals; |
422 (* simplifies expressions with numerals; |
423 does NOT rearrange the term by AC-rewriting; thus terms with variables |
423 does NOT rearrange the term by AC-rewriting; thus terms with variables |
424 need to have constants to be commuted together respectively *) |
424 need to have constants to be commuted together respectively *) |
425 val calculate_Rational = |
425 val calculate_Rational = |
426 prep_rls' (Rule_Set.merge "calculate_Rational" |
426 prep_rls' (Rule_Set.merge "calculate_Rational" |
427 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
427 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
428 erls = calc_rat_erls, srls = Rule_Set.Empty, |
428 erls = calc_rat_erls, srls = Rule_Set.Empty, |
429 calc = [], errpatts = [], |
429 calc = [], errpatts = [], |
430 rules = [ |
430 rules = [ |
431 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
431 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
432 |
432 |
604 section \<open>Rulesets for general simplification\<close> |
604 section \<open>Rulesets for general simplification\<close> |
605 ML \<open> |
605 ML \<open> |
606 (*.all powers over + distributed; atoms over * collected, other distributed |
606 (*.all powers over + distributed; atoms over * collected, other distributed |
607 contains absolute minimum of thms for context in norm_Rational .*) |
607 contains absolute minimum of thms for context in norm_Rational .*) |
608 val powers = prep_rls'( |
608 val powers = prep_rls'( |
609 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
609 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
610 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
610 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
611 rules = [ |
611 rules = [ |
612 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
612 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
613 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
613 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
614 \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*) |
614 \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*) |
628 |
628 |
629 \<close> ML \<open> |
629 \<close> ML \<open> |
630 (*.contains absolute minimum of thms for context in norm_Rational.*) |
630 (*.contains absolute minimum of thms for context in norm_Rational.*) |
631 val rat_mult_divide = prep_rls'( |
631 val rat_mult_divide = prep_rls'( |
632 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], |
632 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], |
633 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
633 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
634 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
634 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
635 rules = [ |
635 rules = [ |
636 \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
636 \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
637 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
637 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
638 otherwise inv.to a / b / c = ...*) |
638 otherwise inv.to a / b / c = ...*) |
645 scr = Rule.Empty_Prog}); |
645 scr = Rule.Empty_Prog}); |
646 |
646 |
647 \<close> ML \<open> |
647 \<close> ML \<open> |
648 (*.contains absolute minimum of thms for context in norm_Rational.*) |
648 (*.contains absolute minimum of thms for context in norm_Rational.*) |
649 val reduce_0_1_2 = prep_rls'( |
649 val reduce_0_1_2 = prep_rls'( |
650 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
650 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
651 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
651 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
652 rules = [ |
652 rules = [ |
653 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*) |
653 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*) |
654 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
654 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
655 \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*) |
655 \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*) |
668 scr = Rule.Empty_Prog}); |
668 scr = Rule.Empty_Prog}); |
669 |
669 |
670 (*erls for calculate_Rational; |
670 (*erls for calculate_Rational; |
671 make local with FIXX@ME result:term *term list WN0609???SKMG*) |
671 make local with FIXX@ME result:term *term list WN0609???SKMG*) |
672 val norm_rat_erls = prep_rls'( |
672 val norm_rat_erls = prep_rls'( |
673 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
673 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
674 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
674 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
675 rules = [ |
675 rules = [ |
676 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_") |
676 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_") |
677 ], |
677 ], |
678 scr = Rule.Empty_Prog}); |
678 scr = Rule.Empty_Prog}); |
681 (* consists of rls containing the absolute minimum of thms *) |
681 (* consists of rls containing the absolute minimum of thms *) |
682 (* |
682 (* |
683 which is now replaced by MGs version "norm_Rational" below |
683 which is now replaced by MGs version "norm_Rational" below |
684 *) |
684 *) |
685 val norm_Rational_min = prep_rls'( |
685 val norm_Rational_min = prep_rls'( |
686 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
686 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
687 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
687 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
688 rules = [(*sequence given by operator precedence*) |
688 rules = [(*sequence given by operator precedence*) |
689 Rule.Rls_ discard_minus, |
689 Rule.Rls_ discard_minus, |
690 Rule.Rls_ powers, |
690 Rule.Rls_ powers, |
691 Rule.Rls_ rat_mult_divide, |
691 Rule.Rls_ rat_mult_divide, |
699 scr = Rule.Empty_Prog}); |
699 scr = Rule.Empty_Prog}); |
700 |
700 |
701 \<close> ML \<open> |
701 \<close> ML \<open> |
702 val norm_Rational_parenthesized = prep_rls'( |
702 val norm_Rational_parenthesized = prep_rls'( |
703 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, |
703 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, |
704 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
704 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
705 erls = Atools_erls, srls = Rule_Set.Empty, |
705 erls = Atools_erls, srls = Rule_Set.Empty, |
706 calc = [], errpatts = [], |
706 calc = [], errpatts = [], |
707 rules = [ |
707 rules = [ |
708 Rule.Rls_ norm_Rational_min, |
708 Rule.Rls_ norm_Rational_min, |
709 Rule.Rls_ discard_parentheses], |
709 Rule.Rls_ discard_parentheses], |
721 \<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*) |
721 \<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*) |
722 \<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*) |
722 \<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*) |
723 \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]); |
723 \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]); |
724 |
724 |
725 val add_fractions_p_rls = prep_rls'( |
725 val add_fractions_p_rls = prep_rls'( |
726 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
726 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
727 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
727 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
728 rules = [Rule.Rls_ add_fractions_p], |
728 rules = [Rule.Rls_ add_fractions_p], |
729 scr = Rule.Empty_Prog}); |
729 scr = Rule.Empty_Prog}); |
730 |
730 |
731 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *) |
731 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *) |
732 val cancel_p_rls = prep_rls'( |
732 val cancel_p_rls = prep_rls'( |
733 Rule_Def.Repeat |
733 Rule_Def.Repeat |
734 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
734 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
735 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
735 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
736 rules = [Rule.Rls_ cancel_p], |
736 rules = [Rule.Rls_ cancel_p], |
737 scr = Rule.Empty_Prog}); |
737 scr = Rule.Empty_Prog}); |
738 |
738 |
739 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
739 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
740 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*) |
740 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*) |
741 val rat_mult_poly = prep_rls'( |
741 val rat_mult_poly = prep_rls'( |
742 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
742 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
743 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [ |
743 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [ |
744 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], |
744 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], |
745 srls = Rule_Set.Empty, calc = [], errpatts = [], |
745 srls = Rule_Set.Empty, calc = [], errpatts = [], |
746 rules = [ |
746 rules = [ |
747 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
747 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
752 used in looping part norm_Rational_rls, see example DA-M02-main.p.60 |
752 used in looping part norm_Rational_rls, see example DA-M02-main.p.60 |
753 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty, |
753 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty, |
754 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028 |
754 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028 |
755 ... WN0609???MG.*) |
755 ... WN0609???MG.*) |
756 val rat_mult_div_pow = prep_rls'( |
756 val rat_mult_div_pow = prep_rls'( |
757 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
757 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
758 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
758 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
759 rules = [ |
759 rules = [ |
760 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
760 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
761 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
761 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
762 \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
762 \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
768 |
768 |
769 \<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)], |
769 \<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)], |
770 scr = Rule.Empty_Prog}); |
770 scr = Rule.Empty_Prog}); |
771 |
771 |
772 val rat_reduce_1 = prep_rls'( |
772 val rat_reduce_1 = prep_rls'( |
773 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
773 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
774 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
774 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
775 rules = [ |
775 rules = [ |
776 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*) |
776 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*) |
777 \<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)], |
777 \<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)], |
778 scr = Rule.Empty_Prog}); |
778 scr = Rule.Empty_Prog}); |
779 |
779 |
780 (* looping part of norm_Rational *) |
780 (* looping part of norm_Rational *) |
781 val norm_Rational_rls = prep_rls' ( |
781 val norm_Rational_rls = prep_rls' ( |
782 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
782 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
783 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
783 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
784 rules = [ |
784 rules = [ |
785 Rule.Rls_ add_fractions_p_rls, |
785 Rule.Rls_ add_fractions_p_rls, |
786 Rule.Rls_ rat_mult_div_pow, |
786 Rule.Rls_ rat_mult_div_pow, |
787 Rule.Rls_ make_rat_poly_with_parentheses, |
787 Rule.Rls_ make_rat_poly_with_parentheses, |
789 Rule.Rls_ rat_reduce_1], |
789 Rule.Rls_ rat_reduce_1], |
790 scr = Rule.Empty_Prog}); |
790 scr = Rule.Empty_Prog}); |
791 |
791 |
792 val norm_Rational = prep_rls' ( |
792 val norm_Rational = prep_rls' ( |
793 Rule_Set.Sequence |
793 Rule_Set.Sequence |
794 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
794 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
795 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
795 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
796 rules = [ |
796 rules = [ |
797 Rule.Rls_ discard_minus, |
797 Rule.Rls_ discard_minus, |
798 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *) |
798 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *) |
799 Rule.Rls_ make_rat_poly_with_parentheses, |
799 Rule.Rls_ make_rat_poly_with_parentheses, |