• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
        • Defun-inst
        • Defequal
        • Defsoft
        • Defthm-inst
        • Defun2
        • Defunvar
        • Defun-sk2
        • Defchoose2
        • Defthm-2nd-order
        • Define-sk2
        • Defund-sk2
        • Define2
        • Defund2
      • Updates-to-workshop-material
      • Soft-implementation
      • Soft-notions
    • 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

• Soft-macros
• Second-order-theorems

Defthm-2nd-order

Introduce a second-order theorem.

General Form

(defthm sothm ...) ; a regular defthm

This is a normal defthm. SOFT does not provide macros for introducing second-order theorems, at this time.

Inputs

The inputs are the ones of defthm.

Generated Events

The defthm itself.

Examples

Example 1

;; Homomorphically lift ?F to on true lists of ?P values:
(defun2 map[?f][?p] (l)
  (declare (xargs :guard (all[?p] l)))
  (cond ((endp l) nil)
        (t (cons (?f (car l)) (map[?f][?p] (cdr l))))))

;; The homomorphic lifting of ?F to lists of ?P values
;; preserves the length of the list,
;; for every function ?F and predicate ?P:
(defthm len-of-map[?f][?p]
  (equal (len (map[?f][?p] l)) (len l)))

Example 2

;; Recognize injective functions:
(defun-sk2 injective[?f] ()
  (forall (x y) (implies (equal (?f x) (?f y)) (equal x y))))

;; The four-fold application of an injective function is injective:
(defthm injective[quad[?f]]-when-injective[?f]
  (implies (injective[?f]) (injective[quad[?f]]))
  :hints ...)

Example 3

;; Folding function on binary trees:
(defun2 fold[?f][?g] (bt)
  (cond ((atom bt) (?f bt))
        (t (?g (fold[?f][?g] (car bt)) (fold[?f][?g] (cdr bt))))))

;; Abstract input/output relation:
(defunvar ?io (* *) => *)

;; Recognize functions ?F that satisfy the input/output relation on atoms:
(defun-sk2 atom-io[?f][?io] ()
  (forall x (implies (atom x) (?io x (?f x))))
  :rewrite :direct)

;; Recognize functions ?G that satisfy
;; the input/output relation on CONSP pairs
;; when the arguments are valid outputs for the CAR and CDR components:
(defun-sk2 consp-io[?g][?io] ()
  (forall (x y1 y2)
          (implies (and (consp x) (?io (car x) y1) (?io (cdr x) y2))
                   (?io x (?g y1 y2))))
  :rewrite :direct)

;; The generic folding function on binary trees
;; satisfies the input/output relation
;; when its function parameters satisfy the predicates just introduced:
(defthm fold-io[?f][?g][?io]
  (implies (and (atom-io[?f][?io]) (consp-io[?g][?io]))
           (?io x (fold[?f][?g] x))))