2762 Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
2762 Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
2763 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *) |
2763 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *) |
2764 rules = |
2764 rules = |
2765 [Calc ("op =",eval_equal "#equal_"), |
2765 [Calc ("op =",eval_equal "#equal_"), |
2766 Calc ("Atools.is'_const",eval_const "#is_const_"), |
2766 Calc ("Atools.is'_const",eval_const "#is_const_"), |
2767 Thm ("not_true",num_str not_true), |
2767 Thm ("not_true",num_str @{not_true), |
2768 Thm ("not_false",num_str not_false) |
2768 Thm ("not_false",num_str @{not_false) |
2769 ], |
2769 ], |
2770 scr = EmptyScr}); |
2770 scr = EmptyScr}); |
2771 |
2771 |
2772 |
2772 |
2773 (*.simplifies expressions with numerals; |
2773 (*.simplifies expressions with numerals; |
2780 calc = [], |
2780 calc = [], |
2781 rules = |
2781 rules = |
2782 [Calc ("HOL.divide" ,eval_cancel "#divide_"), |
2782 [Calc ("HOL.divide" ,eval_cancel "#divide_"), |
2783 |
2783 |
2784 Thm ("minus_divide_left", |
2784 Thm ("minus_divide_left", |
2785 num_str (real_minus_divide_eq RS sym)), |
2785 num_str @{(real_minus_divide_eq RS sym)), |
2786 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*) |
2786 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*) |
2787 |
2787 |
2788 Thm ("rat_add",num_str rat_add), |
2788 Thm ("rat_add",num_str @{rat_add), |
2789 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \ |
2789 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \ |
2790 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*) |
2790 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*) |
2791 Thm ("rat_add1",num_str rat_add1), |
2791 Thm ("rat_add1",num_str @{rat_add1), |
2792 (*"[| a is_const; b is_const; c is_const |] ==> \ |
2792 (*"[| a is_const; b is_const; c is_const |] ==> \ |
2793 \"a / c + b / c = (a + b) / c"*) |
2793 \"a / c + b / c = (a + b) / c"*) |
2794 Thm ("rat_add2",num_str rat_add2), |
2794 Thm ("rat_add2",num_str @{rat_add2), |
2795 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> \ |
2795 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> \ |
2796 \?a / ?c + ?b = (?a + ?b * ?c) / ?c"*) |
2796 \?a / ?c + ?b = (?a + ?b * ?c) / ?c"*) |
2797 Thm ("rat_add3",num_str rat_add3), |
2797 Thm ("rat_add3",num_str @{rat_add3), |
2798 (*"[| a is_const; b is_const; c is_const |] ==> \ |
2798 (*"[| a is_const; b is_const; c is_const |] ==> \ |
2799 \"a + b / c = (a * c) / c + b / c"\ |
2799 \"a + b / c = (a * c) / c + b / c"\ |
2800 \.... is_const to be omitted here FIXME*) |
2800 \.... is_const to be omitted here FIXME*) |
2801 |
2801 |
2802 Thm ("rat_mult",num_str rat_mult), |
2802 Thm ("rat_mult",num_str @{rat_mult), |
2803 (*a / b * (c / d) = a * c / (b * d)*) |
2803 (*a / b * (c / d) = a * c / (b * d)*) |
2804 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
2804 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
2805 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
2805 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
2806 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
2806 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
2807 (*?y / ?z * ?x = ?y * ?x / ?z*) |
2807 (*?y / ?z * ?x = ?y * ?x / ?z*) |
2808 |
2808 |
2809 Thm ("real_divide_divide1",num_str real_divide_divide1), |
2809 Thm ("real_divide_divide1",num_str @{real_divide_divide1), |
2810 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*) |
2810 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*) |
2811 Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}), |
2811 Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}), |
2812 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
2812 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
2813 |
2813 |
2814 Thm ("rat_power", num_str rat_power), |
2814 Thm ("rat_power", num_str @{rat_power), |
2815 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
2815 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
2816 |
2816 |
2817 Thm ("mult_cross",num_str mult_cross), |
2817 Thm ("mult_cross",num_str @{mult_cross), |
2818 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*) |
2818 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*) |
2819 Thm ("mult_cross1",num_str mult_cross1), |
2819 Thm ("mult_cross1",num_str @{mult_cross1), |
2820 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*) |
2820 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*) |
2821 Thm ("mult_cross2",num_str mult_cross2) |
2821 Thm ("mult_cross2",num_str @{mult_cross2) |
2822 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*) |
2822 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*) |
2823 ], scr = EmptyScr}) |
2823 ], scr = EmptyScr}) |
2824 calculate_Poly); |
2824 calculate_Poly); |
2825 |
2825 |
2826 |
2826 |
2910 fun init_state thy eval_rls ro t = |
2910 fun init_state thy eval_rls ro t = |
2911 let val SOME (t',_) = factout_p_ thy t |
2911 let val SOME (t',_) = factout_p_ thy t |
2912 val SOME (t'',asm) = cancel_p_ thy t |
2912 val SOME (t'',asm) = cancel_p_ thy t |
2913 val der = reverse_deriv thy eval_rls rules ro NONE t' |
2913 val der = reverse_deriv thy eval_rls rules ro NONE t' |
2914 val der = der @ [(Thm ("real_mult_div_cancel2", |
2914 val der = der @ [(Thm ("real_mult_div_cancel2", |
2915 num_str real_mult_div_cancel2), |
2915 num_str @{real_mult_div_cancel2), |
2916 (t'',asm))] |
2916 (t'',asm))] |
2917 val rs = (distinct_Thm o (map #1)) der |
2917 val rs = (distinct_Thm o (map #1)) der |
2918 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
2918 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
2919 "sym_real_mult_0", |
2919 "sym_real_mult_0", |
2920 "sym_real_mult_1" |
2920 "sym_real_mult_1" |
3041 fun init_state thy eval_rls ro t = |
3041 fun init_state thy eval_rls ro t = |
3042 let val SOME (t',_) = factout_ thy t; |
3042 let val SOME (t',_) = factout_ thy t; |
3043 val SOME (t'',asm) = cancel_ thy t; |
3043 val SOME (t'',asm) = cancel_ thy t; |
3044 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3044 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3045 val der = der @ [(Thm ("real_mult_div_cancel2", |
3045 val der = der @ [(Thm ("real_mult_div_cancel2", |
3046 num_str real_mult_div_cancel2), |
3046 num_str @{real_mult_div_cancel2), |
3047 (t'',asm))] |
3047 (t'',asm))] |
3048 val rs = map #1 der; |
3048 val rs = map #1 der; |
3049 in (t,t'',[rs],der) end; |
3049 in (t,t'',[rs],der) end; |
3050 |
3050 |
3051 fun locate_rule thy eval_rls ro [rs] t r = |
3051 fun locate_rule thy eval_rls ro [rs] t r = |
3135 fun init_state thy eval_rls ro t = |
3135 fun init_state thy eval_rls ro t = |
3136 let val SOME (t',_) = common_nominator_p_ thy t; |
3136 let val SOME (t',_) = common_nominator_p_ thy t; |
3137 val SOME (t'',asm) = add_fraction_p_ thy t; |
3137 val SOME (t'',asm) = add_fraction_p_ thy t; |
3138 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3138 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3139 val der = der @ [(Thm ("real_mult_div_cancel2", |
3139 val der = der @ [(Thm ("real_mult_div_cancel2", |
3140 num_str real_mult_div_cancel2), |
3140 num_str @{real_mult_div_cancel2), |
3141 (t'',asm))] |
3141 (t'',asm))] |
3142 val rs = (distinct_Thm o (map #1)) der; |
3142 val rs = (distinct_Thm o (map #1)) der; |
3143 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
3143 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
3144 "sym_real_mult_0", |
3144 "sym_real_mult_0", |
3145 "sym_real_mult_1"]) rs; |
3145 "sym_real_mult_1"]) rs; |
3284 fun init_state thy eval_rls ro t = |
3284 fun init_state thy eval_rls ro t = |
3285 let val SOME (t',_) = common_nominator_ thy t; |
3285 let val SOME (t',_) = common_nominator_ thy t; |
3286 val SOME (t'',asm) = add_fraction_ thy t; |
3286 val SOME (t'',asm) = add_fraction_ thy t; |
3287 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3287 val der = reverse_deriv thy eval_rls rules ro NONE t'; |
3288 val der = der @ [(Thm ("real_mult_div_cancel2", |
3288 val der = der @ [(Thm ("real_mult_div_cancel2", |
3289 num_str real_mult_div_cancel2), |
3289 num_str @{real_mult_div_cancel2), |
3290 (t'',asm))] |
3290 (t'',asm))] |
3291 val rs = (distinct_Thm o (map #1)) der; |
3291 val rs = (distinct_Thm o (map #1)) der; |
3292 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
3292 val rs = filter_out (eq_Thms ["sym_real_add_zero_left", |
3293 "sym_real_mult_0", |
3293 "sym_real_mult_0", |
3294 "sym_real_mult_1"]) rs; |
3294 "sym_real_mult_1"]) rs; |
3455 unary minus before numerals are put into the numeral by parsing; |
3455 unary minus before numerals are put into the numeral by parsing; |
3456 contains absolute minimum of thms for context in norm_Rational .*) |
3456 contains absolute minimum of thms for context in norm_Rational .*) |
3457 val discard_minus = prep_rls( |
3457 val discard_minus = prep_rls( |
3458 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
3458 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
3459 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
3459 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
3460 rules = [Thm ("real_diff_minus", num_str real_diff_minus), |
3460 rules = [Thm ("real_diff_minus", num_str @{real_diff_minus), |
3461 (*"a - b = a + -1 * b"*) |
3461 (*"a - b = a + -1 * b"*) |
3462 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)) |
3462 Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym)) |
3463 (*- ?z = "-1 * ?z"*) |
3463 (*- ?z = "-1 * ?z"*) |
3464 ], |
3464 ], |
3465 scr = Script ((term_of o the o (parse thy)) |
3465 scr = Script ((term_of o the o (parse thy)) |
3466 "empty_script") |
3466 "empty_script") |
3467 }):rls; |
3467 }):rls; |
3482 (*.all powers over + distributed; atoms over * collected, other distributed |
3482 (*.all powers over + distributed; atoms over * collected, other distributed |
3483 contains absolute minimum of thms for context in norm_Rational .*) |
3483 contains absolute minimum of thms for context in norm_Rational .*) |
3484 val powers = prep_rls( |
3484 val powers = prep_rls( |
3485 Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
3485 Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
3486 erls = powers_erls, srls = Erls, calc = [], (*asm_thm = [],*) |
3486 erls = powers_erls, srls = Erls, calc = [], (*asm_thm = [],*) |
3487 rules = [Thm ("realpow_multI", num_str realpow_multI), |
3487 rules = [Thm ("realpow_multI", num_str @{realpow_multI), |
3488 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
3488 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
3489 Thm ("realpow_pow",num_str realpow_pow), |
3489 Thm ("realpow_pow",num_str @{realpow_pow), |
3490 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
3490 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
3491 Thm ("realpow_oneI",num_str realpow_oneI), |
3491 Thm ("realpow_oneI",num_str @{realpow_oneI), |
3492 (*"r ^^^ 1 = r"*) |
3492 (*"r ^^^ 1 = r"*) |
3493 Thm ("realpow_minus_even",num_str realpow_minus_even), |
3493 Thm ("realpow_minus_even",num_str @{realpow_minus_even), |
3494 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*) |
3494 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*) |
3495 Thm ("realpow_minus_odd",num_str realpow_minus_odd), |
3495 Thm ("realpow_minus_odd",num_str @{realpow_minus_odd), |
3496 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*) |
3496 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*) |
3497 |
3497 |
3498 (*----- collect atoms over * -----*) |
3498 (*----- collect atoms over * -----*) |
3499 Thm ("realpow_two_atom",num_str realpow_two_atom), |
3499 Thm ("realpow_two_atom",num_str @{realpow_two_atom), |
3500 (*"r is_atom ==> r * r = r ^^^ 2"*) |
3500 (*"r is_atom ==> r * r = r ^^^ 2"*) |
3501 Thm ("realpow_plus_1",num_str realpow_plus_1), |
3501 Thm ("realpow_plus_1",num_str @{realpow_plus_1), |
3502 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*) |
3502 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*) |
3503 Thm ("realpow_addI_atom",num_str realpow_addI_atom), |
3503 Thm ("realpow_addI_atom",num_str @{realpow_addI_atom), |
3504 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*) |
3504 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*) |
3505 |
3505 |
3506 (*----- distribute none-atoms -----*) |
3506 (*----- distribute none-atoms -----*) |
3507 Thm ("realpow_def_atom",num_str realpow_def_atom), |
3507 Thm ("realpow_def_atom",num_str @{realpow_def_atom), |
3508 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*) |
3508 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*) |
3509 Thm ("realpow_eq_oneI",num_str realpow_eq_oneI), |
3509 Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI), |
3510 (*"1 ^^^ n = 1"*) |
3510 (*"1 ^^^ n = 1"*) |
3511 Calc ("op +",eval_binop "#add_") |
3511 Calc ("op +",eval_binop "#add_") |
3512 ], |
3512 ], |
3513 scr = Script ((term_of o the o (parse thy)) |
3513 scr = Script ((term_of o the o (parse thy)) |
3514 "empty_script") |
3514 "empty_script") |
3516 (*.contains absolute minimum of thms for context in norm_Rational.*) |
3516 (*.contains absolute minimum of thms for context in norm_Rational.*) |
3517 val rat_mult_divide = prep_rls( |
3517 val rat_mult_divide = prep_rls( |
3518 Rls {id = "rat_mult_divide", preconds = [], |
3518 Rls {id = "rat_mult_divide", preconds = [], |
3519 rew_ord = ("dummy_ord",dummy_ord), |
3519 rew_ord = ("dummy_ord",dummy_ord), |
3520 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
3520 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
3521 rules = [Thm ("rat_mult",num_str rat_mult), |
3521 rules = [Thm ("rat_mult",num_str @{rat_mult), |
3522 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3522 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3523 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
3523 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
3524 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
3524 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
3525 otherwise inv.to a / b / c = ...*) |
3525 otherwise inv.to a / b / c = ...*) |
3526 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
3526 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
3541 erls = e_rls,srls = Erls,calc = [],(*asm_thm = [],*) |
3541 erls = e_rls,srls = Erls,calc = [],(*asm_thm = [],*) |
3542 rules = [(*Thm ("divide_1",num_str @{thm divide_1}), |
3542 rules = [(*Thm ("divide_1",num_str @{thm divide_1}), |
3543 "?x / 1 = ?x" unnecess.for normalform*) |
3543 "?x / 1 = ?x" unnecess.for normalform*) |
3544 Thm ("mult_1_left",num_str @{thm mult_1_left}), |
3544 Thm ("mult_1_left",num_str @{thm mult_1_left}), |
3545 (*"1 * z = z"*) |
3545 (*"1 * z = z"*) |
3546 (*Thm ("real_mult_minus1",num_str real_mult_minus1), |
3546 (*Thm ("real_mult_minus1",num_str @{real_mult_minus1), |
3547 "-1 * z = - z"*) |
3547 "-1 * z = - z"*) |
3548 (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel), |
3548 (*Thm ("real_minus_mult_cancel",num_str @{real_minus_mult_cancel), |
3549 "- ?x * - ?y = ?x * ?y"*) |
3549 "- ?x * - ?y = ?x * ?y"*) |
3550 |
3550 |
3551 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
3551 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
3552 (*"0 * z = 0"*) |
3552 (*"0 * z = 0"*) |
3553 Thm ("add_0_left",num_str @{thm add_0_left}), |
3553 Thm ("add_0_left",num_str @{thm add_0_left}), |
3554 (*"0 + z = z"*) |
3554 (*"0 + z = z"*) |
3555 (*Thm ("right_minus",num_str @{thm right_minus}), |
3555 (*Thm ("right_minus",num_str @{thm right_minus}), |
3556 "?z + - ?z = 0"*) |
3556 "?z + - ?z = 0"*) |
3557 |
3557 |
3558 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
3558 Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)), |
3559 (*"z1 + z1 = 2 * z1"*) |
3559 (*"z1 + z1 = 2 * z1"*) |
3560 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc), |
3560 Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc), |
3561 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
3561 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
3562 |
3562 |
3563 Thm ("divide_zero_left",num_str @{thm divide_zero_left}) |
3563 Thm ("divide_zero_left",num_str @{thm divide_zero_left}) |
3564 (*"0 / ?x = 0"*) |
3564 (*"0 / ?x = 0"*) |
3565 ], scr = EmptyScr}:rls); |
3565 ], scr = EmptyScr}:rls); |
3615 val simplify_rational = |
3615 val simplify_rational = |
3616 merge_rls "simplify_rational" expand_binoms |
3616 merge_rls "simplify_rational" expand_binoms |
3617 (append_rls "divide" calculate_Rational |
3617 (append_rls "divide" calculate_Rational |
3618 [Thm ("divide_1",num_str @{thm divide_1}), |
3618 [Thm ("divide_1",num_str @{thm divide_1}), |
3619 (*"?x / 1 = ?x"*) |
3619 (*"?x / 1 = ?x"*) |
3620 Thm ("rat_mult",num_str rat_mult), |
3620 Thm ("rat_mult",num_str @{rat_mult), |
3621 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3621 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3622 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
3622 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
3623 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
3623 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
3624 otherwise inv.to a / b / c = ...*) |
3624 otherwise inv.to a / b / c = ...*) |
3625 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
3625 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
3626 (*"?a / ?b * ?c = ?a * ?c / ?b"*) |
3626 (*"?a / ?b * ?c = ?a * ?c / ?b"*) |
3627 Thm ("add_minus",num_str add_minus), |
3627 Thm ("add_minus",num_str @{add_minus), |
3628 (*"?a + ?b - ?b = ?a"*) |
3628 (*"?a + ?b - ?b = ?a"*) |
3629 Thm ("add_minus1",num_str add_minus1), |
3629 Thm ("add_minus1",num_str @{add_minus1), |
3630 (*"?a - ?b + ?b = ?a"*) |
3630 (*"?a - ?b + ?b = ?a"*) |
3631 Thm ("real_divide_minus1",num_str real_divide_minus1) |
3631 Thm ("real_divide_minus1",num_str @{real_divide_minus1) |
3632 (*"?x / -1 = - ?x"*) |
3632 (*"?x / -1 = - ?x"*) |
3633 (* |
3633 (* |
3634 , |
3634 , |
3635 Thm ("",num_str ) |
3635 Thm ("",num_str @{) |
3636 *) |
3636 *) |
3637 ]); |
3637 ]); |
3638 |
3638 |
3639 (*---------vvv-------------MG ab 1.07.2003--------------vvv-----------*) |
3639 (*---------vvv-------------MG ab 1.07.2003--------------vvv-----------*) |
3640 |
3640 |
3672 rew_ord = ("dummy_ord",dummy_ord), |
3672 rew_ord = ("dummy_ord",dummy_ord), |
3673 erls = append_rls "e_rls-is_polyexp" e_rls |
3673 erls = append_rls "e_rls-is_polyexp" e_rls |
3674 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
3674 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
3675 srls = Erls, calc = [], |
3675 srls = Erls, calc = [], |
3676 rules = |
3676 rules = |
3677 [Thm ("rat_mult_poly_l",num_str rat_mult_poly_l), |
3677 [Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l), |
3678 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
3678 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
3679 Thm ("rat_mult_poly_r",num_str rat_mult_poly_r) |
3679 Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r) |
3680 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
3680 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
3681 ], |
3681 ], |
3682 scr = EmptyScr}); |
3682 scr = EmptyScr}); |
3683 (* ------------------------------------------------------------------ *) |
3683 (* ------------------------------------------------------------------ *) |
3684 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
3684 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; |
3694 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
3694 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
3695 with this correction ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ we get |
3695 with this correction ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ we get |
3696 error "rational.sml.sml: diff.behav. in norm_Rational_mg 29" etc. |
3696 error "rational.sml.sml: diff.behav. in norm_Rational_mg 29" etc. |
3697 thus we decided to go on with this flaw*) |
3697 thus we decided to go on with this flaw*) |
3698 srls = Erls, calc = [], |
3698 srls = Erls, calc = [], |
3699 rules = [Thm ("rat_mult",num_str rat_mult), |
3699 rules = [Thm ("rat_mult",num_str @{rat_mult), |
3700 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3700 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
3701 Thm ("rat_mult_poly_l",num_str rat_mult_poly_l), |
3701 Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l), |
3702 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
3702 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
3703 Thm ("rat_mult_poly_r",num_str rat_mult_poly_r), |
3703 Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r), |
3704 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
3704 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
3705 |
3705 |
3706 Thm ("real_divide_divide1_mg", real_divide_divide1_mg), |
3706 Thm ("real_divide_divide1_mg", real_divide_divide1_mg), |
3707 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) |
3707 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) |
3708 Thm ("divide_divide_eq_right", real_divide_divide1_eq), |
3708 Thm ("divide_divide_eq_right", real_divide_divide1_eq), |
3709 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
3709 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
3710 Thm ("divide_divide_eq_left", real_divide_divide2_eq), |
3710 Thm ("divide_divide_eq_left", real_divide_divide2_eq), |
3711 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
3711 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
3712 Calc ("HOL.divide" ,eval_cancel "#divide_"), |
3712 Calc ("HOL.divide" ,eval_cancel "#divide_"), |
3713 |
3713 |
3714 Thm ("rat_power", num_str rat_power) |
3714 Thm ("rat_power", num_str @{rat_power) |
3715 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
3715 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
3716 ], |
3716 ], |
3717 scr = Script ((term_of o the o (parse thy)) "empty_script") |
3717 scr = Script ((term_of o the o (parse thy)) "empty_script") |
3718 }:rls); |
3718 }:rls); |
3719 (* ------------------------------------------------------------------ *) |
3719 (* ------------------------------------------------------------------ *) |