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_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_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

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