230 |
230 |
231 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*) |
231 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*) |
232 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*) |
232 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*) |
233 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*) |
233 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*) |
234 |
234 |
235 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
235 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
236 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"), |
236 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_"), |
237 |
237 |
238 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
238 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
239 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
239 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
240 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*) |
240 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*) |
241 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*) |
241 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*) |
255 \<^rule_thm>\<open>vorzeichen_minus_weg1\<close>, (*"l kleiner 0 ==> a + l * b = a - -l * b"*) |
255 \<^rule_thm>\<open>vorzeichen_minus_weg1\<close>, (*"l kleiner 0 ==> a + l * b = a - -l * b"*) |
256 \<^rule_thm>\<open>vorzeichen_minus_weg2\<close>, (*"l kleiner 0 ==> a - l * b = a + -l * b"*) |
256 \<^rule_thm>\<open>vorzeichen_minus_weg2\<close>, (*"l kleiner 0 ==> a - l * b = a + -l * b"*) |
257 \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*) |
257 \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*) |
258 \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) |
258 \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) |
259 |
259 |
260 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
260 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
261 |
261 |
262 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
262 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
263 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
263 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
264 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
264 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
265 \<^rule_thm>\<open>null_minus\<close>, (*"0 - a = -a"*) |
265 \<^rule_thm>\<open>null_minus\<close>, (*"0 - a = -a"*) |
314 Rule.Rls_ ordne_alphabetisch, |
314 Rule.Rls_ ordne_alphabetisch, |
315 Rule.Rls_ fasse_zusammen, |
315 Rule.Rls_ fasse_zusammen, |
316 Rule.Rls_ verschoenere]; |
316 Rule.Rls_ verschoenere]; |
317 val rechnen = |
317 val rechnen = |
318 Rule_Set.append_rules "rechnen" Rule_Set.empty [ |
318 Rule_Set.append_rules "rechnen" Rule_Set.empty [ |
319 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
319 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
320 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
320 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
321 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")]; |
321 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_")]; |
322 \<close> |
322 \<close> |
323 rule_set_knowledge |
323 rule_set_knowledge |
324 ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and |
324 ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and |
325 fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and |
325 fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and |
326 verschoenere = \<open>prep_rls' verschoenere\<close> and |
326 verschoenere = \<open>prep_rls' verschoenere\<close> and |