Theory "patricia_casts"

Parents     patricia

Signature

Type Arity
word_ptree 2
Constant Type
ADD_LISTs :α ptree -> (string, α) alist -> α ptree
ADD_LISTw :(α, β) word_ptree -> (α word, β) alist -> (α, β) word_ptree
ADDs :α ptree -> string # α -> α ptree
ADDw :(α, β) word_ptree -> α word # β -> (α, β) word_ptree
DEPTHw :(α, β) word_ptree -> num
EVERY_LEAFw :(α word -> β -> bool) -> (α, β) word_ptree -> bool
EXISTS_LEAFw :(α word -> β -> bool) -> (α, β) word_ptree -> bool
FINDs :α ptree -> string -> α
FINDw :(β, α) word_ptree -> β word -> α
INSERT_PTREEs :string -> ptreeset -> ptreeset
INSERT_PTREEw :α word -> α word_ptreeset -> α word_ptreeset
IN_PTREEs :string -> ptreeset -> bool
IN_PTREEw :α word -> α word_ptreeset -> bool
KEYSs :α ptree -> string list
KEYSw :(α, β) word_ptree -> α word list
PEEKs :α ptree -> string -> α option
PEEKw :(α, β) word_ptree -> α word -> β option
PTREE_OF_STRINGSET :ptreeset -> (string -> bool) -> ptreeset
PTREE_OF_WORDSET :α word_ptreeset -> (α word -> bool) -> α word_ptreeset
REMOVEs :α ptree -> string -> α ptree
REMOVEw :(α, β) word_ptree -> α word -> (α, β) word_ptree
SIZEw :(α, β) word_ptree -> num
SKIP1 :string -> string
SOME_PTREE :β ptree -> (α, β) word_ptree
STRINGSET_OF_PTREE :ptreeset -> string -> bool
THE_PTREE :(β, α) word_ptree -> α ptree
TRANSFORMw :(α -> β) -> (γ, α) word_ptree -> (γ, β) word_ptree
TRAVERSEs :α ptree -> string list
TRAVERSEw :(α, β) word_ptree -> α word list
UNION_PTREEw :β word_ptreeset -> γ word_ptreeset -> α word_ptreeset
WORDSET_OF_PTREE :α word_ptreeset -> α word -> bool
WordEmpty :(α, β) word_ptree
Word_ptree :(α -> unit) -> β ptree -> (α, β) word_ptree
num_to_string :num -> string
string_to_num :string -> num
word_ptree_CASE :(α, β) word_ptree -> ((α -> unit) -> β ptree -> γ) -> γ
word_ptree_size :(α -> num) -> (β -> num) -> (α, β) word_ptree -> num

Definitions

SKIP1_def 
⊢ ∀c s. SKIP1 (STRING c s) = s
string_to_num_def 
⊢ ∀s. string_to_num s = s2n 256 ORD (STRING #"\^A" s)
num_to_string_def 
⊢ ∀n. num_to_string n = SKIP1 (n2s 256 CHR n)
PEEKs_def 
⊢ ∀t w. t ' w = t ' (string_to_num w)
FINDs_def 
⊢ ∀t w. FINDs t w = THE (t ' w)
ADDs_def 
⊢ ∀t w d. t |+ (w,d) = t |+ (string_to_num w,d)
ADD_LISTs_def 
⊢ $|++ = FOLDL $|+
REMOVEs_def 
⊢ ∀t w. t \\ w = t \\ string_to_num w
TRAVERSEs_def 
⊢ ∀t. TRAVERSEs t = MAP num_to_string (TRAVERSE t)
KEYSs_def 
⊢ ∀t. KEYSs t = QSORT $< (TRAVERSEs t)
IN_PTREEs_def 
⊢ ∀w t. w IN_PTREEs t ⇔ string_to_num w IN_PTREE t
INSERT_PTREEs_def 
⊢ ∀w t. w INSERT_PTREEs t = string_to_num w INSERT_PTREE t
STRINGSET_OF_PTREE_def 
⊢ ∀t. STRINGSET_OF_PTREE t = LIST_TO_SET (TRAVERSEs t)
PTREE_OF_STRINGSET_def 
⊢ ∀t s. t |++ s = t |++ IMAGE string_to_num s
word_ptree_TY_DEF 
⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'word_ptree' .
                 (∀a0'.
                      (∃a0 a1.
                           a0' =
                           (λa0 a1.
                                ind_type$CONSTR 0 (a0,a1)
                                  (λn. ind_type$BOTTOM)) a0 a1) ⇒
                      'word_ptree' a0') ⇒
                 'word_ptree' a0') rep
word_ptree_case_def 
⊢ ∀a0 a1 f. word_ptree_CASE (Word_ptree a0 a1) f = f a0 a1
word_ptree_size_def 
⊢ ∀f f1 a0 a1. word_ptree_size f f1 (Word_ptree a0 a1) = 1 + ptree_size f1 a1
THE_PTREE_def 
⊢ ∀a t. THE_PTREE (Word_ptree a t) = t
SOME_PTREE_def 
⊢ ∀t. SOME_PTREE t = Word_ptree (K ()) t
WordEmpty_def 
⊢ +{}+ = SOME_PTREE -{}-
PEEKw_def 
⊢ ∀t w. t ' w = THE_PTREE t ' (w2n w)
FINDw_def 
⊢ ∀t w. FINDw t w = THE (t ' w)
ADDw_def 
⊢ ∀t w d. t |+ (w,d) = SOME_PTREE (THE_PTREE t |+ (w2n w,d))
ADD_LISTw_def 
⊢ $|++ = FOLDL $|+
REMOVEw_def 
⊢ ∀t w. t \\ w = SOME_PTREE (THE_PTREE t \\ w2n w)
TRAVERSEw_def 
⊢ ∀t. TRAVERSEw t = MAP n2w (TRAVERSE (THE_PTREE t))
KEYSw_def 
⊢ ∀t. KEYSw t = QSORT $<+ (TRAVERSEw t)
TRANSFORMw_def 
⊢ ∀f t. TRANSFORMw f t = SOME_PTREE (TRANSFORM f (THE_PTREE t))
EVERY_LEAFw_def 
⊢ ∀P t. EVERY_LEAFw P t ⇔ EVERY_LEAF (λk d. P (n2w k) d) (THE_PTREE t)
EXISTS_LEAFw_def 
⊢ ∀P t. EXISTS_LEAFw P t ⇔ EXISTS_LEAF (λk d. P (n2w k) d) (THE_PTREE t)
SIZEw_def 
⊢ ∀t. SIZEw t = SIZE (THE_PTREE t)
DEPTHw_def 
⊢ ∀t. DEPTHw t = DEPTH (THE_PTREE t)
IN_PTREEw_def 
⊢ ∀w t. w IN_PTREEw t ⇔ w2n w IN_PTREE THE_PTREE t
INSERT_PTREEw_def 
⊢ ∀w t. w INSERT_PTREEw t = SOME_PTREE (w2n w INSERT_PTREE THE_PTREE t)
WORDSET_OF_PTREE_def 
⊢ ∀t. WORDSET_OF_PTREE t = LIST_TO_SET (TRAVERSEw t)
UNION_PTREEw_def 
⊢ ∀t1 t2.
      t1 UNION_PTREEw t2 = SOME_PTREE (THE_PTREE t1 UNION_PTREE THE_PTREE t2)
PTREE_OF_WORDSET_def 
⊢ ∀t s. t |++ s = SOME_PTREE (THE_PTREE t |++ IMAGE w2n s)

Theorems

datatype_word_ptree 
⊢ DATATYPE (word_ptree Word_ptree)
word_ptree_11 
⊢ ∀a0 a1 a0' a1'. Word_ptree a0 a1 = Word_ptree a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
word_ptree_nchotomy 
⊢ ∀ww. ∃f p. ww = Word_ptree f p
word_ptree_Axiom 
⊢ ∀f. ∃fn. ∀a0 a1. fn (Word_ptree a0 a1) = f a0 a1
word_ptree_induction 
⊢ ∀P. (∀f p. P (Word_ptree f p)) ⇒ ∀w. P w
word_ptree_case_cong 
⊢ ∀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 
⊢ word_ptree_CASE x f = v ⇔ ∃f' p. x = Word_ptree f' p ∧ f f' p = v
ADD_INSERT_STRING 
⊢ ∀w v t. t |+ (w,v) = t |+ (w,())
l2n_APPEND 
⊢ ∀b l1 l2. l2n b (l1 ++ l2) = l2n b l1 + b ** LENGTH l1 * l2n b l2
l2n_LENGTH 
⊢ ∀b l. 1 < b ⇒ l2n b l < b ** LENGTH l
l2n_11 
⊢ ∀b l1 l2.
      1 < b ∧ EVERY ($> b) l1 ∧ EVERY ($> b) l2 ⇒
      (l2n b (l1 ++ [1]) = l2n b (l2 ++ [1]) ⇔ l1 = l2)
EVERY_MAP_ORD 
⊢ ∀l. EVERY ($> 256) (MAP ORD l)
MAP_11 
⊢ ∀f l1 l2. (∀x y. f x = f y ⇔ x = y) ⇒ (MAP f l1 = MAP f l2 ⇔ l1 = l2)
REVERSE_11 
⊢ ∀l1 l2. REVERSE l1 = REVERSE l2 ⇔ l1 = l2
string_to_num_11 
⊢ ∀s t. string_to_num s = string_to_num t ⇔ s = t
IMAGE_string_to_num 
⊢ ∀n.
      n = 1 ∨ 256 ≤ n ∧ n DIV 256 ** LOG 256 n = 1 ⇔
      n ∈ IMAGE string_to_num 𝕌(:string)
string_to_num_num_to_string 
⊢ ∀n. n ∈ IMAGE string_to_num 𝕌(:string) ⇒ string_to_num (num_to_string n) = n
num_to_string_string_to_num 
⊢ ∀s. num_to_string (string_to_num s) = s
ADD_INSERT_WORD 
⊢ ∀w v t. t |+ (w,v) = t |+ (w,())
THE_PTREE_SOME_PTREE 
⊢ ∀t. THE_PTREE (SOME_PTREE t) = t