Structure patricia_castsTheory

signature patricia_castsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ADD_LISTs_def : thm
    val ADD_LISTw_def : thm
    val ADDs_def : thm
    val ADDw_def : thm
    val DEPTHw_def : thm
    val EVERY_LEAFw_def : thm
    val EXISTS_LEAFw_def : thm
    val FINDs_def : thm
    val FINDw_def : thm
    val INSERT_PTREEs_def : thm
    val INSERT_PTREEw_def : thm
    val IN_PTREEs_def : thm
    val IN_PTREEw_def : thm
    val KEYSs_def : thm
    val KEYSw_def : thm
    val PEEKs_def : thm
    val PEEKw_def : thm
    val PTREE_OF_STRINGSET_def : thm
    val PTREE_OF_WORDSET_def : thm
    val REMOVEs_def : thm
    val REMOVEw_def : thm
    val SIZEw_def : thm
    val SKIP1_def : thm
    val SOME_PTREE_def : thm
    val STRINGSET_OF_PTREE_def : thm
    val THE_PTREE_def : thm
    val TRANSFORMw_def : thm
    val TRAVERSEs_def : thm
    val TRAVERSEw_def : thm
    val UNION_PTREEw_def : thm
    val WORDSET_OF_PTREE_def : thm
    val WordEmpty_def : thm
    val num_to_string_def : thm
    val string_to_num_def : thm
    val word_ptree_TY_DEF : thm
    val word_ptree_case_def : thm
    val word_ptree_size_def : thm
  
  (*  Theorems  *)
    val ADD_INSERT_STRING : thm
    val ADD_INSERT_WORD : thm
    val EVERY_MAP_ORD : thm
    val IMAGE_string_to_num : thm
    val MAP_11 : thm
    val REVERSE_11 : thm
    val THE_PTREE_SOME_PTREE : thm
    val datatype_word_ptree : thm
    val l2n_11 : thm
    val l2n_APPEND : thm
    val l2n_LENGTH : thm
    val num_to_string_string_to_num : thm
    val string_to_num_11 : thm
    val string_to_num_num_to_string : thm
    val word_ptree_11 : thm
    val word_ptree_Axiom : thm
    val word_ptree_case_cong : thm
    val word_ptree_case_eq : thm
    val word_ptree_induction : thm
    val word_ptree_nchotomy : thm
  
  val patricia_casts_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [patricia] Parent theory of "patricia_casts"
   
   [ADD_LISTs_def]  Definition
      
      ⊢ $|++ = FOLDL $|+
   
   [ADD_LISTw_def]  Definition
      
      ⊢ $|++ = FOLDL $|+
   
   [ADDs_def]  Definition
      
      ⊢ ∀t w d. t |+ (w,d) = t |+ (string_to_num w,d)
   
   [ADDw_def]  Definition
      
      ⊢ ∀t w d. t |+ (w,d) = SOME_PTREE (THE_PTREE t |+ (w2n w,d))
   
   [DEPTHw_def]  Definition
      
      ⊢ ∀t. DEPTHw t = DEPTH (THE_PTREE t)
   
   [EVERY_LEAFw_def]  Definition
      
      ⊢ ∀P t.
            EVERY_LEAFw P t ⇔ EVERY_LEAF (λk d. P (n2w k) d) (THE_PTREE t)
   
   [EXISTS_LEAFw_def]  Definition
      
      ⊢ ∀P t.
            EXISTS_LEAFw P t ⇔
            EXISTS_LEAF (λk d. P (n2w k) d) (THE_PTREE t)
   
   [FINDs_def]  Definition
      
      ⊢ ∀t w. FINDs t w = THE (t ' w)
   
   [FINDw_def]  Definition
      
      ⊢ ∀t w. FINDw t w = THE (t ' w)
   
   [INSERT_PTREEs_def]  Definition
      
      ⊢ ∀w t. w INSERT_PTREEs t = string_to_num w INSERT_PTREE t
   
   [INSERT_PTREEw_def]  Definition
      
      ⊢ ∀w t.
            w INSERT_PTREEw t = SOME_PTREE (w2n w INSERT_PTREE THE_PTREE t)
   
   [IN_PTREEs_def]  Definition
      
      ⊢ ∀w t. w IN_PTREEs t ⇔ string_to_num w IN_PTREE t
   
   [IN_PTREEw_def]  Definition
      
      ⊢ ∀w t. w IN_PTREEw t ⇔ w2n w IN_PTREE THE_PTREE t
   
   [KEYSs_def]  Definition
      
      ⊢ ∀t. KEYSs t = QSORT $< (TRAVERSEs t)
   
   [KEYSw_def]  Definition
      
      ⊢ ∀t. KEYSw t = QSORT $<+ (TRAVERSEw t)
   
   [PEEKs_def]  Definition
      
      ⊢ ∀t w. t ' w = t ' (string_to_num w)
   
   [PEEKw_def]  Definition
      
      ⊢ ∀t w. t ' w = THE_PTREE t ' (w2n w)
   
   [PTREE_OF_STRINGSET_def]  Definition
      
      ⊢ ∀t s. t |++ s = t |++ IMAGE string_to_num s
   
   [PTREE_OF_WORDSET_def]  Definition
      
      ⊢ ∀t s. t |++ s = SOME_PTREE (THE_PTREE t |++ IMAGE w2n s)
   
   [REMOVEs_def]  Definition
      
      ⊢ ∀t w. t \\ w = t \\ string_to_num w
   
   [REMOVEw_def]  Definition
      
      ⊢ ∀t w. t \\ w = SOME_PTREE (THE_PTREE t \\ w2n w)
   
   [SIZEw_def]  Definition
      
      ⊢ ∀t. SIZEw t = SIZE (THE_PTREE t)
   
   [SKIP1_def]  Definition
      
      ⊢ ∀c s. SKIP1 (STRING c s) = s
   
   [SOME_PTREE_def]  Definition
      
      ⊢ ∀t. SOME_PTREE t = Word_ptree (K ()) t
   
   [STRINGSET_OF_PTREE_def]  Definition
      
      ⊢ ∀t. STRINGSET_OF_PTREE t = LIST_TO_SET (TRAVERSEs t)
   
   [THE_PTREE_def]  Definition
      
      ⊢ ∀a t. THE_PTREE (Word_ptree a t) = t
   
   [TRANSFORMw_def]  Definition
      
      ⊢ ∀f t. TRANSFORMw f t = SOME_PTREE (TRANSFORM f (THE_PTREE t))
   
   [TRAVERSEs_def]  Definition
      
      ⊢ ∀t. TRAVERSEs t = MAP num_to_string (TRAVERSE t)
   
   [TRAVERSEw_def]  Definition
      
      ⊢ ∀t. TRAVERSEw t = MAP n2w (TRAVERSE (THE_PTREE t))
   
   [UNION_PTREEw_def]  Definition
      
      ⊢ ∀t1 t2.
            t1 UNION_PTREEw t2 =
            SOME_PTREE (THE_PTREE t1 UNION_PTREE THE_PTREE t2)
   
   [WORDSET_OF_PTREE_def]  Definition
      
      ⊢ ∀t. WORDSET_OF_PTREE t = LIST_TO_SET (TRAVERSEw t)
   
   [WordEmpty_def]  Definition
      
      ⊢ +{}+ = SOME_PTREE -{}-
   
   [num_to_string_def]  Definition
      
      ⊢ ∀n. num_to_string n = SKIP1 (n2s 256 CHR n)
   
   [string_to_num_def]  Definition
      
      ⊢ ∀s. string_to_num s = s2n 256 ORD (STRING #"\^A" s)
   
   [word_ptree_TY_DEF]  Definition
      
      ⊢ ∃rep.
            TYPE_DEFINITION
              (λa0'.
                   ∀ $var$('word_ptree').
                       (∀a0'.
                            (∃a0 a1.
                                 a0' =
                                 (λa0 a1.
                                      ind_type$CONSTR 0 (a0,a1)
                                        (λn. ind_type$BOTTOM)) a0 a1) ⇒
                            $var$('word_ptree') a0') ⇒
                       $var$('word_ptree') a0') rep
   
   [word_ptree_case_def]  Definition
      
      ⊢ ∀a0 a1 f. word_ptree_CASE (Word_ptree a0 a1) f = f a0 a1
   
   [word_ptree_size_def]  Definition
      
      ⊢ ∀f f1 a0 a1.
            word_ptree_size f f1 (Word_ptree a0 a1) = 1 + ptree_size f1 a1
   
   [ADD_INSERT_STRING]  Theorem
      
      ⊢ ∀w v t. t |+ (w,v) = t |+ (w,())
   
   [ADD_INSERT_WORD]  Theorem
      
      ⊢ ∀w v t. t |+ (w,v) = t |+ (w,())
   
   [EVERY_MAP_ORD]  Theorem
      
      ⊢ ∀l. EVERY ($> 256) (MAP ORD l)
   
   [IMAGE_string_to_num]  Theorem
      
      ⊢ ∀n.
            (n = 1) ∨ 256 ≤ n ∧ (n DIV 256 ** LOG 256 n = 1) ⇔
            n ∈ IMAGE string_to_num 𝕌(:string)
   
   [MAP_11]  Theorem
      
      ⊢ ∀f l1 l2.
            (∀x y. (f x = f y) ⇔ (x = y)) ⇒
            ((MAP f l1 = MAP f l2) ⇔ (l1 = l2))
   
   [REVERSE_11]  Theorem
      
      ⊢ ∀l1 l2. (REVERSE l1 = REVERSE l2) ⇔ (l1 = l2)
   
   [THE_PTREE_SOME_PTREE]  Theorem
      
      ⊢ ∀t. THE_PTREE (SOME_PTREE t) = t
   
   [datatype_word_ptree]  Theorem
      
      ⊢ DATATYPE (word_ptree Word_ptree)
   
   [l2n_11]  Theorem
      
      ⊢ ∀b l1 l2.
            1 < b ∧ EVERY ($> b) l1 ∧ EVERY ($> b) l2 ⇒
            ((l2n b (l1 ⧺ [1]) = l2n b (l2 ⧺ [1])) ⇔ (l1 = l2))
   
   [l2n_APPEND]  Theorem
      
      ⊢ ∀b l1 l2. l2n b (l1 ⧺ l2) = l2n b l1 + b ** LENGTH l1 * l2n b l2
   
   [l2n_LENGTH]  Theorem
      
      ⊢ ∀b l. 1 < b ⇒ l2n b l < b ** LENGTH l
   
   [num_to_string_string_to_num]  Theorem
      
      ⊢ ∀s. num_to_string (string_to_num s) = s
   
   [string_to_num_11]  Theorem
      
      ⊢ ∀s t. (string_to_num s = string_to_num t) ⇔ (s = t)
   
   [string_to_num_num_to_string]  Theorem
      
      ⊢ ∀n.
            n ∈ IMAGE string_to_num 𝕌(:string) ⇒
            (string_to_num (num_to_string n) = n)
   
   [word_ptree_11]  Theorem
      
      ⊢ ∀a0 a1 a0' a1'.
            (Word_ptree a0 a1 = Word_ptree a0' a1') ⇔
            (a0 = a0') ∧ (a1 = a1')
   
   [word_ptree_Axiom]  Theorem
      
      ⊢ ∀f. ∃fn. ∀a0 a1. fn (Word_ptree a0 a1) = f a0 a1
   
   [word_ptree_case_cong]  Theorem
      
      ⊢ ∀M M' f.
            (M = M') ∧
            (∀a0 a1. (M' = Word_ptree a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ⇒
            (word_ptree_CASE M f = word_ptree_CASE M' f')
   
   [word_ptree_case_eq]  Theorem
      
      ⊢ (word_ptree_CASE x f = v) ⇔
        ∃f' p. (x = Word_ptree f' p) ∧ (f f' p = v)
   
   [word_ptree_induction]  Theorem
      
      ⊢ ∀P. (∀f p. P (Word_ptree f p)) ⇒ ∀w. P w
   
   [word_ptree_nchotomy]  Theorem
      
      ⊢ ∀ww. ∃f p. ww = Word_ptree f p
   
   
*)
end

HOL 4, Kananaskis-13