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_FORALL : thm
    val FMSP_FUNION : thm
    val FMSP_FUPDATE : thm
    val FMSP_bitotal : 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) $\\ (combin$C delete)
   
   [FMSP_FEMPTY]  Theorem
      
      ⊢ FMSP AN BC FEMPTY LN
   
   [FMSP_FORALL]  Theorem
      
      ⊢ bitotal AN ∧ bitotal BC ∧ bi_unique AN ⇒
        ((FMSP AN BC ===> $<=>) ===> $<=>) $! $!
   
   [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 AN ∧ bitotal BC ∧ bi_unique AN ⇒ bitotal (FMSP AN BC)
   
   
*)
end

HOL 4, Kananaskis-13