[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: 2 Questions
Bettina,
unfortunately, I can't help you with your first question concerning TCC
generation, but I give a try on your second one:
> 2. A more basic technical problem: I would like to replace a single
> occurrence of a term in a formula that contains multiple occurrences of
> the term. I couldn't find a way of using expand, rewrite or replace for
> this.
> More concrete:
> I have a lemma l = r and a formula f (g(l), h(l))
> and I would like to replace only the occurrence of l in "g(l)"
> with r.
It would indeed be nice to have an 'occurrence' option for rewrite and replace
as in expand. The only way I know of to simulate this is to "hide" the
occurrences that should stay unchanged:
(NAME-REPLACE "hl" "h(l)")
(REWRITE "lemma")
(REVEAL -1)
(REPLACE -1 :DIR RL)
(DELETE -1)
Obviously, this approach is unacceptable if there are n occurrences out of m
to be replaced.
Best regards,
- Holger
--
-----------------------------------------------------------------------------
Holger Pfeifer Tel.: (+49) 731 / 502-4117
Abteilung KI Fax: (+49) 731 / 502-4119
Universität Ulm
D-89069 Ulm e-mail: pfeifer@ki.informatik.uni-ulm.de
-----------------------------------------------------------------------------