		Search-engine friendly clone of the ACL2 documentation.

Defun-sk

Def::un-sk

An extension of defun-sk that supports automated skolemization and instantiation of quantified formulae

The def::un-sk macro is an extension of defun-sk that supports automated skolemization and instantiation of quantified formulae via the computed hints quant::inst? and quant::skosimp.

Usage:

 (include-book "coi/quantification/quantification" :dir :system)

 (def::un-sk forall-zen (a)
   (forall (x y) (implies (boo a x) (hoo a y))))

 (def::un-sk exists-zen (a)
   (exists (x y) (not (implies (boo a x) (hoo a y)))))

 (defthmd forall-zen-instantiation-test
   (implies
    (forall-zen q)
    (implies (boo q x1) (hoo q y1)))
   :hints ((quant::inst?)))

 (defthmd exists-zen-instantiation-test
   (implies
    (not (exists-zen q))
    (implies (boo q x1) (hoo q y1)))
   :hints ((quant::inst?)))

 ;; This is kind of a cool theorem

 (defthmd forall-is-not-exists
   (iff (forall-zen q)
        (not (exists-zen q)))
   :hints ((quant::skosimp)
	    (quant::inst?)))

 ;; Here we use it to do "pick-a-point" proofs

 (def::un-sk assox-equiv (x y)
   (forall (a) (equal (assoc a x) (assoc a y))))

 (defequiv assox-equiv
   :hints ((quant::skosimp)
           (quant::inst?)))

 (defcong assox-equiv equal (assoc a x) 2
   :hints ((quant::skosimp)
           (quant::inst?)))

 (defcong assox-equiv assox-equiv (cons pair y) 2
   :hints ((quant::skosimp)
           (quant::inst?)))

 (defcong assox-equiv assox-equiv (acons key value y) 3
   :hints ((quant::skosimp)
 	    (quant::inst?)))

Subtopics

Skosimp: A hint for performing automated skolemization of quantified formulae
Inst?: A hint that attempts automated instantiation of quantified formulae