173 val thy = @{theory}; |
173 val thy = @{theory}; |
174 |
174 |
175 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
175 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
176 fun is_polyrat_in t v = |
176 fun is_polyrat_in t v = |
177 let fun coeff_in c v = member op = (vars c) v; |
177 let fun coeff_in c v = member op = (vars c) v; |
178 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:") |
178 fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:") |
179 (* at the moment there is no term like this, but ....*) |
179 (* at the moment there is no term like this, but ....*) |
180 | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = |
180 | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = |
181 not(coeff_in b v) |
181 not(coeff_in b v) |
182 | finddivide (_ $ t1 $ t2) v = |
182 | finddivide (_ $ t1 $ t2) v = |
183 (finddivide t1 v) orelse (finddivide t2 v) |
183 (finddivide t1 v) orelse (finddivide t2 v) |
1139 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *) |
1139 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *) |
1140 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str |
1140 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str |
1141 | get_basStr (Free (str, _)) = str |
1141 | get_basStr (Free (str, _)) = str |
1142 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *) |
1142 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *) |
1143 (*| get_basStr t = |
1143 (*| get_basStr t = |
1144 raise error("get_basStr: called with t= "^(term2str t));*) |
1144 error("get_basStr: called with t= "^(term2str t));*) |
1145 |
1145 |
1146 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *) |
1146 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *) |
1147 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str |
1147 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str |
1148 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *) |
1148 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *) |
1149 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *) |
1149 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *) |
1150 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *) |
1150 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *) |
1151 (*| get_potStr t = |
1151 (*| get_potStr t = |
1152 raise error("get_potStr: called with t= "^(term2str t));*) |
1152 error("get_potStr: called with t= "^(term2str t));*) |
1153 |
1153 |
1154 (* Umgekehrte string_ord *) |
1154 (* Umgekehrte string_ord *) |
1155 val string_ord_rev = rev_order o string_ord; |
1155 val string_ord_rev = rev_order o string_ord; |
1156 |
1156 |
1157 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) |
1157 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) |
1206 counter (n + (the (int_of_str str_h)), xs) |
1206 counter (n + (the (int_of_str str_h)), xs) |
1207 else counter (n + 1000, xs) (*FIXME.MG?!*) |
1207 else counter (n + 1000, xs) (*FIXME.MG?!*) |
1208 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => |
1208 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => |
1209 counter (n + 1000, xs) (*FIXME.MG?!*) |
1209 counter (n + 1000, xs) (*FIXME.MG?!*) |
1210 | (Free (str, _)) => counter (n + 1, xs) |
1210 | (Free (str, _)) => counter (n + 1, xs) |
1211 (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*) |
1211 (*| _ => error("monom_degree: called with factor: "^(term2str x)))*) |
1212 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*) |
1212 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*) |
1213 in |
1213 in |
1214 fun monom_degree l = counter (0, l) |
1214 fun monom_degree l = counter (0, l) |
1215 end;(*local*) |
1215 end;(*local*) |
1216 |
1216 |
1238 |
1238 |
1239 fun hd_str str = substring (str, 0, 1); |
1239 fun hd_str str = substring (str, 0, 1); |
1240 fun tl_str str = substring (str, 1, (size str) - 1); |
1240 fun tl_str str = substring (str, 1, (size str) - 1); |
1241 |
1241 |
1242 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *) |
1242 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *) |
1243 fun get_koeff_of_mon [] = raise error("get_koeff_of_mon: called with l = []") |
1243 fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []") |
1244 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x |
1244 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x |
1245 else NONE; |
1245 else NONE; |
1246 |
1246 |
1247 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *) |
1247 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *) |
1248 fun koeff2ordStr (SOME x) = (case x of |
1248 fun koeff2ordStr (SOME x) = (case x of |