1 (* questionable attempts to perserve binary minus as wanted by teachers |
|
2 WN071207 |
|
3 (c) due to copyright terms |
|
4 remove_thy"PolyMinus"; |
|
5 use_thy"IsacKnowledge/PolyMinus"; |
|
6 |
|
7 use_thy"IsacKnowledge/Isac"; |
|
8 use"IsacKnowledge/PolyMinus.ML"; |
|
9 *) |
|
10 |
|
11 (** interface isabelle -- isac **) |
|
12 theory' := overwritel (!theory', [("PolyMinus.thy",PolyMinus.thy)]); |
|
13 |
|
14 (** eval functions **) |
|
15 |
|
16 (*. get the identifier from specific monomials; see fun ist_monom .*) |
|
17 (*HACK.WN080107*) |
|
18 fun increase str = |
|
19 let val s::ss = explode str |
|
20 in implode ((chr (ord s + 1))::ss) end; |
|
21 fun identifier (Free (id,_)) = id (* 2, a *) |
|
22 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = |
|
23 id (* 2*a, a*b *) |
|
24 | identifier (Const ("op *", _) $ (* 3*a*b *) |
|
25 (Const ("op *", _) $ |
|
26 Free (num, _) $ Free _) $ Free (id, _)) = |
|
27 if is_numeral num then id |
|
28 else "|||||||||||||" |
|
29 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
|
30 if is_numeral base then "|||||||||||||" (* a^2 *) |
|
31 else (*increase*) base |
|
32 | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) |
|
33 (Const ("Atools.pow", _) $ |
|
34 Free (base, _) $ Free (exp, _))) = |
|
35 if is_numeral num andalso not (is_numeral base) then (*increase*) base |
|
36 else "|||||||||||||" |
|
37 | identifier _ = "|||||||||||||"(*the "largest" string*); |
|
38 |
|
39 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*) |
|
40 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *) |
|
41 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ = |
|
42 if is_num b then |
|
43 if is_num a then (*123 kleiner 32 = True !!!*) |
|
44 if int_of_Free a < int_of_Free b then |
|
45 SOME ((term2str p) ^ " = True", |
|
46 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
47 else SOME ((term2str p) ^ " = False", |
|
48 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
49 else (* -1 * -2 kleiner 0 *) |
|
50 SOME ((term2str p) ^ " = False", |
|
51 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
52 else |
|
53 if identifier a < identifier b then |
|
54 SOME ((term2str p) ^ " = True", |
|
55 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
56 else SOME ((term2str p) ^ " = False", |
|
57 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
58 | eval_kleiner _ _ _ _ = NONE; |
|
59 |
|
60 fun ist_monom (Free (id,_)) = true |
|
61 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = |
|
62 if is_numeral num then true else false |
|
63 | ist_monom _ = false; |
|
64 (*. this function only accepts the most simple monoms vvvvvvvvvv .*) |
|
65 fun ist_monom (Free (id,_)) = true (* 2, a *) |
|
66 | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) |
|
67 if is_numeral id then false else true |
|
68 | ist_monom (Const ("op *", _) $ (* 3*a*b *) |
|
69 (Const ("op *", _) $ |
|
70 Free (num, _) $ Free _) $ Free (id, _)) = |
|
71 if is_numeral num andalso not (is_numeral id) then true else false |
|
72 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = |
|
73 true (* a^2 *) |
|
74 | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) |
|
75 (Const ("Atools.pow", _) $ |
|
76 Free (base, _) $ Free (exp, _))) = |
|
77 if is_numeral num then true else false |
|
78 | ist_monom _ = false; |
|
79 |
|
80 (* is this a univariate monomial ? *) |
|
81 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*) |
|
82 fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ = |
|
83 if ist_monom a then |
|
84 SOME ((term2str p) ^ " = True", |
|
85 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
86 else SOME ((term2str p) ^ " = False", |
|
87 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
88 | eval_ist_monom _ _ _ _ = NONE; |
|
89 |
|
90 |
|
91 (** rewrite order **) |
|
92 |
|
93 (** rulesets **) |
|
94 |
|
95 val erls_ordne_alphabetisch = |
|
96 append_rls "erls_ordne_alphabetisch" e_rls |
|
97 [Calc ("PolyMinus.kleiner", eval_kleiner ""), |
|
98 Calc ("PolyMinus.ist'_monom", eval_ist_monom "") |
|
99 ]; |
|
100 |
|
101 val ordne_alphabetisch = |
|
102 Rls{id = "ordne_alphabetisch", preconds = [], |
|
103 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], |
|
104 erls = erls_ordne_alphabetisch, |
|
105 rules = [Thm ("tausche_plus",num_str tausche_plus), |
|
106 (*"b kleiner a ==> (b + a) = (a + b)"*) |
|
107 Thm ("tausche_minus",num_str tausche_minus), |
|
108 (*"b kleiner a ==> (b - a) = (-a + b)"*) |
|
109 Thm ("tausche_vor_plus",num_str tausche_vor_plus), |
|
110 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*) |
|
111 Thm ("tausche_vor_minus",num_str tausche_vor_minus), |
|
112 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*) |
|
113 Thm ("tausche_plus_plus",num_str tausche_plus_plus), |
|
114 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*) |
|
115 Thm ("tausche_plus_minus",num_str tausche_plus_minus), |
|
116 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*) |
|
117 Thm ("tausche_minus_plus",num_str tausche_minus_plus), |
|
118 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*) |
|
119 Thm ("tausche_minus_minus",num_str tausche_minus_minus) |
|
120 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*) |
|
121 ], scr = EmptyScr}:rls; |
|
122 |
|
123 val fasse_zusammen = |
|
124 Rls{id = "fasse_zusammen", preconds = [], |
|
125 rew_ord = ("dummy_ord", dummy_ord), |
|
126 erls = append_rls "erls_fasse_zusammen" e_rls |
|
127 [Calc ("Atools.is'_const",eval_const "#is_const_")], |
|
128 srls = Erls, calc = [], |
|
129 rules = |
|
130 [Thm ("real_num_collect",num_str real_num_collect), |
|
131 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
132 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r), |
|
133 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*) |
|
134 Thm ("real_one_collect",num_str real_one_collect), |
|
135 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
136 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r), |
|
137 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
|
138 |
|
139 |
|
140 Thm ("subtrahiere",num_str subtrahiere), |
|
141 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*) |
|
142 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1), |
|
143 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*) |
|
144 Thm ("subtrahiere_1",num_str subtrahiere_1), |
|
145 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*) |
|
146 |
|
147 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus), |
|
148 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*) |
|
149 Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus), |
|
150 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*) |
|
151 Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1), |
|
152 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*) |
|
153 |
|
154 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus), |
|
155 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*) |
|
156 Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus), |
|
157 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*) |
|
158 Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1), |
|
159 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*) |
|
160 |
|
161 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus), |
|
162 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*) |
|
163 Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus), |
|
164 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*) |
|
165 Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1), |
|
166 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*) |
|
167 |
|
168 Calc ("op +", eval_binop "#add_"), |
|
169 Calc ("op -", eval_binop "#subtr_"), |
|
170 |
|
171 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
|
172 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
|
173 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r), |
|
174 (*"(k + z1) + z1 = k + 2 * z1"*) |
|
175 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
176 (*"z1 + z1 = 2 * z1"*) |
|
177 |
|
178 Thm ("addiere_vor_minus",num_str addiere_vor_minus), |
|
179 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*) |
|
180 Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus), |
|
181 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*) |
|
182 Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus), |
|
183 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*) |
|
184 Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus) |
|
185 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*) |
|
186 |
|
187 ], scr = EmptyScr}:rls; |
|
188 |
|
189 val verschoenere = |
|
190 Rls{id = "verschoenere", preconds = [], |
|
191 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], |
|
192 erls = append_rls "erls_verschoenere" e_rls |
|
193 [Calc ("PolyMinus.kleiner", eval_kleiner "")], |
|
194 rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1), |
|
195 (*"l kleiner 0 ==> a + l * b = a - -l * b"*) |
|
196 Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2), |
|
197 (*"l kleiner 0 ==> a - l * b = a + -l * b"*) |
|
198 Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3), |
|
199 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*) |
|
200 Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4), |
|
201 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) |
|
202 |
|
203 Calc ("op *", eval_binop "#mult_"), |
|
204 |
|
205 Thm ("real_mult_0",num_str real_mult_0), |
|
206 (*"0 * z = 0"*) |
|
207 Thm ("real_mult_1",num_str real_mult_1), |
|
208 (*"1 * z = z"*) |
|
209 Thm ("real_add_zero_left",num_str real_add_zero_left), |
|
210 (*"0 + z = z"*) |
|
211 Thm ("null_minus",num_str null_minus), |
|
212 (*"0 - a = -a"*) |
|
213 Thm ("vor_minus_mal",num_str vor_minus_mal) |
|
214 (*"- a * b = (-a) * b"*) |
|
215 |
|
216 (*Thm ("",num_str ),*) |
|
217 (**) |
|
218 ], scr = EmptyScr}:rls (*end verschoenere*); |
|
219 |
|
220 val klammern_aufloesen = |
|
221 Rls{id = "klammern_aufloesen", preconds = [], |
|
222 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, |
|
223 rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)), |
|
224 (*"a + (b + c) = (a + b) + c"*) |
|
225 Thm ("klammer_plus_minus",num_str klammer_plus_minus), |
|
226 (*"a + (b - c) = (a + b) - c"*) |
|
227 Thm ("klammer_minus_plus",num_str klammer_minus_plus), |
|
228 (*"a - (b + c) = (a - b) - c"*) |
|
229 Thm ("klammer_minus_minus",num_str klammer_minus_minus) |
|
230 (*"a - (b - c) = (a - b) + c"*) |
|
231 ], scr = EmptyScr}:rls; |
|
232 |
|
233 val klammern_ausmultiplizieren = |
|
234 Rls{id = "klammern_ausmultiplizieren", preconds = [], |
|
235 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, |
|
236 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
237 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
238 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
239 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
240 |
|
241 Thm ("klammer_mult_minus",num_str klammer_mult_minus), |
|
242 (*"a * (b - c) = a * b - a * c"*) |
|
243 Thm ("klammer_minus_mult",num_str klammer_minus_mult) |
|
244 (*"(b - c) * a = b * a - c * a"*) |
|
245 |
|
246 (*Thm ("",num_str ), |
|
247 (*""*)*) |
|
248 ], scr = EmptyScr}:rls; |
|
249 |
|
250 val ordne_monome = |
|
251 Rls{id = "ordne_monome", preconds = [], |
|
252 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], |
|
253 erls = append_rls "erls_ordne_monome" e_rls |
|
254 [Calc ("PolyMinus.kleiner", eval_kleiner ""), |
|
255 Calc ("Atools.is'_atom", eval_is_atom "") |
|
256 ], |
|
257 rules = [Thm ("tausche_mal",num_str tausche_mal), |
|
258 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*) |
|
259 Thm ("tausche_vor_mal",num_str tausche_vor_mal), |
|
260 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*) |
|
261 Thm ("tausche_mal_mal",num_str tausche_mal_mal), |
|
262 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*) |
|
263 Thm ("x_quadrat",num_str x_quadrat) |
|
264 (*"(x * a) * a = x * a ^^^ 2"*) |
|
265 |
|
266 (*Thm ("",num_str ), |
|
267 (*""*)*) |
|
268 ], scr = EmptyScr}:rls; |
|
269 |
|
270 |
|
271 val rls_p_33 = |
|
272 append_rls "rls_p_33" e_rls |
|
273 [Rls_ ordne_alphabetisch, |
|
274 Rls_ fasse_zusammen, |
|
275 Rls_ verschoenere |
|
276 ]; |
|
277 val rls_p_34 = |
|
278 append_rls "rls_p_34" e_rls |
|
279 [Rls_ klammern_aufloesen, |
|
280 Rls_ ordne_alphabetisch, |
|
281 Rls_ fasse_zusammen, |
|
282 Rls_ verschoenere |
|
283 ]; |
|
284 val rechnen = |
|
285 append_rls "rechnen" e_rls |
|
286 [Calc ("op *", eval_binop "#mult_"), |
|
287 Calc ("op +", eval_binop "#add_"), |
|
288 Calc ("op -", eval_binop "#subtr_") |
|
289 ]; |
|
290 |
|
291 ruleset' := |
|
292 overwritelthy thy (!ruleset', |
|
293 [("ordne_alphabetisch", prep_rls ordne_alphabetisch), |
|
294 ("fasse_zusammen", prep_rls fasse_zusammen), |
|
295 ("verschoenere", prep_rls verschoenere), |
|
296 ("ordne_monome", prep_rls ordne_monome), |
|
297 ("klammern_aufloesen", prep_rls klammern_aufloesen), |
|
298 ("klammern_ausmultiplizieren", |
|
299 prep_rls klammern_ausmultiplizieren) |
|
300 ]); |
|
301 |
|
302 (** problems **) |
|
303 |
|
304 store_pbt |
|
305 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID |
|
306 (["polynom","vereinfachen"], |
|
307 [], Erls, NONE, [])); |
|
308 |
|
309 store_pbt |
|
310 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID |
|
311 (["plus_minus","polynom","vereinfachen"], |
|
312 [("#Given" ,["term t_"]), |
|
313 ("#Where" ,["t_ is_polyexp", |
|
314 "Not (matchsub (?a + (?b + ?c)) t_ | \ |
|
315 \ matchsub (?a + (?b - ?c)) t_ | \ |
|
316 \ matchsub (?a - (?b + ?c)) t_ | \ |
|
317 \ matchsub (?a + (?b - ?c)) t_ )", |
|
318 "Not (matchsub (?a * (?b + ?c)) t_ | \ |
|
319 \ matchsub (?a * (?b - ?c)) t_ | \ |
|
320 \ matchsub ((?b + ?c) * ?a) t_ | \ |
|
321 \ matchsub ((?b - ?c) * ?a) t_ )"]), |
|
322 ("#Find" ,["normalform n_"]) |
|
323 ], |
|
324 append_rls "prls_pbl_vereinf_poly" e_rls |
|
325 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
|
326 Calc ("Tools.matchsub", eval_matchsub ""), |
|
327 Thm ("or_true",or_true), |
|
328 (*"(?a | True) = True"*) |
|
329 Thm ("or_false",or_false), |
|
330 (*"(?a | False) = ?a"*) |
|
331 Thm ("not_true",num_str not_true), |
|
332 (*"(~ True) = False"*) |
|
333 Thm ("not_false",num_str not_false) |
|
334 (*"(~ False) = True"*)], |
|
335 SOME "Vereinfache t_", |
|
336 [["simplification","for_polynomials","with_minus"]])); |
|
337 |
|
338 store_pbt |
|
339 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID |
|
340 (["klammer","polynom","vereinfachen"], |
|
341 [("#Given" ,["term t_"]), |
|
342 ("#Where" ,["t_ is_polyexp", |
|
343 "Not (matchsub (?a * (?b + ?c)) t_ | \ |
|
344 \ matchsub (?a * (?b - ?c)) t_ | \ |
|
345 \ matchsub ((?b + ?c) * ?a) t_ | \ |
|
346 \ matchsub ((?b - ?c) * ?a) t_ )"]), |
|
347 ("#Find" ,["normalform n_"]) |
|
348 ], |
|
349 append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
|
350 Calc ("Tools.matchsub", eval_matchsub ""), |
|
351 Thm ("or_true",or_true), |
|
352 (*"(?a | True) = True"*) |
|
353 Thm ("or_false",or_false), |
|
354 (*"(?a | False) = ?a"*) |
|
355 Thm ("not_true",num_str not_true), |
|
356 (*"(~ True) = False"*) |
|
357 Thm ("not_false",num_str not_false) |
|
358 (*"(~ False) = True"*)], |
|
359 SOME "Vereinfache t_", |
|
360 [["simplification","for_polynomials","with_parentheses"]])); |
|
361 |
|
362 store_pbt |
|
363 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID |
|
364 (["binom_klammer","polynom","vereinfachen"], |
|
365 [("#Given" ,["term t_"]), |
|
366 ("#Where" ,["t_ is_polyexp"]), |
|
367 ("#Find" ,["normalform n_"]) |
|
368 ], |
|
369 append_rls "e_rls" e_rls [(*for preds in where_*) |
|
370 Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
|
371 SOME "Vereinfache t_", |
|
372 [["simplification","for_polynomials","with_parentheses_mult"]])); |
|
373 |
|
374 store_pbt |
|
375 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID |
|
376 (["probe"], |
|
377 [], Erls, NONE, [])); |
|
378 |
|
379 store_pbt |
|
380 (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID |
|
381 (["polynom","probe"], |
|
382 [("#Given" ,["Pruefe e_", "mitWert ws_"]), |
|
383 ("#Where" ,["e_ is_polyexp"]), |
|
384 ("#Find" ,["Geprueft p_"]) |
|
385 ], |
|
386 append_rls "prls_pbl_probe_poly" |
|
387 e_rls [(*for preds in where_*) |
|
388 Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
|
389 SOME "Probe e_ ws_", |
|
390 [["probe","fuer_polynom"]])); |
|
391 |
|
392 store_pbt |
|
393 (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID |
|
394 (["bruch","probe"], |
|
395 [("#Given" ,["Pruefe e_", "mitWert ws_"]), |
|
396 ("#Where" ,["e_ is_ratpolyexp"]), |
|
397 ("#Find" ,["Geprueft p_"]) |
|
398 ], |
|
399 append_rls "prls_pbl_probe_bruch" |
|
400 e_rls [(*for preds in where_*) |
|
401 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], |
|
402 SOME "Probe e_ ws_", |
|
403 [["probe","fuer_bruch"]])); |
|
404 |
|
405 |
|
406 (** methods **) |
|
407 |
|
408 store_met |
|
409 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID |
|
410 (["simplification","for_polynomials","with_minus"], |
|
411 [("#Given" ,["term t_"]), |
|
412 ("#Where" ,["t_ is_polyexp", |
|
413 "Not (matchsub (?a + (?b + ?c)) t_ | \ |
|
414 \ matchsub (?a + (?b - ?c)) t_ | \ |
|
415 \ matchsub (?a - (?b + ?c)) t_ | \ |
|
416 \ matchsub (?a + (?b - ?c)) t_ )"]), |
|
417 ("#Find" ,["normalform n_"]) |
|
418 ], |
|
419 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
420 prls = append_rls "prls_met_simp_poly_minus" e_rls |
|
421 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
|
422 Calc ("Tools.matchsub", eval_matchsub ""), |
|
423 Thm ("and_true",and_true), |
|
424 (*"(?a & True) = ?a"*) |
|
425 Thm ("and_false",and_false), |
|
426 (*"(?a & False) = False"*) |
|
427 Thm ("not_true",num_str not_true), |
|
428 (*"(~ True) = False"*) |
|
429 Thm ("not_false",num_str not_false) |
|
430 (*"(~ False) = True"*)], |
|
431 crls = e_rls, nrls = rls_p_33}, |
|
432 "Script SimplifyScript (t_::real) = \ |
|
433 \ ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
|
434 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
|
435 \ (Try (Rewrite_Set verschoenere False)))) t_)" |
|
436 )); |
|
437 |
|
438 store_met |
|
439 (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID |
|
440 (["simplification","for_polynomials","with_parentheses"], |
|
441 [("#Given" ,["term t_"]), |
|
442 ("#Where" ,["t_ is_polyexp"]), |
|
443 ("#Find" ,["normalform n_"]) |
|
444 ], |
|
445 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
446 prls = append_rls "simplification_for_polynomials_prls" e_rls |
|
447 [(*for preds in where_*) |
|
448 Calc("Poly.is'_polyexp",eval_is_polyexp"")], |
|
449 crls = e_rls, nrls = rls_p_34}, |
|
450 "Script SimplifyScript (t_::real) = \ |
|
451 \ ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ \ |
|
452 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
|
453 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
|
454 \ (Try (Rewrite_Set verschoenere False)))) t_)" |
|
455 )); |
|
456 |
|
457 store_met |
|
458 (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID |
|
459 (["simplification","for_polynomials","with_parentheses_mult"], |
|
460 [("#Given" ,["term t_"]), |
|
461 ("#Where" ,["t_ is_polyexp"]), |
|
462 ("#Find" ,["normalform n_"]) |
|
463 ], |
|
464 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
465 prls = append_rls "simplification_for_polynomials_prls" e_rls |
|
466 [(*for preds in where_*) |
|
467 Calc("Poly.is'_polyexp",eval_is_polyexp"")], |
|
468 crls = e_rls, nrls = rls_p_34}, |
|
469 "Script SimplifyScript (t_::real) = \ |
|
470 \ ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \ |
|
471 \ (Try (Rewrite_Set discard_parentheses False)) @@ \ |
|
472 \ (Try (Rewrite_Set ordne_monome False)) @@ \ |
|
473 \ (Try (Rewrite_Set klammern_aufloesen False)) @@ \ |
|
474 \ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
|
475 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
|
476 \ (Try (Rewrite_Set verschoenere False)))) t_)" |
|
477 )); |
|
478 |
|
479 store_met |
|
480 (prep_met PolyMinus.thy "met_probe" [] e_metID |
|
481 (["probe"], |
|
482 [], |
|
483 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
484 prls = Erls, crls = e_rls, nrls = Erls}, |
|
485 "empty_script")); |
|
486 |
|
487 store_met |
|
488 (prep_met PolyMinus.thy "met_probe_poly" [] e_metID |
|
489 (["probe","fuer_polynom"], |
|
490 [("#Given" ,["Pruefe e_", "mitWert ws_"]), |
|
491 ("#Where" ,["e_ is_polyexp"]), |
|
492 ("#Find" ,["Geprueft p_"]) |
|
493 ], |
|
494 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
495 prls = append_rls "prls_met_probe_bruch" |
|
496 e_rls [(*for preds in where_*) |
|
497 Calc ("Rational.is'_ratpolyexp", |
|
498 eval_is_ratpolyexp "")], |
|
499 crls = e_rls, nrls = rechnen}, |
|
500 "Script ProbeScript (e_::bool) (ws_::bool list) = \ |
|
501 \ (let e_ = Take e_; \ |
|
502 \ e_ = Substitute ws_ e_ \ |
|
503 \ in (Repeat((Try (Repeat (Calculate times))) @@ \ |
|
504 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
505 \ (Try (Repeat (Calculate minus))))) e_)" |
|
506 )); |
|
507 |
|
508 store_met |
|
509 (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID |
|
510 (["probe","fuer_bruch"], |
|
511 [("#Given" ,["Pruefe e_", "mitWert ws_"]), |
|
512 ("#Where" ,["e_ is_ratpolyexp"]), |
|
513 ("#Find" ,["Geprueft p_"]) |
|
514 ], |
|
515 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
|
516 prls = append_rls "prls_met_probe_bruch" |
|
517 e_rls [(*for preds in where_*) |
|
518 Calc ("Rational.is'_ratpolyexp", |
|
519 eval_is_ratpolyexp "")], |
|
520 crls = e_rls, nrls = Erls}, |
|
521 "empty_script")); |
|