Structure fmspTheory

signature fmspTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FMSP_def : thm
  
  (*  Theorems  *)
    val FMSP_FDOM : thm
    val FMSP_FDOMSUB : thm
    val FMSP_FEMPTY : thm
    val FMSP_FUNION : thm
    val FMSP_FUPDATE : thm
    val FMSP_bitotal : thm
    val FMSP_surj : thm
  
  val fmsp_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [sptree] Parent theory of "fmsp"
   
   [transfer] Parent theory of "fmsp"
   
   [FMSP_def]  Definition
      
      ⊢ ∀AN BC fm sp.
          FMSP AN BC fm sp ⇔
          ∀a n. AN a n ⇒ OPTREL BC (FLOOKUP fm a) (lookup n sp)
   
   [FMSP_FDOM]  Theorem
      
      ⊢ (FMSP AN BC |==> AN |==> $<=>) FDOM domain
   
   [FMSP_FDOMSUB]  Theorem
      
      ⊢ bi_unique AN ⇒
        (FMSP AN BC |==> AN |==> FMSP AN BC) $\\ (flip delete)
   
   [FMSP_FEMPTY]  Theorem
      
      ⊢ FMSP AN BC FEMPTY LN
   
   [FMSP_FUNION]  Theorem
      
      ⊢ (FMSP AN BC |==> FMSP AN BC |==> FMSP AN BC) FUNION union
   
   [FMSP_FUPDATE]  Theorem
      
      ⊢ bi_unique AN ⇒
        (FMSP AN BC |==> AN ### BC |==> FMSP AN BC) $|+
          (λsp (n,v). insert n v sp)
   
   [FMSP_bitotal]  Theorem
      
      ⊢ bitotal BC ∧ bi_unique AN ⇒ bitotal (FMSP AN BC)
   
   [FMSP_surj]  Theorem
      
      ⊢ bi_unique AN ∧ surj BC ⇒ surj (FMSP AN BC)
   
   
*)
end

HOL 4, Kananaskis-14