A
Function:
(defun abstract-rule (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (prog2$ (abstract-fail) (rule (rulename "") nil nil))) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (and (consp treess) (consp (cdr treess)) (consp (cddr treess)))) (fail)) (trees-rulename (car treess)) (trees-defined-as (cadr treess)) (trees-elements (caddr treess)) ((unless (consp trees-rulename)) (fail)) (tree-rulename (car trees-rulename)) ((unless (consp trees-defined-as)) (fail)) (tree-defined-as (car trees-defined-as)) ((unless (consp trees-elements)) (fail)) (tree-elements (car trees-elements)) (rulename (abstract-rulename tree-rulename)) (incremental (abstract-defined-as tree-defined-as)) (alternation (abstract-elements tree-elements))) (make-rule :name rulename :incremental incremental :definiens alternation)))
Theorem:
(defthm rulep-of-abstract-rule (b* ((rule (abstract-rule tree))) (rulep rule)) :rule-classes :rewrite)