Theory "lbtree"

Signature

Definitions

Lfrep_def

|- Lfrep = (λl. NONE)

Ndrep_def

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

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

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)

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

Lf_def

|- Lf = lbtree_abs Lfrep

Nd_def

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

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)

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)

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)

finite_def

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

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)

mindepth_def

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

optmin_tupled_primitive_def

|- optmin_tupled =
   WFREC (@R. WF R)
     (λoptmin_tupled a.
        case a of
          (NONE,NONE) => I NONE
        | (NONE,SOME y) => I (SOME y)
        | (SOME x,NONE) => I (SOME x)
        | (SOME x,SOME y') => I (SOME (MIN x y')))

optmin_curried_def

|- ∀x x1. lbtree$optmin x x1 = optmin_tupled (x,x1)

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')

Theorems

lbtree_cases

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

Lf_NOT_Nd

|- Lf ≠ Nd a t1 t2

Nd_11

|- (Nd a1 t1 u1 = Nd a2 t2 u2) ⇔ (a1 = a2) ∧ (t1 = t2) ∧ (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)

lbtree_case_thm

|- (lbtree_case e f Lf = e) ∧ (lbtree_case e f (Nd a t1 t2) = f a t1 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_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)

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

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

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')

finite_rules

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

finite_ind

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

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_cases

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

finite_thm

|- (finite Lf ⇔ T) ∧ (finite (Nd a t1 t2) ⇔ finite t1 ∧ finite t2)

finite_map

|- finite (map f t) ⇔ finite t

bf_flatten_eq_lnil

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

bf_flatten_append

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

EXISTS_FIRST

|- ∀l. EXISTS P l ⇒ ∃l1 x l2. (l = l1 ++ x::l2) ∧ EVERY ($~ o P) l1 ∧ P x

exists_bf_flatten

|- exists ($= x) (bf_flatten tlist) ⇒ EXISTS (mem x) tlist

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

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

mem_depth

|- ∀x t. mem x t ⇒ ∃n. lbtree$depth x t n

depth_mem

|- ∀x t n. lbtree$depth x t n ⇒ mem x t

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

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

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

mem_mindepth

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

mindepth_depth

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

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)

mem_bf_flatten

|- exists ($= x) (bf_flatten tlist) ⇔ EXISTS (mem x) tlist