Theory "update"

Signature

Definitions

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

FIND_def

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

Theorems

UPDATE_EQ

⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈

UPDATE_def

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

UPDATE_COMMUTES

⊢ ∀f a b c d. a ≠ b ⇒ (f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈)

UPDATE_APPLY_IMP_ID

⊢ ∀f b a. (f a = b) ⇒ (f⦇a ↦ b⦈ = f)

UPDATE_APPLY_ID

⊢ ∀f a b. (f a = b) ⇔ (f⦇a ↦ b⦈ = f)

SAME_KEY_UPDATE_DIFFER

⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈

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_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. f⦇l1 ↦ r1; l2 ↦ r2⦈ = LIST_UPDATE [(l1,r1); (l2,r2)] f) ∧
   ∀l r t f. (LIST_UPDATE t f)⦇l ↦ r⦈ = 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 f⦇l2 ↦ r⦈ = LIST_UPDATE (SNOC (l2,r) l1) f

LIST_UPDATE_SORT_OVERRIDE

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

LIST_UPDATE_OVERRIDE

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

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_ALL_DISTINCT

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

APPLY_UPDATE_THM

⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c

APPLY_UPDATE_ID

⊢ ∀f a. f⦇a ↦ f a⦈ = f