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 _ => raise error ("free2int: "^term2str t)) |
38 handle _ => error ("free2int: "^term2str t)) |
39 | free2int t = raise error ("free2int: "^term2str t); |
39 | free2int t = error ("free2int: "^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 raise error ("term2poly.1 "^term2str t1) |
59 else error ("term2poly.1 "^term2str t1) |
60 | mono (t as Const ("op *",_) $ t1 $ |
60 | mono (t as Const ("op *",_) $ 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 raise error ("term2poly.2 "^term2str t) |
63 else error ("term2poly.2 "^term2str t) |
64 | mono t _ _ = raise error ("term2poly.3 "^term2str t); |
64 | mono t _ _ = error ("term2poly.3 "^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 _ => raise error "rewrite_set_' not for Rrls" |
188 Rrls _ => error "rewrite_set_' not for Rrls" |
189 | Rls _ => |
189 | 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 |
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 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 raise 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 (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 rep_rls) ruless; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
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 _ => raise error "rewrite_set_' not for Rrls" |
224 Rrls _ => error "rewrite_set_' not for Rrls" |
225 | Rls _ => |
225 | 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 |
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 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 raise 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 (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 rep_rls) ruless; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |