SIMP_CONV
bossLib.SIMP_CONV : simpset -> thm list -> conv
Also exported as simpLib.SIMP_CONV.
Applies a simpset and a list of rewrite rules to simplify a term.
SIMP_CONV is the fundamental engine of the HOL simplification library.
It repeatedly applies the transformations included in the provided
simpset (which is augmented with the given rewrite rules) to a term,
ultimately yielding a theorem equating the original term to another.
Values of the simpset type embody a suite of different transformations
that might be applicable to given terms. These "transformational
components" are rewrites, conversions, AC-rules, congruences, decision
procedures and a filter, which is used to modify the way in which
rewrite rules are added to the simpset. The exact types for these
components, known as simpset fragments, and the way they can be combined
to create simpsets is given in the reference entry for SSFRAG.
Rewrite rules are used similarly to the way in they are used in the
rewriting system (REWRITE_TAC et al.). These are equational theorems
oriented to rewrite from left-hand-side to right-hand-side. Further,
SIMP_CONV handles obvious problems. If a rewrite rule is of the
general form [...] |- x = f x, then it will be discarded, and a
message is printed to this effect. On the other hand, if the
right-hand-side is a permutation of the pattern on the left, as in
|- x + y = y + x and
|- x INSERT (y INSERT s) = y INSERT (x INSERT s), then such rules will
only be applied if the term to which they are being applied is strictly
reduced according to some term ordering.
Rewriting is done using a form of higher-order matching, and also uses
conditional rewriting. This latter means that theorems of the form
|- P ==> (x = y) can be used as rewrites. If a term matching x is
found, the simplifier will attempt to satisfy the side-condition P. If
it is able to do so, then the rewriting will be performed. In the
process of attempting to rewrite P to true, further side conditions
may be generated. The simplifier limits the size of the stack of side
conditions to be solved (the reference variable Cond_rewr.stack_limit
holds this limit), so this will not introduce an infinite loop.
Rewrite rules can always be added "on the fly" as all of the
simplification functions take a thm list argument where these rules
can be specified. If a set of rewrite rules is frequently used, then
these should probably be made into a ssfrag value with the rewrites
function and then added to an existing simpset with ++.
The conversions which are part of simpsets are useful for situations
where simple rewriting is not enough to transform certain terms. For
example, the BETA_CONV conversion is not expressible as a standard
first order rewrite, but is part of the bool_ss simpset and the
application of this simpset will thus simplify all occurrences of
(\x. e1) e2.
In fact, conversions in simpsets are not typically applied
indiscriminately to all sub-terms. (If a conversion is applied to an
inappropriate sub-term and fails, this failure is caught by the
simplifier and ignored.) Instead, conversions in simpsets are
accompanied by a term-pattern which specifies the sort of situations in
which they should be applied. This facility is used in the definition of
bool_ss to include ETA_CONV, but stop it from transforming !x. P x
into $! P.
AC-rules allow simpsets to be constructed that automatically normalise terms involving associative and commutative operators, again according to some arbitrary term ordering metric.
Congruence rules allow SIMP_CONV to assume additional context as a
term is rewritten. In a term such as P ==> Q /\ f x the truth of term
P may be assumed as an additional piece of context in the rewriting of
Q /\ f x. The congruence theorem that states this is valid is
(IMP_CONG):
|- (P = P') ==> (P' ==> (Q = Q')) ==> ((P ==> Q) = (P' ==> Q'))
Other congruence theorems can be part of simpsets. The system provides
IMP_CONG above and COND_CONG as part of the CONG_ss ssfrag
value. (These simpset fragments can be incorporated into simpsets with
the ++ function.) Other congruence theorems are already proved for
operators such as conjunction and disjunction, but use of these in
standard simpsets is not recommended as the computation of all the
additional contexts for a simple chain of conjuncts or disjuncts can be
very computationally intensive.
Decision procedures in simpsets are similar to conversions. They are
arbitrary pieces of code that are applied to sub-terms at low priority.
They are given access to the wider context through a list of relevant
theorems. The arith_ss simpset includes an arithmetic decision
procedure implemented in this way.
Failure
SIMP_CONV never fails, but may diverge.
Example
> SIMP_CONV arith_ss [] ``(\x. x + 3) 4``;
val it = ⊢ (λx. x + 3) 4 = 7: thm
SIMP_CONV is a powerful way of manipulating terms. Other functions in
the simplification library provide the same facilities when in the
contexts of goals and tactics (SIMP_TAC, ASM_SIMP_TAC etc.), and
theorems (SIMP_RULE), but SIMP_CONV provides the underlying
functionality, and is useful in its own right, just as conversions are
generally.
See also
bossLib.++,
bossLib.ASM_SIMP_TAC,
bossLib.FULL_SIMP_TAC,
simpLib.mk_simpset,
bossLib.rewrites,
bossLib.SIMP_RULE,
bossLib.SIMP_TAC,
simpLib.SSFRAG, bossLib.EVAL