[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
-----------------------------------------------------------------------------