Structure containerTheory

signature containerTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BAG_OF_FMAP_def : thm
    val BAG_TO_LIST_primitive_def : thm
    val LIST_TO_BAG_def : thm
    val mlt_list_def : thm
  
  (*  Theorems  *)
    val BAG_IN_BAG_OF_FMAP : thm
    val BAG_IN_MEM : thm
    val BAG_OF_FMAP_THM : thm
    val BAG_TO_LIST_CARD : thm
    val BAG_TO_LIST_EQ_NIL : thm
    val BAG_TO_LIST_IND : thm
    val BAG_TO_LIST_INV : thm
    val BAG_TO_LIST_THM : thm
    val CARD_LIST_TO_BAG : thm
    val EVERY_LIST_TO_BAG : thm
    val FINITE_BAG_OF_FMAP : thm
    val FINITE_LIST_TO_BAG : thm
    val FINITE_LIST_TO_SET : thm
    val INN_LIST_TO_BAG : thm
    val IN_LIST_TO_BAG : thm
    val LIST_ELEM_COUNT_LIST_TO_BAG : thm
    val LIST_TO_BAG_APPEND : thm
    val LIST_TO_BAG_DISTINCT : thm
    val LIST_TO_BAG_EQ_EMPTY : thm
    val LIST_TO_BAG_FILTER : thm
    val LIST_TO_BAG_MAP : thm
    val LIST_TO_BAG_SUBSET : thm
    val LIST_TO_BAG_SUB_BAG_FLAT_suff : thm
    val LIST_TO_BAG_alt : thm
    val LIST_TO_SET_APPEND : thm
    val LIST_TO_SET_THM : thm
    val MEM_BAG_TO_LIST : thm
    val MEM_SET_TO_LIST : thm
    val PERM_LIST_TO_BAG : thm
    val SET_TO_LIST_CARD : thm
    val SET_TO_LIST_IND : thm
    val SET_TO_LIST_INV : thm
    val SET_TO_LIST_IN_MEM : thm
    val SET_TO_LIST_SING : thm
    val SET_TO_LIST_THM : thm
    val UNION_APPEND : thm
    val WF_mlt_list : thm
  
  val container_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [bag] Parent theory of "container"
   
   [finite_map] Parent theory of "container"
   
   [BAG_OF_FMAP_def]  Definition
      
      ⊢ ∀f b.
          BAG_OF_FMAP f b = (λx. CARD (λk. k ∈ FDOM b ∧ x = f k (b ' k)))
   
   [BAG_TO_LIST_primitive_def]  Definition
      
      ⊢ BAG_TO_LIST =
        WFREC
          (@R. WF R ∧
               ∀bag. FINITE_BAG bag ∧ bag ≠ {||} ⇒ R (BAG_REST bag) bag)
          (λBAG_TO_LIST a.
               I
                 (if FINITE_BAG a then
                    if a = {||} then []
                    else BAG_CHOICE a::BAG_TO_LIST (BAG_REST a)
                  else ARB))
   
   [LIST_TO_BAG_def]  Definition
      
      ⊢ LIST_TO_BAG [] = {||} ∧
        ∀h t. LIST_TO_BAG (h::t) = BAG_INSERT h (LIST_TO_BAG t)
   
   [mlt_list_def]  Definition
      
      ⊢ ∀R. mlt_list R =
            (λl1 l2.
                 ∃h t list.
                   l1 = list ⧺ t ∧ l2 = h::t ∧ ∀e. MEM e list ⇒ R e h)
   
   [BAG_IN_BAG_OF_FMAP]  Theorem
      
      ⊢ ∀x f b. x ⋲ BAG_OF_FMAP f b ⇔ ∃k. k ∈ FDOM b ∧ x = f k (b ' k)
   
   [BAG_IN_MEM]  Theorem
      
      ⊢ ∀b. FINITE_BAG b ⇒ ∀x. x ⋲ b ⇔ MEM x (BAG_TO_LIST b)
   
   [BAG_OF_FMAP_THM]  Theorem
      
      ⊢ (∀f. BAG_OF_FMAP f FEMPTY = {||}) ∧
        ∀f b k v.
          BAG_OF_FMAP f (b |+ (k,v)) =
          BAG_INSERT (f k v) (BAG_OF_FMAP f (b \\ k))
   
   [BAG_TO_LIST_CARD]  Theorem
      
      ⊢ ∀b. FINITE_BAG b ⇒ LENGTH (BAG_TO_LIST b) = BAG_CARD b
   
   [BAG_TO_LIST_EQ_NIL]  Theorem
      
      ⊢ FINITE_BAG b ⇒
        ([] = BAG_TO_LIST b ⇔ b = {||}) ∧ (BAG_TO_LIST b = [] ⇔ b = {||})
   
   [BAG_TO_LIST_IND]  Theorem
      
      ⊢ ∀P. (∀bag. (FINITE_BAG bag ∧ bag ≠ {||} ⇒ P (BAG_REST bag)) ⇒ P bag) ⇒
            ∀v. P v
   
   [BAG_TO_LIST_INV]  Theorem
      
      ⊢ ∀b. FINITE_BAG b ⇒ LIST_TO_BAG (BAG_TO_LIST b) = b
   
   [BAG_TO_LIST_THM]  Theorem
      
      ⊢ FINITE_BAG bag ⇒
        BAG_TO_LIST bag =
        if bag = {||} then []
        else BAG_CHOICE bag::BAG_TO_LIST (BAG_REST bag)
   
   [CARD_LIST_TO_BAG]  Theorem
      
      ⊢ BAG_CARD (LIST_TO_BAG ls) = LENGTH ls
   
   [EVERY_LIST_TO_BAG]  Theorem
      
      ⊢ BAG_EVERY P (LIST_TO_BAG ls) ⇔ EVERY P ls
   
   [FINITE_BAG_OF_FMAP]  Theorem
      
      ⊢ ∀f b. FINITE_BAG (BAG_OF_FMAP f b)
   
   [FINITE_LIST_TO_BAG]  Theorem
      
      ⊢ FINITE_BAG (LIST_TO_BAG ls)
   
   [FINITE_LIST_TO_SET]  Theorem
      
      ⊢ ∀l. FINITE (set l)
   
   [INN_LIST_TO_BAG]  Theorem
      
      ⊢ ∀n h l. BAG_INN h n (LIST_TO_BAG l) ⇔ LENGTH (FILTER ($= h) l) ≥ n
   
   [IN_LIST_TO_BAG]  Theorem
      
      ⊢ ∀h l. h ⋲ LIST_TO_BAG l ⇔ MEM h l
   
   [LIST_ELEM_COUNT_LIST_TO_BAG]  Theorem
      
      ⊢ LIST_ELEM_COUNT e ls = LIST_TO_BAG ls e
   
   [LIST_TO_BAG_APPEND]  Theorem
      
      ⊢ ∀l1 l2. LIST_TO_BAG (l1 ⧺ l2) = LIST_TO_BAG l1 ⊎ LIST_TO_BAG l2
   
   [LIST_TO_BAG_DISTINCT]  Theorem
      
      ⊢ BAG_ALL_DISTINCT (LIST_TO_BAG b) ⇔ ALL_DISTINCT b
   
   [LIST_TO_BAG_EQ_EMPTY]  Theorem
      
      ⊢ ∀l. LIST_TO_BAG l = {||} ⇔ l = []
   
   [LIST_TO_BAG_FILTER]  Theorem
      
      ⊢ LIST_TO_BAG (FILTER f b) = BAG_FILTER f (LIST_TO_BAG b)
   
   [LIST_TO_BAG_MAP]  Theorem
      
      ⊢ LIST_TO_BAG (MAP f b) = BAG_IMAGE f (LIST_TO_BAG b)
   
   [LIST_TO_BAG_SUBSET]  Theorem
      
      ⊢ ∀l1 l2. LIST_TO_BAG l1 ≤ LIST_TO_BAG l2 ⇒ set l1 ⊆ set l2
   
   [LIST_TO_BAG_SUB_BAG_FLAT_suff]  Theorem
      
      ⊢ ∀ls1 ls2.
          LIST_REL (λl1 l2. LIST_TO_BAG l1 ≤ LIST_TO_BAG l2) ls1 ls2 ⇒
          LIST_TO_BAG (FLAT ls1) ≤ LIST_TO_BAG (FLAT ls2)
   
   [LIST_TO_BAG_alt]  Theorem
      
      ⊢ ∀l x. LIST_TO_BAG l x = LENGTH (FILTER ($= x) l)
   
   [LIST_TO_SET_APPEND]  Theorem
      
      ⊢ ∀l1 l2. set (l1 ⧺ l2) = set l1 ∪ set l2
   
   [LIST_TO_SET_THM]  Theorem
      
      ⊢ set [] = ∅ ∧ set (h::t) = h INSERT set t
   
   [MEM_BAG_TO_LIST]  Theorem
      
      ⊢ ∀b. FINITE_BAG b ⇒ ∀x. MEM x (BAG_TO_LIST b) ⇔ x ⋲ b
   
   [MEM_SET_TO_LIST]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. MEM x (SET_TO_LIST s) ⇔ x ∈ s
   
   [PERM_LIST_TO_BAG]  Theorem
      
      ⊢ ∀l1 l2. LIST_TO_BAG l1 = LIST_TO_BAG l2 ⇔ PERM l1 l2
   
   [SET_TO_LIST_CARD]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ LENGTH (SET_TO_LIST s) = CARD s
   
   [SET_TO_LIST_IND]  Theorem
      
      ⊢ ∀P. (∀s. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s)) ⇒ P s) ⇒ ∀v. P v
   
   [SET_TO_LIST_INV]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ set (SET_TO_LIST s) = s
   
   [SET_TO_LIST_IN_MEM]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇔ MEM x (SET_TO_LIST s)
   
   [SET_TO_LIST_SING]  Theorem
      
      ⊢ SET_TO_LIST {x} = [x]
   
   [SET_TO_LIST_THM]  Theorem
      
      ⊢ FINITE s ⇒
        SET_TO_LIST s =
        if s = ∅ then [] else CHOICE s::SET_TO_LIST (REST s)
   
   [UNION_APPEND]  Theorem
      
      ⊢ ∀l1 l2. set l1 ∪ set l2 = set (l1 ⧺ l2)
   
   [WF_mlt_list]  Theorem
      
      ⊢ ∀R. WF R ⇒ WF (mlt_list R)
   
   
*)
end

HOL 4, Kananaskis-14