Theory: cv_string

Definitions

cv_finite_map_FUPDATE_LIST_def

⊢ ∀cv_f cv_v.
    cv_finite_map_FUPDATE_LIST cv_f cv_v =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_ispair (cv_fst cv_v))
         (cv_finite_map_FUPDATE_LIST
            (cv_st_set cv_f (cv_fst (cv_fst cv_v)) (cv_snd (cv_fst cv_v)))
            (cv_snd cv_v)) (Num 0)) cv_f

cv_mk_Branch_def

⊢ ∀cv_x cv_t1 cv_t2.
    cv_mk_Branch cv_x cv_t1 cv_t2 =
    cv_if (cv_eq cv_t1 (Num 0)) cv_t2
      (Pair (Num 2) (Pair cv_x (Pair cv_t1 cv_t2)))

cv_st_del_def

⊢ ∀cv_t cv_v.
    cv_st_del cv_t cv_v =
    cv_if (cv_ispair cv_v)
      (cv_st_del_cons cv_t (cv_fst cv_v) (cv_snd cv_v))
      (cv_st_del_nil cv_t)

cv_st_del_nil_def_primitive

⊢ cv_st_del_nil =
  WFREC
    (@R. WF R ∧
         ∀cv_v.
           cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
           R (cv_snd (cv_snd (cv_snd cv_v))) cv_v)
    (λcv_st_del_nil a.
         I
           (cv_if (cv_ispair a)
              (cv_if (cv_lt (Num 1) (cv_fst a))
                 (Pair (Num 2)
                    (Pair (cv_fst (cv_snd a))
                       (Pair (cv_fst (cv_snd (cv_snd a)))
                          (cv_st_del_nil (cv_snd (cv_snd (cv_snd a)))))))
                 (Num 0)) (Num 0)))

cv_st_get_def

⊢ (∀cv_t cv_v.
     cv_st_get cv_t cv_v =
     cv_if (cv_ispair cv_v)
       (cv_st_get_cons cv_t (cv_fst cv_v) (cv_snd cv_v))
       (cv_st_get_nil cv_t)) ∧
  ∀cv_v cv_x cv_xs.
    cv_st_get_cons cv_v cv_x cv_xs =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v))) (Num 0)
            (cv_if (cv_lt (cv_fst (cv_snd cv_v)) cv_x)
               (cv_st_get_cons (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs)
               (cv_st_get (cv_fst (cv_snd (cv_snd cv_v))) cv_xs))) (Num 0))
      (Num 0)

cv_st_get_nil_def

⊢ ∀cv_v.
    cv_st_get_nil cv_v =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (cv_st_get_nil (cv_snd (cv_snd (cv_snd cv_v))))
         (Pair (Num 1) (cv_snd cv_v))) (Num 0)

cv_st_set_def

⊢ ∀cv_t cv_v cv_y.
    cv_st_set cv_t cv_v cv_y =
    cv_if (cv_ispair cv_v)
      (cv_st_set_cons cv_t (cv_fst cv_v) (cv_snd cv_v) cv_y)
      (cv_st_set_nil cv_t cv_y)

from_cv_string_fmap_str_trie_def

⊢ (∀f0. from_cv_string_fmap_str_trie f0 Nothing = Num 0) ∧
  (∀f0 v0. from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0)) ∧
  ∀f0 v0 v1 v2.
    from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
    Pair (Num 2)
      (Pair (from_char v0)
         (Pair (from_cv_string_fmap_str_trie f0 v1)
            (from_cv_string_fmap_str_trie f0 v2)))

from_string_fmap_def

⊢ ∀f m.
    from_string_fmap f m =
    from_cv_string_fmap_str_trie f (st_sets Nothing (fmap_to_alist m))

mk_Branch_def

⊢ ∀x t1 t2. mk_Branch x t1 t2 = if t1 = Nothing then t2 else Branch x t1 t2

st_del_cons_def

⊢ (∀x xs. st_del_cons Nothing x xs = Nothing) ∧
  (∀z x xs. st_del_cons (Just z) x xs = Just z) ∧
  ∀c subtrie rest x xs.
    st_del_cons (Branch c subtrie rest) x xs =
    if char_gt c x then Branch c subtrie rest
    else if char_lt c x then Branch c subtrie (st_del_cons rest x xs)
    else
      mk_Branch c
        (case xs of
           "" => st_del_nil subtrie
         | STRING x xs => st_del_cons subtrie x xs) rest

st_del_def

⊢ (∀t. st_del t "" = st_del_nil t) ∧
  ∀t x xs. st_del t (STRING x xs) = st_del_cons t x xs

st_del_nil_def_primitive

⊢ st_del_nil =
  WFREC (@R. WF R ∧ ∀y x rest. R rest (Branch x y rest))
    (λst_del_nil a.
         case a of
           Nothing => I Nothing
         | Just v4 => I Nothing
         | Branch x y rest => I (Branch x y (st_del_nil rest)))

st_flat_def

⊢ st_flat Nothing = [] ∧ (∀a. st_flat (Just a) = [("",a)]) ∧
  ∀c t1 t2.
    st_flat (Branch c t1 t2) =
    MAP (λ(k,v). (STRING c k,v)) (st_flat t1) ⧺ st_flat t2

st_get_nil_def

⊢ (∀v0 v1 rest. st_get_nil (Branch v0 v1 rest) = st_get_nil rest) ∧
  (∀x. st_get_nil (Just x) = SOME x) ∧ st_get_nil Nothing = NONE

st_make_def

⊢ (∀y. st_make "" y = Just y) ∧
  ∀x xs y. st_make (STRING x xs) y = Branch x (st_make xs y) Nothing

st_set_cons_def

⊢ (∀x xs y. st_set_cons Nothing x xs y = Branch x (st_make xs y) Nothing) ∧
  (∀z x xs y.
     st_set_cons (Just z) x xs y = Branch x (st_make xs y) (Just z)) ∧
  ∀c subtrie rest x xs y.
    st_set_cons (Branch c subtrie rest) x xs y =
    if char_gt c x then Branch x (st_make xs y) (Branch c subtrie rest)
    else if char_lt c x then Branch c subtrie (st_set_cons rest x xs y)
    else
      Branch c
        (case xs of
           "" => st_set_nil subtrie y
         | STRING x xs => st_set_cons subtrie x xs y) rest

st_set_def

⊢ (∀t y. st_set t "" y = st_set_nil t y) ∧
  ∀t x xs y. st_set t (STRING x xs) y = st_set_cons t x xs y

st_sorted_def

⊢ (st_sorted Nothing ⇔ T) ∧ (∀x. st_sorted (Just x) ⇔ T) ∧
  ∀c t1 t2.
    st_sorted (Branch c t1 t2) ⇔
    t1 ≠ Nothing ∧ st_sorted t1 ∧ st_sorted t2 ∧
    ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ char_lt c c'

str_trie_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('str_trie').
             (∀a0'.
                a0' = ind_type$CONSTR 0 (ARB,ARB) (λn. ind_type$BOTTOM) ∨
                (∃a. a0' =
                     (λa.
                          ind_type$CONSTR (SUC 0) (a,ARB)
                            (λn. ind_type$BOTTOM)) a) ∨
                (∃a0 a1 a2.
                   a0' =
                   (λa0 a1 a2.
                        ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
                          (ind_type$FCONS a1
                             (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))) a0
                     a1 a2 ∧ $var$('str_trie') a1 ∧ $var$('str_trie') a2) ⇒
                $var$('str_trie') a0') ⇒
             $var$('str_trie') a0') rep

str_trie_case_def

⊢ (∀v f f1. str_trie_CASE Nothing v f f1 = v) ∧
  (∀a v f f1. str_trie_CASE (Just a) v f f1 = f a) ∧
  ∀a0 a1 a2 v f f1. str_trie_CASE (Branch a0 a1 a2) v f f1 = f1 a0 a1 a2

str_trie_size_def

⊢ (∀f. str_trie_size f Nothing = 0) ∧
  (∀f a. str_trie_size f (Just a) = 1 + f a) ∧
  ∀f a0 a1 a2.
    str_trie_size f (Branch a0 a1 a2) =
    1 + (char_size a0 + (str_trie_size f a1 + str_trie_size f a2))

to_str_trie_curried_def

⊢ ∀x x0. to_str_trie x x0 = to_str_trie_tupled (x,x0)

to_str_trie_tupled_primitive_def

⊢ to_str_trie_tupled =
  WFREC
    (@R. WF R ∧
         (∀t0 v.
            cv_has_shape [SOME 2; NONE; NONE] v ⇒
            R (t0,cv_fst (cv_snd (cv_snd v))) (t0,v)) ∧
         ∀t0 v.
           cv_has_shape [SOME 2; NONE; NONE] v ⇒
           R (t0,cv_snd (cv_snd (cv_snd v))) (t0,v))
    (λto_str_trie_tupled a.
         case a of
           (t0,v) =>
             I
               (if cv_has_shape [SOME 2; NONE; NONE] v then
                  Branch (to_char (cv_fst (cv_snd v)))
                    (to_str_trie_tupled (t0,cv_fst (cv_snd (cv_snd v))))
                    (to_str_trie_tupled (t0,cv_snd (cv_snd (cv_snd v))))
                else if v = Num 0 then Nothing
                else Just (t0 (cv_snd v))))

to_string_fmap_def

⊢ ∀t m. to_string_fmap t m = alist_to_fmap (st_flat (to_str_trie t m))

Theorems

ALOOKUP_st_flat

⊢ st_sorted t ⇒ ALOOKUP (st_flat t) n = st_get t n

FUPDATE_LIST_pre

⊢ ∀f ls. FUPDATE_LIST_pre f ls

FUPDATE_LIST_pre_cases

⊢ ∀a0 a1.
    FUPDATE_LIST_pre a0 a1 ⇔
    ∀v0 v1.
      a1 = v0::v1 ⇒
      ∀v0' v1'. v0 = (v0',v1') ⇒ FUPDATE_LIST_pre a0⟨v0' ↦ v1'⟩ v1

FUPDATE_LIST_pre_ind

⊢ ∀FUPDATE_LIST_pre'.
    (∀f v.
       (∀v0 v1.
          v = v0::v1 ⇒
          ∀v0' v1'. v0 = (v0',v1') ⇒ FUPDATE_LIST_pre' f⟨v0' ↦ v1'⟩ v1) ⇒
       FUPDATE_LIST_pre' f v) ⇒
    ∀a0 a1. FUPDATE_LIST_pre a0 a1 ⇒ FUPDATE_LIST_pre' a0 a1

FUPDATE_LIST_pre_rules

⊢ ∀f v.
    (∀v0 v1.
       v = v0::v1 ⇒
       ∀v0' v1'. v0 = (v0',v1') ⇒ FUPDATE_LIST_pre f⟨v0' ↦ v1'⟩ v1) ⇒
    FUPDATE_LIST_pre f v

FUPDATE_LIST_pre_strongind

⊢ ∀FUPDATE_LIST_pre'.
    (∀f v.
       (∀v0 v1.
          v = v0::v1 ⇒
          ∀v0' v1'.
            v0 = (v0',v1') ⇒
            FUPDATE_LIST_pre f⟨v0' ↦ v1'⟩ v1 ∧
            FUPDATE_LIST_pre' f⟨v0' ↦ v1'⟩ v1) ⇒
       FUPDATE_LIST_pre' f v) ⇒
    ∀a0 a1. FUPDATE_LIST_pre a0 a1 ⇒ FUPDATE_LIST_pre' a0 a1

cv_finite_map_FUPDATE_LIST_thm

⊢ FUPDATE_LIST_pre f v ⇒
  from_string_fmap f_b (f |++ v) =
  cv_finite_map_FUPDATE_LIST (from_string_fmap f_b f)
    (from_list (from_pair (from_list from_char) f_b) v)

cv_mk_Branch_thm

[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_cv_string_fmap_str_trie f_a (mk_Branch x t1 t2) =
  cv_mk_Branch (from_char x) (from_cv_string_fmap_str_trie f_a t1)
    (from_cv_string_fmap_str_trie f_a t2)

cv_rep_cv_string_fmap_str_trie_datatype

⊢ (cv_rep p cv (from_cv_string_fmap_str_trie f_a) x ∧
   cv_rep Nothing_pre Nothing_cv f_b f0 ∧
   (∀v0. cv_rep (Just_pre v0) (Just_cv (f_a v0)) f_b (f1 v0)) ∧
   (∀v0 v1 v2.
      cv_rep (Branch_pre v0 v1 v2)
        (Branch_cv (from_char v0) (from_cv_string_fmap_str_trie f_a v1)
           (from_cv_string_fmap_str_trie f_a v2)) f_b (f2 v0 v1 v2)) ⇒
   cv_rep
     (p ∧ (x = Nothing ⇒ Nothing_pre) ∧ (∀v0. x = Just v0 ⇒ Just_pre v0) ∧
      ∀v0 v1 v2. x = Branch v0 v1 v2 ⇒ Branch_pre v0 v1 v2)
     (cv_if (cv_ispair cv)
        (cv_if (cv_lt (Num 1) (cv_fst cv))
           (Branch_cv (cv_fst (cv_snd cv)) (cv_fst (cv_snd (cv_snd cv)))
              (cv_snd (cv_snd (cv_snd cv)))) (Just_cv (cv_snd cv)))
        Nothing_cv) f_b (str_trie_CASE x f0 f1 f2)) ∧
  from_cv_string_fmap_str_trie f0 Nothing = Num 0 ∧
  from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0) ∧
  from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
  Pair (Num 2)
    (Pair (from_char v0)
       (Pair (from_cv_string_fmap_str_trie f0 v1)
          (from_cv_string_fmap_str_trie f0 v2)))

cv_rep_string_DOMSUB

⊢ from_to f t ⇒
  from_string_fmap f (m \\ k) =
  cv_st_del (from_string_fmap f m) (from_list from_char k)

cv_rep_string_FEMPTY

⊢ from_string_fmap f FEMPTY = Num 0

cv_rep_string_FLOOKUP

⊢ from_option f (FLOOKUP m n) =
  cv_st_get (from_string_fmap f m) (from_list from_char n)

cv_rep_string_FUPDATE

⊢ from_string_fmap f m⟨k ↦ v⟩ =
  cv_st_set (from_string_fmap f m) (from_list from_char k) (f v)

cv_st_del_cons_def

⊢ ∀cv_xs cv_x cv_v.
    cv_st_del_cons cv_v cv_x cv_xs =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v)))
            (Pair (Num 2)
               (Pair (cv_fst (cv_snd cv_v))
                  (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                     (cv_snd (cv_snd (cv_snd cv_v))))))
            (cv_if (cv_lt (cv_fst (cv_snd cv_v)) cv_x)
               (Pair (Num 2)
                  (Pair (cv_fst (cv_snd cv_v))
                     (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                        (cv_st_del_cons (cv_snd (cv_snd (cv_snd cv_v)))
                           cv_x cv_xs))))
               (cv_mk_Branch (cv_fst (cv_snd cv_v))
                  (cv_if (cv_ispair cv_xs)
                     (cv_st_del_cons (cv_fst (cv_snd (cv_snd cv_v)))
                        (cv_fst cv_xs) (cv_snd cv_xs))
                     (cv_st_del_nil (cv_fst (cv_snd (cv_snd cv_v)))))
                  (cv_snd (cv_snd (cv_snd cv_v))))))
         (Pair (Num 1) (cv_snd cv_v))) (Num 0)

cv_st_del_cons_ind

⊢ ∀P. (∀cv_v cv_x cv_xs.
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
          ¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
          cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ⇒
          P (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs) ∧
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
          ¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
          ¬cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ∧
          cv$c2b (cv_ispair cv_xs) ⇒
          P (cv_fst (cv_snd (cv_snd cv_v))) (cv_fst cv_xs) (cv_snd cv_xs)) ⇒
         P cv_v cv_x cv_xs) ⇒
      ∀v v1 v2. P v v1 v2

cv_st_del_cons_thm

[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_cv_string_fmap_str_trie f_a (st_del_cons v x xs) =
  cv_st_del_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
    (from_list from_char xs)

cv_st_del_nil_def

⊢ ∀cv_v.
    cv_st_del_nil cv_v =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (Pair (Num 2)
            (Pair (cv_fst (cv_snd cv_v))
               (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                  (cv_st_del_nil (cv_snd (cv_snd (cv_snd cv_v)))))))
         (Num 0)) (Num 0)

cv_st_del_nil_ind

⊢ ∀P. (∀cv_v.
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
          P (cv_snd (cv_snd (cv_snd cv_v)))) ⇒
         P cv_v) ⇒
      ∀v. P v

cv_st_del_nil_thm

⊢ from_cv_string_fmap_str_trie f_a (st_del_nil v) =
  cv_st_del_nil (from_cv_string_fmap_str_trie f_a v)

cv_st_del_thm

[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_cv_string_fmap_str_trie f_a (st_del t v) =
  cv_st_del (from_cv_string_fmap_str_trie f_a t) (from_list from_char v)

cv_st_get_nil_thm

⊢ from_option f_a (st_get_nil v) =
  cv_st_get_nil (from_cv_string_fmap_str_trie f_a v)

cv_st_get_thm

⊢ from_option f_a (st_get t v) =
  cv_st_get (from_cv_string_fmap_str_trie f_a t) (from_list from_char v) ∧
  from_option f_a (st_get_cons v x xs) =
  cv_st_get_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
    (from_list from_char xs)

cv_st_make_def

⊢ ∀cv_y cv_v.
    cv_st_make cv_v cv_y =
    cv_if (cv_ispair cv_v)
      (Pair (Num 2)
         (Pair (cv_fst cv_v) (Pair (cv_st_make (cv_snd cv_v) cv_y) (Num 0))))
      (Pair (Num 1) cv_y)

cv_st_make_ind

⊢ ∀P. (∀cv_v cv_y.
         (cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v) cv_y) ⇒ P cv_v cv_y) ⇒
      ∀v v1. P v v1

cv_st_make_thm

⊢ from_cv_string_fmap_str_trie f_a (st_make v y) =
  cv_st_make (from_list from_char v) (f_a y)

cv_st_set_cons_def

⊢ ∀cv_y cv_xs cv_x cv_v.
    cv_st_set_cons cv_v cv_x cv_xs cv_y =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v)))
            (Pair (Num 2)
               (Pair cv_x
                  (Pair (cv_st_make cv_xs cv_y)
                     (Pair (Num 2)
                        (Pair (cv_fst (cv_snd cv_v))
                           (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                              (cv_snd (cv_snd (cv_snd cv_v)))))))))
            (cv_if (cv_lt (cv_fst (cv_snd cv_v)) cv_x)
               (Pair (Num 2)
                  (Pair (cv_fst (cv_snd cv_v))
                     (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                        (cv_st_set_cons (cv_snd (cv_snd (cv_snd cv_v)))
                           cv_x cv_xs cv_y))))
               (Pair (Num 2)
                  (Pair (cv_fst (cv_snd cv_v))
                     (Pair
                        (cv_if (cv_ispair cv_xs)
                           (cv_st_set_cons (cv_fst (cv_snd (cv_snd cv_v)))
                              (cv_fst cv_xs) (cv_snd cv_xs) cv_y)
                           (cv_st_set_nil (cv_fst (cv_snd (cv_snd cv_v)))
                              cv_y)) (cv_snd (cv_snd (cv_snd cv_v))))))))
         (Pair (Num 2)
            (Pair cv_x
               (Pair (cv_st_make cv_xs cv_y) (Pair (Num 1) (cv_snd cv_v))))))
      (Pair (Num 2) (Pair cv_x (Pair (cv_st_make cv_xs cv_y) (Num 0))))

cv_st_set_cons_ind

⊢ ∀P. (∀cv_v cv_x cv_xs cv_y.
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
          ¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
          cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ⇒
          P (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs cv_y) ∧
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
          ¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
          ¬cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ∧
          cv$c2b (cv_ispair cv_xs) ⇒
          P (cv_fst (cv_snd (cv_snd cv_v))) (cv_fst cv_xs) (cv_snd cv_xs)
            cv_y) ⇒
         P cv_v cv_x cv_xs cv_y) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

cv_st_set_cons_thm

⊢ from_cv_string_fmap_str_trie f_a (st_set_cons v x xs y) =
  cv_st_set_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
    (from_list from_char xs) (f_a y)

cv_st_set_nil_def

⊢ ∀cv_y cv_v.
    cv_st_set_nil cv_v cv_y =
    cv_if (cv_ispair cv_v)
      (cv_if (cv_lt (Num 1) (cv_fst cv_v))
         (Pair (Num 2)
            (Pair (cv_fst (cv_snd cv_v))
               (Pair (cv_fst (cv_snd (cv_snd cv_v)))
                  (cv_st_set_nil (cv_snd (cv_snd (cv_snd cv_v))) cv_y))))
         (Pair (Num 1) cv_y)) (Pair (Num 1) cv_y)

cv_st_set_nil_ind

⊢ ∀P. (∀cv_v cv_y.
         (cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
          P (cv_snd (cv_snd (cv_snd cv_v))) cv_y) ⇒
         P cv_v cv_y) ⇒
      ∀v v1. P v v1

cv_st_set_nil_thm

⊢ from_cv_string_fmap_str_trie f_a (st_set_nil v y) =
  cv_st_set_nil (from_cv_string_fmap_str_trie f_a v) (f_a y)

cv_st_set_thm

⊢ from_cv_string_fmap_str_trie f_a (st_set t v y) =
  cv_st_set (from_cv_string_fmap_str_trie f_a t) (from_list from_char v)
    (f_a y)

datatype_str_trie

⊢ DATATYPE (str_trie Nothing Just Branch)

from_str_trie_def

⊢ from_cv_string_fmap_str_trie f0 Nothing = Num 0 ∧
  from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0) ∧
  from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
  Pair (Num 2)
    (Pair (from_char v0)
       (Pair (from_cv_string_fmap_str_trie f0 v1)
          (from_cv_string_fmap_str_trie f0 v2)))

from_to_str_trie_thm

⊢ from_to f0 t0 ⇒
  from_to (from_cv_string_fmap_str_trie f0) (to_str_trie t0)

from_to_string_fmap

⊢ from_to f0 t0 ⇒ from_to (from_string_fmap f0) (to_string_fmap t0)

st_del_Nothing

⊢ ∀xs. st_del Nothing xs = Nothing

st_del_cons_not_Branch_Nothing

⊢ ∀t x xs c rest. st_sorted t ⇒ st_del_cons t x xs ≠ Branch c Nothing rest

st_del_nil_def

⊢ (∀y x rest. st_del_nil (Branch x y rest) = Branch x y (st_del_nil rest)) ∧
  st_del_nil Nothing = Nothing ∧ ∀v. st_del_nil (Just v) = Nothing

st_del_nil_ind

⊢ ∀P. (∀x y rest. P rest ⇒ P (Branch x y rest)) ∧ P Nothing ∧
      (∀v. P (Just v)) ⇒
      ∀v. P v

st_del_st_set

⊢ st_sorted t ⇒
  st_del (st_set t n x) m =
  if m = n then st_del t m else st_set (st_del t m) n x

st_del_st_sets

⊢ st_sorted t ⇒
  st_del (st_sets t xs) n =
  st_sets (st_del t n) (FILTER (λ(k,v). k ≠ n) xs)

st_get_Nothing

⊢ ∀xs. st_get Nothing xs = NONE

st_get_cons_mk_Branch

⊢ ∀c t1 t2 x xs.
    st_get_cons (mk_Branch c t1 t2) x xs =
    if t1 = Nothing then st_get_cons t2 x xs
    else st_get_cons (Branch c t1 t2) x xs

st_get_cons_sorted_lt

⊢ ∀t h rest.
    st_sorted t ⇒
    (∀c' t1' t2'. t = Branch c' t1' t2' ⇒ char_lt h c') ⇒
    st_get_cons t h rest = NONE

st_get_cons_st_del_cons

⊢ ∀t x xs h rest.
    st_sorted t ⇒
    st_get_cons (st_del_cons t x xs) h rest =
    if h = x ∧ rest = xs then NONE else st_get_cons t h rest

st_get_cons_st_del_nil

⊢ ∀t x xs. st_get_cons (st_del_nil t) x xs = st_get_cons t x xs

st_get_cons_st_set_cons

⊢ ∀t x xs y h rest.
    st_sorted t ⇒
    st_get_cons (st_set_cons t x xs y) h rest =
    if h = x ∧ rest = xs then SOME y else st_get_cons t h rest

st_get_cons_st_set_nil

⊢ ∀t y x xs. st_get_cons (st_set_nil t y) x xs = st_get_cons t x xs

st_get_def

⊢ (∀t. st_get t "" = st_get_nil t) ∧
  (∀xs x t. st_get t (STRING x xs) = st_get_cons t x xs) ∧
  (∀xs x. st_get_cons Nothing x xs = NONE) ∧
  (∀xs x v0. st_get_cons (Just v0) x xs = NONE) ∧
  ∀xs x subtrie rest c.
    st_get_cons (Branch c subtrie rest) x xs =
    if char_gt c x then NONE
    else if char_lt c x then st_get_cons rest x xs
    else st_get subtrie xs

st_get_ind

⊢ ∀P0 P1.
    (∀t. P0 t "") ∧ (∀t x xs. P1 t x xs ⇒ P0 t (STRING x xs)) ∧
    (∀x xs. P1 Nothing x xs) ∧ (∀v0 x xs. P1 (Just v0) x xs) ∧
    (∀c subtrie rest x xs.
       (¬char_gt c x ∧ ¬char_lt c x ⇒ P0 subtrie xs) ∧
       (¬char_gt c x ∧ char_lt c x ⇒ P1 rest x xs) ⇒
       P1 (Branch c subtrie rest) x xs) ⇒
    (∀v0 v1. P0 v0 v1) ∧ ∀v0 v1 v2. P1 v0 v1 v2

st_get_nil_mk_Branch

⊢ ∀c t1 t2. st_get_nil (mk_Branch c t1 t2) = st_get_nil t2

st_get_nil_st_del_cons

⊢ ∀t x xs. st_get_nil (st_del_cons t x xs) = st_get_nil t

st_get_nil_st_del_nil

⊢ ∀t. st_get_nil (st_del_nil t) = NONE

st_get_nil_st_make

⊢ ∀xs y. st_get_nil (st_make xs y) = if xs = "" then SOME y else NONE

st_get_nil_st_set_cons

⊢ ∀t x xs y. st_get_nil (st_set_cons t x xs y) = st_get_nil t

st_get_nil_st_set_nil

⊢ ∀t y. st_get_nil (st_set_nil t y) = SOME y

st_get_st_del

⊢ ∀t k n.
    st_sorted t ⇒
    st_get (st_del t k) n = if n = k then NONE else st_get t n

st_get_st_make

⊢ ∀xs y n. st_get (st_make xs y) n = if n = xs then SOME y else NONE

st_get_st_set

⊢ ∀t k v n.
    st_sorted t ⇒
    st_get (st_set t k v) n = if n = k then SOME v else st_get t n

st_get_st_sets

⊢ st_sorted t ⇒
  st_get (st_sets t xs) n =
  case ALOOKUP xs n of NONE => st_get t n | SOME v1 => SOME v1

st_make_not_nothing

⊢ st_make xs y ≠ Nothing

st_set_cons_not_nothing

⊢ st_set_cons t x xs y ≠ Nothing

st_set_nil_def

⊢ (∀y t rest c.
     st_set_nil (Branch c t rest) y = Branch c t (st_set_nil rest y)) ∧
  (∀y. st_set_nil Nothing y = Just y) ∧
  ∀y v2. st_set_nil (Just v2) y = Just y

st_set_nil_ind

⊢ ∀P. (∀c t rest y. P rest y ⇒ P (Branch c t rest) y) ∧ (∀y. P Nothing y) ∧
      (∀v2 y. P (Just v2) y) ⇒
      ∀v v1. P v v1

st_set_nil_not_nothing

⊢ st_set_nil t y ≠ Nothing

st_sets_def

⊢ (∀t. st_sets t [] = t) ∧
  ∀t s rest a. st_sets t ((s,a)::rest) = st_set (st_sets t rest) s a

st_sets_eq

⊢ st_sorted t ⇒ ALOOKUP xs = ALOOKUP ys ⇒ st_sets t xs = st_sets t ys

st_sets_ind

⊢ ∀P. (∀t. P t []) ∧ (∀t s a rest. P t rest ⇒ P t ((s,a)::rest)) ⇒
      ∀v v1. P v v1

st_sorted_base

⊢ st_sorted Nothing ∧ st_sorted (Just x)

st_sorted_mk_Branch

⊢ st_sorted (mk_Branch c t1 t2) ⇔
  st_sorted t1 ∧ st_sorted t2 ∧
  (t1 ≠ Nothing ⇒ ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ char_lt c c')

st_sorted_not_Nothing_get

⊢ ∀t. st_sorted t ∧ t ≠ Nothing ⇒ ∃k v. st_get t k = SOME v

st_sorted_st_del

⊢ ∀t k. st_sorted t ⇒ st_sorted (st_del t k)

st_sorted_st_del_cons

⊢ ∀t x xs. st_sorted t ⇒ st_sorted (st_del_cons t x xs)

st_sorted_st_del_nil

⊢ ∀t. st_sorted t ⇒ st_sorted (st_del_nil t)

st_sorted_st_get_eq

⊢ ∀t1 t2.
    st_sorted t1 ∧ st_sorted t2 ∧ (∀n. st_get t1 n = st_get t2 n) ⇒ t1 = t2

st_sorted_st_make

⊢ ∀xs y. st_sorted (st_make xs y)

st_sorted_st_set

⊢ st_sorted t ⇒ st_sorted (st_set t m x)

st_sorted_st_set_cons

⊢ ∀t x xs y. st_sorted t ⇒ st_sorted (st_set_cons t x xs y)

st_sorted_st_set_nil

⊢ ∀t y. st_sorted t ⇒ st_sorted (st_set_nil t y)

st_sorted_st_sets

⊢ st_sorted t ⇒ st_sorted (st_sets t xs)

str_trie_11

⊢ (∀a a'. Just a = Just a' ⇔ a = a') ∧
  ∀a0 a1 a2 a0' a1' a2'.
    Branch a0 a1 a2 = Branch a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

str_trie_Axiom

⊢ ∀f0 f1 f2. ∃fn.
    fn Nothing = f0 ∧ (∀a. fn (Just a) = f1 a) ∧
    ∀a0 a1 a2. fn (Branch a0 a1 a2) = f2 a0 a1 a2 (fn a1) (fn a2)

str_trie_case_cong

⊢ ∀M M' v f f1.
    M = M' ∧ (M' = Nothing ⇒ v = v') ∧ (∀a. M' = Just a ⇒ f a = f' a) ∧
    (∀a0 a1 a2. M' = Branch a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ⇒
    str_trie_CASE M v f f1 = str_trie_CASE M' v' f' f1'

str_trie_case_eq

⊢ str_trie_CASE x v f f1 = v' ⇔
  x = Nothing ∧ v = v' ∨ (∃a. x = Just a ∧ f a = v') ∨
  ∃c s s0. x = Branch c s s0 ∧ f1 c s s0 = v'

str_trie_distinct

⊢ (∀a. Nothing ≠ Just a) ∧ (∀a2 a1 a0. Nothing ≠ Branch a0 a1 a2) ∧
  ∀a2 a1 a0 a. Just a ≠ Branch a0 a1 a2

str_trie_induction

⊢ ∀P. P Nothing ∧ (∀a. P (Just a)) ∧
      (∀s s0. P s ∧ P s0 ⇒ ∀c. P (Branch c s s0)) ⇒
      ∀s. P s

str_trie_nchotomy

⊢ ∀ss. ss = Nothing ∨ (∃a. ss = Just a) ∨ ∃c s s0. ss = Branch c s s0

to_str_trie_def

⊢ to_str_trie t0 v =
  if cv_has_shape [SOME 2; NONE; NONE] v then
    Branch (to_char (cv_fst (cv_snd v)))
      (to_str_trie t0 (cv_fst (cv_snd (cv_snd v))))
      (to_str_trie t0 (cv_snd (cv_snd (cv_snd v))))
  else if v = Num 0 then Nothing
  else Just (t0 (cv_snd v))

Theory cv_string_fmap

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems