Define a Skolem (witnessing) function

Examples: (defchoose choose-x-for-p1-and-p2 (x) (y z) (and (p1 x y z) (p2 x y z))) ; Axiom added by the event above: (IMPLIES (AND (P1 X Y Z) (P2 X Y Z)) (LET ((X (CHOOSE-X-FOR-P1-AND-P2 Y Z))) (AND (P1 X Y Z) (P2 X Y Z)))) (defchoose choose-x-for-p1-and-p2 x (y z) ; equivalent to the above (and (p1 x y z) (p2 x y z))) ; The following is as above, but strengthens the axiom added to pick a sort ; of canonical witness, as described below. (defchoose choose-x-for-p1-and-p2 x (y z) (and (p1 x y z) (p2 x y z)) :strengthen t) (defchoose choose-x-and-y-for-p1-and-p2 (x y) (z) (and (p1 x y z) (p2 x y z))) General Form: (defchoose fn (bound-var1 ... bound-varn) (free-var1 ... free-vark) body :strengthen b),

where

The system treats `encapsulate` event, with a single axiom exported as
described below. If you supply a `rewrite` or
otherwise; see rule-classes) is created for

`logic`;
see defun-mode. Also see defun-sk.

In the most common case, where there is only one bound variable, it is
permissible to omit the enclosing parentheses on that variable. The effect is
the same whether or not those parentheses are omitted. We describe this case
first, where there is only one bound variable, and then address the other
case. Both cases are discussed assuming

The effect of the form

(defchoose fn bound-var (free-var1 ... free-vark) body)

is to introduce a new function symbol,

(1) (implies body (let ((bound-var (fn free-var1 ... free-vark))) body))

This axiom is ``clearly conservative'' under the conditions expressed
above: the function

Next consider the case that there is more than one bound variable, i.e., there is more than one bound-var in the following.

(defchoose fn (bound-var1 ... bound-varn) (free-var1 ... free-vark) body)

Then `mv-let` as follows:

(implies body (mv-let (bound-var1 ... bound-varn) (fn free-var1 ... free-vark) body))

We now discuss the case that

(2) (or (equal (fn y) (fn y1)) (let ((bound-var (fn y))) (and body (not body1))) (let ((bound-var (fn y1))) (and body1 (not body))))

An important application of this additional axiom is to be able to define a ``fixing'' function that picks a canonical representative of each equivalence class, for a given equivalence relation. The following events illustrate this point.

(encapsulate ((equiv (x y) t)) (local (defun equiv (x y) (equal x y))) (defequiv equiv)) (defchoose efix (x) (y) (equiv x y) :strengthen t) (defthm equiv-implies-equal-efix-1 (implies (equiv y y1) (equal (efix y) (efix y1))) :hints (("Goal" :use efix)) :rule-classes (:congruence)) (defthm efix-fixes (equiv (efix x) x) :hints (("Goal" :use ((:instance efix (y x))))))

If there is more than one bound variable, then (2) is modified in complete
analogy to (1) to use `mv-let` in place of `let`.

Comment for logicians: As we point out in the documentation for `defun-sk`,

- Conservativity-of-defchoose
- Proof of conservativity of
`defchoose` - Defchoose-queries
- Utilities to query
`defchoose`functions.