# 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)"

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 = [[]]"
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 ```