1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:01:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 10:10:26 2010 +0200
1.3 @@ -213,12 +213,12 @@
1.4 if (1) then degree 0
1.5 if (2) then v is a factor on the very right, ev. with exponent.*)
1.6 fun factor_right_deg (*case 2*)
1.7 - (t as Const ("op *",_) $ t1 $
1.8 + (t as Const ("Groups.times_class.times",_) $ t1 $
1.9 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
1.10 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
1.11 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
1.12 if (vv = v) then SOME (int_of_str' d) else NONE
1.13 - | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
1.14 + | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
1.15 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
1.16 | factor_right_deg vv v =
1.17 if (vv = v) then SOME 1 else NONE;
1.18 @@ -401,7 +401,7 @@
1.19 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.20 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.21 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.22 - Calc ("op *",eval_binop "#mult_"),
1.23 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.24 Calc ("Atools.pow" ,eval_binop "#power_")
1.25 ];
1.26
1.27 @@ -411,7 +411,7 @@
1.28 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.29 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.30 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.31 - Calc ("op *",eval_binop "#mult_"),
1.32 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.33 Calc ("Atools.pow" ,eval_binop "#power_")
1.34 ];
1.35
1.36 @@ -555,13 +555,13 @@
1.37 fun is_polyexp (Free _) = true
1.38 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
1.39 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
1.40 - | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
1.41 + | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
1.42 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.43 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.44 ((is_polyexp t1) andalso (is_polyexp t2))
1.45 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.46 ((is_polyexp t1) andalso (is_polyexp t2))
1.47 - | is_polyexp (Const ("op *",_) $ t1 $ t2) =
1.48 + | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1.49 ((is_polyexp t1) andalso (is_polyexp t2))
1.50 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
1.51 ((is_polyexp t1) andalso (is_polyexp t2))
1.52 @@ -659,12 +659,12 @@
1.53 rew_ord = ("dummy_ord", dummy_ord),
1.54 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.55 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.56 - ("TIMES" , ("op *", eval_binop "#mult_")),
1.57 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.58 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.59 ],
1.60 (*asm_thm = [],*)
1.61 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.62 - Calc ("op *", eval_binop "#mult_"),
1.63 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.64 Calc ("Atools.pow", eval_binop "#power_")
1.65 ], scr = EmptyScr}:rls;
1.66
1.67 @@ -752,7 +752,7 @@
1.68 rew_ord = ("dummy_ord", dummy_ord),
1.69 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.70 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.71 - ("TIMES" , ("op *", eval_binop "#mult_")),
1.72 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.73 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.74 ],
1.75 (*asm_thm = [],*)
1.76 @@ -880,7 +880,7 @@
1.77 rew_ord = ("dummy_ord", dummy_ord),
1.78 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.79 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.80 - ("TIMES" , ("op *", eval_binop "#mult_")),
1.81 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.82 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.83 ],
1.84 (*asm_thm = [],*)
1.85 @@ -894,7 +894,7 @@
1.86 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1.87 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.88 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.89 - Calc ("op *", eval_binop "#mult_"),
1.90 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.91 Calc ("Atools.pow", eval_binop "#power_")
1.92 ], scr = EmptyScr}:rls;
1.93 val reduce_012 =
1.94 @@ -1025,7 +1025,7 @@
1.95 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.96 erls = Atools_erls, srls = Erls,
1.97 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.98 - ("TIMES" , ("op *", eval_binop "#mult_")),
1.99 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.100 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.101 ],
1.102 rules = [Thm ("real_plus_binom_pow2",
1.103 @@ -1080,7 +1080,7 @@
1.104 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
1.105
1.106 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.107 - Calc ("op *", eval_binop "#mult_"),
1.108 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.109 Calc ("Atools.pow", eval_binop "#power_"),
1.110 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
1.111 (*AC-rewriting*)
1.112 @@ -1115,7 +1115,7 @@
1.113 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.114
1.115 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.116 - Calc ("op *", eval_binop "#mult_"),
1.117 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.118 Calc ("Atools.pow", eval_binop "#power_")
1.119 ],
1.120 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
1.121 @@ -1132,7 +1132,7 @@
1.122 | poly2list t = [t];
1.123
1.124 (* Monom --> Liste von Variablen *)
1.125 -fun monom2list (Const ("op *",_) $ t1 $ t2) =
1.126 +fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1.127 (monom2list t1) @ (monom2list t2)
1.128 | monom2list t = [t];
1.129
1.130 @@ -1278,7 +1278,7 @@
1.131 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1.132 (mit gewuenschtem Typen T) *)
1.133 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
1.134 -fun mult T = Const ("op *", [T,T] ---> T);
1.135 +fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
1.136 fun binop op_ t1 t2 = op_ $ t1 $ t2;
1.137 fun create_prod T (a,b) = binop (mult T) a b;
1.138 fun create_sum T (a,b) = binop (plus T) a b;
1.139 @@ -1353,7 +1353,7 @@
1.140 [Calc ("Poly.is'_multUnordered",
1.141 eval_is_multUnordered "")],
1.142 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")),
1.143 - ("TIMES" , ("op *" , eval_binop "#mult_")),
1.144 + ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")),
1.145 ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
1.146 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1.147 scr=Rfuns {init_state = init_state,
1.148 @@ -1406,7 +1406,7 @@
1.149 (*WN.18.6.03 definiert in thy,
1.150 evaluiert prepat*)],
1.151 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
1.152 - ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.153 + ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
1.154 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
1.155 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1.156 (*asm_thm=[],*)
1.157 @@ -1433,7 +1433,7 @@
1.158 erls = Atools_erls, srls = Erls,calc = [],
1.159 rules = [Rls_ discard_minus,
1.160 Rls_ expand_poly_,
1.161 - Calc ("op *", eval_binop "#mult_"),
1.162 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.163 Rls_ order_mult_rls_,
1.164 Rls_ simplify_power_,
1.165 Rls_ calc_add_mult_pow_,
1.166 @@ -1451,7 +1451,7 @@
1.167 erls = Atools_erls, srls = Erls, calc = [],
1.168 rules = [Rls_ discard_minus,
1.169 Rls_ expand_poly_,
1.170 - Calc ("op *", eval_binop "#mult_"),
1.171 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.172 Rls_ order_mult_rls_,
1.173 Rls_ simplify_power_,
1.174 Rls_ calc_add_mult_pow_,
1.175 @@ -1473,7 +1473,7 @@
1.176 erls = Atools_erls, srls = Erls, calc = [],
1.177 rules = [Rls_ discard_minus,
1.178 Rls_ expand_poly_rat_,(*ignors rationals*)
1.179 - Calc ("op *", eval_binop "#mult_"),
1.180 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.181 Rls_ order_mult_rls_,
1.182 Rls_ simplify_power_,
1.183 Rls_ calc_add_mult_pow_,
1.184 @@ -1492,7 +1492,7 @@
1.185 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1.186 erls = Atools_erls, srls = Erls,
1.187 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.188 - ("TIMES" , ("op *", eval_binop "#mult_")),
1.189 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.190 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1.191 ],
1.192 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1.193 @@ -1515,7 +1515,7 @@
1.194 (*Rls_ order_add_rls_,*)
1.195
1.196 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.197 - Calc ("op *", eval_binop "#mult_"),
1.198 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.199 Calc ("Atools.pow", eval_binop "#power_"),
1.200
1.201 Thm ("sym_realpow_twoI",
1.202 @@ -1541,7 +1541,7 @@
1.203 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.204
1.205 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.206 - Calc ("op *", eval_binop "#mult_"),
1.207 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.208 Calc ("Atools.pow", eval_binop "#power_"),
1.209
1.210 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)