PSPEC_TAC : term * term -> tactic

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Generalizes a goal.
- DESCRIPTION
- When applied to a pair of terms (q,p), where p is a paired structure of variables and a goal A ?- t, the tactic PSPEC_TAC generalizes the goal to A ?- !p. t[p/q], that is, all components of q are turned into the corresponding components of p.
A ?- t ================= PSPEC_TAC (q,p) A ?- !x. t[p/q]

- FAILURE
- Fails unless p is a paired structure of variables with the same type as q.
- EXAMPLE
- g `1 + 2 = 2 + 1`; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: 1 + 2 = 2 + 1 - e (PSPEC_TAC (Term`(1,2)`, Term`(x:num,y:num)`)); OK.. 1 subgoal: > val it = !(x,y). x + y = y + x : proof

- USES
- Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.
- SEEALSO

HOL Kananaskis-14