1\DOC EXISTS 2 3\TYPE {EXISTS : term * term -> thm -> thm} 4 5\SYNOPSIS 6Introduces existential quantification given a particular witness. 7 8\KEYWORDS 9rule, existential. 10 11\DESCRIBE 12When applied to a pair of terms and a theorem, the first term an existentially 13quantified pattern indicating the desired form of the result, and the second a 14witness whose substitution for the quantified variable gives a term which is 15the same as the conclusion of the theorem, {EXISTS} gives the desired theorem. 16{ 17 A |- p[u/x] 18 ------------- EXISTS (?x. p, u) 19 A |- ?x. p 20} 21 22 23\FAILURE 24Fails unless the substituted pattern is the same as the conclusion of the 25theorem. 26 27\EXAMPLE 28The following examples illustrate how it is possible to deduce different 29things from the same theorem: 30{ 31 - EXISTS (Term `?x. x=T`,T) (REFL T); 32 > val it = |- ?x. x = T : thm 33 34 - EXISTS (Term `?x:bool. x=x`,T) (REFL T); 35 > val it = |- ?x. x = x : thm 36} 37 38 39\SEEALSO 40Thm.CHOOSE, Drule.SIMPLE_EXISTS, Tactic.EXISTS_TAC. 41\ENDDOC 42