• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Defomap
      • 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
      • Deffixequiv-mutual
      • Fty::baselists
      • 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
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deffixequiv-sk-implementation

Deffixequiv-sk-lemma-insts-arg

Generate lemma instances to prove the fixing of an argument.

Signature

(deffixequiv-sk-lemma-insts-arg fn-rule fn-witness 
                                bvars args-names arg-name arg-fix) 
 
  → 
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).

arg-name — Guard (symbolp arg-name).

arg-fix — Guard (symbolp arg-fix).

Returns

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

Each argument of the function has some associated lemma instances, which are then used in the hints to prove the fixing of the argument. This code generates the lemma instances for the argument whose name is arg-name and whose fixer is arg-fix (meaning the fixer for the type for the predicate paired to the argument in the :args input.

Definitions and Theorems

Function: deffixequiv-sk-lemma-insts-arg

(defun deffixequiv-sk-lemma-insts-arg
       (fn-rule fn-witness
                bvars args-names arg-name arg-fix)
 (declare (xargs :guard (and (symbolp fn-rule)
                             (symbolp fn-witness)
                             (symbol-listp bvars)
                             (symbol-listp args-names)
                             (symbolp arg-name)
                             (symbolp arg-fix))))
 (declare (xargs :guard (not (eq fn-witness 'quote))))
 (let ((__function__ 'deffixequiv-sk-lemma-insts-arg))
  (declare (ignorable __function__))
  (b*
   ((call1 (acl2::fcons-term fn-witness args-names))
    (call2 (acl2::fcons-term fn-witness
                             (subst (list arg-fix arg-name)
                                    arg-name args-names)))
    (instance1
     (cons
      ':instance
      (cons
        fn-rule
        (cons (cons arg-name
                    (cons (cons arg-fix (cons arg-name 'nil))
                          'nil))
              (if (= (len bvars) 1)
                  (list (list (car bvars) call1))
                (deffixequiv-sk-lemma-inst-subst bvars 0 call1))))))
    (instance2
     (cons
        ':instance
        (cons fn-rule
              (if (= (len bvars) 1)
                  (list (list (car bvars) call2))
                (deffixequiv-sk-lemma-inst-subst bvars 0 call2))))))
   (list instance1 instance2))))

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

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