Theory "ltree"

Parents llist alist

Signature

Type	Arity
ltree	1
rose_tree	1
Constant	Type
Branch	:α -> α ltree llist -> α ltree
Branch_rep	:α -> (num list -> α # num option) llist -> num list -> α # num option
Rose	:α -> α rose_tree list -> α rose_tree
dest_Branch_rep	:(num list -> α # num option) -> α # (num list -> α # num option) llist
from_rose	:α rose_tree -> α ltree
gen_ltree	:(num list -> α # num option) -> α ltree
ltree_CASE	:β ltree -> (β -> β ltree llist -> α) -> α
ltree_abs	:(num list -> α # num option) -> α ltree
ltree_el	:α ltree -> num list -> (α # num option) option
ltree_finite	:α ltree -> bool
ltree_lookup	:α ltree -> num list -> α ltree option
ltree_map	:(α -> β) -> α ltree -> β ltree
ltree_rel	:(α -> β -> bool) -> α ltree -> β ltree -> bool
ltree_rep	:α ltree -> num list -> α # num option
ltree_rep_ok	:(num list -> α # num option) -> bool
ltree_set	:α ltree -> α -> bool
ltree_unfold	:(β -> α # β llist) -> β -> α ltree
make_ltree_rep	:(num list -> α # num option) -> num list -> α # num option
make_unfold	:(β -> α # β llist) -> β -> num list -> α # num option
path_ok	:num list -> (num list -> α # num option) -> bool
rose_tree1_size	:(α -> num) -> α rose_tree list -> num
rose_tree_CASE	:α rose_tree -> (α -> α rose_tree list -> β) -> β
rose_tree_size	:(α -> num) -> α rose_tree -> num
subtrees	:α ltree -> α ltree -> bool

Definitions

ltree_TY_DEF

⊢ ∃rep. TYPE_DEFINITION ltree_rep_ok rep

ltree_map_def

⊢ ∀f. ltree_map f = ltree_unfold (λt. case t of Branch a ts => (f a,ts))

ltree_rel_def

⊢ ∀R x y.
    ltree_rel R x y ⇔
    ∀path.
      OPTREL (λx y. R (FST x) (FST y) ∧ (SND x = SND y)) (ltree_el x path)
        (ltree_el y path)

ltree_set_def

⊢ ∀t. ltree_set t = {a | ∃ts. Branch a ts ∈ subtrees t}

rose_tree_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('rose_tree') $var$('@temp @ind_typeltree0list').
             (∀a0'.
                (∃a0 a1.
                   (a0' =
                    (λa0 a1.
                         ind_type$CONSTR 0 a0
                           (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0 a1) ∧
                   $var$('@temp @ind_typeltree0list') a1) ⇒
                $var$('rose_tree') a0') ∧
             (∀a1'.
                (a1' = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
                (∃a0 a1.
                   (a1' =
                    (λa0 a1.
                         ind_type$CONSTR (SUC (SUC 0)) ARB
                           (ind_type$FCONS a0
                              (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
                      a1) ∧ $var$('rose_tree') a0 ∧
                   $var$('@temp @ind_typeltree0list') a1) ⇒
                $var$('@temp @ind_typeltree0list') a1') ⇒
             $var$('rose_tree') a0') rep

rose_tree_case_def

⊢ ∀a0 a1 f. rose_tree_CASE (Rose a0 a1) f = f a0 a1

rose_tree_size_def

⊢ (∀f a0 a1. rose_tree_size f (Rose a0 a1) = 1 + (f a0 + rose_tree1_size f a1)) ∧
  (∀f. rose_tree1_size f [] = 0) ∧
  ∀f a0 a1.
    rose_tree1_size f (a0::a1) =
    1 + (rose_tree_size f a0 + rose_tree1_size f a1)

subtrees_def

⊢ ∀t. subtrees t = {u | ∃path. ltree_lookup t path = SOME u}

Theorems

Branch_11

⊢ ∀a1 a2 ts1 ts2. (Branch a1 ts1 = Branch a2 ts2) ⇔ (a1 = a2) ∧ (ts1 = ts2)

datatype_ltree

⊢ DATATYPE (ltree Branch)

datatype_rose_tree

⊢ DATATYPE (rose_tree Rose)

from_rose_def

⊢ ∀ts a.
    from_rose (Rose a ts) = Branch a (fromList (MAP (λa'. from_rose a') ts))

from_rose_ind

⊢ ∀P. (∀a ts. (∀a'. MEM a' ts ⇒ P a') ⇒ P (Rose a ts)) ⇒ ∀v. P v

gen_ltree

⊢ gen_ltree f =
  (let
     (a,len) = f []
   in
     Branch a (LGENLIST (λn. gen_ltree (λpath. f (n::path))) len))

gen_ltree_LNIL

⊢ (gen_ltree f = Branch a [||]) ⇔ (f [] = (a,SOME 0))

ltree_CASE

⊢ ltree_CASE (Branch a ts) f = f a ts

ltree_CASE_cong

⊢ ∀M M' f f'.
    (M = M') ∧ (∀a ts. (M' = Branch a ts) ⇒ (f a ts = f' a ts)) ⇒
    (ltree_CASE M f = ltree_CASE M' f')

ltree_CASE_eq

⊢ (ltree_CASE t f = v) ⇔ ∃a ts. (t = Branch a ts) ∧ (f a ts = v)

ltree_bisimulation

⊢ ∀t1 t2.
    (t1 = t2) ⇔
    ∃R. R t1 t2 ∧
        ∀a ts a' ts'.
          R (Branch a ts) (Branch a' ts') ⇒ (a = a') ∧ llist_rel R ts ts'

ltree_cases

⊢ ∀t. ∃a ts. t = Branch a ts

ltree_el_def

⊢ (ltree_el (Branch a ts) [] = SOME (a,LLENGTH ts)) ∧
  (ltree_el (Branch a ts) (n::ns) =
   case LNTH n ts of NONE => NONE | SOME t => ltree_el t ns)

ltree_el_eqv

⊢ ∀t1 t2. (t1 = t2) ⇔ ∀path. ltree_el t1 path = ltree_el t2 path

ltree_finite

⊢ ltree_finite (Branch a ts) ⇔ LFINITE ts ∧ ∀t. t ∈ LSET ts ⇒ ltree_finite t

ltree_finite_cases

⊢ ∀a0.
    ltree_finite a0 ⇔
    ∃a ts. (a0 = Branch a (fromList ts)) ∧ EVERY ltree_finite ts

ltree_finite_from_rose

⊢ ltree_finite t ⇔ ∃r. from_rose r = t

ltree_finite_ind

⊢ ∀P. (∀a ts. EVERY P ts ⇒ P (Branch a (fromList ts))) ⇒
      ∀t. ltree_finite t ⇒ P t

ltree_finite_rules

⊢ ∀a ts. EVERY ltree_finite ts ⇒ ltree_finite (Branch a (fromList ts))

ltree_finite_strongind

⊢ ∀P. (∀a ts.
         EVERY (λa0. ltree_finite a0 ∧ P a0) ts ⇒ P (Branch a (fromList ts))) ⇒
      ∀t. ltree_finite t ⇒ P t

ltree_lookup_def

⊢ (ltree_lookup t [] = SOME t) ∧
  (ltree_lookup (Branch a ts) (n::ns) =
   case LNTH n ts of NONE => NONE | SOME t => ltree_lookup t ns)

ltree_map

⊢ ltree_map f (Branch a xs) = Branch (f a) (LMAP (ltree_map f) xs)

ltree_map_id

⊢ ltree_map I t = t

ltree_map_map

⊢ ltree_map f (ltree_map g t) = ltree_map (f ∘ g) t

ltree_rel

⊢ ltree_rel R (Branch a ts) (Branch b us) ⇔
  R a b ∧ llist_rel (ltree_rel R) ts us

ltree_rel_O

⊢ ltree_rel R1 ∘ᵣ ltree_rel R2 ⊆ᵣ ltree_rel (R1 ∘ᵣ R2)

ltree_rel_eq

⊢ ltree_rel $= x y ⇔ (x = y)

ltree_set

⊢ ltree_set (Branch a ts) = a INSERT BIGUNION (IMAGE ltree_set (LSET ts))

ltree_set_map

⊢ ltree_set (ltree_map f t) = IMAGE f (ltree_set t)

ltree_unfold

⊢ ltree_unfold f seed =
  (let (a,seeds) = f seed in Branch a (LMAP (ltree_unfold f) seeds))

rose_tree_11

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

rose_tree_Axiom

⊢ ∀f0 f1 f2. ∃fn0 fn1.
    (∀a0 a1. fn0 (Rose a0 a1) = f0 a0 a1 (fn1 a1)) ∧ (fn1 [] = f1) ∧
    ∀a0 a1. fn1 (a0::a1) = f2 a0 a1 (fn0 a0) (fn1 a1)

rose_tree_case_cong

⊢ ∀M M' f.
    (M = M') ∧ (∀a0 a1. (M' = Rose a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ⇒
    (rose_tree_CASE M f = rose_tree_CASE M' f')

rose_tree_case_eq

⊢ (rose_tree_CASE x f = v) ⇔ ∃a l. (x = Rose a l) ∧ (f a l = v)

rose_tree_induction

⊢ ∀P. (∀a ts. (∀a'. MEM a' ts ⇒ P a') ⇒ P (Rose a ts)) ⇒ ∀v. P v

rose_tree_nchotomy

⊢ ∀rr. ∃a l. rr = Rose a l

subtrees

⊢ subtrees (Branch a ts) =
  Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts))