61 (Const ("RatArith.pow",_) $ t2 $ t3)) v g = |
61 (Const ("RatArith.pow",_) $ t2 $ t3)) v g = |
62 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] |
62 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] |
63 else raise error ("term2poly.2 "^term2str t) |
63 else raise error ("term2poly.2 "^term2str t) |
64 | mono t _ _ = raise error ("term2poly.3 "^term2str t); |
64 | mono t _ _ = raise error ("term2poly.3 "^term2str t); |
65 |
65 |
66 fun poly (Const ("op +",_) $ t1 $ t2) v g = |
66 fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = |
67 let val l = mono t1 v g |
67 let val l = mono t1 v g |
68 in (l @ (poly t2 v ((length l) + g))) end |
68 in (l @ (poly t2 v ((length l) + g))) end |
69 | poly t v g = mono t v g; |
69 | poly t v g = mono t v g; |
70 |
70 |
71 fun term2poly (t as Free (s, _)) v = |
71 fun term2poly (t as Free (s, _)) v = |
72 if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s] |
72 if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s] |
73 handle _ => NONE) |
73 handle _ => NONE) |
74 | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = |
74 | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = |
75 if t = v then SOME [0, (the o int_of_str) s1] else NONE |
75 if t = v then SOME [0, (the o int_of_str) s1] else NONE |
76 | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v = |
76 | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = |
77 SOME ([(the o int_of_str) s1] @ (poly t v 1)) |
77 SOME ([(the o int_of_str) s1] @ (poly t v 1)) |
78 | term2poly t v = |
78 | term2poly t v = |
79 SOME (poly t v 0) handle _ => NONE; |
79 SOME (poly t v 0) handle _ => NONE; |
80 |
80 |
81 (*tests*) |
81 (*tests*) |
142 (cterm_of thy) t; |
142 (cterm_of thy) t; |
143 val t = mk_mono cT vT pT eT 1 "x" 1; |
143 val t = mk_mono cT vT pT eT 1 "x" 1; |
144 (cterm_of thy) t; |
144 (cterm_of thy) t; |
145 |
145 |
146 |
146 |
147 fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2; |
147 fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2; |
148 |
148 |
149 |
149 |
150 fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0 |
150 fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0 |
151 | poly2term cT vT pT eT (p:poly) v = |
151 | poly2term cT vT pT eT (p:poly) v = |
152 let |
152 let |