bossLib.FULL_SIMP

STRUCTURE

SYNOPSIS

Simplifies the goal (assumptions as well as conclusion) with the given simpset.

LIBRARY

simpLib

DESCRIPTION

FULL_SIMP_TAC is a powerful simplification tactic that simplifies all of a goal. It proceeds by applying simplification to each assumption of the goal in turn, accumulating simplified assumptions as it goes. These simplified assumptions are used to simplify further assumptions, and all of the simplified assumptions are used as additional rewrites when the conclusion of the goal is simplified.

In addition, simplified assumptions are added back onto the goal using the equivalent of STRIP_ASSUME_TAC and this causes automatic skolemization of existential assumptions, case splits on disjunctions, and the separate assumption of conjunctions. If an assumption is simplified to TRUTH, then this is left on the assumption list. If an assumption is simplified to falsity, this proves the goal.

FAILURE

FULL_SIMP_TAC never fails, but it may diverge.

EXAMPLE

Here FULL_SIMP_TAC is used to prove a goal:

   > FULL_SIMP_TAC arith_ss [] (map Term [`x = 3`, `x < 2`],
                              Term `?y. x * y = 51`)
   - val it = ([], fn) : tactic_result

Using LESS_OR_EQ |- !m n. m <= n = m < n \/ (m = n), a useful case split can be induced in the next goal:

   > FULL_SIMP_TAC bool_ss [LESS_OR_EQ] (map Term [`x <= y`, `x < z`],
                                         Term `x + y < z`);
   - val it =
       ([([`x < y`, `x < z`], `x + y < z`),
         ([`x = y`, `x < z`], `y + y < z`)], fn)
       : tactic_result

Note that the equality x = y is not used to simplify the subsequent assumptions, but is used to simplify the conclusion of the goal.

COMMENTS

The application of STRIP_ASSUME_TAC to simplified assumptions means that FULL_SIMP_TAC can cause unwanted case-splits and other undesirable transformations to occur in one’s assumption list. If one wants to apply the simplifier to assumptions without this occurring, the best approach seems to be the use of RULE_ASSUM_TAC and SIMP_RULE.

Each assumption is used to rewrite lower-numbered assumptions. To get the opposite effect, where each assumption is used to rewrite higher-numbered assumptions, use REV_FULL_SIMP_TAC.

SEEALSO

REV_FULL_SIMP_TAC, ASM_SIMP_TAC, SIMP_CONV, SIMP_RULE, SIMP_TAC, VAR_EQ_TAC