Presents a simpset fragment as a theorem for inclusion in simplification
DESCRIPTION
A call to SF sfrag creates a theorem that encodes (by way of an
indirection through a global register of fragments) the simpset
fragment sfrag. If this theorem is then passed to a simplification
tactic (or conversion), the simplification tactic will add the given
fragment to the simpset underpinning the simplification.
FAILURE
Fails if the given fragment doesn’t have a name.
COMMENTS
If the given fragment has a name, but has not been previously
registered, it is registered at the time the simplification tactic or
conversion is called. Given that this registration probably happens as
part of a script’s execution, this registration is unlikely to
persist.
EXAMPLE
> SIMP_CONV bool_ss [SF ETA_ss] “P (λx. f x) ∧ Q”;
val it = ⊢ P (λx. f x) ∧ Q ⇔ P f ∧ Q : thm
> simp[SF ETA_ss] ([], “P (λx. f x) ∧ Q”);
val it = ([([], “P f ∧ Q”)], fn): goal list * validation