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