|
1 (* tools for arithmetic |
|
2 WN.8.3.01 |
|
3 use"../IsacKnowledge/Atools.ML"; |
|
4 use"IsacKnowledge/Atools.ML"; |
|
5 use"Atools.ML"; |
|
6 *) |
|
7 |
|
8 (* |
|
9 copy from doc/math-eng.tex WN.28.3.03 |
|
10 WN071228 extended |
|
11 |
|
12 \section{Coding standards} |
|
13 |
|
14 %WN071228 extended -----vvv |
|
15 \subsection{Identifiers} |
|
16 Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem). |
|
17 |
|
18 This are the preliminary rules for naming identifiers> |
|
19 \begin{description} |
|
20 \item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}. |
|
21 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}. |
|
22 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~! |
|
23 \item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}. |
|
24 \item [???] ??? |
|
25 \item [???] ??? |
|
26 \end{description} |
|
27 %WN071228 extended -----^^^ |
|
28 |
|
29 |
|
30 \subsection{Rule sets} |
|
31 The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers. |
|
32 |
|
33 There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below. |
|
34 \begin{description} |
|
35 |
|
36 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents). |
|
37 |
|
38 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student. |
|
39 |
|
40 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only. |
|
41 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise). |
|
42 |
|
43 \end{description} |
|
44 The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc. |
|
45 The following rulesets are used for internal purposes and usually invisible to the (naive) user: |
|
46 \begin{description} |
|
47 |
|
48 \item [*\_erls] |
|
49 \item [*\_prls] |
|
50 \item [*\_srls] |
|
51 |
|
52 \end{description} |
|
53 {\tt append_rls, merge_rls, remove_rls} |
|
54 *) |
|
55 |
|
56 "******* Atools.ML begin *******"; |
|
57 theory' := overwritel (!theory', [("Atools.thy",Atools.thy)]); |
|
58 |
|
59 (** evaluation of numerals and special predicates on the meta-level **) |
|
60 (*-------------------------functions---------------------*) |
|
61 local (* rlang 09.02 *) |
|
62 (*.a 'c is coefficient of v' if v does occur in c.*) |
|
63 fun coeff_in v c = v mem (vars c); |
|
64 in |
|
65 fun occurs_in v t = coeff_in v t; |
|
66 end; |
|
67 |
|
68 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*) |
|
69 fun eval_occurs_in _ "Atools.occurs'_in" |
|
70 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ = |
|
71 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v)); |
|
72 writeln("@@@ eval_occurs_in: t= "^(term2str t));*) |
|
73 if occurs_in v t |
|
74 then Some ((term2str p) ^ " = True", |
|
75 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
76 else Some ((term2str p) ^ " = False", |
|
77 Trueprop $ (mk_equality (p, HOLogic.false_const)))) |
|
78 | eval_occurs_in _ _ _ _ = None; |
|
79 |
|
80 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*) |
|
81 fun some_occur_in vs t = |
|
82 let fun occurs_in' a b = occurs_in b a |
|
83 in foldl or_ (false, map (occurs_in' t) vs) end; |
|
84 |
|
85 (*("some_occur_in", ("Atools.some'_occur'_in", |
|
86 eval_some_occur_in "#eval_some_occur_in_"))*) |
|
87 fun eval_some_occur_in _ "Atools.some'_occur'_in" |
|
88 (p as (Const ("Atools.some'_occur'_in",_) |
|
89 $ vs $ t)) _ = |
|
90 if some_occur_in (isalist2list vs) t |
|
91 then Some ((term2str p) ^ " = True", |
|
92 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
93 else Some ((term2str p) ^ " = False", |
|
94 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
95 | eval_some_occur_in _ _ _ _ = None; |
|
96 |
|
97 |
|
98 |
|
99 |
|
100 (*evaluate 'is_atom'*) |
|
101 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*) |
|
102 fun eval_is_atom (thmid:string) "Atools.is'_atom" |
|
103 (t as (Const(op0,_) $ arg)) thy = |
|
104 (case arg of |
|
105 Free (n,_) => Some (mk_thmid thmid op0 n "", |
|
106 Trueprop $ (mk_equality (t, true_as_term))) |
|
107 | _ => Some (mk_thmid thmid op0 "" "", |
|
108 Trueprop $ (mk_equality (t, false_as_term)))) |
|
109 | eval_is_atom _ _ _ _ = None; |
|
110 |
|
111 (*evaluate 'is_even'*) |
|
112 fun even i = (i div 2) * 2 = i; |
|
113 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*) |
|
114 fun eval_is_even (thmid:string) "Atools.is'_even" |
|
115 (t as (Const(op0,_) $ arg)) thy = |
|
116 (case arg of |
|
117 Free (n,_) => |
|
118 (case int_of_str n of |
|
119 Some i => |
|
120 if even i then Some (mk_thmid thmid op0 n "", |
|
121 Trueprop $ (mk_equality (t, true_as_term))) |
|
122 else Some (mk_thmid thmid op0 "" "", |
|
123 Trueprop $ (mk_equality (t, false_as_term))) |
|
124 | _ => None) |
|
125 | _ => None) |
|
126 | eval_is_even _ _ _ _ = None; |
|
127 |
|
128 (*evaluate 'is_const'*) |
|
129 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*) |
|
130 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*) |
|
131 (t as (Const(op0,t0) $ arg)) (thy:theory) = |
|
132 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*) |
|
133 (case arg of |
|
134 Const (n1,_) => |
|
135 Some (mk_thmid thmid op0 n1 "", |
|
136 Trueprop $ (mk_equality (t, false_as_term))) |
|
137 | Free (n1,_) => |
|
138 if is_numeral n1 |
|
139 then Some (mk_thmid thmid op0 n1 "", |
|
140 Trueprop $ (mk_equality (t, true_as_term))) |
|
141 else Some (mk_thmid thmid op0 n1 "", |
|
142 Trueprop $ (mk_equality (t, false_as_term))) |
|
143 | Const ("Float.Float",_) => |
|
144 Some (mk_thmid thmid op0 (term2str arg) "", |
|
145 Trueprop $ (mk_equality (t, true_as_term))) |
|
146 | _ => (*None*) |
|
147 Some (mk_thmid thmid op0 (term2str arg) "", |
|
148 Trueprop $ (mk_equality (t, false_as_term)))) |
|
149 | eval_const _ _ _ _ = None; |
|
150 |
|
151 (*. evaluate binary, associative, commutative operators: *,+,^ .*) |
|
152 (*("plus" ,("op +" ,eval_binop "#add_")), |
|
153 ("times" ,("op *" ,eval_binop "#mult_")), |
|
154 ("power_" ,("Atools.pow" ,eval_binop "#power_"))*) |
|
155 |
|
156 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = |
|
157 ("xxxxxx",op_,t,thy); |
|
158 *) |
|
159 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = |
|
160 thmid ^ "Float ((" ^ |
|
161 (string_of_int v11)^","^(string_of_int v12)^"), ("^ |
|
162 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^ |
|
163 (string_of_int v21)^","^(string_of_int v22)^"), ("^ |
|
164 (string_of_int p21)^","^(string_of_int p22)^"))"; |
|
165 |
|
166 (*.convert int and float to internal floatingpoint prepresentation.*) |
|
167 fun numeral (Free (str, T)) = |
|
168 (case int_of_str str of |
|
169 Some i => Some ((i, 0), (0, 0)) |
|
170 | None => None) |
|
171 | numeral (Const ("Float.Float", _) $ |
|
172 (Const ("Pair", _) $ |
|
173 (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $ |
|
174 (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))= |
|
175 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of |
|
176 (Some v1', Some v2', Some p1', Some p2') => |
|
177 Some ((v1', v2'), (p1', p2')) |
|
178 | _ => None) |
|
179 | numeral _ = None; |
|
180 |
|
181 (*.evaluate binary associative operations.*) |
|
182 fun eval_binop (thmid:string) (op_:string) |
|
183 (t as ( Const(op0,t0) $ |
|
184 (Const(op0',t0') $ v $ t1) $ t2)) |
|
185 thy = (*binary . (v.n1).n2*) |
|
186 if op0 = op0' then |
|
187 case (numeral t1, numeral t2) of |
|
188 (Some n1, Some n2) => |
|
189 let val (T1,T2,Trange) = dest_binop_typ t0 |
|
190 val res = calc (if op0 = "op -" then "op +" else op0) n1 n2 |
|
191 (*WN071229 "HOL.divide" never tried*) |
|
192 val rhs = var_op_float v op_ t0 T1 res |
|
193 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
194 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
195 | _ => None |
|
196 else None |
|
197 | eval_binop (thmid:string) (op_:string) |
|
198 (t as |
|
199 (Const (op0, t0) $ t1 $ |
|
200 (Const (op0', t0') $ t2 $ v))) |
|
201 thy = (*binary . n1.(n2.v)*) |
|
202 if op0 = op0' then |
|
203 case (numeral t1, numeral t2) of |
|
204 (Some n1, Some n2) => |
|
205 if op0 = "op -" then None else |
|
206 let val (T1,T2,Trange) = dest_binop_typ t0 |
|
207 val res = calc op0 n1 n2 |
|
208 val rhs = float_op_var v op_ t0 T1 res |
|
209 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
210 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
211 | _ => None |
|
212 else None |
|
213 |
|
214 | eval_binop (thmid:string) (op_:string) |
|
215 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*) |
|
216 (case (numeral t1, numeral t2) of |
|
217 (Some n1, Some n2) => |
|
218 let val (T1,T2,Trange) = dest_binop_typ t0; |
|
219 val res = calc op0 n1 n2; |
|
220 val rhs = term_of_float Trange res; |
|
221 val prop = Trueprop $ (mk_equality (t, rhs)); |
|
222 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
223 | _ => None) |
|
224 | eval_binop _ _ _ _ = None; |
|
225 (* |
|
226 > val Some (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy; |
|
227 > term2str t; |
|
228 val it = "-1 + 2 = 1" |
|
229 > val t = str2term "-1 * (-1 * a)"; |
|
230 > val Some (thmid, t) = eval_binop "#mult_" "op *" t thy; |
|
231 > term2str t; |
|
232 val it = "-1 * (-1 * a) = 1 * a"*) |
|
233 |
|
234 |
|
235 |
|
236 (*.evaluate < and <= for numerals.*) |
|
237 (*("le" ,("op <" ,eval_equ "#less_")), |
|
238 ("leq" ,("op <=" ,eval_equ "#less_equal_"))*) |
|
239 fun eval_equ (thmid:string) (op_:string) (t as |
|
240 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
241 (case (int_of_str n1, int_of_str n2) of |
|
242 (Some n1', Some n2') => |
|
243 if calc_equ (strip_thy op0) (n1', n2') |
|
244 then Some (mk_thmid thmid op0 n1 n2, |
|
245 Trueprop $ (mk_equality (t, true_as_term))) |
|
246 else Some (mk_thmid thmid op0 n1 n2, |
|
247 Trueprop $ (mk_equality (t, false_as_term))) |
|
248 | _ => None) |
|
249 |
|
250 | eval_equ _ _ _ _ = None; |
|
251 |
|
252 |
|
253 (*evaluate identity |
|
254 > reflI; |
|
255 val it = "(?t = ?t) = True" |
|
256 > val t = str2term "x = 0"; |
|
257 > val None = rewrite_ thy dummy_ord e_rls false reflI t; |
|
258 |
|
259 > val t = str2term "1 = 0"; |
|
260 > val None = rewrite_ thy dummy_ord e_rls false reflI t; |
|
261 ----------- thus needs Calc ! |
|
262 > val t = str2term "0 = 0"; |
|
263 > val Some (t',_) = rewrite_ thy dummy_ord e_rls false reflI t; |
|
264 > term2str t'; |
|
265 val it = "True" |
|
266 |
|
267 val t = str2term "Not (x = 0)"; |
|
268 atomt t; term2str t; |
|
269 *** ------------- |
|
270 *** Const ( Not) |
|
271 *** . Const ( op =) |
|
272 *** . . Free ( x, ) |
|
273 *** . . Free ( 0, ) |
|
274 val it = "x ~= 0" : string*) |
|
275 |
|
276 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of |
|
277 the arguments: thus special handling by 'fun eval_binop'*) |
|
278 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*) |
|
279 fun eval_ident (thmid:string) "Atools.ident" (t as |
|
280 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
281 if t1 = t2 |
|
282 then Some (mk_thmid thmid op0 |
|
283 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
284 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
285 Trueprop $ (mk_equality (t, true_as_term))) |
|
286 else Some (mk_thmid thmid op0 |
|
287 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
288 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
289 Trueprop $ (mk_equality (t, false_as_term))) |
|
290 | eval_ident _ _ _ _ = None; |
|
291 (* TODO |
|
292 > val t = str2term "x =!= 0"; |
|
293 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
294 > term2str t'; |
|
295 val str = "ident_(x)_(0)" : string |
|
296 val it = "(x =!= 0) = False" : string |
|
297 > val t = str2term "1 =!= 0"; |
|
298 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
299 > term2str t'; |
|
300 val str = "ident_(1)_(0)" : string |
|
301 val it = "(1 =!= 0) = False" : string |
|
302 > val t = str2term "0 =!= 0"; |
|
303 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
304 > term2str t'; |
|
305 val str = "ident_(0)_(0)" : string |
|
306 val it = "(0 =!= 0) = True" : string |
|
307 *) |
|
308 |
|
309 (*.evaluate identity of terms, which stay ready for evaluation in turn; |
|
310 thus returns False only for atoms.*) |
|
311 (*("equal" ,("op =",eval_equal "#equal_")):calc*) |
|
312 fun eval_equal (thmid:string) "op =" (t as |
|
313 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
314 if t1 = t2 |
|
315 then ((*writeln"... eval_equal: t1 = t2 --> True";*) |
|
316 Some (mk_thmid thmid op0 |
|
317 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
318 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
319 Trueprop $ (mk_equality (t, true_as_term))) |
|
320 ) |
|
321 else (case (is_atom t1, is_atom t2) of |
|
322 (true, true) => |
|
323 ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*) |
|
324 Some (mk_thmid thmid op0 |
|
325 ("("^(term2str t1)^")") ("("^(term2str t2)^")"), |
|
326 Trueprop $ (mk_equality (t, false_as_term))) |
|
327 ) |
|
328 | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*) |
|
329 None)) |
|
330 | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit"; |
|
331 None); |
|
332 (* |
|
333 val t = str2term "x ~= 0"; |
|
334 val None = eval_equal "equal_" "b" t thy; |
|
335 |
|
336 |
|
337 > val t = str2term "(x + 1) = (x + 1)"; |
|
338 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
339 > term2str t'; |
|
340 val str = "equal_(x + 1)_(x + 1)" : string |
|
341 val it = "(x + 1 = x + 1) = True" : string |
|
342 > val t = str2term "x = 0"; |
|
343 > val None = eval_equal "equal_" "b" t thy; |
|
344 |
|
345 > val t = str2term "1 = 0"; |
|
346 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
347 > term2str t'; |
|
348 val str = "equal_(1)_(0)" : string |
|
349 val it = "(1 = 0) = False" : string |
|
350 > val t = str2term "0 = 0"; |
|
351 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
352 > term2str t'; |
|
353 val str = "equal_(0)_(0)" : string |
|
354 val it = "(0 = 0) = True" : string |
|
355 *) |
|
356 |
|
357 |
|
358 (** evaluation on the metalevel **) |
|
359 |
|
360 (*. evaluate HOL.divide .*) |
|
361 (*("divide_" ,("HOL.divide" ,eval_cancel "#divide_"))*) |
|
362 fun eval_cancel (thmid:string) "HOL.divide" (t as |
|
363 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
364 (case (int_of_str n1, int_of_str n2) of |
|
365 (Some n1', Some n2') => |
|
366 let |
|
367 val sg = sign2 n1' n2'; |
|
368 val (T1,T2,Trange) = dest_binop_typ t0; |
|
369 val gcd' = gcd (abs n1') (abs n2'); |
|
370 in if gcd' = abs n2' |
|
371 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd') |
|
372 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
373 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
374 else if 0 < n2' andalso gcd' = 1 then None |
|
375 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd') |
|
376 ((abs n2') div gcd') |
|
377 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
378 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
379 end |
|
380 | _ => ((*writeln"@@@ eval_cancel None";*)None)) |
|
381 |
|
382 | eval_cancel _ _ _ _ = None; |
|
383 |
|
384 (*. get the argument from a function-definition.*) |
|
385 (*("argument_in" ,("Atools.argument'_in", |
|
386 eval_argument_in "Atools.argument'_in"))*) |
|
387 fun eval_argument_in _ "Atools.argument'_in" |
|
388 (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ = |
|
389 if is_Free arg (*could be something to be simplified before*) |
|
390 then Some (term2str t ^ " = " ^ term2str arg, |
|
391 Trueprop $ (mk_equality (t, arg))) |
|
392 else None |
|
393 | eval_argument_in _ _ _ _ = None; |
|
394 |
|
395 (*.check if the function-identifier of the first argument matches |
|
396 the function-identifier of the lhs of the second argument.*) |
|
397 (*("sameFunId" ,("Atools.sameFunId", |
|
398 eval_same_funid "Atools.sameFunId"))*) |
|
399 fun eval_sameFunId _ "Atools.sameFunId" |
|
400 (p as Const ("Atools.sameFunId",_) $ |
|
401 (f1 $ _) $ |
|
402 (Const ("op =", _) $ (f2 $ _) $ _)) _ = |
|
403 if f1 = f2 |
|
404 then Some ((term2str p) ^ " = True", |
|
405 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
406 else Some ((term2str p) ^ " = False", |
|
407 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
408 | eval_sameFunId _ _ _ _ = None; |
|
409 |
|
410 |
|
411 (*.from a list of fun-definitions "f x = ..." as 2nd argument |
|
412 filter the elements with the same fun-identfier in "f y" |
|
413 as the fst argument; |
|
414 this is, because Isabelles filter takes more than 1 sec.*) |
|
415 fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2 |
|
416 | same_funid f1 t = raise error ("same_funid called with t = (" |
|
417 ^term2str f1^") ("^term2str t^")"); |
|
418 (*("filter_sameFunId" ,("Atools.filter'_sameFunId", |
|
419 eval_filter_sameFunId "Atools.filter'_sameFunId"))*) |
|
420 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" |
|
421 (p as Const ("Atools.filter'_sameFunId",_) $ |
|
422 (fid $ _) $ fs) _ = |
|
423 let val fs' = ((list2isalist HOLogic.boolT) o |
|
424 (filter (same_funid fid))) (isalist2list fs) |
|
425 in Some (term2str (mk_equality (p, fs')), |
|
426 Trueprop $ (mk_equality (p, fs'))) end |
|
427 | eval_filter_sameFunId _ _ _ _ = None; |
|
428 |
|
429 |
|
430 (*make a list of terms to a sum*) |
|
431 fun list2sum [] = error ("list2sum called with []") |
|
432 | list2sum [s] = s |
|
433 | list2sum (s::ss) = |
|
434 let fun sum su [s'] = |
|
435 Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
|
436 $ su $ s' |
|
437 | sum su (s'::ss') = |
|
438 sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
|
439 $ su $ s') ss' |
|
440 in sum s ss end; |
|
441 |
|
442 (*make a list of equalities to the sum of the lhs*) |
|
443 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*) |
|
444 fun eval_boollist2sum _ "Atools.boollist2sum" |
|
445 (p as Const ("Atools.boollist2sum", _) $ |
|
446 (l as Const ("List.list.Cons", _) $ _ $ _)) _ = |
|
447 let val isal = isalist2list l |
|
448 val lhss = map lhs isal |
|
449 val sum = list2sum lhss |
|
450 in Some ((term2str p) ^ " = " ^ (term2str sum), |
|
451 Trueprop $ (mk_equality (p, sum))) |
|
452 end |
|
453 | eval_boollist2sum _ _ _ _ = None; |
|
454 |
|
455 |
|
456 |
|
457 local |
|
458 |
|
459 open Term; |
|
460 |
|
461 in |
|
462 fun termlessI (_:subst) uv = termless uv; |
|
463 fun term_ordI (_:subst) uv = term_ord uv; |
|
464 end; |
|
465 |
|
466 |
|
467 (** rule set, for evaluating list-expressions in scripts 8.01.02 **) |
|
468 |
|
469 |
|
470 val list_rls = |
|
471 append_rls "list_rls" list_rls |
|
472 [Calc ("op *",eval_binop "#mult_"), |
|
473 Calc ("op +", eval_binop "#add_"), |
|
474 Calc ("op <",eval_equ "#less_"), |
|
475 Calc ("op <=",eval_equ "#less_equal_"), |
|
476 Calc ("Atools.ident",eval_ident "#ident_"), |
|
477 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*) |
|
478 |
|
479 Calc ("Tools.Vars",eval_var "#Vars_"), |
|
480 |
|
481 Thm ("if_True",num_str if_True), |
|
482 Thm ("if_False",num_str if_False) |
|
483 ]; |
|
484 |
|
485 ruleset' := overwritelthy thy (!ruleset', |
|
486 [("list_rls",list_rls) |
|
487 ]); |
|
488 |
|
489 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*) |
|
490 val tless_true = dummy_ord; |
|
491 rew_ord' := overwritel (!rew_ord', |
|
492 [("tless_true", tless_true), |
|
493 ("e_rew_ord'", tless_true), |
|
494 ("dummy_ord", dummy_ord)]); |
|
495 |
|
496 val calculate_Atools = |
|
497 append_rls "calculate_Atools" e_rls |
|
498 [Calc ("op <",eval_equ "#less_"), |
|
499 Calc ("op <=",eval_equ "#less_equal_"), |
|
500 Calc ("op =",eval_equal "#equal_"), |
|
501 |
|
502 Thm ("real_unari_minus",num_str real_unari_minus), |
|
503 Calc ("op +",eval_binop "#add_"), |
|
504 Calc ("op -",eval_binop "#sub_"), |
|
505 Calc ("op *",eval_binop "#mult_") |
|
506 ]; |
|
507 |
|
508 val Atools_erls = |
|
509 append_rls "Atools_erls" e_rls |
|
510 [Calc ("op =",eval_equal "#equal_"), |
|
511 Thm ("not_true",num_str not_true), |
|
512 (*"(~ True) = False"*) |
|
513 Thm ("not_false",num_str not_false), |
|
514 (*"(~ False) = True"*) |
|
515 Thm ("and_true",and_true), |
|
516 (*"(?a & True) = ?a"*) |
|
517 Thm ("and_false",and_false), |
|
518 (*"(?a & False) = False"*) |
|
519 Thm ("or_true",or_true), |
|
520 (*"(?a | True) = True"*) |
|
521 Thm ("or_false",or_false), |
|
522 (*"(?a | False) = ?a"*) |
|
523 |
|
524 Thm ("rat_leq1",rat_leq1), |
|
525 Thm ("rat_leq2",rat_leq2), |
|
526 Thm ("rat_leq3",rat_leq3), |
|
527 Thm ("refl",num_str refl), |
|
528 Thm ("le_refl",num_str le_refl), |
|
529 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
530 |
|
531 Calc ("op <",eval_equ "#less_"), |
|
532 Calc ("op <=",eval_equ "#less_equal_"), |
|
533 |
|
534 Calc ("Atools.ident",eval_ident "#ident_"), |
|
535 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
536 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
|
537 Calc ("Tools.matches",eval_matches "") |
|
538 ]; |
|
539 |
|
540 val Atools_crls = |
|
541 append_rls "Atools_crls" e_rls |
|
542 [Calc ("op =",eval_equal "#equal_"), |
|
543 Thm ("not_true",num_str not_true), |
|
544 Thm ("not_false",num_str not_false), |
|
545 Thm ("and_true",and_true), |
|
546 Thm ("and_false",and_false), |
|
547 Thm ("or_true",or_true), |
|
548 Thm ("or_false",or_false), |
|
549 |
|
550 Thm ("rat_leq1",rat_leq1), |
|
551 Thm ("rat_leq2",rat_leq2), |
|
552 Thm ("rat_leq3",rat_leq3), |
|
553 Thm ("refl",num_str refl), |
|
554 Thm ("le_refl",num_str le_refl), |
|
555 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
556 |
|
557 Calc ("op <",eval_equ "#less_"), |
|
558 Calc ("op <=",eval_equ "#less_equal_"), |
|
559 |
|
560 Calc ("Atools.ident",eval_ident "#ident_"), |
|
561 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
562 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
|
563 Calc ("Tools.matches",eval_matches "") |
|
564 ]; |
|
565 |
|
566 (*val atools_erls = ... waere zu testen ... |
|
567 merge_rls calculate_Atools |
|
568 (append_rls Atools_erls (*i.A. zu viele rules*) |
|
569 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
570 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
571 Calc ("Atools.occurs'_in", |
|
572 eval_occurs_in "#occurs_in"), |
|
573 Calc ("Tools.matches",eval_matches "#matches") |
|
574 ] (*i.A. zu viele rules*) |
|
575 );*) |
|
576 (* val atools_erls = prep_rls( |
|
577 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
|
578 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
|
579 rules = [Thm ("refl",num_str refl), |
|
580 Thm ("le_refl",num_str le_refl), |
|
581 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
582 Thm ("not_true",num_str not_true), |
|
583 Thm ("not_false",num_str not_false), |
|
584 Thm ("and_true",and_true), |
|
585 Thm ("and_false",and_false), |
|
586 Thm ("or_true",or_true), |
|
587 Thm ("or_false",or_false), |
|
588 Thm ("and_commute",num_str and_commute), |
|
589 Thm ("or_commute",num_str or_commute), |
|
590 |
|
591 Calc ("op <",eval_equ "#less_"), |
|
592 Calc ("op <=",eval_equ "#less_equal_"), |
|
593 |
|
594 Calc ("Atools.ident",eval_ident "#ident_"), |
|
595 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
596 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
|
597 Calc ("Tools.matches",eval_matches "") |
|
598 ], |
|
599 scr = Script ((term_of o the o (parse thy)) |
|
600 "empty_script") |
|
601 }:rls); |
|
602 ruleset' := overwritelth thy |
|
603 (!ruleset', |
|
604 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*) |
|
605 ]); |
|
606 *) |
|
607 "******* Atools.ML end *******"; |
|
608 |
|
609 calclist':= overwritel (!calclist', |
|
610 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")), |
|
611 ("some_occur_in", |
|
612 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")), |
|
613 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")), |
|
614 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")), |
|
615 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")), |
|
616 ("le" ,("op <" ,eval_equ "#less_")), |
|
617 ("leq" ,("op <=" ,eval_equ "#less_equal_")), |
|
618 ("ident" ,("Atools.ident",eval_ident "#ident_")), |
|
619 ("equal" ,("op =",eval_equal "#equal_")), |
|
620 ("plus" ,("op +" ,eval_binop "#add_")), |
|
621 ("minus" ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls |
|
622 no script with "minus"*) |
|
623 ("times" ,("op *" ,eval_binop "#mult_")), |
|
624 ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")), |
|
625 ("power_" ,("Atools.pow" ,eval_binop "#power_")), |
|
626 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum "")) |
|
627 ]); |
|
628 |
|
629 val list_rls = prep_rls( |
|
630 merge_rls "list_erls" |
|
631 (Rls {id="replaced",preconds = [], |
|
632 rew_ord = ("termlessI", termlessI), |
|
633 erls = Rls {id="list_elrs", preconds = [], |
|
634 rew_ord = ("termlessI",termlessI), |
|
635 erls = e_rls, |
|
636 srls = Erls, calc = [], (*asm_thm = [],*) |
|
637 rules = [Calc ("op +", eval_binop "#add_"), |
|
638 Calc ("op <",eval_equ "#less_") |
|
639 (* ~~~~~~ for nth_Cons_*) |
|
640 ], |
|
641 scr = EmptyScr}, |
|
642 srls = Erls, calc = [], (*asm_thm = [], *) |
|
643 rules = [], scr = EmptyScr}) |
|
644 list_rls); |
|
645 ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]); |