Generate macros and theorems convenient for using meta-extract with a given evaluator.

Using the 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.

Usage:

(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)

We will use the above invocation on

The above invocation of

(mx-ev-meta-extract-contextual-facts a :mfc mfc :state state) (mx-ev-meta-extract-global-facts :state state)

(Note: The keyword arguments listed default to the variable names

The exact meta-extract hypotheses produced use a bad-guy function as the

**Theorem: **

(defthm mx-ev-meta-extract-contextual-badguy-sufficient (implies (mx-ev-meta-extract-contextual-facts a) (mx-ev (meta-extract-contextual-fact obj mfc state) a)))

**Theorem: **

(defthm mx-ev-meta-extract-global-badguy-sufficient (implies (mx-ev-meta-extract-global-facts) (mx-ev (meta-extract-global-fact+ obj st state) a)))

However,

(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))

But the following theorem proved by

(implies (and (mx-ev-meta-extract-global-facts) (equal (w st) (w state))) (mx-ev (meta-extract-formula name st) a))

(Note:

The following theorem allows the user to conclude that a typeset returned by mfc-ts correctly describes the type of a term:

**Theorem: **

(defthm mx-ev-meta-extract-typeset (implies (mx-ev-meta-extract-contextual-facts a) (typespec-check (mfc-ts term mfc state :forcep nil) (mx-ev term a))) :rule-classes ((:rewrite)))

The following six theorems allow the user to conclude that a call of mfc-rw returns an equivalent term, or that a call of mfc-rw+ returns a
term equivalent to the substitution of

**Theorem: **

(defthm mx-ev-meta-extract-rw-equal (implies (mx-ev-meta-extract-contextual-facts a) (equal (mx-ev (mfc-rw term obj nil mfc state :forcep nil) a) (mx-ev (sublis-var nil term) a))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-rw-iff (implies (mx-ev-meta-extract-contextual-facts a) (iff (mx-ev (mfc-rw term obj t mfc state :forcep nil) a) (mx-ev (sublis-var nil term) a))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-rw-equiv (implies (and (mx-ev-meta-extract-contextual-facts a) equiv (not (equal equiv t)) (symbolp equiv) (getprop equiv 'coarsenings nil 'current-acl2-world (w state))) (mx-ev (cons equiv (cons (sublis-var nil term) (cons (mfc-rw term obj equiv mfc state :forcep nil) 'nil))) a)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-rw+-equal (implies (mx-ev-meta-extract-contextual-facts a) (equal (mx-ev (mfc-rw+ term alist obj nil mfc state :forcep nil) a) (mx-ev (sublis-var alist term) a))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-rw+-iff (implies (mx-ev-meta-extract-contextual-facts a) (iff (mx-ev (mfc-rw+ term alist obj t mfc state :forcep nil) a) (mx-ev (sublis-var alist term) a))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-rw+-equiv (implies (and (mx-ev-meta-extract-contextual-facts a) equiv (not (equal equiv t)) (symbolp equiv) (getprop equiv 'coarsenings nil 'current-acl2-world (w state))) (mx-ev (cons equiv (cons (sublis-var alist term) (cons (mfc-rw+ term alist obj equiv mfc state :forcep nil) 'nil))) a)) :rule-classes ((:rewrite)))

The following theorem allows the user to conclude that a term is false under
the given environment

**Theorem: **

(defthm mx-ev-meta-extract-mfc-ap (implies (and (mx-ev-meta-extract-contextual-facts a) (mx-ev term a)) (not (mfc-ap term mfc state :forcep nil))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-relieve-hyp (implies (and (mx-ev-meta-extract-contextual-facts a) (not (mx-ev (sublis-var alist hyp) a))) (not (mfc-relieve-hyp hyp alist rune target bkptr mfc state :forcep nil))) :rule-classes ((:rewrite)))

(Note:

**Theorem: **

(defthm mx-ev-meta-extract-formula (implies (and (mx-ev-meta-extract-global-facts) (equal (w st) (w state))) (mx-ev (meta-extract-formula name st) a)) :rule-classes ((:rewrite)))

The following two theorems conclude that a rewrite rule extracted from a
function's

**Theorem: **

(defthm mx-ev-meta-extract-lemma-term (implies (and (mx-ev-meta-extract-global-facts) (member rule (fgetprop fn 'lemmas nil (w st))) (equal (w st) (w state))) (mx-ev (rewrite-rule-term rule) a)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-lemma (implies (and (mx-ev-meta-extract-global-facts) (member rule (fgetprop fn 'lemmas nil (w st))) (not (eq (access rewrite-rule rule :subclass) 'meta)) (mx-ev (conjoin (access rewrite-rule rule :hyps)) a) (equal (w st) (w state))) (mx-ev (cons (access rewrite-rule rule :equiv) (cons (access rewrite-rule rule :lhs) (cons (access rewrite-rule rule :rhs) 'nil))) a)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-fncall (mv-let (erp val) (magic-ev-fncall fn arglist st t nil) (implies (and (mx-ev-meta-extract-global-facts) (equal (w st) (w state)) (not erp) (logicp fn (w st))) (equal val (mx-ev (cons fn (kwote-lst arglist)) nil)))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-magic-ev (mv-let (erp val) (magic-ev x alist st hard-errp aokp) (implies (and (mx-ev-meta-extract-global-facts) (equal (w st) (w state)) (not erp) (equal hard-errp t) (equal aokp nil) (pseudo-termp x)) (equal val (mx-ev x alist)))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-meta-extract-magic-ev-lst (mv-let (erp val) (magic-ev-lst x alist st hard-errp aokp) (implies (and (mx-ev-meta-extract-global-facts) (equal (w st) (w state)) (not erp) (equal hard-errp t) (equal aokp nil) (pseudo-term-listp x)) (equal val (mx-ev-lst x alist)))) :rule-classes ((:rewrite)))

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 fn-get-def. Note: The term

**Theorem: **

(defthm mx-ev-meta-extract-fn-check-def (implies (and (fn-check-def fn st formals body) (mx-ev-meta-extract-global-facts) (equal (w st) (w state)) (equal (len args) (len formals))) (equal (mx-ev (cons fn args) a) (mx-ev body (pairlis$ formals (mx-ev-lst args a))))) :rule-classes ((:rewrite)))

The following three theorems may help in reasoning about expansions of function calls and lambdas:

**Theorem: **

(defthm mx-ev-lst-of-pairlis (implies (and (no-duplicatesp keys) (symbol-listp keys) (not (member nil keys))) (equal (mx-ev-lst keys (pairlis$ keys vals)) (take (len keys) vals))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-ev-lst-of-pairlis-append-rest (implies (and (no-duplicatesp keys) (symbol-listp keys) (not (member nil keys))) (equal (mx-ev-lst keys (append (pairlis$ keys vals) rest)) (take (len keys) vals))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm mx-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 (mx-ev-lst keys (append head (pairlis$ keys vals) rest)) (take (len keys) vals))) :rule-classes ((:rewrite)))