|
|
|---|
|
|
|
|---|
Introduce a second-order theorem.
(defthm sothm ...) ; a regular defthm
This is a normal defthm. SOFT does not provide macros for introducing second-order theorems, at this time.
The inputs are the ones of defthm.
The defthm itself.
;; 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)))
;; 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 ...)
;; 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))))