Recommendations for writing understandable rule names.
Do not non-locally use common names for local lemmas, such as:
lemma* crock* crux* a0 b0 c0 ... temp* goal* main-goal* a1 b1 c1 stupid* wtf* corollary* ...
Using the above names may make your book hard to include for people who (perhaps via macros) are already using these names or who may want to use them.
(defthm append-of-cons (equal (append (cons a x) y) (cons a (append x y)))) (defthm true-listp-of-append (equal (true-listp (append x y)) (true-listp y)))
(defthm consp-of-cons (consp (cons x y)))
(defthm member-when-atom ;; lhs is (member a x) (implies (atom x) (not (member a x)))) (defthm logbitp-of-0-when-bitp (implies (bitp b) (equal (logbitp 0 b) (equal b 1))))
(defthm append-under-iff ;; lhs is (append x y) (iff (append x y) (or (consp x) y))) (defthm union-equal-under-set-equiv ;; lhs is (union-equal a b) (set-equiv (union-equal a b) (append a b)))
Obviously you can take this too far. For complex theorems, these recommendations would lead to names that are far too long. Think of them as a starting point, not a mandate.
Following these conventions can help lead to more consistently named rules whose effect may be more easy to guess.