Filtering...

meta-extract-user

books/clause-processors/meta-extract-user

Included Books

ev-theoremp def-functional-instance match-tree flag magic-ev top sublis-var meta-extract
other
(in-package "ACL2")
include-book
(include-book "ev-theoremp")
include-book
(include-book "tools/def-functional-instance" :dir :system)
include-book
(include-book "tools/match-tree" :dir :system)
include-book
(include-book "tools/flag" :dir :system)
include-book
(include-book "magic-ev")
include-book
(include-book "xdoc/top" :dir :system)
include-book
(include-book "system/sublis-var" :dir :system)
include-book
(include-book "system/meta-extract" :dir :system)
in-theory
(in-theory (disable mv-nth))
other
(defevaluator mextract-ev
  mextract-ev-lst
  ((typespec-check ts x) (if a
      b
      c)
    (equal a b)
    (not a)
    (iff a b)
    (implies a b))
  :namedp t)
other
(def-ev-theoremp mextract-ev)
other
(defchoose mextract-contextual-badguy
  (obj)
  (a mfc state)
  (not (mextract-ev (meta-extract-contextual-fact obj mfc state) a)))
mextract-ev-contextual-factsmacro
(defmacro mextract-ev-contextual-facts
  (a &key (mfc 'mfc) (state 'state))
  `(mextract-ev (meta-extract-contextual-fact (mextract-contextual-badguy ,A ,MFC ,STATE)
      ,MFC
      ,STATE)
    ,A))
mextract-contextual-badguy-sufficienttheorem
(defthmd mextract-contextual-badguy-sufficient
  (implies (mextract-ev-contextual-facts a)
    (mextract-ev (meta-extract-contextual-fact obj mfc state) a))
  :hints (("goal" :use mextract-contextual-badguy
     :in-theory (disable meta-extract-contextual-fact))))
other
(defchoose mextract-global-badguy
  (obj st)
  (state)
  (not (mextract-ev-theoremp (meta-extract-global-fact+ obj st state))))
mextract-ev-global-factsmacro
(defmacro mextract-ev-global-facts
  (&key (state 'state))
  `(mextract-ev (meta-extract-global-fact+ (mv-nth 0 (mextract-global-badguy ,STATE))
      (mv-nth 1 (mextract-global-badguy ,STATE))
      ,STATE)
    (mextract-ev-falsify (meta-extract-global-fact+ (mv-nth 0 (mextract-global-badguy ,STATE))
        (mv-nth 1 (mextract-global-badguy ,STATE))
        ,STATE))))
mextract-global-badguy-sufficienttheorem
(defthmd mextract-global-badguy-sufficient
  (implies (mextract-ev-global-facts)
    (mextract-ev (meta-extract-global-fact+ obj st state) a))
  :hints (("goal" :use ((:instance mextract-global-badguy) (:instance mextract-ev-falsify
         (x (meta-extract-global-fact+ obj st state))))
     :in-theory (disable meta-extract-global-fact+))))
local
(local (in-theory (disable w sublis-var)))
mextract-typesettheorem
(defthm mextract-typeset
  (implies (mextract-ev-contextual-facts a)
    (typespec-check (mfc-ts term mfc state :forcep nil)
      (mextract-ev term a)))
  :hints (("goal" :use ((:instance mextract-contextual-badguy
        (obj `(:typeset ,TERM))))
     :in-theory (disable typespec-check))))
mextract-rw+-equaltheorem
(defthm mextract-rw+-equal
  (implies (mextract-ev-contextual-facts a)
    (equal (mextract-ev (mfc-rw+ term alist obj nil mfc state :forcep nil)
        a)
      (mextract-ev (sublis-var alist term) a)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw+ term alist obj nil)))))))
mextract-rw+-ifftheorem
(defthm mextract-rw+-iff
  (implies (mextract-ev-contextual-facts a)
    (iff (mextract-ev (mfc-rw+ term alist obj t mfc state :forcep nil)
        a)
      (mextract-ev (sublis-var alist term) a)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw+ term alist obj t)))))))
mextract-rw+-equivtheorem
(defthm mextract-rw+-equiv
  (implies (and (mextract-ev-contextual-facts a)
      equiv
      (not (equal equiv t))
      (symbolp equiv)
      (getprop equiv
        'coarsenings
        nil
        'current-acl2-world
        (w state)))
    (mextract-ev `(,EQUIV ,(SUBLIS-VAR ALIST TERM)
        ,(MFC-RW+ TERM ALIST OBJ EQUIV MFC STATE :FORCEP NIL))
      a))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw+ term alist obj equiv)))))))
mextract-rw-equaltheorem
(defthm mextract-rw-equal
  (implies (mextract-ev-contextual-facts a)
    (equal (mextract-ev (mfc-rw term obj nil mfc state :forcep nil) a)
      (mextract-ev (sublis-var nil term) a)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw term obj nil)))))))
mextract-rw-ifftheorem
(defthm mextract-rw-iff
  (implies (mextract-ev-contextual-facts a)
    (iff (mextract-ev (mfc-rw term obj t mfc state :forcep nil) a)
      (mextract-ev (sublis-var nil term) a)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw term obj t)))))))
mextract-rw-equivtheorem
(defthm mextract-rw-equiv
  (implies (and (mextract-ev-contextual-facts a)
      equiv
      (not (equal equiv t))
      (symbolp equiv)
      (getprop equiv
        'coarsenings
        nil
        'current-acl2-world
        (w state)))
    (mextract-ev `(,EQUIV ,(SUBLIS-VAR NIL TERM)
        ,(MFC-RW TERM OBJ EQUIV MFC STATE :FORCEP NIL))
      a))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :rw term obj equiv)))))))
mextract-mfc-aptheorem
(defthm mextract-mfc-ap
  (implies (and (mextract-ev-contextual-facts a) (mextract-ev term a))
    (not (mfc-ap term mfc state :forcep nil)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy (obj (list :ap term)))))))
mextract-relieve-hyptheorem
(defthm mextract-relieve-hyp
  (implies (and (mextract-ev-contextual-facts a)
      (not (mextract-ev (sublis-var alist hyp) a)))
    (not (mfc-relieve-hyp hyp
        alist
        rune
        target
        bkptr
        mfc
        state
        :forcep nil)))
  :hints (("Goal" :use ((:instance mextract-contextual-badguy
        (obj (list :relieve-hyp hyp alist rune target bkptr)))))))
mextract-formulatheorem
(defthm mextract-formula
  (implies (and (mextract-ev-global-facts) (equal (w st) (w state)))
    (mextract-ev (meta-extract-formula name st) a))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :formula name)))))))
local
(local (encapsulate nil
    (local (defthm minus-over-plus (equal (- (+ a b)) (+ (- a) (- b)))))
    (local (defthm plus-move-constant
        (implies (syntaxp (quotep b)) (equal (+ a b c) (+ b a c)))))
    (local (defthm nth-plus-1
        (implies (natp b) (equal (nth (+ 1 b) x) (nth b (cdr x))))))
    (defthm len-member-equal
      (<= (len (member-equal x y)) (len y))
      :rule-classes :linear)
    (defthm len-member-equal-pos
      (implies (member-equal x y) (< 0 (len (member-equal x y))))
      :rule-classes :linear)
    (defthm nth-by-member-equal
      (implies (member x y)
        (equal (nth (+ (len y) (- (len (member x y)))) y) x)))))
mextract-lemma-termtheorem
(defthm mextract-lemma-term
  (implies (and (mextract-ev-global-facts)
      (member rule (fgetprop fn 'lemmas nil (w st)))
      (equal (w st) (w state)))
    (mextract-ev (rewrite-rule-term rule) a))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :lemma fn
            (let ((lemmas (getprop fn 'lemmas nil 'current-acl2-world (w state))))
              (- (len lemmas) (len (member rule lemmas)))))))))))
mextract-lemmatheorem
(defthm mextract-lemma
  (implies (and (mextract-ev-global-facts)
      (member rule (fgetprop fn 'lemmas nil (w st)))
      (not (eq (access rewrite-rule rule :subclass) 'meta))
      (mextract-ev (conjoin (access rewrite-rule rule :hyps)) a)
      (equal (w st) (w state)))
    (mextract-ev `(,(ACCESS REWRITE-RULE RULE :EQUIV) ,(ACCESS REWRITE-RULE RULE :LHS)
        ,(ACCESS REWRITE-RULE RULE :RHS))
      a))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :lemma fn
            (let ((lemmas (getprop fn 'lemmas nil 'current-acl2-world (w state))))
              (- (len lemmas) (len (member rule lemmas)))))))))))
mextract-linear-lemma-termtheorem
(defthm mextract-linear-lemma-term
  (implies (and (mextract-ev-global-facts)
      (member rule (fgetprop fn 'linear-lemmas nil (w st)))
      (equal (w st) (w state)))
    (mextract-ev (linear-lemma-term rule) a))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :linear-lemma fn
            (let ((lemmas (getprop fn
                   'linear-lemmas
                   nil
                   'current-acl2-world
                   (w state))))
              (- (len lemmas) (len (member rule lemmas)))))))))))
mextract-linear-lemmatheorem
(defthm mextract-linear-lemma
  (implies (and (mextract-ev-global-facts)
      (member rule (fgetprop fn 'linear-lemmas nil (w st)))
      (mextract-ev (conjoin (access linear-lemma rule :hyps)) a)
      (equal (w st) (w state)))
    (mextract-ev (access linear-lemma rule :concl) a))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :linear-lemma fn
            (let ((lemmas (getprop fn
                   'linear-lemmas
                   nil
                   'current-acl2-world
                   (w state))))
              (- (len lemmas) (len (member rule lemmas)))))))))))
plist-worldp-w-statetheorem
(defthm plist-worldp-w-state
  (implies (state-p1 state) (plist-worldp (w state)))
  :hints (("Goal" :in-theory (enable w))))
magic-ev-fncall-logicfunction
(defun magic-ev-fncall-logic
  (fn arglist state)
  (declare (xargs :guard (symbolp fn) :stobjs state))
  (if (logicp fn (w state))
    (magic-ev-fncall fn arglist state t nil)
    (mv (msg "Not logic mode: ~x0" fn) nil)))
mextract-fncall-logictheorem
(defthm mextract-fncall-logic
  (mv-let (erp val)
    (magic-ev-fncall-logic fn arglist st)
    (implies (and (mextract-ev-global-facts)
        (equal (w st) (w state))
        (not erp))
      (equal val (mextract-ev (cons fn (kwote-lst arglist)) nil))))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :fncall fn arglist))
        (a nil))))))
local
(local (in-theory (disable magic-ev-fncall-logic)))
mextract-fncalltheorem
(defthm mextract-fncall
  (mv-let (erp val)
    (magic-ev-fncall fn arglist st t nil)
    (implies (and (mextract-ev-global-facts)
        (equal (w st) (w state))
        (not erp)
        (logicp fn (w st)))
      (equal val (mextract-ev (cons fn (kwote-lst arglist)) nil))))
  :hints (("Goal" :use ((:instance mextract-global-badguy-sufficient
        (obj (list :fncall fn arglist))
        (a nil))))))
other
(set-state-ok t)
other
(make-flag magic-ev-flg magic-ev)
other
(defthm-magic-ev-flg (defthm mextract-ev-magic-ev
    (mv-let (erp val)
      (magic-ev x alist st hard-errp aokp)
      (implies (and (mextract-ev-global-facts)
          (equal (w st) (w state))
          (not erp)
          (equal hard-errp t)
          (equal aokp nil)
          (pseudo-termp x))
        (equal val (mextract-ev x alist))))
    :flag magic-ev)
  (defthm mextract-ev-magic-ev-lst
    (mv-let (erp val)
      (magic-ev-lst x alist st hard-errp aokp)
      (implies (and (mextract-ev-global-facts)
          (equal (w st) (w state))
          (not erp)
          (equal hard-errp t)
          (equal aokp nil)
          (pseudo-term-listp x))
        (equal val (mextract-ev-lst x alist))))
    :flag magic-ev-lst)
  :hints (("goal" :in-theory (e/d (mextract-ev-of-fncall-args)
       (meta-extract-global-fact+))
     :induct (magic-ev-flg flag x alist st hard-errp aokp))))
fn-get-deffunction
(defun fn-get-def
  (fn state)
  (declare (xargs :guard (symbolp fn) :stobjs state))
  (b* (((when (eq fn 'quote)) (mv nil nil nil)) (formula (meta-extract-formula fn state))
      ((unless-match formula
         (equal ((:! fn) :? formals) (:? body))) (mv nil nil nil))
      ((unless (and (symbol-listp formals)
           (not (member-eq nil formals))
           (no-duplicatesp-eq formals))) (mv nil nil nil)))
    (mv t formals body)))
fn-get-def-formalstheorem
(defthm fn-get-def-formals
  (b* (((mv ok formals ?body) (fn-get-def fn st)))
    (implies ok
      (and (symbol-listp formals)
        (not (member nil formals))
        (no-duplicatesp formals)))))
ev-lst-of-pairlis-append-head-restencapsulate
(encapsulate nil
  (local (defun ev-pair-ind
      (head keys vals)
      (if (atom keys)
        head
        (ev-pair-ind (append head (list (cons (car keys) (car vals))))
          (cdr keys)
          (cdr vals)))))
  (local (defthm intersectp-commutes
      (equal (intersectp x y) (intersectp y x))))
  (local (defthm intersectp-of-append
      (equal (intersectp (append y z) x)
        (or (intersectp y x) (intersectp z x)))
      :hints (("goal" :induct (append y z)
         :in-theory (disable intersectp-commutes)))))
  (local (defthm intersectp-of-append2
      (equal (intersectp x (append y z))
        (or (intersectp x y) (intersectp x z)))
      :hints (("goal" :use intersectp-of-append
         :in-theory (disable intersectp-of-append)
         :do-not-induct t))))
  (local (defthm intersectp-list
      (iff (intersectp x (list y)) (member y x))))
  (local (defthm append-append
      (equal (append (append a b) c) (append a b c))))
  (local (defthm alistp-append
      (implies (and (alistp a) (alistp b)) (alistp (append a b)))))
  (local (defthm commutativity-2-of-+
      (equal (+ x (+ y z)) (+ y (+ x z)))))
  (local (defthm fold-consts-in-+
      (implies (and (syntaxp (quotep x)) (syntaxp (quotep y)))
        (equal (+ x (+ y z)) (+ (+ x y) z)))))
  (local (defthm distributivity-of-minus-over-+
      (equal (- (+ x y)) (+ (- x) (- y)))))
  (local (defthm assoc-when-not-member-strip-cars
      (implies (and (not (member k (strip-cars x))) (alistp x))
        (not (assoc k x)))))
  (local (defthm assoc-of-append-alist
      (implies (alistp head)
        (equal (assoc k (append head rest))
          (or (assoc k head) (assoc k rest))))))
  (local (defthm strip-cars-append
      (equal (strip-cars (append a b))
        (append (strip-cars a) (strip-cars b)))))
  (defthm ev-lst-of-pairlis-append-head-rest
    (implies (and (no-duplicatesp keys)
        (alistp head)
        (not (intersectp keys (strip-cars head)))
        (symbol-listp keys)
        (not (member nil keys)))
      (equal (mextract-ev-lst keys
          (append head (pairlis$ keys vals) rest))
        (take (len keys) vals)))
    :hints (("goal" :induct (ev-pair-ind head keys vals)
       :do-not-induct t)))
  (defthm ev-lst-of-pairlis-append-rest
    (implies (and (no-duplicatesp keys)
        (symbol-listp keys)
        (not (member nil keys)))
      (equal (mextract-ev-lst keys (append (pairlis$ keys vals) rest))
        (take (len keys) vals)))
    :hints (("goal" :use ((:instance ev-lst-of-pairlis-append-head-rest (head nil))))))
  (defthm ev-lst-of-pairlis
    (implies (and (no-duplicatesp keys)
        (symbol-listp keys)
        (not (member nil keys)))
      (equal (mextract-ev-lst keys (pairlis$ keys vals))
        (take (len keys) vals)))
    :hints (("goal" :use ((:instance ev-lst-of-pairlis-append-head-rest
          (head nil)
          (rest nil))))))
  (defthm kwote-lst-of-take
    (implies (equal n (len args))
      (equal (kwote-lst (take n args)) (kwote-lst args)))))
len-of-mextract-ev-lsttheorem
(defthm len-of-mextract-ev-lst
  (equal (len (mextract-ev-lst x a)) (len x)))
local
(local (defthm mextract-ev-match-tree
    (b* (((mv ok alist) (match-tree pat x alist)))
      (implies ok
        (equal (mextract-ev x a)
          (mextract-ev (subst-tree pat alist) a))))
    :hints (("Goal" :in-theory (enable match-tree-is-subst-tree)))))
mextract-ev-fn-get-deftheorem
(defthm mextract-ev-fn-get-def
  (b* (((mv ok formals body) (fn-get-def fn st)))
    (implies (and ok
        (mextract-ev-global-facts)
        (equal (w st) (w state))
        (equal (len args) (len formals)))
      (equal (mextract-ev (cons fn args) a)
        (mextract-ev body
          (pairlis$ formals (mextract-ev-lst args a))))))
  :hints (("Goal" :in-theory (e/d (mextract-ev-of-fncall-args match-tree-opener-theory
         match-tree-alist-opener-theory)
       (mextract-formula meta-extract-global-fact+
         meta-extract-formula
         take))
     :use ((:instance mextract-formula
        (name fn)
        (st st)
        (a (pairlis$ (mv-nth 1 (fn-get-def fn st))
            (mextract-ev-lst args a))))))))
in-theory
(in-theory (disable fn-get-def))
fn-check-deffunction
(defun fn-check-def
  (fn state formals body)
  (declare (xargs :guard (symbolp fn) :stobjs state))
  (b* (((mv ok fformals fbody) (fn-get-def fn state)))
    (and ok (equal fformals formals) (equal fbody body))))
fn-check-def-formalstheorem
(defthm fn-check-def-formals
  (implies (fn-check-def fn st formals body)
    (and (symbol-listp formals)
      (not (member nil formals))
      (no-duplicatesp formals))))
fn-check-def-not-quotetheorem
(defthm fn-check-def-not-quote
  (implies (fn-check-def fn st formals body)
    (not (equal fn 'quote)))
  :hints (("Goal" :in-theory (enable fn-get-def))))
mextract-ev-fn-check-deftheorem
(defthm mextract-ev-fn-check-def
  (implies (and (fn-check-def fn st formals body)
      (mextract-ev-global-facts)
      (equal (w st) (w state))
      (equal (len args) (len formals)))
    (equal (mextract-ev (cons fn args) a)
      (mextract-ev body
        (pairlis$ formals (mextract-ev-lst args a)))))
  :hints (("Goal" :in-theory (disable meta-extract-global-fact+))))
fn-check-def-is-fn-get-deftheorem
(defthm fn-check-def-is-fn-get-def
  (b* (((mv ok formals body) (fn-get-def fn state)))
    (equal ok (fn-check-def fn state formals body)))
  :hints (("Goal" :in-theory (enable fn-get-def))))
in-theory
(in-theory (disable fn-check-def))
*def-meta-extract-events*constant
(defconst *def-meta-extract-events*
  '(encapsulate nil
    (local (in-theory nil))
    (def-ev-theoremp evfn)
    (defchoose evfn-meta-extract-contextual-badguy
      (obj)
      (a mfc state)
      (not (evfn (meta-extract-contextual-fact obj mfc state) a)))
    (defchoose evfn-meta-extract-global-badguy
      (obj st)
      (state)
      (not (evfn (meta-extract-global-fact+ obj st state)
          (evfn-falsify (meta-extract-global-fact+ obj st state)))))
    (defthmd evfn-falsify-sufficient
      (implies (evfn x (evfn-falsify x)) (evfn x a))
      :hints (("goal" :use evfn-falsify)))
    (defmacro evfn-meta-extract-contextual-facts
      (a &key (mfc 'mfc) (state 'state))
      `(evfn (meta-extract-contextual-fact (evfn-meta-extract-contextual-badguy ,A ,MFC ,STATE)
          ,MFC
          ,STATE)
        ,A))
    (defthmd evfn-meta-extract-contextual-badguy-sufficient
      (implies (evfn-meta-extract-contextual-facts a)
        (evfn (meta-extract-contextual-fact obj mfc state) a))
      :hints (("goal" :use evfn-meta-extract-contextual-badguy
         :in-theory (disable meta-extract-contextual-fact))))
    (defmacro evfn-meta-extract-global-facts
      (&key (state 'state))
      `(evfn (meta-extract-global-fact+ (mv-nth 0 (evfn-meta-extract-global-badguy ,STATE))
          (mv-nth 1 (evfn-meta-extract-global-badguy ,STATE))
          ,STATE)
        (evfn-falsify (meta-extract-global-fact+ (mv-nth 0 (evfn-meta-extract-global-badguy ,STATE))
            (mv-nth 1 (evfn-meta-extract-global-badguy ,STATE))
            ,STATE))))
    (defthmd evfn-meta-extract-global-badguy-sufficient
      (implies (evfn-meta-extract-global-facts)
        (evfn (meta-extract-global-fact+ obj st state) a))
      :hints (("goal" :use ((:instance evfn-meta-extract-global-badguy) (:instance evfn-falsify
             (x (meta-extract-global-fact+ obj st state))))
         :in-theory (disable meta-extract-global-fact))))
    (defthm evfn-meta-extract-global-badguy-true-listp
      (true-listp (evfn-meta-extract-global-badguy state))
      :hints (("goal" :use evfn-meta-extract-global-badguy))
      :rule-classes (:rewrite :type-prescription))
    (local (in-theory (enable evfn-meta-extract-global-badguy-sufficient
          evfn-meta-extract-contextual-badguy-sufficient)))
    (local (in-theory (disable meta-extract-global-fact
          meta-extract-contextual-fact)))
    (local (make-event (let ((rule (find-matching-rule :dont-care :dont-care :dont-care '(evfn (cons (car x) (kwote-lst (evlst-fn (cdr x) a))) 'nil)
               (getprop 'evfn 'lemmas nil 'current-acl2-world (w state)))))
          (prog2$ (or rule
              (er hard?
                'def-meta-extract
                "Couldn't find fncall on args rule for ~x0~%"
                'evfn))
            `(add-default-hints '((and stable-under-simplificationp
                 '(:in-theory (enable ,RULE evfn-falsify-sufficient)))))))))
    (local (make-event `(in-theory (enable ,(EV-FIND-FNCALL-RULE 'EVFN 'TYPESPEC-CHECK (W STATE))
            ,(EV-FIND-FNCALL-RULE 'EVFN 'IF (W STATE))
            ,(EV-FIND-FNCALL-RULE 'EVFN 'EQUAL (W STATE))
            ,(EV-FIND-FNCALL-RULE 'EVFN 'NOT (W STATE))
            ,(EV-FIND-FNCALL-RULE 'EVFN 'IFF (W STATE))
            ,(EV-FIND-FNCALL-RULE 'EVFN 'IMPLIES (W STATE))
            ,(EV-LST-FIND-CONS-RULE 'EVLST-FN (W STATE))
            ,(EV-LST-FIND-ATOM-RULE 'EVLST-FN (W STATE))
            ,(EV-FIND-QUOTE-RULE 'EVFN (W STATE))
            ,(EV-FIND-VARIABLE-RULE 'EVFN (W STATE))
            ,(EV-FIND-LAMBDA-RULE 'EVFN (W STATE))
            ,(EV-FIND-NONSYMBOL-ATOM-RULE 'EVFN (W STATE))
            ,(EV-FIND-BAD-FNCALL-RULE 'EVFN (W STATE))))))
    (def-functional-instance evfn-meta-extract-typeset
      mextract-typeset
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw+-equal
      mextract-rw+-equal
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw+-iff
      mextract-rw+-iff
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw+-equiv
      mextract-rw+-equiv
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw-equal
      mextract-rw-equal
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw-iff
      mextract-rw-iff
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-rw-equiv
      mextract-rw-equiv
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-mfc-ap
      mextract-mfc-ap
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-relieve-hyp
      mextract-relieve-hyp
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-contextual-badguy evfn-meta-extract-contextual-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-formula
      mextract-formula
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-lemma-term
      mextract-lemma-term
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-lemma
      mextract-lemma
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-linear-lemma-term
      mextract-linear-lemma-term
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-linear-lemma
      mextract-linear-lemma
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-fncall-logic
      mextract-fncall-logic
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-fncall
      mextract-fncall
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-magic-ev
      mextract-ev-magic-ev
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-magic-ev-lst
      mextract-ev-magic-ev-lst
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-meta-extract-fn-check-def
      mextract-ev-fn-check-def
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-lst-of-pairlis
      ev-lst-of-pairlis
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-lst-of-pairlis-append-rest
      ev-lst-of-pairlis-append-rest
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))
    (def-functional-instance evfn-lst-of-pairlis-append-head-rest
      ev-lst-of-pairlis-append-head-rest
      ((mextract-ev evfn) (mextract-ev-lst evlst-fn)
        (mextract-ev-falsify evfn-falsify)
        (mextract-global-badguy evfn-meta-extract-global-badguy))
      :translate nil
      :macro-subst ((mextract-ev-global-facts evfn-meta-extract-global-facts) (mextract-ev-contextual-facts evfn-meta-extract-contextual-facts)))))
meta-extract-replace-symfunction
(defun meta-extract-replace-sym
  (from to x)
  (let* ((name (symbol-name x)) (pos (search from name)))
    (if pos
      (let* ((pre (subseq name 0 pos)) (post (subseq name (+ pos (length from)) nil)))
        (intern-in-package-of-symbol (concatenate 'string pre (symbol-name to) post)
          to))
      x)))
meta-extract-replace-evfnmutual-recursion
(mutual-recursion (defun meta-extract-replace-evfn
    (evfn evlst-fn x)
    (declare (xargs :mode :program))
    (if (atom x)
      (if (symbolp x)
        (meta-extract-replace-sym "EVLST-FN"
          evlst-fn
          (meta-extract-replace-sym "EVFN" evfn x))
        x)
      (meta-extract-replace-evfn-list evfn evlst-fn x)))
  (defun meta-extract-replace-evfn-list
    (evfn evlst-fn x)
    (if (atom x)
      nil
      (cons (meta-extract-replace-evfn evfn evlst-fn (car x))
        (meta-extract-replace-evfn-list evfn evlst-fn (cdr x))))))
def-meta-extractmacro
(defmacro def-meta-extract
  (evfn evlst-fn)
  (meta-extract-replace-evfn evfn
    evlst-fn
    *def-meta-extract-events*))
in-theory
(in-theory (disable meta-extract-contextual-fact
    meta-extract-global-fact))
local
(local (defmacro localize-example
    (name &rest events)
    `(encapsulate nil
      (value-triple ',NAME)
      (local (progn . ,EVENTS))
      (value-triple ',NAME))))
local
(local (localize-example using-typeset-and-type-alist
    (defthm nth-when-symbolp
      (implies (symbolp n) (equal (nth n x) (car x)))
      :rule-classes nil)
    (defevaluator nthmeta-ev
      nthmeta-ev-lst
      ((typespec-check ts x) (if a
          b
          c)
        (equal a b)
        (not a)
        (iff a b)
        (implies a b)
        (nth n x)
        (car x))
      :namedp t)
    (def-meta-extract nthmeta-ev nthmeta-ev-lst)
    (defun nth-symbolp-metafn
      (term mfc state)
      (declare (xargs :stobjs state))
      (case-match term
        (('nth n x) (if (equal (mfc-ts n mfc state :forcep nil) *ts-symbol*)
            `(car ,X)
            (prog2$ (cw "Oops, the typeset of n is ~x0~%"
                (mfc-ts n mfc state :forcep nil))
              term)))
        (& term)))
    (defthm nth-symbolp-meta
      (implies (nthmeta-ev-meta-extract-contextual-facts a)
        (equal (nthmeta-ev term a)
          (nthmeta-ev (nth-symbolp-metafn term mfc state) a)))
      :hints (("goal" :use ((:instance nthmeta-ev-meta-extract-typeset
            (term (cadr term))))
         :in-theory (disable nthmeta-ev-meta-extract-typeset)))
      :rule-classes ((:meta :trigger-fns (nth))))
    (defmacro nth-symbolp-test
      (n)
      `(encapsulate nil
        (local (progn (encapsulate (((foo *) => *) ((bar *) => *) ((baz *) => *))
              (local (defun foo (x) (declare (ignore x)) t))
              (local (defun bar (x) (symbolp x)))
              (local (defun baz (x) (symbolp x)))
              (defthm foo-type
                (symbolp (foo x))
                :rule-classes :type-prescription)
              (defthm bar-booleanp
                (booleanp (bar x))
                :rule-classes :type-prescription)
              (defthm bar-implies-symbolp
                (implies (bar x) (symbolp x))
                :rule-classes :compound-recognizer)
              (defthm baz-implies-symbolp
                (implies (baz x) (symbolp x))
                :rule-classes :forward-chaining))
            (make-event (mv-let (erp val state)
                (defthm nth-foo (equal (nth (foo x) y) (car y)))
                (declare (ignore val))
                (if erp
                  (prog2$ (cw "FOO failed~%")
                    (value '(value-triple ':foo-failed)))
                  (prog2$ (cw "FOO passed~%")
                    (value '(value-triple ':foo-passed))))))
            (make-event (mv-let (erp val state)
                (defthm nth-when-bar
                  (implies (bar x) (equal (nth x y) (car y))))
                (declare (ignore val))
                (if erp
                  (prog2$ (cw "BAR failed~%")
                    (value '(value-triple ':bar-failed)))
                  (prog2$ (cw "BAR passed~%")
                    (value '(value-triple ':bar-passed))))))
            (make-event (mv-let (erp val state)
                (defthm nth-when-baz
                  (implies (baz x) (equal (nth x y) (car y))))
                (declare (ignore val))
                (if erp
                  (prog2$ (cw "BAZ failed~%")
                    (value '(value-triple ':baz-failed)))
                  (prog2$ (cw "BAZ passed~%")
                    (value '(value-triple ':baz-passed))))))))
        (value-triple '(nth-symbol-test ,N))))
    (nth-symbolp-test 1)
    (defthm type-alistp-of-mfc-type-alist
      (type-alistp (mfc-type-alist mfc)))
    (in-theory (disable mfc-type-alist))
    (encapsulate nil
      (local (defthm alistp-when-type-alistp
          (implies (type-alistp x) (alistp x))))
      (defthm alistp-of-mfc-type-alist
        (alistp (mfc-type-alist mfc))))
    (local (defthm assoc-equal-when-alistp
        (implies (alistp x)
          (iff (consp (assoc-equal a x)) (assoc-equal a x)))))
    (defthm cdr-assoc-equal-when-type-alistp
      (implies (type-alistp x)
        (iff (consp (cdr (assoc-equal a x))) (assoc-equal a x))))
    (in-theory (disable nth nth-symbolp-meta))
    (nth-symbolp-test 2)))
local
(local (localize-example using-mfc-rw+
    (encapsulate (((foo *) => *) ((bar *) => *) ((baz *) => *))
      (set-ignore-ok t)
      (set-irrelevant-formals-ok t)
      (local (defun foo (x) nil))
      (local (defun bar (x) nil))
      (local (defun baz (x) nil))
      (defthm bar-of-foo (equal (bar (foo x)) (bar x)))
      (defthm foo-of-baz (equal (foo (baz x)) (foo x))))
    (make-event (b* (((mv erp & state) (defthm bar-of-baz-fails (equal (bar (baz x)) (bar x)))))
        (if erp
          (value '(value-triple :failed))
          (er soft 'bar-of-baz-fails "Proof unexpectedly succeeded"))))
    (defevaluator foobar-ev
      foobar-ev-lst
      ((typespec-check ts x) (if a
          b
          c)
        (equal a b)
        (not a)
        (iff a b)
        (implies a b)
        (foo x)
        (bar x))
      :namedp t)
    (def-meta-extract foobar-ev foobar-ev-lst)
    (defun reduce-bar-with-foo
      (x mfc state)
      (declare (xargs :stobjs state))
      (case-match x
        (('bar xx . &) (let* ((xxx (case-match xx
                 (('foo xxx . &) (prog2$ (cw "note: reduce-bar-with-foo caught xx not in ~
                                 normal form: ~x0~%"
                       xx)
                     xxx))
                 (& xx))) (foo-xxx-rw (mfc-rw+ '(foo xxx)
                  `((xxx . ,XXX))
                  '?
                  nil
                  mfc
                  state
                  :forcep nil))
              (y (case-match foo-xxx-rw (('foo y . &) y) (& foo-xxx-rw))))
            `(bar ,Y)))
        (& x)))
    (encapsulate nil
      (local (defthm bar-of-foo-free
          (implies (equal x (foo y)) (equal (bar x) (bar y)))))
      (make-event (b* (((mv erp & state) (defthm bar-of-baz-fails (equal (bar (baz x)) (bar x)))))
          (if erp
            (value '(value-triple :failed))
            (er soft 'bar-of-baz-fails "Proof unexpectedly succeeded"))))
      (defthm reduce-bar-with-foo-meta
        (implies (foobar-ev-meta-extract-contextual-facts a)
          (equal (foobar-ev x a)
            (foobar-ev (reduce-bar-with-foo x mfc state) a)))
        :hints (("goal" :use ((:instance foobar-ev-meta-extract-rw+-equal
              (term '(foo xxx))
              (alist (let ((xx (cadr x)))
                  `((xxx . ,(CASE-MATCH XX (('FOO XXX . &) XXX) (& XX))))))
              (obj '?)) (:instance bar-of-foo
               (x (foobar-ev (let ((xx (cadr x)))
                     (case-match xx (('foo xxx . &) xxx) (& xx)))
                   a))))
           :in-theory (e/d (sublis-var)
             (foobar-ev-meta-extract-rw+-equal bar-of-foo))))
        :rule-classes ((:meta :trigger-fns (bar)))))
    (defthm bar-of-baz (equal (bar (baz x)) (bar x)))))
meta-extract-formula-wfunction
(defund meta-extract-formula-w
  (name wrld)
  (declare (xargs :guard (and (symbolp name) (plist-worldp wrld))))
  (or (getprop name 'theorem nil 'current-acl2-world wrld)
    (cond ((logicp name wrld) (mv-let (flg prop)
          (pre-v8-7-constraint-info name wrld)
          (cond ((unknown-constraints-p prop) *t*)
            (flg (ec-call (conjoin prop)))
            (t prop))))
      (t *t*))))
meta-extract-formula-w-rewritetheorem
(defthm meta-extract-formula-w-rewrite
  (equal (meta-extract-formula-w name (w state))
    (meta-extract-formula name state))
  :hints (("Goal" :in-theory (enable meta-extract-formula-w meta-extract-formula))))
fn-get-def-wfunction
(defund fn-get-def-w
  (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (b* (((when (eq fn 'quote)) (mv nil nil nil)) (formula (meta-extract-formula-w fn wrld))
      ((unless-match formula
         (equal ((:! fn) :? formals) (:? body))) (mv nil nil nil))
      ((unless (and (symbol-listp formals)
           (not (member-eq nil formals))
           (no-duplicatesp-eq formals))) (mv nil nil nil)))
    (mv t formals body)))
fn-get-def-w-rewritetheorem
(defthm fn-get-def-w-rewrite
  (equal (fn-get-def-w name (w state))
    (fn-get-def name state))
  :hints (("Goal" :in-theory (enable fn-get-def fn-get-def-w))))
fn-check-def-wfunction
(defund fn-check-def-w
  (fn wrld formals body)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (b* (((mv ok fformals fbody) (fn-get-def-w fn wrld)))
    (and ok (equal fformals formals) (equal fbody body))))
fn-check-def-w-rewritetheorem
(defthm fn-check-def-w-rewrite
  (equal (fn-check-def-w name (w state) formals body)
    (fn-check-def name state formals body))
  :hints (("Goal" :in-theory (enable fn-check-def fn-check-def-w))))
local
(local (localize-example using-fncall
    (defevaluator fnc-ev
      fnc-ev-lst
      ((typespec-check ts x) (if a
          b
          c)
        (equal a b)
        (not a)
        (iff a b)
        (implies a b)))
    (defun unquote-lst
      (x)
      (declare (xargs :guard (and (pseudo-term-listp x) (quote-listp x))))
      (if (atom x)
        nil
        (cons (unquote (car x)) (unquote-lst (cdr x)))))
    (defthm kwote-lst-of-unquote-lst-when-quote-listp
      (implies (and (quote-listp x) (pseudo-term-listp x))
        (equal (kwote-lst (unquote-lst x)) x)))
    (defthm fnc-ev-list-when-quote-listp
      (implies (quote-listp x)
        (equal (fnc-ev-lst x a) (unquote-lst x))))
    (defun ev-call-metafn
      (x mfc state)
      (declare (xargs :guard (pseudo-termp x) :stobjs state)
        (ignorable mfc))
      (if (and (consp x)
          (symbolp (car x))
          (not (eq (car x) 'quote))
          (quote-listp (cdr x))
          (mbt (pseudo-term-listp (cdr x))))
        (mv-let (erp val)
          (magic-ev-fncall-logic (car x) (unquote-lst (cdr x)) state)
          (if erp
            x
            (kwote val)))
        x))
    (def-meta-extract fnc-ev fnc-ev-lst)
    (defthm ev-call-metafn-correct
      (implies (fnc-ev-meta-extract-global-facts)
        (equal (fnc-ev (ev-call-metafn x mfc state) a) (fnc-ev x a)))
      :hints (("Goal" :in-theory (enable fnc-ev-constraint-0))))
    (defun fib
      (x)
      (if (or (zp x) (eql x 1))
        1
        (+ (fib (- x 1)) (fib (- x 2)))))
    (in-theory (disable fib (fib)))
    (defun fib-hyp-metafn
      (x mfc state)
      (declare (xargs :guard (pseudo-termp x) :stobjs state)
        (ignorable mfc state))
      (if (and (consp x)
          (eq (car x) 'fib)
          (quotep (cadr x))
          (< (nfix (cadr (cadr x))) 10))
        *t*
        *nil*))
    (defthm ev-call-metafn-for-fib
      (implies (and (fnc-ev-meta-extract-global-facts)
          (fnc-ev (fib-hyp-metafn x mfc state) a))
        (equal (fnc-ev x a) (fnc-ev (ev-call-metafn x mfc state) a)))
      :hints (("Goal" :in-theory (disable ev-call-metafn)))
      :rule-classes ((:meta :trigger-fns (fib))))
    (defthm fib-9 (equal (fib 9) 55))))
other
(defevaluator mx-ev
  mx-ev-lst
  ((typespec-check ts x) (if a
      b
      c)
    (equal a b)
    (not a)
    (iff a b)
    (implies a b)))
other
(defxdoc magic-ev
  :parents (meta)
  :short "Evaluate a term under a ground substitution using @(see magic-ev-fncall)."
  :long "<p>Invocation:</p>
@({
 (magic-ev term alist state hard-error-returns-nilp aokp)
 })

<p>evaluates the given term under the alist mapping variables to values.
Functions within the term are evaluated using @(see magic-ev-fncall) and the
values returned are the same as for @(see magic-ev-fncall), that is,</p>
@({
 (mv NIL value)
 })
<p>on success or</p>
@({
 (mv T error-msg)
 })
<p>on failure.</p>")
other
(defxdoc magic-ev-lst
  :parents (magic-ev)
  :short "Evaluate a list of terms using @(see magic-ev).")
other
(defxdoc fn-get-def
  :parents (meta-extract)
  :short "Look up a function's definition from the world."
  :long "<p>Invocation:</p>
@({
 (fn-get-def fnname state)
 })
<p>or equivalently,if @('world') is @('(w state)'),</p>
@({
 (fn-get-def-w fnname world)
 })

<p>produces @('(mv successp formals body)'), where if @('successp') is true,
then @('(fnname . formals)') is equal to @('body') under evaluation.</p>

<p>@('fn-get-def') can be assumed to work correctly in the context of
metafunctions and clause processors via @(see meta-extract).</p>

<p>The @(see def-meta-extract) macro supports @('fn-get-def') indirectly: we
rewrite the @('successp') return value to a call of @('fn-check-def'), and
@('def-meta-extract') provides a theorem that rewrites an evaluation of
@('(fnname . args)') to the evaluation of @('body') under the pairing of
@('formals') to @('args') when it can relieve the hypothesis</p>
@({
 (fn-check-def fnname state formals body).
 })")
other
(defpointer fn-check-def fn-get-def)
local
(local (progn (make-event (let ((curr-preprocess (cdr (assoc 'untranslate-preprocess
               (table-alist 'user-defined-functions-table (w state))))))
        `(defun my-preprocess
          (term wrld)
          (declare (ignorable wrld)
            (xargs :mode :program))
          (cond ((equal term
               '(mx-ev (meta-extract-global-fact+ (mv-nth '0 (mx-ev-meta-extract-global-badguy state))
                   (mv-nth '1 (mx-ev-meta-extract-global-badguy state))
                   state)
                 (mx-ev-falsify (meta-extract-global-fact+ (mv-nth '0 (mx-ev-meta-extract-global-badguy state))
                     (mv-nth '1 (mx-ev-meta-extract-global-badguy state))
                     state)))) '(mx-ev-meta-extract-global-facts))
            ((equal term
               '(mx-ev (meta-extract-contextual-fact (mx-ev-meta-extract-contextual-badguy a mfc state)
                   mfc
                   state)
                 a)) '(mx-ev-meta-extract-contextual-facts a))
            ((and (consp term)
               (equal (car term)
                 '(lambda (x l)
                   (return-last 'mbe1-raw
                     (member-eql-exec x l)
                     (return-last 'progn
                       (member-eql-exec$guard-check x l)
                       (member-equal x l)))))) (cons 'member (cdr term)))
            ((and (consp term)
               (equal (car term)
                 '(lambda (x)
                   (return-last 'mbe1-raw
                     (no-duplicatesp-eql-exec x)
                     (return-last 'progn
                       (no-duplicatesp-eql-exec$guard-check x)
                       (no-duplicatesp-equal x)))))) (cons 'no-duplicatesp (cdr term)))
            (t ,(IF CURR-PREPROCESS
     `(,CURR-PREPROCESS TERM WRLD)
     'TERM))))))
    (table user-defined-functions-table
      'untranslate-preprocess
      'my-preprocess)))
other
(def-meta-extract mx-ev mx-ev-lst)
other
(defxdoc def-meta-extract
  :parents (meta-extract)
  :short "Generate macros and theorems convenient for using @(see meta-extract) with a given evaluator."
  :long "<p>Using the @(see meta-extract) feature in proofs of meta rules and
clause processors is fairly inconvenient when starting from scratch.
Def-meta-extract generates a set of theorems for a given evaluator that are
a more convenient starting point for reasoning about meta-extract.</p>

<p>Usage:</p>

@({
 (defevaluator mx-ev mx-ev-lst
   ((typespec-check ts x)
    (if a b c)
    (equal a b)
    (not a)
    (iff a b)
    (implies a b)
    ...))   ;; other functions as needed for the application

 (def-meta-extract mx-ev mx-ev-lst)
 })

<p>We will use the above invocation on @('mx-ev') as an example;
@('def-meta-extract') should be applicable to any evaluator that supports the
six functions listed in the defevaluator form above.</p>

<p>The above invocation of @('def-meta-extract') produces two macros that
expand to well-formed meta-extract hypotheses:</p>
@({
 (mx-ev-meta-extract-contextual-facts a :mfc mfc :state state)
 (mx-ev-meta-extract-global-facts :state state)
 })
<p>(Note: The keyword arguments listed default to the variable names @('mfc')
and @('state'), which are usually the right arguments.)</p>

<p>The exact meta-extract hypotheses produced use a bad-guy function as the
@('obj') argument to the meta-extract function, and for the global macro, for
the @('st') argument to @('meta-extract-global-fact+'), so that they
effectively universally quantify them, as shown by the following two theorems:</p>
@(def mx-ev-meta-extract-contextual-badguy-sufficient)
@(def mx-ev-meta-extract-global-badguy-sufficient)

<p>However, @('def-meta-extract') proves several theorems for the given
evaluator so that the user doesn't need to reason directly about invocations of
@(see meta-extract-contextual-fact) and @(see meta-extract-global-fact+).  For
example, to show that an invocation of @('meta-extract-formula') is true under
@('mx-ev'), you could prove:</p>
@({
  (implies (and (mx-ev (meta-extract-global-fact+ (list :formula name) st state) a)
                (equal (w st) (w state)))
           (mx-ev (meta-extract-formula name st) a))
})
<p>But the following theorem proved by @('def-meta-extract') obviates the need
to reason directly about @(see meta-extract-global-fact+) and provide the correct
@('obj = (list :formula name)') in this manner:</p>
@({
  (implies (and (mx-ev-meta-extract-global-facts)
                (equal (w st) (w state)))
           (mx-ev (meta-extract-formula name st) a))
 })

<p>(Note: @('st'), the state from which the formula is extracted, and
@('state'), the original state on which the metafunction or clause processor
was invoked, may differ in the case of a clause processor because the clause
processor can update state.  As long as the @('w') field (holding the ACL2
logical world) of the state is not updated, global facts can still be extracted
from the state and assumed correct.)</p>

<h3>List of theorems proved by @('def-meta-extract')</h3>

<h4>Typset reasoning with @(see mfc-ts)</h4>
<p>The following theorem allows the user to conclude that a typeset returned by
@(see mfc-ts) correctly describes the type of a term:</p>
@(def mx-ev-meta-extract-typeset)

<h4>Rewriting with @(see mfc-rw) and under substitution with @(see mfc-rw+)</h4>
<p>The following six theorems allow the user to conclude that a call of @(see
mfc-rw) returns an equivalent term, or that a call of @(see mfc-rw+) returns a
term equivalent to the substitution of @('alist') into @('term'), with the
equivalence given by the @('equiv-info') argument provided (@('nil') for
equality, @('t') for @('iff'), or the name of an equivalence relation):</p>
@(def mx-ev-meta-extract-rw-equal)
@(def mx-ev-meta-extract-rw-iff)
@(def mx-ev-meta-extract-rw-equiv)
@(def mx-ev-meta-extract-rw+-equal)
@(def mx-ev-meta-extract-rw+-iff)
@(def mx-ev-meta-extract-rw+-equiv)

<h4>Detecting linear arithmetic contradictions with @(see mfc-ap)</h4>
<p>The following theorem allows the user to conclude that a term is false under
the given environment @('a') when @(see mfc-ap) returns @('t') indicating a
linear arithmetic contradiction:</p>
@(def mx-ev-meta-extract-mfc-ap)

<h4>Proving terms true with @(see mfc-relieve-hyp)</h4>
@(def mx-ev-meta-extract-relieve-hyp)

<h4>Looking up formulas by name using @(see meta-extract-formula)</h4>
<p>(Note: @('meta-extract-formula') can be used to look up a theorem,
definition of a defined function, or constraint of a constrained function.)</p>
@(def mx-ev-meta-extract-formula)

<h4>Looking up rewrite rules from a @('lemmas') property</h4>
<p>The following two theorems conclude that a rewrite rule extracted from a
function's @('lemmas') property is valid (the second somewhat more explicitly
than the first):</p>
@(def mx-ev-meta-extract-lemma-term)
@(def mx-ev-meta-extract-lemma)

<h4>Calling a function with @(see magic-ev-fncall)</h4>
@(def mx-ev-meta-extract-fncall)

<h4>Evaluating a term with @(see magic-ev) or termlist with @(see magic-ev-lst)</h4>
@(def mx-ev-meta-extract-magic-ev)
@(def mx-ev-meta-extract-magic-ev-lst)

<h4>Looking up a function definition with @(see fn-get-def)</h4>
<p>The following theorem allows a function call to be expaneded to its body
when the function definition is successfully looked up in the world with @(see
fn-get-def).  Note: The term @('(mv-nth 0 (fn-get-def ...))') indicating
success of the @(see fn-get-def) call is rewritten to the call of @(see
fn-check-def):</p>
@(def mx-ev-meta-extract-fn-check-def)

<h4>Technical lemmas about pairing formals with actuals</h4>
<p>The following three theorems may help in reasoning about expansions of
function calls and lambdas:</p>
@(def mx-ev-lst-of-pairlis)
@(def mx-ev-lst-of-pairlis-append-rest)
@(def mx-ev-lst-of-pairlis-append-head-rest)")