Disambiguate a label.
(dimb-label label table) → (mv erp new-label new-table)
This may affect the disambiguation table, for a label that is a constant expression.
Function:
(defun dimb-label (label table) (declare (xargs :guard (and (labelp label) (dimb-tablep table)))) (let ((__function__ 'dimb-label)) (declare (ignorable __function__)) (b* (((reterr) (irr-label) (irr-dimb-table))) (label-case label :name (retok (label-fix label) (dimb-table-fix table)) :const (b* (((erp new-cexpr table) (dimb-const-expr label.unwrap table))) (retok (label-const new-cexpr) table)) :default (retok (label-fix label) (dimb-table-fix table))))))
Theorem:
(defthm labelp-of-dimb-label.new-label (b* (((mv acl2::?erp ?new-label ?new-table) (dimb-label label table))) (labelp new-label)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-label.new-table (b* (((mv acl2::?erp ?new-label ?new-table) (dimb-label label table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm label-unambp-of-dimb-label (b* (((mv acl2::?erp ?new-label ?new-table) (dimb-label label table))) (implies (not erp) (label-unambp new-label))))
Theorem:
(defthm dimb-label-of-label-fix-label (equal (dimb-label (label-fix label) table) (dimb-label label table)))
Theorem:
(defthm dimb-label-label-equiv-congruence-on-label (implies (label-equiv label label-equiv) (equal (dimb-label label table) (dimb-label label-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-label-of-dimb-table-fix-table (equal (dimb-label label (dimb-table-fix table)) (dimb-label label table)))
Theorem:
(defthm dimb-label-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-label label table) (dimb-label label table-equiv))) :rule-classes :congruence)