Theory "alist_tree"

Parents alist

Signature

Constant	Type
count_append	:num -> α list -> α list -> α list
is_insert	:bool -> bool -> (α -> α -> bool) -> α -> β -> (α # β) list -> (α # β) list -> bool
is_lookup	:bool -> bool -> (α -> α -> bool) -> (α # β) list -> α -> β option -> bool
option_choice_f	:(α -> β option) -> (α -> β option) -> α -> β option
sorted_alist_repr	:(α -> α -> bool) -> (α # β) list -> (α -> β option) -> bool

Definitions

sorted_alist_repr_def

⊢ ∀R al f.
      sorted_alist_repr R al f ⇔
      SORTED R (MAP FST al) ∧ irreflexive R ∧ transitive R ∧ (f = ALOOKUP al)

option_choice_f_def

⊢ ∀f g. option_choice_f f g = (λx. OPTION_CHOICE (f x) (g x))

is_lookup_def

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

is_insert_def

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

count_append_def

⊢ ∀n xs ys. count_append n xs ys = xs ++ ys

Theorems

sorted_fst_insert_centre

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

SORTED_APPEND_trans_IFF

⊢ transitive R ⇒
  (SORTED R (xs ++ ys) ⇔
   SORTED R xs ∧ SORTED R ys ∧ ∀x y. MEM x xs ⇒ MEM y ys ⇒ R x y)

set_count

⊢ ∀j. count_append i xs ys = count_append j xs ys

repr_insert

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

option_choice_f_assoc

⊢ option_choice_f (option_choice_f f g) h =
  option_choice_f f (option_choice_f g h)

lookup_repr

⊢ sorted_alist_repr R al f ∧ is_lookup fl fr R al x r ⇒ (f x = r)

LAST_APPEND

⊢ LAST (xs ++ ys) = if ys = [] then LAST xs else LAST ys

is_lookup_r

⊢ ∀n. is_lookup T fr R r x res ⇒ is_lookup T fr R (count_append n l r) x res

is_lookup_l

⊢ ∀n. is_lookup fl T R l x res ⇒ is_lookup fl T R (count_append n l r) x res

is_lookup_hit

⊢ ∀R k k' v. (k' = k) ⇒ is_lookup T T R [(k',v)] k (SOME v)

is_lookup_far_right

⊢ ∀R k k' v. R k' k ⇒ is_lookup T F R [(k',v)] k NONE

is_lookup_far_left

⊢ ∀R k k' v. R k k' ⇒ is_lookup F T R [(k',v)] k NONE

is_lookup_empty

⊢ ∀R k al. (al = []) ⇒ is_lookup F F R al k NONE

is_lookup_centre

⊢ ∀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_insert_to_empty

⊢ ∀R k x. is_insert F F R k x [] [(k,x)]

is_insert_r

⊢ ∀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_overwrite

⊢ ∀R k x v. (FST v = k) ⇒ is_insert T T R k x [v] [(k,x)]

is_insert_l

⊢ ∀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_far_right

⊢ ∀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_far_left

⊢ ∀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_centre_rule

⊢ (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_centre

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

insert_fl_R_append

⊢ is_insert T fr R k x r r' ⇒
  SORTED R (MAP FST (l ++ r)) ⇒
  irreflexive R ∧ transitive R ⇒
  ¬MEM k (MAP FST l)

insert_fl_R

⊢ 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

HD_MEM

⊢ xs ≠ [] ⇒ MEM (HD xs) xs

HD_MAP

⊢ xs ≠ [] ⇒ (HD (MAP f xs) = f (HD xs))

HD_APPEND

⊢ HD (xs ++ ys) = if xs = [] then HD ys else HD xs

empty_is_ALOOKUP

⊢ (λx. NONE) = ALOOKUP []

DISJ_EQ_IMP

⊢ P ∨ Q ⇔ ¬P ⇒ Q

count_append_HD_LAST

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

balance_r

⊢ count_append i (count_append j xs ys) zs =
  count_append ARB xs (count_append ARB ys zs)

balance_l

⊢ count_append i xs (count_append j ys zs) =
  count_append ARB (count_append ARB xs ys) zs

alookup_to_option_choice

⊢ (ALOOKUP (x::y::zs) = option_choice_f (ALOOKUP [x]) (ALOOKUP (y::zs))) ∧
  (option_choice_f (ALOOKUP []) g = g)

alookup_empty_option_choice_f

⊢ (option_choice_f (ALOOKUP []) f = f) ∧ (option_choice_f f (ALOOKUP []) = f)

alookup_append_option_choice_f

⊢ ALOOKUP (xs ++ ys) = option_choice_f (ALOOKUP xs) (ALOOKUP ys)

alist_repr_refl

⊢ ∀al.
      irreflexive R ∧ transitive R ⇒
      SORTED R (MAP FST al) ⇒
      sorted_alist_repr R al (ALOOKUP al)

alist_repr_choice_trans_left

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