Structure alistTheory

signature alistTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ADELKEY_def : thm
    val alist_range_def : thm
    val alist_to_fmap_def : thm
    val fmap_to_alist_def : thm
  
  (*  Theorems  *)
    val ADELKEY_AFUPDKEY : thm
    val ADELKEY_AFUPDKEY_same : thm
    val ADELKEY_unchanged : thm
    val AFUPDKEY_ALOOKUP : thm
    val AFUPDKEY_I : thm
    val AFUPDKEY_comm : thm
    val AFUPDKEY_def : thm
    val AFUPDKEY_eq : thm
    val AFUPDKEY_ind : thm
    val AFUPDKEY_o : thm
    val AFUPDKEY_unchanged : thm
    val ALL_DISTINCT_FEVERY_alist_to_fmap : thm
    val ALL_DISTINCT_fmap_to_alist_keys : thm
    val ALOOKUP_ADELKEY : thm
    val ALOOKUP_ALL_DISTINCT_EL : thm
    val ALOOKUP_ALL_DISTINCT_MEM : thm
    val ALOOKUP_ALL_DISTINCT_PERM_same : thm
    val ALOOKUP_APPEND : thm
    val ALOOKUP_APPEND_same : thm
    val ALOOKUP_EQ_FLOOKUP : thm
    val ALOOKUP_FAILS : thm
    val ALOOKUP_FILTER : thm
    val ALOOKUP_IN_FRANGE : thm
    val ALOOKUP_LEAST_EL : thm
    val ALOOKUP_MAP : thm
    val ALOOKUP_MAP_2 : thm
    val ALOOKUP_MEM : thm
    val ALOOKUP_NONE : thm
    val ALOOKUP_SOME_FAPPLY_alist_to_fmap : thm
    val ALOOKUP_TABULATE : thm
    val ALOOKUP_ZIP_MAP_SND : thm
    val ALOOKUP_def : thm
    val ALOOKUP_ind : thm
    val ALOOKUP_prefix : thm
    val FDOM_alist_to_fmap : thm
    val FEVERY_alist_to_fmap : thm
    val FLOOKUP_FUPDATE_LIST_ALOOKUP_NONE : thm
    val FLOOKUP_FUPDATE_LIST_ALOOKUP_SOME : thm
    val FRANGE_alist_to_fmap_SUBSET : thm
    val FUNION_alist_to_fmap : thm
    val FUPDATE_LIST_EQ_APPEND_REVERSE : thm
    val IN_FRANGE_alist_to_fmap_suff : thm
    val LENGTH_AFUPDKEY : thm
    val LENGTH_fmap_to_alist : thm
    val MAP_FST_AFUPDKEY : thm
    val MAP_KEYS_I : thm
    val MAP_values_fmap_to_alist : thm
    val MEM_ADELKEY : thm
    val MEM_fmap_to_alist : thm
    val MEM_fmap_to_alist_FLOOKUP : thm
    val MEM_pair_fmap_to_alist_FLOOKUP : thm
    val PERM_fmap_to_alist : thm
    val alist_to_fmap_APPEND : thm
    val alist_to_fmap_FAPPLY_MEM : thm
    val alist_to_fmap_MAP : thm
    val alist_to_fmap_MAP_matchable : thm
    val alist_to_fmap_MAP_values : thm
    val alist_to_fmap_PERM : thm
    val alist_to_fmap_prefix : thm
    val alist_to_fmap_thm : thm
    val alist_to_fmap_to_alist : thm
    val alist_to_fmap_to_alist_PERM : thm
    val alookup_distinct_reverse : thm
    val alookup_filter : thm
    val alookup_stable_sorted : thm
    val flookup_fupdate_list : thm
    val fmap_to_alist_FEMPTY : thm
    val fmap_to_alist_inj : thm
    val fmap_to_alist_preserves_FDOM : thm
    val fmap_to_alist_to_fmap : thm
    val fupdate_list_funion : thm
    val mem_to_flookup : thm
    val set_MAP_FST_fmap_to_alist : thm
  
  val alist_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [finite_map] Parent theory of "alist"
   
   [ADELKEY_def]  Definition
      
      ⊢ ∀k alist. ADELKEY k alist = FILTER (λp. FST p ≠ k) alist
   
   [alist_range_def]  Definition
      
      ⊢ ∀m. alist_range m = {v | ∃k. ALOOKUP m k = SOME v}
   
   [alist_to_fmap_def]  Definition
      
      ⊢ ∀s. alist_to_fmap s = FOLDR (λ(k,v) f. f |+ (k,v)) FEMPTY s
   
   [fmap_to_alist_def]  Definition
      
      ⊢ ∀s. fmap_to_alist s = MAP (λk. (k,s ' k)) (SET_TO_LIST (FDOM s))
   
   [ADELKEY_AFUPDKEY]  Theorem
      
      ⊢ ∀ls f x y.
            x ≠ y ⇒
            ADELKEY x (AFUPDKEY y f ls) = AFUPDKEY y f (ADELKEY x ls)
   
   [ADELKEY_AFUPDKEY_same]  Theorem
      
      ⊢ ∀fd f ls. ADELKEY fd (AFUPDKEY fd f ls) = ADELKEY fd ls
   
   [ADELKEY_unchanged]  Theorem
      
      ⊢ ∀x ls. ADELKEY x ls = ls ⇔ ¬MEM x (MAP FST ls)
   
   [AFUPDKEY_ALOOKUP]  Theorem
      
      ⊢ ALOOKUP (AFUPDKEY k2 f al) k1 =
        case ALOOKUP al k1 of
          NONE => NONE
        | SOME v => if k1 = k2 then SOME (f v) else SOME v
   
   [AFUPDKEY_I]  Theorem
      
      ⊢ AFUPDKEY n I = I
   
   [AFUPDKEY_comm]  Theorem
      
      ⊢ ∀k1 k2 f1 f2 l.
            k1 ≠ k2 ⇒
            AFUPDKEY k2 f2 (AFUPDKEY k1 f1 l) =
            AFUPDKEY k1 f1 (AFUPDKEY k2 f2 l)
   
   [AFUPDKEY_def]  Theorem
      
      ⊢ (∀k f. AFUPDKEY k f [] = []) ∧
        ∀v rest k' k f.
            AFUPDKEY k f ((k',v)::rest) =
            if k = k' then (k,f v)::rest else (k',v)::AFUPDKEY k f rest
   
   [AFUPDKEY_eq]  Theorem
      
      ⊢ ∀k f1 l f2.
            (∀v. ALOOKUP l k = SOME v ⇒ f1 v = f2 v) ⇒
            AFUPDKEY k f1 l = AFUPDKEY k f2 l
   
   [AFUPDKEY_ind]  Theorem
      
      ⊢ ∀P.
            (∀k f. P k f []) ∧
            (∀k f k' v rest. (k ≠ k' ⇒ P k f rest) ⇒ P k f ((k',v)::rest)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [AFUPDKEY_o]  Theorem
      
      ⊢ AFUPDKEY k f1 (AFUPDKEY k f2 al) = AFUPDKEY k (f1 ∘ f2) al
   
   [AFUPDKEY_unchanged]  Theorem
      
      ⊢ ∀k f alist.
            (∀v. ALOOKUP alist k = SOME v ⇒ f v = v) ⇒
            AFUPDKEY k f alist = alist
   
   [ALL_DISTINCT_FEVERY_alist_to_fmap]  Theorem
      
      ⊢ ALL_DISTINCT (MAP FST ls) ⇒
        (FEVERY P (alist_to_fmap ls) ⇔ EVERY P ls)
   
   [ALL_DISTINCT_fmap_to_alist_keys]  Theorem
      
      ⊢ ∀fm. ALL_DISTINCT (MAP FST (fmap_to_alist fm))
   
   [ALOOKUP_ADELKEY]  Theorem
      
      ⊢ ∀al.
            ALOOKUP (ADELKEY k1 al) k2 =
            if k1 = k2 then NONE else ALOOKUP al k2
   
   [ALOOKUP_ALL_DISTINCT_EL]  Theorem
      
      ⊢ ∀ls n.
            n < LENGTH ls ∧ ALL_DISTINCT (MAP FST ls) ⇒
            ALOOKUP ls (FST (EL n ls)) = SOME (SND (EL n ls))
   
   [ALOOKUP_ALL_DISTINCT_MEM]  Theorem
      
      ⊢ ALL_DISTINCT (MAP FST al) ∧ MEM (k,v) al ⇒ ALOOKUP al k = SOME v
   
   [ALOOKUP_ALL_DISTINCT_PERM_same]  Theorem
      
      ⊢ ∀l1 l2.
            ALL_DISTINCT (MAP FST l1) ∧ PERM (MAP FST l1) (MAP FST l2) ∧
            set l1 = set l2 ⇒
            ALOOKUP l1 = ALOOKUP l2
   
   [ALOOKUP_APPEND]  Theorem
      
      ⊢ ∀l1 l2 k.
            ALOOKUP (l1 ⧺ l2) k =
            case ALOOKUP l1 k of NONE => ALOOKUP l2 k | SOME v => SOME v
   
   [ALOOKUP_APPEND_same]  Theorem
      
      ⊢ ∀l1 l2 l.
            ALOOKUP l1 = ALOOKUP l2 ⇒ ALOOKUP (l1 ⧺ l) = ALOOKUP (l2 ⧺ l)
   
   [ALOOKUP_EQ_FLOOKUP]  Theorem
      
      ⊢ FLOOKUP (alist_to_fmap al) = ALOOKUP al ∧
        ALOOKUP (fmap_to_alist fm) = FLOOKUP fm
   
   [ALOOKUP_FAILS]  Theorem
      
      ⊢ ALOOKUP l x = NONE ⇔ ∀k v. MEM (k,v) l ⇒ k ≠ x
   
   [ALOOKUP_FILTER]  Theorem
      
      ⊢ ∀ls x.
            ALOOKUP (FILTER (λ(k,v). P k) ls) x =
            if P x then ALOOKUP ls x else NONE
   
   [ALOOKUP_IN_FRANGE]  Theorem
      
      ⊢ ∀ls k v. ALOOKUP ls k = SOME v ⇒ v ∈ FRANGE (alist_to_fmap ls)
   
   [ALOOKUP_LEAST_EL]  Theorem
      
      ⊢ ∀ls k.
            ALOOKUP ls k =
            if MEM k (MAP FST ls) then
              SOME (EL (LEAST n. EL n (MAP FST ls) = k) (MAP SND ls))
            else NONE
   
   [ALOOKUP_MAP]  Theorem
      
      ⊢ ∀f al.
            ALOOKUP (MAP (λ(x,y). (x,f y)) al) = OPTION_MAP f ∘ ALOOKUP al
   
   [ALOOKUP_MAP_2]  Theorem
      
      ⊢ ∀f al x.
            ALOOKUP (MAP (λ(x,y). (x,f x y)) al) x =
            OPTION_MAP (f x) (ALOOKUP al x)
   
   [ALOOKUP_MEM]  Theorem
      
      ⊢ ∀al k v. ALOOKUP al k = SOME v ⇒ MEM (k,v) al
   
   [ALOOKUP_NONE]  Theorem
      
      ⊢ ∀l x. ALOOKUP l x = NONE ⇔ ¬MEM x (MAP FST l)
   
   [ALOOKUP_SOME_FAPPLY_alist_to_fmap]  Theorem
      
      ⊢ ∀al k v. ALOOKUP al k = SOME v ⇒ alist_to_fmap al ' k = v
   
   [ALOOKUP_TABULATE]  Theorem
      
      ⊢ MEM x l ⇒ ALOOKUP (MAP (λk. (k,f k)) l) x = SOME (f x)
   
   [ALOOKUP_ZIP_MAP_SND]  Theorem
      
      ⊢ ∀l1 l2 k f.
            LENGTH l1 = LENGTH l2 ⇒
            ALOOKUP (ZIP (l1,MAP f l2)) =
            OPTION_MAP f ∘ ALOOKUP (ZIP (l1,l2))
   
   [ALOOKUP_def]  Theorem
      
      ⊢ (∀q. ALOOKUP [] q = NONE) ∧
        ∀y x t q.
            ALOOKUP ((x,y)::t) q = if x = q then SOME y else ALOOKUP t q
   
   [ALOOKUP_ind]  Theorem
      
      ⊢ ∀P.
            (∀q. P [] q) ∧ (∀x y t q. (x ≠ q ⇒ P t q) ⇒ P ((x,y)::t) q) ⇒
            ∀v v1. P v v1
   
   [ALOOKUP_prefix]  Theorem
      
      ⊢ ∀ls k ls2.
            (ALOOKUP ls k = SOME v ⇒ ALOOKUP (ls ⧺ ls2) k = SOME v) ∧
            (ALOOKUP ls k = NONE ⇒ ALOOKUP (ls ⧺ ls2) k = ALOOKUP ls2 k)
   
   [FDOM_alist_to_fmap]  Theorem
      
      ⊢ ∀al. FDOM (alist_to_fmap al) = set (MAP FST al)
   
   [FEVERY_alist_to_fmap]  Theorem
      
      ⊢ EVERY P ls ⇒ FEVERY P (alist_to_fmap ls)
   
   [FLOOKUP_FUPDATE_LIST_ALOOKUP_NONE]  Theorem
      
      ⊢ ALOOKUP ls k = NONE ⇒ FLOOKUP (fm |++ REVERSE ls) k = FLOOKUP fm k
   
   [FLOOKUP_FUPDATE_LIST_ALOOKUP_SOME]  Theorem
      
      ⊢ ALOOKUP ls k = SOME v ⇒ FLOOKUP (fm |++ REVERSE ls) k = SOME v
   
   [FRANGE_alist_to_fmap_SUBSET]  Theorem
      
      ⊢ FRANGE (alist_to_fmap ls) ⊆ IMAGE SND (set ls)
   
   [FUNION_alist_to_fmap]  Theorem
      
      ⊢ ∀ls fm. alist_to_fmap ls ⊌ fm = fm |++ REVERSE ls
   
   [FUPDATE_LIST_EQ_APPEND_REVERSE]  Theorem
      
      ⊢ ∀ls fm. fm |++ ls = alist_to_fmap (REVERSE ls ⧺ fmap_to_alist fm)
   
   [IN_FRANGE_alist_to_fmap_suff]  Theorem
      
      ⊢ (∀v. MEM v (MAP SND ls) ⇒ P v) ⇒
        ∀v. v ∈ FRANGE (alist_to_fmap ls) ⇒ P v
   
   [LENGTH_AFUPDKEY]  Theorem
      
      ⊢ ∀ls. LENGTH (AFUPDKEY k f ls) = LENGTH ls
   
   [LENGTH_fmap_to_alist]  Theorem
      
      ⊢ ∀fm. LENGTH (fmap_to_alist fm) = CARD (FDOM fm)
   
   [MAP_FST_AFUPDKEY]  Theorem
      
      ⊢ MAP FST (AFUPDKEY f k alist) = MAP FST alist
   
   [MAP_KEYS_I]  Theorem
      
      ⊢ ∀fm. MAP_KEYS I fm = fm
   
   [MAP_values_fmap_to_alist]  Theorem
      
      ⊢ ∀f fm.
            MAP (λ(k,v). (k,f v)) (fmap_to_alist fm) =
            fmap_to_alist (f o_f fm)
   
   [MEM_ADELKEY]  Theorem
      
      ⊢ ∀al. MEM (k1,v) (ADELKEY k2 al) ⇔ k1 ≠ k2 ∧ MEM (k1,v) al
   
   [MEM_fmap_to_alist]  Theorem
      
      ⊢ MEM (x,y) (fmap_to_alist fm) ⇔ x ∈ FDOM fm ∧ fm ' x = y
   
   [MEM_fmap_to_alist_FLOOKUP]  Theorem
      
      ⊢ ∀p fm. MEM p (fmap_to_alist fm) ⇔ FLOOKUP fm (FST p) = SOME (SND p)
   
   [MEM_pair_fmap_to_alist_FLOOKUP]  Theorem
      
      ⊢ ∀x y fm. MEM (x,y) (fmap_to_alist fm) ⇔ FLOOKUP fm x = SOME y
   
   [PERM_fmap_to_alist]  Theorem
      
      ⊢ PERM (fmap_to_alist fm1) (fmap_to_alist fm2) ⇔ fm1 = fm2
   
   [alist_to_fmap_APPEND]  Theorem
      
      ⊢ ∀l1 l2.
            alist_to_fmap (l1 ⧺ l2) = alist_to_fmap l1 ⊌ alist_to_fmap l2
   
   [alist_to_fmap_FAPPLY_MEM]  Theorem
      
      ⊢ ∀al z.
            z ∈ FDOM (alist_to_fmap al) ⇒ MEM (z,alist_to_fmap al ' z) al
   
   [alist_to_fmap_MAP]  Theorem
      
      ⊢ ∀f1 f2 al.
            INJ f1 (set (MAP FST al)) 𝕌(:β) ⇒
            alist_to_fmap (MAP (λ(x,y). (f1 x,f2 y)) al) =
            MAP_KEYS f1 (f2 o_f alist_to_fmap al)
   
   [alist_to_fmap_MAP_matchable]  Theorem
      
      ⊢ ∀f1 f2 al mal v.
            INJ f1 (set (MAP FST al)) 𝕌(:β) ∧
            mal = MAP (λ(x,y). (f1 x,f2 y)) al ∧
            v = MAP_KEYS f1 (f2 o_f alist_to_fmap al) ⇒
            alist_to_fmap mal = v
   
   [alist_to_fmap_MAP_values]  Theorem
      
      ⊢ ∀f al.
            alist_to_fmap (MAP (λ(k,v). (k,f v)) al) =
            f o_f alist_to_fmap al
   
   [alist_to_fmap_PERM]  Theorem
      
      ⊢ ∀l1 l2.
            PERM l1 l2 ∧ ALL_DISTINCT (MAP FST l1) ⇒
            alist_to_fmap l1 = alist_to_fmap l2
   
   [alist_to_fmap_prefix]  Theorem
      
      ⊢ ∀ls l1 l2.
            alist_to_fmap l1 = alist_to_fmap l2 ⇒
            alist_to_fmap (ls ⧺ l1) = alist_to_fmap (ls ⧺ l2)
   
   [alist_to_fmap_thm]  Theorem
      
      ⊢ alist_to_fmap [] = FEMPTY ∧
        alist_to_fmap ((k,v)::t) = alist_to_fmap t |+ (k,v)
   
   [alist_to_fmap_to_alist]  Theorem
      
      ⊢ ∀al.
            fmap_to_alist (alist_to_fmap al) =
            MAP (λk. (k,THE (ALOOKUP al k)))
              (SET_TO_LIST (set (MAP FST al)))
   
   [alist_to_fmap_to_alist_PERM]  Theorem
      
      ⊢ ∀al.
            ALL_DISTINCT (MAP FST al) ⇒
            PERM (fmap_to_alist (alist_to_fmap al)) al
   
   [alookup_distinct_reverse]  Theorem
      
      ⊢ ∀l k.
            ALL_DISTINCT (MAP FST l) ⇒ ALOOKUP (REVERSE l) k = ALOOKUP l k
   
   [alookup_filter]  Theorem
      
      ⊢ ∀f l x. ALOOKUP l x = ALOOKUP (FILTER (λ(x',y). x = x') l) x
   
   [alookup_stable_sorted]  Theorem
      
      ⊢ ∀R sort x l.
            transitive R ∧ total R ∧ STABLE sort (inv_image R FST) ⇒
            ALOOKUP (sort (inv_image R FST) l) x = ALOOKUP l x
   
   [flookup_fupdate_list]  Theorem
      
      ⊢ ∀l k m.
            FLOOKUP (m |++ l) k =
            case ALOOKUP (REVERSE l) k of
              NONE => FLOOKUP m k
            | SOME v => SOME v
   
   [fmap_to_alist_FEMPTY]  Theorem
      
      ⊢ fmap_to_alist FEMPTY = []
   
   [fmap_to_alist_inj]  Theorem
      
      ⊢ ∀f1 f2. fmap_to_alist f1 = fmap_to_alist f2 ⇒ f1 = f2
   
   [fmap_to_alist_preserves_FDOM]  Theorem
      
      ⊢ ∀fm1 fm2.
            FDOM fm1 = FDOM fm2 ⇒
            MAP FST (fmap_to_alist fm1) = MAP FST (fmap_to_alist fm2)
   
   [fmap_to_alist_to_fmap]  Theorem
      
      ⊢ alist_to_fmap (fmap_to_alist fm) = fm
   
   [fupdate_list_funion]  Theorem
      
      ⊢ ∀m l. m |++ l = FEMPTY |++ l ⊌ m
   
   [mem_to_flookup]  Theorem
      
      ⊢ ∀x y l.
            ALL_DISTINCT (MAP FST l) ∧ MEM (x,y) l ⇒
            FLOOKUP (FEMPTY |++ l) x = SOME y
   
   [set_MAP_FST_fmap_to_alist]  Theorem
      
      ⊢ set (MAP FST (fmap_to_alist fm)) = FDOM fm
   
   
*)
end

HOL 4, Kananaskis-13