189 \<^rule_eval>\<open>kleiner\<close> (eval_kleiner ""), |
189 \<^rule_eval>\<open>kleiner\<close> (eval_kleiner ""), |
190 \<^rule_eval>\<open>ist_monom\<close> (eval_ist_monom "")]; |
190 \<^rule_eval>\<open>ist_monom\<close> (eval_ist_monom "")]; |
191 |
191 |
192 val ordne_alphabetisch = |
192 val ordne_alphabetisch = |
193 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], |
193 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], |
194 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], |
194 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [], |
195 erls = erls_ordne_alphabetisch, |
195 erls = erls_ordne_alphabetisch, |
196 rules = [ |
196 rules = [ |
197 \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*) |
197 \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*) |
198 \<^rule_thm>\<open>tausche_minus\<close>, (*"b kleiner a ==> (b - a) = (-a + b)"*) |
198 \<^rule_thm>\<open>tausche_minus\<close>, (*"b kleiner a ==> (b - a) = (-a + b)"*) |
199 \<^rule_thm>\<open>tausche_vor_plus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*) |
199 \<^rule_thm>\<open>tausche_vor_plus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*) |
204 \<^rule_thm>\<open>tausche_minus_minus\<close>], (*"c kleiner b ==> (a - c - b) = (a - b - c)"*) |
204 \<^rule_thm>\<open>tausche_minus_minus\<close>], (*"c kleiner b ==> (a - c - b) = (a - b - c)"*) |
205 scr = Rule.Empty_Prog}; |
205 scr = Rule.Empty_Prog}; |
206 |
206 |
207 val fasse_zusammen = |
207 val fasse_zusammen = |
208 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], |
208 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], |
209 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
209 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
210 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty |
210 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty |
211 [\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")], |
211 [\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")], |
212 srls = Rule_Set.Empty, calc = [], errpatts = [], |
212 srls = Rule_Set.Empty, calc = [], errpatts = [], |
213 rules = [ |
213 rules = [ |
214 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
214 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
246 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_num |] ==> - v - m * v = (-1 - m) * v"*) |
246 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_num |] ==> - v - m * v = (-1 - m) * v"*) |
247 scr = Rule.Empty_Prog}; |
247 scr = Rule.Empty_Prog}; |
248 |
248 |
249 val verschoenere = |
249 val verschoenere = |
250 Rule_Def.Repeat{id = "verschoenere", preconds = [], |
250 Rule_Def.Repeat{id = "verschoenere", preconds = [], |
251 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], |
251 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [], |
252 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty |
252 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty |
253 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")], |
253 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")], |
254 rules = [ |
254 rules = [ |
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"*) |
266 \<^rule_thm>\<open>vor_minus_mal\<close>], (*"- a * b = (-a) * b"*) |
266 \<^rule_thm>\<open>vor_minus_mal\<close>], (*"- a * b = (-a) * b"*) |
267 scr = Rule.Empty_Prog}; |
267 scr = Rule.Empty_Prog}; |
268 |
268 |
269 val klammern_aufloesen = |
269 val klammern_aufloesen = |
270 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], |
270 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], |
271 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, |
271 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, |
272 calc = [], errpatts = [], erls = Rule_Set.Empty, |
272 calc = [], errpatts = [], erls = Rule_Set.Empty, |
273 rules = [ |
273 rules = [ |
274 \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*) |
274 \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*) |
275 \<^rule_thm>\<open>klammer_plus_minus\<close>, (*"a + (b - c) = (a + b) - c"*) |
275 \<^rule_thm>\<open>klammer_plus_minus\<close>, (*"a + (b - c) = (a + b) - c"*) |
276 \<^rule_thm>\<open>klammer_minus_plus\<close>, (*"a - (b + c) = (a - b) - c"*) |
276 \<^rule_thm>\<open>klammer_minus_plus\<close>, (*"a - (b + c) = (a - b) - c"*) |
277 \<^rule_thm>\<open>klammer_minus_minus\<close>], (*"a - (b - c) = (a - b) + c"*) |
277 \<^rule_thm>\<open>klammer_minus_minus\<close>], (*"a - (b - c) = (a - b) + c"*) |
278 scr = Rule.Empty_Prog}; |
278 scr = Rule.Empty_Prog}; |
279 |
279 |
280 val klammern_ausmultiplizieren = |
280 val klammern_ausmultiplizieren = |
281 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], |
281 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], |
282 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, |
282 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, |
283 calc = [], errpatts = [], erls = Rule_Set.Empty, |
283 calc = [], errpatts = [], erls = Rule_Set.Empty, |
284 rules = [ |
284 rules = [ |
285 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
285 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
286 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
286 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
287 |
287 |
289 \<^rule_thm>\<open>klammer_minus_mult\<close>], (*"(b - c) * a = b * a - c * a"*) |
289 \<^rule_thm>\<open>klammer_minus_mult\<close>], (*"(b - c) * a = b * a - c * a"*) |
290 scr = Rule.Empty_Prog}; |
290 scr = Rule.Empty_Prog}; |
291 |
291 |
292 val ordne_monome = |
292 val ordne_monome = |
293 Rule_Def.Repeat { |
293 Rule_Def.Repeat { |
294 id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
294 id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
295 srls = Rule_Set.Empty, calc = [], errpatts = [], |
295 srls = Rule_Set.Empty, calc = [], errpatts = [], |
296 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [ |
296 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [ |
297 \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""), |
297 \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""), |
298 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")], |
298 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")], |
299 rules = [ |
299 rules = [ |