Theory Maximal_Path_Trie

section ‹Maximal Path Tries›

text ‹Drastically reduced implementation of tries that consider only maximum length sequences as elements.
      Inserting a sequence that is prefix of some already contained sequence does not alter the trie.
      Intended to store IO-sequences to apply in testing, as in this use-case proper prefixes need not be applied separately.›

theory Maximal_Path_Trie
imports "../Util"
begin

subsection ‹Utils for Updating Associative Lists›

fun update_assoc_list_with_default :: "'a ⇒ ('b ⇒ 'b) ⇒ 'b ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where
  "update_assoc_list_with_default k f d [] = [(k,f d)]" |
  "update_assoc_list_with_default k f d ((x,y)#xys) = (if k = x
    then ((x,f y)#xys)
    else (x,y) # (update_assoc_list_with_default k f d xys))"

lemma update_assoc_list_with_default_key_found :
  assumes "distinct (map fst xys)"
  and     "i < length xys"
  and     "fst (xys ! i) = k"
shows "update_assoc_list_with_default k f d xys =
        ((take i xys) @ [(k, f (snd (xys ! i)))] @ (drop (Suc i) xys))" 
using assms proof (induction xys arbitrary: i)
  case Nil
  then show ?case by auto
next
  case (Cons a xys)
  
  show ?case
  proof (cases i)
    case 0
    then have "fst a = k" using Cons.prems(3) by auto
    then have "update_assoc_list_with_default k f d (a#xys) = (k, f (snd a)) # xys"
      unfolding 0 by (metis prod.collapse update_assoc_list_with_default.simps(2)) 
    then show ?thesis unfolding 0 by auto
  next
    case (Suc j)
    then have "fst a ≠ k"
      using Cons.prems by auto 

    have "distinct (map fst xys)"
    and  "j < length xys"
    and  "fst (xys ! j) = k"
      using Cons.prems unfolding Suc by auto

    then have "update_assoc_list_with_default k f d xys = take j xys @ [(k, f (snd (xys ! j)))] @ drop (Suc j) xys"
      using Cons.IH[of j] by auto

    then show ?thesis unfolding Suc using ‹fst a ≠ k›
      by (metis append_Cons drop_Suc_Cons nth_Cons_Suc prod.collapse take_Suc_Cons update_assoc_list_with_default.simps(2)) 
  qed 
qed 

lemma update_assoc_list_with_default_key_not_found :
  assumes "distinct (map fst xys)"
  and     "k ∉ set (map fst xys)"
shows "update_assoc_list_with_default k f d xys = xys @ [(k,f d)]"  
  using assms by (induction xys; auto)


lemma update_assoc_list_with_default_key_distinct :
  assumes "distinct (map fst xys)"
  shows "distinct (map fst (update_assoc_list_with_default k f d xys))"
proof (cases "k ∈ set (map fst xys)")
  case True
  then obtain i where "i < length xys" and "fst (xys ! i) = k"
    by (metis in_set_conv_nth length_map nth_map) 
  then have *: "(map fst (take i xys @ [(k, f (snd (xys ! i)))] @ drop (Suc i) xys)) = (map fst xys)"
  proof -
    have "xys ! i # drop (Suc i) xys = drop i xys"
      using Cons_nth_drop_Suc ‹i < length xys› by blast
    then show ?thesis
      by (metis (no_types) ‹fst (xys ! i) = k› append_Cons append_self_conv2 append_take_drop_id fst_conv list.simps(9) map_append)
  qed
  show ?thesis
    unfolding update_assoc_list_with_default_key_found[OF assms ‹i < length xys› ‹fst (xys ! i) = k›] * 
    using assms by assumption
next
  case False
  have *: "(map fst (xys @ [(k, f d)])) = (map fst xys)@[k]" by auto
  show ?thesis
    using assms False
    unfolding update_assoc_list_with_default_key_not_found[OF assms False] * by auto
qed






subsection ‹Maximum Path Trie Implementation›


datatype 'a mp_trie = MP_Trie "('a × 'a mp_trie) list"

fun mp_trie_invar :: "'a mp_trie ⇒ bool" where
  "mp_trie_invar (MP_Trie ts) = (distinct (map fst ts) ∧ (∀ t ∈ set (map snd ts) . mp_trie_invar t))"



definition empty :: "'a mp_trie" where
  "empty = MP_Trie []"

lemma empty_invar : "mp_trie_invar empty" unfolding empty_def by auto



fun height :: "'a mp_trie ⇒ nat" where
  "height (MP_Trie []) = 0" |
  "height (MP_Trie (xt#xts)) = Suc (foldr (λ t m . max (height t) m) (map snd (xt#xts)) 0)"

lemma height_0 : 
  assumes "height t = 0" 
  shows "t = empty" 
proof (rule ccontr)
  assume "t ≠ empty"
  then obtain xt xts where "t = MP_Trie (xt#xts)"
    by (metis empty_def height.cases)
  have "height t > 0" 
    unfolding ‹t = MP_Trie (xt#xts)› height.simps
    by simp
  then show "False"
    using assms by simp
qed


lemma height_inc :
  assumes "t ∈ set (map snd ts)"
  shows "height t < height (MP_Trie ts)"
proof -
  obtain xt xts where "ts = xt#xts"
    using assms
    by (metis list.set_cases list_map_source_elem) 
  
  have "height t < Suc (foldr (λ t m . max (height t) m) (map snd (xt#xts)) 0)"
    using assms unfolding ‹ts = xt#xts› using max_by_foldr[of t "(map snd (xt#xts))" height] 
    by blast

  then show ?thesis unfolding ‹ts = xt#xts› by auto
qed


fun insert :: "'a list ⇒ 'a mp_trie ⇒ 'a mp_trie" where
  "insert [] t = t" |
  "insert (x#xs) (MP_Trie ts) = (MP_Trie (update_assoc_list_with_default x (λ t . insert xs t) empty ts))"


lemma insert_invar : "mp_trie_invar t ⟹ mp_trie_invar (insert xs t)" 
proof (induction xs arbitrary: t)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)

  obtain ts where "t = MP_Trie ts"
    using mp_trie_invar.cases by auto

  then have "distinct (map fst ts)"
       and  "⋀ t . t ∈ set (map snd ts) ⟹ mp_trie_invar t"
    using Cons.prems by auto
    
  
  show ?case proof (cases "x ∈ set (map fst ts)")
    case True
    then obtain i where "i < length ts" and "fst (ts ! i) = x"
      by (metis in_set_conv_nth length_map nth_map) 
    have "insert (x#xs) (MP_Trie ts) = (MP_Trie (take i ts @ [(x, insert xs (snd (ts ! i)))] @ drop (Suc i) ts))"
      unfolding insert.simps empty_def
      unfolding update_assoc_list_with_default_key_found[OF ‹distinct (map fst ts)› ‹i < length ts› ‹fst (ts ! i) = x›
                                                        ,of "(λ t . insert xs t)" "(MP_Trie [])"] 
      by simp
    
    have "⋀ t . t ∈ set (map snd (take i ts @ [(x, insert xs (snd (ts ! i)))] @ drop (Suc i) ts)) ⟹ mp_trie_invar t"
    proof - 
      fix t assume "t ∈ set (map snd (take i ts @ [(x, insert xs (snd (ts ! i)))] @ drop (Suc i) ts))"
      then consider (a) "t ∈ set (map snd (take i ts @ drop (Suc i) ts))" |
                    (b) "t = insert xs (snd (ts ! i))" 
        by auto
      then show "mp_trie_invar t" proof cases
        case a
        then have "t ∈ set (map snd ts)"
          by (metis drop_map in_set_dropD in_set_takeD list_concat_non_elem map_append take_map) 
        then show ?thesis using ‹⋀ t . t ∈ set (map snd ts) ⟹ mp_trie_invar t› by blast
      next
        case b
        have "(snd (ts ! i)) ∈ set (map snd ts)"
          using ‹i < length ts› by auto
        then have "mp_trie_invar (snd (ts ! i))" using ‹⋀ t . t ∈ set (map snd ts) ⟹ mp_trie_invar t› by blast 
        then show ?thesis using Cons.IH unfolding b by blast
      qed 
    qed
    moreover have "distinct (map fst (take i ts @ [(x, insert xs (snd (ts ! i)))] @ drop (Suc i) ts))"
      using update_assoc_list_with_default_key_distinct[OF ‹distinct (map fst ts)›]
      by (metis ‹distinct (map fst ts)› ‹fst (ts ! i) = x› ‹i < length ts› update_assoc_list_with_default_key_found)
    
    ultimately show ?thesis 
      unfolding ‹t = MP_Trie ts› ‹insert (x#xs) (MP_Trie ts) = (MP_Trie (take i ts @ [(x, insert xs (snd (ts ! i)))] @ drop (Suc i) ts))›
      by auto
  next
    case False

    have "mp_trie_invar (insert xs empty)"
      by (simp add: empty_invar Cons.IH) 

    then show ?thesis
      using Cons.prems update_assoc_list_with_default_key_distinct[OF ‹distinct (map fst ts)›, of x "(insert xs)" "(MP_Trie [])"]
      unfolding ‹t = MP_Trie ts› insert.simps
      unfolding update_assoc_list_with_default_key_not_found[OF ‹distinct (map fst ts)› False] 
      by auto
  qed
qed 




fun paths :: "'a mp_trie ⇒ 'a list list" where
  "paths (MP_Trie []) = [[]]" |
  "paths (MP_Trie (t#ts)) = concat (map (λ (x,t) . map ((#) x) (paths t)) (t#ts))"



lemma paths_empty :
  assumes "[] ∈ set (paths t)"
  shows "t = empty"
proof (rule ccontr)
  assume "t ≠ empty"
  then obtain xt xts where "t = MP_Trie (xt#xts)"
    by (metis empty_def height.cases)
  then have "[] ∈ set (concat (map (λ (x,t) . map ((#) x) (paths t)) (xt#xts)))"
    using assms by auto
  then show "False" by auto
qed

lemma paths_nonempty :
  assumes "[] ∉ set (paths t)"
  shows "set (paths t) ≠ {}"
using assms proof (induction t rule: mp_trie_invar.induct)
  case (1 ts)
  have "ts ≠ []" using "1.prems" by auto
  then obtain x t xts where "ts = ((x,t)#xts)"
    using linear_order_from_list_position'.cases
    by (metis old.prod.exhaust) 
  
  then have "t ∈ set (map snd ts)" by auto
    
  show ?case 
  proof (cases "[] ∈ set (paths t)")
    case True
    then show ?thesis  
      unfolding ‹ts = ((x,t)#xts)› paths.simps by auto
  next
    case False
    show ?thesis 
      using "1.IH"[OF ‹t ∈ set (map snd ts)› False]  
      unfolding ‹ts = ((x,t)#xts)› paths.simps by auto
  qed
qed


lemma paths_maximal: "mp_trie_invar t ⟹ xs' ∈ set (paths t) ⟹ ¬ (∃ xs'' . xs'' ≠ [] ∧ xs'@xs'' ∈ set (paths t))"
proof (induction xs' arbitrary: t)
  case Nil
  then have "t = empty"
    using paths_empty by blast
  then have "paths t = [[]]"
    by (simp add: empty_def)
  then show ?case by auto
next
  case (Cons x xs')

  then have "t ≠ empty" unfolding empty_def by auto
  then obtain xt xts where "t = MP_Trie (xt#xts)"
    by (metis empty_def height.cases)

  obtain t' where "(x,t') ∈ set (xt#xts)"
            and   "xs' ∈ set (paths t')"
    using Cons.prems(2) 
    unfolding ‹t = MP_Trie (xt#xts)› paths.simps 
    by force

  have "mp_trie_invar t'"
    using Cons.prems(1) ‹(x,t') ∈ set (xt#xts)› unfolding ‹t = MP_Trie (xt#xts)› by auto

  show ?case 
  proof 
    assume "∃xs''. xs'' ≠ [] ∧ (x # xs') @ xs'' ∈ set (paths t)"
    then obtain xs'' where "xs'' ≠ []" and "(x # (xs' @ xs'')) ∈ set (paths (MP_Trie (xt # xts)))"
      unfolding ‹t = MP_Trie (xt#xts)› by force


    obtain t'' where "(x,t'') ∈ set (xt#xts)"
               and   "(xs' @ xs'') ∈ set (paths t'')"
      using ‹(x # (xs' @ xs'')) ∈ set (paths (MP_Trie (xt # xts)))›
      unfolding ‹t = MP_Trie (xt#xts)› paths.simps 
      by force

    have "distinct (map fst (xt#xts))"
      using Cons.prems(1) unfolding ‹t = MP_Trie (xt#xts)› by simp
    then have "t'' = t'"
      using ‹(x,t') ∈ set (xt#xts)› ‹(x,t'') ∈ set (xt#xts)›
      by (meson eq_key_imp_eq_value)  
    then have "xs'@xs'' ∈ set (paths t')"
      using ‹(xs' @ xs'') ∈ set (paths t'')› by auto
    then show "False"
      using ‹xs'' ≠ []› Cons.IH[OF ‹mp_trie_invar t'› ‹xs' ∈ set (paths t')›] by blast
  qed
qed
            


lemma paths_insert_empty : 
  "paths (insert xs empty) = [xs]"
proof (induction xs)
  case Nil
  then show ?case unfolding empty_def by auto
next
  case (Cons x xs)
  then show ?case unfolding empty_def insert.simps by auto
qed

lemma paths_order :
  assumes "set ts = set ts'"
  and     "length ts = length ts'" (* length requirement not actually necessary *)
shows "set (paths (MP_Trie ts)) = set (paths (MP_Trie ts'))"
  using assms(2,1) proof (induction ts ts' rule: list_induct2)
  case Nil
  then show ?case by auto
next
  case (Cons x xs y ys)

  have scheme: "⋀ f xs ys . set xs = set ys ⟹ set (concat (map f xs)) = set (concat (map f ys))"
    by auto

  show ?case 
    using scheme[OF Cons.prems(1), of "(λ(x, t). map ((#) x) (paths t))"] by simp
qed


lemma paths_insert_maximal :
  assumes "mp_trie_invar t" 
  shows "set (paths (insert xs t)) = (if (∃ xs' . xs@xs' ∈ set (paths t))
                                         then set (paths t)
                                         else Set.insert xs (set (paths t) - {xs' . ∃ xs'' . xs'@xs'' = xs}))" 
using assms proof (induction xs arbitrary: t)
  case Nil
  then show ?case
    using paths_nonempty by force    
next
  case (Cons x xs)
  show ?case proof (cases "t = empty")
    case True
    show ?thesis 
      unfolding True
      unfolding paths_insert_empty  
      unfolding empty_def paths.simps by auto
  next
    case False
    
    then obtain xt xts where "t = MP_Trie (xt#xts)"
      by (metis empty_def height.cases)
    then have "t = MP_Trie ((fst xt, snd xt)#xts)" 
      by auto

    have "distinct (map fst (xt#xts))"
      using Cons.prems ‹t = MP_Trie (xt#xts)› by auto

     have "(paths t) = concat (map (λ(x, t). map ((#) x) (paths t)) (xt # xts))"
      unfolding ‹t = MP_Trie ((fst xt, snd xt)#xts)› by simp
    then have "set (paths t) = {x#xs | x xs t . (x,t) ∈ set (xt#xts) ∧ xs ∈ set (paths t)}"
      by auto
    then have "Set.insert (x#xs) (set (paths t)) = Set.insert (x#xs) {x#xs | x xs t . (x,t) ∈ set (xt#xts) ∧ xs ∈ set (paths t)}"
      by blast

    show ?thesis proof (cases "x ∈ set (map fst (xt#xts))")
      case True
      case True
      then obtain i where "i < length (xt#xts)" and "fst ((xt#xts) ! i) = x"
        by (metis in_set_conv_nth list_map_source_elem)
      then have "((xt#xts) ! i) = (x,snd ((xt#xts) ! i))" by auto

      have "mp_trie_invar (snd ((xt # xts) ! i))"
        using Cons.prems ‹i < length (xt#xts)› unfolding ‹t = MP_Trie (xt#xts)›
        by (metis ‹(xt # xts) ! i = (x, snd ((xt # xts) ! i))› in_set_zipE mp_trie_invar.simps nth_mem zip_map_fst_snd) 


      have "insert (x#xs) t = MP_Trie (take i (xt # xts) @ [(x, insert xs (snd ((xt # xts) ! i)))] @ drop (Suc i) (xt # xts))"
        unfolding ‹t = MP_Trie (xt#xts)› insert.simps
        unfolding update_assoc_list_with_default_key_found[OF ‹distinct (map fst (xt#xts))› ‹i < length (xt#xts)› ‹fst ((xt#xts) ! i) = x›]
        by simp
      
      then have "set (paths (insert (x#xs) t)) 
                 = set (paths (MP_Trie (take i (xt # xts) @ [(x, insert xs (snd ((xt # xts) ! i)))] @ drop (Suc i) (xt # xts))))"
        by simp
      also have "... = set (paths (MP_Trie ((x, insert xs (snd ((xt # xts) ! i))) # (take i (xt # xts) @ drop (Suc i) (xt # xts)))))"
        using paths_order[of "(take i (xt # xts) @ [(x, insert xs (snd ((xt # xts) ! i)))] @ drop (Suc i) (xt # xts))" 
                             "((x, insert xs (snd ((xt # xts) ! i))) # (take i (xt # xts) @ drop (Suc i) (xt # xts)))"]
        by force
      also have "... = set ((map ((#) x) (paths (insert xs (snd ((xt # xts) ! i))))) @ (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))))"
        unfolding paths.simps by force
      finally have "set (paths (insert (x#xs) t)) = 
                      set (map ((#) x) (paths (insert xs (snd ((xt # xts) ! i))))) 
                      ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        by force
      also have "… = (image ((#) x) (set (paths (insert xs (snd ((xt # xts) ! i))))))
                      ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        by auto
      finally have pi1: "set (paths (insert (x#xs) t)) = 
                      image ((#) x) (if ∃xs'. xs @ xs' ∈ set (paths (snd ((xt # xts) ! i))) then set (paths (snd ((xt # xts) ! i)))
                                                                                            else Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs}))
                       ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        unfolding Cons.IH[OF ‹mp_trie_invar (snd ((xt # xts) ! i))›] by blast



      have po1: "set (xt#xts) = set ((x,snd ((xt#xts) ! i)) # ((take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        using list_index_split_set[OF ‹i < length (xt#xts)›] 
        unfolding ‹((xt#xts) ! i) = (x,snd ((xt#xts) ! i))›[symmetric] by assumption
      have po2: "length (xt#xts) = length ((x,snd ((xt#xts) ! i)) # ((take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        using ‹i < length (xt#xts)› by auto


      have "set (paths t) = set (paths (MP_Trie ((x,snd ((xt#xts) ! i)) # ((take i (xt # xts) @ drop (Suc i) (xt # xts))))))"
        unfolding ‹t = MP_Trie (xt#xts)› 
        using paths_order[OF po1 po2] by assumption
      also have "… = set ((map ((#) x) (paths (snd ((xt # xts) ! i)))) @ (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))))"
        unfolding paths.simps by auto
      finally have "set (paths t) = 
                      set (map ((#) x) (paths (snd ((xt # xts) ! i)))) 
                      ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        by force

      then have pi2: "set (paths t) = (image ((#) x) (set (paths (snd ((xt # xts) ! i))))) 
                      ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
        by auto


      show ?thesis proof (cases "∃xs'. xs @ xs' ∈ set (paths (snd ((xt # xts) ! i)))")
        case True
        then have pi1': "set (paths (insert (x#xs) t)) = image ((#) x) (set (paths (snd ((xt # xts) ! i))))
                                                         ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
          using pi1 by auto

        have "set (paths (insert (x # xs) t)) = set (paths t)"
          unfolding pi1' pi2 by simp
        moreover have "∃xs'. (x # xs) @ xs' ∈ set (paths t)"
          using True unfolding pi2 by force
        ultimately show ?thesis by simp
      next
        case False
        then have pi1': "set (paths (insert (x#xs) t)) = image ((#) x) (Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs}))
                                                         ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
          using pi1 by auto

        have x1: "((#) x ` Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs}))  
              = Set.insert (x # xs) ((#) x ` set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})" 
        proof -
          have "⋀ a . a ∈ ((#) x ` Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs})) ⟹
                       a ∈ Set.insert (x # xs) ((#) x ` set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})"
            by fastforce
          moreover have "⋀ a . a ∈ Set.insert (x # xs) ((#) x ` set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = x # xs}) ⟹
                                a ∈ ((#) x ` Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs}))"
          proof -
            fix a assume "a ∈ Set.insert (x # xs) ((#) x ` set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})"
            then consider (a) "a = (x#xs)" |
                          (b) "a ∈ ((#) x ` set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})" by blast
            then show "a ∈ ((#) x ` Set.insert xs (set (paths (snd ((xt # xts) ! i))) - {xs'. ∃xs''. xs' @ xs'' = xs}))" 
            proof cases
              case a
              then show ?thesis by blast
            next
              case b
              then show ?thesis by force
            qed 
          qed
          ultimately show ?thesis by blast
        qed

        have x2: "set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))) 
                      = (set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})" 
        and  x3: "¬(∃xs'. (x # xs) @ xs' ∈ set (paths t))"
        proof -
          

          have "⋀ j . j < length (xt#xts) ⟹ j ≠ i ⟹ fst ((xt#xts) ! j) ≠ x"
            using ‹i < length (xt#xts)› ‹fst ((xt#xts) ! i) = x› ‹distinct (map fst (xt#xts))›
            by (metis (no_types, lifting) length_map nth_eq_iff_index_eq nth_map)  

          have "⋀ xt' . xt' ∈ set (take i (xt # xts) @ drop (Suc i) (xt # xts)) ⟹ fst xt' ≠ x"
          proof -
            fix xt' assume "xt' ∈ set (take i (xt # xts) @ drop (Suc i) (xt # xts))"
            then consider (a) "xt' ∈ set (take i (xt # xts))" |
                          (b) "xt' ∈ set (drop (Suc i) (xt # xts))"
              by auto
            then show "fst xt' ≠ x" proof cases
              case a
              then obtain j where "j < length (take i (xt#xts))" "(take i (xt#xts)) ! j = xt'"
                by (meson in_set_conv_nth)
                
              have "j < length (xt#xts)" and "j < i"
                using ‹j < length (take i (xt#xts))› by auto
              moreover have "(xt#xts) ! j = xt'"
                using ‹(take i (xt#xts)) ! j = xt'› ‹j < i› by auto 
              ultimately show ?thesis using ‹⋀ j . j < length (xt#xts) ⟹ j ≠ i ⟹ fst ((xt#xts) ! j) ≠ x› by blast
            next
              case b
              then obtain j where "j < length (drop (Suc i) (xt#xts))" "(drop (Suc i) (xt#xts)) ! j = xt'"
                by (meson in_set_conv_nth)

              have "(Suc i) + j < length (xt#xts)" and "(Suc i) + j > i"
                using ‹j < length (drop (Suc i) (xt#xts))› by auto
              moreover have "(xt#xts) ! ((Suc i) + j) = xt'"
                using ‹(drop (Suc i) (xt#xts)) ! j = xt'›
                using ‹i < length (xt # xts)› by auto  
              ultimately show ?thesis using ‹⋀ j . j < length (xt#xts) ⟹ j ≠ i ⟹ fst ((xt#xts) ! j) ≠ x›[of "(Suc i) + j"] 
                by auto
            qed
          qed
          then show "set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))) 
                      = (set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})" 
            by force

          show "¬(∃xs'. (x # xs) @ xs' ∈ set (paths t))"
          proof 
            assume "∃xs'. (x # xs) @ xs' ∈ set (paths t)"
            then obtain xs' where "(x # (xs @ xs')) ∈ ((#) x ` set (paths (snd ((xt # xts) ! i)))) ∪
                                                          set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))" 
              unfolding pi2 by force
            then consider (a) "(x # (xs @ xs')) ∈ ((#) x ` set (paths (snd ((xt # xts) ! i))))" |
                          (b) "(x # (xs @ xs')) ∈ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))"
              by blast
            then show False proof cases
              case a
              then show ?thesis using False by force
            next
              case b
              then show ?thesis using ‹⋀ xt' . xt' ∈ set (take i (xt # xts) @ drop (Suc i) (xt # xts)) ⟹ fst xt' ≠ x› by force
            qed          
          qed
        qed

        have *: "Set.insert (x # xs) ((#) x ` set (paths (snd ((xt # xts) ! i))) ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts)))) - {xs'. ∃xs''. xs' @ xs'' = x # xs})
                  = Set.insert (x # xs) (((#) x ` set (paths (snd ((xt # xts) ! i)))) - {xs'. ∃xs''. xs' @ xs'' = x # xs}) ∪ set (concat (map (λ(x, t). map ((#) x) (paths t)) (take i (xt # xts) @ drop (Suc i) (xt # xts))))" 
          using x2 by blast
          

        have "set (paths (insert (x # xs) t)) = Set.insert (x # xs) (set (paths t) - {xs'. ∃xs''. xs' @ xs'' = x # xs})"
          unfolding pi1' pi2 x1 * by blast
        then show ?thesis
          using x3 by simp 
      qed
    next
      case False
      have "insert (x#xs) t = MP_Trie (xt # (xts @ [(x, insert xs empty)]))"
        unfolding ‹t = MP_Trie (xt#xts)› insert.simps
        unfolding update_assoc_list_with_default_key_not_found[OF ‹distinct (map fst (xt#xts))› False]
        by simp
      
      have "(paths (MP_Trie (xt # (xts @ [(x, insert xs empty)])))) = concat (map (λ(x, t). map ((#) x) (paths t)) (xt # xts @ [(x, insert xs empty)]))"
        unfolding paths.simps empty_def by simp
      also have "... = (concat (map (λ(x, t). map ((#) x) (paths t)) (xt # xts))) @ (map ((#) x) (paths (insert xs empty))) "
        by auto
      finally have "paths (insert (x#xs) t) = (paths t) @ [x#xs]"
        unfolding ‹insert (x#xs) t = MP_Trie (xt # (xts @ [(x, insert xs empty)]))›
                  ‹(paths t) = concat (map (λ(x, t). map ((#) x) (paths t)) (xt # xts))›[symmetric]
                  paths_insert_empty 
        by auto
      then have "set (paths (insert (x#xs) t)) = Set.insert (x#xs) (set (paths t))"
        by force
        
        
      have "⋀ p . p ∈ set (paths t) ⟹ p ≠ [] ∧ hd p ≠ x"
        using False
        unfolding ‹(paths t) = concat (map (λ(x, t). map ((#) x) (paths t)) (xt # xts))› by force
      then have "⋀ xs' . xs' ∈ set (paths t) ⟹ ¬(∃ xs'' . xs'@xs'' = x#xs)"
        by (metis hd_append2 list.sel(1))
      then have "set (paths t) = (set (paths t) - {xs' . ∃ xs'' . xs'@xs'' = x#xs})"
        by blast
      then show ?thesis 
        unfolding ‹set (paths (insert (x#xs) t)) = Set.insert (x#xs) (set (paths t))›
        using ‹⋀p. p ∈ set (paths t) ⟹ p ≠ [] ∧ hd p ≠ x› by force
    qed
  qed
qed




fun from_list :: "'a list list ⇒ 'a mp_trie" where
  "from_list seqs = foldr insert seqs empty"

lemma from_list_invar : "mp_trie_invar (from_list xs)"
  using empty_invar insert_invar by (induction xs; auto)

lemma from_list_paths :
  "set (paths (from_list (x#xs))) = {y. y ∈ set (x#xs) ∧ ¬(∃ y' . y' ≠ [] ∧ y@y' ∈ set (x#xs))}"
proof (induction xs arbitrary: x)
  case Nil
  have *: "paths (from_list [x]) = paths (insert x empty)" by auto
  
  show ?case 
    unfolding *
    unfolding paths_insert_maximal[OF empty_invar, of "x"]
    unfolding empty_def  
    by (cases x ; auto)
next
  case (Cons x' xs)

  have "from_list (x#x'#xs) = insert x (insert x' (from_list xs))" by auto
  have "from_list (x#x'#xs) = insert x (from_list (x'#xs))" by auto

  have "mp_trie_invar (insert x' (from_list xs))"
    using from_list_invar insert_invar by metis
  have "(insert x' (from_list xs)) = from_list (x'#xs)" by auto


  thm paths_insert_maximal[OF ‹mp_trie_invar (insert x' (from_list xs))›, of x]

  show ?case proof (cases "∃xs'. x @ xs' ∈ set (paths (insert x' (from_list xs)))")
    case True
    then have "set (paths (insert x (insert x' (from_list xs)))) = set (paths (insert x' (from_list xs)))"
      using paths_insert_maximal[OF ‹mp_trie_invar (insert x' (from_list xs))›, of x] by simp
    then have "set (paths (insert x (from_list (x' # xs)))) = set (paths (from_list (x' # xs)))"
      unfolding ‹(insert x' (from_list xs)) = from_list (x'#xs)› 
      by assumption
    then have "set (paths (from_list (x#x'#xs))) = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}"
      unfolding Cons ‹from_list (x#x'#xs) = insert x (from_list (x'#xs))›
      by assumption

    show ?thesis proof (cases "x ∈ set (paths (insert x' (from_list xs)))")
      case True
      then have "x ∈ set (x'#xs)"
        using ‹set (paths (insert x (insert x' (from_list xs)))) = set (paths (insert x' (from_list xs)))› ‹set (paths (from_list (x # x' # xs))) = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› by auto
      then show ?thesis 
        unfolding ‹set (paths (from_list (x#x'#xs))) = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› by auto
    next
      case False
      
      have "{y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} = {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}" 
      proof -
        obtain xs' where "xs' ≠ []" and "x @ xs' ∈  {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}"
          using True False
          by (metis ‹from_list (x # x' # xs) = insert x (insert x' (from_list xs))› ‹set (paths (insert x (insert x' (from_list xs)))) = set (paths (insert x' (from_list xs)))› ‹set (paths (from_list (x # x' # xs))) = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› append_Nil2) 
        then have s1: "{y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)} = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}"
          by auto 
            
        have "⋀ y . (∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)) ⟹ (∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs))"
        proof -
          fix y assume "(∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs))"
          
          show "(∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs))"
          proof 
            assume "∃y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)"
            then have "∃y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs) - set (x' # xs)"
              using ‹(∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs))› by auto
            then have "∃y' . y' ≠ [] ∧ y @ y' = x"
              by auto
            then show "False"
              by (metis (no_types, lifting) Nil_is_append_conv ‹∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)› ‹x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› append.assoc mem_Collect_eq) 
          qed
        qed
        then have s2: "{y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}"
          by auto

        show ?thesis 
          unfolding s1 s2 by simp
      qed
      then show ?thesis
        using ‹set (paths (from_list (x # x' # xs))) = {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› by auto 
    qed
      
  next
    case False
    

    then have *: "set (paths (insert x (insert x' (from_list xs)))) 
                = Set.insert x (set (paths (insert x' (from_list xs))) - {xs'. ∃xs''. xs' @ xs'' = x})"
      using paths_insert_maximal[OF ‹mp_trie_invar (insert x' (from_list xs))›, of x] by simp

    have f: "∄xs'. x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}"
      using False
      unfolding ‹(insert x' (from_list xs)) = from_list (x'#xs)› Cons
      by assumption
    then have "x ∉ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}"
      by (metis (no_types, lifting) append_Nil2)

    have "x ∉ set (x' # xs)"
    proof
      assume "x ∈ set (x' # xs)"
      then have "∃y'. y' ≠ [] ∧ x @ y' ∈ set (x' # xs)"
        using ‹x ∉ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}› by auto

      let ?xms = "{xs' . xs' ≠ [] ∧ x @ xs' ∈ set (x' # xs)}"
      have "?xms ≠ {}"
        using ‹∃y'. y' ≠ [] ∧ x @ y' ∈ set (x' # xs)›
        by simp 
      moreover have "finite ?xms"
      proof -
        have "?xms ⊆ image (drop (length x)) (set (x'#xs))" by force
        then show ?thesis by (meson List.finite_set finite_surj) 
      qed
      ultimately have "∃ xs' ∈ ?xms . ∀ xs'' ∈ ?xms . length xs'' ≤ length xs'"
        by (meson max_length_elem not_le_imp_less) 
      then obtain xs' where "xs' ≠ []"
                      and   "x@xs' ∈ set (x'#xs)"
                      and   "⋀ xs'' . xs'' ≠ [] ⟹ x@xs'' ∈ set (x'#xs) ⟹ length xs'' ≤ length xs'"
        by blast
      
      have "∄y'. y' ≠ [] ∧ (x@xs') @ y' ∈ set (x' # xs)"
      proof 
        assume "∃y'. y' ≠ [] ∧ (x @ xs') @ y' ∈ set (x' # xs)"
        then obtain xs'' where "xs'' ≠ []" and "(x @ xs') @ xs'' ∈ set (x' # xs)"
          by blast
        then have "xs'@xs'' ≠ []" and "x @ (xs' @ xs'') ∈ set (x' # xs)"
          by auto
        then have "length (xs'@xs'') ≤ length xs'"
          using ‹⋀ xs'' . xs'' ≠ [] ⟹ x@xs'' ∈ set (x'#xs) ⟹ length xs'' ≤ length xs'› by blast
        then show "False"
          using ‹xs'' ≠ []› by auto
      qed
        
      then have "x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}" 
        using ‹x@xs' ∈ set (x'#xs)› by blast
      then show "False" using ‹∄xs'. x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}›
        by blast
    qed
    
    have "∄y'. y' ≠ [] ∧ x @ y' ∈ set (x # x' # xs)"
    proof 
      assume "∃y'. y' ≠ [] ∧ x @ y' ∈ set (x # x' # xs)"
      then obtain y' where "y' ≠ []" and "x@y' ∈ set (x#x'#xs)"
        by blast
      then have "x@y' ∈ set (x'#xs)"
        by auto

      let ?xms = "{xs' . xs' ≠ [] ∧ x @ xs' ∈ set (x # x' # xs)}"
      have "?xms ≠ {}"
        using ‹∃y'. y' ≠ [] ∧ x @ y' ∈ set (x # x' # xs)›
        by simp 
      moreover have "finite ?xms"
      proof -
        have "?xms ⊆ image (drop (length x)) (set (x'#xs))" by force
        then show ?thesis by (meson List.finite_set finite_surj) 
      qed
      ultimately have "∃ xs' ∈ ?xms . ∀ xs'' ∈ ?xms . length xs'' ≤ length xs'"
        by (meson max_length_elem not_le_imp_less) 
      then obtain xs' where "xs' ≠ []"
                      and   "x@xs' ∈ set (x#x'#xs)"
                      and   "⋀ xs'' . xs'' ≠ [] ⟹ x@xs'' ∈ set (x#x'#xs) ⟹ length xs'' ≤ length xs'"
        by blast
      


      have "∄y'. y' ≠ [] ∧ (x@xs') @ y' ∈ set (x # x' # xs)"
      proof 
        assume "∃y'. y' ≠ [] ∧ (x @ xs') @ y' ∈ set (x # x' # xs)"
        then obtain xs'' where "xs'' ≠ []" and "(x @ xs') @ xs'' ∈ set (x # x' # xs)"
          by blast
        then have "xs'@xs'' ≠ []" and "x @ (xs' @ xs'') ∈ set (x # x' # xs)"
          by auto
        then have "length (xs'@xs'') ≤ length xs'"
          using ‹⋀ xs'' . xs'' ≠ [] ⟹ x@xs'' ∈ set (x#x'#xs) ⟹ length xs'' ≤ length xs'› by blast
        then show "False"
          using ‹xs'' ≠ []› by auto
      qed
        
      then have "x @ xs' ∈ {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}" 
        using ‹x@xs' ∈ set (x # x'#xs)› by blast
      then have "x @ xs' ∈ set (x' # xs)" and "∄y'. y' ≠ [] ∧ (x@xs') @ y' ∈ set (x' # xs)"
        using ‹xs' ≠ []› by auto
      then have "x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}" 
        by blast
      then show "False" using ‹∄xs'. x @ xs' ∈ {y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)}›
        by blast
    qed


    have "Set.insert x ({y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} - {xs'. ∃xs''. xs' @ xs'' = x})
              = {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}" 
    proof -
      have "⋀ y . y ∈ Set.insert x ({y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} - {xs'. ∃xs''. xs' @ xs'' = x}) ⟹ y ∈ {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}"
      proof -
        fix y assume "y ∈ Set.insert x ({y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} - {xs'. ∃xs''. xs' @ xs'' = x})"
        then consider (a) "y = x" |
                      (b) "y ∈ ({y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} - {xs'. ∃xs''. xs' @ xs'' = x})"
          by blast
        then show "y ∈ {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)}"
        proof cases
          case a
          show ?thesis
            using ‹∄y'. y' ≠ [] ∧ x @ y' ∈ set (x # x' # xs)› unfolding a by auto
        next
          case b
          then have "y ∈ set (x' # xs)" and "∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)" and "¬(∃xs''. y @ xs'' = x)"
            by blast+

          have "y ∈ set (x#x'#xs)"
            using ‹y ∈ set (x' # xs)› by auto
          moreover have "∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)"
            using ‹∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)› ‹¬(∃xs''. y @ xs'' = x)›
            by auto 
          ultimately show ?thesis by blast
        qed
      qed

      moreover have "⋀ y .y ∈ {y ∈ set (x # x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x # x' # xs)} ⟹  y ∈ Set.insert x ({y ∈ set (x' # xs). ∄y'. y' ≠ [] ∧ y @ y' ∈ set (x' # xs)} - {xs'. ∃xs''. xs' @ xs'' = x})"
        by auto
      ultimately show ?thesis by blast
    qed
    then show ?thesis
      using "*" Cons.IH by auto 
  qed
qed



subsubsection ‹New Code Generation for @{text "remove_proper_prefixes"}›

declare [[code drop: remove_proper_prefixes]]

lemma remove_proper_prefixes_code_trie[code] :
  "remove_proper_prefixes (set xs) = (case xs of [] ⇒ {} | (x#xs') ⇒ set (paths (from_list (x#xs'))))"
  unfolding from_list_paths remove_proper_prefixes_def by (cases xs; auto)


end