119 |
119 |
120 section \<open>Cancellation and addition of fractions\<close> |
120 section \<open>Cancellation and addition of fractions\<close> |
121 subsection \<open>Conversion term <--> poly\<close> |
121 subsection \<open>Conversion term <--> poly\<close> |
122 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close> |
122 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close> |
123 ML \<open> |
123 ML \<open> |
124 fun monom_of_term vs (c, es) (Const (id, _)) = |
124 fun monom_of_term vs (c, es) (t as Const _) = |
125 (c, list_update es (find_index (curry op = (strip_thy id)) vs) 1) |
125 (c, list_update es (find_index (curry op = t) vs) 1) |
126 | monom_of_term vs (c, es) (Free (id, _)) = |
126 | monom_of_term vs (c, es) (t as Free (id, _)) = |
127 if TermC.is_num' id |
127 if TermC.is_num' id |
128 then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*) |
128 then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*) |
129 else (c, list_update es (find_index (curry op = id) vs) 1) |
129 else (c, list_update es (find_index (curry op = t) vs) 1) |
130 | monom_of_term vs (c, es) (Const ("Atools.pow", _) $ Free (id, _) $ Free (e, _)) = |
130 | monom_of_term vs (c, es) (Const ("Atools.pow", _) $ (t as Free _) $ Free (e, _)) = |
131 (c, list_update es (find_index (curry op = id) vs) (the (TermC.int_of_str_opt e))) |
131 (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_of_str_opt e))) |
132 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) = |
132 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) = |
133 let val (c', es') = monom_of_term vs (c, es) m1 |
133 let val (c', es') = monom_of_term vs (c, es) m1 |
134 in monom_of_term vs (c', es') m2 end |
134 in monom_of_term vs (c', es') m2 end |
135 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ Rule.term2str t) |
135 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ Rule.term2str t) |
136 |
136 |
162 | poly_of_term vs t = |
162 | poly_of_term vs t = |
163 (SOME [monom_of_term vs (1, replicate (length vs) 0) t] |
163 (SOME [monom_of_term vs (1, replicate (length vs) 0) t] |
164 handle ERROR _ => NONE) |
164 handle ERROR _ => NONE) |
165 |
165 |
166 fun is_poly t = |
166 fun is_poly t = |
167 let |
167 let |
168 val vs = t |> TermC.vars |> map TermC.str_of_free_opt (* tolerate Var in simplification *) |
168 val vs = TermC.vars_of t |
169 |> filter is_some |> map the |> sort string_ord |
|
170 in |
169 in |
171 case poly_of_term vs t of SOME _ => true | NONE => false |
170 case poly_of_term vs t of SOME _ => true | NONE => false |
172 end |
171 end |
173 val is_expanded = is_poly (* TODO: check names *) |
172 val is_expanded = is_poly (* TODO: check names *) |
174 val is_polynomial = is_poly (* TODO: check names *) |
173 val is_polynomial = is_poly (* TODO: check names *) |
175 \<close> |
174 \<close> |
176 |
175 |
177 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close> |
176 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close> |
178 ML \<open> |
177 ML \<open> |
179 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*) |
178 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*) |
180 | term_of_es baseT expT (_ :: vs) (0 :: es) = |
179 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es |
181 [] @ term_of_es baseT expT vs es |
180 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es |
182 | term_of_es baseT expT (v :: vs) (1 :: es) = |
|
183 [(Free (v, baseT))] @ term_of_es baseT expT vs es |
|
184 | term_of_es baseT expT (v :: vs) (e :: es) = |
181 | term_of_es baseT expT (v :: vs) (e :: es) = |
185 [Const ("Atools.pow", [baseT, expT] ---> baseT) $ |
182 Const ("Atools.pow", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT)) |
186 (Free (v, baseT)) $ (Free (TermC.isastr_of_int e, expT))] |
183 :: term_of_es baseT expT vs es |
187 @ term_of_es baseT expT vs es |
184 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es" |
188 |
185 |
189 fun term_of_monom baseT expT vs ((c, es): monom) = |
186 fun term_of_monom baseT expT vs ((c, es): monom) = |
190 let val es' = term_of_es baseT expT vs es |
187 let val es' = term_of_es baseT expT vs es |
191 in |
188 in |
192 if c = 1 |
189 if c = 1 |
226 let val opt = check_fraction t |
223 let val opt = check_fraction t |
227 in |
224 in |
228 case opt of |
225 case opt of |
229 NONE => NONE |
226 NONE => NONE |
230 | SOME (numerator, denominator) => |
227 | SOME (numerator, denominator) => |
231 let |
228 let |
232 val vs = t |> TermC.vars |> map TermC.str_of_free_opt (* tolerate Var in simplification *) |
229 val vs = TermC.vars_of t |
233 |> filter is_some |> map the |> sort string_ord |
|
234 val baseT = type_of numerator |
230 val baseT = type_of numerator |
235 val expT = HOLogic.realT |
231 val expT = HOLogic.realT |
236 in |
232 in |
237 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
233 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
238 (SOME a, SOME b) => |
234 (SOME a, SOME b) => |
272 let val opt = check_fraction t |
268 let val opt = check_fraction t |
273 in |
269 in |
274 case opt of |
270 case opt of |
275 NONE => NONE |
271 NONE => NONE |
276 | SOME (numerator, denominator) => |
272 | SOME (numerator, denominator) => |
277 let |
273 let |
278 val vs = t |> TermC.vars |> map TermC.str_of_free_opt (* tolerate Var in simplification *) |
274 val vs = TermC.vars_of t |
279 |> filter is_some |> map the |> sort string_ord |
|
280 val baseT = type_of numerator |
275 val baseT = type_of numerator |
281 val expT = HOLogic.realT |
276 val expT = HOLogic.realT |
282 in |
277 in |
283 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
278 case (poly_of_term vs numerator, poly_of_term vs denominator) of |
284 (SOME a, SOME b) => |
279 (SOME a, SOME b) => |
329 let val opt = check_frac_sum t |
324 let val opt = check_frac_sum t |
330 in |
325 in |
331 case opt of |
326 case opt of |
332 NONE => NONE |
327 NONE => NONE |
333 | SOME ((n1, d1), (n2, d2)) => |
328 | SOME ((n1, d1), (n2, d2)) => |
334 let |
329 let |
335 val vs = t |> TermC.vars |> map TermC.str_of_free_opt (* tolerate Var in simplification *) |
330 val vs = TermC.vars_of t |
336 |> filter is_some |> map the |> sort string_ord |
|
337 in |
331 in |
338 case (poly_of_term vs d1, poly_of_term vs d2) of |
332 case (poly_of_term vs d1, poly_of_term vs d2) of |
339 (SOME a, SOME b) => |
333 (SOME a, SOME b) => |
340 let |
334 let |
341 val ((a', b'), c) = gcd_poly a b |
335 val ((a', b'), c) = gcd_poly a b |
371 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*) |
365 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*) |
372 fun add_fraction_p_ (_: theory) t = |
366 fun add_fraction_p_ (_: theory) t = |
373 case check_frac_sum t of |
367 case check_frac_sum t of |
374 NONE => NONE |
368 NONE => NONE |
375 | SOME ((n1, d1), (n2, d2)) => |
369 | SOME ((n1, d1), (n2, d2)) => |
376 let (* vvvvvvv vvvvvvvvvvv tolerate Free, Const, Var *) |
370 let |
377 val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord |
371 val vs = TermC.vars_of t |
378 in |
372 in |
379 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of |
373 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of |
380 (SOME _, SOME a, SOME _, SOME b) => |
374 (SOME _, SOME a, SOME _, SOME b) => |
381 let |
375 let |
382 val ((a', b'), c) = gcd_poly a b |
376 val ((a', b'), c) = gcd_poly a b |