equal
deleted
inserted
replaced
93 (*asm false .. thm not applied ^^^; continue until False vvv*) |
93 (*asm false .. thm not applied ^^^; continue until False vvv*) |
94 else chk (indets @ [t] @ a') asms); |
94 else chk (indets @ [t] @ a') asms); |
95 in chk [] asms end |
95 in chk [] asms end |
96 (* rewrite with a rule set, which must not be the empty Erls *) |
96 (* rewrite with a rule set, which must not be the empty Erls *) |
97 and rewrite__set_ _ _ __ Erls t = |
97 and rewrite__set_ _ _ __ Erls t = |
98 raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'") |
98 error("rewrite__set_ called with 'Erls' for '"^term2str t^"'") |
99 (* rewrite with a 'reverse rule set' based on ML code *) |
99 (* rewrite with a 'reverse rule set' based on ML code *) |
100 | rewrite__set_ thy i _ _ (rrls as Rrls _) t = |
100 | rewrite__set_ thy i _ _ (rrls as Rrls _) t = |
101 let val _= if ! trace_rewrite andalso i < ! depth |
101 let val _= if ! trace_rewrite andalso i < ! depth |
102 then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^ |
102 then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^ |
103 (term2str t)) else () |
103 (term2str t)) else () |
139 let |
139 let |
140 val pairopt = |
140 val pairopt = |
141 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
141 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
142 ((#erls o rep_rls) rls) put_asm thm' ct; |
142 ((#erls o rep_rls) rls) put_asm thm' ct; |
143 val _ = if pairopt <> NONE then () |
143 val _ = if pairopt <> NONE then () |
144 else raise error("rewrite_set_, rewrite_ \""^ |
144 else error("rewrite_set_, rewrite_ \""^ |
145 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
145 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
146 val _ = if ! trace_rewrite andalso i < ! depth |
146 val _ = if ! trace_rewrite andalso i < ! depth |
147 then tracing((idt"="(i+1))^" calc. to: "^ |
147 then tracing((idt"="(i+1))^" calc. to: "^ |
148 (term2str ((fst o the) pairopt))) |
148 (term2str ((fst o the) pairopt))) |
149 else() |
149 else() |
159 let |
159 let |
160 val pairopt = |
160 val pairopt = |
161 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
161 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
162 ((#erls o rep_rls) rls) put_asm thm' ct; |
162 ((#erls o rep_rls) rls) put_asm thm' ct; |
163 val _ = if pairopt <> NONE then () |
163 val _ = if pairopt <> NONE then () |
164 else raise error("rewrite_set_, rewrite_ \""^ |
164 else error("rewrite_set_, rewrite_ \""^ |
165 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
165 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
166 val _ = if ! trace_rewrite andalso i < ! depth |
166 val _ = if ! trace_rewrite andalso i < ! depth |
167 then tracing((idt"="(i+1))^" cal1. to: "^ |
167 then tracing((idt"="(i+1))^" cal1. to: "^ |
168 (term2str ((fst o the) pairopt))) |
168 (term2str ((fst o the) pairopt))) |
169 else() |
169 else() |
331 |
331 |
332 |
332 |
333 |
333 |
334 |
334 |
335 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs')) |
335 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs')) |
336 handle _ => raise error ("get_rls_scr: no script for "^rs'); |
336 handle _ => error ("get_rls_scr: no script for "^rs'); |
337 |
337 |
338 |
338 |
339 (*make_thm added to Pure/thm.ML*) |
339 (*make_thm added to Pure/thm.ML*) |
340 fun mk_thm thy str = |
340 fun mk_thm thy str = |
341 let val t = (term_of o the o (parse thy)) str |
341 let val t = (term_of o the o (parse thy)) str |
413 | id => |
413 | id => |
414 if hd id = "#" |
414 if hd id = "#" |
415 then mk_thm thy ct' |
415 then mk_thm thy ct' |
416 else (num_str o (PureThy.get_thm thy)) thmid |
416 else (num_str o (PureThy.get_thm thy)) thmid |
417 ) handle _ => |
417 ) handle _ => |
418 raise error ("assoc_thm': '"^thmid^"' not in '"^ |
418 error ("assoc_thm': '"^thmid^"' not in '"^ |
419 (theory2domID thy)^"' (and parents)"); |
419 (theory2domID thy)^"' (and parents)"); |
420 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); |
420 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); |
421 val it = "6 = 2 * 3" : thm |
421 val it = "6 = 2 * 3" : thm |
422 |
422 |
423 > assoc_thm' Isac.thy ("add_0_left",""); |
423 > assoc_thm' Isac.thy ("add_0_left",""); |