% For HTML
(defstep use-lemma (lemma &optional subst (if-match best))
(then (use lemma :subst subst :if-match if-match)
(if *new-fmla-nums*
(let ((fnum (car *new-fmla-nums*)))
(spread (split fnum)
((then (let ((fnums *new-fmla-nums*))
(flatten fnums))
(let ((new-fnums *new-fmla-nums*))
(then (replace* new-fnums)
(delete new-fnums)))))))
(skip)))
"Introduce LEMMA instance, then does BETA, INST?, and SPLIT on this,
and then on the main branch a REPLACE* followed by a deletion of any
remnants of the lemma."
"Using and discarding")
(defun cleanup-fnums (fnums)
(cond ((consp fnums)(loop for fnum in fnums
collect (if (stringp fnum)
(intern fnum)
fnum)))
((stringp fnums) (list (intern fnums)))
((memq fnums '(* + -)) fnums)
(t (list fnums))))
(defun gather-fnums (sforms yesnums nonums
&optional (pred #'(lambda (x) T))
(pos 1) (neg -1))
(let ((yesnums (cleanup-fnums yesnums))
(nonums (cleanup-fnums nonums)))
(gather-fnums* sforms yesnums nonums pred pos neg)))
(defun gather-fnums* (seq yesnums nonums
pred pos neg)
(cond ((null seq) nil)
((not-expr? (formula (car seq)))
(if (and (in-sformnums? (car seq) pos neg yesnums)
(not (in-sformnums? (car seq) pos neg nonums))
(funcall pred (car seq)))
(cons neg
(gather-fnums* (cdr seq) yesnums nonums pred
pos (1- neg)))
(gather-fnums* (cdr seq) yesnums nonums pred pos (1- neg))))
(t (if (and (in-sformnums? (car seq) pos neg yesnums)
(not (in-sformnums? (car seq) pos neg nonums))
(funcall pred (car seq)))
(cons pos
(gather-fnums* (cdr seq) yesnums nonums
pred (1+ pos) neg))
(gather-fnums* (cdr seq) yesnums nonums pred
(1+ pos) neg)))))
(defstep auto-rewrite-antecedents ()
(let ((fnums (gather-fnums (s-forms (current-goal *ps*))
'- nil)))
(auto-rewrite :names fnums))
"Help string with examples"
"Commentary string")