		Search-engine friendly clone of the ACL2 documentation.

Omaps

Update-induction-on-maps

Induction on omaps based on abstract characterization of update.

This is similar to the induction on osets in [books]/std/osets/primitives.lisp.

We want to do certain proofs by induction based on update, but not based on the definition of update, which involves the internal representation of omaps. Instead

Definitions and Theorems

Theorem: weak-update-induction-helper-1

(defthm weak-update-induction-helper-1
  (implies (and (mapp m)
                (not (assoc key m))
                (not (equal (mv-nth 0 (head (update key val m)))
                            key)))
           (equal (head (update key val m))
                  (head m))))

Theorem: weak-update-induction-helper-2

(defthm weak-update-induction-helper-2
  (implies (and (not (assoc key m))
                (not (equal (mv-nth 0 (head (update key val m)))
                            key)))
           (equal (tail (update key val m))
                  (update key val (tail m)))))

Theorem: weak-update-induction-helper-3

(defthm weak-update-induction-helper-3
  (implies (and (not (assoc key m))
                (equal (mv-nth 0 (head (update key val m)))
                       key))
           (equal (tail (update key val m))
                  (mfix m))))

Function: weak-update-induction

(defun weak-update-induction (key val m)
  (declare (xargs :guard (mapp m)))
  (cond ((emptyp m) nil)
        ((assoc key m) nil)
        ((equal (head-key (update key val m))
                key)
         nil)
        (t (list (weak-update-induction key val (tail m))))))

Theorem: use-weak-update-induction

(defthm use-weak-update-induction
  t
  :rule-classes
  ((:induction :pattern (update key val m)
               :scheme (weak-update-induction key val m))))