238 SOME (mk_thmid thmid op0 (term2str arg) "", |
238 SOME (mk_thmid thmid op0 (term2str arg) "", |
239 Trueprop $ (mk_equality (t, false_as_term)))) |
239 Trueprop $ (mk_equality (t, false_as_term)))) |
240 | eval_const _ _ _ _ = NONE; |
240 | eval_const _ _ _ _ = NONE; |
241 |
241 |
242 (*. evaluate binary, associative, commutative operators: *,+,^ .*) |
242 (*. evaluate binary, associative, commutative operators: *,+,^ .*) |
243 (*("PLUS" ,("op +" ,eval_binop "#add_")), |
243 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
244 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
244 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
245 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*) |
245 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*) |
246 |
246 |
247 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = |
247 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = |
248 ("xxxxxx",op_,t,thy); |
248 ("xxxxxx",op_,t,thy); |
276 thy = (*binary . (v.n1).n2*) |
276 thy = (*binary . (v.n1).n2*) |
277 if op0 = op0' then |
277 if op0 = op0' then |
278 case (numeral t1, numeral t2) of |
278 case (numeral t1, numeral t2) of |
279 (SOME n1, SOME n2) => |
279 (SOME n1, SOME n2) => |
280 let val (T1,T2,Trange) = dest_binop_typ t0 |
280 let val (T1,T2,Trange) = dest_binop_typ t0 |
281 val res = calc (if op0 = "op -" then "op +" else op0) n1 n2 |
281 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2 |
282 (*WN071229 "HOL.divide" never tried*) |
282 (*WN071229 "Rings.inverse_class.divide" never tried*) |
283 val rhs = var_op_float v op_ t0 T1 res |
283 val rhs = var_op_float v op_ t0 T1 res |
284 val prop = Trueprop $ (mk_equality (t, rhs)) |
284 val prop = Trueprop $ (mk_equality (t, rhs)) |
285 in SOME (mk_thmid_f thmid n1 n2, prop) end |
285 in SOME (mk_thmid_f thmid n1 n2, prop) end |
286 | _ => NONE |
286 | _ => NONE |
287 else NONE |
287 else NONE |
291 (Const (op0', t0') $ t2 $ v))) |
291 (Const (op0', t0') $ t2 $ v))) |
292 thy = (*binary . n1.(n2.v)*) |
292 thy = (*binary . n1.(n2.v)*) |
293 if op0 = op0' then |
293 if op0 = op0' then |
294 case (numeral t1, numeral t2) of |
294 case (numeral t1, numeral t2) of |
295 (SOME n1, SOME n2) => |
295 (SOME n1, SOME n2) => |
296 if op0 = "op -" then NONE else |
296 if op0 = "Groups.minus_class.minus" then NONE else |
297 let val (T1,T2,Trange) = dest_binop_typ t0 |
297 let val (T1,T2,Trange) = dest_binop_typ t0 |
298 val res = calc op0 n1 n2 |
298 val res = calc op0 n1 n2 |
299 val rhs = float_op_var v op_ t0 T1 res |
299 val rhs = float_op_var v op_ t0 T1 res |
300 val prop = Trueprop $ (mk_equality (t, rhs)) |
300 val prop = Trueprop $ (mk_equality (t, rhs)) |
301 in SOME (mk_thmid_f thmid n1 n2, prop) end |
301 in SOME (mk_thmid_f thmid n1 n2, prop) end |
312 val prop = Trueprop $ (mk_equality (t, rhs)); |
312 val prop = Trueprop $ (mk_equality (t, rhs)); |
313 in SOME (mk_thmid_f thmid n1 n2, prop) end |
313 in SOME (mk_thmid_f thmid n1 n2, prop) end |
314 | _ => NONE) |
314 | _ => NONE) |
315 | eval_binop _ _ _ _ = NONE; |
315 | eval_binop _ _ _ _ = NONE; |
316 (* |
316 (* |
317 > val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy; |
317 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy; |
318 > term2str t; |
318 > term2str t; |
319 val it = "-1 + 2 = 1" |
319 val it = "-1 + 2 = 1" |
320 > val t = str2term "-1 * (-1 * a)"; |
320 > val t = str2term "-1 * (-1 * a)"; |
321 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy; |
321 > val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy; |
322 > term2str t; |
322 > term2str t; |
447 |
447 |
448 |
448 |
449 (** evaluation on the metalevel **) |
449 (** evaluation on the metalevel **) |
450 |
450 |
451 (*. evaluate HOL.divide .*) |
451 (*. evaluate HOL.divide .*) |
452 (*("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e"))*) |
452 (*("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e"))*) |
453 fun eval_cancel (thmid:string) "HOL.divide" (t as |
453 fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as |
454 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
454 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = |
455 (case (int_of_str n1, int_of_str n2) of |
455 (case (int_of_str n1, int_of_str n2) of |
456 (SOME n1', SOME n2') => |
456 (SOME n1', SOME n2') => |
457 let |
457 let |
458 val sg = sign2 n1' n2'; |
458 val sg = sign2 n1' n2'; |
521 (*make a list of terms to a sum*) |
521 (*make a list of terms to a sum*) |
522 fun list2sum [] = error ("list2sum called with []") |
522 fun list2sum [] = error ("list2sum called with []") |
523 | list2sum [s] = s |
523 | list2sum [s] = s |
524 | list2sum (s::ss) = |
524 | list2sum (s::ss) = |
525 let fun sum su [s'] = |
525 let fun sum su [s'] = |
526 Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
526 Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
527 $ su $ s' |
527 $ su $ s' |
528 | sum su (s'::ss') = |
528 | sum su (s'::ss') = |
529 sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
529 sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT) |
530 $ su $ s') ss' |
530 $ su $ s') ss' |
531 in sum s ss end; |
531 in sum s ss end; |
532 |
532 |
533 (*make a list of equalities to the sum of the lhs*) |
533 (*make a list of equalities to the sum of the lhs*) |
534 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*) |
534 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*) |
559 |
559 |
560 |
560 |
561 val list_rls = |
561 val list_rls = |
562 append_rls "list_rls" list_rls |
562 append_rls "list_rls" list_rls |
563 [Calc ("op *",eval_binop "#mult_"), |
563 [Calc ("op *",eval_binop "#mult_"), |
564 Calc ("op +", eval_binop "#add_"), |
564 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
565 Calc ("op <",eval_equ "#less_"), |
565 Calc ("op <",eval_equ "#less_"), |
566 Calc ("op <=",eval_equ "#less_equal_"), |
566 Calc ("op <=",eval_equ "#less_equal_"), |
567 Calc ("Atools.ident",eval_ident "#ident_"), |
567 Calc ("Atools.ident",eval_ident "#ident_"), |
568 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*) |
568 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*) |
569 |
569 |
589 [Calc ("op <",eval_equ "#less_"), |
589 [Calc ("op <",eval_equ "#less_"), |
590 Calc ("op <=",eval_equ "#less_equal_"), |
590 Calc ("op <=",eval_equ "#less_equal_"), |
591 Calc ("op =",eval_equal "#equal_"), |
591 Calc ("op =",eval_equal "#equal_"), |
592 |
592 |
593 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
593 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
594 Calc ("op +",eval_binop "#add_"), |
594 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
595 Calc ("op -",eval_binop "#sub_"), |
595 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
596 Calc ("op *",eval_binop "#mult_") |
596 Calc ("op *",eval_binop "#mult_") |
597 ]; |
597 ]; |
598 |
598 |
599 val Atools_erls = |
599 val Atools_erls = |
600 append_rls "Atools_erls" e_rls |
600 append_rls "Atools_erls" e_rls |
706 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")), |
706 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")), |
707 ("le" ,("op <" ,eval_equ "#less_")), |
707 ("le" ,("op <" ,eval_equ "#less_")), |
708 ("leq" ,("op <=" ,eval_equ "#less_equal_")), |
708 ("leq" ,("op <=" ,eval_equ "#less_equal_")), |
709 ("ident" ,("Atools.ident",eval_ident "#ident_")), |
709 ("ident" ,("Atools.ident",eval_ident "#ident_")), |
710 ("equal" ,("op =",eval_equal "#equal_")), |
710 ("equal" ,("op =",eval_equal "#equal_")), |
711 ("PLUS" ,("op +" ,eval_binop "#add_")), |
711 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
712 ("MINUS" ,("op -",eval_binop "#sub_")), |
712 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")), |
713 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
713 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
714 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")), |
714 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), |
715 ("POWER" ,("Atools.pow" ,eval_binop "#power_")), |
715 ("POWER" ,("Atools.pow" ,eval_binop "#power_")), |
716 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum "")) |
716 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum "")) |
717 ]); |
717 ]); |
718 |
718 |
719 val list_rls = prep_rls( |
719 val list_rls = prep_rls( |
722 rew_ord = ("termlessI", termlessI), |
722 rew_ord = ("termlessI", termlessI), |
723 erls = Rls {id="list_elrs", preconds = [], |
723 erls = Rls {id="list_elrs", preconds = [], |
724 rew_ord = ("termlessI",termlessI), |
724 rew_ord = ("termlessI",termlessI), |
725 erls = e_rls, |
725 erls = e_rls, |
726 srls = Erls, calc = [], (*asm_thm = [],*) |
726 srls = Erls, calc = [], (*asm_thm = [],*) |
727 rules = [Calc ("op +", eval_binop "#add_"), |
727 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
728 Calc ("op <",eval_equ "#less_") |
728 Calc ("op <",eval_equ "#less_") |
729 (* ~~~~~~ for nth_Cons_*) |
729 (* ~~~~~~ for nth_Cons_*) |
730 ], |
730 ], |
731 scr = EmptyScr}, |
731 scr = EmptyScr}, |
732 srls = Erls, calc = [], (*asm_thm = [], *) |
732 srls = Erls, calc = [], (*asm_thm = [], *) |