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 _")
|
walther@60278
|
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@52148
|
23 |
axiomatization where
|
neuper@37906
|
24 |
|
neuper@52148
|
25 |
null_minus: "0 - a = -a" and
|
neuper@52148
|
26 |
vor_minus_mal: "- a * b = (-a) * b" and
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*commute with invariant (a.b).c -association*)
|
neuper@37980
|
29 |
tausche_plus: "[| b ist_monom; a kleiner b |] ==>
|
neuper@52148
|
30 |
(b + a) = (a + b)" and
|
neuper@37980
|
31 |
tausche_minus: "[| b ist_monom; a kleiner b |] ==>
|
neuper@52148
|
32 |
(b - a) = (-a + b)" and
|
neuper@37980
|
33 |
tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
|
neuper@52148
|
34 |
(- b + a) = (a - b)" and
|
neuper@37980
|
35 |
tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
|
neuper@52148
|
36 |
(- b - a) = (-a - b)" and
|
walther@60269
|
37 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
|
neuper@52148
|
38 |
tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
|
neuper@52148
|
39 |
tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
|
neuper@52148
|
40 |
tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
|
neuper@52148
|
41 |
tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
|
walther@60269
|
42 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
|
neuper@37906
|
43 |
|
neuper@37906
|
44 |
(*commute with invariant (a.b).c -association*)
|
neuper@37980
|
45 |
tausche_mal: "[| b is_atom; a kleiner b |] ==>
|
neuper@52148
|
46 |
(b * a) = (a * b)" and
|
neuper@37980
|
47 |
tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
|
neuper@52148
|
48 |
(-b * a) = (-a * b)" and
|
neuper@37980
|
49 |
tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
|
neuper@52148
|
50 |
(x * c * b) = (x * b * c)" and
|
walther@60242
|
51 |
x_quadrat: "(x * a) * a = x * a \<up> 2" and
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
|
walther@60385
|
54 |
subtrahiere: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
55 |
m * v - l * v = (m - l) * v" and
|
walther@60385
|
56 |
subtrahiere_von_1: "[| l is_num |] ==>
|
neuper@52148
|
57 |
v - l * v = (1 - l) * v" and
|
walther@60385
|
58 |
subtrahiere_1: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
59 |
m * v - v = (m - 1) * v" and
|
neuper@37906
|
60 |
|
walther@60385
|
61 |
subtrahiere_x_plus_minus: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
62 |
(x + m * v) - l * v = x + (m - l) * v" and
|
walther@60385
|
63 |
subtrahiere_x_plus1_minus: "[| l is_num |] ==>
|
neuper@52148
|
64 |
(x + v) - l * v = x + (1 - l) * v" and
|
walther@60385
|
65 |
subtrahiere_x_plus_minus1: "[| m is_num |] ==>
|
neuper@52148
|
66 |
(x + m * v) - v = x + (m - 1) * v" and
|
neuper@37906
|
67 |
|
walther@60385
|
68 |
subtrahiere_x_minus_plus: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
69 |
(x - m * v) + l * v = x + (-m + l) * v" and
|
walther@60385
|
70 |
subtrahiere_x_minus1_plus: "[| l is_num |] ==>
|
neuper@52148
|
71 |
(x - v) + l * v = x + (-1 + l) * v" and
|
walther@60385
|
72 |
subtrahiere_x_minus_plus1: "[| m is_num |] ==>
|
neuper@52148
|
73 |
(x - m * v) + v = x + (-m + 1) * v" and
|
neuper@37906
|
74 |
|
walther@60385
|
75 |
subtrahiere_x_minus_minus: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
76 |
(x - m * v) - l * v = x + (-m - l) * v" and
|
walther@60385
|
77 |
subtrahiere_x_minus1_minus:"[| l is_num |] ==>
|
neuper@52148
|
78 |
(x - v) - l * v = x + (-1 - l) * v" and
|
walther@60385
|
79 |
subtrahiere_x_minus_minus1:"[| m is_num |] ==>
|
neuper@52148
|
80 |
(x - m * v) - v = x + (-m - 1) * v" and
|
neuper@37906
|
81 |
|
neuper@37906
|
82 |
|
walther@60385
|
83 |
addiere_vor_minus: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
84 |
- (l * v) + m * v = (-l + m) * v" and
|
walther@60385
|
85 |
addiere_eins_vor_minus: "[| m is_num |] ==>
|
neuper@52148
|
86 |
- v + m * v = (-1 + m) * v" and
|
walther@60385
|
87 |
subtrahiere_vor_minus: "[| l is_num; m is_num |] ==>
|
neuper@52148
|
88 |
- (l * v) - m * v = (-l - m) * v" and
|
walther@60385
|
89 |
subtrahiere_eins_vor_minus:"[| m is_num |] ==>
|
neuper@52148
|
90 |
- v - m * v = (-1 - m) * v" and
|
neuper@37906
|
91 |
|
walther@60269
|
92 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
|
neuper@52148
|
93 |
vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
|
neuper@52148
|
94 |
vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
|
neuper@52148
|
95 |
vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
|
neuper@52148
|
96 |
vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
|
walther@60269
|
97 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
|
neuper@37906
|
98 |
|
walther@59877
|
99 |
(*klammer_plus_plus = (add.assoc RS sym)*)
|
neuper@52148
|
100 |
klammer_plus_minus: "a + (b - c) = (a + b) - c" and
|
neuper@52148
|
101 |
klammer_minus_plus: "a - (b + c) = (a - b) - c" and
|
neuper@52148
|
102 |
klammer_minus_minus: "a - (b - c) = (a - b) + c" and
|
neuper@37906
|
103 |
|
neuper@52148
|
104 |
klammer_mult_minus: "a * (b - c) = a * b - a * c" and
|
neuper@37980
|
105 |
klammer_minus_mult: "(b - c) * a = b * a - c * a"
|
neuper@37906
|
106 |
|
wneuper@59472
|
107 |
ML \<open>
|
neuper@37950
|
108 |
(** eval functions **)
|
neuper@37906
|
109 |
|
neuper@37950
|
110 |
(*. get the identifier from specific monomials; see fun ist_monom .*)
|
walther@60351
|
111 |
fun Free_to_string (Free (str, _)) = str
|
walther@60351
|
112 |
| Free_to_string t =
|
walther@60351
|
113 |
if TermC.is_num t then TermC.string_of_num t else "|||||||||||||"(*the "largest" string*);
|
walther@60351
|
114 |
|
walther@60351
|
115 |
(* quick and dirty solution just before a field test *)
|
walther@60351
|
116 |
fun identifier (Free (id,_)) = id (* _a_ *)
|
walther@60351
|
117 |
| identifier (Const (\<^const_name>\<open>times\<close>, _) $ t1 $ t2) = (* 2*_a_, a*_b_, 3*a*_b_ *)
|
walther@60351
|
118 |
if TermC.is_atom t2
|
walther@60351
|
119 |
then Free_to_string t2
|
walther@60351
|
120 |
else
|
walther@60351
|
121 |
(case t1 of
|
walther@60351
|
122 |
Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' => (* 3*_a_ \<up> 2 *)
|
walther@60351
|
123 |
if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2
|
walther@60351
|
124 |
else "|||||||||||||"
|
walther@60351
|
125 |
| _ =>
|
walther@60351
|
126 |
(case t2 of
|
wenzelm@60405
|
127 |
Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp =>
|
walther@60351
|
128 |
if TermC.is_atom base andalso TermC.is_atom exp then
|
walther@60351
|
129 |
if TermC.is_num base then "|||||||||||||"
|
walther@60351
|
130 |
else Free_to_string base
|
walther@60351
|
131 |
else "|||||||||||||"
|
walther@60351
|
132 |
| _ => "|||||||||||||"))
|
wenzelm@60405
|
133 |
| identifier (Const (\<^const_name>\<open>realpow\<close>, _) $ base $ exp) = (* _a_\<up>2, _3_^2 *)
|
walther@60351
|
134 |
if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base
|
neuper@37950
|
135 |
else "|||||||||||||"
|
walther@60351
|
136 |
| identifier t = (* 12 *)
|
walther@60351
|
137 |
if TermC.is_num t
|
walther@60351
|
138 |
then TermC.string_of_num t
|
walther@60351
|
139 |
else "|||||||||||||" (*the "largest" string*);
|
neuper@37950
|
140 |
|
neuper@37950
|
141 |
(*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
|
neuper@37950
|
142 |
(* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
|
walther@60335
|
143 |
fun eval_kleiner _ _ (p as (Const (\<^const_name>\<open>PolyMinus.kleiner\<close>,_) $ a $ b)) _ =
|
walther@60325
|
144 |
if TermC.is_num b then
|
walther@60325
|
145 |
if TermC.is_num a then (*123 kleiner 32 = True !!!*)
|
walther@60325
|
146 |
if TermC.num_of_term a < TermC.num_of_term b then
|
walther@60325
|
147 |
SOME ((UnparseC.term p) ^ " = True",
|
walther@60325
|
148 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@60325
|
149 |
else SOME ((UnparseC.term p) ^ " = False",
|
walther@60325
|
150 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
walther@60325
|
151 |
else (* -1 * -2 kleiner 0 *)
|
walther@60325
|
152 |
SOME ((UnparseC.term p) ^ " = False",
|
walther@60325
|
153 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37950
|
154 |
else
|
walther@60325
|
155 |
if identifier a < identifier b then
|
walther@60325
|
156 |
SOME ((UnparseC.term p) ^ " = True",
|
walther@60325
|
157 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@60325
|
158 |
else SOME ((UnparseC.term p) ^ " = False",
|
walther@60325
|
159 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37950
|
160 |
| eval_kleiner _ _ _ _ = NONE;
|
neuper@37950
|
161 |
|
walther@60325
|
162 |
fun ist_monom t =
|
walther@60325
|
163 |
if TermC.is_atom t then true
|
walther@60325
|
164 |
else
|
walther@60325
|
165 |
case t of
|
walther@60335
|
166 |
Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 =>
|
walther@60325
|
167 |
ist_monom t1 andalso ist_monom t2
|
wenzelm@60405
|
168 |
| Const (\<^const_name>\<open>realpow\<close>, _) $ t1 $ t2 =>
|
walther@60325
|
169 |
ist_monom t1 andalso ist_monom t2
|
walther@60325
|
170 |
| _ => false
|
neuper@37950
|
171 |
|
neuper@37950
|
172 |
(* is this a univariate monomial ? *)
|
walther@60278
|
173 |
(*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
|
walther@60335
|
174 |
fun eval_ist_monom _ _ (p as (Const (\<^const_name>\<open>PolyMinus.ist_monom\<close>,_) $ a)) _ =
|
neuper@37950
|
175 |
if ist_monom a then
|
walther@59868
|
176 |
SOME ((UnparseC.term p) ^ " = True",
|
wneuper@59390
|
177 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@59868
|
178 |
else SOME ((UnparseC.term p) ^ " = False",
|
wneuper@59390
|
179 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37950
|
180 |
| eval_ist_monom _ _ _ _ = NONE;
|
neuper@37950
|
181 |
|
neuper@37950
|
182 |
|
neuper@37950
|
183 |
(** rewrite order **)
|
neuper@37950
|
184 |
|
neuper@37950
|
185 |
(** rulesets **)
|
neuper@37950
|
186 |
|
neuper@37950
|
187 |
val erls_ordne_alphabetisch =
|
walther@60358
|
188 |
Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty [
|
walther@60358
|
189 |
\<^rule_eval>\<open>kleiner\<close> (eval_kleiner ""),
|
walther@60358
|
190 |
\<^rule_eval>\<open>ist_monom\<close> (eval_ist_monom "")];
|
neuper@37950
|
191 |
|
neuper@37950
|
192 |
val ordne_alphabetisch =
|
walther@59851
|
193 |
Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
|
walther@60358
|
194 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
195 |
erls = erls_ordne_alphabetisch,
|
walther@60358
|
196 |
rules = [
|
walther@60358
|
197 |
\<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*)
|
walther@60358
|
198 |
\<^rule_thm>\<open>tausche_minus\<close>, (*"b kleiner a ==> (b - a) = (-a + b)"*)
|
walther@60358
|
199 |
\<^rule_thm>\<open>tausche_vor_plus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
|
walther@60358
|
200 |
\<^rule_thm>\<open>tausche_vor_minus\<close>, (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
|
walther@60358
|
201 |
\<^rule_thm>\<open>tausche_plus_plus\<close>, (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
|
walther@60358
|
202 |
\<^rule_thm>\<open>tausche_plus_minus\<close>, (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
|
walther@60358
|
203 |
\<^rule_thm>\<open>tausche_minus_plus\<close>, (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
|
walther@60358
|
204 |
\<^rule_thm>\<open>tausche_minus_minus\<close>], (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
|
walther@60358
|
205 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
206 |
|
neuper@37950
|
207 |
val fasse_zusammen =
|
walther@60358
|
208 |
Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
|
walther@60358
|
209 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
210 |
erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
|
walther@60385
|
211 |
[\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")],
|
walther@60358
|
212 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
213 |
rules = [
|
walther@60385
|
214 |
\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
|
walther@60385
|
215 |
\<^rule_thm>\<open>real_num_collect_assoc_r\<close>, (*"[| l is_num; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
|
walther@60385
|
216 |
\<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
|
walther@60385
|
217 |
\<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
|
neuper@37950
|
218 |
|
walther@60385
|
219 |
\<^rule_thm>\<open>subtrahiere\<close>, (*"[| l is_num; m is_num |] ==> m * v - l * v = (m - l) * v"*)
|
walther@60385
|
220 |
\<^rule_thm>\<open>subtrahiere_von_1\<close>, (*"[| l is_num |] ==> v - l * v = (1 - l) * v"*)
|
walther@60385
|
221 |
\<^rule_thm>\<open>subtrahiere_1\<close>, (*"[| l is_num; m is_num |] ==> m * v - v = (m - 1) * v"*)
|
neuper@37950
|
222 |
|
walther@60385
|
223 |
\<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, (*"[| l is_num; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
|
walther@60385
|
224 |
\<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>, (*"[| l is_num |] ==> (x + v) - l * v = x + (1 - l) * v"*)
|
walther@60385
|
225 |
\<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>, (*"[| m is_num |] ==> (x + m * v) - v = x + (m - 1) * v"*)
|
neuper@37950
|
226 |
|
walther@60385
|
227 |
\<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
|
walther@60385
|
228 |
\<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>, (*"[| l is_num |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
|
walther@60385
|
229 |
\<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>, (*"[| m is_num |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
|
neuper@37950
|
230 |
|
walther@60385
|
231 |
\<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_num; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
|
walther@60385
|
232 |
\<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
|
walther@60385
|
233 |
\<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
|
neuper@37950
|
234 |
|
walther@60358
|
235 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
walther@60358
|
236 |
\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
|
neuper@37950
|
237 |
|
walther@60358
|
238 |
(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
|
walther@60358
|
239 |
(a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
|
walther@60358
|
240 |
\<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*)
|
walther@60358
|
241 |
\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
|
walther@60358
|
242 |
|
walther@60385
|
243 |
\<^rule_thm>\<open>addiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) + m * v = (-l + m) *v"*)
|
walther@60385
|
244 |
\<^rule_thm>\<open>addiere_eins_vor_minus\<close>, (*"[| m is_num |] ==> - v + m * v = (-1 + m) * v"*)
|
walther@60385
|
245 |
\<^rule_thm>\<open>subtrahiere_vor_minus\<close>, (*"[| l is_num; m is_num |] ==> -(l * v) - m * v = (-l - m) *v"*)
|
walther@60385
|
246 |
\<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_num |] ==> - v - m * v = (-1 - m) * v"*)
|
walther@60358
|
247 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
248 |
|
neuper@37950
|
249 |
val verschoenere =
|
walther@59851
|
250 |
Rule_Def.Repeat{id = "verschoenere", preconds = [],
|
walther@60358
|
251 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
252 |
erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
|
walther@60358
|
253 |
[\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
|
walther@60358
|
254 |
rules = [
|
walther@60358
|
255 |
\<^rule_thm>\<open>vorzeichen_minus_weg1\<close>, (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
|
walther@60358
|
256 |
\<^rule_thm>\<open>vorzeichen_minus_weg2\<close>, (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
|
walther@60358
|
257 |
\<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
|
walther@60358
|
258 |
\<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
|
neuper@37950
|
259 |
|
walther@60358
|
260 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
neuper@37950
|
261 |
|
walther@60358
|
262 |
\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
|
walther@60358
|
263 |
\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
|
walther@60358
|
264 |
\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
|
walther@60358
|
265 |
\<^rule_thm>\<open>null_minus\<close>, (*"0 - a = -a"*)
|
walther@60358
|
266 |
\<^rule_thm>\<open>vor_minus_mal\<close>], (*"- a * b = (-a) * b"*)
|
walther@60358
|
267 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
268 |
|
neuper@37950
|
269 |
val klammern_aufloesen =
|
walther@59851
|
270 |
Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
|
walther@60358
|
271 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty,
|
walther@60358
|
272 |
calc = [], errpatts = [], erls = Rule_Set.Empty,
|
walther@60358
|
273 |
rules = [
|
walther@60358
|
274 |
\<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*)
|
walther@60358
|
275 |
\<^rule_thm>\<open>klammer_plus_minus\<close>, (*"a + (b - c) = (a + b) - c"*)
|
walther@60358
|
276 |
\<^rule_thm>\<open>klammer_minus_plus\<close>, (*"a - (b + c) = (a - b) - c"*)
|
walther@60358
|
277 |
\<^rule_thm>\<open>klammer_minus_minus\<close>], (*"a - (b - c) = (a - b) + c"*)
|
walther@60358
|
278 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
279 |
|
neuper@37950
|
280 |
val klammern_ausmultiplizieren =
|
walther@59851
|
281 |
Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
|
walther@60358
|
282 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty,
|
walther@60358
|
283 |
calc = [], errpatts = [], erls = Rule_Set.Empty,
|
walther@60358
|
284 |
rules = [
|
walther@60358
|
285 |
\<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
walther@60358
|
286 |
\<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
walther@60358
|
287 |
|
walther@60358
|
288 |
\<^rule_thm>\<open>klammer_mult_minus\<close>, (*"a * (b - c) = a * b - a * c"*)
|
walther@60358
|
289 |
\<^rule_thm>\<open>klammer_minus_mult\<close>], (*"(b - c) * a = b * a - c * a"*)
|
walther@60358
|
290 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
291 |
|
neuper@37950
|
292 |
val ordne_monome =
|
walther@60358
|
293 |
Rule_Def.Repeat {
|
walther@60358
|
294 |
id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
295 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
296 |
erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
|
walther@60358
|
297 |
\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
|
walther@60358
|
298 |
\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")],
|
walther@60358
|
299 |
rules = [
|
walther@60358
|
300 |
\<^rule_thm>\<open>tausche_mal\<close>, (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
|
walther@60358
|
301 |
\<^rule_thm>\<open>tausche_vor_mal\<close>, (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
|
walther@60358
|
302 |
\<^rule_thm>\<open>tausche_mal_mal\<close>, (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
|
walther@60358
|
303 |
\<^rule_thm>\<open>x_quadrat\<close>], (*"(x * a) * a = x * a \<up> 2"*)
|
walther@60358
|
304 |
scr = Rule.Empty_Prog};
|
neuper@37950
|
305 |
|
neuper@37950
|
306 |
val rls_p_33 =
|
walther@60358
|
307 |
Rule_Set.append_rules "rls_p_33" Rule_Set.empty [
|
walther@60358
|
308 |
Rule.Rls_ ordne_alphabetisch,
|
wneuper@59416
|
309 |
Rule.Rls_ fasse_zusammen,
|
walther@60358
|
310 |
Rule.Rls_ verschoenere];
|
neuper@37950
|
311 |
val rls_p_34 =
|
walther@60358
|
312 |
Rule_Set.append_rules "rls_p_34" Rule_Set.empty [
|
walther@60358
|
313 |
Rule.Rls_ klammern_aufloesen,
|
walther@60358
|
314 |
Rule.Rls_ ordne_alphabetisch,
|
walther@60358
|
315 |
Rule.Rls_ fasse_zusammen,
|
walther@60358
|
316 |
Rule.Rls_ verschoenere];
|
neuper@37950
|
317 |
val rechnen =
|
walther@60358
|
318 |
Rule_Set.append_rules "rechnen" Rule_Set.empty [
|
walther@60358
|
319 |
\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
|
walther@60358
|
320 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
|
walther@60358
|
321 |
\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
|
wneuper@59472
|
322 |
\<close>
|
wenzelm@60289
|
323 |
rule_set_knowledge
|
wenzelm@60286
|
324 |
ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
|
wenzelm@60286
|
325 |
fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and
|
wenzelm@60286
|
326 |
verschoenere = \<open>prep_rls' verschoenere\<close> and
|
wenzelm@60286
|
327 |
ordne_monome = \<open>prep_rls' ordne_monome\<close> and
|
wenzelm@60286
|
328 |
klammern_aufloesen = \<open>prep_rls' klammern_aufloesen\<close> and
|
wenzelm@60286
|
329 |
klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>
|
neuper@37950
|
330 |
|
neuper@37950
|
331 |
(** problems **)
|
wenzelm@60306
|
332 |
|
wenzelm@60306
|
333 |
problem pbl_vereinf_poly : "polynom/vereinfachen" = \<open>Rule_Set.Empty\<close>
|
wenzelm@60306
|
334 |
|
wenzelm@60306
|
335 |
problem pbl_vereinf_poly_minus : "plus_minus/polynom/vereinfachen" =
|
walther@60358
|
336 |
\<open>Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty [
|
walther@60358
|
337 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
|
wenzelm@60306
|
338 |
\<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
|
walther@60358
|
339 |
\<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
|
walther@60358
|
340 |
\<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
|
walther@60358
|
341 |
\<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
|
walther@60358
|
342 |
\<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
|
wenzelm@60306
|
343 |
Method: "simplification/for_polynomials/with_minus"
|
wenzelm@60306
|
344 |
CAS: "Vereinfache t_t"
|
wenzelm@60306
|
345 |
Given: "Term t_t"
|
wenzelm@60306
|
346 |
Where:
|
wenzelm@60306
|
347 |
"t_t is_polyexp"
|
wenzelm@60306
|
348 |
"Not (matchsub (?a + (?b + ?c)) t_t |
|
wenzelm@60306
|
349 |
matchsub (?a + (?b - ?c)) t_t |
|
wenzelm@60306
|
350 |
matchsub (?a - (?b + ?c)) t_t |
|
wenzelm@60306
|
351 |
matchsub (?a + (?b - ?c)) t_t )"
|
wenzelm@60306
|
352 |
"Not (matchsub (?a * (?b + ?c)) t_t |
|
wenzelm@60306
|
353 |
matchsub (?a * (?b - ?c)) t_t |
|
wenzelm@60306
|
354 |
matchsub ((?b + ?c) * ?a) t_t |
|
wenzelm@60306
|
355 |
matchsub ((?b - ?c) * ?a) t_t )"
|
wenzelm@60306
|
356 |
Find: "normalform n_n"
|
wenzelm@60306
|
357 |
|
wenzelm@60306
|
358 |
problem pbl_vereinf_poly_klammer : "klammer/polynom/vereinfachen" =
|
walther@60358
|
359 |
\<open>Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty [
|
walther@60358
|
360 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
|
wenzelm@60306
|
361 |
\<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
|
walther@60358
|
362 |
\<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
|
walther@60358
|
363 |
\<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
|
walther@60358
|
364 |
\<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
|
walther@60358
|
365 |
\<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
|
wenzelm@60306
|
366 |
Method: "simplification/for_polynomials/with_parentheses"
|
wenzelm@60306
|
367 |
CAS: "Vereinfache t_t"
|
wenzelm@60306
|
368 |
Given: "Term t_t"
|
wenzelm@60306
|
369 |
Where:
|
wenzelm@60306
|
370 |
"t_t is_polyexp"
|
wenzelm@60306
|
371 |
"Not (matchsub (?a * (?b + ?c)) t_t |
|
wenzelm@60306
|
372 |
matchsub (?a * (?b - ?c)) t_t |
|
wenzelm@60306
|
373 |
matchsub ((?b + ?c) * ?a) t_t |
|
wenzelm@60306
|
374 |
matchsub ((?b - ?c) * ?a) t_t )"
|
wenzelm@60306
|
375 |
Find: "normalform n_n"
|
wenzelm@60306
|
376 |
|
wenzelm@60306
|
377 |
problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
|
wenzelm@60306
|
378 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
|
wenzelm@60306
|
379 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
|
wenzelm@60306
|
380 |
Method: "simplification/for_polynomials/with_parentheses_mult"
|
wenzelm@60306
|
381 |
CAS: "Vereinfache t_t"
|
wenzelm@60306
|
382 |
Given: "Term t_t"
|
wenzelm@60306
|
383 |
Where: "t_t is_polyexp"
|
wenzelm@60306
|
384 |
Find: "normalform n_n"
|
wenzelm@60306
|
385 |
|
wenzelm@60306
|
386 |
problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close>
|
wenzelm@60306
|
387 |
|
wenzelm@60306
|
388 |
problem pbl_probe_poly : "polynom/probe" =
|
wenzelm@60306
|
389 |
\<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
|
wenzelm@60306
|
390 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
|
wenzelm@60306
|
391 |
Method: "probe/fuer_polynom"
|
wenzelm@60306
|
392 |
CAS: "Probe e_e w_w"
|
wenzelm@60306
|
393 |
Given: "Pruefe e_e" "mitWert w_w"
|
wenzelm@60306
|
394 |
Where: "e_e is_polyexp"
|
wenzelm@60306
|
395 |
Find: "Geprueft p_p"
|
wenzelm@60306
|
396 |
|
wenzelm@60306
|
397 |
problem pbl_probe_bruch : "bruch/probe" =
|
wenzelm@60306
|
398 |
\<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
|
wenzelm@60306
|
399 |
\<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
|
wenzelm@60306
|
400 |
Method: "probe/fuer_bruch"
|
wenzelm@60306
|
401 |
CAS: "Probe e_e w_w"
|
wenzelm@60306
|
402 |
Given: "Pruefe e_e" "mitWert w_w"
|
wenzelm@60306
|
403 |
Where: "e_e is_ratpolyexp"
|
wenzelm@60306
|
404 |
Find: "Geprueft p_p"
|
neuper@37950
|
405 |
|
neuper@37950
|
406 |
(** methods **)
|
wneuper@59545
|
407 |
|
wneuper@59504
|
408 |
partial_function (tailrec) simplify :: "real \<Rightarrow> real"
|
wneuper@59504
|
409 |
where
|
walther@59635
|
410 |
"simplify t_t = (
|
walther@59635
|
411 |
(Repeat(
|
walther@59637
|
412 |
(Try (Rewrite_Set ''ordne_alphabetisch'')) #>
|
walther@59637
|
413 |
(Try (Rewrite_Set ''fasse_zusammen'')) #>
|
walther@59635
|
414 |
(Try (Rewrite_Set ''verschoenere'')))
|
walther@59635
|
415 |
) t_t)"
|
wenzelm@60303
|
416 |
|
wenzelm@60303
|
417 |
method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =
|
wenzelm@60303
|
418 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
walther@60358
|
419 |
prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty [
|
walther@60358
|
420 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
|
walther@60358
|
421 |
\<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
|
walther@60358
|
422 |
\<^rule_thm>\<open>and_true\<close>, (*"(?a & True) = ?a"*)
|
walther@60358
|
423 |
\<^rule_thm>\<open>and_false\<close>, (*"(?a & False) = False"*)
|
walther@60358
|
424 |
\<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
|
walther@60358
|
425 |
\<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)],
|
wenzelm@60303
|
426 |
crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>
|
wenzelm@60303
|
427 |
Program: simplify.simps
|
wenzelm@60303
|
428 |
Given: "Term t_t"
|
wenzelm@60303
|
429 |
Where:
|
wenzelm@60303
|
430 |
"t_t is_polyexp"
|
wenzelm@60303
|
431 |
"Not (matchsub (?a + (?b + ?c)) t_t |
|
wenzelm@60303
|
432 |
matchsub (?a + (?b - ?c)) t_t |
|
wenzelm@60303
|
433 |
matchsub (?a - (?b + ?c)) t_t |
|
wenzelm@60303
|
434 |
matchsub (?a + (?b - ?c)) t_t)"
|
wenzelm@60303
|
435 |
Find: "normalform n_n"
|
wneuper@59545
|
436 |
|
wneuper@59504
|
437 |
partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
|
wneuper@59504
|
438 |
where
|
walther@59635
|
439 |
"simplify2 t_t = (
|
walther@59635
|
440 |
(Repeat(
|
walther@59637
|
441 |
(Try (Rewrite_Set ''klammern_aufloesen'')) #>
|
walther@59637
|
442 |
(Try (Rewrite_Set ''ordne_alphabetisch'')) #>
|
walther@59637
|
443 |
(Try (Rewrite_Set ''fasse_zusammen'')) #>
|
walther@59635
|
444 |
(Try (Rewrite_Set ''verschoenere'')))
|
walther@59635
|
445 |
) t_t)"
|
wenzelm@60303
|
446 |
|
wenzelm@60303
|
447 |
method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =
|
wenzelm@60303
|
448 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
wenzelm@60303
|
449 |
prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
|
wenzelm@60303
|
450 |
[(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
|
wenzelm@60303
|
451 |
crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
|
wenzelm@60303
|
452 |
Program: simplify2.simps
|
wenzelm@60303
|
453 |
Given: "Term t_t"
|
wenzelm@60303
|
454 |
Where: "t_t is_polyexp"
|
wenzelm@60303
|
455 |
Find: "normalform n_n"
|
wneuper@59545
|
456 |
|
wneuper@59504
|
457 |
partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
|
wneuper@59504
|
458 |
where
|
walther@59635
|
459 |
"simplify3 t_t = (
|
walther@59635
|
460 |
(Repeat(
|
walther@59637
|
461 |
(Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
|
walther@59637
|
462 |
(Try (Rewrite_Set ''discard_parentheses'')) #>
|
walther@59637
|
463 |
(Try (Rewrite_Set ''ordne_monome'')) #>
|
walther@59637
|
464 |
(Try (Rewrite_Set ''klammern_aufloesen'')) #>
|
walther@59637
|
465 |
(Try (Rewrite_Set ''ordne_alphabetisch'')) #>
|
walther@59637
|
466 |
(Try (Rewrite_Set ''fasse_zusammen'')) #>
|
walther@59635
|
467 |
(Try (Rewrite_Set ''verschoenere'')))
|
walther@59635
|
468 |
) t_t)"
|
wenzelm@60303
|
469 |
|
wenzelm@60303
|
470 |
method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =
|
wenzelm@60303
|
471 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
wenzelm@60303
|
472 |
prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
|
wenzelm@60303
|
473 |
[(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
|
wenzelm@60303
|
474 |
crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
|
wenzelm@60303
|
475 |
Program: simplify3.simps
|
wenzelm@60303
|
476 |
Given: "Term t_t"
|
wenzelm@60303
|
477 |
Where: "t_t is_polyexp"
|
wenzelm@60303
|
478 |
Find: "normalform n_n"
|
wenzelm@60303
|
479 |
|
wenzelm@60303
|
480 |
method met_probe : "probe" =
|
wenzelm@60303
|
481 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
|
wenzelm@60303
|
482 |
errpats = [], nrls = Rule_Set.Empty}\<close>
|
wneuper@59545
|
483 |
|
wneuper@59504
|
484 |
partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
|
wneuper@59504
|
485 |
where
|
walther@59635
|
486 |
"mache_probe e_e w_w = (
|
walther@59635
|
487 |
let
|
walther@59635
|
488 |
e_e = Take e_e;
|
walther@59635
|
489 |
e_e = Substitute w_w e_e
|
walther@59635
|
490 |
in (
|
walther@59635
|
491 |
Repeat (
|
walther@59637
|
492 |
(Try (Repeat (Calculate ''TIMES''))) #>
|
walther@59637
|
493 |
(Try (Repeat (Calculate ''PLUS'' ))) #>
|
walther@59635
|
494 |
(Try (Repeat (Calculate ''MINUS''))))
|
walther@59635
|
495 |
) e_e)"
|
wenzelm@60303
|
496 |
|
wenzelm@60303
|
497 |
method met_probe_poly : "probe/fuer_polynom" =
|
wenzelm@60303
|
498 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
wenzelm@60303
|
499 |
prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
|
wenzelm@60303
|
500 |
[(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
|
wenzelm@60303
|
501 |
crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>
|
wenzelm@60303
|
502 |
Program: mache_probe.simps
|
wenzelm@60303
|
503 |
Given: "Pruefe e_e" "mitWert w_w"
|
wenzelm@60303
|
504 |
Where: "e_e is_polyexp"
|
wenzelm@60303
|
505 |
Find: "Geprueft p_p"
|
wenzelm@60303
|
506 |
|
wenzelm@60303
|
507 |
method met_probe_bruch : "probe/fuer_bruch" =
|
wenzelm@60303
|
508 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
wenzelm@60303
|
509 |
prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
|
wenzelm@60303
|
510 |
[(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
|
wenzelm@60303
|
511 |
crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>
|
wenzelm@60303
|
512 |
Given: "Pruefe e_e" "mitWert w_w"
|
wenzelm@60303
|
513 |
Where: "e_e is_ratpolyexp"
|
wenzelm@60303
|
514 |
Find: "Geprueft p_p"
|
wenzelm@60303
|
515 |
|
wenzelm@60303
|
516 |
ML \<open>
|
walther@60278
|
517 |
\<close> ML \<open>
|
wneuper@59472
|
518 |
\<close>
|
neuper@37906
|
519 |
|
neuper@37906
|
520 |
end
|
neuper@37906
|
521 |
|