Structure lbtreeTheory

signature lbtreeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Lf_def : thm
    val Lfrep_def : thm
    val Nd_def : thm
    val Ndrep_def : thm
    val bf_flatten_def : thm
    val depth_def : thm
    val finite_def : thm
    val is_lbtree_def : thm
    val is_mmindex_def : thm
    val lbtree_TY_DEF : thm
    val lbtree_absrep : thm
    val lbtree_case_def : thm
    val map_def : thm
    val mem_def : thm
    val mindepth_def : thm
    val path_follow_def : thm
  
  (*  Theorems  *)
    val EXISTS_FIRST : thm
    val Lf_NOT_Nd : thm
    val Nd_11 : thm
    val bf_flatten_append : thm
    val bf_flatten_eq_lnil : thm
    val depth_cases : thm
    val depth_ind : thm
    val depth_mem : thm
    val depth_rules : thm
    val depth_strongind : thm
    val exists_bf_flatten : thm
    val finite_cases : thm
    val finite_ind : thm
    val finite_map : thm
    val finite_rules : thm
    val finite_strongind : thm
    val finite_thm : thm
    val lbtree_bisimulation : thm
    val lbtree_case_thm : thm
    val lbtree_cases : thm
    val lbtree_strong_bisimulation : thm
    val lbtree_ue_Axiom : thm
    val map_eq_Lf : thm
    val map_eq_Nd : thm
    val mem_bf_flatten : thm
    val mem_cases : thm
    val mem_depth : thm
    val mem_ind : thm
    val mem_mindepth : thm
    val mem_rules : thm
    val mem_strongind : thm
    val mem_thm : thm
    val mindepth_depth : thm
    val mindepth_thm : thm
    val mmindex_EXISTS : thm
    val mmindex_unique : thm
    val optmin_def : thm
    val optmin_ind : thm
  
  val lbtree_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [llist] Parent theory of "lbtree"
   
   [Lf_def]  Definition
      
      ⊢ Lf = lbtree_abs Lfrep
   
   [Lfrep_def]  Definition
      
      ⊢ Lfrep = (λl. NONE)
   
   [Nd_def]  Definition
      
      ⊢ ∀a t1 t2.
            Nd a t1 t2 =
            lbtree_abs (Ndrep a (lbtree_rep t1) (lbtree_rep t2))
   
   [Ndrep_def]  Definition
      
      ⊢ ∀a t1 t2.
            Ndrep a t1 t2 =
            (λl. case l of [] => SOME a | T::xs => t1 xs | F::xs => t2 xs)
   
   [bf_flatten_def]  Definition
      
      ⊢ (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]  Definition
      
      ⊢ 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]  Definition
      
      ⊢ 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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION is_lbtree rep
   
   [lbtree_absrep]  Definition
      
      ⊢ (∀a. lbtree_abs (lbtree_rep a) = a) ∧
        ∀r. is_lbtree r ⇔ (lbtree_rep (lbtree_abs r) = r)
   
   [lbtree_case_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ 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]  Definition
      
      ⊢ ∀x t.
            lbtree$mindepth x t =
            if mem x t then SOME (LEAST n. lbtree$depth x t n)
            else NONE
   
   [path_follow_def]  Definition
      
      ⊢ (∀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
   
   [EXISTS_FIRST]  Theorem
      
      ⊢ ∀l.
            EXISTS P l ⇒
            ∃l1 x l2. (l = l1 ⧺ x::l2) ∧ EVERY ($~ ∘ P) l1 ∧ P x
   
   [Lf_NOT_Nd]  Theorem
      
      ⊢ Lf ≠ Nd a t1 t2
   
   [Nd_11]  Theorem
      
      ⊢ (Nd a1 t1 u1 = Nd a2 t2 u2) ⇔ (a1 = a2) ∧ (t1 = t2) ∧ (u1 = u2)
   
   [bf_flatten_append]  Theorem
      
      ⊢ ∀l1. EVERY ($= Lf) l1 ⇒ (bf_flatten (l1 ⧺ l2) = bf_flatten l2)
   
   [bf_flatten_eq_lnil]  Theorem
      
      ⊢ ∀l. (bf_flatten l = [||]) ⇔ EVERY ($= Lf) l
   
   [depth_cases]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x t n. lbtree$depth x t n ⇒ mem x t
   
   [depth_rules]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ exists ($= x) (bf_flatten tlist) ⇒ EXISTS (mem x) tlist
   
   [finite_cases]  Theorem
      
      ⊢ ∀a0.
            finite a0 ⇔
            (a0 = Lf) ∨ ∃a t1 t2. (a0 = Nd a t1 t2) ∧ finite t1 ∧ finite t2
   
   [finite_ind]  Theorem
      
      ⊢ ∀finite'.
            finite' Lf ∧
            (∀a t1 t2. finite' t1 ∧ finite' t2 ⇒ finite' (Nd a t1 t2)) ⇒
            ∀a0. finite a0 ⇒ finite' a0
   
   [finite_map]  Theorem
      
      ⊢ finite (map f t) ⇔ finite t
   
   [finite_rules]  Theorem
      
      ⊢ finite Lf ∧ ∀a t1 t2. finite t1 ∧ finite t2 ⇒ finite (Nd a t1 t2)
   
   [finite_strongind]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (finite Lf ⇔ T) ∧ (finite (Nd a t1 t2) ⇔ finite t1 ∧ finite t2)
   
   [lbtree_bisimulation]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (lbtree_case e f Lf = e) ∧
        (lbtree_case e f (Nd a t1 t2) = f a t1 t2)
   
   [lbtree_cases]  Theorem
      
      ⊢ ∀t. (t = Lf) ∨ ∃a t1 t2. t = Nd a t1 t2
   
   [lbtree_strong_bisimulation]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f.
            ∃!g.
                ∀x.
                    g x =
                    case f x of
                      NONE => Lf
                    | SOME (b,y,z) => Nd b (g y) (g z)
   
   [map_eq_Lf]  Theorem
      
      ⊢ ((map f t = Lf) ⇔ (t = Lf)) ∧ ((Lf = map f t) ⇔ (t = Lf))
   
   [map_eq_Nd]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ exists ($= x) (bf_flatten tlist) ⇔ EXISTS (mem x) tlist
   
   [mem_cases]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x t. mem x t ⇒ ∃n. lbtree$depth x t n
   
   [mem_ind]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x t. mem x t ⇒ ∃n. lbtree$mindepth x t = SOME n
   
   [mem_rules]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (mem a Lf ⇔ F) ∧
        (mem a (Nd b t1 t2) ⇔ (a = b) ∨ mem a t1 ∨ mem a t2)
   
   [mindepth_depth]  Theorem
      
      ⊢ (lbtree$mindepth x t = SOME n) ⇒ lbtree$depth x t n
   
   [mindepth_thm]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ EXISTS (λe. ∃n. f e = SOME n) l ⇒ ∃i m. lbtree$is_mmindex f l i m
   
   [mmindex_unique]  Theorem
      
      ⊢ lbtree$is_mmindex f l i m ⇒
        ∀j n. lbtree$is_mmindex f l j n ⇔ (j = i) ∧ (n = m)
   
   [optmin_def]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ ∀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
   
   
*)
end

HOL 4, Kananaskis-11