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_const; m is_const |] ==>
55 m * v - l * v = (m - l) * v" and
56 subtrahiere_von_1: "[| l is_const |] ==>
57 v - l * v = (1 - l) * v" and
58 subtrahiere_1: "[| l is_const; m is_const |] ==>
59 m * v - v = (m - 1) * v" and
61 subtrahiere_x_plus_minus: "[| l is_const; m is_const |] ==>
62 (x + m * v) - l * v = x + (m - l) * v" and
63 subtrahiere_x_plus1_minus: "[| l is_const |] ==>
64 (x + v) - l * v = x + (1 - l) * v" and
65 subtrahiere_x_plus_minus1: "[| m is_const |] ==>
66 (x + m * v) - v = x + (m - 1) * v" and
68 subtrahiere_x_minus_plus: "[| l is_const; m is_const |] ==>
69 (x - m * v) + l * v = x + (-m + l) * v" and
70 subtrahiere_x_minus1_plus: "[| l is_const |] ==>
71 (x - v) + l * v = x + (-1 + l) * v" and
72 subtrahiere_x_minus_plus1: "[| m is_const |] ==>
73 (x - m * v) + v = x + (-m + 1) * v" and
75 subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>
76 (x - m * v) - l * v = x + (-m - l) * v" and
77 subtrahiere_x_minus1_minus:"[| l is_const |] ==>
78 (x - v) - l * v = x + (-1 - l) * v" and
79 subtrahiere_x_minus_minus1:"[| m is_const |] ==>
80 (x - m * v) - v = x + (-m - 1) * v" and
83 addiere_vor_minus: "[| l is_const; m is_const |] ==>
84 - (l * v) + m * v = (-l + m) * v" and
85 addiere_eins_vor_minus: "[| m is_const |] ==>
86 - v + m * v = (-1 + m) * v" and
87 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==>
88 - (l * v) - m * v = (-l - m) * v" and
89 subtrahiere_eins_vor_minus:"[| m is_const |] ==>
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"
110 (** eval functions **)
112 (*. get the identifier from specific monomials; see fun ist_monom .*)
117 case Symbol.explode str of
119 | _ => raise ERROR "PolyMinus.increase: uncovered case"
120 in implode ((chr (ord s + 1))::ss) end;
121 fun identifier (Free (id,_)) = id (* 2 , a *)
122 | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) =
124 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
125 (Const ("Groups.times_class.times", _) $
126 Free (num, _) $ Free _) $ Free (id, _)) =
127 if TermC.is_num' num then id
129 | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =
130 if TermC.is_num' base then "|||||||||||||" (* a^2 *)
131 else (*increase*) base
132 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
133 (Const ("Transcendental.powr", _) $
134 Free (base, _) $ Free (_(*exp*), _))) =
135 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
137 | identifier _ = "|||||||||||||"(*the "largest" string*);
139 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
140 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
141 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
142 if TermC.is_num b then
143 if TermC.is_num a then (*123 kleiner 32 = True !!!*)
144 if TermC.num_of_term a < TermC.num_of_term b then
145 SOME ((UnparseC.term p) ^ " = True",
146 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
147 else SOME ((UnparseC.term p) ^ " = False",
148 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
149 else (* -1 * -2 kleiner 0 *)
150 SOME ((UnparseC.term p) ^ " = False",
151 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
153 if identifier a < identifier b then
154 SOME ((UnparseC.term p) ^ " = True",
155 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
156 else SOME ((UnparseC.term p) ^ " = False",
157 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
158 | eval_kleiner _ _ _ _ = NONE;
160 fun ist_monom (Free _) = true
161 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) =
162 if TermC.is_num' num then true else false
163 | ist_monom _ = false;
164 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
165 fun ist_monom (Free _) = true (* 2, a *)
166 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
167 if TermC.is_num' id then false else true
168 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
169 (Const ("Groups.times_class.times", _) $
170 Free (num, _) $ Free _) $ Free (id, _)) =
171 if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
172 | ist_monom (Const ("Transcendental.powr", _) $ Free _ $ Free _) =
174 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
175 (Const ("Transcendental.powr", _) $
177 if TermC.is_num' num then true else false
178 | ist_monom _ = false;
180 (* is this a univariate monomial ? *)
181 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
182 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
184 SOME ((UnparseC.term p) ^ " = True",
185 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
186 else SOME ((UnparseC.term p) ^ " = False",
187 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
188 | eval_ist_monom _ _ _ _ = NONE;
191 (** rewrite order **)
195 val erls_ordne_alphabetisch =
196 Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
197 [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
198 Rule.Eval ("PolyMinus.ist'_monom", eval_ist_monom "")
201 val ordne_alphabetisch =
202 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
203 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
204 erls = erls_ordne_alphabetisch,
205 rules = [Rule.Thm ("tausche_plus",ThmC.numerals_to_Free @{thm tausche_plus}),
206 (*"b kleiner a ==> (b + a) = (a + b)"*)
207 Rule.Thm ("tausche_minus",ThmC.numerals_to_Free @{thm tausche_minus}),
208 (*"b kleiner a ==> (b - a) = (-a + b)"*)
209 Rule.Thm ("tausche_vor_plus",ThmC.numerals_to_Free @{thm tausche_vor_plus}),
210 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
211 Rule.Thm ("tausche_vor_minus",ThmC.numerals_to_Free @{thm tausche_vor_minus}),
212 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
213 Rule.Thm ("tausche_plus_plus",ThmC.numerals_to_Free @{thm tausche_plus_plus}),
214 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
215 Rule.Thm ("tausche_plus_minus",ThmC.numerals_to_Free @{thm tausche_plus_minus}),
216 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
217 Rule.Thm ("tausche_minus_plus",ThmC.numerals_to_Free @{thm tausche_minus_plus}),
218 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
219 Rule.Thm ("tausche_minus_minus",ThmC.numerals_to_Free @{thm tausche_minus_minus})
220 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
221 ], scr = Rule.Empty_Prog};
224 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
225 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
226 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
227 [Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")],
228 srls = Rule_Set.Empty, calc = [], errpatts = [],
230 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
231 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
232 Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
233 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
234 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
235 (*"m is_const ==> n + m * n = (1 + m) * n"*)
236 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
237 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
240 Rule.Thm ("subtrahiere",ThmC.numerals_to_Free @{thm subtrahiere}),
241 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
242 Rule.Thm ("subtrahiere_von_1",ThmC.numerals_to_Free @{thm subtrahiere_von_1}),
243 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
244 Rule.Thm ("subtrahiere_1",ThmC.numerals_to_Free @{thm subtrahiere_1}),
245 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
247 Rule.Thm ("subtrahiere_x_plus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus}),
248 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
249 Rule.Thm ("subtrahiere_x_plus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus1_minus}),
250 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
251 Rule.Thm ("subtrahiere_x_plus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus1}),
252 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
254 Rule.Thm ("subtrahiere_x_minus_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus}),
255 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
256 Rule.Thm ("subtrahiere_x_minus1_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_plus}),
257 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
258 Rule.Thm ("subtrahiere_x_minus_plus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus1}),
259 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
261 Rule.Thm ("subtrahiere_x_minus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus}),
262 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
263 Rule.Thm ("subtrahiere_x_minus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_minus}),
264 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
265 Rule.Thm ("subtrahiere_x_minus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus1}),
266 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
268 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
269 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_"),
271 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
272 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
273 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
274 (*"(k + z1) + z1 = k + 2 * z1"*)
275 Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
276 (*"z1 + z1 = 2 * z1"*)
278 Rule.Thm ("addiere_vor_minus",ThmC.numerals_to_Free @{thm addiere_vor_minus}),
279 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
280 Rule.Thm ("addiere_eins_vor_minus",ThmC.numerals_to_Free @{thm addiere_eins_vor_minus}),
281 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
282 Rule.Thm ("subtrahiere_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_vor_minus}),
283 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
284 Rule.Thm ("subtrahiere_eins_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_eins_vor_minus})
285 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
287 ], scr = Rule.Empty_Prog};
290 Rule_Def.Repeat{id = "verschoenere", preconds = [],
291 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
292 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
293 [Rule.Eval ("PolyMinus.kleiner", eval_kleiner "")],
294 rules = [Rule.Thm ("vorzeichen_minus_weg1",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg1}),
295 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
296 Rule.Thm ("vorzeichen_minus_weg2",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg2}),
297 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
298 Rule.Thm ("vorzeichen_minus_weg3",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg3}),
299 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
300 Rule.Thm ("vorzeichen_minus_weg4",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg4}),
301 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
303 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
305 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
307 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
309 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
311 Rule.Thm ("null_minus",ThmC.numerals_to_Free @{thm null_minus}),
313 Rule.Thm ("vor_minus_mal",ThmC.numerals_to_Free @{thm vor_minus_mal})
314 (*"- a * b = (-a) * b"*)
316 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),*)
318 ], scr = Rule.Empty_Prog} (*end verschoenere*);
320 val klammern_aufloesen =
321 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
322 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
323 rules = [Rule.Thm ("sym_add.assoc",
324 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
325 (*"a + (b + c) = (a + b) + c"*)
326 Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
327 (*"a + (b - c) = (a + b) - c"*)
328 Rule.Thm ("klammer_minus_plus",ThmC.numerals_to_Free @{thm klammer_minus_plus}),
329 (*"a - (b + c) = (a - b) - c"*)
330 Rule.Thm ("klammer_minus_minus",ThmC.numerals_to_Free @{thm klammer_minus_minus})
331 (*"a - (b - c) = (a - b) + c"*)
332 ], scr = Rule.Empty_Prog};
334 val klammern_ausmultiplizieren =
335 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
336 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
337 rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
338 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
339 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
340 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
342 Rule.Thm ("klammer_mult_minus",ThmC.numerals_to_Free @{thm klammer_mult_minus}),
343 (*"a * (b - c) = a * b - a * c"*)
344 Rule.Thm ("klammer_minus_mult",ThmC.numerals_to_Free @{thm klammer_minus_mult})
345 (*"(b - c) * a = b * a - c * a"*)
347 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
349 ], scr = Rule.Empty_Prog};
352 Rule_Def.Repeat{id = "ordne_monome", preconds = [],
353 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
354 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
355 [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
356 Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")
358 rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
359 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
360 Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}),
361 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
362 Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}),
363 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
364 Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat})
365 (*"(x * a) * a = x * a \<up> 2"*)
367 (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
369 ], scr = Rule.Empty_Prog};
373 Rule_Set.append_rules "rls_p_33" Rule_Set.empty
374 [Rule.Rls_ ordne_alphabetisch,
375 Rule.Rls_ fasse_zusammen,
376 Rule.Rls_ verschoenere
379 Rule_Set.append_rules "rls_p_34" Rule_Set.empty
380 [Rule.Rls_ klammern_aufloesen,
381 Rule.Rls_ ordne_alphabetisch,
382 Rule.Rls_ fasse_zusammen,
383 Rule.Rls_ verschoenere
386 Rule_Set.append_rules "rechnen" Rule_Set.empty
387 [Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
388 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
389 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_")
392 setup \<open>KEStore_Elems.add_rlss
393 [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls' ordne_alphabetisch)),
394 ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls' fasse_zusammen)),
395 ("verschoenere", (Context.theory_name @{theory}, prep_rls' verschoenere)),
396 ("ordne_monome", (Context.theory_name @{theory}, prep_rls' ordne_monome)),
397 ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls' klammern_aufloesen)),
398 ("klammern_ausmultiplizieren",
399 (Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))]\<close>
402 setup \<open>KEStore_Elems.add_pbts
403 [(Problem.prep_input thy "pbl_vereinf_poly" [] Problem.id_empty
404 (["polynom", "vereinfachen"], [], Rule_Set.Empty, NONE, [])),
405 (Problem.prep_input thy "pbl_vereinf_poly_minus" [] Problem.id_empty
406 (["plus_minus", "polynom", "vereinfachen"],
407 [("#Given", ["Term t_t"]),
408 ("#Where", ["t_t is_polyexp",
409 "Not (matchsub (?a + (?b + ?c)) t_t | " ^
410 " matchsub (?a + (?b - ?c)) t_t | " ^
411 " matchsub (?a - (?b + ?c)) t_t | " ^
412 " matchsub (?a + (?b - ?c)) t_t )",
413 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
414 " matchsub (?a * (?b - ?c)) t_t | " ^
415 " matchsub ((?b + ?c) * ?a) t_t | " ^
416 " matchsub ((?b - ?c) * ?a) t_t )"]),
417 ("#Find", ["normalform n_n"])],
418 Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
419 [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
420 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
421 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
422 (*"(?a | True) = True"*)
423 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
424 (*"(?a | False) = ?a"*)
425 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
426 (*"(~ True) = False"*)
427 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
428 (*"(~ False) = True"*)],
429 SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),
430 (Problem.prep_input thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
431 (["klammer", "polynom", "vereinfachen"],
432 [("#Given" ,["Term t_t"]),
433 ("#Where" ,["t_t is_polyexp",
434 "Not (matchsub (?a * (?b + ?c)) t_t | " ^
435 " matchsub (?a * (?b - ?c)) t_t | " ^
436 " matchsub ((?b + ?c) * ?a) t_t | " ^
437 " matchsub ((?b - ?c) * ?a) t_t )"]),
438 ("#Find" ,["normalform n_n"])],
439 Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
440 [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
441 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
442 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
443 (*"(?a | True) = True"*)
444 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
445 (*"(?a | False) = ?a"*)
446 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
447 (*"(~ True) = False"*)
448 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
449 (*"(~ False) = True"*)],
450 SOME "Vereinfache t_t",
451 [["simplification", "for_polynomials", "with_parentheses"]])),
452 (Problem.prep_input thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
453 (["binom_klammer", "polynom", "vereinfachen"],
454 [("#Given", ["Term t_t"]),
455 ("#Where", ["t_t is_polyexp"]),
456 ("#Find", ["normalform n_n"])],
457 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
458 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
459 SOME "Vereinfache t_t",
460 [["simplification", "for_polynomials", "with_parentheses_mult"]])),
461 (Problem.prep_input thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
462 (Problem.prep_input thy "pbl_probe_poly" [] Problem.id_empty
463 (["polynom", "probe"],
464 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
465 ("#Where", ["e_e is_polyexp"]),
466 ("#Find", ["Geprueft p_p"])],
467 Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
468 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
469 SOME "Probe e_e w_w",
470 [["probe", "fuer_polynom"]])),
471 (Problem.prep_input thy "pbl_probe_bruch" [] Problem.id_empty
473 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
474 ("#Where" ,["e_e is_ratpolyexp"]),
475 ("#Find" ,["Geprueft p_p"])],
476 Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
477 Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
478 SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>
482 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
486 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
487 (Try (Rewrite_Set ''fasse_zusammen'')) #>
488 (Try (Rewrite_Set ''verschoenere'')))
490 setup \<open>KEStore_Elems.add_mets
491 [MethodC.prep_input thy "met_simp_poly_minus" [] MethodC.id_empty
492 (["simplification", "for_polynomials", "with_minus"],
493 [("#Given" ,["Term t_t"]),
494 ("#Where" ,["t_t is_polyexp",
495 "Not (matchsub (?a + (?b + ?c)) t_t | " ^
496 " matchsub (?a + (?b - ?c)) t_t | " ^
497 " matchsub (?a - (?b + ?c)) t_t | " ^
498 " matchsub (?a + (?b - ?c)) t_t )"]),
499 ("#Find" ,["normalform n_n"])],
500 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
501 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
502 [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
503 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
504 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
505 (*"(?a & True) = ?a"*)
506 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
507 (*"(?a & False) = False"*)
508 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
509 (*"(~ True) = False"*)
510 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
511 (*"(~ False) = True"*)],
512 crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
513 @{thm simplify.simps})]
516 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
520 (Try (Rewrite_Set ''klammern_aufloesen'')) #>
521 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
522 (Try (Rewrite_Set ''fasse_zusammen'')) #>
523 (Try (Rewrite_Set ''verschoenere'')))
525 setup \<open>KEStore_Elems.add_mets
526 [MethodC.prep_input thy "met_simp_poly_parenth" [] MethodC.id_empty
527 (["simplification", "for_polynomials", "with_parentheses"],
528 [("#Given" ,["Term t_t"]),
529 ("#Where" ,["t_t is_polyexp"]),
530 ("#Find" ,["normalform n_n"])],
531 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
532 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
533 [(*for preds in where_*) Rule.Eval("Poly.is'_polyexp", eval_is_polyexp"")],
534 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
535 @{thm simplify2.simps})]
538 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
542 (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
543 (Try (Rewrite_Set ''discard_parentheses'')) #>
544 (Try (Rewrite_Set ''ordne_monome'')) #>
545 (Try (Rewrite_Set ''klammern_aufloesen'')) #>
546 (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
547 (Try (Rewrite_Set ''fasse_zusammen'')) #>
548 (Try (Rewrite_Set ''verschoenere'')))
550 setup \<open>KEStore_Elems.add_mets
551 [MethodC.prep_input thy "met_simp_poly_parenth_mult" [] MethodC.id_empty
552 (["simplification", "for_polynomials", "with_parentheses_mult"],
553 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
554 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
555 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
556 [(*for preds in where_*) Rule.Eval("Poly.is'_polyexp", eval_is_polyexp"")],
557 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
558 @{thm simplify3.simps})]
560 setup \<open>KEStore_Elems.add_mets
561 [MethodC.prep_input thy "met_probe" [] MethodC.id_empty
563 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
564 errpats = [], nrls = Rule_Set.Empty},
568 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
570 "mache_probe e_e w_w = (
573 e_e = Substitute w_w e_e
576 (Try (Repeat (Calculate ''TIMES''))) #>
577 (Try (Repeat (Calculate ''PLUS'' ))) #>
578 (Try (Repeat (Calculate ''MINUS''))))
580 setup \<open>KEStore_Elems.add_mets
581 [MethodC.prep_input thy "met_probe_poly" [] MethodC.id_empty
582 (["probe", "fuer_polynom"],
583 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
584 ("#Where" ,["e_e is_polyexp"]),
585 ("#Find" ,["Geprueft p_p"])],
586 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
587 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
588 [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
589 crls = Rule_Set.empty, errpats = [], nrls = rechnen},
590 @{thm mache_probe.simps})]
592 setup \<open>KEStore_Elems.add_mets
593 [MethodC.prep_input thy "met_probe_bruch" [] MethodC.id_empty
594 (["probe", "fuer_bruch"],
595 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
596 ("#Where" ,["e_e is_ratpolyexp"]),
597 ("#Find" ,["Geprueft p_p"])],
598 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
599 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
600 [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
601 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty},