Subject: Tactics

Keywords: ::Refiner
          ::proof

Title: functionality and rewriting

--------------------------------------------------

Functionality lemmas are aggregated by name by matching the opid of
definitions concatenated with "_functionality". Functionality
lemma names can be suffixed with arbitrary text but no other
text should prefix the opid. For example, the foo_functionality
would be associated with definitions whose lhs has opid `foo`.
bar_foo_functionality would be associated with `bar_foo`.
foo_functionality-bar would be associated with `foo`.   

Functionality lemmas have to use only declared relations otherwise
they can mess up finding the other ones. Also, they have to use only
variables for the subterms of the operator, they can't have some 
other pattern matching. The constraints have to be expressed as
declared relations (that are defined as abstractions).
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home