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