Theory "patricia_casts"

Parents patricia

Signature

Type	Arity
word_ptree	2
Constant	Type
ADD_LISTs	:α ptree -> (string # α) list -> α ptree
ADD_LISTw	:(α, β) word_ptree -> (α word # β) list -> (α, β) 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 -> unit ptree -> unit ptree
INSERT_PTREEw	:α word -> (α, unit) word_ptree -> (α, unit) word_ptree
IN_PTREEs	:string -> unit ptree -> bool
IN_PTREEw	:α word -> (α, unit) word_ptree -> bool
KEYSs	:α ptree -> string list
KEYSw	:(α, β) word_ptree -> α word list
PEEKs	:α ptree -> string -> α option
PEEKw	:(α, β) word_ptree -> α word -> β option
PTREE_OF_STRINGSET	:unit ptree -> (string -> bool) -> unit ptree
PTREE_OF_WORDSET	:(α, unit) word_ptree -> (α word -> bool) -> (α, unit) word_ptree
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	:unit ptree -> string -> bool
THE_PTREE	:(β, α) word_ptree -> α ptree
TRANSFORMw	:(α -> β) -> (γ, α) word_ptree -> (γ, β) word_ptree
TRAVERSEs	:α ptree -> string list
TRAVERSEw	:(α, β) word_ptree -> α word list
UNION_PTREEw	:(β, unit) word_ptree -> (γ, unit) word_ptree -> (α, unit) word_ptree
WORDSET_OF_PTREE	:(α, unit) word_ptree -> α 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

WORDSET_OF_PTREE_def

⊢ ∀t. WORDSET_OF_PTREE t = LIST_TO_SET (TRAVERSEw t)

WordEmpty_def

⊢ +{}+ = SOME_PTREE -{}-

word_ptree_TY_DEF

⊢ ∃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_size_def

⊢ ∀f f1 a0 a1. word_ptree_size f f1 (Word_ptree a0 a1) = 1 + ptree_size f1 a1

word_ptree_case_def

⊢ ∀a0 a1 f. word_ptree_CASE (Word_ptree a0 a1) f = f a0 a1

UNION_PTREEw_def

⊢ ∀t1 t2.
      t1 UNION_PTREEw t2 = SOME_PTREE (THE_PTREE t1 UNION_PTREE THE_PTREE t2)

TRAVERSEw_def

⊢ ∀t. TRAVERSEw t = MAP n2w (TRAVERSE (THE_PTREE t))

TRAVERSEs_def

⊢ ∀t. TRAVERSEs t = MAP num_to_string (TRAVERSE t)

TRANSFORMw_def

⊢ ∀f t. TRANSFORMw f t = SOME_PTREE (TRANSFORM f (THE_PTREE t))

THE_PTREE_def

⊢ ∀a t. THE_PTREE (Word_ptree a t) = t

STRINGSET_OF_PTREE_def

⊢ ∀t. STRINGSET_OF_PTREE t = LIST_TO_SET (TRAVERSEs t)

string_to_num_def

⊢ ∀s. string_to_num s = s2n 256 ORD (STRING #"\^A" s)

SOME_PTREE_def

⊢ ∀t. SOME_PTREE t = Word_ptree (K ()) t

SKIP1_def

⊢ ∀c s. SKIP1 (STRING c s) = s

SIZEw_def

⊢ ∀t. SIZEw t = SIZE (THE_PTREE t)

REMOVEw_def

⊢ ∀t w. t \\ w = SOME_PTREE (THE_PTREE t \\ w2n w)

REMOVEs_def

⊢ ∀t w. t \\ w = t \\ string_to_num w

PTREE_OF_WORDSET_def

⊢ ∀t s. t |++ s = SOME_PTREE (THE_PTREE t |++ IMAGE w2n s)

PTREE_OF_STRINGSET_def

⊢ ∀t s. t |++ s = t |++ IMAGE string_to_num s

PEEKw_def

⊢ ∀t w. t ' w = THE_PTREE t ' (w2n w)

PEEKs_def

⊢ ∀t w. t ' w = t ' (string_to_num w)

num_to_string_def

⊢ ∀n. num_to_string n = SKIP1 (n2s 256 CHR n)

KEYSw_def

⊢ ∀t. KEYSw t = QSORT $<+ (TRAVERSEw t)

KEYSs_def

⊢ ∀t. KEYSs t = QSORT $< (TRAVERSEs t)

INSERT_PTREEw_def

⊢ ∀w t. w INSERT_PTREEw t = SOME_PTREE (w2n w INSERT_PTREE THE_PTREE t)

INSERT_PTREEs_def

⊢ ∀w t. w INSERT_PTREEs t = string_to_num w INSERT_PTREE t

IN_PTREEw_def

⊢ ∀w t. w IN_PTREEw t ⇔ w2n w IN_PTREE THE_PTREE t

IN_PTREEs_def

⊢ ∀w t. w IN_PTREEs t ⇔ string_to_num w IN_PTREE t

FINDw_def

⊢ ∀t w. FINDw t w = THE (t ' w)

FINDs_def

⊢ ∀t w. FINDs t w = THE (t ' w)

EXISTS_LEAFw_def

⊢ ∀P t. EXISTS_LEAFw P t ⇔ EXISTS_LEAF (λk d. P (n2w k) d) (THE_PTREE t)

EVERY_LEAFw_def

⊢ ∀P t. EVERY_LEAFw P t ⇔ EVERY_LEAF (λk d. P (n2w k) d) (THE_PTREE t)

DEPTHw_def

⊢ ∀t. DEPTHw t = DEPTH (THE_PTREE t)

ADDw_def

⊢ ∀t w d. t |+ (w,d) = SOME_PTREE (THE_PTREE t |+ (w2n w,d))

ADDs_def

⊢ ∀t w d. t |+ (w,d) = t |+ (string_to_num w,d)

ADD_LISTw_def

⊢ $|++ = FOLDL $|+

ADD_LISTs_def

⊢ $|++ = FOLDL $|+

Theorems

word_ptree_nchotomy

⊢ ∀ww. ∃f p. ww = Word_ptree f p

word_ptree_induction

⊢ ∀P. (∀f p. P (Word_ptree f p)) ⇒ ∀w. P w

word_ptree_case_eq

⊢ (word_ptree_CASE x f = v) ⇔ ∃f' p. (x = Word_ptree f' p) ∧ (f f' p = v)

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_Axiom

⊢ ∀f. ∃fn. ∀a0 a1. fn (Word_ptree a0 a1) = f a0 a1

word_ptree_11

⊢ ∀a0 a1 a0' a1'.
      (Word_ptree a0 a1 = Word_ptree a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')

THE_PTREE_SOME_PTREE

⊢ ∀t. THE_PTREE (SOME_PTREE t) = t

string_to_num_num_to_string

⊢ ∀n.
      n ∈ IMAGE string_to_num 𝕌(:string) ⇒
      (string_to_num (num_to_string n) = n)

string_to_num_11

⊢ ∀s t. (string_to_num s = string_to_num t) ⇔ (s = t)

REVERSE_11

⊢ ∀l1 l2. (REVERSE l1 = REVERSE l2) ⇔ (l1 = l2)

num_to_string_string_to_num

⊢ ∀s. num_to_string (string_to_num s) = s

MAP_11

⊢ ∀f l1 l2.
      (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ((MAP f l1 = MAP f l2) ⇔ (l1 = l2))

l2n_LENGTH

⊢ ∀b l. 1 < b ⇒ l2n b l < b ** LENGTH l

l2n_APPEND

⊢ ∀b l1 l2. l2n b (l1 ++ l2) = l2n b l1 + b ** LENGTH l1 * l2n b l2

l2n_11

⊢ ∀b l1 l2.
      1 < b ∧ EVERY ($> b) l1 ∧ EVERY ($> b) l2 ⇒
      ((l2n b (l1 ++ [1]) = l2n b (l2 ++ [1])) ⇔ (l1 = l2))

IMAGE_string_to_num

⊢ ∀n.
      (n = 1) ∨ 256 ≤ n ∧ (n DIV 256 ** LOG 256 n = 1) ⇔
      n ∈ IMAGE string_to_num 𝕌(:string)

EVERY_MAP_ORD

⊢ ∀l. EVERY ($> 256) (MAP ORD l)

datatype_word_ptree

⊢ DATATYPE (word_ptree Word_ptree)

ADD_INSERT_WORD

⊢ ∀w v t. t |+ (w,v) = t |+ (w,())

ADD_INSERT_STRING

⊢ ∀w v t. t |+ (w,v) = t |+ (w,())