33 | ato (Abs(a,T,body)) n = |
33 | ato (Abs(a,T,body)) n = |
34 "\n"^indent n^"Abs( "^a^",.."^ato body (n+1) |
34 "\n"^indent n^"Abs( "^a^",.."^ato body (n+1) |
35 | ato (f$t') n = ato f n^ato t' (n+1) |
35 | ato (f$t') n = ato f n^ato t' (n+1) |
36 in "\n-------------"^ato t 0^"\n" end; |
36 in "\n-------------"^ato t 0^"\n" end; |
37 fun free2int (t as Free (s, _)) = (((the o int_of_str) s) |
37 fun free2int (t as Free (s, _)) = (((the o int_of_str) s) |
38 handle _ => error ("free2int: "^term2str t)) |
38 handle _ => error ("free2int: "^Celem.term2str t)) |
39 | free2int t = error ("free2int: "^term2str t); |
39 | free2int t = error ("free2int: "^Celem.term2str t); |
40 (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*) |
40 (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*) |
41 |
41 |
42 |
42 |
43 (* remark on exceptions: 'error' is implemented by Isabelle |
43 (* remark on exceptions: 'error' is implemented by Isabelle |
44 as the typical system error *) |
44 as the typical system error *) |
54 parentheses right side (caused by 'ordered rewriting') |
54 parentheses right side (caused by 'ordered rewriting') |
55 variable as power (not as product) *) |
55 variable as power (not as product) *) |
56 |
56 |
57 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = |
57 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = |
58 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly |
58 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly |
59 else error ("term2poly.1 "^term2str t1) |
59 else error ("term2poly.1 "^Celem.term2str t1) |
60 | mono (t as Const ("Groups.times_class.times",_) $ t1 $ |
60 | mono (t as Const ("Groups.times_class.times",_) $ t1 $ |
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 error ("term2poly.2 "^term2str t) |
63 else error ("term2poly.2 "^Celem.term2str t) |
64 | mono t _ _ = error ("term2poly.3 "^term2str t); |
64 | mono t _ _ = error ("term2poly.3 "^Celem.term2str t); |
65 |
65 |
66 fun poly (Const ("Groups.plus_class.plus",_) $ 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; |
183 "***************************************************************************"; |
183 "***************************************************************************"; |
184 "* reverse-rewriting 12.8.02 *"; |
184 "* reverse-rewriting 12.8.02 *"; |
185 "***************************************************************************"; |
185 "***************************************************************************"; |
186 fun rewrite_set_' thy rls put_asm ruless ct = |
186 fun rewrite_set_' thy rls put_asm ruless ct = |
187 case ruless of |
187 case ruless of |
188 Rrls _ => error "rewrite_set_' not for Rrls" |
188 Celem.Rrls _ => error "rewrite_set_' not for Celem.Rrls" |
189 | Rls _ => |
189 | Celem.Rls _ => |
190 let |
190 let |
191 datatype switch = Appl | Noap; |
191 datatype switch = Appl | Noap; |
192 fun rew_once ruls asm ct Noap [] = (ct,asm) |
192 fun rew_once ruls asm ct Noap [] = (ct,asm) |
193 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls |
193 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls |
194 | rew_once ruls asm ct apno (rul::thms) = |
194 | rew_once ruls asm ct apno (rul::thms) = |
195 case rul of |
195 case rul of |
196 Thm (thmid, thm) => |
196 Celem.Thm (thmid, thm) => |
197 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
197 (case rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) |
198 rls put_asm (thm_of_thm rul) ct of |
198 rls put_asm (Celem.thm_of_thm rul) ct of |
199 NONE => rew_once ruls asm ct apno thms |
199 NONE => rew_once ruls asm ct apno thms |
200 | SOME (ct',asm') => |
200 | SOME (ct',asm') => |
201 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
201 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
202 | Calc (cc as (op_,_)) => |
202 | Celem.Calc (cc as (op_,_)) => |
203 (case adhoc_thm thy cc ct of |
203 (case adhoc_thm thy cc ct of |
204 NONE => rew_once ruls asm ct apno thms |
204 NONE => rew_once ruls asm ct apno thms |
205 | SOME (thmid, thm') => |
205 | SOME (thmid, thm') => |
206 let |
206 let |
207 val pairopt = |
207 val pairopt = |
208 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
208 rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) |
209 rls put_asm thm' ct; |
209 rls put_asm thm' ct; |
210 val _ = if pairopt <> NONE then () |
210 val _ = if pairopt <> NONE then () |
211 else error("rewrite_set_, rewrite_ \""^ |
211 else error("rewrite_set_, rewrite_ \""^ |
212 (string_of_thmI thm')^"\" \""^ |
212 (string_of_thmI thm')^"\" \""^ |
213 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE") |
213 (Syntax.string_of_term (Celem.thy2ctxt thy) ct)^"\" = NONE") |
214 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
214 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
215 val ruls = (#rules o rep_rls) ruless; |
215 val ruls = (#rules o Celem.rep_rls) ruless; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
217 in if ct = ct' then NONE else SOME (ct',asm') end; |
217 in if ct = ct' then NONE else SOME (ct',asm') end; |
218 |
218 |
219 (* |
219 (* |
220 fun reverse_rewrite t1 t2 rls = |
220 fun reverse_rewrite t1 t2 rls = |
221 *) |
221 *) |
222 fun rewrite_set_' thy rls put_asm ruless ct = |
222 fun rewrite_set_' thy rls put_asm ruless ct = |
223 case ruless of |
223 case ruless of |
224 Rrls _ => error "rewrite_set_' not for Rrls" |
224 Celem.Rrls _ => error "rewrite_set_' not for Celem.Rrls" |
225 | Rls _ => |
225 | Celem.Rls _ => |
226 let |
226 let |
227 datatype switch = Appl | Noap; |
227 datatype switch = Appl | Noap; |
228 fun rew_once ruls asm ct Noap [] = (ct,asm) |
228 fun rew_once ruls asm ct Noap [] = (ct,asm) |
229 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls |
229 | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls |
230 | rew_once ruls asm ct apno (rul::thms) = |
230 | rew_once ruls asm ct apno (rul::thms) = |
231 case rul of |
231 case rul of |
232 Thm (thmid, thm) => |
232 Celem.Thm (thmid, thm) => |
233 (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
233 (case rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) |
234 rls put_asm (thm_of_thm rul) ct of |
234 rls put_asm (Celem.thm_of_thm rul) ct of |
235 NONE => rew_once ruls asm ct apno thms |
235 NONE => rew_once ruls asm ct apno thms |
236 | SOME (ct',asm') => |
236 | SOME (ct',asm') => |
237 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
237 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
238 | Calc (cc as (op_,_)) => |
238 | Celem.Calc (cc as (op_,_)) => |
239 (case adhoc_thm thy cc ct of |
239 (case adhoc_thm thy cc ct of |
240 NONE => rew_once ruls asm ct apno thms |
240 NONE => rew_once ruls asm ct apno thms |
241 | SOME (thmid, thm') => |
241 | SOME (thmid, thm') => |
242 let |
242 let |
243 val pairopt = |
243 val pairopt = |
244 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
244 rewrite_ thy ((snd o #rew_ord o Celem.rep_rls) ruless) |
245 rls put_asm thm' ct; |
245 rls put_asm thm' ct; |
246 val _ = if pairopt <> NONE then () |
246 val _ = if pairopt <> NONE then () |
247 else error("rewrite_set_, rewrite_ \""^ |
247 else error("rewrite_set_, rewrite_ \""^ |
248 (string_of_thmI thm')^"\" \""^ |
248 (string_of_thmI thm')^"\" \""^ |
249 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE") |
249 (Syntax.string_of_term (Celem.thy2ctxt thy) ct)^"\" = NONE") |
250 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
250 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
251 val ruls = (#rules o rep_rls) ruless; |
251 val ruls = (#rules o Celem.rep_rls) ruless; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
253 in if ct = ct' then NONE else SOME (ct',asm') end; |
253 in if ct = ct' then NONE else SOME (ct',asm') end; |
254 |
254 |
255 realpow_two; |
255 realpow_two; |
256 real_mult_div_cancel1; |
256 real_mult_div_cancel1; |