1.1 --- a/src/Tools/isac/Interpret/solve.sml Tue Sep 28 10:01:18 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Tue Sep 28 10:10:26 2010 +0200
1.3 @@ -91,7 +91,7 @@
1.4
1.5 (*13.9.02--------------
1.6 type ctr = (loc * pos) list;
1.7 -val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"),
1.8 +val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"),
1.9 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
1.10 ML {*
1.11 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*)
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Sep 28 10:01:18 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Sep 28 10:10:26 2010 +0200
2.3 @@ -241,7 +241,7 @@
2.4
2.5 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
2.6 (*("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
2.7 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
2.8 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
2.9 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))*)
2.10
2.11 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
2.12 @@ -318,7 +318,7 @@
2.13 > term2str t;
2.14 val it = "-1 + 2 = 1"
2.15 > val t = str2term "-1 * (-1 * a)";
2.16 -> val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
2.17 +> val SOME (thmid, t) = eval_binop "#mult_" "Groups.times_class.times" t thy;
2.18 > term2str t;
2.19 val it = "-1 * (-1 * a) = 1 * a"*)
2.20
2.21 @@ -560,7 +560,7 @@
2.22
2.23 val list_rls =
2.24 append_rls "list_rls" list_rls
2.25 - [Calc ("op *",eval_binop "#mult_"),
2.26 + [Calc ("Groups.times_class.times",eval_binop "#mult_"),
2.27 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
2.28 Calc ("op <",eval_equ "#less_"),
2.29 Calc ("op <=",eval_equ "#less_equal_"),
2.30 @@ -593,7 +593,7 @@
2.31 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
2.32 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
2.33 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
2.34 - Calc ("op *",eval_binop "#mult_")
2.35 + Calc ("Groups.times_class.times",eval_binop "#mult_")
2.36 ];
2.37
2.38 val Atools_erls =
2.39 @@ -710,7 +710,7 @@
2.40 ("equal" ,("op =",eval_equal "#equal_")),
2.41 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
2.42 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
2.43 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
2.44 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
2.45 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
2.46 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
2.47 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
3.1 --- a/src/Tools/isac/Knowledge/Delete.thy Tue Sep 28 10:01:18 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Tue Sep 28 10:10:26 2010 +0200
3.3 @@ -25,7 +25,7 @@
3.4 else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
3.5 | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
3.6 ((a - c,0),(0,0))
3.7 - | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
3.8 + | calc "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
3.9 ((a * c, b + d), (0, 0))
3.10 | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
3.11 ((a div c, 0), (0, 0))
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Sep 28 10:01:18 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Sep 28 10:10:26 2010 +0200
4.3 @@ -135,7 +135,7 @@
4.4 Thm ("sqrt_conv", num_str @{thm sqrt_conv}),
4.5 Thm ("root_conv", num_str @{thm root_conv}),
4.6 Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}),
4.7 - Calc ("op *", eval_binop "#mult_"),
4.8 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
4.9 Thm ("rat_mult",num_str @{thm rat_mult}),
4.10 (*a / b * (c / d) = a * c / (b * d)*)
4.11 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
4.12 @@ -167,7 +167,7 @@
4.13 (*?x * (?y / ?z) = ?x * ?y / ?z*)
4.14 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
4.15 (*?y / ?z * ?x = ?y * ?x / ?z*)
4.16 - Calc ("op *", eval_binop "#mult_")
4.17 + Calc ("Groups.times_class.times", eval_binop "#mult_")
4.18 ],
4.19 scr = EmptyScr};
4.20
5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 28 10:01:18 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 28 10:10:26 2010 +0200
5.3 @@ -86,7 +86,7 @@
5.4 Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
5.5 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
5.6 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.7 - Calc ("op *",eval_binop "#mult_"),
5.8 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.9 (* Dont use
5.10 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
5.11 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:01:18 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:10:26 2010 +0200
6.3 @@ -213,12 +213,12 @@
6.4 if (1) then degree 0
6.5 if (2) then v is a factor on the very right, ev. with exponent.*)
6.6 fun factor_right_deg (*case 2*)
6.7 - (t as Const ("op *",_) $ t1 $
6.8 + (t as Const ("Groups.times_class.times",_) $ t1 $
6.9 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
6.10 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
6.11 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
6.12 if (vv = v) then SOME (int_of_str' d) else NONE
6.13 - | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
6.14 + | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
6.15 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
6.16 | factor_right_deg vv v =
6.17 if (vv = v) then SOME 1 else NONE;
6.18 @@ -401,7 +401,7 @@
6.19 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
6.20 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
6.21 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
6.22 - Calc ("op *",eval_binop "#mult_"),
6.23 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
6.24 Calc ("Atools.pow" ,eval_binop "#power_")
6.25 ];
6.26
6.27 @@ -411,7 +411,7 @@
6.28 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
6.29 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
6.30 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
6.31 - Calc ("op *",eval_binop "#mult_"),
6.32 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
6.33 Calc ("Atools.pow" ,eval_binop "#power_")
6.34 ];
6.35
6.36 @@ -555,13 +555,13 @@
6.37 fun is_polyexp (Free _) = true
6.38 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
6.39 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
6.40 - | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
6.41 + | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
6.42 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
6.43 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
6.44 ((is_polyexp t1) andalso (is_polyexp t2))
6.45 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
6.46 ((is_polyexp t1) andalso (is_polyexp t2))
6.47 - | is_polyexp (Const ("op *",_) $ t1 $ t2) =
6.48 + | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
6.49 ((is_polyexp t1) andalso (is_polyexp t2))
6.50 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
6.51 ((is_polyexp t1) andalso (is_polyexp t2))
6.52 @@ -659,12 +659,12 @@
6.53 rew_ord = ("dummy_ord", dummy_ord),
6.54 erls = Atools_erls(*erls3.4.03*),srls = Erls,
6.55 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.56 - ("TIMES" , ("op *", eval_binop "#mult_")),
6.57 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.58 ("POWER", ("Atools.pow", eval_binop "#power_"))
6.59 ],
6.60 (*asm_thm = [],*)
6.61 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.62 - Calc ("op *", eval_binop "#mult_"),
6.63 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.64 Calc ("Atools.pow", eval_binop "#power_")
6.65 ], scr = EmptyScr}:rls;
6.66
6.67 @@ -752,7 +752,7 @@
6.68 rew_ord = ("dummy_ord", dummy_ord),
6.69 erls = Atools_erls(*erls3.4.03*),srls = Erls,
6.70 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.71 - ("TIMES" , ("op *", eval_binop "#mult_")),
6.72 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.73 ("POWER", ("Atools.pow", eval_binop "#power_"))
6.74 ],
6.75 (*asm_thm = [],*)
6.76 @@ -880,7 +880,7 @@
6.77 rew_ord = ("dummy_ord", dummy_ord),
6.78 erls = Atools_erls(*erls3.4.03*),srls = Erls,
6.79 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.80 - ("TIMES" , ("op *", eval_binop "#mult_")),
6.81 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.82 ("POWER", ("Atools.pow", eval_binop "#power_"))
6.83 ],
6.84 (*asm_thm = [],*)
6.85 @@ -894,7 +894,7 @@
6.86 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
6.87 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
6.88 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.89 - Calc ("op *", eval_binop "#mult_"),
6.90 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.91 Calc ("Atools.pow", eval_binop "#power_")
6.92 ], scr = EmptyScr}:rls;
6.93 val reduce_012 =
6.94 @@ -1025,7 +1025,7 @@
6.95 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
6.96 erls = Atools_erls, srls = Erls,
6.97 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.98 - ("TIMES" , ("op *", eval_binop "#mult_")),
6.99 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.100 ("POWER", ("Atools.pow", eval_binop "#power_"))
6.101 ],
6.102 rules = [Thm ("real_plus_binom_pow2",
6.103 @@ -1080,7 +1080,7 @@
6.104 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
6.105
6.106 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.107 - Calc ("op *", eval_binop "#mult_"),
6.108 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.109 Calc ("Atools.pow", eval_binop "#power_"),
6.110 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
6.111 (*AC-rewriting*)
6.112 @@ -1115,7 +1115,7 @@
6.113 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
6.114
6.115 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.116 - Calc ("op *", eval_binop "#mult_"),
6.117 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.118 Calc ("Atools.pow", eval_binop "#power_")
6.119 ],
6.120 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
6.121 @@ -1132,7 +1132,7 @@
6.122 | poly2list t = [t];
6.123
6.124 (* Monom --> Liste von Variablen *)
6.125 -fun monom2list (Const ("op *",_) $ t1 $ t2) =
6.126 +fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
6.127 (monom2list t1) @ (monom2list t2)
6.128 | monom2list t = [t];
6.129
6.130 @@ -1278,7 +1278,7 @@
6.131 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
6.132 (mit gewuenschtem Typen T) *)
6.133 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
6.134 -fun mult T = Const ("op *", [T,T] ---> T);
6.135 +fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
6.136 fun binop op_ t1 t2 = op_ $ t1 $ t2;
6.137 fun create_prod T (a,b) = binop (mult T) a b;
6.138 fun create_sum T (a,b) = binop (plus T) a b;
6.139 @@ -1353,7 +1353,7 @@
6.140 [Calc ("Poly.is'_multUnordered",
6.141 eval_is_multUnordered "")],
6.142 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")),
6.143 - ("TIMES" , ("op *" , eval_binop "#mult_")),
6.144 + ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")),
6.145 ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
6.146 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
6.147 scr=Rfuns {init_state = init_state,
6.148 @@ -1406,7 +1406,7 @@
6.149 (*WN.18.6.03 definiert in thy,
6.150 evaluiert prepat*)],
6.151 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
6.152 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
6.153 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
6.154 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
6.155 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
6.156 (*asm_thm=[],*)
6.157 @@ -1433,7 +1433,7 @@
6.158 erls = Atools_erls, srls = Erls,calc = [],
6.159 rules = [Rls_ discard_minus,
6.160 Rls_ expand_poly_,
6.161 - Calc ("op *", eval_binop "#mult_"),
6.162 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.163 Rls_ order_mult_rls_,
6.164 Rls_ simplify_power_,
6.165 Rls_ calc_add_mult_pow_,
6.166 @@ -1451,7 +1451,7 @@
6.167 erls = Atools_erls, srls = Erls, calc = [],
6.168 rules = [Rls_ discard_minus,
6.169 Rls_ expand_poly_,
6.170 - Calc ("op *", eval_binop "#mult_"),
6.171 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.172 Rls_ order_mult_rls_,
6.173 Rls_ simplify_power_,
6.174 Rls_ calc_add_mult_pow_,
6.175 @@ -1473,7 +1473,7 @@
6.176 erls = Atools_erls, srls = Erls, calc = [],
6.177 rules = [Rls_ discard_minus,
6.178 Rls_ expand_poly_rat_,(*ignors rationals*)
6.179 - Calc ("op *", eval_binop "#mult_"),
6.180 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.181 Rls_ order_mult_rls_,
6.182 Rls_ simplify_power_,
6.183 Rls_ calc_add_mult_pow_,
6.184 @@ -1492,7 +1492,7 @@
6.185 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
6.186 erls = Atools_erls, srls = Erls,
6.187 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.188 - ("TIMES" , ("op *", eval_binop "#mult_")),
6.189 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.190 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
6.191 ],
6.192 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
6.193 @@ -1515,7 +1515,7 @@
6.194 (*Rls_ order_add_rls_,*)
6.195
6.196 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.197 - Calc ("op *", eval_binop "#mult_"),
6.198 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.199 Calc ("Atools.pow", eval_binop "#power_"),
6.200
6.201 Thm ("sym_realpow_twoI",
6.202 @@ -1541,7 +1541,7 @@
6.203 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
6.204
6.205 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
6.206 - Calc ("op *", eval_binop "#mult_"),
6.207 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
6.208 Calc ("Atools.pow", eval_binop "#power_"),
6.209
6.210 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 28 10:01:18 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 28 10:10:26 2010 +0200
7.3 @@ -460,7 +460,7 @@
7.4 Thm ("realpow_multI",num_str @{thm realpow_multI}),
7.5 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.6 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
7.7 - Calc ("op *",eval_binop "#mult_"),
7.8 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
7.9 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
7.10 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
7.11 Calc ("Atools.pow" ,eval_binop "#power_"),
8.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:01:18 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:10:26 2010 +0200
8.3 @@ -116,17 +116,17 @@
8.4 let val s::ss = explode str
8.5 in implode ((chr (ord s + 1))::ss) end;
8.6 fun identifier (Free (id,_)) = id (* 2, a *)
8.7 - | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
8.8 + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
8.9 id (* 2*a, a*b *)
8.10 - | identifier (Const ("op *", _) $ (* 3*a*b *)
8.11 - (Const ("op *", _) $
8.12 + | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
8.13 + (Const ("Groups.times_class.times", _) $
8.14 Free (num, _) $ Free _) $ Free (id, _)) =
8.15 if is_numeral num then id
8.16 else "|||||||||||||"
8.17 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
8.18 if is_numeral base then "|||||||||||||" (* a^2 *)
8.19 else (*increase*) base
8.20 - | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
8.21 + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
8.22 (Const ("Atools.pow", _) $
8.23 Free (base, _) $ Free (exp, _))) =
8.24 if is_numeral num andalso not (is_numeral base) then (*increase*) base
8.25 @@ -155,20 +155,20 @@
8.26 | eval_kleiner _ _ _ _ = NONE;
8.27
8.28 fun ist_monom (Free (id,_)) = true
8.29 - | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
8.30 + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
8.31 if is_numeral num then true else false
8.32 | ist_monom _ = false;
8.33 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
8.34 fun ist_monom (Free (id,_)) = true (* 2, a *)
8.35 - | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
8.36 + | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
8.37 if is_numeral id then false else true
8.38 - | ist_monom (Const ("op *", _) $ (* 3*a*b *)
8.39 - (Const ("op *", _) $
8.40 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
8.41 + (Const ("Groups.times_class.times", _) $
8.42 Free (num, _) $ Free _) $ Free (id, _)) =
8.43 if is_numeral num andalso not (is_numeral id) then true else false
8.44 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
8.45 true (* a^2 *)
8.46 - | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
8.47 + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
8.48 (Const ("Atools.pow", _) $
8.49 Free (base, _) $ Free (exp, _))) =
8.50 if is_numeral num then true else false
8.51 @@ -297,7 +297,7 @@
8.52 Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}),
8.53 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
8.54
8.55 - Calc ("op *", eval_binop "#mult_"),
8.56 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
8.57
8.58 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
8.59 (*"0 * z = 0"*)
8.60 @@ -381,7 +381,7 @@
8.61 ];
8.62 val rechnen =
8.63 append_rls "rechnen" e_rls
8.64 - [Calc ("op *", eval_binop "#mult_"),
8.65 + [Calc ("Groups.times_class.times", eval_binop "#mult_"),
8.66 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.67 Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
8.68 ];
9.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:01:18 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:10:26 2010 +0200
9.3 @@ -57,7 +57,7 @@
9.4 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
9.5 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
9.6 else error ("term2poly.1 "^term2str t1)
9.7 - | mono (t as Const ("op *",_) $ t1 $
9.8 + | mono (t as Const ("Groups.times_class.times",_) $ t1 $
9.9 (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
9.10 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
9.11 else error ("term2poly.2 "^term2str t)
9.12 @@ -71,7 +71,7 @@
9.13 fun term2poly (t as Free (s, _)) v =
9.14 if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
9.15 handle _ => NONE)
9.16 - | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
9.17 + | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
9.18 if t = v then SOME [0, (the o int_of_str) s1] else NONE
9.19 | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
9.20 SOME ([(the o int_of_str) s1] @ (poly t v 1))
9.21 @@ -125,11 +125,11 @@
9.22 case g of
9.23 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
9.24 | 1 => if c = 1 then Free (v, vT)
9.25 - else Const ("op *", [cT, vT]--->pT) $
9.26 + else Const ("Groups.times_class.times", [cT, vT]--->pT) $
9.27 Free (str_of_int c, cT) $ Free (v, vT)
9.28 | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
9.29 Free (v, vT) $ Free (str_of_int g, eT))
9.30 - else Const ("op *", [cT, vT]--->pT) $
9.31 + else Const ("Groups.times_class.times", [cT, vT]--->pT) $
9.32 Free (str_of_int c, cT) $
9.33 (Const ("RatArith.pow", [vT, eT]--->pT) $
9.34 Free (v, vT) $ Free (str_of_int g, eT));
10.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 10:01:18 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 10:10:26 2010 +0200
10.3 @@ -1322,7 +1322,7 @@
10.4 checks the order of the operators .*)
10.5 fun test_polynomial (Const ("uminus",_) $ Free (str,_)) _ = true (*WN.13.3.03*)
10.6 | test_polynomial (t as Free(str,_)) v = true
10.7 - | test_polynomial (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
10.8 + | test_polynomial (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false
10.9 else (test_polynomial t1 "*") andalso (test_polynomial t2 "*")
10.10 | test_polynomial (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
10.11 else (test_polynomial t1 " ") andalso (test_polynomial t2 " ")
10.12 @@ -1335,7 +1335,7 @@
10.13 (*. help function for is_expanded
10.14 checks the order of the operators .*)
10.15 fun test_exp (t as Free(str,_)) v = true
10.16 - | test_exp (t as Const ("op *",_) $ t1 $ t2) v = if v="^" then false
10.17 + | test_exp (t as Const ("Groups.times_class.times",_) $ t1 $ t2) v = if v="^" then false
10.18 else (test_exp t1 "*") andalso (test_exp t2 "*")
10.19 | test_exp (t as Const ("Groups.plus_class.plus",_) $ t1 $ t2) v = if v="*" orelse v="^" then false
10.20 else (test_exp t1 " ") andalso (test_exp t2 " ")
10.21 @@ -1379,7 +1379,7 @@
10.22 SOME [(1,rev(!vl))] handle _ => NONE
10.23 )
10.24 end
10.25 - | term2coef' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
10.26 + | term2coef' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option=
10.27 let
10.28 val t1pp= Unsynchronized.ref [];
10.29 val t2pp= Unsynchronized.ref [];
10.30 @@ -1492,7 +1492,7 @@
10.31 SOME [(1,rev(!vl))] handle _ => NONE
10.32 )
10.33 end
10.34 - | term2poly' (Const ("op *",_) $ t1 $ t2) v :mv_poly option=
10.35 + | term2poly' (Const ("Groups.times_class.times",_) $ t1 $ t2) v :mv_poly option=
10.36 let
10.37 val t1pp= Unsynchronized.ref [];
10.38 val t2pp= Unsynchronized.ref [];
10.39 @@ -1603,13 +1603,13 @@
10.40 (
10.41 if hd(!xss)=1 then
10.42 (
10.43 - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.44 + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.45 Free(hd(!vv), HOLogic.realT) $
10.46 powerproduct2term(tl(!xss),tl(!vv))
10.47 )
10.48 else
10.49 (
10.50 - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.51 + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.52 (
10.53 Const("Atools.pow",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.54 Free(hd(!vv), HOLogic.realT) $ Free(str_of_int (hd(!xss)),HOLogic.realT)
10.55 @@ -1637,7 +1637,7 @@
10.56 )
10.57 else
10.58 (
10.59 - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.60 + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.61 Free(str_of_int c,HOLogic.realT) $
10.62 powerproduct2term(e,v)
10.63 )
10.64 @@ -1654,10 +1654,10 @@
10.65 Free ((str_of_int o abs) i, HOLogic.realT)
10.66 else
10.67 if i > 0
10.68 - then Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
10.69 + then Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
10.70 (Free (str_of_int i, HOLogic.realT)) $
10.71 powerproduct2term(is, v)
10.72 - else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
10.73 + else Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
10.74 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
10.75 Free ((str_of_int o abs) i, HOLogic.realT)) $
10.76 powerproduct2term(is, vs);---------------------------*)
10.77 @@ -1666,7 +1666,7 @@
10.78 then Free (str_of_int i, HOLogic.realT)
10.79 else if i = 1
10.80 then powerproduct2term (is, vs)
10.81 - else Const ("op *", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
10.82 + else Const ("Groups.times_class.times", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
10.83 (Free (str_of_int i, HOLogic.realT)) $
10.84 powerproduct2term (is, vs);
10.85
10.86 @@ -1697,7 +1697,7 @@
10.87 )
10.88 else
10.89 (
10.90 - Const("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.91 + Const("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.92 Free(str_of_int (abs(c)),HOLogic.realT) $
10.93 powerproduct2term(e,v)
10.94 )
10.95 @@ -1769,13 +1769,13 @@
10.96 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.97 $
10.98 (
10.99 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.100 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.101 poly2term(!p1',vars) $
10.102 poly2term(!p3,vars)
10.103 )
10.104 $
10.105 (
10.106 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.107 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.108 poly2term(!p2',vars) $
10.109 poly2term(!p3,vars)
10.110 )
10.111 @@ -1789,13 +1789,13 @@
10.112 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.113 $
10.114 (
10.115 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.116 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.117 poly2term(!p1',vars) $
10.118 poly2term(!p3,vars)
10.119 )
10.120 $
10.121 (
10.122 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.123 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.124 poly2term(!p2',vars) $
10.125 poly2term(!p3,vars)
10.126 )
10.127 @@ -1834,13 +1834,13 @@
10.128 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.129 $
10.130 (
10.131 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.132 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.133 poly2expanded(!p1',vars) $
10.134 poly2expanded(!p3,vars)
10.135 )
10.136 $
10.137 (
10.138 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.139 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.140 poly2expanded(!p2',vars) $
10.141 poly2expanded(!p3,vars)
10.142 )
10.143 @@ -1854,13 +1854,13 @@
10.144 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.145 $
10.146 (
10.147 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.148 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.149 poly2expanded(!p1',vars) $
10.150 poly2expanded(!p3,vars)
10.151 )
10.152 $
10.153 (
10.154 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.155 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.156 poly2expanded(!p2',vars) $
10.157 poly2expanded(!p3,vars)
10.158 )
10.159 @@ -2283,7 +2283,7 @@
10.160 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.161 $
10.162 (
10.163 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.164 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.165 poly2term(the (term2poly p1' p1var),p1var) $
10.166 poly2term(p3,var)
10.167 )
10.168 @@ -2315,7 +2315,7 @@
10.169 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.170 $
10.171 (
10.172 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.173 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.174 poly2term(the (term2poly p1' p1var),p1var) $
10.175 poly2term(p3,var)
10.176 )
10.177 @@ -2359,7 +2359,7 @@
10.178 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.179 $
10.180 (
10.181 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.182 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.183 poly2expanded(the(expanded2poly p1' p1var),p1var) $
10.184 poly2expanded(p3,var)
10.185 )
10.186 @@ -2391,7 +2391,7 @@
10.187 Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
10.188 $
10.189 (
10.190 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.191 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.192 poly2expanded(the(expanded2poly p1' p1var),p1var) $
10.193 poly2expanded(p3,var)
10.194 )
10.195 @@ -2559,7 +2559,7 @@
10.196 | make_term ((x::xs),vars) = if length(xs)=0 then poly2term(sort (mv_geq LEX_) (x),vars)
10.197 else
10.198 (
10.199 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.200 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.201 poly2term(sort (mv_geq LEX_) (x),vars) $
10.202 make_term(xs,vars)
10.203 );
10.204 @@ -2584,7 +2584,7 @@
10.205 | make_exp ((x::xs),vars) = if length(xs)=0 then poly2expanded(sort (mv_geq LEX_) (x),vars)
10.206 else
10.207 (
10.208 - Const ("op *",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.209 + Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.210 poly2expanded(sort (mv_geq LEX_) (x),vars) $
10.211 make_exp(xs,vars)
10.212 );
10.213 @@ -2682,7 +2682,7 @@
10.214 [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.215 t $ Free("1",HOLogic.realT)
10.216 ]
10.217 - | term2list (t as (Const("op *",_) $ _ $ _)) =
10.218 + | term2list (t as (Const("Groups.times_class.times",_) $ _ $ _)) =
10.219 [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
10.220 t $ Free("1",HOLogic.realT)
10.221 ]
10.222 @@ -3002,7 +3002,7 @@
10.223 ord_make_polynomial false thy),
10.224 erls = rational_erls,
10.225 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
10.226 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
10.227 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
10.228 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
10.229 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
10.230 (*asm_thm=[("real_mult_div_cancel2","")],*)
10.231 @@ -3084,7 +3084,7 @@
10.232 ord_make_polynomial false thy),
10.233 erls = rational_erls,
10.234 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
10.235 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
10.236 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
10.237 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
10.238 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
10.239 scr=Rfuns {init_state = init_state thy Atools_erls ro,
10.240 @@ -3236,7 +3236,7 @@
10.241 ord_make_polynomial false thy),
10.242 erls = rational_erls,
10.243 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
10.244 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
10.245 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
10.246 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
10.247 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
10.248 scr=Rfuns {init_state = init_state thy Atools_erls ro,
10.249 @@ -3384,7 +3384,7 @@
10.250 ord_make_polynomial false thy),
10.251 erls = rational_erls,
10.252 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
10.253 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
10.254 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
10.255 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
10.256 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
10.257 (*asm_thm=[("real_mult_div_cancel2","")],*)
10.258 @@ -3404,14 +3404,14 @@
10.259 fun is_ratpolyexp (Free _) = true
10.260 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
10.261 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
10.262 - | is_ratpolyexp (Const ("op *",_) $ Free _ $ Free _) = true
10.263 + | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
10.264 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
10.265 | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true
10.266 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
10.267 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
10.268 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
10.269 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
10.270 - | is_ratpolyexp (Const ("op *",_) $ t1 $ t2) =
10.271 + | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
10.272 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
10.273 | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
10.274 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
11.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Sep 28 10:01:18 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Sep 28 10:10:26 2010 +0200
11.3 @@ -172,7 +172,7 @@
11.4 Calc ("Atools.pow" ,eval_binop "#power_"),
11.5 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.6 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.7 - Calc ("op *", eval_binop "#mult_"),
11.8 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.9 Calc ("op =",eval_equal "#equal_")
11.10 ];
11.11
11.12 @@ -184,7 +184,7 @@
11.13 Calc ("Atools.pow" ,eval_binop "#power_"),
11.14 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.15 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.16 - Calc ("op *", eval_binop "#mult_"),
11.17 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.18 Calc ("op =",eval_equal "#equal_")
11.19 ];
11.20
11.21 @@ -252,7 +252,7 @@
11.22 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
11.23
11.24 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.25 - Calc ("op *", eval_binop "#mult_"),
11.26 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.27 Calc ("Atools.pow", eval_binop "#power_")
11.28 ],
11.29 scr = Script ((term_of o the o (parse thy)) "empty_script")
11.30 @@ -298,7 +298,7 @@
11.31
11.32 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.33 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.34 - Calc ("op *", eval_binop "#mult_"),
11.35 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.36 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
11.37 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
11.38 Calc ("Atools.pow", eval_binop "#power_"),
11.39 @@ -323,7 +323,7 @@
11.40
11.41 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.42 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.43 - Calc ("op *", eval_binop "#mult_"),
11.44 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.45 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
11.46 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
11.47 Calc ("Atools.pow", eval_binop "#power_")
12.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 28 10:01:18 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 28 10:10:26 2010 +0200
12.3 @@ -157,7 +157,7 @@
12.4 fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:")
12.5 (* at the moment there is no term like this, but ....*)
12.6 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
12.7 - | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
12.8 + | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
12.9 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
12.10 | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
12.11 (is_sqrtTerm_in t2 v)
12.12 @@ -447,7 +447,7 @@
12.13 (* a*(b*c) = a*b*c *)
12.14 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
12.15 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
12.16 - Calc ("op *",eval_binop "#mult_"),
12.17 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
12.18 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
12.19 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
12.20 Calc ("Atools.pow" ,eval_binop "#power_"),
13.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 10:01:18 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 10:10:26 2010 +0200
13.3 @@ -228,7 +228,7 @@
13.4 Calc ("Tools.matches",eval_matches ""),
13.5
13.6 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
13.7 - Calc ("op *",eval_binop "#mult_"),
13.8 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
13.9 Calc ("Atools.pow" ,eval_binop "#power_"),
13.10
13.11 Calc ("op <",eval_equ "#less_"),
13.12 @@ -273,7 +273,7 @@
13.13 eval_contains_root"#contains_root_"),
13.14
13.15 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
13.16 - Calc ("op *",eval_binop "#mult_"),
13.17 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
13.18 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
13.19 Calc ("Atools.pow" ,eval_binop "#power_"),
13.20
13.21 @@ -407,7 +407,7 @@
13.22 (* these 2 rules are invers to distr_div_right wrt. termination.
13.23 thus they MUST be done IMMEDIATELY before calc *)
13.24 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.25 - Calc ("op *", eval_binop "#mult_"),
13.26 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.27 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
13.28 Calc ("Atools.pow", eval_binop "#power_"),
13.29
13.30 @@ -485,7 +485,7 @@
13.31 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
13.32 (*aus Atools.ML*)
13.33 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.34 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
13.35 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
13.36 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.37 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
13.38 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
13.39 @@ -1296,7 +1296,7 @@
13.40 rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),
13.41 erls = testerls, srls = Erls,
13.42 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
13.43 - ("TIMES" , ("op *", eval_binop "#mult_")),
13.44 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
13.45 ("POWER", ("Atools.pow", eval_binop "#power_"))
13.46 ],
13.47 (*asm_thm = [],*)
13.48 @@ -1353,7 +1353,7 @@
13.49 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
13.50
13.51 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.52 - Calc ("op *", eval_binop "#mult_"),
13.53 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.54 Calc ("Atools.pow", eval_binop "#power_")
13.55 ],
13.56 scr = EmptyScr(*Script ((term_of o the o (parse thy))
13.57 @@ -1402,7 +1402,7 @@
13.58 rew_ord = ("termlessI",termlessI),
13.59 erls = testerls, srls = Erls,
13.60 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
13.61 - ("TIMES" , ("op *", eval_binop "#mult_")),
13.62 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
13.63 ("POWER", ("Atools.pow", eval_binop "#power_"))
13.64 ],
13.65 rules =
13.66 @@ -1453,7 +1453,7 @@
13.67 (*"0 + z = z"*)
13.68
13.69 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.70 - Calc ("op *", eval_binop "#mult_"),
13.71 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.72 Calc ("Atools.pow", eval_binop "#power_"),
13.73 (*
13.74 Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
13.75 @@ -1486,7 +1486,7 @@
13.76 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
13.77
13.78 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.79 - Calc ("op *", eval_binop "#mult_"),
13.80 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.81 Calc ("Atools.pow", eval_binop "#power_")
13.82 ],
13.83 scr = EmptyScr
14.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:01:18 2010 +0200
14.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:10:26 2010 +0200
14.3 @@ -173,8 +173,8 @@
14.4 > Syntax.string_of_term (thy2ctxt thy) t';
14.5 >
14.6 > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
14.7 -> val eval_fn = the (assoc (!eval_list, "op *"));
14.8 -> val (SOME (id,t')) = get_pair thy "op *" eval_fn t;
14.9 +> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
14.10 +> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
14.11 > Syntax.string_of_term (thy2ctxt thy) t';
14.12 >
14.13 > val t = (term_of o the o (parse thy)) "#0 < #4";
14.14 @@ -283,7 +283,7 @@
14.15 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
14.16
14.17 > val ct = (the o (parse thy)) "#3*(#4*a)";
14.18 -> get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct;
14.19 +> get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
14.20 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
14.21
14.22 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
14.23 @@ -303,7 +303,7 @@
14.24
14.25 (*
14.26 > val ct = (the o (parse thy)) "a + 3*4";
14.27 -> applicable "calculate" (Calc("op *", "mult_")) ct;
14.28 +> applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;
14.29 val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option
14.30
14.31 --------------------------
15.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 10:01:18 2010 +0200
15.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 10:10:26 2010 +0200
15.3 @@ -565,7 +565,7 @@
15.4 | num_of_term t = error ("num_of_term not for "^term2str t);
15.5
15.6 fun mk_factroot op_(*=thy.sqrt*) T fact root =
15.7 - Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
15.8 + Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
15.9 (Const (op_, T --> T) $ term_of_num T root);
15.10 (*
15.11 val T = (type_of o term_of o the) (parse thy "#12::real");
15.12 @@ -608,7 +608,7 @@
15.13 (*used for calculating built in binary operations in Isabelle2002->Float.ML*)
15.14 (*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
15.15 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
15.16 - | calc "op *" (n1, n2) = n1*n2
15.17 + | calc "Groups.times_class.times" (n1, n2) = n1*n2
15.18 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
15.19 | calc "Atools.pow"(n1, n2) = power n1 n2
15.20 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
15.21 @@ -1159,10 +1159,10 @@
15.22 use length (vars term) = 1 instead*)
15.23 fun is_atom (Const ("Float.Float",_) $ _) = true
15.24 | is_atom (Const ("ComplexI.I'_'_",_)) = true
15.25 - | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
15.26 + | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
15.27 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
15.28 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
15.29 - (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
15.30 + (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
15.31 is_atom t1 andalso is_atom t2
15.32 | is_atom (Const _) = true
15.33 | is_atom (Free _) = true
15.34 @@ -1182,7 +1182,7 @@
15.35 > is_atom t;
15.36 val it = true : bool
15.37 > val t = str2term "1 + 2*I__";
15.38 -> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
15.39 +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
15.40 *)
15.41
15.42 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
16.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 10:01:18 2010 +0200
16.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 10:10:26 2010 +0200
16.3 @@ -70,7 +70,7 @@
16.4 Calc ("Tools.matches",eval_matches ""),
16.5
16.6 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
16.7 - Calc ("op *",eval_binop "#mult_"),
16.8 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
16.9 Calc ("Atools.pow" ,eval_binop "#power_"),
16.10
16.11 Calc ("op <",eval_equ "#less_"),
17.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:01:18 2010 +0200
17.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:10:26 2010 +0200
17.3 @@ -282,7 +282,7 @@
17.4 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
17.5
17.6 val (i,is) = (~1,[2]);
17.7 - val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
17.8 + val ttt = Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
17.9 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
17.10 Free ((str_of_int o abs) i, HOLogic.realT)) $
17.11 powerproduct2term(is, vs);
18.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:01:18 2010 +0200
18.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Sep 28 10:10:26 2010 +0200
18.3 @@ -103,7 +103,7 @@
18.4 ],
18.5 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
18.6 calc=[("PLUS" ,("op +" ,eval_binop "#add_")),
18.7 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
18.8 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
18.9 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
18.10 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
18.11 crls=tval_rls, nrls=e_rls(*,