|
1 (* tools for arithmetic |
|
2 WN.8.3.01 |
|
3 use"../knowledge/Atools.ML"; |
|
4 use"knowledge/Atools.ML"; |
|
5 use"Atools.ML"; |
|
6 *) |
|
7 |
|
8 (* |
|
9 copy from doc/math-eng.tex WN.28.3.03 |
|
10 |
|
11 \section{Coding standards} |
|
12 \subsection{Rule sets} |
|
13 The actual version of the coding standards for rulesets is in {\tt /Isa02/Tools.ML} where it can be viewed using the knowledge browsers. |
|
14 |
|
15 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. |
|
16 \begin{description} |
|
17 |
|
18 \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). |
|
19 |
|
20 \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. |
|
21 |
|
22 \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. |
|
23 |
|
24 \end{description} |
|
25 The following rulesets are used for internal purposes and usually invisible to the (naive) user: |
|
26 \begin{description} |
|
27 |
|
28 \item [*\_erls] |
|
29 \item [*\_prls] |
|
30 \item [*\_srls] |
|
31 |
|
32 \end{description} |
|
33 {\tt append_rls, merge_rls, remove_rls} |
|
34 *) |
|
35 |
|
36 "******* Atools.ML begin *******"; |
|
37 theory' := overwritel (!theory', [("Atools.thy",Atools.thy)]); |
|
38 |
|
39 (** evaluation of numerals and special predicates on the meta-level **) |
|
40 (*-------------------------functions---------------------*) |
|
41 local (* rlang 09.02 *) |
|
42 (*.a 'c is coefficient of v' if v does occur in c.*) |
|
43 fun coeff_in v c = v mem (vars c); |
|
44 in |
|
45 fun occurs_in v t = coeff_in v t; |
|
46 end; |
|
47 |
|
48 (*("occurs_in", ("Atools.occurs'_in", eval_occurs'_in ""))*) |
|
49 fun eval_occurs_in _ _ |
|
50 (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ = |
|
51 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v)); |
|
52 writeln("@@@ eval_occurs_in: t= "^(term2str t));*) |
|
53 if occurs_in v t |
|
54 then Some ((term2str p) ^ " = True", |
|
55 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
56 else Some ((term2str p) ^ " = True", |
|
57 Trueprop $ (mk_equality (p, HOLogic.false_const)))) |
|
58 | eval_occurs_in _ _ _ _ = None; |
|
59 |
|
60 (*evaluate 'is_atom'*) |
|
61 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*) |
|
62 fun eval_is_atom (thmid:string) _ (t as (Const(op0,_) $ arg)) thy = |
|
63 (case arg of |
|
64 Free (n,_) => Some (mk_thmid thmid op0 n "", |
|
65 Trueprop $ (mk_equality (t, true_as_term))) |
|
66 | _ => Some (mk_thmid thmid op0 "" "", |
|
67 Trueprop $ (mk_equality (t, false_as_term)))) |
|
68 | eval_is_atom _ _ _ _ = None; |
|
69 |
|
70 (*evaluate 'is_even'*) |
|
71 fun even i = (i div 2) * 2 = i; |
|
72 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*) |
|
73 fun eval_is_even (thmid:string) _ (t as (Const(op0,_) $ arg)) thy = |
|
74 (case arg of |
|
75 Free (n,_) => |
|
76 (case int_of_str n of |
|
77 Some i => |
|
78 if even i then Some (mk_thmid thmid op0 n "", |
|
79 Trueprop $ (mk_equality (t, true_as_term))) |
|
80 else Some (mk_thmid thmid op0 "" "", |
|
81 Trueprop $ (mk_equality (t, false_as_term))) |
|
82 | _ => None) |
|
83 | _ => None) |
|
84 | eval_is_even _ _ _ _ = None; |
|
85 |
|
86 (*evaluate 'is_const'*) |
|
87 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*) |
|
88 fun eval_const (thmid:string) _ (t as (Const(op0,t0) $ arg)) (thy:theory) = |
|
89 (case arg of |
|
90 Const (n1,_) => |
|
91 Some (mk_thmid thmid op0 n1 "", |
|
92 Trueprop $ (mk_equality (t, false_as_term))) |
|
93 | Free (n1,_) => |
|
94 if is_numeral n1 |
|
95 then Some (mk_thmid thmid op0 n1 "", |
|
96 Trueprop $ (mk_equality (t, true_as_term))) |
|
97 else Some (mk_thmid thmid op0 n1 "", |
|
98 Trueprop $ (mk_equality (t, false_as_term))) |
|
99 | _ => None) |
|
100 | eval_const _ _ _ _ = None; |
|
101 |
|
102 (*. evaluate binary, associative, commutative operators: *,+,^ .*) |
|
103 (*("plus" ,("op +" ,eval_binop "#add_")), |
|
104 ("times" ,("op *" ,eval_binop "#mult_")), |
|
105 ("power_" ,("Atools.pow" ,eval_binop "#power_"))*) |
|
106 |
|
107 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = |
|
108 ("xxxxxx",op_,t,thy); |
|
109 *) |
|
110 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = |
|
111 thmid ^ "Float ((" ^ |
|
112 (string_of_int v11)^","^(string_of_int v12)^"), ("^ |
|
113 (string_of_int p11)^","^(string_of_int p12)^")) __ (("^ |
|
114 (string_of_int v21)^","^(string_of_int v22)^"), ("^ |
|
115 (string_of_int p21)^","^(string_of_int p22)^"))"; |
|
116 |
|
117 fun eval_binop (thmid:string) (op_:string) |
|
118 (t as ( Const(op0,t0) $ |
|
119 (Const(op0',t0') $ v $ t1) $ t2)) |
|
120 thy = (*binary . (v.n1).n2*) |
|
121 if op0 = op0' then |
|
122 case (numeral t1, numeral t2) of |
|
123 (Some n1, Some n2) => |
|
124 let val (T1,T2,Trange) = dest_binop_typ t0 |
|
125 val res = calc op0 n1 n2 |
|
126 val rhs = var_op_float v op_ t0 T1 res |
|
127 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
128 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
129 | _ => None |
|
130 else None |
|
131 | eval_binop (thmid:string) (op_:string) |
|
132 (t as |
|
133 (Const (op0, t0) $ t1 $ |
|
134 (Const (op0', t0') $ t2 $ v))) |
|
135 thy = (*binary . n1.(n2.v)*) |
|
136 if op0 = op0' then |
|
137 case (numeral t1, numeral t2) of |
|
138 (Some n1, Some n2) => |
|
139 let val (T1,T2,Trange) = dest_binop_typ t0 |
|
140 val res = calc op0 n1 n2 |
|
141 val rhs = float_op_var v op_ t0 T1 res |
|
142 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
143 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
144 | _ => None |
|
145 else None |
|
146 |
|
147 | eval_binop (thmid:string) (op_:string) |
|
148 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*) |
|
149 (case (numeral t1, numeral t2) of |
|
150 (Some n1, Some n2) => |
|
151 let val (T1,T2,Trange) = dest_binop_typ t0; |
|
152 val res = calc op0 n1 n2; |
|
153 val rhs = term_of_float Trange res; |
|
154 val prop = Trueprop $ (mk_equality (t, rhs)); |
|
155 in Some (mk_thmid_f thmid n1 n2, prop) end |
|
156 | _ => None) |
|
157 | eval_binop _ _ _ _ = None; |
|
158 (* |
|
159 > val Some (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy; |
|
160 > term2str t; |
|
161 val it = "-1 + 2 = 1" |
|
162 > val t = str2term "-1 * (-1 * a)"; |
|
163 > val Some (thmid, t) = eval_binop "#mult_" "op *" t thy; |
|
164 > term2str t; |
|
165 val it = "-1 * (-1 * a) = 1 * a"*) |
|
166 |
|
167 |
|
168 |
|
169 (*.evaluate < and <= for numerals.*) |
|
170 (*("le" ,("op <" ,eval_equ "#less_")), |
|
171 ("leq" ,("op <=" ,eval_equ "#less_equal_"))*) |
|
172 fun eval_equ (thmid:string) (op_:string) (t as |
|
173 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
174 (case (int_of_str n1, int_of_str n2) of |
|
175 (Some n1', Some n2') => |
|
176 if calc_equ (strip_thy op0) (n1', n2') |
|
177 then Some (mk_thmid thmid op0 n1 n2, |
|
178 Trueprop $ (mk_equality (t, true_as_term))) |
|
179 else Some (mk_thmid thmid op0 n1 n2, |
|
180 Trueprop $ (mk_equality (t, false_as_term))) |
|
181 | _ => None) |
|
182 |
|
183 | eval_equ _ _ _ _ = None; |
|
184 |
|
185 |
|
186 (*evaluate identity |
|
187 > reflI; |
|
188 val it = "(?t = ?t) = True" |
|
189 > val t = str2term "x = 0"; |
|
190 > val None = rewrite_ thy dummy_ord e_rls false reflI t; |
|
191 |
|
192 > val t = str2term "1 = 0"; |
|
193 > val None = rewrite_ thy dummy_ord e_rls false reflI t; |
|
194 ----------- thus needs Calc ! |
|
195 > val t = str2term "0 = 0"; |
|
196 > val Some (t',_) = rewrite_ thy dummy_ord e_rls false reflI t; |
|
197 > term2str t'; |
|
198 val it = "True" |
|
199 |
|
200 val t = str2term "Not (x = 0)"; |
|
201 atomt t; term2str t; |
|
202 *** ------------- |
|
203 *** Const ( Not) |
|
204 *** . Const ( op =) |
|
205 *** . . Free ( x, ) |
|
206 *** . . Free ( 0, ) |
|
207 val it = "x ~= 0" : string*) |
|
208 |
|
209 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of |
|
210 the arguments: thus this Calculation MUST be at the head of an rls*) |
|
211 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*) |
|
212 fun eval_ident (thmid:string) (op_:string) (t as |
|
213 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
214 if t1 = t2 |
|
215 then Some (mk_thmid thmid op0 |
|
216 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
217 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
218 Trueprop $ (mk_equality (t, true_as_term))) |
|
219 else Some (mk_thmid thmid op0 |
|
220 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
221 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
222 Trueprop $ (mk_equality (t, false_as_term))) |
|
223 | eval_ident _ _ _ _ = None; |
|
224 (* TODO |
|
225 > val t = str2term "x =!= 0"; |
|
226 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
227 > term2str t'; |
|
228 val str = "ident_(x)_(0)" : string |
|
229 val it = "(x =!= 0) = False" : string |
|
230 > val t = str2term "1 =!= 0"; |
|
231 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
232 > term2str t'; |
|
233 val str = "ident_(1)_(0)" : string |
|
234 val it = "(1 =!= 0) = False" : string |
|
235 > val t = str2term "0 =!= 0"; |
|
236 > val Some (str, t') = eval_ident "ident_" "b" t thy; |
|
237 > term2str t'; |
|
238 val str = "ident_(0)_(0)" : string |
|
239 val it = "(0 =!= 0) = True" : string |
|
240 *) |
|
241 |
|
242 (*.evaluate identity of terns, which stay ready for evaluation in turn; |
|
243 thus returns False only for numerals.*) |
|
244 (*("equal" ,("op =",eval_equal "#equal_")):calc*) |
|
245 fun eval_equal (thmid:string) (op_:string) (t as |
|
246 (Const (op0,t0) $ t1 $ t2 )) thy = |
|
247 if t1 = t2 |
|
248 then Some (mk_thmid thmid op0 |
|
249 ("("^(Sign.string_of_term (sign_of thy) t1)^")") |
|
250 ("("^(Sign.string_of_term (sign_of thy) t2)^")"), |
|
251 Trueprop $ (mk_equality (t, true_as_term))) |
|
252 else (case (is_num t1, is_num t2) of |
|
253 (true, true) => |
|
254 if free2int t1 = free2int t2 |
|
255 then Some (mk_thmid thmid op0 |
|
256 ("("^(term2str t1)^")") ("("^(term2str t2)^")"), |
|
257 Trueprop $ (mk_equality (t, true_as_term))) |
|
258 else Some (mk_thmid thmid op0 |
|
259 ("("^(term2str t1)^")") ("("^(term2str t2)^")"), |
|
260 Trueprop $ (mk_equality (t, false_as_term))) |
|
261 | _ => None) |
|
262 | eval_equal _ _ _ _ = None; |
|
263 (* |
|
264 > val t = str2term "(x + 1) = (x + 1)"; |
|
265 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
266 > term2str t'; |
|
267 val str = "equal_(x + 1)_(x + 1)" : string |
|
268 val it = "(x + 1 = x + 1) = True" : string |
|
269 > val t = str2term "x = 0"; |
|
270 > val None = eval_equal "equal_" "b" t thy; |
|
271 |
|
272 > val t = str2term "1 = 0"; |
|
273 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
274 > term2str t'; |
|
275 val str = "equal_(1)_(0)" : string |
|
276 val it = "(1 = 0) = False" : string |
|
277 > val t = str2term "0 = 0"; |
|
278 > val Some (str, t') = eval_equal "equal_" "b" t thy; |
|
279 > term2str t'; |
|
280 val str = "equal_(0)_(0)" : string |
|
281 val it = "(0 = 0) = True" : string |
|
282 *) |
|
283 |
|
284 |
|
285 (** evaluation on the metalevel **) |
|
286 |
|
287 (*. evaluate HOL.divide .*) |
|
288 (*("divide_" ,("HOL.divide" ,eval_cancel "#divide_"))*) |
|
289 fun eval_cancel (thmid:string) _ (t as |
|
290 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
|
291 (case (int_of_str n1, int_of_str n2) of |
|
292 (Some n1', Some n2') => |
|
293 let |
|
294 (*val _= writeln"@@@ eval_cancel Some";*) |
|
295 val sg = sign2 n1' n2'; |
|
296 val (T1,T2,Trange) = dest_binop_typ t0; |
|
297 val gcd' = gcd (abs n1') (abs n2'); |
|
298 in if gcd' = abs n2' |
|
299 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd') |
|
300 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
301 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
302 else if 0 < n2' andalso gcd' = 1 then None |
|
303 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd') |
|
304 ((abs n2') div gcd') |
|
305 val prop = Trueprop $ (mk_equality (t, rhs)) |
|
306 in Some (mk_thmid thmid op0 n1 n2, prop) end |
|
307 end |
|
308 | _ => ((*writeln"@@@ eval_cancel None";*)None)) |
|
309 |
|
310 | eval_cancel _ _ _ _ = None; |
|
311 |
|
312 |
|
313 local |
|
314 |
|
315 open Term; |
|
316 |
|
317 in |
|
318 fun termlessI (_:subst) uv = termless uv; |
|
319 fun term_ordI (_:subst) uv = term_ord uv; |
|
320 end; |
|
321 |
|
322 |
|
323 (** rule set, for evaluating list-expressions in scripts 8.01.02 |
|
324 |
|
325 val simprls = |
|
326 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
|
327 rules = [Calc ("Atools.ident",eval_ident "#ident_"), |
|
328 Calc ("Atools.Var",eval_var "#Var_"), |
|
329 Calc ("Atools.Length",eval_Length "#Length_"), |
|
330 Calc ("Atools.Nth",eval_Nth "#Nth_"), |
|
331 Calc ("op <",eval_equ "#less_"), |
|
332 Calc ("op <=",eval_equ "#less_equal_"), |
|
333 Calc ("Atools.ident",eval_ident "#ident_"), |
|
334 |
|
335 Thm ("if_True",num_str if_True), |
|
336 Thm ("if_False",num_str if_False) |
|
337 ], |
|
338 scr = Script ((term_of o the o (parse thy)) |
|
339 "empty_script") |
|
340 }:rls; *) |
|
341 |
|
342 (** rule set for evaluating listexpr in scripts FIXXXME -> ListG.ML**) |
|
343 val list_rls = |
|
344 Rls{id="list_rls",preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), |
|
345 erls = e_rls, srls = Erls, calc = [], asm_thm=[], |
|
346 rules = (*8.01: copied from*) |
|
347 [Thm ("length_Nil_",num_str length_Nil_), |
|
348 Thm ("length_Cons_",num_str length_Cons_), |
|
349 (* Thm ("",), |
|
350 Thm ("",), |
|
351 Thm ("",), |
|
352 Thm ("",), |
|
353 *) |
|
354 Calc ("op *",eval_binop "#mult_"), |
|
355 Calc ("op +", eval_binop "#add_"), |
|
356 |
|
357 Calc ("Atools.ident",eval_ident "#ident_"), |
|
358 Calc ("Atools.Var",eval_var "#Var_"), |
|
359 Calc ("Atools.Length",eval_Length "#Length_"),(*8.01 Thm length_Nil_ !*) |
|
360 Calc ("Atools.Nth",eval_Nth "#Nth_"), (*8.01 Thm nth_Cons_ !!*) |
|
361 Calc ("op <",eval_equ "#less_"), |
|
362 Calc ("op <=",eval_equ "#less_equal_"), |
|
363 Calc ("Atools.ident",eval_ident "#ident_"), |
|
364 |
|
365 Thm ("if_True",num_str if_True), |
|
366 Thm ("if_False",num_str if_False) |
|
367 ], scr = EmptyScr}:rls; |
|
368 |
|
369 ruleset' := overwritel (!ruleset', |
|
370 [("list_rls",list_rls) |
|
371 ]); |
|
372 |
|
373 val tless_true = dummy_ord; |
|
374 rew_ord' := overwritel (!rew_ord', |
|
375 [("tless_true", tless_true)]); |
|
376 |
|
377 val calculate_Atools = |
|
378 append_rls "calculate_Atools" e_rls |
|
379 [Calc ("op <",eval_equ "#less_"), |
|
380 Calc ("op <=",eval_equ "#less_equal_"), |
|
381 Calc ("op =",eval_equal "#equal_"), |
|
382 |
|
383 Thm ("real_unari_minus",num_str real_unari_minus), |
|
384 Calc ("op +",eval_binop "#add_"), |
|
385 Calc ("op -",eval_binop "#subtract_"), |
|
386 Calc ("op *",eval_binop "#mult_") |
|
387 ]; |
|
388 |
|
389 val Atools_erls = |
|
390 append_rls "Atools_erls" e_rls |
|
391 [Thm ("not_true",num_str not_true), |
|
392 Thm ("not_false",num_str not_false), |
|
393 Thm ("and_true",and_true), |
|
394 Thm ("and_false",and_false), |
|
395 Thm ("or_true",or_true), |
|
396 Thm ("or_false",or_false) |
|
397 ]; |
|
398 |
|
399 (*val atools_erls = waere zu testen ... |
|
400 merge_rls calculate_Atools |
|
401 (append_rls Atools_erls (*i.A. zu viele rules*) |
|
402 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
403 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
404 Calc ("Atools.occurs'_in", |
|
405 eval_occurs_in "#occurs_in"), |
|
406 Calc ("Tools.matches",eval_matches "#matches") |
|
407 ] (*i.A. zu viele rules*) |
|
408 );*) |
|
409 val atools_erls = |
|
410 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
|
411 erls = e_rls, srls = Erls, calc = [], asm_thm = [], |
|
412 rules = [Thm ("refl",num_str refl), |
|
413 Thm ("le_refl",num_str le_refl), |
|
414 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le), |
|
415 Thm ("not_true",num_str not_true), |
|
416 Thm ("not_false",num_str not_false), |
|
417 Thm ("and_true",and_true), |
|
418 Thm ("and_false",and_false), |
|
419 Thm ("or_true",or_true), |
|
420 Thm ("or_false",or_false), |
|
421 Thm ("and_commute",num_str and_commute), |
|
422 Thm ("or_commute",num_str or_commute), |
|
423 |
|
424 Calc ("op <",eval_equ "#less_"), |
|
425 Calc ("op <=",eval_equ "#less_equal_"), |
|
426 |
|
427 Calc ("Atools.ident",eval_ident "#ident_"), |
|
428 Calc ("Atools.is'_const",eval_const "#is_const_"), |
|
429 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
|
430 Calc ("Tools.matches",eval_matches "") |
|
431 ], |
|
432 scr = Script ((term_of o the o (parse thy)) |
|
433 "empty_script") |
|
434 }:rls; |
|
435 ruleset' := overwritel |
|
436 (!ruleset', |
|
437 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*) |
|
438 ]); |
|
439 "******* Atools.ML end *******"; |
|
440 |
|
441 |