ABBREV_TAC : term -> (string * thm) list * term -> goalstate

SYNOPSIS

Tactic to introduce an abbreviation.

DESCRIPTION

The tactic ABBREV_TAC `x = t` abbreviates any instances of the term t in the goal (assumptions or conclusion) with x, and adds a new assumption t = x. (Reversed so that rules like ASM_REWRITE_TAC will not immediately expand it again.) The LHS may be of the form f x in which case abstraction will happen first.

FAILURE CONDITIONS

Fails unless the left-hand side is a variable or a variable applied to a list of variable arguments.

EXAMPLE

  # g `(12345 + 12345) + f(12345 + 12345) = f(12345 + 12345)`;;
  Warning: Free variables in goal: f
  val it : goalstack = 1 subgoal (1 total)

  `(12345 + 12345) + f (12345 + 12345) = f (12345 + 12345)`

  # e(ABBREV_TAC `n = 12345 + 12345`);;
  val it : goalstack = 1 subgoal (1 total)

   0 [`12345 + 12345 = n`]

  `n + f n = f n`

USES

Convenient for abbreviating large and unwieldy expressions as a sort of `local definition'.

SEE ALSO

EXPAND_TAC.