1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 12:56:51 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Sep 23 14:49:23 2010 +0200
1.3 @@ -177,7 +177,7 @@
1.4 let fun coeff_in c v = member op = (vars c) v;
1.5 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
1.6 (* at the moment there is no term like this, but ....*)
1.7 - | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v =
1.8 + | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v =
1.9 not(coeff_in b v)
1.10 | finddivide (_ $ t1 $ t2) v =
1.11 (finddivide t1 v) orelse (finddivide t2 v)
1.12 @@ -250,21 +250,21 @@
1.13 (*val it = NONE*)
1.14 ------------------------------------------------------------------*)
1.15 fun expand_deg_in t v =
1.16 - let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.17 + let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.18 (case mono_deg_in t2 v of (* $ is left associative*)
1.19 SOME d' => edi d' d' t1
1.20 | NONE => NONE)
1.21 - | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
1.22 + | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.23 (case mono_deg_in t2 v of
1.24 SOME d' => edi d' d' t1
1.25 | NONE => NONE)
1.26 - | edi d dmax (Const ("op -",_) $ t1 $ t2) =
1.27 + | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.28 (case mono_deg_in t2 v of
1.29 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.30 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
1.31 then edi d' dmax t1 else NONE
1.32 | NONE => NONE)
1.33 - | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.34 + | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.35 (case mono_deg_in t2 v of
1.36 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.37 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
1.38 @@ -297,11 +297,11 @@
1.39 expand_deg_in t v;
1.40 -------------------------------------------------------------------*)
1.41 fun poly_deg_in t v =
1.42 - let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
1.43 + let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.44 (case mono_deg_in t2 v of (* $ is left associative*)
1.45 SOME d' => edi d' d' t1
1.46 | NONE => NONE)
1.47 - | edi d dmax (Const ("op +",_) $ t1 $ t2) =
1.48 + | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.49 (case mono_deg_in t2 v of
1.50 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
1.51 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
1.52 @@ -399,8 +399,8 @@
1.53 append_rls "Poly_erls" Atools_erls
1.54 [ Calc ("op =",eval_equal "#equal_"),
1.55 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.56 - Calc ("op +",eval_binop "#add_"),
1.57 - Calc ("op -",eval_binop "#sub_"),
1.58 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.59 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.60 Calc ("op *",eval_binop "#mult_"),
1.61 Calc ("Atools.pow" ,eval_binop "#power_")
1.62 ];
1.63 @@ -409,8 +409,8 @@
1.64 append_rls "poly_crls" Atools_crls
1.65 [ Calc ("op =",eval_equal "#equal_"),
1.66 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.67 - Calc ("op +",eval_binop "#add_"),
1.68 - Calc ("op -",eval_binop "#sub_"),
1.69 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.70 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.71 Calc ("op *",eval_binop "#mult_"),
1.72 Calc ("Atools.pow" ,eval_binop "#power_")
1.73 ];
1.74 @@ -553,13 +553,13 @@
1.75 (*.the expression contains + - * ^ only ?
1.76 this is weaker than 'is_polynomial' !.*)
1.77 fun is_polyexp (Free _) = true
1.78 - | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
1.79 - | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
1.80 + | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
1.81 + | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
1.82 | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
1.83 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.84 - | is_polyexp (Const ("op +",_) $ t1 $ t2) =
1.85 + | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.86 ((is_polyexp t1) andalso (is_polyexp t2))
1.87 - | is_polyexp (Const ("op -",_) $ t1 $ t2) =
1.88 + | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.89 ((is_polyexp t1) andalso (is_polyexp t2))
1.90 | is_polyexp (Const ("op *",_) $ t1 $ t2) =
1.91 ((is_polyexp t1) andalso (is_polyexp t2))
1.92 @@ -658,12 +658,12 @@
1.93 Rls{id = "calc_add_mult_pow_", preconds = [],
1.94 rew_ord = ("dummy_ord", dummy_ord),
1.95 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.96 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.97 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.98 ("TIMES" , ("op *", eval_binop "#mult_")),
1.99 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.100 ],
1.101 (*asm_thm = [],*)
1.102 - rules = [Calc ("op +", eval_binop "#add_"),
1.103 + rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.104 Calc ("op *", eval_binop "#mult_"),
1.105 Calc ("Atools.pow", eval_binop "#power_")
1.106 ], scr = EmptyScr}:rls;
1.107 @@ -689,7 +689,7 @@
1.108 Rls{id = "collect_numerals_", preconds = [],
1.109 rew_ord = ("dummy_ord", dummy_ord),
1.110 erls = Atools_erls, srls = Erls,
1.111 - calc = [("PLUS" , ("op +", eval_binop "#add_"))
1.112 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
1.113 ],
1.114 rules =
1.115 [Thm ("real_num_collect",num_str @{thm real_num_collect}),
1.116 @@ -702,7 +702,7 @@
1.117 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
1.118 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.119
1.120 - Calc ("op +", eval_binop "#add_"),
1.121 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.122
1.123 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.124 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.125 @@ -751,7 +751,7 @@
1.126 Rls{id = "collect_numerals", preconds = [],
1.127 rew_ord = ("dummy_ord", dummy_ord),
1.128 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.129 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.130 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.131 ("TIMES" , ("op *", eval_binop "#mult_")),
1.132 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.133 ],
1.134 @@ -766,7 +766,7 @@
1.135 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1.136 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
1.137
1.138 - Calc ("op +", eval_binop "#add_"),
1.139 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.140
1.141 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
1.142 Thm ("sym_real_mult_2",
1.143 @@ -879,7 +879,7 @@
1.144 Rls{id = "collect_numerals", preconds = [],
1.145 rew_ord = ("dummy_ord", dummy_ord),
1.146 erls = Atools_erls(*erls3.4.03*),srls = Erls,
1.147 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.148 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.149 ("TIMES" , ("op *", eval_binop "#mult_")),
1.150 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.151 ],
1.152 @@ -893,7 +893,7 @@
1.153 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.154 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1.155 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.156 - Calc ("op +", eval_binop "#add_"),
1.157 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.158 Calc ("op *", eval_binop "#mult_"),
1.159 Calc ("Atools.pow", eval_binop "#power_")
1.160 ], scr = EmptyScr}:rls;
1.161 @@ -1024,7 +1024,7 @@
1.162 val expand_binoms =
1.163 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.164 erls = Atools_erls, srls = Erls,
1.165 - calc = [("PLUS" , ("op +", eval_binop "#add_")),
1.166 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.167 ("TIMES" , ("op *", eval_binop "#mult_")),
1.168 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.169 ],
1.170 @@ -1079,7 +1079,7 @@
1.171 (*"0 * z = 0"*)
1.172 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
1.173
1.174 - Calc ("op +", eval_binop "#add_"),
1.175 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.176 Calc ("op *", eval_binop "#mult_"),
1.177 Calc ("Atools.pow", eval_binop "#power_"),
1.178 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
1.179 @@ -1114,7 +1114,7 @@
1.180 num_str @{thm real_one_collect_assoc}),
1.181 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.182
1.183 - Calc ("op +", eval_binop "#add_"),
1.184 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.185 Calc ("op *", eval_binop "#mult_"),
1.186 Calc ("Atools.pow", eval_binop "#power_")
1.187 ],
1.188 @@ -1127,7 +1127,7 @@
1.189 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
1.190 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1.191 (* Polynom --> List von Monomen *)
1.192 -fun poly2list (Const ("op +",_) $ t1 $ t2) =
1.193 +fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.194 (poly2list t1) @ (poly2list t2)
1.195 | poly2list t = [t];
1.196
1.197 @@ -1277,7 +1277,7 @@
1.198
1.199 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1.200 (mit gewuenschtem Typen T) *)
1.201 -fun plus T = Const ("op +", [T,T] ---> T);
1.202 +fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
1.203 fun mult T = Const ("op *", [T,T] ---> T);
1.204 fun binop op_ t1 t2 = op_ $ t1 $ t2;
1.205 fun create_prod T (a,b) = binop (mult T) a b;
1.206 @@ -1352,9 +1352,9 @@
1.207 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
1.208 [Calc ("Poly.is'_multUnordered",
1.209 eval_is_multUnordered "")],
1.210 - calc = [("PLUS" , ("op +" , eval_binop "#add_")),
1.211 + calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")),
1.212 ("TIMES" , ("op *" , eval_binop "#mult_")),
1.213 - ("DIVIDE", ("HOL.divide", eval_cancel "#divide_e")),
1.214 + ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
1.215 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1.216 scr=Rfuns {init_state = init_state,
1.217 normal_form = normal_form,
1.218 @@ -1405,9 +1405,9 @@
1.219 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
1.220 (*WN.18.6.03 definiert in thy,
1.221 evaluiert prepat*)],
1.222 - calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1.223 + calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
1.224 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.225 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_e")),
1.226 + ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
1.227 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1.228 (*asm_thm=[],*)
1.229 scr=Rfuns {init_state = init_state,
1.230 @@ -1491,7 +1491,7 @@
1.231 val rev_rew_p =
1.232 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1.233 erls = Atools_erls, srls = Erls,
1.234 - calc = [(*("PLUS" , ("op +", eval_binop "#add_")),
1.235 + calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.236 ("TIMES" , ("op *", eval_binop "#mult_")),
1.237 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1.238 ],
1.239 @@ -1514,7 +1514,7 @@
1.240 Rls_ order_mult_rls_,
1.241 (*Rls_ order_add_rls_,*)
1.242
1.243 - Calc ("op +", eval_binop "#add_"),
1.244 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.245 Calc ("op *", eval_binop "#mult_"),
1.246 Calc ("Atools.pow", eval_binop "#power_"),
1.247
1.248 @@ -1540,7 +1540,7 @@
1.249 Thm ("realpow_multI", num_str @{thm realpow_multI}),
1.250 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.251
1.252 - Calc ("op +", eval_binop "#add_"),
1.253 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.254 Calc ("op *", eval_binop "#mult_"),
1.255 Calc ("Atools.pow", eval_binop "#power_"),
1.256