Structure fsetsTheory

signature fsetsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FSET_def : thm
  
  (*  Theorems  *)
    val KT_FINITE : thm
    val RDOM_FSET_EQ : thm
    val RRANGE_FSET : thm
    val RRANGE_FSET_EQ : thm
    val bi_unique_FSET : thm
    val fDELETE_DELETE : thm
    val fEMPTY_EMPTY : thm
    val fINSERT_INSERT : thm
    val fIN_IN : thm
    val fUNION_UNION : thm
    val fset_ext : thm
    val fupdate_correct : thm
    val left_unique_FSET : thm
    val right_unique_FSET : thm
    val toSet_correct : thm
    val total_FSET : thm
  
  val fsets_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [finite_map] Parent theory of "fsets"
   
   [transfer] Parent theory of "fsets"
   
   [FSET_def]  Definition
      
      ⊢ ∀AB fs s. FSET AB fs s ⇔ ∀a b. AB a b ⇒ (fIN a fs ⇔ b ∈ s)
   
   [KT_FINITE]  Theorem
      
      ⊢ surj AB ∧ right_unique AB ⇒ (FSET AB |==> $<=>) (K T) FINITE
   
   [RDOM_FSET_EQ]  Theorem
      
      ⊢ RDOM (FSET $=) = 𝕌(:α fset)
   
   [RRANGE_FSET]  Theorem
      
      ⊢ RRANGE (FSET AB) =
        {bset |
         FINITE {a | (∃b. AB a b ∧ b ∈ bset)} ∧
         ∀a b b'. b ∈ bset ∧ AB a b ∧ AB a b' ⇒ b' ∈ bset}
   
   [RRANGE_FSET_EQ]  Theorem
      
      ⊢ RRANGE (FSET $=) = FINITE
   
   [bi_unique_FSET]  Theorem
      
      ⊢ bi_unique AB ∧ bitotal AB ⇒ bi_unique (FSET AB)
   
   [fDELETE_DELETE]  Theorem
      
      ⊢ bi_unique AB ⇒ (FSET AB |==> AB |==> FSET AB) fDELETE $DELETE
   
   [fEMPTY_EMPTY]  Theorem
      
      ⊢ FSET AB FEMPTY ∅
   
   [fINSERT_INSERT]  Theorem
      
      ⊢ bi_unique AB ⇒
        (AB |==> FSET AB |==> FSET AB) (λe fs. fINSERT e fs) $INSERT
   
   [fIN_IN]  Theorem
      
      ⊢ (AB |==> FSET AB |==> $<=>) (λe fs. fIN e fs) $IN
   
   [fUNION_UNION]  Theorem
      
      ⊢ (FSET AB |==> FSET AB |==> FSET AB) fUNION $UNION
   
   [fset_ext]  Theorem
      
      ⊢ fm1 = fm2 ⇔ toSet fm1 = toSet fm2
   
   [fupdate_correct]  Theorem
      
      ⊢ bi_unique AB ⇒
        (FSET AB |==> PAIRU AB |==> FSET AB) $|+ (flip $INSERT)
   
   [left_unique_FSET]  Theorem
      
      ⊢ total AB ⇒ left_unique (FSET AB)
   
   [right_unique_FSET]  Theorem
      
      ⊢ surj AB ⇒ right_unique (FSET AB)
   
   [toSet_correct]  Theorem
      
      ⊢ (FSET AB |==> AB |==> $<=>) toSet I
   
   [total_FSET]  Theorem
      
      ⊢ left_unique AB ⇒ total (FSET AB)
   
   
*)
end

HOL 4, Kananaskis-14