536 else false |
536 else false |
537 | bin_ops_only t = |
537 | bin_ops_only t = |
538 if atom t then true else bin_ops_only t; |
538 if atom t then true else bin_ops_only t; |
539 |
539 |
540 fun polynomial opl t bdVar = (* bdVar TODO *) |
540 fun polynomial opl t bdVar = (* bdVar TODO *) |
541 (bin_op t) subset opl andalso (bin_ops_only t); |
541 subset op = (bin_op t, opl) andalso (bin_ops_only t); |
542 |
542 |
543 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) |
543 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) |
544 andalso polynomial opl (equ_lhs t) bdVar |
544 andalso polynomial opl (equ_lhs t) bdVar |
545 andalso polynomial opl (equ_rhs t) bdVar |
545 andalso polynomial opl (equ_rhs t) bdVar |
546 andalso ((varids bdVar) subset (varids (equ_lhs t)) |
546 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse |
547 orelse(varids bdVar) subset (varids (equ_lhs t))); |
547 subset op = (varids bdVar, varids (equ_lhs t))); |
548 |
548 |
549 (*fun max is = |
549 (*fun max is = |
550 let fun max_ m [] = m |
550 let fun max_ m [] = m |
551 | max_ m (i::is) = if m<i then max_ i is else max_ m is; |
551 | max_ m (i::is) = if m<i then max_ i is else max_ m is; |
552 in max_ (hd is) is end; |
552 in max_ (hd is) is end; |
561 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0 |
561 | deg _ _ v (Free (s,Type (_,[]))) = if v=strip_thy s then 1 else 0 |
562 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0 |
562 | deg _ _ v (Var((s,_),Type (_,[]))) = if v=strip_thy s then 1 else 0 |
563 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *) |
563 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *) |
564 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 |
564 | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 |
565 | deg addl mul v (h $ t1 $ t2) = |
565 | deg addl mul v (h $ t1 $ t2) = |
566 if(bin_op h)subset addl |
566 if subset op = (bin_op h, addl) |
567 then max (deg addl mul v t1 ,deg addl mul v t2) |
567 then max (deg addl mul v t1 ,deg addl mul v t2) |
568 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2) |
568 else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2) |
569 in if polynomial (addl @ [mul]) t bdVar |
569 in if polynomial (addl @ [mul]) t bdVar |
570 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option) |
570 then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option) |
571 end; |
571 end; |