PSPEC_TAC
PairRules.PSPEC_TAC : term * term -> tactic
Generalizes a goal.
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: 2 proofs.
2. Incomplete goalstack:
Initial goal:
∃R. WF R ∧ (∀rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)) ∧
∀rst x ord. R (ord,FILTER ($¬ ∘ ord x) rst) (ord,x::rst)
1. Incomplete goalstack:
Initial goal:
1 + 2 = 2 + 1
> e (PairRules.PSPEC_TAC (Term`(1,2)`, Term`(x:num,y:num)`));
OK..
1 subgoal:
val it =
∀(x,y). x + y = y + x
Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.
See also
PairRules.PGEN,
PairRules.PGENL,
PairRules.PGEN_TAC,
PairRules.PSPEC,
PairRules.PSPECL,
PairRules.PSPEC_ALL,
PairRules.PSTRIP_TAC