1 (* calculate values for function constants
2 (c) Walther Neuper 000106
4 use"Scripts/calculate.sml";
8 (* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)
10 val aT = Type ("'a", []);
11 (* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)":
13 > val (TFree(ss2,TT2)) = T2;
14 val ss2 = "'a" : string
15 val TT2 = ["term"] : sort
17 > val (Type(ss2',TT2')) = T2';
18 val ss2' = "RealDef.real" : string
19 val TT2' = [] : typ list
21 val realType = TFree ("RealDef.real", HOLogic.termS);
22 is different internally, too;
24 (1) .. (3) are displayed equally !!!
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
36 (3) binary operators fixed to type real in RatArith.thy
37 (trick by Markus Wenzel)
43 (** calculate numerals **)
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
50 fun popt2str (SOME (str, term)) = "SOME "^term2str term
51 | popt2str NONE = "NONE";
53 (* scan a term for applying eval_fn ef
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
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)
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);
71 let val popt = ef op_ t thy
74 | NONE => get_pair thy op_ ef arg end
75 else get_pair thy op_ ef arg
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);
81 ef "Atools.ident" t thy (* not nested *)
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);
87 ((*writeln("1.. get_pair: binop = "^op_);*)
89 let val popt = ef op_ t thy
90 (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
94 let val popt = get_pair thy op_ ef t1
95 (*val _ = writeln("3.. get_pair: "^term2str t1^
96 " -> "^popt2str popt)*)
99 | NONE => get_pair thy op_ ef t2
102 else (*search subterms*)
103 let val popt = get_pair thy op_ ef t1
104 (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
107 | NONE => get_pair thy op_ ef t2
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);*)
116 | NONE => (case get_pair thy op_ ef t2 of
118 | NONE => get_pair thy op_ ef t3)
119 else (case get_pair thy op_ ef t1 of
121 | NONE => (case get_pair thy op_ ef t2 of
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^"
132 val popt = get_pair thy op_ ef t1
135 | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*)
136 get_pair thy op_ ef t2)
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
155 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
156 > Sign.string_of_term (sign_of thy) t';
157 > val it = "#3 + (#4 + a) = #7 + a" : string
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
171 > val eval_fn = the (assoc (!eval_list, "pow"));
172 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
173 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of 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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of 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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
205 > val it = "sqrt #12 = #2 * sqrt #3 " : string
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 > Sign.string_of_term (sign_of thy) t';
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 > Sign.string_of_term (sign_of thy) t';
217 (* val ((op_, eval_fn),ct)=(cc,pre);
218 (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
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);
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;*)
232 ((*writeln("@@@ get_calculation: NONE, op_="^op_);
233 writeln("@@@ get_calculation: ct= ");atomty ct;*)
234 SOME (thmid, (make_thm o (cterm_of thy)) t));
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]")
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
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 = "#";
247 val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
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
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]")
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";
265 val t = (term_of o the o (parse thy)) "0";
267 val t = (term_of o the o (parse thy)) "1";
269 val t = (term_of o the o (parse thy)) "2";
271 val t = (term_of o the o (parse thy)) "999999999";
273 -------------------------------------------------------------------6.8.02:
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]")
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]")
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
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]")
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
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)]")
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]")
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
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
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
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
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"
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"
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 --------------------------
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);
345 fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
346 case eval_fn op_ ct thy of
349 SOME (thmid, (make_thm o (cterm_of thy)) t);
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);
367 | inst_thm' _ calc = calc;
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,
374 rules = map (inst_thm' subs) rules}:rls);---------------------------*)
378 (** rewriting: ordered, conditional **)
380 fun mk_rule (prems,l,r) =
381 Trueprop $ (list_implies (prems, mk_equality (l,r)));
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 *)
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
397 (*2*) mk_rule(prems,concl,true_as_term)
399 else (*3*) mk_rule(prems,concl,true_as_term)