1\DOC ABBREV_TAC
2
3\TYPE {Q.ABBREV_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Introduces an abbreviation into a goal.
7
8\DESCRIBE
9
10The tactic {Q.ABBREV_TAC q} parses the quotation {q} in the context of
11the goal to which it is applied.  The result must be a term of the
12form {v = e} with {v} a variable.  The effect of the tactic is to
13replace the term {e} wherever it occurs in the goal by {v} (or a
14primed variant of {v} if {v} already occurs in the goal), and to add
15the assumption {Abbrev(v = e)} to the goal's assumptions.  Again, if
16{v} already occurs free in the goal, then the new assumption will be
17{Abbrev(v' = e)}, with {v'} a suitably primed version of {v}.
18
19It is not an error if the expression {e} does not occur anywhere
20within the goal.  In this situation, the effect of the tactic is
21simply to add the assumption {Abbrev(v = e)}.
22
23The {Abbrev} constant is defined in {markerTheory} to be the identity
24function over boolean values.  It is used solely as a tag, so that
25abbreviations can be found by other tools, and so that simplification
26tactics such as {RW_TAC} will not eliminate them.  When it sees them
27as part of its context, the simplifier treats terms of the form
28{Abbrev(v = e)} as assumptions {e = v}.  In this way, the simplifier
29can use abbreviations to create further sharing, after an
30abbreviation's creation.
31
32\FAILURE
33Fails if the quotation is ill-typed.  This may happen because
34variables in the quotation that also appear in the goal are given the
35same type in the quotation as they have in the goal.  Also fails if
36the variable of the equation appears in the expression that it is
37supposed to be abbreviating.
38
39\EXAMPLE
40Substitution in the goal:
41{
42   - Q.ABBREV_TAC `n = 10` ([], ``10 < 9 * 10``);
43   > val it = ([([``Abbrev(n = 10)``], ``n < 9 * n``)], fn) :
44     (term list * term) list * (thm list -> thm)
45}
46and the assumptions:
47{
48   - Q.ABBREV_TAC `m = n + 2` ([``f (n + 2) < 6``], ``n < 7``);
49   > val it = ([([``Abbrev(m = n + 2)``, ``f m < 6``], ``n < 7``)], fn) :
50     (term list * term) list * (thm list -> thm)
51}
52and both
53{
54   - Q.ABBREV_TAC `u = x ** 32` ([``x ** 32 = f z``],
55                                  ``g (x ** 32 + 6) - 10 < 65``);
56   > val it =
57       ([([``Abbrev(u = x ** 32)``, ``u = f z``], ``g (u + 6) - 10 < 65``)],
58        fn) :
59       (term list * term) list * (thm list -> thm)
60}
61
62\COMMENTS
63The {bossLib} library provides {qabbrev_tac} as a synonym for {Q.ABBREV_TAC}.
64
65It is possible to abbreviate functions, using quotations such
66as {`f = \n. n + 3`}. When this is done {ABBREV_TAC} will not itself do anything
67more than replace exact copies of the abstraction, but the simplifier will subsequently see occurrences of the pattern and replace them.
68Thus:
69{
70   > (qabbrev_tac `f = \x. x + 1` >> asm_simp_tac bool_ss [])
71        ([], ``3 + 1 = 4 + 1``);
72   val it =
73      ([([``Abbrev (f = (\x. x + 1))``], ``f 3 = f 4``)], fn):
74      goal list * (thm list -> thm)
75}
76where the simplifier has seen occurrences of the ``{x+1}'' pattern and replaced it with calls to the {f}-abbreviation.
77
78\SEEALSO
79BasicProvers.Abbr, Q.HO_MATCH_ABBREV_TAC, Q.MATCH_ABBREV_TAC, Q.UNABBREV_TAC.
80
81\ENDDOC
82