Q.ABBREV

STRUCTURE

SYNOPSIS

Introduces an abbreviation into a goal.

DESCRIPTION

The tactic Q.ABBREV_TAC q parses the quotation q in the context of the goal to which it is applied. The result must be a term of the form v = e with v a variable. The effect of the tactic is to replace the term e wherever it occurs in the goal by v (or a primed variant of v if v already occurs in the goal), and to add the assumption Abbrev(v = e) to the goal’s assumptions. Again, if v already occurs free in the goal, then the new assumption will be Abbrev(v' = e), with v' a suitably primed version of v.

It is not an error if the expression e does not occur anywhere within the goal. In this situation, the effect of the tactic is simply to add the assumption Abbrev(v = e).

The Abbrev constant is defined in markerTheory to be the identity function over boolean values. It is used solely as a tag, so that abbreviations can be found by other tools, and so that simplification tactics such as RW_TAC will not eliminate them. When it sees them as part of its context, the simplifier treats terms of the form Abbrev(v = e) as assumptions e = v. In this way, the simplifier can use abbreviations to create further sharing, after an abbreviation’s creation.

FAILURE

Fails if the quotation is ill-typed. This may happen because variables in the quotation that also appear in the goal are given the same type in the quotation as they have in the goal. Also fails if the variable of the equation appears in the expression that it is supposed to be abbreviating.

EXAMPLE

Substitution in the goal:

   - Q.ABBREV_TAC `n = 10` ([], ``10 < 9 * 10``);
   > val it = ([([``Abbrev(n = 10)``], ``n < 9 * n``)], fn) :
     (term list * term) list * (thm list -> thm)

and the assumptions:

   - Q.ABBREV_TAC `m = n + 2` ([``f (n + 2) < 6``], ``n < 7``);
   > val it = ([([``Abbrev(m = n + 2)``, ``f m < 6``], ``n < 7``)], fn) :
     (term list * term) list * (thm list -> thm)

and both

   - Q.ABBREV_TAC `u = x ** 32` ([``x ** 32 = f z``],
                                  ``g (x ** 32 + 6) - 10 < 65``);
   > val it =
       ([([``Abbrev(u = x ** 32)``, ``u = f z``], ``g (u + 6) - 10 < 65``)],
        fn) :
       (term list * term) list * (thm list -> thm)

COMMENTS

Though it is possible to abbreviate functions, using quotations such as `f = \n. n + 3`, in this case ABBREV_TAC will not do anything more than replace exact copies of the abstraction. Following ABBREV_TAC with

   POP_ASSUM (ASSUME_TAC o GSYM o
              SIMP_RULE bool_ss [FUN_EQ_THM, markerTheory.Abbrev_def])

will turn the assumption `Abbrev(f = (\n. n + 3))` into `!n. n + 3 = f n` which may find more instances of the desired pattern.

SEEALSO

Abbr, HO_MATCH_ABBREV_TAC, MATCH_ABBREV_TAC, UNABBREV_TAC