equal
deleted
inserted
replaced
257 let val (T1,T2,Trange) = dest_binop_typ t0 |
257 let val (T1,T2,Trange) = dest_binop_typ t0 |
258 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2 |
258 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2 |
259 (*WN071229 "Fields.inverse_class.divide" never tried*) |
259 (*WN071229 "Fields.inverse_class.divide" never tried*) |
260 val rhs = var_op_float v op_ t0 T1 res |
260 val rhs = var_op_float v op_ t0 T1 res |
261 val prop = Trueprop $ (mk_equality (t, rhs)) |
261 val prop = Trueprop $ (mk_equality (t, rhs)) |
262 in SOME (mk_thmid_f thmid n1 n2, prop) end |
262 in SOME ("#: " ^ term2str prop, prop) end |
263 | _ => NONE |
263 | _ => NONE |
264 else NONE |
264 else NONE |
265 | eval_binop (thmid:string) (op_:string) |
265 | eval_binop (thmid:string) (op_:string) |
266 (t as |
266 (t as |
267 (Const (op0, t0) $ t1 $ |
267 (Const (op0, t0) $ t1 $ |
273 if op0 = "Groups.minus_class.minus" then NONE else |
273 if op0 = "Groups.minus_class.minus" then NONE else |
274 let val (T1,T2,Trange) = dest_binop_typ t0 |
274 let val (T1,T2,Trange) = dest_binop_typ t0 |
275 val res = calc op0 n1 n2 |
275 val res = calc op0 n1 n2 |
276 val rhs = float_op_var v op_ t0 T1 res |
276 val rhs = float_op_var v op_ t0 T1 res |
277 val prop = Trueprop $ (mk_equality (t, rhs)) |
277 val prop = Trueprop $ (mk_equality (t, rhs)) |
278 in SOME (mk_thmid_f thmid n1 n2, prop) end |
278 in SOME ("#: " ^ term2str prop, prop) end |
279 | _ => NONE |
279 | _ => NONE |
280 else NONE |
280 else NONE |
281 |
281 |
282 | eval_binop (thmid:string) (op_:string) |
282 | eval_binop (thmid:string) (op_:string) |
283 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*) |
283 (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*) |
285 (SOME n1, SOME n2) => |
285 (SOME n1, SOME n2) => |
286 let val (T1,T2,Trange) = dest_binop_typ t0; |
286 let val (T1,T2,Trange) = dest_binop_typ t0; |
287 val res = calc op0 n1 n2; |
287 val res = calc op0 n1 n2; |
288 val rhs = term_of_float Trange res; |
288 val rhs = term_of_float Trange res; |
289 val prop = Trueprop $ (mk_equality (t, rhs)); |
289 val prop = Trueprop $ (mk_equality (t, rhs)); |
290 in SOME (mk_thmid_f thmid n1 n2, prop) end |
290 in SOME ("#: " ^ term2str prop, prop) end |
291 | _ => NONE) |
291 | _ => NONE) |
292 | eval_binop _ _ _ _ = NONE; |
292 | eval_binop _ _ _ _ = NONE; |
293 (* |
293 (* |
294 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy; |
294 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy; |
295 > term2str t; |
295 > term2str t; |