Structure containerTheory

signature containerTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BAG_TO_LIST_primitive : thm
    val LIST_TO_BAG : thm
    val SET_TO_LIST_primitive : thm
  
  (*  Theorems  *)
    val BAG_IN_MEM : thm
    val BAG_TO_LIST_CARD : thm
    val BAG_TO_LIST_IND : thm
    val BAG_TO_LIST_INV : thm
    val BAG_TO_LIST_THM : thm
    val FINITE_LIST_TO_SET : 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 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 container_grammars : type_grammar.grammar * term_grammar.grammar
  
  val container_rwts : simpLib.ssfrag
(*
   [bag] Parent theory of "container"
   
   [list] Parent theory of "container"
   
   [BAG_TO_LIST_primitive]  Definition
      
      |- BAG_TO_LIST =
         WFREC
           (@R.
              WF R /\
              !bag. FINITE_BAG bag /\ ~(bag = {| |}) ==> R (BAG_REST bag) bag)
           (\BAG_TO_LIST bag.
              I
                (if FINITE_BAG bag then
                   (if bag = {| |} then
                      []
                    else
                      BAG_CHOICE bag::BAG_TO_LIST (BAG_REST bag))
                 else
                   ARB))
   
   [LIST_TO_BAG]  Definition
      
      |- (LIST_TO_BAG [] = {| |}) /\
         !h t. LIST_TO_BAG (h::t) = BAG_INSERT h (LIST_TO_BAG t)
   
   [SET_TO_LIST_primitive]  Definition
      
      |- SET_TO_LIST =
         WFREC (@R. WF R /\ !s. FINITE s /\ ~(s = {}) ==> R (REST s) s)
           (\SET_TO_LIST s.
              I
                (if FINITE s then
                   (if s = {} then [] else CHOICE s::SET_TO_LIST (REST s))
                 else
                   ARB))
   
   [BAG_IN_MEM]  Theorem
      
      |- !b. FINITE_BAG b ==> !x. BAG_IN x b = MEM x (BAG_TO_LIST b)
   
   [BAG_TO_LIST_CARD]  Theorem
      
      |- !b. FINITE_BAG b ==> (LENGTH (BAG_TO_LIST b) = BAG_CARD 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)))
   
   [FINITE_LIST_TO_SET]  Theorem
      
      |- !l. FINITE (LIST_TO_SET l)
   
   [LIST_TO_SET_APPEND]  Theorem
      
      |- !l1 l2. LIST_TO_SET (l1 ++ l2) = LIST_TO_SET l1 UNION LIST_TO_SET l2
   
   [LIST_TO_SET_THM]  Theorem
      
      |- (LIST_TO_SET [] = {}) /\ (LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)
   
   [MEM_BAG_TO_LIST]  Theorem
      
      |- !b. FINITE_BAG b ==> !x. MEM x (BAG_TO_LIST b) = BAG_IN x b
   
   [MEM_SET_TO_LIST]  Theorem
      
      |- !s. FINITE s ==> !x. MEM x (SET_TO_LIST s) = x IN s
   
   [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 ==> (LIST_TO_SET (SET_TO_LIST s) = s)
   
   [SET_TO_LIST_IN_MEM]  Theorem
      
      |- !s. FINITE s ==> !x. x IN 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. LIST_TO_SET l1 UNION LIST_TO_SET l2 = LIST_TO_SET (l1 ++ l2)
   
   
*)
end