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