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