1 (*Stefan K.*) |
|
2 |
|
3 (*protokoll 14.3.02 -------------------------------------------------- |
|
4 val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)"; |
|
5 val t = (term_of o the) ct; |
|
6 atomt t; |
|
7 val ct = parse thy "not (#1+a)"; (*HOL.thy ?*) |
|
8 val t = (term_of o the) ct; |
|
9 atomt t; |
|
10 val ct = parse thy "x"; (*momentan ist alles 'real'*) |
|
11 val t = (term_of o the) ct; |
|
12 atomty t; |
|
13 val ct = parse thy "(x::int)"; (* !!! *) |
|
14 val t = (term_of o the) ct; |
|
15 atomty t; |
|
16 |
|
17 val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*) |
|
18 |
|
19 val Const ("RatArith.cancel",_) $ zaehler $ nenner = t; |
|
20 ---------------------------------------------------------------------*) |
|
21 |
|
22 |
|
23 (*diese vvv funktionen kommen nach src/Isa99/term_G.sml -------------*) |
|
24 fun term2str t = |
|
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^"), "^")" |
|
31 | ato (Bound ix) n = |
|
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 _ => raise error ("free2int: "^term2str t)) |
|
39 | free2int t = raise error ("free2int: "^term2str t); |
|
40 (*diese ^^^ funktionen kommen nach src/Isa99/term_G.sml -------------*) |
|
41 |
|
42 |
|
43 (* remark on exceptions: 'error' is implemented by Isabelle |
|
44 as the typical system error *) |
|
45 |
|
46 |
|
47 type poly = int list; |
|
48 |
|
49 (* transform a Isabelle-term t into internal polynomial format |
|
50 preconditions for t: |
|
51 a-b -> a+(-b) |
|
52 x^1 -> x |
|
53 term ordered ascending |
|
54 parentheses right side (caused by 'ordered rewriting') |
|
55 variable as power (not as product) *) |
|
56 |
|
57 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = |
|
58 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly |
|
59 else raise error ("term2poly.1 "^term2str t1) |
|
60 | mono (t as Const ("op *",_) $ t1 $ |
|
61 (Const ("RatArith.pow",_) $ t2 $ t3)) v g = |
|
62 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] |
|
63 else raise error ("term2poly.2 "^term2str t) |
|
64 | mono t _ _ = raise error ("term2poly.3 "^term2str t); |
|
65 |
|
66 fun poly (Const ("op +",_) $ 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; |
|
70 |
|
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] |
|
73 handle _ => NONE) |
|
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 |
|
76 | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v = |
|
77 SOME ([(the o int_of_str) s1] @ (poly t v 1)) |
|
78 | term2poly t v = |
|
79 SOME (poly t v 0) handle _ => NONE; |
|
80 |
|
81 (*tests*) |
|
82 val v = (term_of o the o (parse thy)) "x::real"; |
|
83 val t = (term_of o the o (parse thy)) "#-1::real"; |
|
84 term2poly t v; |
|
85 val t = (term_of o the o (parse thy)) "x::real"; |
|
86 term2poly t v; |
|
87 val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*) |
|
88 term2poly t v; |
|
89 val t = (term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*) |
|
90 term2poly t v; |
|
91 val t = (term_of o the o (parse thy)) "x^^^#3"; |
|
92 term2poly t v; |
|
93 val t = (term_of o the o (parse thy)) "#3 * x^^^#3"; |
|
94 term2poly t v; |
|
95 val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3"; |
|
96 term2poly t v; |
|
97 val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)"; |
|
98 term2poly t v; |
|
99 val t = (term_of o the o (parse thy)) |
|
100 "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))"; |
|
101 term2poly t v; |
|
102 val t = (term_of o the o (parse thy)) |
|
103 "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)"; |
|
104 term2poly t v; |
|
105 |
|
106 |
|
107 fun is_polynomial_in t v = |
|
108 case term2poly t v of SOME _ => true | NONE => false; |
|
109 |
|
110 (* transform the internal polynomial p into an Isabelle term t |
|
111 where t meets the preconditions of term2poly |
|
112 val mk_mono = |
|
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 |
|
120 term |
|
121 remark: all the typs above are "RealDef.real" due to the typs of * + ^ |
|
122 which may change in the future |
|
123 *) |
|
124 fun mk_mono cT vT pT eT c v g = |
|
125 case g of |
|
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 ("op *", [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 ("op *", [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)); |
|
136 (*tests*) |
|
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; |
|
140 (cterm_of thy) t; |
|
141 val t = mk_mono cT vT pT eT ~1 "x" 0; |
|
142 (cterm_of thy) t; |
|
143 val t = mk_mono cT vT pT eT 1 "x" 1; |
|
144 (cterm_of thy) t; |
|
145 |
|
146 |
|
147 fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2; |
|
148 |
|
149 |
|
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 = |
|
152 let |
|
153 fun mk_poly cT vT pT eT [] t v g = t |
|
154 | mk_poly cT vT pT eT [p] t v g = |
|
155 if p = 0 then t |
|
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; |
|
164 |
|
165 (*tests*) |
|
166 val t = poly2term cT vT pT eT [~1] "x"; |
|
167 (cterm_of thy) t; |
|
168 val t = poly2term cT vT pT eT [0,1] "x"; |
|
169 (cterm_of thy) t; |
|
170 val t = poly2term cT vT pT eT [0,0,0,1] "x"; |
|
171 (cterm_of thy) t; |
|
172 val t = poly2term cT vT pT eT [0,0,0,3] "x"; |
|
173 (cterm_of thy) t; |
|
174 val t = poly2term cT vT pT eT [~1,0,0,3] "x"; |
|
175 (cterm_of thy) t; |
|
176 val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x"; |
|
177 (cterm_of thy) t; |
|
178 val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x"; |
|
179 (cterm_of thy) t; |
|
180 val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x"; |
|
181 (cterm_of thy) t; |
|
182 |
|
183 "***************************************************************************"; |
|
184 "* reverse-rewriting 12.8.02 *"; |
|
185 "***************************************************************************"; |
|
186 fun rewrite_set_' thy rls put_asm ruless ct = |
|
187 case ruless of |
|
188 Rrls _ => raise error "rewrite_set_' not for Rrls" |
|
189 | Rls _ => |
|
190 let |
|
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) = |
|
195 case rul of |
|
196 Thm (thmid, thm) => |
|
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 |
|
200 | SOME (ct',asm') => |
|
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') => |
|
206 let |
|
207 val pairopt = |
|
208 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
|
209 rls put_asm thm' ct; |
|
210 val _ = if pairopt <> NONE then () |
|
211 else raise 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; |
|
218 |
|
219 (* |
|
220 fun reverse_rewrite t1 t2 rls = |
|
221 *) |
|
222 fun rewrite_set_' thy rls put_asm ruless ct = |
|
223 case ruless of |
|
224 Rrls _ => raise error "rewrite_set_' not for Rrls" |
|
225 | Rls _ => |
|
226 let |
|
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) = |
|
231 case rul of |
|
232 Thm (thmid, thm) => |
|
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 |
|
236 | SOME (ct',asm') => |
|
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') => |
|
242 let |
|
243 val pairopt = |
|
244 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
|
245 rls put_asm thm' ct; |
|
246 val _ = if pairopt <> NONE then () |
|
247 else raise 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; |
|
254 |
|
255 realpow_two; |
|
256 real_mult_div_cancel1; |
|
257 |
|