Structure alist_treeTheory

signature alist_treeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val count_append_def : thm
    val is_insert_def : thm
    val is_lookup_def : thm
    val option_choice_f_def : thm
    val sorted_alist_repr_def : thm
  
  (*  Theorems  *)
    val DISJ_EQ_IMP : thm
    val HD_APPEND : thm
    val HD_MAP : thm
    val HD_MEM : thm
    val LAST_APPEND : thm
    val SORTED_APPEND_trans_IFF : thm
    val alist_repr_choice_trans_left : thm
    val alist_repr_refl : thm
    val alookup_append_option_choice_f : thm
    val alookup_empty_option_choice_f : thm
    val alookup_to_option_choice : thm
    val balance_l : thm
    val balance_r : thm
    val count_append_HD_LAST : thm
    val empty_is_ALOOKUP : thm
    val insert_fl_R : thm
    val insert_fl_R_append : thm
    val is_insert_centre : thm
    val is_insert_centre_rule : thm
    val is_insert_far_left : thm
    val is_insert_far_right : thm
    val is_insert_l : thm
    val is_insert_overwrite : thm
    val is_insert_r : thm
    val is_insert_to_empty : thm
    val is_lookup_centre : thm
    val is_lookup_empty : thm
    val is_lookup_far_left : thm
    val is_lookup_far_right : thm
    val is_lookup_hit : thm
    val is_lookup_l : thm
    val is_lookup_r : thm
    val lookup_repr : thm
    val option_choice_f_assoc : thm
    val repr_insert : thm
    val set_count : thm
    val sorted_fst_insert_centre : thm
  
  val alist_tree_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [alist] Parent theory of "alist_tree"
   
   [count_append_def]  Definition
      
      ⊢ ∀n xs ys. count_append n xs ys = xs ⧺ ys
   
   [is_insert_def]  Definition
      
      ⊢ ∀frame_l frame_r R k x al al'.
            is_insert frame_l frame_r R k x al al' ⇔
            irreflexive R ∧ transitive R ⇒
            SORTED R (MAP FST al) ⇒
            ALOOKUP al' = ALOOKUP ((k,x)::al) ∧
            (frame_l ⇒ al ≠ [] ∧ FST (HD al') = FST (HD al)) ∧
            (frame_r ⇒ al ≠ [] ∧ FST (LAST al') = FST (LAST al)) ∧
            SORTED R (MAP FST al')
   
   [is_lookup_def]  Definition
      
      ⊢ ∀fl fr R al x r.
            is_lookup fl fr R al x r ⇔
            ∀xs ys.
                fl ∨ xs = [] ⇒
                fr ∨ ys = [] ⇒
                irreflexive R ∧ transitive R ⇒
                SORTED R (MAP FST (xs ⧺ al ⧺ ys)) ⇒
                ALOOKUP (xs ⧺ al ⧺ ys) x = r
   
   [option_choice_f_def]  Definition
      
      ⊢ ∀f g. option_choice_f f g = (λx. OPTION_CHOICE (f x) (g x))
   
   [sorted_alist_repr_def]  Definition
      
      ⊢ ∀R al f.
            sorted_alist_repr R al f ⇔
            SORTED R (MAP FST al) ∧ irreflexive R ∧ transitive R ∧
            f = ALOOKUP al
   
   [DISJ_EQ_IMP]  Theorem
      
      ⊢ P ∨ Q ⇔ ¬P ⇒ Q
   
   [HD_APPEND]  Theorem
      
      ⊢ HD (xs ⧺ ys) = if xs = [] then HD ys else HD xs
   
   [HD_MAP]  Theorem
      
      ⊢ xs ≠ [] ⇒ HD (MAP f xs) = f (HD xs)
   
   [HD_MEM]  Theorem
      
      ⊢ xs ≠ [] ⇒ MEM (HD xs) xs
   
   [LAST_APPEND]  Theorem
      
      ⊢ LAST (xs ⧺ ys) = if ys = [] then LAST xs else LAST ys
   
   [SORTED_APPEND_trans_IFF]  Theorem
      
      ⊢ transitive R ⇒
        (SORTED R (xs ⧺ ys) ⇔
         SORTED R xs ∧ SORTED R ys ∧ ∀x y. MEM x xs ⇒ MEM y ys ⇒ R x y)
   
   [alist_repr_choice_trans_left]  Theorem
      
      ⊢ sorted_alist_repr R al f ∧
        sorted_alist_repr R al' (option_choice_f (ALOOKUP al) g) ⇒
        sorted_alist_repr R al' (option_choice_f f g)
   
   [alist_repr_refl]  Theorem
      
      ⊢ ∀al.
            irreflexive R ∧ transitive R ⇒
            SORTED R (MAP FST al) ⇒
            sorted_alist_repr R al (ALOOKUP al)
   
   [alookup_append_option_choice_f]  Theorem
      
      ⊢ ALOOKUP (xs ⧺ ys) = option_choice_f (ALOOKUP xs) (ALOOKUP ys)
   
   [alookup_empty_option_choice_f]  Theorem
      
      ⊢ option_choice_f (ALOOKUP []) f = f ∧
        option_choice_f f (ALOOKUP []) = f
   
   [alookup_to_option_choice]  Theorem
      
      ⊢ ALOOKUP (x::y::zs) =
        option_choice_f (ALOOKUP [x]) (ALOOKUP (y::zs)) ∧
        option_choice_f (ALOOKUP []) g = g
   
   [balance_l]  Theorem
      
      ⊢ count_append i xs (count_append j ys zs) =
        count_append ARB (count_append ARB xs ys) zs
   
   [balance_r]  Theorem
      
      ⊢ count_append i (count_append j xs ys) zs =
        count_append ARB xs (count_append ARB ys zs)
   
   [count_append_HD_LAST]  Theorem
      
      ⊢ HD (count_append i (count_append j xs ys) zs) =
        HD (count_append 0 xs (count_append 0 ys zs)) ∧
        HD (count_append i (x::xs) ys) = x ∧
        HD (count_append i [] ys) = HD ys ∧
        LAST (count_append i xs (count_append j ys zs)) =
        LAST (count_append 0 (count_append 0 xs ys) zs) ∧
        LAST (count_append i xs (y::ys)) = LAST (y::ys) ∧
        LAST (count_append i xs []) = LAST xs ∧ HD (x::xs) = x ∧
        LAST (x::y::zs) = LAST (y::zs) ∧ LAST [x] = x ∧
        (count_append i (count_append j xs ys) zs = [] ⇔
         count_append 0 xs (count_append 0 ys zs) = []) ∧
        (count_append i [] ys = [] ⇔ ys = []) ∧
        (count_append i (x::xs) ys = [] ⇔ F) ∧ (x::xs = [] ⇔ F)
   
   [empty_is_ALOOKUP]  Theorem
      
      ⊢ (λx. NONE) = ALOOKUP []
   
   [insert_fl_R]  Theorem
      
      ⊢ is_insert fl fr R k x al al' ⇒
        fl ⇒
        SORTED R (MAP FST al) ⇒
        irreflexive R ∧ transitive R ⇒
        k = FST (HD al) ∨ R (HD (MAP FST al)) k
   
   [insert_fl_R_append]  Theorem
      
      ⊢ is_insert T fr R k x r r' ⇒
        SORTED R (MAP FST (l ⧺ r)) ⇒
        irreflexive R ∧ transitive R ⇒
        ¬MEM k (MAP FST l)
   
   [is_insert_centre]  Theorem
      
      ⊢ ∀R n k x.
            l ≠ [] ⇒
            R (FST (LAST l)) k ⇒
            r ≠ [] ⇒
            R k (FST (HD r)) ⇒
            is_insert T T R k x (count_append n l r)
              (count_append ARB l (count_append ARB [(k,x)] r))
   
   [is_insert_centre_rule]  Theorem
      
      ⊢ (fl ⇒ l ≠ []) ⇒
        (l ≠ [] ⇒ R (FST (LAST l)) k) ⇒
        (fr ⇒ r ≠ []) ⇒
        (r ≠ [] ⇒ R k (FST (HD r))) ⇒
        is_insert fl fr R k x (count_append n l r)
          (count_append ARB l (count_append ARB [(k,x)] r))
   
   [is_insert_far_left]  Theorem
      
      ⊢ ∀R k x xs.
            xs ≠ [] ⇒
            R k (FST (HD xs)) ⇒
            is_insert F T R k x xs (count_append ARB [(k,x)] xs)
   
   [is_insert_far_right]  Theorem
      
      ⊢ ∀R k x xs.
            xs ≠ [] ⇒
            R (FST (LAST xs)) k ⇒
            is_insert T F R k x xs (count_append ARB xs [(k,x)])
   
   [is_insert_l]  Theorem
      
      ⊢ ∀n.
            is_insert fl T R k x l l' ⇒
            is_insert fl T R k x (count_append n l r)
              (count_append ARB l' r)
   
   [is_insert_overwrite]  Theorem
      
      ⊢ ∀R k x v. FST v = k ⇒ is_insert T T R k x [v] [(k,x)]
   
   [is_insert_r]  Theorem
      
      ⊢ ∀n.
            is_insert T fr R k x r r' ⇒
            is_insert T fr R k x (count_append n l r)
              (count_append ARB l r')
   
   [is_insert_to_empty]  Theorem
      
      ⊢ ∀R k x. is_insert F F R k x [] [(k,x)]
   
   [is_lookup_centre]  Theorem
      
      ⊢ ∀R n l r k.
            l ≠ [] ⇒
            R (FST (LAST l)) k ⇒
            r ≠ [] ⇒
            R k (FST (HD r)) ⇒
            is_lookup T T R (count_append n l r) k NONE
   
   [is_lookup_empty]  Theorem
      
      ⊢ ∀R k al. al = [] ⇒ is_lookup F F R al k NONE
   
   [is_lookup_far_left]  Theorem
      
      ⊢ ∀R k k' v. R k k' ⇒ is_lookup F T R [(k',v)] k NONE
   
   [is_lookup_far_right]  Theorem
      
      ⊢ ∀R k k' v. R k' k ⇒ is_lookup T F R [(k',v)] k NONE
   
   [is_lookup_hit]  Theorem
      
      ⊢ ∀R k k' v. k' = k ⇒ is_lookup T T R [(k',v)] k (SOME v)
   
   [is_lookup_l]  Theorem
      
      ⊢ ∀n.
            is_lookup fl T R l x res ⇒
            is_lookup fl T R (count_append n l r) x res
   
   [is_lookup_r]  Theorem
      
      ⊢ ∀n.
            is_lookup T fr R r x res ⇒
            is_lookup T fr R (count_append n l r) x res
   
   [lookup_repr]  Theorem
      
      ⊢ sorted_alist_repr R al f ∧ is_lookup fl fr R al x r ⇒ f x = r
   
   [option_choice_f_assoc]  Theorem
      
      ⊢ option_choice_f (option_choice_f f g) h =
        option_choice_f f (option_choice_f g h)
   
   [repr_insert]  Theorem
      
      ⊢ sorted_alist_repr R al f ∧ is_insert fl fr R k x al al' ⇒
        sorted_alist_repr R al' (option_choice_f (ALOOKUP [(k,x)]) f)
   
   [set_count]  Theorem
      
      ⊢ ∀j. count_append i xs ys = count_append j xs ys
   
   [sorted_fst_insert_centre]  Theorem
      
      ⊢ ∀k.
            SORTED R (MAP FST l ⧺ MAP FST r) ⇒
            (l ≠ [] ⇒ R (FST (LAST l)) k) ⇒
            (r ≠ [] ⇒ R k (FST (HD r))) ⇒
            SORTED R (MAP FST l ⧺ k::MAP FST r)
   
   
*)
end

HOL 4, Kananaskis-13