Theory "lbtree"

Signature

Definitions

Lf_def

⊢ Lf = lbtree_abs Lfrep

Lfrep_def

⊢ Lfrep = (λl. NONE)

Nd_def

⊢ ∀a t1 t2. Nd a t1 t2 = lbtree_abs (Ndrep a (lbtree_rep t1) (lbtree_rep t2))

Ndrep_def

⊢ ∀a t1 t2.
    Ndrep a t1 t2 =
    (λl. case l of [] => SOME a | T::xs => t1 xs | F::xs => t2 xs)

bf_flatten_def

⊢ (bf_flatten [] = [||]) ∧ (∀ts. bf_flatten (Lf::ts) = bf_flatten ts) ∧
  ∀a t1 t2 ts. bf_flatten (Nd a t1 t2::ts) = a:::bf_flatten (ts ++ [t1; t2])

depth_def

⊢ lbtree$depth =
  (λa0 a1 a2.
       ∀depth'.
         (∀a0 a1 a2.
            (∃t1 t2. (a1 = Nd a0 t1 t2) ∧ (a2 = 0)) ∨
            (∃m a t1 t2. (a1 = Nd a t1 t2) ∧ (a2 = SUC m) ∧ depth' a0 t1 m) ∨
            (∃m a t1 t2. (a1 = Nd a t1 t2) ∧ (a2 = SUC m) ∧ depth' a0 t2 m) ⇒
            depth' a0 a1 a2) ⇒
         depth' a0 a1 a2)

finite_def

⊢ finite =
  (λa0.
       ∀finite'.
         (∀a0.
            (a0 = Lf) ∨
            (∃a t1 t2. (a0 = Nd a t1 t2) ∧ finite' t1 ∧ finite' t2) ⇒
            finite' a0) ⇒
         finite' a0)

is_lbtree_def

⊢ ∀t. is_lbtree t ⇔
      ∃P. (∀t. P t ⇒ (t = Lfrep) ∨ ∃a t1 t2. P t1 ∧ P t2 ∧ (t = Ndrep a t1 t2)) ∧
          P t

is_mmindex_def

⊢ ∀f l n d.
    lbtree$is_mmindex f l n d ⇔
    n < LENGTH l ∧ (f (EL n l) = SOME d) ∧
    ∀i. i < LENGTH l ⇒
        (f (EL i l) = NONE) ∨
        ∃d'. (f (EL i l) = SOME d') ∧ d ≤ d' ∧ (i < n ⇒ d < d')

lbtree_TY_DEF

⊢ ∃rep. TYPE_DEFINITION is_lbtree rep

lbtree_absrep

⊢ (∀a. lbtree_abs (lbtree_rep a) = a) ∧
  ∀r. is_lbtree r ⇔ (lbtree_rep (lbtree_abs r) = r)

lbtree_case_def

⊢ ∀e f t.
    lbtree_case e f t =
    if t = Lf then e
    else
      f (@a. ∃t1 t2. t = Nd a t1 t2) (@t1. ∃a t2. t = Nd a t1 t2)
        (@t2. ∃a t1. t = Nd a t1 t2)

map_def

⊢ ∀f. (map f Lf = Lf) ∧
      ∀a t1 t2. map f (Nd a t1 t2) = Nd (f a) (map f t1) (map f t2)

mem_def

⊢ mem =
  (λa0 a1.
       ∀mem'.
         (∀a0 a1.
            (∃t1 t2. a1 = Nd a0 t1 t2) ∨
            (∃b t1 t2. (a1 = Nd b t1 t2) ∧ mem' a0 t1) ∨
            (∃b t1 t2. (a1 = Nd b t1 t2) ∧ mem' a0 t2) ⇒
            mem' a0 a1) ⇒
         mem' a0 a1)

mindepth_def

⊢ ∀x t.
    lbtree$mindepth x t =
    if mem x t then SOME (LEAST n. lbtree$depth x t n) else NONE

path_follow_def

⊢ (∀g x. path_follow g x [] = OPTION_MAP FST (g x)) ∧
  ∀g x h t.
    path_follow g x (h::t) =
    case g x of
      NONE => NONE
    | SOME (a,y,z) => path_follow g (if h then y else z) t

Theorems

EXISTS_FIRST

⊢ ∀l. EXISTS P l ⇒ ∃l1 x l2. (l = l1 ++ x::l2) ∧ EVERY ($¬ ∘ P) l1 ∧ P x

Lf_NOT_Nd

⊢ Lf ≠ Nd a t1 t2

Nd_11

⊢ (Nd a1 t1 u1 = Nd a2 t2 u2) ⇔ (a1 = a2) ∧ (t1 = t2) ∧ (u1 = u2)

bf_flatten_append

⊢ ∀l1. EVERY ($= Lf) l1 ⇒ (bf_flatten (l1 ++ l2) = bf_flatten l2)

bf_flatten_eq_lnil

⊢ ∀l. (bf_flatten l = [||]) ⇔ EVERY ($= Lf) l

depth_cases

⊢ ∀a0 a1 a2.
    lbtree$depth a0 a1 a2 ⇔
    (∃t1 t2. (a1 = Nd a0 t1 t2) ∧ (a2 = 0)) ∨
    (∃m a t1 t2. (a1 = Nd a t1 t2) ∧ (a2 = SUC m) ∧ lbtree$depth a0 t1 m) ∨
    ∃m a t1 t2. (a1 = Nd a t1 t2) ∧ (a2 = SUC m) ∧ lbtree$depth a0 t2 m

depth_ind

⊢ ∀depth'.
    (∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
    (∀m x a t1 t2. depth' x t1 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ∧
    (∀m x a t1 t2. depth' x t2 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ⇒
    ∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2

depth_mem

⊢ ∀x t n. lbtree$depth x t n ⇒ mem x t

depth_rules

⊢ (∀x t1 t2. lbtree$depth x (Nd x t1 t2) 0) ∧
  (∀m x a t1 t2. lbtree$depth x t1 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)) ∧
  ∀m x a t1 t2. lbtree$depth x t2 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)

depth_strongind

⊢ ∀depth'.
    (∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
    (∀m x a t1 t2.
       lbtree$depth x t1 m ∧ depth' x t1 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ∧
    (∀m x a t1 t2.
       lbtree$depth x t2 m ∧ depth' x t2 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ⇒
    ∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2

exists_bf_flatten

⊢ exists ($= x) (bf_flatten tlist) ⇒ EXISTS (mem x) tlist

finite_cases

⊢ ∀a0.
    finite a0 ⇔
    (a0 = Lf) ∨ ∃a t1 t2. (a0 = Nd a t1 t2) ∧ finite t1 ∧ finite t2

finite_ind

⊢ ∀finite'.
    finite' Lf ∧ (∀a t1 t2. finite' t1 ∧ finite' t2 ⇒ finite' (Nd a t1 t2)) ⇒
    ∀a0. finite a0 ⇒ finite' a0

finite_map

⊢ finite (map f t) ⇔ finite t

finite_rules

⊢ finite Lf ∧ ∀a t1 t2. finite t1 ∧ finite t2 ⇒ finite (Nd a t1 t2)

finite_strongind

⊢ ∀finite'.
    finite' Lf ∧
    (∀a t1 t2.
       finite t1 ∧ finite' t1 ∧ finite t2 ∧ finite' t2 ⇒ finite' (Nd a t1 t2)) ⇒
    ∀a0. finite a0 ⇒ finite' a0

finite_thm

⊢ (finite Lf ⇔ T) ∧ (finite (Nd a t1 t2) ⇔ finite t1 ∧ finite t2)

lbtree_bisimulation

⊢ ∀t u.
    (t = u) ⇔
    ∃R. R t u ∧
        ∀t u.
          R t u ⇒
          (t = Lf) ∧ (u = Lf) ∨
          ∃a t1 u1 t2 u2.
            R t1 u1 ∧ R t2 u2 ∧ (t = Nd a t1 t2) ∧ (u = Nd a u1 u2)

lbtree_case_thm

⊢ (lbtree_case e f Lf = e) ∧ (lbtree_case e f (Nd a t1 t2) = f a t1 t2)

lbtree_cases

⊢ ∀t. (t = Lf) ∨ ∃a t1 t2. t = Nd a t1 t2

lbtree_strong_bisimulation

⊢ ∀t u.
    (t = u) ⇔
    ∃R. R t u ∧
        ∀t u.
          R t u ⇒
          (t = u) ∨
          ∃a t1 u1 t2 u2.
            R t1 u1 ∧ R t2 u2 ∧ (t = Nd a t1 t2) ∧ (u = Nd a u1 u2)

lbtree_ue_Axiom

⊢ ∀f. ∃!g. ∀x. g x = case f x of NONE => Lf | SOME (b,y,z) => Nd b (g y) (g z)

map_eq_Lf

⊢ ((map f t = Lf) ⇔ (t = Lf)) ∧ ((Lf = map f t) ⇔ (t = Lf))

map_eq_Nd

⊢ (map f t = Nd a t1 t2) ⇔
  ∃a' t1' t2'.
    (t = Nd a' t1' t2') ∧ (a = f a') ∧ (t1 = map f t1') ∧ (t2 = map f t2')

mem_bf_flatten

⊢ exists ($= x) (bf_flatten tlist) ⇔ EXISTS (mem x) tlist

mem_cases

⊢ ∀a0 a1.
    mem a0 a1 ⇔
    (∃t1 t2. a1 = Nd a0 t1 t2) ∨ (∃b t1 t2. (a1 = Nd b t1 t2) ∧ mem a0 t1) ∨
    ∃b t1 t2. (a1 = Nd b t1 t2) ∧ mem a0 t2

mem_depth

⊢ ∀x t. mem x t ⇒ ∃n. lbtree$depth x t n

mem_ind

⊢ ∀mem'.
    (∀a t1 t2. mem' a (Nd a t1 t2)) ∧
    (∀a b t1 t2. mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
    (∀a b t1 t2. mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
    ∀a0 a1. mem a0 a1 ⇒ mem' a0 a1

mem_mindepth

⊢ ∀x t. mem x t ⇒ ∃n. lbtree$mindepth x t = SOME n

mem_rules

⊢ (∀a t1 t2. mem a (Nd a t1 t2)) ∧
  (∀a b t1 t2. mem a t1 ⇒ mem a (Nd b t1 t2)) ∧
  ∀a b t1 t2. mem a t2 ⇒ mem a (Nd b t1 t2)

mem_strongind

⊢ ∀mem'.
    (∀a t1 t2. mem' a (Nd a t1 t2)) ∧
    (∀a b t1 t2. mem a t1 ∧ mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
    (∀a b t1 t2. mem a t2 ∧ mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
    ∀a0 a1. mem a0 a1 ⇒ mem' a0 a1

mem_thm

⊢ (mem a Lf ⇔ F) ∧ (mem a (Nd b t1 t2) ⇔ (a = b) ∨ mem a t1 ∨ mem a t2)

mindepth_depth

⊢ (lbtree$mindepth x t = SOME n) ⇒ lbtree$depth x t n

mindepth_thm

⊢ (lbtree$mindepth x Lf = NONE) ∧
  (lbtree$mindepth x (Nd a t1 t2) =
   if x = a then SOME 0
   else
     OPTION_MAP SUC
       (lbtree$optmin (lbtree$mindepth x t1) (lbtree$mindepth x t2)))

mmindex_EXISTS

⊢ EXISTS (λe. ∃n. f e = SOME n) l ⇒ ∃i m. lbtree$is_mmindex f l i m

mmindex_unique

⊢ lbtree$is_mmindex f l i m ⇒
  ∀j n. lbtree$is_mmindex f l j n ⇔ (j = i) ∧ (n = m)

optmin_def

⊢ (lbtree$optmin NONE NONE = NONE) ∧ (lbtree$optmin (SOME x) NONE = SOME x) ∧
  (lbtree$optmin NONE (SOME y) = SOME y) ∧
  (lbtree$optmin (SOME x) (SOME y) = SOME (MIN x y))

optmin_ind

⊢ ∀P. P NONE NONE ∧ (∀x. P (SOME x) NONE) ∧ (∀y. P NONE (SOME y)) ∧
      (∀x y. P (SOME x) (SOME y)) ⇒
      ∀v v1. P v v1