rewriting lemmas

[Marcelo Glusman <marce@cs.technion.ac.il>]

Hello,
I have a theory with proven lemmas with the forms:
1)
 my_lemma : LEMMA 
     something IMPLIES this OR that

and 
2)
 my_lemma : LEMMA
     something IFF this AND that

and 
3)
 my_lemma: LEMMA
     something = otherthing

I think that when I use (GRIND :theories "theory_with_lemmas"),
it manages to use only lemmas of last form (equalities) to rewrite.
It gives me sequents with antecedents that match the "something" part of the lemmas in the 1st and 2nd forms. These
lemmas can be manually "USEd" (usually getting the right instantiation).

How can I cause GRIND to apply the first two forms of lemmas automatically?

Where in the documentation is an explanation of the kinds of lemmas that can be used automatically, and how to do it?

Thanks,

Marcelo Glusman

---

• Prev by Date: PhD STUDENTSHIP available
• Next by Date: Type-correctness conditions in HOL
• Prev by thread: PhD STUDENTSHIP available
• Next by thread: Type-correctness conditions in HOL
• Index(es):
  • Date
  • Thread