Structure updateTheory

signature updateTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val LIST_UPDATE_def : thm
    val OVERRIDE_def_primitive : thm
  
  (*  Theorems  *)
    val APPLY_UPDATE_ID : thm
    val APPLY_UPDATE_THM : thm
    val FIND_def : thm
    val LIST_UPDATE_ALL_DISTINCT : thm
    val LIST_UPDATE_LOOKUP : thm
    val LIST_UPDATE_OVERRIDE : thm
    val LIST_UPDATE_SORT_OVERRIDE : thm
    val LIST_UPDATE_THMS : thm
    val OVERRIDE_def : thm
    val OVERRIDE_ind : thm
    val SAME_KEY_UPDATE_DIFFER : thm
    val UPDATE_APPLY_ID : thm
    val UPDATE_APPLY_IMP_ID : thm
    val UPDATE_COMMUTES : thm
    val UPDATE_EQ : thm
    val UPDATE_def : thm
  
  val update_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [sorting] Parent theory of "update"
   
   [LIST_UPDATE_def]  Definition
      
      ⊢ LIST_UPDATE [] = I ∧
        ∀h t. LIST_UPDATE (h::t) = (FST h =+ SND h) ∘ LIST_UPDATE t
   
   [OVERRIDE_def_primitive]  Definition
      
      ⊢ 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)))
   
   [APPLY_UPDATE_ID]  Theorem
      
      ⊢ ∀f a. f⦇a ↦ f a⦈ = f
   
   [APPLY_UPDATE_THM]  Theorem
      
      ⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c
   
   [FIND_def]  Theorem
      
      ⊢ FIND P [] = NONE ∧ FIND P (h::t) = if P h then SOME h else FIND P t
   
   [LIST_UPDATE_ALL_DISTINCT]  Theorem
      
      ⊢ ∀l1 l2.
          ALL_DISTINCT (MAP FST l2) ∧ PERM l1 l2 ⇒
          LIST_UPDATE l1 = LIST_UPDATE l2
   
   [LIST_UPDATE_LOOKUP]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀l. LIST_UPDATE l = LIST_UPDATE (OVERRIDE l)
   
   [LIST_UPDATE_SORT_OVERRIDE]  Theorem
      
      ⊢ ∀R l. LIST_UPDATE l = LIST_UPDATE (QSORT R (OVERRIDE l))
   
   [LIST_UPDATE_THMS]  Theorem
      
      ⊢ ((∀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
   
   [OVERRIDE_def]  Theorem
      
      ⊢ OVERRIDE [] = [] ∧
        ∀x t. OVERRIDE (x::t) = x::OVERRIDE (FILTER (λy. FST x ≠ FST y) t)
   
   [OVERRIDE_ind]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀x t. P (FILTER (λy. FST x ≠ FST y) t) ⇒ P (x::t)) ⇒
            ∀v. P v
   
   [SAME_KEY_UPDATE_DIFFER]  Theorem
      
      ⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈
   
   [UPDATE_APPLY_ID]  Theorem
      
      ⊢ ∀f a b. f a = b ⇔ f⦇a ↦ b⦈ = f
   
   [UPDATE_APPLY_IMP_ID]  Theorem
      
      ⊢ ∀f b a. f a = b ⇒ f⦇a ↦ b⦈ = f
   
   [UPDATE_COMMUTES]  Theorem
      
      ⊢ ∀f a b c d. a ≠ b ⇒ f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈
   
   [UPDATE_EQ]  Theorem
      
      ⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈
   
   [UPDATE_def]  Theorem
      
      ⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)
   
   
*)
end

HOL 4, Trindemossen-1