# HG changeset patch # User Walther Neuper # Date 1285661426 -7200 # Node ID 928cebc9c4aaa8c99751e04543da56f586b4f425 # Parent 491b133d154a67015992af8ecce20fa68dfcb0c8 updated "op *" --> Groups.times_class.times in src and test find . -type f -exec sed -i s/"\"op \*\""/"\"Groups.times_class.times\""/g {} \; diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Interpret/solve.sml Tue Sep 28 10:10:26 2010 +0200 @@ -91,7 +91,7 @@ (*13.9.02-------------- type ctr = (loc * pos) list; -val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"), +val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"), ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; ML {* @{term "PLUS"}; (*Free ("PLUS", "'a") : term*) diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Atools.thy --- a/src/Tools/isac/Knowledge/Atools.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Sep 28 10:10:26 2010 +0200 @@ -241,7 +241,7 @@ (*. evaluate binary, associative, commutative operators: *,+,^ .*) (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*) (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) = @@ -318,7 +318,7 @@ > term2str t; val it = "-1 + 2 = 1" > val t = str2term "-1 * (-1 * a)"; -> val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy; +> val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy; > term2str t; val it = "-1 * (-1 * a) = 1 * a"*) @@ -560,7 +560,7 @@ val list_rls = append_rls "list_rls" list_rls - [Calc ("op *",eval_binop "#mult_"), + [Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("op <",eval_equ "#less_"), Calc ("op <=",eval_equ "#less_equal_"), @@ -593,7 +593,7 @@ Thm ("real_unari_minus",num_str @{thm real_unari_minus}), Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_") + Calc ("Groups.times_class.times",eval_binop "#mult_") ]; val Atools_erls = @@ -710,7 +710,7 @@ ("equal" ,("op =",eval_equal "#equal_")), ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_")), ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum "")) diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Delete.thy --- a/src/Tools/isac/Knowledge/Delete.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Delete.thy Tue Sep 28 10:10:26 2010 +0200 @@ -25,7 +25,7 @@ else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*) | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) ((a - c,0),(0,0)) - | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*) + | calc "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*) ((a * c, b + d), (0, 0)) | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) ((a div c, 0), (0, 0)) diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Sep 28 10:10:26 2010 +0200 @@ -135,7 +135,7 @@ Thm ("sqrt_conv", num_str @{thm sqrt_conv}), Thm ("root_conv", num_str @{thm root_conv}), Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Thm ("rat_mult",num_str @{thm rat_mult}), (*a / b * (c / d) = a * c / (b * d)*) Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), @@ -167,7 +167,7 @@ (*?x * (?y / ?z) = ?x * ?y / ?z*) Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), (*?y / ?z * ?x = ?y * ?x / ?z*) - Calc ("op *", eval_binop "#mult_") + Calc ("Groups.times_class.times", eval_binop "#mult_") ], scr = EmptyScr}; diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/LinEq.thy --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 28 10:10:26 2010 +0200 @@ -86,7 +86,7 @@ Thm ("real_assoc_1",num_str @{thm real_assoc_1}), Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), (* Dont use Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:10:26 2010 +0200 @@ -213,12 +213,12 @@ if (1) then degree 0 if (2) then v is a factor on the very right, ev. with exponent.*) fun factor_right_deg (*case 2*) - (t as Const ("op *",_) $ t1 $ + (t as Const ("Groups.times_class.times",_) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d,_))) v = if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v = if (vv = v) then SOME (int_of_str' d) else NONE - | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v = + | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v = if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE | factor_right_deg vv v = if (vv = v) then SOME 1 else NONE; @@ -401,7 +401,7 @@ Thm ("real_unari_minus",num_str @{thm real_unari_minus}), Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Atools.pow" ,eval_binop "#power_") ]; @@ -411,7 +411,7 @@ Thm ("real_unari_minus",num_str @{thm real_unari_minus}), Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Atools.pow" ,eval_binop "#power_") ]; @@ -555,13 +555,13 @@ fun is_polyexp (Free _) = true | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true - | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true + | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = ((is_polyexp t1) andalso (is_polyexp t2)) | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = ((is_polyexp t1) andalso (is_polyexp t2)) - | is_polyexp (Const ("op *",_) $ t1 $ t2) = + | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = ((is_polyexp t1) andalso (is_polyexp t2)) | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = ((is_polyexp t1) andalso (is_polyexp t2)) @@ -659,12 +659,12 @@ rew_ord = ("dummy_ord", dummy_ord), erls = Atools_erls(*erls3.4.03*),srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], (*asm_thm = [],*) rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = EmptyScr}:rls; @@ -752,7 +752,7 @@ rew_ord = ("dummy_ord", dummy_ord), erls = Atools_erls(*erls3.4.03*),srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], (*asm_thm = [],*) @@ -880,7 +880,7 @@ rew_ord = ("dummy_ord", dummy_ord), erls = Atools_erls(*erls3.4.03*),srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], (*asm_thm = [],*) @@ -894,7 +894,7 @@ Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = EmptyScr}:rls; val reduce_012 = @@ -1025,7 +1025,7 @@ Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), erls = Atools_erls, srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], rules = [Thm ("real_plus_binom_pow2", @@ -1080,7 +1080,7 @@ Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_"), (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*) @@ -1115,7 +1115,7 @@ (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = Script ((term_of o the o (parse thy)) scr_expand_binoms) @@ -1132,7 +1132,7 @@ | poly2list t = [t]; (* Monom --> Liste von Variablen *) -fun monom2list (Const ("op *",_) $ t1 $ t2) = +fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) = (monom2list t1) @ (monom2list t2) | monom2list t = [t]; @@ -1278,7 +1278,7 @@ (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt (mit gewuenschtem Typen T) *) fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T); -fun mult T = Const ("op *", [T,T] ---> T); +fun mult T = Const ("Groups.times_class.times", [T,T] ---> T); fun binop op_ t1 t2 = op_ $ t1 $ t2; fun create_prod T (a,b) = binop (mult T) a b; fun create_sum T (a,b) = binop (plus T) a b; @@ -1353,7 +1353,7 @@ [Calc ("Poly.is'_multUnordered", eval_is_multUnordered "")], calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")), - ("TIMES" , ("op *" , eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")), ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")), ("POWER" , ("Atools.pow", eval_binop "#power_"))], scr=Rfuns {init_state = init_state, @@ -1406,7 +1406,7 @@ (*WN.18.6.03 definiert in thy, evaluiert prepat*)], calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], (*asm_thm=[],*) @@ -1433,7 +1433,7 @@ erls = Atools_erls, srls = Erls,calc = [], rules = [Rls_ discard_minus, Rls_ expand_poly_, - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Rls_ order_mult_rls_, Rls_ simplify_power_, Rls_ calc_add_mult_pow_, @@ -1451,7 +1451,7 @@ erls = Atools_erls, srls = Erls, calc = [], rules = [Rls_ discard_minus, Rls_ expand_poly_, - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Rls_ order_mult_rls_, Rls_ simplify_power_, Rls_ calc_add_mult_pow_, @@ -1473,7 +1473,7 @@ erls = Atools_erls, srls = Erls, calc = [], rules = [Rls_ discard_minus, Rls_ expand_poly_rat_,(*ignors rationals*) - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Rls_ order_mult_rls_, Rls_ simplify_power_, Rls_ calc_add_mult_pow_, @@ -1492,7 +1492,7 @@ Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI), erls = Atools_erls, srls = Erls, calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_"))*) ], rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}), @@ -1515,7 +1515,7 @@ (*Rls_ order_add_rls_,*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_"), Thm ("sym_realpow_twoI", @@ -1541,7 +1541,7 @@ (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_"), Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*) diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 28 10:10:26 2010 +0200 @@ -460,7 +460,7 @@ Thm ("realpow_multI",num_str @{thm realpow_multI}), Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), Calc ("Atools.pow" ,eval_binop "#power_"), diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/PolyMinus.thy --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:10:26 2010 +0200 @@ -116,17 +116,17 @@ let val s::ss = explode str in implode ((chr (ord s + 1))::ss) end; fun identifier (Free (id,_)) = id (* 2, a *) - | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = id (* 2*a, a*b *) - | identifier (Const ("op *", _) $ (* 3*a*b *) - (Const ("op *", _) $ + | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *) + (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) $ Free (id, _)) = if is_numeral num then id else "|||||||||||||" | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = if is_numeral base then "|||||||||||||" (* a^2 *) else (*increase*) base - | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _))) = if is_numeral num andalso not (is_numeral base) then (*increase*) base @@ -155,20 +155,20 @@ | eval_kleiner _ _ _ _ = NONE; fun ist_monom (Free (id,_)) = true - | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = if is_numeral num then true else false | ist_monom _ = false; (*. this function only accepts the most simple monoms vvvvvvvvvv .*) fun ist_monom (Free (id,_)) = true (* 2, a *) - | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) + | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *) if is_numeral id then false else true - | ist_monom (Const ("op *", _) $ (* 3*a*b *) - (Const ("op *", _) $ + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *) + (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) $ Free (id, _)) = if is_numeral num andalso not (is_numeral id) then true else false | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = true (* a^2 *) - | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *) + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *) (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _))) = if is_numeral num then true else false @@ -297,7 +297,7 @@ Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}), (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*) - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*) @@ -381,7 +381,7 @@ ]; val rechnen = append_rls "rechnen" e_rls - [Calc ("op *", eval_binop "#mult_"), + [Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("Groups.minus_class.minus", eval_binop "#subtr_") ]; diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Rational-WN.sml --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:10:26 2010 +0200 @@ -57,7 +57,7 @@ fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly else error ("term2poly.1 "^term2str t1) - | mono (t as Const ("op *",_) $ t1 $ + | mono (t as Const ("Groups.times_class.times",_) $ t1 $ (Const ("RatArith.pow",_) $ t2 $ t3)) v g = if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] else error ("term2poly.2 "^term2str t) @@ -71,7 +71,7 @@ fun term2poly (t as Free (s, _)) v = if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s] handle _ => NONE) - | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = + | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = if t = v then SOME [0, (the o int_of_str) s1] else NONE | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = SOME ([(the o int_of_str) s1] @ (poly t v 1)) @@ -125,11 +125,11 @@ case g of 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*) | 1 => if c = 1 then Free (v, vT) - else Const ("op *", [cT, vT]--->pT) $ + else Const ("Groups.times_class.times", [cT, vT]--->pT) $ Free (str_of_int c, cT) $ Free (v, vT) | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $ Free (v, vT) $ Free (str_of_int g, eT)) - else Const ("op *", [cT, vT]--->pT) $ + else Const ("Groups.times_class.times", [cT, vT]--->pT) $ Free (str_of_int c, cT) $ (Const ("RatArith.pow", [vT, eT]--->pT) $ Free (v, vT) $ Free (str_of_int g, eT)); diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 10:10:26 2010 +0200 @@ -1322,7 +1322,7 @@ checks the order of the operators .*) fun test_polynomial (Const ("uminus",_) $ Free (str,_)) _ = true (*WN.13.3.03*) | test_polynomial (t as Free(str,_)) v = true - | test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false + | test_polynomial (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false else (test_polynomial t1 "*") andalso (test_polynomial t2 "*") | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false else (test_polynomial t1 " ") andalso (test_polynomial t2 " ") @@ -1335,7 +1335,7 @@ (*. help function for is_expanded checks the order of the operators .*) fun test_exp (t as Free(str,_)) v = true - | test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false + | test_exp (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false else (test_exp t1 "*") andalso (test_exp t2 "*") | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false else (test_exp t1 " ") andalso (test_exp t2 " ") @@ -1379,7 +1379,7 @@ SOME [(1,rev(!vl))] handle _ => NONE ) end - | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option= + | term2coef' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option= let val t1pp= Unsynchronized.ref []; val t2pp= Unsynchronized.ref []; @@ -1492,7 +1492,7 @@ SOME [(1,rev(!vl))] handle _ => NONE ) end - | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option= + | term2poly' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option= let val t1pp= Unsynchronized.ref []; val t2pp= Unsynchronized.ref []; @@ -1603,13 +1603,13 @@ ( if hd(!xss)=1 then ( - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ Free(hd(!vv), HOLogic.realT) $ powerproduct2term(tl(!xss),tl(!vv)) ) else ( - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ Free(hd(!vv), HOLogic.realT) $ Free(str_of_int (hd(!xss)),HOLogic.realT) @@ -1637,7 +1637,7 @@ ) else ( - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ Free(str_of_int c,HOLogic.realT) $ powerproduct2term(e,v) ) @@ -1654,10 +1654,10 @@ Free ((str_of_int o abs) i, HOLogic.realT) else if i > 0 - then Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ + then Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ (Free (str_of_int i, HOLogic.realT)) $ powerproduct2term(is, v) - else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ + else Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ (Const ("uminus", HOLogic.realT --> HOLogic.realT) $ Free ((str_of_int o abs) i, HOLogic.realT)) $ powerproduct2term(is, vs);---------------------------*) @@ -1666,7 +1666,7 @@ then Free (str_of_int i, HOLogic.realT) else if i = 1 then powerproduct2term (is, vs) - else Const ("op *", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $ + else Const ("Groups.times_class.times", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $ (Free (str_of_int i, HOLogic.realT)) $ powerproduct2term (is, vs); @@ -1697,7 +1697,7 @@ ) else ( - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ Free(str_of_int (abs(c)),HOLogic.realT) $ powerproduct2term(e,v) ) @@ -1769,13 +1769,13 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(!p1',vars) $ poly2term(!p3,vars) ) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(!p2',vars) $ poly2term(!p3,vars) ) @@ -1789,13 +1789,13 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(!p1',vars) $ poly2term(!p3,vars) ) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(!p2',vars) $ poly2term(!p3,vars) ) @@ -1834,13 +1834,13 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(!p1',vars) $ poly2expanded(!p3,vars) ) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(!p2',vars) $ poly2expanded(!p3,vars) ) @@ -1854,13 +1854,13 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(!p1',vars) $ poly2expanded(!p3,vars) ) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(!p2',vars) $ poly2expanded(!p3,vars) ) @@ -2283,7 +2283,7 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(the (term2poly p1' p1var),p1var) $ poly2term(p3,var) ) @@ -2315,7 +2315,7 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(the (term2poly p1' p1var),p1var) $ poly2term(p3,var) ) @@ -2359,7 +2359,7 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(the(expanded2poly p1' p1var),p1var) $ poly2expanded(p3,var) ) @@ -2391,7 +2391,7 @@ Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(the(expanded2poly p1' p1var),p1var) $ poly2expanded(p3,var) ) @@ -2559,7 +2559,7 @@ | make_term ((x::xs),vars) = if length(xs)=0 then poly2term(sort (mv_geq LEX_) (x),vars) else ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2term(sort (mv_geq LEX_) (x),vars) $ make_term(xs,vars) ); @@ -2584,7 +2584,7 @@ | make_exp ((x::xs),vars) = if length(xs)=0 then poly2expanded(sort (mv_geq LEX_) (x),vars) else ( - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ poly2expanded(sort (mv_geq LEX_) (x),vars) $ make_exp(xs,vars) ); @@ -2682,7 +2682,7 @@ [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ t $ Free("1",HOLogic.realT) ] - | term2list (t as (Const("op *",_) $ _ $ _)) = + | term2list (t as (Const("Groups.times_class.times",_) $ _ $ _)) = [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ t $ Free("1",HOLogic.realT) ] @@ -3002,7 +3002,7 @@ ord_make_polynomial false thy), erls = rational_erls, calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], (*asm_thm=[("real_mult_div_cancel2","")],*) @@ -3084,7 +3084,7 @@ ord_make_polynomial false thy), erls = rational_erls, calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], scr=Rfuns {init_state = init_state thy Atools_erls ro, @@ -3236,7 +3236,7 @@ ord_make_polynomial false thy), erls = rational_erls, calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], scr=Rfuns {init_state = init_state thy Atools_erls ro, @@ -3384,7 +3384,7 @@ ord_make_polynomial false thy), erls = rational_erls, calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], (*asm_thm=[("real_mult_div_cancel2","")],*) @@ -3404,14 +3404,14 @@ fun is_ratpolyexp (Free _) = true | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true - | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true + | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = ((is_ratpolyexp t1) andalso (is_ratpolyexp t2)) | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = ((is_ratpolyexp t1) andalso (is_ratpolyexp t2)) - | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) = + | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = ((is_ratpolyexp t1) andalso (is_ratpolyexp t2)) | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) = ((is_ratpolyexp t1) andalso (is_ratpolyexp t2)) diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Sep 28 10:10:26 2010 +0200 @@ -172,7 +172,7 @@ Calc ("Atools.pow" ,eval_binop "#power_"), Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("Groups.minus_class.minus", eval_binop "#sub_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("op =",eval_equal "#equal_") ]; @@ -184,7 +184,7 @@ Calc ("Atools.pow" ,eval_binop "#power_"), Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("Groups.minus_class.minus", eval_binop "#sub_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("op =",eval_equal "#equal_") ]; @@ -252,7 +252,7 @@ (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = Script ((term_of o the o (parse thy)) "empty_script") @@ -298,7 +298,7 @@ Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("Groups.minus_class.minus", eval_binop "#sub_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), Calc ("Atools.pow", eval_binop "#power_"), @@ -323,7 +323,7 @@ Calc ("Groups.plus_class.plus", eval_binop "#add_"), Calc ("Groups.minus_class.minus", eval_binop "#sub_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), Calc ("Atools.pow", eval_binop "#power_") diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 28 10:10:26 2010 +0200 @@ -157,7 +157,7 @@ fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:") (* at the moment there is no term like this, but ....*) | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v - | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v + | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse (is_sqrtTerm_in t2 v) @@ -447,7 +447,7 @@ (* a*(b*c) = a*b*c *) Calc ("Groups.plus_class.plus",eval_binop "#add_"), Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), Calc ("Atools.pow" ,eval_binop "#power_"), diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 10:10:26 2010 +0200 @@ -228,7 +228,7 @@ Calc ("Tools.matches",eval_matches ""), Calc ("Groups.plus_class.plus",eval_binop "#add_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Atools.pow" ,eval_binop "#power_"), Calc ("op <",eval_equ "#less_"), @@ -273,7 +273,7 @@ eval_contains_root"#contains_root_"), Calc ("Groups.plus_class.plus",eval_binop "#add_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), Calc ("Atools.pow" ,eval_binop "#power_"), @@ -407,7 +407,7 @@ (* these 2 rules are invers to distr_div_right wrt. termination. thus they MUST be done IMMEDIATELY before calc *) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), Calc ("Atools.pow", eval_binop "#power_"), @@ -485,7 +485,7 @@ ("lhs" ,("Tools.lhs" ,eval_lhs "")), (*aus Atools.ML*) ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), ("POWER" ,("Atools.pow" ,eval_binop "#power_")), ("is_const",("Atools.is'_const",eval_const "#is_const_")), @@ -1296,7 +1296,7 @@ rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")), erls = testerls, srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], (*asm_thm = [],*) @@ -1353,7 +1353,7 @@ (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = EmptyScr(*Script ((term_of o the o (parse thy)) @@ -1402,7 +1402,7 @@ rew_ord = ("termlessI",termlessI), erls = testerls, srls = Erls, calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), - ("TIMES" , ("op *", eval_binop "#mult_")), + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], rules = @@ -1453,7 +1453,7 @@ (*"0 + z = z"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_"), (* Thm ("real_mult_commute",num_str @{thm real_mult_commute}), @@ -1486,7 +1486,7 @@ (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) Calc ("Groups.plus_class.plus", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), + Calc ("Groups.times_class.times", eval_binop "#mult_"), Calc ("Atools.pow", eval_binop "#power_") ], scr = EmptyScr diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/ProgLang/calculate.sml --- a/src/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:10:26 2010 +0200 @@ -173,8 +173,8 @@ > Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; -> val eval_fn = the (assoc (!eval_list, "op *")); -> val (SOME (id,t')) = get_pair thy "op *" eval_fn t; +> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times")); +> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t; > Syntax.string_of_term (thy2ctxt thy) t'; > > val t = (term_of o the o (parse thy)) "#0 < #4"; @@ -283,7 +283,7 @@ val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option > val ct = (the o (parse thy)) "#3*(#4*a)"; -> get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct; +> get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct; val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]") > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5"; @@ -303,7 +303,7 @@ (* > val ct = (the o (parse thy)) "a + 3*4"; -> applicable "calculate" (Calc("op *", "mult_")) ct; +> applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct; val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option -------------------------- diff -r 491b133d154a -r 928cebc9c4aa src/Tools/isac/ProgLang/termC.sml --- a/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 10:10:26 2010 +0200 @@ -565,7 +565,7 @@ | num_of_term t = error ("num_of_term not for "^term2str t); fun mk_factroot op_(*=thy.sqrt*) T fact root = - Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $ + Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $ (Const (op_, T --> T) $ term_of_num T root); (* val T = (type_of o term_of o the) (parse thy "#12::real"); @@ -608,7 +608,7 @@ (*used for calculating built in binary operations in Isabelle2002->Float.ML*) (*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2 - | calc "op *" (n1, n2) = n1*n2 + | calc "Groups.times_class.times" (n1, n2) = n1*n2 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2 | calc "Atools.pow"(n1, n2) = power n1 n2 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*) @@ -1159,10 +1159,10 @@ use length (vars term) = 1 instead*) fun is_atom (Const ("Float.Float",_) $ _) = true | is_atom (Const ("ComplexI.I'_'_",_)) = true - | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t + | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ - (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = + (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = is_atom t1 andalso is_atom t2 | is_atom (Const _) = true | is_atom (Free _) = true @@ -1182,7 +1182,7 @@ > is_atom t; val it = true : bool > val t = str2term "1 + 2*I__"; -> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t; +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t; *) (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's diff -r 491b133d154a -r 928cebc9c4aa test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 10:10:26 2010 +0200 @@ -70,7 +70,7 @@ Calc ("Tools.matches",eval_matches ""), Calc ("Groups.plus_class.plus",eval_binop "#add_"), - Calc ("op *",eval_binop "#mult_"), + Calc ("Groups.times_class.times",eval_binop "#mult_"), Calc ("Atools.pow" ,eval_binop "#power_"), Calc ("op <",eval_equ "#less_"), diff -r 491b133d154a -r 928cebc9c4aa test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:10:26 2010 +0200 @@ -282,7 +282,7 @@ val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*) val (i,is) = (~1,[2]); - val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ + val ttt = Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ (Const ("uminus", HOLogic.realT --> HOLogic.realT) $ Free ((str_of_int o abs) i, HOLogic.realT)) $ powerproduct2term(is, vs); diff -r 491b133d154a -r 928cebc9c4aa test/Tools/isac/ProgLang/calculate.sml --- a/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:01:18 2010 +0200 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:10:26 2010 +0200 @@ -103,7 +103,7 @@ ], {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, calc=[("PLUS" ,("op +" ,eval_binop "#add_")), - ("TIMES" ,("op *" ,eval_binop "#mult_")), + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], crls=tval_rls, nrls=e_rls(*,