PSPEC : (term -> thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Specializes the conclusion of a theorem.
- DESCRIPTION
- When applied to a term q and a theorem A |- !p. t, then PSPEC returns the theorem A |- t[q/p]. If necessary, variables will be renamed prior to the specialization to ensure that q is free for p in t, that is, no variables free in q become bound after substitution.
A |- !p. t -------------- PSPEC "q" A |- t[q/p]

- FAILURE
- Fails if the theorem’s conclusion is not a paired universal quantification, or if p and q have different types.
- EXAMPLE
- PSPEC specialised paired quantifications.
- PSPEC (Term `(1,2)`) (ASSUME (Term`!(x,y). (x + y) = (y + x)`)); > val it = [.] |- 1 + 2 = 2 + 1 : thm

PSPEC treats paired structures of variables as variables and preserves structure accordingly.

- PSPEC (Term `x:'a#'a`) (ASSUME (Term `!(x:'a,y:'a). (x,y) = (x,y)`)); > val it = [.] |- x = x : thm

- SEEALSO

HOL Kananaskis-14