Theory "update"

Signature

Definitions

FIND_def

⊢ (∀P. FIND P [] = NONE) ∧
  ∀P h t. FIND P (h::t) = if P h then SOME h else FIND P t

OVERRIDE_primitive_def

⊢ OVERRIDE =
  WFREC (@R. WF R ∧ ∀t x. R (FILTER (λy. FST x ≠ FST y) t) (x::t))
    (λOVERRIDE a.
         case a of
           [] => I []
         | x::t => I (x::OVERRIDE (FILTER (λy. FST x ≠ FST y) t)))

LIST_UPDATE_def

⊢ LIST_UPDATE [] = I ∧
  ∀h t. LIST_UPDATE (h::t) = (FST h =+ SND h) ∘ LIST_UPDATE t

Theorems

OVERRIDE_ind

⊢ ∀P. P [] ∧ (∀x t. P (FILTER (λy. FST x ≠ FST y) t) ⇒ P (x::t)) ⇒ ∀v. P v

OVERRIDE_def

⊢ OVERRIDE [] = [] ∧
  ∀x t. OVERRIDE (x::t) = x::OVERRIDE (FILTER (λy. FST x ≠ FST y) t)

LIST_UPDATE_LOOKUP

⊢ ∀l f i.
      LIST_UPDATE l f i =
      case FIND (λx. FST x = i) l of NONE => f i | SOME (v1,e) => e

LIST_UPDATE_OVERRIDE

⊢ ∀l. LIST_UPDATE l = LIST_UPDATE (OVERRIDE l)

LIST_UPDATE_ALL_DISTINCT

⊢ ∀l1 l2.
      ALL_DISTINCT (MAP FST l2) ∧ PERM l1 l2 ⇒ LIST_UPDATE l1 = LIST_UPDATE l2

LIST_UPDATE_SORT_OVERRIDE

⊢ ∀R l. LIST_UPDATE l = LIST_UPDATE (QSORT R (OVERRIDE l))

LIST_UPDATE_THMS

⊢ ((∀l1 l2 r1 r2. (l1 =+ r1) ∘ (l2 =+ r2) = LIST_UPDATE [(l1,r1); (l2,r2)]) ∧
   (∀l r t. (l =+ r) ∘ LIST_UPDATE t = LIST_UPDATE ((l,r)::t)) ∧
   (∀l1 l2 r1 r2 f.
        (l1 =+ r1) ((l2 =+ r2) f) = LIST_UPDATE [(l1,r1); (l2,r2)] f) ∧
   ∀l r t f. (l =+ r) (LIST_UPDATE t f) = LIST_UPDATE ((l,r)::t) f) ∧
  (∀l1 l2. LIST_UPDATE l1 ∘ LIST_UPDATE l2 = LIST_UPDATE (l1 ++ l2)) ∧
  (∀l1 l2 r. LIST_UPDATE l1 ∘ (l2 =+ r) = LIST_UPDATE (SNOC (l2,r) l1)) ∧
  (∀l1 l2 f. LIST_UPDATE l1 (LIST_UPDATE l2 f) = LIST_UPDATE (l1 ++ l2) f) ∧
  ∀l1 l2 r f. LIST_UPDATE l1 ((l2 =+ r) f) = LIST_UPDATE (SNOC (l2,r) l1) f

APPLY_UPDATE_ID

⊢ ∀f a. (a =+ f a) f = f

APPLY_UPDATE_THM

⊢ ∀f a b c. (a =+ b) f c = if a = c then b else f c

SAME_KEY_UPDATE_DIFFER

⊢ ∀f1 f2 a b c. b ≠ c ⇒ (a =+ b) f ≠ (a =+ c) f

UPDATE_APPLY_ID

⊢ ∀f a b. f a = b ⇔ (a =+ b) f = f

UPDATE_APPLY_IMP_ID

⊢ ∀f b a. f a = b ⇒ (a =+ b) f = f

UPDATE_COMMUTES

⊢ ∀f a b c d. a ≠ b ⇒ (a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f)

UPDATE_EQ

⊢ ∀f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f

UPDATE_def

⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)