3 (*protokoll 14.3.02 --------------------------------------------------
4 val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";
5 val t = (term_of o the) ct;
7 val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)
8 val t = (term_of o the) ct;
10 val ct = parse thy "x"; (*momentan ist alles 'real'*)
11 val t = (term_of o the) ct;
13 val ct = parse thy "(x::int)"; (* !!! *)
14 val t = (term_of o the) ct;
17 val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)
19 val Const ("RatArith.cancel",_) $ zaehler $ nenner = t;
20 ---------------------------------------------------------------------*)
23 (*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*)
25 let fun ato (Const(a,T)) n =
26 "\n"^indent n^"Const ( "^a^")"
27 | ato (Free (a,T)) n =
28 "\n"^indent n^"Free ( "^a^", "^")"
29 | ato (Var ((a,ix),T)) n =
30 "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"
32 "\n"^indent n^"Bound "^string_of_int ix
33 | ato (Abs(a,T,body)) n =
34 "\n"^indent n^"Abs( "^a^",.."^ato body (n+1)
35 | ato (f$t') n = ato f n^ato t' (n+1)
36 in "\n-------------"^ato t 0^"\n" end;
37 fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
38 handle _ => error ("free2int: "^term2str t))
39 | free2int t = error ("free2int: "^term2str t);
40 (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)
43 (* remark on exceptions: 'error' is implemented by Isabelle
44 as the typical system error *)
49 (* transform a Isabelle-term t into internal polynomial format
53 term ordered ascending
54 parentheses right side (caused by 'ordered rewriting')
55 variable as power (not as product) *)
57 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
58 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
59 else error ("term2poly.1 "^term2str t1)
60 | mono (t as Const ("Groups.times_class.times",_) $ t1 $
61 (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
62 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
63 else error ("term2poly.2 "^term2str t)
64 | mono t _ _ = error ("term2poly.3 "^term2str t);
66 fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g =
67 let val l = mono t1 v g
68 in (l @ (poly t2 v ((length l) + g))) end
69 | poly t v g = mono t v g;
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]
74 | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
75 if t = v then SOME [0, (the o int_of_str) s1] else NONE
76 | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
77 SOME ([(the o int_of_str) s1] @ (poly t v 1))
79 SOME (poly t v 0) handle _ => NONE;
82 val v = (term_of o the o (parse thy)) "x::real";
83 val t = (term_of o the o (parse thy)) "#-1::real";
85 val t = (term_of o the o (parse thy)) "x::real";
87 val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
89 val t = (term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
91 val t = (term_of o the o (parse thy)) "x^^^#3";
93 val t = (term_of o the o (parse thy)) "#3 * x^^^#3";
95 val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
97 val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
99 val t = (term_of o the o (parse thy))
100 "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";
102 val t = (term_of o the o (parse thy))
103 "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";
107 fun is_polynomial_in t v =
108 case term2poly t v of SOME _ => true | NONE => false;
110 (* transform the internal polynomial p into an Isabelle term t
111 where t meets the preconditions of term2poly
113 fn : typ -> of the coefficients
114 typ -> of the unknown
115 typ -> of the monomial and polynomial
116 typ -> of the exponent of the unknown
117 int -> the coefficient <> 0
118 string -> the unknown
119 int -> the degree, i.e. the value of the exponent
121 remark: all the typs above are "RealDef.real" due to the typs of * + ^
122 which may change in the future
124 fun mk_mono cT vT pT eT c v g =
126 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
127 | 1 => if c = 1 then Free (v, vT)
128 else Const ("Groups.times_class.times", [cT, vT]--->pT) $
129 Free (str_of_int c, cT) $ Free (v, vT)
130 | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
131 Free (v, vT) $ Free (str_of_int g, eT))
132 else Const ("Groups.times_class.times", [cT, vT]--->pT) $
133 Free (str_of_int c, cT) $
134 (Const ("RatArith.pow", [vT, eT]--->pT) $
135 Free (v, vT) $ Free (str_of_int g, eT));
137 val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
138 val eT = HOLogic.realT;
139 val t = mk_mono cT vT pT eT ~5 "x" 5;
141 val t = mk_mono cT vT pT eT ~1 "x" 0;
143 val t = mk_mono cT vT pT eT 1 "x" 1;
147 fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
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 =
153 fun mk_poly cT vT pT eT [] t v g = t
154 | mk_poly cT vT pT eT [p] t v g =
156 else mk_sum pT (mk_mono cT vT pT eT p v g) t
157 | mk_poly cT vT pT eT (p::ps) t v g =
158 if p = 0 then mk_poly cT vT pT eT ps t v (g-1)
159 else mk_poly cT vT pT eT ps
160 (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1)
161 val (p'::ps') = rev p
162 val g = (length p) - 1
163 in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end;
166 val t = poly2term cT vT pT eT [~1] "x";
168 val t = poly2term cT vT pT eT [0,1] "x";
170 val t = poly2term cT vT pT eT [0,0,0,1] "x";
172 val t = poly2term cT vT pT eT [0,0,0,3] "x";
174 val t = poly2term cT vT pT eT [~1,0,0,3] "x";
176 val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
178 val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
180 val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
183 "***************************************************************************";
184 "* reverse-rewriting 12.8.02 *";
185 "***************************************************************************";
186 fun rewrite_set_' thy rls put_asm ruless ct =
188 Rrls _ => error "rewrite_set_' not for Rrls"
191 datatype switch = Appl | Noap;
192 fun rew_once ruls asm ct Noap [] = (ct,asm)
193 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
194 | rew_once ruls asm ct apno (rul::thms) =
197 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
198 rls put_asm (thm_of_thm rul) ct of
199 NONE => rew_once ruls asm ct apno thms
201 rew_once ruls (asm union asm') ct' Appl (rul::thms))
202 | Calc (cc as (op_,_)) =>
203 (case get_calculation_ thy cc ct of
204 NONE => rew_once ruls asm ct apno thms
205 | SOME (thmid, thm') =>
208 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
210 val _ = if pairopt <> NONE then ()
211 else error("rewrite_set_, rewrite_ \""^
212 (string_of_thmI thm')^"\" \""^
213 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
214 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
215 val ruls = (#rules o rep_rls) ruless;
216 val (ct',asm') = rew_once ruls [] ct Noap ruls;
217 in if ct = ct' then NONE else SOME (ct',asm') end;
220 fun reverse_rewrite t1 t2 rls =
222 fun rewrite_set_' thy rls put_asm ruless ct =
224 Rrls _ => error "rewrite_set_' not for Rrls"
227 datatype switch = Appl | Noap;
228 fun rew_once ruls asm ct Noap [] = (ct,asm)
229 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
230 | rew_once ruls asm ct apno (rul::thms) =
233 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
234 rls put_asm (thm_of_thm rul) ct of
235 NONE => rew_once ruls asm ct apno thms
237 rew_once ruls (asm union asm') ct' Appl (rul::thms))
238 | Calc (cc as (op_,_)) =>
239 (case get_calculation_ thy cc ct of
240 NONE => rew_once ruls asm ct apno thms
241 | SOME (thmid, thm') =>
244 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
246 val _ = if pairopt <> NONE then ()
247 else error("rewrite_set_, rewrite_ \""^
248 (string_of_thmI thm')^"\" \""^
249 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
250 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
251 val ruls = (#rules o rep_rls) ruless;
252 val (ct',asm') = rew_once ruls [] ct Noap ruls;
253 in if ct = ct' then NONE else SOME (ct',asm') end;
256 real_mult_div_cancel1;