87 rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and |
87 rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and |
88 rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and |
88 rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and |
89 |
89 |
90 (*real_times_divide1_eq .. Isa02*) |
90 (*real_times_divide1_eq .. Isa02*) |
91 real_times_divide_1_eq: "-1 * (c / d) = -1 * c / d " and |
91 real_times_divide_1_eq: "-1 * (c / d) = -1 * c / d " and |
92 real_times_divide_num: "a is_const ==> a * (c / d) = a * c / d " and |
92 real_times_divide_num: "a is_num ==> a * (c / d) = a * c / d " and |
93 |
93 |
94 real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and |
94 real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and |
95 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*) |
95 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*) |
96 |
96 |
97 real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and |
97 real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and |
98 real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and |
98 real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and |
99 (*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*) |
99 (*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*) |
100 |
100 |
101 rat_power: "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and |
101 rat_power: "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and |
102 |
102 |
103 rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==> |
103 rat_add: "[| a is_num; b is_num; c is_num; d is_num |] ==> |
104 a / c + b / d = (a * d + b * c) / (c * d)" and |
104 a / c + b / d = (a * d + b * c) / (c * d)" and |
105 rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==> |
105 rat_add_assoc: "[| a is_num; b is_num; c is_num; d is_num |] ==> |
106 a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and |
106 a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and |
107 rat_add1: "[| a is_const; b is_const; c is_const |] ==> |
107 rat_add1: "[| a is_num; b is_num; c is_num |] ==> |
108 a / c + b / c = (a + b) / c" and |
108 a / c + b / c = (a + b) / c" and |
109 rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==> |
109 rat_add1_assoc: "[| a is_num; b is_num; c is_num |] ==> |
110 a / c + (b / c + e) = (a + b) / c + e" and |
110 a / c + (b / c + e) = (a + b) / c + e" and |
111 rat_add2: "[| a is_const; b is_const; c is_const |] ==> |
111 rat_add2: "[| a is_num; b is_num; c is_num |] ==> |
112 a / c + b = (a + b * c) / c" and |
112 a / c + b = (a + b * c) / c" and |
113 rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==> |
113 rat_add2_assoc: "[| a is_num; b is_num; c is_num |] ==> |
114 a / c + (b + e) = (a + b * c) / c + e" and |
114 a / c + (b + e) = (a + b * c) / c + e" and |
115 rat_add3: "[| a is_const; b is_const; c is_const |] ==> |
115 rat_add3: "[| a is_num; b is_num; c is_num |] ==> |
116 a + b / c = (a * c + b) / c" and |
116 a + b / c = (a * c + b) / c" and |
117 rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==> |
117 rat_add3_assoc: "[| a is_num; b is_num; c is_num |] ==> |
118 a + (b / c + e) = (a * c + b) / c + e" |
118 a + (b / c + e) = (a * c + b) / c + e" |
119 |
119 |
120 section \<open>Cancellation and addition of fractions\<close> |
120 section \<open>Cancellation and addition of fractions\<close> |
121 subsection \<open>Conversion term <--> poly\<close> |
121 subsection \<open>Conversion term <--> poly\<close> |
122 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close> |
122 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close> |
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.dummy_ord), |
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_const\<close> (Prog_Expr.eval_const "#is_const_"), |
417 (*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* ) |
|
418 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
|
419 ( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*) |
418 \<^rule_thm>\<open>not_true\<close>, |
420 \<^rule_thm>\<open>not_true\<close>, |
419 \<^rule_thm>\<open>not_false\<close>], |
421 \<^rule_thm>\<open>not_false\<close>], |
420 scr = Rule.Empty_Prog}); |
422 scr = Rule.Empty_Prog}); |
421 |
423 |
422 (* simplifies expressions with numerals; |
424 (* simplifies expressions with numerals; |
430 rules = [ |
432 rules = [ |
431 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
433 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
432 |
434 |
433 \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*) |
435 \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*) |
434 \<^rule_thm>\<open>rat_add\<close>, |
436 \<^rule_thm>\<open>rat_add\<close>, |
435 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*) |
437 (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*) |
436 \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*) |
438 \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*) |
437 \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*) |
439 \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*) |
438 \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *) |
440 \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *) |
439 |
441 |
440 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*) |
442 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*) |
441 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*) |
443 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*) |
442 \<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*) |
444 \<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*) |
443 |
445 |
624 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*) |
626 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*) |
625 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*) |
627 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*) |
626 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
628 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
627 scr = Rule.Empty_Prog}); |
629 scr = Rule.Empty_Prog}); |
628 |
630 |
|
631 \<close> ML \<open> |
629 (*.contains absolute minimum of thms for context in norm_Rational.*) |
632 (*.contains absolute minimum of thms for context in norm_Rational.*) |
630 val rat_mult_divide = prep_rls'( |
633 val rat_mult_divide = prep_rls'( |
631 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], |
634 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], |
632 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
635 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
633 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
636 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
641 \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
644 \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
642 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
645 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
643 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")], |
646 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")], |
644 scr = Rule.Empty_Prog}); |
647 scr = Rule.Empty_Prog}); |
645 |
648 |
|
649 \<close> ML \<open> |
646 (*.contains absolute minimum of thms for context in norm_Rational.*) |
650 (*.contains absolute minimum of thms for context in norm_Rational.*) |
647 val reduce_0_1_2 = prep_rls'( |
651 val reduce_0_1_2 = prep_rls'( |
648 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
652 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
649 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
653 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
650 rules = [ |
654 rules = [ |
662 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
666 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
663 |
667 |
664 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)], |
668 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)], |
665 scr = Rule.Empty_Prog}); |
669 scr = Rule.Empty_Prog}); |
666 |
670 |
|
671 \<close> ML \<open> |
|
672 \<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*) |
|
673 ML \<open> |
667 (*erls for calculate_Rational; |
674 (*erls for calculate_Rational; |
668 make local with FIXX@ME result:term *term list WN0609???SKMG*) |
675 make local with FIXX@ME result:term *term list WN0609???SKMG*) |
669 val norm_rat_erls = prep_rls'( |
676 val norm_rat_erls = prep_rls'( |
670 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
677 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
671 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
678 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
672 rules = [ |
679 rules = [ |
673 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")], |
680 \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*) |
|
681 (*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* ) |
|
682 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_") |
|
683 ( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*) |
|
684 ], |
674 scr = Rule.Empty_Prog}); |
685 scr = Rule.Empty_Prog}); |
675 |
686 |
|
687 \<close> ML \<open> |
676 (* consists of rls containing the absolute minimum of thms *) |
688 (* consists of rls containing the absolute minimum of thms *) |
677 (* |
689 (* |
678 which is now replaced by MGs version "norm_Rational" below |
690 which is now replaced by MGs version "norm_Rational" below |
679 *) |
691 *) |
680 val norm_Rational_min = prep_rls'( |
692 val norm_Rational_min = prep_rls'( |
691 Rule.Rls_ add_fractions_p, |
703 Rule.Rls_ add_fractions_p, |
692 Rule.Rls_ cancel_p |
704 Rule.Rls_ cancel_p |
693 ], |
705 ], |
694 scr = Rule.Empty_Prog}); |
706 scr = Rule.Empty_Prog}); |
695 |
707 |
|
708 \<close> ML \<open> |
696 val norm_Rational_parenthesized = prep_rls'( |
709 val norm_Rational_parenthesized = prep_rls'( |
697 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, |
710 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, |
698 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
711 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
699 erls = Atools_erls, srls = Rule_Set.Empty, |
712 erls = Atools_erls, srls = Rule_Set.Empty, |
700 calc = [], errpatts = [], |
713 calc = [], errpatts = [], |