1 (* attempts to perserve binary minus as wanted by Austrian teachers
3 (c) due to copyright terms
6 theory PolyMinus imports (*Poly// due to "is_ratpolyexp" in...*) Rational begin
10 (*predicates for conditions in rewriting*)
11 kleiner :: "['a, 'a] => bool" ("_ kleiner _")
12 ist_monom :: "'a => bool" ("_ ist'_monom")
15 Probe :: "[bool, bool list] => bool"
16 (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
18 (*descriptions for the pbl and met*)
19 Pruefe :: "bool => una"
20 mitWert :: "bool list => tobooll"
21 Geprueft :: "bool => una"
25 null_minus: "0 - a = -a" and
26 vor_minus_mal: "- a * b = (-a) * b" and
28 (*commute with invariant (a.b).c -association*)
29 tausche_plus: "[| b ist_monom; a kleiner b |] ==>
30 (b + a) = (a + b)" and
31 tausche_minus: "[| b ist_monom; a kleiner b |] ==>
32 (b - a) = (-a + b)" and
33 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
34 (- b + a) = (a - b)" and
35 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
36 (- b - a) = (-a - b)" and
37 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
38 tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
39 tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
40 tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
41 tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
42 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
44 (*commute with invariant (a.b).c -association*)
45 tausche_mal: "[| b is_atom; a kleiner b |] ==>
46 (b * a) = (a * b)" and
47 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
48 (-b * a) = (-a * b)" and
49 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
50 (x * c * b) = (x * b * c)" and
51 x_quadrat: "(x * a) * a = x * a \<up> 2" and
54 subtrahiere: "[| l is_num; m is_num |] ==>
55 m * v - l * v = (m - l) * v" and
56 subtrahiere_von_1: "[| l is_num |] ==>
57 v - l * v = (1 - l) * v" and
58 subtrahiere_1: "[| l is_num; m is_num |] ==>
59 m * v - v = (m - 1) * v" and
61 subtrahiere_x_plus_minus: "[| l is_num; m is_num |] ==>
62 (x + m * v) - l * v = x + (m - l) * v" and
63 subtrahiere_x_plus1_minus: "[| l is_num |] ==>
64 (x + v) - l * v = x + (1 - l) * v" and
65 subtrahiere_x_plus_minus1: "[| m is_num |] ==>
66 (x + m * v) - v = x + (m - 1) * v" and
68 subtrahiere_x_minus_plus: "[| l is_num; m is_num |] ==>
69 (x - m * v) + l * v = x + (-m + l) * v" and
70 subtrahiere_x_minus1_plus: "[| l is_num |] ==>
71 (x - v) + l * v = x + (-1 + l) * v" and
72 subtrahiere_x_minus_plus1: "[| m is_num |] ==>
73 (x - m * v) + v = x + (-m + 1) * v" and
75 subtrahiere_x_minus_minus: "[| l is_num; m is_num |] ==>
76 (x - m * v) - l * v = x + (-m - l) * v" and
77 subtrahiere_x_minus1_minus:"[| l is_num |] ==>
78 (x - v) - l * v = x + (-1 - l) * v" and
79 subtrahiere_x_minus_minus1:"[| m is_num |] ==>
80 (x - m * v) - v = x + (-m - 1) * v" and
83 addiere_vor_minus: "[| l is_num; m is_num |] ==>
84 - (l * v) + m * v = (-l + m) * v" and
85 addiere_eins_vor_minus: "[| m is_num |] ==>
86 - v + m * v = (-1 + m) * v" and
87 subtrahiere_vor_minus: "[| l is_num; m is_num |] ==>
88 - (l * v) - m * v = (-l - m) * v" and
89 subtrahiere_eins_vor_minus:"[| m is_num |] ==>
90 - v - m * v = (-1 - m) * v" and
92 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
93 vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
94 vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
95 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
96 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
97 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
99 (*klammer_plus_plus = (add.assoc RS sym)*)
100 klammer_plus_minus: "a + (b - c) = (a + b) - c" and
101 klammer_minus_plus: "a - (b + c) = (a - b) - c" and
102 klammer_minus_minus: "a - (b - c) = (a - b) + c" and
104 klammer_mult_minus: "a * (b - c) = a * b - a * c" and
105 klammer_minus_mult: "(b - c) * a = b * a - c * a"
108 (** eval functions **)
110 (*. get the identifier from specific monomials; see fun ist_monom .*)
111 fun Free_to_string (Free (str, _)) = str
113 if TermC.is_num t then TermC.string_of_num t else "|||||||||||||"(*the "largest" string*);
115 (* quick and dirty solution just before a field test *)
116 fun identifier (Free (id,_)) = id (* _a_ *)
117 | identifier (Const (\<^const_name>\<open>times\<close>, _) $ t1 $ t2) = (* 2*_a_, a*_b_, 3*a*_b_ *)
119 then Free_to_string t2
122 Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' => (* 3*_a_ \<up> 2 *)
123 if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2
127 Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp =>
128 if TermC.is_atom base andalso TermC.is_atom exp then
129 if TermC.is_num base then "|||||||||||||"
130 else Free_to_string base
132 | _ => "|||||||||||||"))
133 | identifier (Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp) = (* _a_\<up>2, _3_^2 *)
134 if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base
136 | identifier t = (* 12 *)
138 then TermC.string_of_num t
139 else "|||||||||||||" (*the "largest" string*);
141 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
142 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
143 fun eval_kleiner _ _ (p as (Const (\<^const_name>\<open>PolyMinus.kleiner\<close>,_) $ a $ b)) _ =
144 if TermC.is_num b then
145 if TermC.is_num a then (*123 kleiner 32 = True !!!*)
146 if TermC.num_of_term a < TermC.num_of_term b then
147 SOME ((UnparseC.term p) ^ " = True",
148 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
149 else SOME ((UnparseC.term p) ^ " = False",
150 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
151 else (* -1 * -2 kleiner 0 *)
152 SOME ((UnparseC.term p) ^ " = False",
153 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
155 if identifier a < identifier b then
156 SOME ((UnparseC.term p) ^ " = True",
157 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
158 else SOME ((UnparseC.term p) ^ " = False",
159 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
160 | eval_kleiner _ _ _ _ = NONE;
163 if TermC.is_atom t then true
166 Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 =>
167 ist_monom t1 andalso ist_monom t2
168 | Const (\<^const_name>\<open>realpow\<close>, _) $ t1 $ t2 =>
169 ist_monom t1 andalso ist_monom t2
172 (* is this a univariate monomial ? *)
173 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
174 fun eval_ist_monom _ _ (p as (Const (\<^const_name>\<open>PolyMinus.ist_monom\<close>,_) $ a)) _ =
176 SOME ((UnparseC.term p) ^ " = True",
177 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
178 else SOME ((UnparseC.term p) ^ " = False",
179 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
180 | eval_ist_monom _ _ _ _ = NONE;
183 (** rewrite order **)
187 val erls_ordne_alphabetisch =
188 Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty [
189 \<^rule_eval>\<open>kleiner\<close> (eval_kleiner ""),
190 \<^rule_eval>\<open>ist_monom\<close> (eval_ist_monom "")];
192 val ordne_alphabetisch =
193 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
194 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
195 erls = erls_ordne_alphabetisch,
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)"*)
199 \<^rule_thm>\<open>tausche_vor_plus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
200 \<^rule_thm>\<open>tausche_vor_minus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
201 \<^rule_thm>\<open>tausche_plus_plus\<close>, (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
202 \<^rule_thm>\<open>tausche_plus_minus\<close>, (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
203 \<^rule_thm>\<open>tausche_minus_plus\<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};
208 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
209 rew_ord = ("dummy_ord", Rewrite_Ord.function_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_")],
212 srls = Rule_Set.Empty, calc = [], errpatts = [],
214 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
215 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, (*"[| l is_num; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
216 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
217 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
219 \<^rule_thm>\<open>subtrahiere\<close>, (*"[| l is_num; m is_num |] ==> m * v - l * v = (m - l) * v"*)
220 \<^rule_thm>\<open>subtrahiere_von_1\<close>, (*"[| l is_num |] ==> v - l * v = (1 - l) * v"*)
221 \<^rule_thm>\<open>subtrahiere_1\<close>, (*"[| l is_num; m is_num |] ==> m * v - v = (m - 1) * v"*)
223 \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, (*"[| l is_num; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
224 \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>, (*"[| l is_num |] ==> (x + v) - l * v = x + (1 - l) * v"*)
225 \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>, (*"[| m is_num |] ==> (x + m * v) - v = x + (m - 1) * v"*)
227 \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
228 \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>, (*"[| l is_num |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
229 \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>, (*"[| m is_num |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
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"*)
233 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
235 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
236 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
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 *)
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"*)
243 \<^rule_thm>\<open>addiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) + m * v = (-l + m) *v"*)
244 \<^rule_thm>\<open>addiere_eins_vor_minus\<close>, (*"[| m is_num |] ==> - v + m * v = (-1 + m) * v"*)
245 \<^rule_thm>\<open>subtrahiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) - m * v = (-l - 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};
250 Rule_Def.Repeat{id = "verschoenere", preconds = [],
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
253 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
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"*)
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"*)
260 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
262 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
263 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
264 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
265 \<^rule_thm>\<open>null_minus\<close>, (*"0 - a = -a"*)
266 \<^rule_thm>\<open>vor_minus_mal\<close>], (*"- a * b = (-a) * b"*)
267 scr = Rule.Empty_Prog};
269 val klammern_aufloesen =
270 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
271 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty,
272 calc = [], errpatts = [], erls = Rule_Set.Empty,
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"*)
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"*)
278 scr = Rule.Empty_Prog};
280 val klammern_ausmultiplizieren =
281 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
282 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty,
283 calc = [], errpatts = [], erls = Rule_Set.Empty,
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"*)
288 \<^rule_thm>\<open>klammer_mult_minus\<close>, (*"a * (b - c) = a * b - a * c"*)
289 \<^rule_thm>\<open>klammer_minus_mult\<close>], (*"(b - c) * a = b * a - c * a"*)
290 scr = Rule.Empty_Prog};
294 id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
295 srls = Rule_Set.Empty, calc = [], errpatts = [],
296 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
297 \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
298 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")],
300 \<^rule_thm>\<open>tausche_mal\<close>, (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
301 \<^rule_thm>\<open>tausche_vor_mal\<close>, (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
302 \<^rule_thm>\<open>tausche_mal_mal\<close>, (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
303 \<^rule_thm>\<open>x_quadrat\<close>], (*"(x * a) * a = x * a \<up> 2"*)
304 scr = Rule.Empty_Prog};
307 Rule_Set.append_rules "rls_p_33" Rule_Set.empty [
308 Rule.Rls_ ordne_alphabetisch,
309 Rule.Rls_ fasse_zusammen,
310 Rule.Rls_ verschoenere];
312 Rule_Set.append_rules "rls_p_34" Rule_Set.empty [
313 Rule.Rls_ klammern_aufloesen,
314 Rule.Rls_ ordne_alphabetisch,
315 Rule.Rls_ fasse_zusammen,
316 Rule.Rls_ verschoenere];
318 Rule_Set.append_rules "rechnen" Rule_Set.empty [
319 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
320 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
321 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
324 ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
325 fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and
326 verschoenere = \<open>prep_rls' verschoenere\<close> and
327 ordne_monome = \<open>prep_rls' ordne_monome\<close> and
328 klammern_aufloesen = \<open>prep_rls' klammern_aufloesen\<close> and
329 klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>
333 problem pbl_vereinf_poly : "polynom/vereinfachen" = \<open>Rule_Set.Empty\<close>
335 problem pbl_vereinf_poly_minus : "plus_minus/polynom/vereinfachen" =
336 \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty [
337 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
338 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
339 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
340 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
341 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
342 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
343 Method_Ref: "simplification/for_polynomials/with_minus"
344 CAS: "Vereinfache t_t"
348 "Not (matchsub (?a + (?b + ?c)) t_t |
349 matchsub (?a + (?b - ?c)) t_t |
350 matchsub (?a - (?b + ?c)) t_t |
351 matchsub (?a + (?b - ?c)) t_t )"
352 "Not (matchsub (?a * (?b + ?c)) t_t |
353 matchsub (?a * (?b - ?c)) t_t |
354 matchsub ((?b + ?c) * ?a) t_t |
355 matchsub ((?b - ?c) * ?a) t_t )"
356 Find: "normalform n_n"
358 problem pbl_vereinf_poly_klammer : "klammer/polynom/vereinfachen" =
359 \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty [
360 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
361 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
362 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
363 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
364 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
365 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
366 Method_Ref: "simplification/for_polynomials/with_parentheses"
367 CAS: "Vereinfache t_t"
371 "Not (matchsub (?a * (?b + ?c)) t_t |
372 matchsub (?a * (?b - ?c)) t_t |
373 matchsub ((?b + ?c) * ?a) t_t |
374 matchsub ((?b - ?c) * ?a) t_t )"
375 Find: "normalform n_n"
377 problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
378 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
379 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
380 Method_Ref: "simplification/for_polynomials/with_parentheses_mult"
381 CAS: "Vereinfache t_t"
383 Where: "t_t is_polyexp"
384 Find: "normalform n_n"
386 problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close>
388 problem pbl_probe_poly : "polynom/probe" =
389 \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
390 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
391 Method_Ref: "probe/fuer_polynom"
393 Given: "Pruefe e_e" "mitWert w_w"
394 Where: "e_e is_polyexp"
397 problem pbl_probe_bruch : "bruch/probe" =
398 \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
399 \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
400 Method_Ref: "probe/fuer_bruch"
402 Given: "Pruefe e_e" "mitWert w_w"
403 Where: "e_e is_ratpolyexp"
408 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
412 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
413 (Try (Rewrite_Set ''fasse_zusammen'')) #>
414 (Try (Rewrite_Set ''verschoenere'')))
417 method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =
418 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
419 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty [
420 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
421 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
422 \<^rule_thm>\<open>and_true\<close>, (*"(?a & True) = ?a"*)
423 \<^rule_thm>\<open>and_false\<close>, (*"(?a & False) = False"*)
424 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
425 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)],
426 crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>
427 Program: simplify.simps
431 "Not (matchsub (?a + (?b + ?c)) t_t |
432 matchsub (?a + (?b - ?c)) t_t |
433 matchsub (?a - (?b + ?c)) t_t |
434 matchsub (?a + (?b - ?c)) t_t)"
435 Find: "normalform n_n"
437 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
441 (Try (Rewrite_Set ''klammern_aufloesen'')) #>
442 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
443 (Try (Rewrite_Set ''fasse_zusammen'')) #>
444 (Try (Rewrite_Set ''verschoenere'')))
447 method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =
448 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
449 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
450 [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
451 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
452 Program: simplify2.simps
454 Where: "t_t is_polyexp"
455 Find: "normalform n_n"
457 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
461 (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
462 (Try (Rewrite_Set ''discard_parentheses'')) #>
463 (Try (Rewrite_Set ''ordne_monome'')) #>
464 (Try (Rewrite_Set ''klammern_aufloesen'')) #>
465 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
466 (Try (Rewrite_Set ''fasse_zusammen'')) #>
467 (Try (Rewrite_Set ''verschoenere'')))
470 method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =
471 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
472 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
473 [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
474 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
475 Program: simplify3.simps
477 Where: "t_t is_polyexp"
478 Find: "normalform n_n"
480 method met_probe : "probe" =
481 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
482 errpats = [], nrls = Rule_Set.Empty}\<close>
484 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
486 "mache_probe e_e w_w = (
489 e_e = Substitute w_w e_e
492 (Try (Repeat (Calculate ''TIMES''))) #>
493 (Try (Repeat (Calculate ''PLUS'' ))) #>
494 (Try (Repeat (Calculate ''MINUS''))))
497 method met_probe_poly : "probe/fuer_polynom" =
498 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
499 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
500 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
501 crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>
502 Program: mache_probe.simps
503 Given: "Pruefe e_e" "mitWert w_w"
504 Where: "e_e is_polyexp"
507 method met_probe_bruch : "probe/fuer_bruch" =
508 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
509 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
510 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
511 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>
512 Given: "Pruefe e_e" "mitWert w_w"
513 Where: "e_e is_ratpolyexp"