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