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

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 ($~ ∘ 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