PEXT : (thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Derives equality of functions from extensional equivalence.
- DESCRIPTION
- When applied to a theorem A |- !p. t1 p = t2 p, the inference rule PEXT returns the theorem A |- t1 = t2.
A |- !p. t1 p = t2 p ---------------------- PEXT [where p is not free in t1 or t2] A |- t1 = t2

- FAILURE
- Fails if the theorem does not have the form indicated above, or if any of the component variables in the paired variable structure p is free either of the functions t1 or t2.
- EXAMPLE
- PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`)); > val it = [.] |- f = g : thm

- SEEALSO

HOL Kananaskis-14