1\DOC PEXT 2 3\TYPE {PEXT : (thm -> thm)} 4 5\KEYWORDS 6rule, extensionality. 7 8\LIBRARY 9pair 10 11\SYNOPSIS 12Derives equality of functions from extensional equivalence. 13 14\DESCRIBE 15When applied to a theorem {A |- !p. t1 p = t2 p}, 16the inference rule {PEXT} returns the theorem {A |- t1 = t2}. 17{ 18 A |- !p. t1 p = t2 p 19 ---------------------- PEXT [where p is not free in t1 or t2] 20 A |- t1 = t2 21} 22 23 24\FAILURE 25Fails if the theorem does not have the form indicated above, or 26if any of the component variables in the paired variable structure {p} 27is free either of the functions {t1} or {t2}. 28 29\EXAMPLE 30{ 31- PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`)); 32> val it = [.] |- f = g : thm 33} 34 35 36\SEEALSO 37Drule.EXT, Thm.AP_THM, PairRules.PETA_CONV, Conv.FUN_EQ_CONV, PairRules.P_FUN_EQ_CONV. 38\ENDDOC 39