neuper@37906: (*Stefan K.*) neuper@37906: neuper@37906: (*protokoll 14.3.02 -------------------------------------------------- neuper@37906: val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)"; wneuper@59186: val t = (Thm.term_of o the) ct; neuper@37906: atomt t; neuper@37906: val ct = parse thy "not (#1+a)"; (*HOL.thy ?*) wneuper@59186: val t = (Thm.term_of o the) ct; neuper@37906: atomt t; neuper@37906: val ct = parse thy "x"; (*momentan ist alles 'real'*) wneuper@59186: val t = (Thm.term_of o the) ct; neuper@37906: atomty t; neuper@37906: val ct = parse thy "(x::int)"; (* !!! *) wneuper@59186: val t = (Thm.term_of o the) ct; neuper@37906: atomty t; neuper@37906: neuper@37906: val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*) neuper@37906: neuper@37906: val Const ("RatArith.cancel",_) $ zaehler $ nenner = t; neuper@37906: ---------------------------------------------------------------------*) neuper@37906: neuper@37906: neuper@38025: (*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*) wneuper@59406: fun Celem.term2str t = neuper@37906: let fun ato (Const(a,T)) n = neuper@37906: "\n"^indent n^"Const ( "^a^")" neuper@37906: | ato (Free (a,T)) n = neuper@37906: "\n"^indent n^"Free ( "^a^", "^")" neuper@37906: | ato (Var ((a,ix),T)) n = neuper@37906: "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")" neuper@37906: | ato (Bound ix) n = neuper@37906: "\n"^indent n^"Bound "^string_of_int ix neuper@37906: | ato (Abs(a,T,body)) n = neuper@37906: "\n"^indent n^"Abs( "^a^",.."^ato body (n+1) neuper@37906: | ato (f$t') n = ato f n^ato t' (n+1) neuper@37906: in "\n-------------"^ato t 0^"\n" end; neuper@37906: fun free2int (t as Free (s, _)) = (((the o int_of_str) s) wneuper@59406: handle _ => error ("free2int: "^Celem.term2str t)) wneuper@59406: | free2int t = error ("free2int: "^Celem.term2str t); neuper@38025: (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*) neuper@37906: neuper@37906: neuper@37906: (* remark on exceptions: 'error' is implemented by Isabelle neuper@37906: as the typical system error *) neuper@37906: neuper@37906: neuper@37906: type poly = int list; neuper@37906: neuper@37906: (* transform a Isabelle-term t into internal polynomial format neuper@37906: preconditions for t: neuper@37906: a-b -> a+(-b) neuper@37906: x^1 -> x neuper@37906: term ordered ascending neuper@37906: parentheses right side (caused by 'ordered rewriting') neuper@37906: variable as power (not as product) *) neuper@37906: neuper@37906: fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = neuper@37906: if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly wneuper@59406: else error ("term2poly.1 "^Celem.term2str t1) neuper@38034: | mono (t as Const ("Groups.times_class.times",_) $ t1 $ neuper@37906: (Const ("RatArith.pow",_) $ t2 $ t3)) v g = neuper@37906: if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] wneuper@59406: else error ("term2poly.2 "^Celem.term2str t) wneuper@59406: | mono t _ _ = error ("term2poly.3 "^Celem.term2str t); neuper@37906: neuper@38014: fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = neuper@37906: let val l = mono t1 v g neuper@37906: in (l @ (poly t2 v ((length l) + g))) end neuper@37906: | poly t v g = mono t v g; neuper@37906: neuper@37906: fun term2poly (t as Free (s, _)) v = neuper@37926: if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s] neuper@37926: handle _ => NONE) neuper@38034: | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = neuper@37926: if t = v then SOME [0, (the o int_of_str) s1] else NONE neuper@38014: | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = neuper@37926: SOME ([(the o int_of_str) s1] @ (poly t v 1)) neuper@37906: | term2poly t v = neuper@37926: SOME (poly t v 0) handle _ => NONE; neuper@37906: neuper@37906: (*tests*) wneuper@59186: val v = (Thm.term_of o the o (parse thy)) "x::real"; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "#-1::real"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "x::real"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*) neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*) neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "x^^^#3"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "#3 * x^^^#3"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x^^^#3"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) neuper@37906: "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))"; neuper@37906: term2poly t v; wneuper@59186: val t = (Thm.term_of o the o (parse thy)) neuper@37906: "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)"; neuper@37906: term2poly t v; neuper@37906: neuper@37906: neuper@37906: fun is_polynomial_in t v = neuper@37926: case term2poly t v of SOME _ => true | NONE => false; neuper@37906: neuper@37906: (* transform the internal polynomial p into an Isabelle term t neuper@37906: where t meets the preconditions of term2poly neuper@37906: val mk_mono = neuper@37906: fn : typ -> of the coefficients neuper@37906: typ -> of the unknown neuper@37906: typ -> of the monomial and polynomial neuper@37906: typ -> of the exponent of the unknown neuper@37906: int -> the coefficient <> 0 neuper@37906: string -> the unknown neuper@37906: int -> the degree, i.e. the value of the exponent neuper@37906: term neuper@37906: remark: all the typs above are "RealDef.real" due to the typs of * + ^ neuper@37906: which may change in the future neuper@37906: *) neuper@37906: fun mk_mono cT vT pT eT c v g = neuper@37906: case g of neuper@37906: 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*) neuper@37906: | 1 => if c = 1 then Free (v, vT) neuper@38034: else Const ("Groups.times_class.times", [cT, vT]--->pT) $ neuper@37906: Free (str_of_int c, cT) $ Free (v, vT) neuper@37906: | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $ neuper@37906: Free (v, vT) $ Free (str_of_int g, eT)) neuper@38034: else Const ("Groups.times_class.times", [cT, vT]--->pT) $ neuper@37906: Free (str_of_int c, cT) $ neuper@37906: (Const ("RatArith.pow", [vT, eT]--->pT) $ neuper@37906: Free (v, vT) $ Free (str_of_int g, eT)); neuper@37906: (*tests*) neuper@37906: val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT; neuper@37906: val eT = HOLogic.realT; neuper@37906: val t = mk_mono cT vT pT eT ~5 "x" 5; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = mk_mono cT vT pT eT ~1 "x" 0; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = mk_mono cT vT pT eT 1 "x" 1; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: neuper@37906: neuper@38014: fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2; neuper@37906: neuper@37906: neuper@37906: fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0 neuper@37906: | poly2term cT vT pT eT (p:poly) v = neuper@37906: let neuper@37906: fun mk_poly cT vT pT eT [] t v g = t neuper@37906: | mk_poly cT vT pT eT [p] t v g = neuper@37906: if p = 0 then t neuper@37906: else mk_sum pT (mk_mono cT vT pT eT p v g) t neuper@37906: | mk_poly cT vT pT eT (p::ps) t v g = neuper@37906: if p = 0 then mk_poly cT vT pT eT ps t v (g-1) neuper@37906: else mk_poly cT vT pT eT ps neuper@37906: (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1) neuper@37906: val (p'::ps') = rev p neuper@37906: val g = (length p) - 1 neuper@37906: in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end; neuper@37906: neuper@37906: (*tests*) neuper@37906: val t = poly2term cT vT pT eT [~1] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [0,1] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [0,0,0,1] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [0,0,0,3] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [~1,0,0,3] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x"; wneuper@59184: (Thm.global_cterm_of thy) t; neuper@37906: neuper@37906: "***************************************************************************"; neuper@37906: "* reverse-rewriting 12.8.02 *"; neuper@37906: "***************************************************************************"; neuper@37906: fun rewrite_set_' thy rls put_asm ruless ct = neuper@37906: case ruless of wneuper@59406: Celem.Rrls _ => error "rewrite_set_' not for Celem.Rrls" wneuper@59406: | Celem.Rls _ => neuper@37906: let neuper@37906: datatype switch = Appl | Noap; neuper@37906: fun rew_once ruls asm ct Noap [] = (ct,asm) neuper@37906: | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls neuper@37906: | rew_once ruls asm ct apno (rul::thms) = neuper@37906: case rul of wneuper@59406: Celem.Thm (thmid, thm) => wneuper@59406: (case rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) wneuper@59406: rls put_asm (Celem.thm_of_thm rul) ct of neuper@37926: NONE => rew_once ruls asm ct apno thms neuper@37926: | SOME (ct',asm') => neuper@37906: rew_once ruls (asm union asm') ct' Appl (rul::thms)) wneuper@59406: | Celem.Calc (cc as (op_,_)) => wneuper@59255: (case adhoc_thm thy cc ct of neuper@37926: NONE => rew_once ruls asm ct apno thms neuper@37926: | SOME (thmid, thm') => neuper@37906: let neuper@37906: val pairopt = wneuper@59406: rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) neuper@37906: rls put_asm thm' ct; neuper@37926: val _ = if pairopt <> NONE then () neuper@38031: else error("rewrite_set_, rewrite_ \""^ neuper@37906: (string_of_thmI thm')^"\" \""^ wneuper@59406: (Syntax.string_of_term (Celem.thy2ctxt thy) ct)^"\" = NONE") neuper@37906: in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); wneuper@59406: val ruls = (#rules o Celem.rep_rls) ruless; neuper@37906: val (ct',asm') = rew_once ruls [] ct Noap ruls; neuper@37926: in if ct = ct' then NONE else SOME (ct',asm') end; neuper@37906: neuper@37906: (* neuper@37906: fun reverse_rewrite t1 t2 rls = neuper@37906: *) neuper@37906: fun rewrite_set_' thy rls put_asm ruless ct = neuper@37906: case ruless of wneuper@59406: Celem.Rrls _ => error "rewrite_set_' not for Celem.Rrls" wneuper@59406: | Celem.Rls _ => neuper@37906: let neuper@37906: datatype switch = Appl | Noap; neuper@37906: fun rew_once ruls asm ct Noap [] = (ct,asm) neuper@37906: | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls neuper@37906: | rew_once ruls asm ct apno (rul::thms) = neuper@37906: case rul of wneuper@59406: Celem.Thm (thmid, thm) => wneuper@59406: (case rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) wneuper@59406: rls put_asm (Celem.thm_of_thm rul) ct of neuper@37926: NONE => rew_once ruls asm ct apno thms neuper@37926: | SOME (ct',asm') => neuper@37906: rew_once ruls (asm union asm') ct' Appl (rul::thms)) wneuper@59406: | Celem.Calc (cc as (op_,_)) => wneuper@59255: (case adhoc_thm thy cc ct of neuper@37926: NONE => rew_once ruls asm ct apno thms neuper@37926: | SOME (thmid, thm') => neuper@37906: let neuper@37906: val pairopt = wneuper@59406: rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) neuper@37906: rls put_asm thm' ct; neuper@37926: val _ = if pairopt <> NONE then () neuper@38031: else error("rewrite_set_, rewrite_ \""^ neuper@37906: (string_of_thmI thm')^"\" \""^ wneuper@59406: (Syntax.string_of_term (Celem.thy2ctxt thy) ct)^"\" = NONE") neuper@37906: in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); wneuper@59406: val ruls = (#rules o Celem.rep_rls) ruless; neuper@37906: val (ct',asm') = rew_once ruls [] ct Noap ruls; neuper@37926: in if ct = ct' then NONE else SOME (ct',asm') end; neuper@37906: neuper@37906: realpow_two; neuper@37906: real_mult_div_cancel1; neuper@37906: