Theory ltree

⊢ finite_branching = ltree_every (λa ts. LFINITE ts)

⊢ ∃rep. TYPE_DEFINITION ltree_rep_ok rep

⊢ ∀t p. ltree_branching t p = SND (THE (ltree_el t p))

⊢ ltree_children =
  WFREC (@R. WF R) (λltree_children a'. case a' of Branch a ts => I ts)

⊢ ∀f t p.
    ltree_delete f t p =
    gen_ltree
      (λns.
           (let
              (d,len) = THE (ltree_el t ns);
              m = THE len
            in
              if ns = p ∧ len ≠ NONE ∧ 0 < m then (f d,SOME (m − 1))
              else (d,len)))

⊢ ∀f t p t0.
    ltree_insert f t p t0 =
    gen_ltree
      (λns.
           if ltree_el t ns ≠ NONE then
             (let
                (d,len) = THE (ltree_el t ns);
                m = THE len
              in
                if ns = p ∧ len ≠ NONE then (f d,SOME (m + 1)) else (d,len))
           else THE (ltree_el t0 (DROP (LENGTH p + 1) ns)))

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

⊢ ltree_node =
  WFREC (@R. WF R) (λltree_node a'. case a' of Branch a ts => I a)

⊢ ∀t. ltree_paths t = {p | ltree_lookup t p ≠ NONE}

⊢ ∀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)

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

⊢ ∀s. parent_inclusive s ⇔ ∀p q. p ∈ s ∧ q ≼ p ⇒ q ∈ s

⊢ ∀s. FINITE s ⇒
      s = IMAGE (path_index s) (count (CARD s)) ∧
      ∀j k.
        j < CARD s ∧ k < CARD s ∧ j < k ⇒
        ¬ltree_path_lt (path_index s k) (path_index s j)

⊢ ∀a ts. rose_children (Rose a ts) = ts

⊢ ∀a ts. rose_node (Rose a ts) = a

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

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

⊢ (∀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)

⊢ ∀s. sibling_inclusive s ⇔
      ∀p q.
        p ∈ s ∧ p ≠ [] ∧ q ≠ [] ∧ FRONT q = FRONT p ∧ LAST q < LAST p ⇒
        q ∈ s

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

⊢ ∀t. ltree_finite t ⇒ from_rose (to_rose t) = t

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

⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_lookup t p ≠ NONE

⊢ [] ∈ ltree_paths t

⊢ DATATYPE (ltree Branch)

⊢ DATATYPE (rose_tree Rose)

⊢ ∀t. finite_branching t ⇔
      ∃a ts. t = Branch a (fromList ts) ∧ EVERY finite_branching ts

⊢ ∀t. finite_branching t ⇔
      ∃a ts. t = Branch a ts ∧ LFINITE ts ∧ every finite_branching ts

⊢ ∀P. (∀t. P t ⇒ ∃a ts. t = Branch a (fromList ts) ∧ EVERY P ts) ⇒
      ∀t. P t ⇒ finite_branching t

⊢ ∀P. (∀t. P t ⇒ ∃a ts. t = Branch a ts ∧ LFINITE ts ∧ every P ts) ⇒
      ∀t. P t ⇒ finite_branching t

⊢ ∀p t.
    finite_branching t ∧ p ∈ ltree_paths t ⇒
    ∃d m. ltree_el t p = SOME (d,SOME m)

⊢ finite_branching (Branch a ts) ⇔ LFINITE ts ∧ every finite_branching ts

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

⊢ ∀a ts.
    LFINITE ts ∧ every finite_branching ts ⇒ finite_branching (Branch a ts)

⊢ ∀t. from_rose t =
      Branch (rose_node t) (fromList (MAP from_rose (rose_children t)))

⊢ ∀r1 r2. from_rose r1 = from_rose r2 ⇔ r1 = r2

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

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

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

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

⊢ ∀t. gen_ltree (λp. THE (ltree_el t p)) = t

⊢ ∀t f.
    gen_ltree (λp. if ltree_el t p ≠ NONE then THE (ltree_el t p) else f p) =
    t

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

⊢ ∀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'

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

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

⊢ ∀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'

⊢ ∀h p a ts.
    h::p ∈ ltree_paths (Branch a ts) ⇒
    ltree_branching (Branch a ts) (h::p) =
    ltree_branching (THE (LNTH h ts)) p

⊢ ∀a ts. ltree_branching (Branch a ts) [] = LLENGTH ts

⊢ ∀p t.
    p ∈ ltree_paths t ⇒
    ltree_branching t p = LLENGTH (ltree_children (THE (ltree_lookup t p)))

⊢ ∀p t m.
    p ∈ ltree_paths t ∧ ltree_branching t p = SOME m ⇒
    ∀h. h < m ⇔ SNOC h p ∈ ltree_paths t

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

⊢ ltree_children (Branch a ts) = ts

⊢ ∀P. (∀a ts. P (Branch a ts)) ⇒ ∀v. P v

⊢ ∀f a ts h p t.
    LNTH h ts = SOME t ∧ ltree_el t p ≠ NONE ⇒
    ltree_delete f (Branch a ts) (h::p) =
    Branch a
      (LGENLIST
         (λi.
              if i = h then ltree_delete f (THE (LNTH h ts)) p
              else THE (LNTH i ts)) (LLENGTH ts))

⊢ ∀f a ts.
    ltree_delete f (Branch a ts) [] =
    if LFINITE ts ∧ 0 < THE (LLENGTH ts) then
      Branch (f a)
        (LGENLIST (λi. THE (LNTH i ts)) (SOME (THE (LLENGTH ts) − 1)))
    else Branch a ts

⊢ ∀f p t. p ∈ ltree_paths t ⇒ p ∈ ltree_paths (ltree_delete f t p)

⊢ ∀f p t n.
    p ∈ ltree_paths t ∧ ltree_branching t p = SOME (SUC n) ⇒
    ltree_paths (ltree_delete f t p) =
    ltree_paths t DIFF
    IMAGE (λq. SNOC n p ⧺ q)
      (ltree_paths (THE (ltree_lookup t (SNOC n p))))

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

⊢ ∀p t.
    p ∈ ltree_paths t ⇒
    ltree_el t p =
    do
      t' <- ltree_lookup t p;
      SOME (ltree_node t',LLENGTH (ltree_children t'))
    od

⊢ 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

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

⊢ ∀f p t.
    ltree_el t p = SOME (a,SOME (SUC n)) ⇒
    ltree_el (ltree_delete f t p) p = SOME (f a,SOME n)

⊢ ∀p t.
    ltree_el t p = SOME (a,SOME (SUC n)) ⇒
    ltree_el (ltree_delete' t p) p = SOME (a,SOME n)

⊢ ∀f p t t0.
    ltree_el t p = SOME (a,SOME n) ⇒
    ltree_el (ltree_insert f t p t0) p = SOME (f a,SOME (SUC n))

⊢ ∀p t t0.
    ltree_el t p = SOME (a,SOME n) ⇒
    ltree_el (ltree_insert' t p t0) p = SOME (a,SOME (SUC n))

⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_el t p ≠ NONE

⊢ ∀p t. p ∈ ltree_paths t ⇔ ∀p'. p' ≼ p ⇒ ltree_el t p' ≠ NONE

⊢ ∀P a0.
    ltree_every P a0 ⇔
    ∃a ts. a0 = Branch a ts ∧ P a ts ∧ every (ltree_every P) ts

⊢ ∀P ltree_every'.
    (∀a0.
       ltree_every' a0 ⇒
       ∃a ts. a0 = Branch a ts ∧ P a ts ∧ every ltree_every' ts) ⇒
    ∀a0. ltree_every' a0 ⇒ ltree_every P a0

⊢ ltree_every P (Branch a ts) ⇔ P a ts ∧ every (ltree_every P) ts

⊢ ∀P a ts. P a ts ∧ every (ltree_every P) ts ⇒ ltree_every P (Branch a ts)

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

⊢ ∀t. ltree_finite t ⇔ FINITE (ltree_paths t)

⊢ ∀P f.
    (∃m. ∀seed.
       P seed ⇒
       (let
          (a,seeds) = f seed
        in
          LFINITE seeds ∧ every (λe. P e ∧ m e < m seed) seeds)) ⇒
    ∀seed. P seed ⇒ ltree_finite (ltree_unfold f seed)

⊢ ∀f. (∃m. ∀seed.
         (let
            (a,seeds) = f seed
          in
            LFINITE seeds ∧ every (λe. m e < m seed) seeds)) ⇒
      ∀seed. ltree_finite (ltree_unfold f seed)

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

⊢ ltree_finite t ⇔ ∃r. from_rose r = t

⊢ ∀t. ltree_finite t ⇒ finite_branching t

⊢ ∀t. ltree_finite t ⇒ FINITE (ltree_paths t)

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

⊢ ∀f p t t0.
    ltree_finite t ∧ p ∈ ltree_paths t ∧ ltree_finite t0 ⇒
    ltree_finite (ltree_insert f t p t0)

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

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

⊢ ∀f a ts h p t t0.
    LNTH h ts = SOME t ∧ ltree_el t p ≠ NONE ⇒
    ltree_insert f (Branch a ts) (h::p) t0 =
    Branch a
      (LGENLIST
         (λi.
              if i = h then ltree_insert f (THE (LNTH h ts)) p t0
              else THE (LNTH i ts)) (LLENGTH ts))

⊢ ∀f a ts t0.
    ltree_insert f (Branch a ts) [] t0 =
    if LFINITE ts then
      Branch (f a)
        (LGENLIST
           (λi. if i < THE (LLENGTH ts) then THE (LNTH i ts) else t0)
           (SOME (THE (LLENGTH ts) + 1)))
    else Branch a ts

⊢ ∀n p t t0 f g d len.
    ltree_branching t p = SOME (SUC n) ∧
    ltree_lookup t (SNOC n p) = SOME t0 ∧ ltree_el t p = SOME (d,len) ∧
    f (g d) = d ⇒
    ltree_insert f (ltree_delete g t p) p t0 = t

⊢ ∀n p t t0.
    ltree_branching t p = SOME (SUC n) ∧
    ltree_lookup t (SNOC n p) = SOME t0 ⇒
    ltree_insert' (ltree_delete' t p) p t0 = t

⊢ ∀f p t t0. p ∈ ltree_paths t ⇒ p ∈ ltree_paths (ltree_insert f t p t0)

⊢ ∀f p t n t0.
    p ∈ ltree_paths t ∧ ltree_branching t p = SOME n ⇒
    ltree_paths (ltree_insert f t p t0) =
    ltree_paths t ∪ IMAGE (λq. SNOC n p ⧺ q) (ltree_paths t0)

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

⊢ ∀t x xs.
    ltree_lookup t xs ≠ NONE ⇒
    ltree_lookup t (SNOC x xs) = ltree_lookup (THE (ltree_lookup t xs)) [x]

⊢ ∀l1 l2 t.
    ltree_lookup t l1 ≠ NONE ⇒
    ltree_lookup t (l1 ⧺ l2) = ltree_lookup (THE (ltree_lookup t l1)) l2

⊢ 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

⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_lookup t p ≠ NONE

⊢ ∀p t. p ∈ ltree_paths t ⇔ ∀p'. p' ≼ p ⇒ ltree_lookup t p' ≠ NONE

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

⊢ ltree_map I t = t

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

⊢ Branch (ltree_node t) (ltree_children t) = t

⊢ ltree_node (Branch a ts) = a

⊢ ∀P. (∀a ts. P (Branch a ts)) ⇒ ∀v. P v

⊢ total ltree_path_le

⊢ (¬ltree_path_lt [] [] ∧ ¬ltree_path_lt (h1::t1) []) ∧
  ltree_path_lt [] (h2::t2) ∧
  (ltree_path_lt (h1::t1) (h2::t2) ⇔
   LENGTH t1 < LENGTH t2 ∨
   LENGTH t1 = LENGTH t2 ∧ (h1 < h2 ∨ h1 = h2 ∧ ltree_path_lt t1 t2))

⊢ antisymmetric ltree_path_lt

⊢ irreflexive ltree_path_lt

⊢ ∀p q.
    p ≠ [] ∧ q ≠ [] ∧ FRONT p = FRONT q ∧ LAST p < LAST q ⇒
    ltree_path_lt p q

⊢ ∀x y xs. x < y ⇒ ltree_path_lt (SNOC x xs) (SNOC y xs)

⊢ transitive ltree_path_lt

⊢ ∀t. ltree_paths t = {p | ltree_el t p ≠ NONE}

⊢ ∀l1 l2 t. l1 ≼ l2 ∧ l2 ∈ ltree_paths t ⇒ l1 ∈ ltree_paths t

⊢ ∀f t. ltree_paths (ltree_map f t) = ltree_paths t

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

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

⊢ ltree_rel $= x y ⇔ x = y

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

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

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

⊢ ∀t. parent_inclusive (ltree_paths t)

⊢ ∀s1 s2.
    parent_inclusive s1 ∧ parent_inclusive s2 ⇒ parent_inclusive (s1 ∪ s2)

⊢ ∀s i. FINITE s ∧ i < CARD s ⇒ path_index s i ∈ s

⊢ ∀s n.
    s HAS_SIZE n ⇒
    BIJ (path_index s) (count n) s ∧
    ∀j k.
      j < n ∧ k < n ⇒
      (ltree_path_lt (path_index s j) (path_index s k) ⇔ j < k)

⊢ ∀t. ltree_finite t ⇒
      rose_children (to_rose t) =
      MAP to_rose (THE (toList (ltree_children t)))

⊢ ∀t. ltree_finite t ⇒
      rose_children (to_rose t) =
      THE (toList (LMAP to_rose (ltree_children t)))

⊢ ∀t. ltree_finite t ⇒ rose_node (to_rose t) = ltree_node t

⊢ ∀f t.
    rose_reduce f t =
    f (rose_node t) (MAP (rose_reduce f) (rose_children t))

⊢ ∀f a ts. rose_reduce f (Rose a ts) = f a (MAP (rose_reduce f) ts)

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

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

⊢ ∀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)

⊢ ∀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 x f = v ⇔ ∃a l. x = Rose a l ∧ f a l = v

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

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

⊢ ∀t. sibling_inclusive (ltree_paths t)

⊢ ∀s1 s2.
    sibling_inclusive s1 ∧ sibling_inclusive s2 ⇒
    sibling_inclusive (s1 ∪ s2)

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

⊢ ∀r. to_rose (from_rose r) = r