• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Specific-types
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Defomap
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
        • Deffixequiv-sk-implementation
          • Deffixequiv-sk-lemma-insts-arg
          • Deffixequiv-sk-lemma-insts-args
          • Deffixequiv-sk-hints
          • Deffixequiv-sk-lemma-inst-subst
          • Deffixequiv-sk-fn
          • Deffixequiv-sk-macro-definition
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deffixequiv-sk-implementation

Deffixequiv-sk-lemma-insts-args

Generate lemma instances to prove the fixing of all the arguments.

Signature

(deffixequiv-sk-lemma-insts-args fn-rule fn-witness 
                                 bvars args-names args-alist wrld) 
 
  → 
lemma-instances

Arguments

fn-rule — Guard (symbolp fn-rule).

fn-witness — Guard (symbolp fn-witness).

bvars — Guard (symbol-listp bvars).

args-names — Guard (symbol-listp args-names).

args-alist — Guard (acl2::symbol-symbol-alistp args-alist).

wrld — Guard (plist-worldp wrld).

Returns

lemma-instances — Type (true-list-listp lemma-instances).

This loops through the alist of arguments and collects the lemma instances.

Definitions and Theorems

Function: deffixequiv-sk-lemma-insts-args

(defun deffixequiv-sk-lemma-insts-args
       (fn-rule fn-witness
                bvars args-names args-alist wrld)
 (declare (xargs :guard (and (symbolp fn-rule)
                             (symbolp fn-witness)
                             (symbol-listp bvars)
                             (symbol-listp args-names)
                             (acl2::symbol-symbol-alistp args-alist)
                             (plist-worldp wrld))))
 (declare (xargs :guard (not (eq fn-witness 'quote))))
 (let ((__function__ 'deffixequiv-sk-lemma-insts-args))
  (declare (ignorable __function__))
  (b*
   (((when (endp args-alist)) nil)
    (arg (car args-alist))
    (arg-name (car arg))
    (arg-pred (cdr arg))
    (arg-fty-info
         (find-fixtype-for-pred arg-pred (get-fixtypes-alist wrld)))
    (arg-fix (fixtype->fix arg-fty-info))
    (arg-lemma-instances (deffixequiv-sk-lemma-insts-arg
                              fn-rule fn-witness
                              bvars args-names arg-name arg-fix))
    (rest-lemma-instances (deffixequiv-sk-lemma-insts-args
                               fn-rule fn-witness
                               bvars args-names (cdr args-alist)
                               wrld)))
   (append arg-lemma-instances
           rest-lemma-instances))))

Theorem: true-list-listp-of-deffixequiv-sk-lemma-insts-args

(defthm true-list-listp-of-deffixequiv-sk-lemma-insts-args
  (b* ((lemma-instances (deffixequiv-sk-lemma-insts-args
                             fn-rule fn-witness
                             bvars args-names args-alist wrld)))
    (true-list-listp lemma-instances))
  :rule-classes :rewrite)