|
1 (* calculate values for function constants |
|
2 (c) Walther Neuper 000106 |
|
3 |
|
4 use"ProgLang/calculate.sml"; |
|
5 *) |
|
6 |
|
7 |
|
8 (* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *) |
|
9 |
|
10 val aT = Type ("'a", []); |
|
11 (* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)": |
|
12 (1) |
|
13 > val (TFree(ss2,TT2)) = T2; |
|
14 val ss2 = "'a" : string |
|
15 val TT2 = ["term"] : sort |
|
16 (2) |
|
17 > val (Type(ss2',TT2')) = T2'; |
|
18 val ss2' = "RealDef.real" : string |
|
19 val TT2' = [] : typ list |
|
20 (3) |
|
21 val realType = TFree ("RealDef.real", HOLogic.termS); |
|
22 is different internally, too; |
|
23 |
|
24 (1) .. (3) are displayed equally !!! |
|
25 *) |
|
26 |
|
27 |
|
28 |
|
29 (* 30.1.00: generating special terms for ME: |
|
30 (1) binary numerals reconverted to Free ("#num",...) |
|
31 by libarary_G.num_str: called from parse (below) and |
|
32 interface_ME_ISA for all thms used |
|
33 (compare HOLogic.dest_binum) |
|
34 (2) 'a types converted to RealDef.real by typ_a2real |
|
35 in parse below |
|
36 (3) binary operators fixed to type real in RatArith.thy |
|
37 (trick by Markus Wenzel) |
|
38 *) |
|
39 |
|
40 |
|
41 |
|
42 |
|
43 (** calculate numerals **) |
|
44 |
|
45 (*27.3.00: problems with patterns below: |
|
46 "Vars (a // #2 = r * xxxxx b)" doesn't work, but |
|
47 "Vars (a // #2 = r * sqrt b)" works |
|
48 *) |
|
49 |
|
50 fun popt2str (SOME (str, term)) = "SOME "^term2str term |
|
51 | popt2str NONE = "NONE"; |
|
52 |
|
53 (* scan a term for applying eval_fn ef |
|
54 args |
|
55 thy: |
|
56 op_: operator (as string) selecting the root of the pair |
|
57 ef : fn : (string -> term -> theory -> (string * term) option) |
|
58 ^^^^^^... for creating the string for the resulting theorem |
|
59 t : term to be scanned |
|
60 result: |
|
61 (string * term) option: found by the eval_* -function of type |
|
62 fn : string -> string -> term -> theory -> (string * term) option |
|
63 ^^^^^^... the selecting operator op_ (variable for eval_binop) |
|
64 *) |
|
65 fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option) |
|
66 (t as (Const(op0,t0) $ arg)) = (* unary fns *) |
|
67 (* val (thy, op_, (ef), (t as (Const(op0,t0) $ arg))) = |
|
68 (thy, op_, eval_fn, ct); |
|
69 *) |
|
70 if op_ = op0 then |
|
71 let val popt = ef op_ t thy |
|
72 in case popt of |
|
73 SOME _ => popt |
|
74 | NONE => get_pair thy op_ ef arg end |
|
75 else get_pair thy op_ ef arg |
|
76 |
|
77 | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) = |
|
78 (* val (thy, "Atools.ident", ef, t as (Const(op0,_) $ t1 $ t2)) = |
|
79 (thy, op_, eval_fn, ct); |
|
80 *) |
|
81 ef "Atools.ident" t thy (* not nested *) |
|
82 |
|
83 | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*) |
|
84 (* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) = |
|
85 (thy, op_, eval_fn, ct); |
|
86 *) |
|
87 ((*writeln("1.. get_pair: binop = "^op_);*) |
|
88 if op_ = op0 then |
|
89 let val popt = ef op_ t thy |
|
90 (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*) |
|
91 in case popt of |
|
92 SOME (id,_) => popt |
|
93 | NONE => |
|
94 let val popt = get_pair thy op_ ef t1 |
|
95 (*val _ = writeln("3.. get_pair: "^term2str t1^ |
|
96 " -> "^popt2str popt)*) |
|
97 in case popt of |
|
98 SOME (id,_) => popt |
|
99 | NONE => get_pair thy op_ ef t2 |
|
100 end |
|
101 end |
|
102 else (*search subterms*) |
|
103 let val popt = get_pair thy op_ ef t1 |
|
104 (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*) |
|
105 in case popt of |
|
106 SOME (id,_) => popt |
|
107 | NONE => get_pair thy op_ ef t2 |
|
108 end) |
|
109 | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*) |
|
110 ((*writeln("### get_pair 4a: t= "^term2str t); |
|
111 writeln("### get_pair 4a: op_= "^op_); |
|
112 writeln("### get_pair 4a: op0= "^op0);*) |
|
113 if op_ = op0 then |
|
114 case ef op_ t thy of |
|
115 SOME tt => SOME tt |
|
116 | NONE => (case get_pair thy op_ ef t2 of |
|
117 SOME tt => SOME tt |
|
118 | NONE => get_pair thy op_ ef t3) |
|
119 else (case get_pair thy op_ ef t1 of |
|
120 SOME tt => SOME tt |
|
121 | NONE => (case get_pair thy op_ ef t2 of |
|
122 SOME tt => SOME tt |
|
123 | NONE => get_pair thy op_ ef t3))) |
|
124 | get_pair thy op_ ef (Const _) = NONE |
|
125 | get_pair thy op_ ef (Free _) = NONE |
|
126 | get_pair thy op_ ef (Var _) = NONE |
|
127 | get_pair thy op_ ef (Bound _) = NONE |
|
128 | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body |
|
129 | get_pair thy op_ ef (t1$t2) = |
|
130 let(*val _= writeln("5.. get_pair t1 $ t2: "^term2str t1^" |
|
131 $ "^term2str t2)*) |
|
132 val popt = get_pair thy op_ ef t1 |
|
133 in case popt of |
|
134 SOME _ => popt |
|
135 | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*) |
|
136 get_pair thy op_ ef t2) |
|
137 end; |
|
138 (* |
|
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
|
140 > val eval_fn = the (assoc (!eval_list, "op +")); |
|
141 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
|
142 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
143 > atomty t'; |
|
144 > |
|
145 > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; |
|
146 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
|
147 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
148 > |
|
149 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; |
|
150 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
|
151 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
152 > |
|
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; |
|
154 > atomty t; |
|
155 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
|
156 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
157 > val it = "#3 + (#4 + a) = #7 + a" : string |
|
158 > |
|
159 > |
|
160 > val t = (term_of o the o (parse thy)) "#-4//#-2"; |
|
161 > val eval_fn = the (assoc (!eval_list, "cancel")); |
|
162 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
|
163 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
164 > |
|
165 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
|
166 > eval_binop "xxx" "pow" t thy; |
|
167 > val eval_fn = (eval_binop "xxx") |
|
168 > : string -> term -> theory -> (string * term) option; |
|
169 > val SOME (id,t') = get_pair thy "pow" eval_fn t; |
|
170 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
171 > val eval_fn = the (assoc (!eval_list, "pow")); |
|
172 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
|
173 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
174 > |
|
175 > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; |
|
176 > val eval_fn = the (assoc (!eval_list, "op *")); |
|
177 > val (SOME (id,t')) = get_pair thy "op *" eval_fn t; |
|
178 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
179 > |
|
180 > val t = (term_of o the o (parse thy)) "#0 < #4"; |
|
181 > val eval_fn = the (assoc (!eval_list, "op <")); |
|
182 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
|
183 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
184 > val t = (term_of o the o (parse thy)) "#0 < #-4"; |
|
185 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
|
186 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
187 > |
|
188 > val t = (term_of o the o (parse thy)) "#3 is_const"; |
|
189 > val eval_fn = the (assoc (!eval_list, "is'_const")); |
|
190 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
|
191 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
192 > val t = (term_of o the o (parse thy)) "a is_const"; |
|
193 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
|
194 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
195 > |
|
196 > val t = (term_of o the o (parse thy)) "#6//(#8::real)"; |
|
197 > val eval_fn = the (assoc (!eval_list, "cancel")); |
|
198 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
|
199 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
200 > |
|
201 > val t = (term_of o the o (parse thy)) "sqrt #12"; |
|
202 > val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt")); |
|
203 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
|
204 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
205 > val it = "sqrt #12 = #2 * sqrt #3 " : string |
|
206 > |
|
207 > val t = (term_of o the o (parse thy)) "sqrt #9"; |
|
208 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
|
209 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
210 > |
|
211 > val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]"; |
|
212 > val eval_fn = the (assoc (!eval_list, "Tools.Nth")); |
|
213 > val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t; |
|
214 > Syntax.string_of_term (thy2ctxt thy) t'; |
|
215 *) |
|
216 |
|
217 (* val ((op_, eval_fn),ct)=(cc,pre); |
|
218 (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e; |
|
219 parse thy "" |
|
220 *) |
|
221 (*.get a thm from an op_ somewhere in the term; |
|
222 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*) |
|
223 fun get_calculation_ thy (op_, eval_fn) ct = |
|
224 (* val (thy, (op_, eval_fn), ct) = |
|
225 (thy, (the (assoc(!calclist',"order_system"))), t); |
|
226 *) |
|
227 case get_pair thy op_ eval_fn ct of |
|
228 NONE => ((*writeln("@@@ get_calculation: NONE, op_="^op_); |
|
229 writeln("@@@ get_calculation: ct= ");atomty ct;*) |
|
230 NONE) |
|
231 | SOME (thmid,t) => |
|
232 ((*writeln("@@@ get_calculation: NONE, op_="^op_); |
|
233 writeln("@@@ get_calculation: ct= ");atomty ct;*) |
|
234 SOME (thmid, (make_thm o (cterm_of thy)) t)); |
|
235 (* |
|
236 > val ct = (the o (parse thy)) "#9 is_const"; |
|
237 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; |
|
238 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") |
|
239 |
|
240 > val ct = (the o (parse thy)) "sqrt #9"; |
|
241 > get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct; |
|
242 val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option |
|
243 |
|
244 > val ct = (the o (parse thy)) "#4<#4"; |
|
245 > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#"; |
|
246 |
|
247 val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]") |
|
248 |
|
249 > val ct = (the o (parse thy)) "a<#4"; |
|
250 > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct; |
|
251 val it = NONE : (string * thm) option |
|
252 |
|
253 > val ct = (the o (parse thy)) "#5<=#4"; |
|
254 > get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct; |
|
255 val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]") |
|
256 |
|
257 -------------------------------------------------------------------6.8.02: |
|
258 val thy = SqRoot.thy; |
|
259 val t = (term_of o the o (parse thy)) "1+2"; |
|
260 get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t; |
|
261 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option |
|
262 -------------------------------------------------------------------6.8.02: |
|
263 val t = (term_of o the o (parse thy)) "-1"; |
|
264 atomty t; |
|
265 val t = (term_of o the o (parse thy)) "0"; |
|
266 atomty t; |
|
267 val t = (term_of o the o (parse thy)) "1"; |
|
268 atomty t; |
|
269 val t = (term_of o the o (parse thy)) "2"; |
|
270 atomty t; |
|
271 val t = (term_of o the o (parse thy)) "999999999"; |
|
272 atomty t; |
|
273 -------------------------------------------------------------------6.8.02: |
|
274 |
|
275 > val ct = (the o (parse thy)) "a+#3+#4"; |
|
276 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
|
277 val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]") |
|
278 |
|
279 > val ct = (the o (parse thy)) "#3+(#4+a)"; |
|
280 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
|
281 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]") |
|
282 |
|
283 > val ct = (the o (parse thy)) "a+(#3+#4)+#5"; |
|
284 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
|
285 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option |
|
286 |
|
287 > val ct = (the o (parse thy)) "#3*(#4*a)"; |
|
288 > get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct; |
|
289 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]") |
|
290 |
|
291 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5"; |
|
292 > get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct; |
|
293 val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option |
|
294 |
|
295 > val ct = (the o (parse thy)) "#-4//#-2"; |
|
296 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct; |
|
297 val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]") |
|
298 |
|
299 > val ct = (the o (parse thy)) "#6//#-8"; |
|
300 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct; |
|
301 val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]") |
|
302 |
|
303 *) |
|
304 |
|
305 |
|
306 (* |
|
307 > val ct = (the o (parse thy)) "a + 3*4"; |
|
308 > applicable "calculate" (Calc("op *", "mult_")) ct; |
|
309 val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option |
|
310 |
|
311 -------------------------- |
|
312 > val ct = (the o (parse thy)) "3 =!= 3"; |
|
313 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); |
|
314 val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm |
|
315 |
|
316 > val ct = (the o (parse thy)) "~ (3 =!= 3)"; |
|
317 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); |
|
318 val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm |
|
319 |
|
320 > val ct = (the o (parse thy)) "3 =!= 4"; |
|
321 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); |
|
322 val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm |
|
323 |
|
324 > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))"; |
|
325 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); |
|
326 "(4 + (4 * x + x ^ 2) =!= (+0)) = False" |
|
327 |
|
328 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))"; |
|
329 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); |
|
330 "(4 + (4 * x + x ^ 2) =!= (+0)) = False" |
|
331 |
|
332 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))"; |
|
333 > val rls = eval_rls; |
|
334 > val (ct,_) = the (rewrite_set_ thy false rls ct); |
|
335 val ct = "True" : cterm |
|
336 -------------------------- |
|
337 *) |
|
338 |
|
339 |
|
340 (*.get a thm applying an op_ to a term; |
|
341 apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*) |
|
342 (* val (thy, (op_, eval_fn), ct) = |
|
343 (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term); |
|
344 *) |
|
345 fun get_calculation1_ thy ((op_, eval_fn):cal) ct = |
|
346 case eval_fn op_ ct thy of |
|
347 NONE => NONE |
|
348 | SOME (thmid,t) => |
|
349 SOME (thmid, (make_thm o (cterm_of thy)) t); |
|
350 |
|
351 |
|
352 |
|
353 |
|
354 |
|
355 (*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*) |
|
356 fun inst_thm' subs (Thm (id, thm)) = |
|
357 Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*) |
|
358 (read_instantiate subs thm) handle _ => thm) |
|
359 | inst_thm' _ calc = calc; |
|
360 fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) = |
|
361 Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thmI thm)); |
|
362 if bdv mem (vars_str o #prop o rep_thm) thm |
|
363 then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm))); |
|
364 read_instantiate subs thm) |
|
365 else (writeln("@@@ inst_thm': not mem.. "^bdv); |
|
366 thm))) |
|
367 | inst_thm' _ calc = calc; |
|
368 |
|
369 fun instantiate_rls subs |
|
370 (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca, |
|
371 asm_thm=at,rules=rules,scr=scr}:rls) = |
|
372 (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca, |
|
373 asm_thm=at,scr=scr, |
|
374 rules = map (inst_thm' subs) rules}:rls);---------------------------*) |
|
375 |
|
376 |
|
377 |
|
378 (** rewriting: ordered, conditional **) |
|
379 |
|
380 fun mk_rule (prems,l,r) = |
|
381 Trueprop $ (list_implies (prems, mk_equality (l,r))); |
|
382 |
|
383 (* 'norms' a rule, e.g. |
|
384 (*1*) a = 1 ==> a*(b+c) = b+c |
|
385 => a = 1 ==> a*(b+c) = b+c no change |
|
386 (*2*) t = t => (t=t) = True !! |
|
387 (*3*) [| k < l; m + l = k + n |] ==> m < n |
|
388 => [| k<l; m+l=k+n |] ==> m < n = True !! *) |
|
389 (* val it = fn : term -> term *) |
|
390 fun norm rule = |
|
391 let |
|
392 val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule), |
|
393 (strip_trueprop o Logic.strip_imp_concl)rule) |
|
394 in if is_equality concl then |
|
395 let val (l,r) = dest_equals' concl |
|
396 in if l = r then |
|
397 (*2*) mk_rule(prems,concl,true_as_term) |
|
398 else (*1*) rule end |
|
399 else (*3*) mk_rule(prems,concl,true_as_term) |
|
400 end; |
|
401 |
|
402 |
|
403 |
|
404 |
|
405 |
|
406 |
|
407 |
|
408 |