185 either (1) v NOT existent in t, or (2) v contained in t, |
185 either (1) v NOT existent in t, or (2) v contained in t, |
186 if (1) then degree 0 |
186 if (1) then degree 0 |
187 if (2) then v is a factor on the very right, ev. with exponent.*) |
187 if (2) then v is a factor on the very right, ev. with exponent.*) |
188 fun factor_right_deg (*case 2*) |
188 fun factor_right_deg (*case 2*) |
189 (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d, _))) v = |
189 (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d, _))) v = |
190 if ((vv = v) andalso (TermC.coeff_in t1 v)) then SOME (TermC.int_of_str d) else NONE |
190 if vv = v andalso not (TermC.coeff_in t1 v) then SOME (TermC.int_of_str d) else NONE |
191 | factor_right_deg (Const ("Atools.pow",_) $ vv $ Free (d,_)) v = |
191 | factor_right_deg (Const ("Atools.pow",_) $ vv $ Free (d,_)) v = |
192 if (vv = v) then SOME (TermC.int_of_str d) else NONE |
192 if (vv = v) then SOME (TermC.int_of_str d) else NONE |
193 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v = |
193 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v = |
194 if ((vv = v) andalso (TermC.coeff_in t1 v)) then SOME 1 else NONE |
194 if vv = v andalso not (TermC.coeff_in t1 v) then SOME 1 else NONE |
195 | factor_right_deg vv v = |
195 | factor_right_deg vv v = |
196 if (vv = v) then SOME 1 else NONE; |
196 if (vv = v) then SOME 1 else NONE; |
197 fun mono_deg_in m v = (*case 1*) |
197 fun mono_deg_in m v = (*case 1*) |
198 if TermC.coeff_in m v then (*case 1*) SOME 0 else factor_right_deg m v; |
198 if not (TermC.coeff_in m v) then (*case 1*) SOME 0 else factor_right_deg m v; |
199 |
199 |
200 fun expand_deg_in t v = |
200 fun expand_deg_in t v = |
201 let |
201 let |
202 fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) = |
202 fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) = |
203 (case mono_deg_in t2 v of (* $ is left associative*) |
203 (case mono_deg_in t2 v of (* $ is left associative*) |
513 subsection \<open>predicates\<close> |
513 subsection \<open>predicates\<close> |
514 subsubsection \<open>in specifications\<close> |
514 subsubsection \<open>in specifications\<close> |
515 ML \<open> |
515 ML \<open> |
516 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
516 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
517 fun is_polyrat_in t v = |
517 fun is_polyrat_in t v = |
518 let |
518 let |
519 fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:") |
519 fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:") |
520 (* at the moment there is no term like this, but ....*) |
520 (* at the moment there is no term like this, but ....*) |
521 | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = |
521 | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (TermC.coeff_in b v) |
522 not(TermC.coeff_in b v) |
522 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v |
523 | finddivide (_ $ t1 $ t2) v = |
523 | finddivide (_ $ t1) v = finddivide t1 v |
524 (finddivide t1 v) orelse (finddivide t2 v) |
|
525 | finddivide (_ $ t1) v = (finddivide t1 v) |
|
526 | finddivide _ _ = false; |
524 | finddivide _ _ = false; |
527 in finddivide t v end; |
525 in finddivide t v end; |
528 |
526 |
529 fun is_expanded_in t v = |
527 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false; |
530 case expand_deg_in t v of SOME _ => true | NONE => false; |
528 fun is_poly_in t v = case poly_deg_in t v of SOME _ => true | NONE => false; |
531 fun is_poly_in t v = |
529 fun has_degree_in t v = case expand_deg_in t v of SOME d => d | NONE => ~1; |
532 case poly_deg_in t v of SOME _ => true | NONE => false; |
|
533 fun has_degree_in t v = |
|
534 case expand_deg_in t v of SOME d => d | NONE => ~1; |
|
535 |
530 |
536 (*.the expression contains + - * ^ only ? |
531 (*.the expression contains + - * ^ only ? |
537 this is weaker than 'is_polynomial' !.*) |
532 this is weaker than 'is_polynomial' !.*) |
538 fun is_polyexp (Free _) = true |
533 fun is_polyexp (Free _) = true |
539 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true |
534 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true |