743 \<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>, |
743 \<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>, |
744 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*) |
744 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*) |
745 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>, |
745 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>, |
746 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*) |
746 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*) |
747 |
747 |
748 Rule.Thm ("real_add_mult_distrib_poly", |
748 \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>, |
749 ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}), |
|
750 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
749 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
751 Rule.Thm("real_add_mult_distrib2_poly", |
750 \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>, |
752 ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}), |
|
753 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
751 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
754 |
752 |
755 \<^rule_thm>\<open>realpow_multI_poly\<close>, |
753 \<^rule_thm>\<open>realpow_multI_poly\<close>, |
756 (*"[| r is_polyexp; s is_polyexp |] ==> |
754 (*"[| r is_polyexp; s is_polyexp |] ==> |
757 (r * s) \<up> n = r \<up> n * s \<up> n"*) |
755 (r * s) \<up> n = r \<up> n * s \<up> n"*) |
771 \<^rule_thm>\<open>realpow_twoI_assoc_l\<close>, |
769 \<^rule_thm>\<open>realpow_twoI_assoc_l\<close>, |
772 (*"r * (r * s) = r \<up> 2 * s"*) |
770 (*"r * (r * s) = r \<up> 2 * s"*) |
773 |
771 |
774 \<^rule_thm>\<open>realpow_plus_1\<close>, |
772 \<^rule_thm>\<open>realpow_plus_1\<close>, |
775 (*"r * r \<up> n = r \<up> (n + 1)"*) |
773 (*"r * r \<up> n = r \<up> (n + 1)"*) |
776 Rule.Thm ("realpow_plus_1_assoc_l", |
774 \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>, |
777 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}), |
|
778 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*) |
775 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*) |
779 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *) |
776 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *) |
780 Rule.Thm ("realpow_plus_1_assoc_l2", |
777 \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>, |
781 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}), |
|
782 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*) |
778 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*) |
783 |
779 |
784 \<^rule_thm_sym>\<open>realpow_addI\<close>, |
780 \<^rule_thm_sym>\<open>realpow_addI\<close>, |
785 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*) |
781 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*) |
786 \<^rule_thm>\<open>realpow_addI_assoc_l\<close>, |
782 \<^rule_thm>\<open>realpow_addI_assoc_l\<close>, |
893 |
889 |
894 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
890 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
895 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*) |
891 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*) |
896 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>, |
892 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>, |
897 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*) |
893 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*) |
898 Rule.Thm ("real_plus_minus_binom1_p", |
894 \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>, |
899 ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}), |
|
900 (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*) |
895 (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*) |
901 Rule.Thm ("real_plus_minus_binom2_p", |
896 \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>, |
902 ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}), |
|
903 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*) |
897 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*) |
904 |
898 |
905 \<^rule_thm>\<open>minus_minus\<close>, |
899 \<^rule_thm>\<open>minus_minus\<close>, |
906 (*"- (- ?z) = ?z"*) |
900 (*"- (- ?z) = ?z"*) |
907 \<^rule_thm>\<open>real_diff_minus\<close>, |
901 \<^rule_thm>\<open>real_diff_minus\<close>, |
908 (*"a - b = a + -1 * b"*) |
902 (*"a - b = a + -1 * b"*) |
909 \<^rule_thm_sym>\<open>real_mult_minus1\<close> |
903 \<^rule_thm_sym>\<open>real_mult_minus1\<close> |
910 (*- ?z = "-1 * ?z"*) |
904 (*- ?z = "-1 * ?z"*) |
911 |
905 |
912 (*Rule.Thm ("real_minus_add_distrib", |
906 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) |
913 ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*) |
|
914 (*"- (?x + ?y) = - ?x + - ?y"*) |
907 (*"- (?x + ?y) = - ?x + - ?y"*) |
915 (*\<^rule_thm>\<open>real_diff_plus\<close>*) |
908 (*\<^rule_thm>\<open>real_diff_plus\<close>*) |
916 (*"a - b = a + -b"*) |
909 (*"a - b = a + -b"*) |
917 ], scr = Rule.Empty_Prog}; |
910 ], scr = Rule.Empty_Prog}; |
918 |
911 |
966 calc = [], errpatts = [], |
959 calc = [], errpatts = [], |
967 rules = [\<^rule_thm>\<open>mult_1_left\<close>, |
960 rules = [\<^rule_thm>\<open>mult_1_left\<close>, |
968 (*"1 * z = z"*) |
961 (*"1 * z = z"*) |
969 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*) |
962 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*) |
970 (*"-1 * z = - z"*) |
963 (*"-1 * z = - z"*) |
971 Rule.Thm ("minus_mult_left", |
964 Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})), |
972 ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})), |
|
973 (*- (?x * ?y) = "- ?x * ?y"*) |
965 (*- (?x * ?y) = "- ?x * ?y"*) |
974 (*Rule.Thm ("real_minus_mult_cancel", |
966 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, |
975 ThmC.numerals_to_Free @{thm real_minus_mult_cancel}), |
|
976 (*"- ?x * - ?y = ?x * ?y"*)---*) |
967 (*"- ?x * - ?y = ?x * ?y"*)---*) |
977 \<^rule_thm>\<open>mult_zero_left\<close>, |
968 \<^rule_thm>\<open>mult_zero_left\<close>, |
978 (*"0 * z = 0"*) |
969 (*"0 * z = 0"*) |
979 \<^rule_thm>\<open>add_0_left\<close>, |
970 \<^rule_thm>\<open>add_0_left\<close>, |
980 (*"0 + z = z"*) |
971 (*"0 + z = z"*) |
1287 erls = Atools_erls, srls = Rule_Set.Empty, |
1278 erls = Atools_erls, srls = Rule_Set.Empty, |
1288 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1279 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1289 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1280 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1290 ("POWER", ("Transcendental.powr", eval_binop "#power_")) |
1281 ("POWER", ("Transcendental.powr", eval_binop "#power_")) |
1291 ], errpatts = [], |
1282 ], errpatts = [], |
1292 rules = [Rule.Thm ("real_plus_binom_pow2", |
1283 rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
1293 ThmC.numerals_to_Free @{thm real_plus_binom_pow2}), |
|
1294 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
1284 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
1295 Rule.Thm ("real_plus_binom_times", |
1285 \<^rule_thm>\<open>real_plus_binom_times\<close>, |
1296 ThmC.numerals_to_Free @{thm real_plus_binom_times}), |
|
1297 (*"(a + b)*(a + b) = ...*) |
1286 (*"(a + b)*(a + b) = ...*) |
1298 Rule.Thm ("real_minus_binom_pow2", |
1287 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, |
1299 ThmC.numerals_to_Free @{thm real_minus_binom_pow2}), |
|
1300 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
1288 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
1301 Rule.Thm ("real_minus_binom_times", |
1289 \<^rule_thm>\<open>real_minus_binom_times\<close>, |
1302 ThmC.numerals_to_Free @{thm real_minus_binom_times}), |
|
1303 (*"(a - b)*(a - b) = ...*) |
1290 (*"(a - b)*(a - b) = ...*) |
1304 Rule.Thm ("real_plus_minus_binom1", |
1291 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, |
1305 ThmC.numerals_to_Free @{thm real_plus_minus_binom1}), |
|
1306 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*) |
1292 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*) |
1307 Rule.Thm ("real_plus_minus_binom2", |
1293 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, |
1308 ThmC.numerals_to_Free @{thm real_plus_minus_binom2}), |
|
1309 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*) |
1294 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*) |
1310 (*RL 020915*) |
1295 (*RL 020915*) |
1311 \<^rule_thm>\<open>real_pp_binom_times\<close>, |
1296 \<^rule_thm>\<open>real_pp_binom_times\<close>, |
1312 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
1297 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
1313 \<^rule_thm>\<open>real_pm_binom_times\<close>, |
1298 \<^rule_thm>\<open>real_pm_binom_times\<close>, |
1318 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*) |
1303 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*) |
1319 \<^rule_thm>\<open>realpow_multI\<close>, |
1304 \<^rule_thm>\<open>realpow_multI\<close>, |
1320 (*(a*b) \<up> n = a \<up> n * b \<up> n*) |
1305 (*(a*b) \<up> n = a \<up> n * b \<up> n*) |
1321 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, |
1306 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, |
1322 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *) |
1307 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *) |
1323 Rule.Thm ("real_minus_binom_pow3", |
1308 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, |
1324 ThmC.numerals_to_Free @{thm real_minus_binom_pow3}), |
|
1325 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *) |
1309 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *) |
1326 |
1310 |
1327 |
1311 |
1328 (*\<^rule_thm>\<open>distrib_right\<close>, |
1312 (*\<^rule_thm>\<open>distrib_right\<close>, |
1329 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
1313 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
1343 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1327 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1344 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1328 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1345 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"), |
1329 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"), |
1346 (*\<^rule_thm>\<open>mult.commute\<close>, |
1330 (*\<^rule_thm>\<open>mult.commute\<close>, |
1347 (*AC-rewriting*) |
1331 (*AC-rewriting*) |
1348 Rule.Thm ("real_mult_left_commute", |
1332 \<^rule_thm>\<open>real_mult_left_commute\<close>, |
1349 ThmC.numerals_to_Free @{thm real_mult_left_commute}), |
|
1350 \<^rule_thm>\<open>mult.assoc\<close>, |
1333 \<^rule_thm>\<open>mult.assoc\<close>, |
1351 \<^rule_thm>\<open>add.commute\<close>, |
1334 \<^rule_thm>\<open>add.commute\<close>, |
1352 \<^rule_thm>\<open>add.left_commute\<close>, |
1335 \<^rule_thm>\<open>add.left_commute\<close>, |
1353 \<^rule_thm>\<open>add.assoc\<close>, |
1336 \<^rule_thm>\<open>add.assoc\<close>, |
1354 *) |
1337 *) |
1361 \<^rule_thm>\<open>real_mult_2_assoc\<close>, |
1344 \<^rule_thm>\<open>real_mult_2_assoc\<close>, |
1362 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
1345 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
1363 |
1346 |
1364 \<^rule_thm>\<open>real_num_collect\<close>, |
1347 \<^rule_thm>\<open>real_num_collect\<close>, |
1365 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*) |
1348 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*) |
1366 Rule.Thm ("real_num_collect_assoc", |
1349 \<^rule_thm>\<open>real_num_collect_assoc\<close>, |
1367 ThmC.numerals_to_Free @{thm real_num_collect_assoc}), |
|
1368 (*"[| l is_const; m is_const |] ==> |
1350 (*"[| l is_const; m is_const |] ==> |
1369 l * n + (m * n + k) = (l + m) * n + k"*) |
1351 l * n + (m * n + k) = (l + m) * n + k"*) |
1370 \<^rule_thm>\<open>real_one_collect\<close>, |
1352 \<^rule_thm>\<open>real_one_collect\<close>, |
1371 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
1353 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
1372 Rule.Thm ("real_one_collect_assoc", |
1354 \<^rule_thm>\<open>real_one_collect_assoc\<close>, |
1373 ThmC.numerals_to_Free @{thm real_one_collect_assoc}), |
|
1374 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
1355 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
1375 |
1356 |
1376 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1357 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1377 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1358 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1378 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_") |
1359 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_") |