# Theory Prefix_Tree

section ‹Prefix Tree›

text ‹This theory introduces a tree to efficiently store prefix-complete sets of lists.
Several functions to lookup or merge subtrees are provided.›

theory Prefix_Tree
imports Util
begin

datatype 'a prefix_tree = PT "'a  'a prefix_tree"

definition empty :: "'a prefix_tree" where
"empty = PT Map.empty"

fun isin :: "'a prefix_tree  'a list  bool" where
"isin t [] = True" |
"isin (PT m) (x # xs) = (case m x of None  False | Some t  isin t xs)"

lemma isin_prefix :
assumes "isin t (xs@xs')"
shows "isin t xs"
proof -
obtain m where "t = PT m"
by (metis prefix_tree.exhaust)

show ?thesis using assms unfolding t = PT m
proof (induction xs arbitrary: m)
case Nil
then show ?case by auto
next
case (Cons x xs)
then have "isin (PT m) (x # (xs @ xs'))"
by auto
then obtain m' where "m x = Some (PT m')"
and "isin (PT m') (xs@xs')"
unfolding isin.simps
by (metis option.exhaust option.simps(4) option.simps(5) prefix_tree.exhaust)
then show ?case
using Cons.IH[of m'] by auto
qed
qed

fun set :: "'a prefix_tree  'a list set" where
"set t = {xs . isin t xs}"

lemma set_empty : "set empty = ({[]} :: 'a list set)"
proof
show "set empty  ({[]} :: 'a list set)"
proof
fix xs :: "'a list"
assume "xs  set empty"
then have "isin empty xs"
by auto

have "xs = []"
proof (rule ccontr)
assume "xs  []"
then obtain x xs' where "xs = x#xs'"
using list.exhaust by auto
then have
using isin empty xs unfolding empty_def
by simp
then show "False"
by auto
qed
then show "xs  {[]}"
by blast
qed
show "({[]} :: 'a list set)  set empty"
unfolding set.simps empty_def
by simp
qed

lemma set_Nil : "[]  set t"
by auto

fun insert :: "'a prefix_tree  'a list  'a prefix_tree" where
"insert t [] = t" |
"insert (PT m) (x#xs) = PT (m(x  insert (case m x of None  empty | Some t'  t') xs))"

lemma insert_isin_prefix : "isin (insert t (xs@xs')) xs"
proof (induction xs arbitrary: t)
case Nil
then show ?case by auto
next
case (Cons x xs)
moreover obtain m where "t = PT m"
using prefix_tree.exhaust by auto
ultimately obtain t' where "(m(x  insert (case m x of None  empty | Some t'  t') xs)) x = Some t'"
by simp
then have "isin (insert t ((x#xs)@xs')) (x#xs) = isin (insert (case m x of None  empty | Some t'  t') (xs@xs')) xs"
unfolding t = PT m
by simp
then show ?case
using Cons.IH by auto
qed

lemma insert_isin_other :
assumes "isin t xs"
shows "isin (insert t xs') xs"
proof (cases "xs = xs'")
case True
then show ?thesis using insert_isin_prefix[of t xs "[]"] by simp
next
case False

have *: " i xs xs' . take i xs = take i xs'  take (Suc i) xs  take (Suc i) xs'  isin t xs  isin (insert t xs') xs"
proof -
fix i xs xs' assume "take i xs = take i xs'"
and "take (Suc i) xs  take (Suc i) xs'"
and "isin t xs"
then show "isin (insert t xs') xs"
proof (induction i arbitrary: xs xs' t)
case 0
then consider (a) "xs = []  xs'  []" |
(b) "xs' = []  xs  []" |
(c) "xs  []  xs'  []  hd xs  hd xs'"
by (metis take_Suc take_eq_Nil)
then show ?case proof cases
case a
then show ?thesis by auto
next
case b
then show ?thesis
next
case c
then obtain b bs c cs where "xs = b#bs" and "xs' = c#cs" and "b  c"
using list.exhaust_sel by blast
obtain m where "t = PT m"
using prefix_tree.exhaust by auto
have "isin (Prefix_Tree.insert t xs') xs = isin t xs"
unfolding t = PT m xs = b#bs xs' = c#cs insert.simps isin.simps using b  c
by simp
then show ?thesis
using isin t xs by simp
qed
next
case (Suc i)

define hxs where hxs: "hxs = hd xs"
define txs where txs: "txs = tl xs"
define txs' where txs': "txs' = tl xs'"

have "xs = hxs#txs"
unfolding hxs txs
using take (Suc i) xs = take (Suc i) xs' take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis Zero_not_Suc hd_Cons_tl take_eq_Nil)
moreover have "xs' = hxs#txs'"
unfolding hxs txs txs'
using take (Suc i) xs = take (Suc i) xs' take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis hd_Cons_tl hd_take take_Nil take_Suc_Cons take_tl zero_less_Suc)
ultimately have "take (Suc i) txs  take (Suc i) txs'"
using take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis take_Suc_Cons)
moreover have "take i txs = take i txs'"
using take (Suc i) xs = take (Suc i) xs' unfolding txs txs'
ultimately have " t . isin t txs  isin (Prefix_Tree.insert t txs') txs"
using Suc.IH by blast

obtain m where "t = PT m"
using prefix_tree.exhaust by auto

obtain t' where "m hxs = Some t'"
and "isin t' txs"
using case_optionE by (metis Suc.prems(3) t = PT m xs = hxs # txs isin.simps(2))

have "isin (Prefix_Tree.insert t xs') xs = isin (Prefix_Tree.insert t' txs') txs"
using m hxs = Some t' unfolding t = PT m xs = hxs#txs xs' = hxs#txs' by auto
then show ?case
using  t . isin t txs  isin (Prefix_Tree.insert t txs') txs isin t' txs
by simp
qed
qed

show ?thesis
using different_lists_shared_prefix[OF False] *[OF _ _ assms] by blast
qed

lemma insert_isin_rev :
assumes "isin (insert t xs') xs"
shows "isin t xs  ( xs'' . xs' = xs@xs'')"
proof (cases "xs = xs'")
case True
then show ?thesis using insert_isin_prefix[of t xs "[]"] by simp
next
case False

have *: " i xs xs' . take i xs = take i xs'  take (Suc i) xs  take (Suc i) xs'  isin (insert t xs') xs  isin t xs  ( xs'' . xs' = xs@xs'')"
proof -
fix i xs xs' assume "take i xs = take i xs'"
and "take (Suc i) xs  take (Suc i) xs'"
and "isin (insert t xs') xs"
then show "isin t xs  ( xs'' . xs' = xs@xs'')"
proof (induction i arbitrary: xs xs' t)
case 0
then consider (a) "xs = []  xs'  []" |
(b) "xs' = []  xs  []" |
(c) "xs  []  xs'  []  hd xs  hd xs'"
by (metis take_Suc take_eq_Nil)
then show ?case proof cases
case a
then show ?thesis
by (metis isin.simps(1) )
next
case b
then show ?thesis
using "0.prems"(3) by auto
next
case c
then obtain b bs c cs where "xs = b#bs" and "xs' = c#cs" and "b  c"
using list.exhaust_sel by blast
obtain m where "t = PT m"
using prefix_tree.exhaust by auto
have "isin (Prefix_Tree.insert t xs') xs = isin t xs"
unfolding t = PT m xs = b#bs xs' = c#cs insert.simps isin.simps using b  c
by simp
then show ?thesis
using isin (insert t xs') xs by simp
qed
next
case (Suc i)

define hxs where hxs: "hxs = hd xs"
define txs where txs: "txs = tl xs"
define txs' where txs': "txs' = tl xs'"

have "xs = hxs#txs"
unfolding hxs txs
using take (Suc i) xs = take (Suc i) xs' take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis Zero_not_Suc hd_Cons_tl take_eq_Nil)
moreover have "xs' = hxs#txs'"
unfolding hxs txs txs'
using take (Suc i) xs = take (Suc i) xs' take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis hd_Cons_tl hd_take take_Nil take_Suc_Cons take_tl zero_less_Suc)
ultimately have "take (Suc i) txs  take (Suc i) txs'"
using take (Suc (Suc i)) xs  take (Suc (Suc i)) xs'
by (metis take_Suc_Cons)
moreover have "take i txs = take i txs'"
using take (Suc i) xs = take (Suc i) xs' unfolding txs txs'
ultimately have " t . isin (Prefix_Tree.insert t txs') txs  isin t txs  (xs''. txs' = txs @ xs'')"
using Suc.IH by blast

obtain m where "t = PT m"
using prefix_tree.exhaust by auto

obtain t' where "(m(hxs  insert (case m hxs of None  empty | Some t'  t') txs')) hxs = Some t'"
and "isin t' txs"
using case_optionE isin (Prefix_Tree.insert t xs') xs
unfolding t = PT m xs = hxs#txs xs' = hxs#txs' insert.simps isin.simps by blast
then have "t' = insert (case m hxs of None  empty | Some t'  t') txs'"
by auto
then have *: "isin (case m hxs of None  empty | Some t'  t') txs  (xs''. txs' = txs @ xs'')"
using  t . isin (Prefix_Tree.insert t txs') txs  isin t txs  (xs''. txs' = txs @ xs'')
isin t' txs
by auto

show ?case proof (cases "m hxs")
case None
then have "isin empty txs  (xs''. txs' = txs @ xs'')"
using * by auto
then have "txs = []  (xs''. txs' = txs @ xs'')"
by (metis Prefix_Tree.empty_def case_optionE isin.elims(2) option.discI prefix_tree.inject)
then have "(xs''. txs' = txs @ xs'')"
by auto
then show ?thesis
unfolding xs = hxs#txs xs' = hxs#txs' by auto
next
case (Some t'')
then consider "isin t'' txs" | "(xs''. txs' = txs @ xs'')"
using * by auto
then show ?thesis proof cases
case 1
moreover have "isin t xs = isin t'' txs"
unfolding t = PT m xs = hxs#txs xs' = hxs#txs' using Some by auto
ultimately show ?thesis by simp
next
case 2
then show ?thesis
unfolding xs = hxs#txs xs' = hxs#txs' by auto
qed
qed
qed
qed

show ?thesis
using different_lists_shared_prefix[OF False] *[OF _ _ assms] by blast
qed

lemma insert_set : "set (insert t xs) = set t  {xs' .  xs'' . xs = xs'@xs''}"
proof -
have "set t  set (insert t xs)"
using insert_isin_other by auto
moreover have "{xs' .  xs'' . xs = xs'@xs''}  set (insert t xs)"
using insert_isin_prefix
by auto
moreover have "set (insert t xs)  set t  {xs' .  xs'' . xs = xs'@xs''}"
using insert_isin_rev[of t xs] unfolding set.simps by blast
ultimately show ?thesis
by blast
qed

lemma insert_isin : "xs  set (insert t xs)"
unfolding insert_set by auto

lemma set_prefix :
assumes "xs@ys  set T"
shows "xs  set T"
using assms isin_prefix by auto

fun after :: "'a prefix_tree  'a list  'a prefix_tree" where
"after t [] = t" |
"after (PT m) (x # xs) = (case m x of None  empty | Some t  after t xs)"

lemma after_set : "set (after t xs) = Set.insert [] {xs' . xs@xs'  set t}"
(is "?A t xs = ?B t xs")
proof
show "?A t xs  ?B t xs"
proof
fix xs' assume "xs'  ?A t xs"
then show "xs'  ?B t xs"
proof (induction xs arbitrary: t)
case Nil
then show ?case by auto
next
case (Cons x xs)
obtain m where "t = PT m"
using prefix_tree.exhaust by auto
show ?case proof (cases "m x")
case None
then have "after t (x#xs) = empty"
unfolding t = PT m by auto
then have "xs' = []"
using Cons.prems set_empty by auto
then show ?thesis by blast
next
case (Some t')
then have "after t (x#xs) = after t' xs"
unfolding t = PT m by auto
then have "xs'  set (after t' xs)"
using Cons.prems by simp
then have "xs'  ?B t' xs"
using Cons.IH by auto

show ?thesis proof (cases "xs' = []")
case True
then show ?thesis by auto
next
case False
then have "isin t' (xs@xs')"
using xs'  ?B t' xs by auto
then have "isin t (x#(xs@xs'))"
unfolding t = PT m using Some by auto
then show ?thesis by auto
qed
qed
qed
qed

show "?B t xs  ?A t xs"
proof
fix xs' assume "xs'  ?B t xs"
then show "xs'  ?A t xs"
proof (induction xs arbitrary: t)
case Nil
then show ?case by (cases xs'; auto)
next
case (Cons x xs)
obtain m where "t = PT m"
using prefix_tree.exhaust by auto

show ?case proof (cases "xs' = []")
case True
then show ?thesis by (cases xs'; auto)
next
case False
then have "x # (xs @ xs')  set t"
using Cons.prems by auto
then have "isin t (x # (xs @ xs'))"
by auto
then obtain t' where "m x = Some t'"
and "isin t' (xs@xs')"
unfolding t = PT m
by (metis case_optionE isin.simps(2))
then have "xs'  ?B t' xs"
by auto
then have "xs'  ?A t' xs"
using Cons.IH by blast
moreover have "after t (x#xs) = after t' xs"
using m x = Some t' unfolding t = PT m by auto
ultimately show ?thesis
by simp
qed
qed
qed
qed

lemma after_set_Cons :
assumes "γ  set (after T α)"
and     "γ  []"
shows "α  set T"
using assms unfolding after_set
by (metis insertE isin_prefix mem_Collect_eq set.simps)

function (domintros) combine :: "'a prefix_tree  'a prefix_tree  'a prefix_tree" where
"combine (PT m1) (PT m2) = (PT (λ x . case m1 x of
None  m2 x |
Some t1  (case m2 x of
None  Some t1 |
Some t2  Some (combine t1 t2))))"
by pat_completeness auto
termination
proof -
{
fix a b :: "'a prefix_tree"

have "combine_dom (a,b)"
proof (induction a arbitrary: b)
case (PT m1)

obtain m2 where "b = PT m2"
by (metis prefix_tree.exhaust)

have "(x a' b'. m1 x = Some a'  m2 x = Some b'  combine_dom (a', b'))"
proof -
fix x a' b' assume "m1 x = Some a'" and "m2 x = Some b'"

have "Some a'  range m1"
by (metis m1 x = Some a' range_eqI)

show "combine_dom (a', b')"
using PT(1)[OF Some a'  range m1, of a']
by simp
qed

then show ?case
using combine.domintros unfolding b = PT m2 by blast
qed
} note t = this

then show ?thesis by auto
qed

lemma combine_alt_def :
"combine (PT m1) (PT m2) = PT (λx . combine_options combine (m1 x) (m2 x))"
unfolding combine.simps

lemma combine_set :
"set (combine t1 t2) = set t1  set t2"
proof

show "set (combine t1 t2)  set t1  set t2"
proof
fix xs assume "xs  set (combine t1 t2)"
then show "xs  set t1  set t2"
proof (induction xs arbitrary: t1 t2)
case Nil
show ?case
using set_Nil by auto
next
case (Cons x xs)

obtain m1 m2 where "t1 = PT m1" and "t2 = PT m2"
by (meson prefix_tree.exhaust)

obtain t' where "combine_options combine (m1 x) (m2 x) = Some t'"
and "isin t' xs"
using Cons.prems unfolding t1 = PT m1 t2 = PT m2 combine_alt_def set.simps
by (metis (no_types, lifting) case_optionE isin.simps(2) mem_Collect_eq)

show ?case proof (cases "m1 x")
case None
show ?thesis proof (cases "m2 x")
case None
then have False
using m1 x = None combine_options combine (m1 x) (m2 x) = Some t'
by simp
then show ?thesis
by simp
next
case (Some t'')
then have "m2 x = Some t'"
using m1 x = None combine_options combine (m1 x) (m2 x) = Some t'
by simp
then have "isin t2 (x#xs)"
using isin t' xs unfolding t2 = PT m2 by auto
then show ?thesis
by simp
qed
next
case (Some t1')
show ?thesis proof (cases "m2 x")
case None
then have "m1 x = Some t'"
using m1 x = Some t1' combine_options combine (m1 x) (m2 x) = Some t'
by simp
then have "isin t1 (x#xs)"
using isin t' xs unfolding t1 = PT m1 by auto
then show ?thesis
by simp
next
case (Some t2')
then have "t' = combine t1' t2'"
using m1 x = Some t1' combine_options combine (m1 x) (m2 x) = Some t'
by simp
then have "xs  Prefix_Tree.set (combine t1' t2')"
using isin t' xs
by simp
then have "xs  Prefix_Tree.set t1'  Prefix_Tree.set t2'"
using Cons.IH by blast
then have "isin t1' xs  isin t2' xs"
by simp
then have "isin t1 (x#xs)  isin t2 (x#xs)"
using m1 x = Some t1' m2 x = Some t2' unfolding t1 = PT m1 t2 = PT m2 by auto
then show ?thesis
by simp
qed
qed
qed
qed

show "(set t1  set t2)  set (combine t1 t2)"
proof -
have "set t1  set (combine t1 t2)"
proof
fix xs assume "xs  set t1"
then have "isin t1 xs"
by auto
then show "xs  set (combine t1 t2)"
proof (induction xs arbitrary: t1 t2)
case Nil
then show ?case using set_Nil by auto
next
case (Cons x xs)

obtain m1 m2 where "t1 = PT m1" and "t2 = PT m2"
by (meson prefix_tree.exhaust)

obtain t1' where "m1 x = Some t1'"
and "isin t1' xs"
using Cons.prems unfolding t1 = PT m1 isin.simps
using case_optionE by blast

show ?case proof (cases "m2 x")
case None
then have "combine_options combine (m1 x) (m2 x) = Some t1'"
by (simp add: m1 x = Some t1')
then have "isin (combine t1 t2) (x#xs)"
using combine_alt_def
by (metis (no_types, lifting) Cons.prems m1 x = Some t1' t1 = PT m1 t2 = PT m2 isin.simps(2))
then show ?thesis
by simp
next
case (Some t2')
then have "combine_options combine (m1 x) (m2 x) = Some (combine t1' t2')"
by (simp add: m1 x = Some t1')
moreover have "isin (combine t1' t2') xs"
using Cons.IH[OF isin t1' xs]
by simp
ultimately have "isin (combine t1 t2) (x#xs)"
unfolding t1 = PT m1 t2 = PT m2 using isin.simps(2)[of _ x xs]
by (metis (no_types, lifting) combine_alt_def option.simps(5))
then show ?thesis by simp
qed
qed
qed
moreover have "set t2  set (combine t1 t2)"
proof
fix xs assume "xs  set t2"
then have "isin t2 xs"
by auto
then show "xs  set (combine t1 t2)"
proof (induction xs arbitrary: t1 t2)
case Nil
then show ?case using set_Nil by auto
next
case (Cons x xs)

obtain m1 m2 where "t1 = PT m1" and "t2 = PT m2"
by (meson prefix_tree.exhaust)

obtain t2' where "m2 x = Some t2'"
and "isin t2' xs"
using Cons.prems unfolding t2 = PT m2 isin.simps
using case_optionE by blast

show ?case proof (cases "m1 x")
case None
then have "combine_options combine (m1 x) (m2 x) = Some t2'"
by (simp add: m2 x = Some t2')
then have "isin (combine t1 t2) (x#xs)"
using combine_alt_def
by (metis (no_types, lifting) Cons.prems m2 x = Some t2' t1 = PT m1 t2 = PT m2 isin.simps(2))
then show ?thesis
by simp
next
case (Some t1')
then have "combine_options combine (m1 x) (m2 x) = Some (combine t1' t2')"
by (simp add: m2 x = Some t2')
moreover have "isin (combine t1' t2') xs"
using Cons.IH[OF isin t2' xs]
by simp
ultimately have "isin (combine t1 t2) (x#xs)"
unfolding t1 = PT m1 t2 = PT m2 using isin.simps(2)[of _ x xs]
by (metis (no_types, lifting) combine_alt_def option.simps(5))
then show ?thesis by simp
qed
qed
qed
ultimately show ?thesis
by blast
qed
qed

fun combine_after :: "'a prefix_tree  'a list  'a prefix_tree  'a prefix_tree" where
"combine_after t1 [] t2 = combine t1 t2" |
"combine_after (PT m) (x#xs) t2 = PT (m(x  combine_after (case m x of None  empty | Some t'  t') xs t2))"

lemma combine_after_set : "set (combine_after t1 xs t2) = set t1  {xs' .  xs'' . xs = xs'@xs''}  {xs@xs' | xs' . xs'  set t2}"
proof
show "set (combine_after t1 xs t2)  set t1  {xs' .  xs'' . xs = xs'@xs''}  {xs@xs' | xs' . xs'  set t2}"
proof
fix ys assume "ys  set (combine_after t1 xs t2)"
then show "ys  set t1  {xs' .  xs'' . xs = xs'@xs''}  {xs@xs' | xs' . xs'  set t2}"
proof (induction ys arbitrary: xs t1)
case Nil
show ?case using set_Nil by auto
next
case (Cons y ys)

obtain m1 where "t1 = PT m1"
by (meson prefix_tree.exhaust)

show ?case proof (cases xs)
case Nil
then show ?thesis using combine_set Cons.prems by auto
next
case (Cons x xs')

show ?thesis proof (cases "x = y")
case True
then have "isin (combine_after t1 (x#xs') t2) (x#ys)"
using Cons Cons.prems by auto
then have "isin (combine_after (case m1 x of None  empty | Some t'  t') xs' t2) ys"
unfolding t1 = PT m1 by auto
then consider "ys  set (case m1 x of None  empty | Some t'  t')" | "ys  {xs'' .  xs''' . xs' = xs''@xs'''}" | "ys  {xs' @ xs'' |xs''. xs''  set t2}"
using Cons.IH by auto
then show ?thesis proof cases
case 1
then show ?thesis proof (cases "m1 x")
case None
then have "ys = []"
using 1 set_empty by auto
then show ?thesis unfolding True Cons by auto
next
case (Some t')
then have "isin t' ys"
using 1 by auto
then have "y # ys  Prefix_Tree.set (PT m1)"
using Some by (simp add: True)
then show ?thesis unfolding t1 = PT m1 by auto
qed
next
case 2
then show ?thesis unfolding True t1 = PT m1 Cons by auto
next
case 3
then show ?thesis unfolding True t1 = PT m1 Cons by auto
qed
next
case False
then have "(m1(x  combine_after (case m1 x of None  empty | Some t'  t') xs' t2)) y = m1 y"
by auto
then have "isin t1 (y#ys)"
using Cons Cons.prems unfolding t1 = PT m1
by simp
then show ?thesis by auto
qed
qed
qed
qed

show "set t1  {xs' .  xs'' . xs = xs'@xs''}  {xs@xs' | xs' . xs'  set t2}  set (combine_after t1 xs t2)"
proof -
have "set t1  set (combine_after t1 xs t2)"
proof
fix ys assume "ys  set t1"
then show "ys  set (combine_after t1 xs t2)"
proof (induction ys arbitrary: t1 xs)
case Nil
then show ?case using set_Nil by auto
next
case (Cons y ys)
then have "isin t1 (y#ys)"
by auto

show ?case proof (cases "xs")
case Nil
then show ?thesis using Cons.prems combine_set by auto
next
case (Cons x xs')

obtain m1 where "t1 = PT m1"
by (meson prefix_tree.exhaust)
obtain t' where "m1 y = Some t'"
and "isin t' ys"
using isin t1 (y#ys) unfolding t1 = PT m1 isin.simps
using case_optionE by blast
then have "ys  set t'"
by auto
then have "isin (combine_after t' xs' t2) ys"
using Cons.IH by auto

show ?thesis proof (cases "x=y")
case True
show ?thesis
using isin (combine_after t' xs' t2) ys m1 y = Some t'
unfolding Cons True t1 = PT m1 by auto
next
case False
then have "isin (combine_after (PT m1) (x # xs') t2) (y#ys) = isin (PT m1) (y#ys)"
unfolding combine_after.simps by auto
then show ?thesis
using y # ys  Prefix_Tree.set t1
unfolding Cons t1 = PT m1
by auto
qed
qed
qed
qed
moreover have "{xs' .  xs'' . xs = xs'@xs''}  {xs@xs' | xs' . xs'  set t2}  set (combine_after t1 xs t2)"
proof -
have "{xs@xs' | xs' . xs'  set t2}  set (combine_after t1 xs t2)  {xs' .  xs'' . xs = xs'@xs''}  set (combine_after t1 xs t2)"
proof
fix ys assume *:"{xs@xs' | xs' . xs'  set t2}  set (combine_after t1 xs t2)"
and "ys  {xs' .  xs'' . xs = xs'@xs''}"
then obtain xs' where "xs = ys@xs'"
by blast
then have **: "isin (combine_after t1 xs t2) (ys@xs')"
using * set_Nil[of t2] by force
show "ys  set (combine_after t1 xs t2)"
using  isin_prefix[OF **] by auto
qed
moreover have "{xs@xs' | xs' . xs'  set t2}  set (combine_after t1 xs t2)"
proof
fix ys assume "ys  {xs@xs' | xs' . xs'  set t2}"
then obtain xs' where "ys = xs@xs'" and "xs'  set t2"
by auto

show "ys  set (combine_after t1 xs t2)"
unfolding ys = xs@xs'
proof (induction xs arbitrary: t1)
case Nil
then show ?case using combine_set xs'  set t2 by auto
next
case (Cons x xs)

obtain m1 where "t1 = PT m1"
by (meson prefix_tree.exhaust)

have "isin (combine_after t1 (x # xs) t2) ((x # xs) @ xs') = isin (combine_after (case m1 x of None  empty | Some t'  t') xs t2) (xs @ xs')"
unfolding t1 = PT m1 by auto
then have *:"(x # xs) @ xs'  Prefix_Tree.set (combine_after t1 (x # xs) t2) = isin (combine_after (case m1 x of None  empty | Some t'  t') xs t2) (xs @ xs')"
by auto

show ?case
using xs'  set t2 Cons
unfolding *
by (cases "m1 x"; simp)
qed
qed
ultimately show ?thesis
by blast
qed
ultimately show ?thesis
by blast
qed
qed

fun from_list :: "'a list list  'a prefix_tree" where
"from_list xs = foldr (λ x t . insert t x) xs empty"

lemma from_list_set : "set (from_list xs) = Set.insert [] {xs'' .  xs' xs''' . xs'  list.set xs  xs' = xs''@xs'''}"
proof (induction xs)
case Nil
have
by auto
then have "set (from_list []) = {[]}"
using set_empty by auto
moreover have "Set.insert [] {xs'' .  xs' xs''' . xs'  list.set []  xs' = xs''@xs'''} = {[]}"
by auto
ultimately show ?case
by blast
next
case (Cons x xs)

have "from_list (x#xs) = insert (from_list xs) x"
by auto
then have "set (from_list (x#xs)) = set (from_list xs)  {xs'. xs''. x = xs' @ xs''}"
using insert_set by auto
then show ?case
unfolding Cons by force
qed

lemma from_list_subset : "list.set xs  set (from_list xs)"
unfolding from_list_set by auto

lemma from_list_set_elem :
assumes "x  list.set xs"
shows "x  set (from_list xs)"
using assms unfolding from_list_set by force

function (domintros) finite_tree :: "'a prefix_tree  bool" where
"finite_tree (PT m) = (finite (dom m)  ( t  ran m . finite_tree t))"
by pat_completeness auto
termination
proof -
{ fix a :: "'a prefix_tree"

have
proof (induction a)
case (PT m)

have "(x. x  ran m  finite_tree_dom x)"
proof -
fix x :: "'a prefix_tree"
assume "x  ran m"
then have "a. m a = Some x"
then show
using PT.IH by blast
qed
then show ?case
using finite_tree.domintros
by blast
qed
}
then show ?thesis by auto
qed

lemma combine_after_after_subset :
"set T2  set (after (combine_after T1 xs T2) xs)"
unfolding combine_after_set after_set
by auto

lemma subset_after_subset :
"set T2  set T1  set (after T2 xs)  set (after T1 xs)"
unfolding after_set by auto

lemma set_alt_def :
"set (PT m) = Set.insert [] ( x  dom m . (Cons x) ` (set (the (m x))))"
(is "?A m = ?B m")
proof
show "?A m  ?B m"
proof
fix xs assume "xs  ?A m"
then have "isin (PT m) xs"
by auto
then show "xs  ?B m"
proof (induction xs arbitrary: m)
case Nil
then show ?case by auto
next
case (Cons x xs)
then obtain t where "m x = Some t"
and "isin t xs"
by (metis (no_types, lifting) case_optionE isin.simps(2))

obtain m' where "t = PT m'"
using prefix_tree.exhaust by blast
then have "xs  ?B m'"
using isin t xs Cons.IH by blast
moreover have "x  dom m"
using m x = Some t
by auto
ultimately show ?case
using m x = Some t
using isin t xs t = PT m'
by fastforce
qed
qed

show "?B m  ?A m"
proof
fix xs assume "xs  ?B m"
then show "xs  ?A m"
proof (induction xs arbitrary: m)
case Nil
show ?case
by auto
next
case (Cons x xs)
then have "x#xs  ( x  dom m . (Cons x) ` (set (the (m x))))"
by auto
then have "x  dom m"
and "xs  (set (the (m x)))"
by auto
then obtain t where "m x = Some t" and "isin t xs"
unfolding keys_is_none_rep
by auto
then show ?case
by auto
qed
qed
qed

lemma finite_tree_iff :
"finite_tree t = finite (set t)"
(is "?P1 = ?P2")
proof
show "?P1  ?P2"
proof induction
case (PT m)

have "set (PT m) = Set.insert [] (xdom m. (#) x ` set (the (m x)))"
unfolding set_alt_def by simp
moreover have "finite (dom m)"
using PT.prems by auto
moreover have " x . x  dom m  finite ((#) x ` set (the (m x)))"
proof -
fix x assume "x  dom m"
then obtain y where "m x = Some y"
by auto
then have "y  ran m"
by (meson ranI)
then have "finite_tree y"
using PT.prems by auto
then have "finite (set y)"
using PT.IH[of "Some y" y] m x = Some y
by (metis option.set_intros rangeI)
moreover have "(the (m x)) = y"
using m x = Some y by auto
ultimately show "finite ((#) x ` set (the (m x)))"
by blast
qed
ultimately show ?case
by simp
qed

show "?P2  ?P1"
proof (induction t)
case (PT m)

have "finite (dom m)"
proof -
have " x . x  dom m  [x]  set (PT m)"
using image_eqI by auto
then have "(λx . [x]) ` dom m  set (PT m)"
by auto
have "inj (λx . [x])"
by (meson inj_onI list.inject)
show ?thesis
by (meson PT.prems UNIV_I (λx. [x]) ` dom m  Prefix_Tree.set (PT m) inj (λx. [x]) inj_on_finite inj_on_subset subsetI)
qed
moreover have " t . t  ran m  finite_tree t"
proof -
fix t assume "t  ran m"
then obtain x where "m x = Some t"
unfolding ran_def by blast
then have "(#) x ` set t  set (PT m)"
unfolding set_alt_def
by auto
then have "finite ((#) x ` set t)"
using PT.prems
moreover have "inj ((#) x)"
by auto
ultimately have "finite (set t)"
then show "finite_tree t"
using PT.IH[of "Some t" t] m x = Some t
by (metis option.set_intros rangeI)
qed
ultimately show ?case
by simp
qed
qed

lemma empty_finite_tree :

unfolding finite_tree_iff set_empty by auto

lemma insert_finite_tree :
assumes "finite_tree t"
shows "finite_tree (insert t xs)"
proof -
have "{xs'. xs''. xs = xs' @ xs''} = list.set (prefixes xs)"
unfolding prefixes_set by blast
then have "finite {xs'. xs''. xs = xs' @ xs''}"
using List.finite_set by simp
then show ?thesis
using assms unfolding finite_tree_iff insert_set
by blast
qed

lemma from_list_finite_tree :
"finite_tree (from_list xs)"
using insert_finite_tree empty_finite_tree by (induction xs; auto)

lemma combine_after_finite_tree :
assumes "finite_tree t1"
and     "finite_tree t2"
shows "finite_tree (combine_after t1 α t2)"
proof -
have "finite (Prefix_Tree.set t2)" and "finite (Prefix_Tree.set t1)"
using assms unfolding finite_tree_iff by auto
then have "finite (Prefix_Tree.set (Prefix_Tree.insert t1 α)  {α @ as |as. as  Prefix_Tree.set t2})"
using finite_tree_iff insert_finite_tree by fastforce
then show ?thesis
unfolding finite_tree_iff combine_after_set
by (metis insert_set)
qed

lemma combine_finite_tree :
assumes "finite_tree t1"
and     "finite_tree t2"
shows "finite_tree (combine t1 t2)"
using assms unfolding finite_tree_iff combine_set
by blast

function (domintros) sorted_list_of_maximal_sequences_in_tree :: "('a :: linorder) prefix_tree  'a list list" where
"sorted_list_of_maximal_sequences_in_tree (PT m) =
(if dom m = {}
then [[]]
else concat (map (λk . map ((#) k) (sorted_list_of_maximal_sequences_in_tree (the (m k)))) (sorted_list_of_set (dom m))))"
by pat_completeness auto
termination
proof -
{ fix a :: "'a prefix_tree"

have
proof (induction a)
case (PT m)
then show ?case
by (metis List.set_empty domIff empty_iff option.set_sel range_eqI set_sorted_list_of_set sorted_list_of_maximal_sequences_in_tree.domintros sorted_list_of_set.fold_insort_key.infinite)
qed
}
then show ?thesis by auto
qed

lemma sorted_list_of_maximal_sequences_in_tree_Nil :
assumes
shows "t = empty"
proof -
obtain m where "t = PT m"
using prefix_tree.exhaust by blast

show ?thesis proof (cases "dom m = {}")
case True
then have "m = Map.empty"
using True by blast
then show ?thesis
unfolding t = PT m
next
case False
then have "[]  list.set (concat (map (λk . map ((#) k) (sorted_list_of_maximal_sequences_in_tree (the (m k)))) (sorted_list_of_set (dom m))))"
using assms unfolding t = PT m by auto
then show ?thesis
by auto
qed
qed

lemma sorted_list_of_maximal_sequences_in_tree_set :
assumes "finite_tree t"
shows "list.set (sorted_list_of_maximal_sequences_in_tree t) = {y. y  set t  ¬( y' . y'  []  y@y'  set t)}"
(is "?S1 = ?S2")
proof
show "?S1  ?S2"
proof
fix xs assume "xs  ?S1"
then show "xs  ?S2"
proof (induction xs arbitrary: t)
case Nil
then have "t = empty"
using sorted_list_of_maximal_sequences_in_tree_Nil by auto
then show ?case
using set_empty by auto
next
case (Cons x xs)

obtain m where "t = PT m"
using prefix_tree.exhaust by blast
have "x#xs  list.set (concat (map (λk . map ((#) k) (sorted_list_of_maximal_sequences_in_tree (the (m k)))) (sorted_list_of_set (dom m))))"
by (metis (no_types) Cons.prems(1) t = PT m empty_iff list.set(1) list.simps(3) set_ConsD sorted_list_of_maximal_sequences_in_tree.simps)
then have "x  list.set (sorted_list_of_set (dom m))"
and
by auto

have "x  dom m"
using x  list.set (sorted_list_of_set (dom m)) unfolding t = PT m
by (metis equals0D list.set(1) sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
then obtain t' where "m x = Some t'"
by auto
then have
using
by auto
then have "xs  set t'" and "¬( y' . y'  []  xs@y'  set t')"
using Cons.IH by blast+

have "x#xs  set t"
unfolding t = PT m using xs  set t' m x = Some t' by auto
moreover have "¬( y' . y'  []  (x#xs)@y'  set t)"
proof
assume "y'. y'  []  (x # xs) @ y'  Prefix_Tree.set t"
then obtain y' where "y'  []" and "(x # xs) @ y'  Prefix_Tree.set t"
by blast
then have "isin (PT m) (x # (xs @ y'))"
unfolding t = PT m by auto
then have "isin t' (xs @ y')"
using m x = Some t' by auto
then have " y' . y'  []  xs@y'  set t'"
using y'  [] by auto
then show False
using ¬( y' . y'  []  xs@y'  set t') by simp
qed
ultimately show ?case by blast
qed
qed

show "?S2  ?S1"
proof
fix xs assume "xs  ?S2"
then show "xs  ?S1"
using assms proof (induction xs arbitrary: t)
case Nil
then have "set t = {[]}"
by auto
moreover obtain m where "t = PT m"
using prefix_tree.exhaust by blast
ultimately have " x . ¬ isin (PT m) [x]"
by force
moreover have " x . x  dom m  isin (PT m) [x]"
by auto
ultimately have "dom m = {}"
by blast
then show ?case
unfolding t = PT m by auto
next
case (Cons x xs)

obtain m where "t = PT m"
using prefix_tree.exhaust by blast
then have "isin (PT m) (x#xs)"
using Cons.prems(1) by auto
then obtain t' where "m x = Some t'"
and "isin t' xs"
by (metis case_optionE isin.simps(2))
then have "x  dom m"
by auto
then have "dom m  {}"
by auto

have "finite_tree t'"
using finite_tree t m x = Some t' unfolding t = PT m
by (meson finite_tree.simps ranI)
moreover have "xs  {y  Prefix_Tree.set t'. y'. y'  []  y @ y'  Prefix_Tree.set t'}"
proof -
have "xs  set t'"
using isin t' xs by auto
moreover have "(y'. y'  []  xs @ y'  Prefix_Tree.set t')"
proof
assume "y'. y'  []  xs @ y'  Prefix_Tree.set t'"
then obtain y' where "y'  []" and "xs @ y'  Prefix_Tree.set t'"
by blast
then have "isin t' (xs@y')"
by auto
then have "isin (PT m) (x#(xs@y'))"
using m x = Some t' by auto
then show False
using Cons.prems(1) y'  [] unfolding t = PT m by auto
qed
ultimately show ?thesis
by blast
qed
ultimately have
using Cons.IH by blast
moreover have "x  list.set (sorted_list_of_set (dom m))"
using x  dom m finite_tree t unfolding t = PT m
by simp
ultimately show ?case
using finite_tree t dom m  {} m x = Some t' unfolding t = PT m
by force
qed
qed
qed

lemma sorted_list_of_maximal_sequences_in_tree_ob :
assumes "finite_tree T"
and     "xs  set T"
obtains xs' where
proof -
let ?xs = "{xs@xs' | xs' . xs@xs'  set T}"

let ?xs' = "arg_max_on length ?xs"

have "xs  ?xs"
using assms(2) by auto
then have "?xs  {}"
by blast
moreover have "finite ?xs"
using finite_subset[of ?xs "set T"]
using assms(1) unfolding finite_tree_iff
by blast
ultimately obtain xs' where "xs'  ?xs" and " xs'' . xs''  ?xs  length xs''  length xs'"
using max_length_elem[of ?xs]
by force

obtain xs'' where "xs' = xs@xs''" and "xs@xs''  set T"
using xs'  ?xs by auto
have " xs''' . xs@xs'''  set T  length xs'''  length xs''"
proof -
fix xs''' assume "xs@xs'''  set T"
then have "xs@xs'''  ?xs"
by auto
then have "length (xs@xs''')   length xs'"
using  xs'' . xs''  ?xs  length xs''  length xs'
by blast
then show "length xs'''  length xs''"
unfolding xs' = xs@xs'' by auto
qed
then have "¬( y' . y'  []  (xs@xs'')@y'  set T)"
by fastforce
then have
using xs@xs''  set T
unfolding sorted_list_of_maximal_sequences_in_tree_set[OF assms(1)]
by blast
then show ?thesis using that by blast
qed

function (domintros) sorted_list_of_sequences_in_tree :: "('a :: linorder) prefix_tree  'a list list" where
"sorted_list_of_sequences_in_tree (PT m) =
(if dom m = {}
then [[]]
else [] # concat (map (λk . map ((#) k) (sorted_list_of_sequences_in_tree (the (m k)))) (sorted_list_of_set (dom m))))"
by pat_completeness auto
termination
proof -
{
fix a :: "'a prefix_tree"

have
proof (induction a)
case (PT m)
then show ?case
by (metis List.set_empty domIff emptyE option.set_sel rangeI sorted_list_of_sequences_in_tree.domintros sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
qed
}
then show ?thesis by auto
qed

lemma sorted_list_of_sequences_in_tree_set :
assumes "finite_tree t"
shows
(is "?S1 = ?S2")
proof
show "?S1  ?S2"
proof
fix xs assume "xs  ?S1"
then show "xs  ?S2"
proof (induction xs arbitrary: t)
case Nil
then show ?case
using set_empty by auto
next
case (Cons x xs)

obtain m where "t = PT m"
using prefix_tree.exhaust by blast
have "x#xs  list.set (concat (map (λk . map ((#) k) (sorted_list_of_sequences_in_tree (the (m k)))) (sorted_list_of_set (dom m))))"
by (metis (no_types) Cons.prems(1) t = PT m empty_iff list.set(1) list.simps(3) set_ConsD sorted_list_of_sequences_in_tree.simps)
then have "x  list.set (sorted_list_of_set (dom m))"
and "xs  list.set (sorted_list_of_sequences_in_tree (the (m x)))"
by auto

have "x  dom m"
using x  list.set (sorted_list_of_set (dom m)) unfolding t = PT m
by (metis emptyE empty_set sorted_list_of_set.fold_insort_key.infinite sorted_list_of_set.set_sorted_key_list_of_set)
then obtain t' where "m x = Some t'"
by auto
then have
using xs  list.set (sorted_list_of_sequences_in_tree (the (m x)))
by auto
then have "xs  set t'"
using Cons.IH by blast+

show "x#xs  set t"
unfolding t = PT m using xs  set t' m x = Some t' by auto
qed
qed

show "?S2  ?S1"
proof
fix xs assume "xs  ?S2"
then show "xs  ?S1"
using assms proof (induction xs arbitrary: t)
case Nil
obtain m where "t = PT m"
using prefix_tree.exhaust by blast
then show ?case
by auto
next
case (Cons x xs)

obtain m where "t = PT m"
using prefix_tree.exhaust by blast
then have "isin (PT m) (x#xs)"
using Cons.prems(1) by auto
then obtain t' where "m x = Some t'"
and "isin t' xs"
by (metis case_optionE isin.simps(2))
then have "x  dom m"
by auto
then have "dom m  {}"
by auto

have "finite_tree t'"
using finite_tree t m x = Some t' unfolding t = PT m
by (meson finite_tree.simps ranI)
moreover have "xs  set t'"
using isin t' xs by auto
ultimately have
using Cons.IH by blast
moreover have "x  list.set (sorted_list_of_set (dom m))"
using x  dom m finite_tree t unfolding t = PT m
by simp
ultimately show ?case
using finite_tree t dom m  {} m x = Some t' unfolding t = PT m
by force
qed
qed
qed

fun difference_list :: "('a::linorder) prefix_tree  'a prefix_tree  'a list list" where
"difference_list t1 t2 = filter (λ xs . ¬ isin t2 xs) (sorted_list_of_sequences_in_tree t1)"

lemma difference_list_set :
assumes "finite_tree t1"
shows "List.set (difference_list t1 t2) = (set t1 - set t2)"
unfolding difference_list.simps
filter_set[symmetric]
sorted_list_of_sequences_in_tree_set[OF assms]
set.simps
by fastforce

fun is_leaf :: "'a prefix_tree  bool" where
"is_leaf t = (t = empty)"

fun is_maximal_in :: "'a prefix_tree  'a list  bool" where
"is_maximal_in T α = (isin T α  is_leaf (after T α))"

function (domintros) height :: "'a prefix_tree  nat" where
"height (PT m) = (if (is_leaf (PT m)) then 0 else 1 + Max (height ` ran m))"
by pat_completeness auto
termination
proof -
{ fix a :: "'a prefix_tree"

have "height_dom a"
proof (induction a)
case (PT m)

have "(x. x  ran m  height_dom x)"
proof -
fix x :: "'a prefix_tree"
assume "x  ran m"
then have "a. m a = Some x"
then show "height_dom x"
using PT.IH by blast
qed
then show ?case
using height.domintros
by blast
qed
}
then show ?thesis by auto
qed

function (domintros) height_over :: "'a list  'a prefix_tree  nat" where
"height_over xs (PT m) = 1 + foldr (λ x maxH . case m x of Some t'  max (height_over xs t') maxH | None  maxH) xs 0"
by pat_completeness auto
termination
proof -
{
fix a :: "'a prefix_tree"
fix xs :: "'a list"

have "height_over_dom (xs, a)"
proof (induction a)
case (PT m)

have "(x. x  ran m  height_over_dom (xs, x))"
proof -
fix x :: "'a prefix_tree"
assume "x  ran m"
then have "a. m a = Some x"
then show "height_over_dom (xs, x)"
using PT.IH by blast
qed
then show ?case
using height_over.domintros
qed
}
then show ?thesis by auto
qed

lemma height_over_empty :

proof -
define xs' where "xs' = xs"
have "foldr (λ x maxH . case Map.empty x of Some t'  max (height_over xs' t') maxH | None  maxH) xs 0 = 0"
by (induction xs; auto)
then show ?thesis
unfolding xs'_def empty_def
by auto
qed

lemma height_over_subtree_less :
assumes "m x = Some t'"
and     "x  list.set xs"
shows "height_over xs t' < height_over xs (PT m)"
proof -

define xs' where "xs' = xs"

have "height_over xs' t'  foldr (λ x maxH . case m x of Some t'  max (height_over xs' t') maxH | None  maxH) xs 0"
using assms(2) proof (induction xs)
case Nil
then show ?case by auto
next
case (Cons x' xs)

define f where "f = foldr (λ x maxH . case m x of Some t'  max (height_over xs' t') maxH | None  maxH) xs 0"

have *: "foldr (λ x maxH . case m x of Some t'  max (height_over xs' t') maxH | None  maxH) (x'#xs) 0
= (case m x' of Some t'  max (height_over xs' t') f | None  f)"
unfolding f_def by auto

show ?case proof (cases "x=x'")
case True
show ?thesis
using m x = Some t'
unfolding * True by auto
next
case False
then have "x  list.set xs"
using Cons.prems(1) by auto
show ?thesis
using Cons.IH[OF x  list.set xs]
unfolding * f_def[symmetric]
by (cases "m x'"; auto)
qed
qed
then show ?thesis
unfolding xs'_def by auto
qed

fun maximum_prefix :: "'a prefix_tree  'a list  'a list" where
"maximum_prefix t [] = []" |
"maximum_prefix (PT m) (x # xs) = (case m x of None  [] | Some t  x # maximum_prefix t xs)"

lemma maximum_prefix_isin :
"isin t (maximum_prefix t xs)"
proof (induction xs arbitrary: t)
case Nil
show ?case
by auto
next
case (Cons x xs)

obtain m where *:"t = PT m"
using finite_tree.cases by blast

show ?case proof (cases "m x")
case None
then have "maximum_prefix t (x#xs) = []"
unfolding * by auto
then show ?thesis
by auto
next
case (Some t')
then have "maximum_prefix t (x#xs) = x # maximum_prefix t' xs"
unfolding * by auto
moreover have "isin t' (maximum_prefix t' xs)"
using Cons.IH by auto
ultimately show ?thesis
qed
qed

lemma maximum_prefix_maximal :
"maximum_prefix t xs = xs
( x' xs' . xs = (maximum_prefix t xs)@[x']@xs'  ¬ isin t ((maximum_prefix t xs)@[x']))"
proof (induction xs arbitrary: t)
case Nil
show ?case by auto
next
case (Cons x xs)
obtain m where *:"t = PT m"
using finite_tree.cases by blast

show ?case proof (cases "m x")
case None
then have "maximum_prefix t (x#xs) = []"
unfolding * by auto
moreover have "¬ isin t ([]@[x]@xs)"
using isin_prefix[of t "[x]" xs]
ultimately show ?thesis
next
case (Some t')
then have "maximum_prefix t (x#xs) = x # maximum_prefix t' xs"
unfolding * by auto
moreover note Cons.IH[of t']
ultimately show ?thesis
qed
qed

(* collects for sequence xs all sequences ys in the tree such that ys is maximal in the tree and
(map fst ys) is a prefix of (map fst xs) *)
fun maximum_fst_prefixes :: "('a×'b) prefix_tree  'a list  'b list  ('a×'b) list list" where
"maximum_fst_prefixes t [] ys = (if is_leaf t then [[]] else [])" |
"maximum_fst_prefixes (PT m) (x # xs) ys = (if is_leaf (PT m) then [[]] else concat (map (λ y . map ((#) (x,y)) (maximum_fst_prefixes (the (m (x,y))) xs ys)) (filter (λ y . (m (x,y)  None)) ys)))"

lemma maximum_fst_prefixes_set :
"list.set (maximum_fst_prefixes t xs ys)  set t"
proof (induction xs arbitrary: t)
case Nil
show ?case
by auto
next
case (Cons x xs)

obtain m where *:"t = PT m"
using finite_tree.cases by blast

show "list.set (maximum_fst_prefixes t (x # xs) ys)  set t"
proof
fix p assume "p  list.set (maximum_fst_prefixes t (x # xs) ys)"

show "p  set t" proof (cases "is_leaf (PT m)")
case True
then have "p = []"
using p  list.set (maximum_fst_prefixes t (x # xs) ys)  unfolding * maximum_fst_prefixes.simps by force
then show ?thesis
using set_Nil[of t]
by blast
next
case False
then obtain y where "y  list.set (filter (λ y . (m (x,y)  None)) ys)"
and "p  list.set (map ((#) (x,y)) (maximum_fst_prefixes (the (m (x,y))) xs ys))"
using p  list.set (maximum_fst_prefixes t (x # xs) ys)
unfolding * by auto

then have "m (x,y)  None"
by auto
then obtain t' where "m (x,y) = Some t'"
by auto
moreover obtain p' where "p = (x,y)#p'" and "p'  list.set (maximum_fst_prefixes (the (m (x,y))) xs ys)"
using p  list.set (map ((#) (x,y)) (maximum_fst_prefixes (the (m (x,y))) xs ys))
by auto
ultimately have "isin t' p'"
using Cons.IH
by auto
then have "isin t p"
unfolding * p = (x,y)#p' using m (x,y) = Some t' by auto
then show "p  set t"
by auto
qed
qed
qed

lemma maximum_fst_prefixes_are_prefixes :
assumes "xys  list.set (maximum_fst_prefixes t xs ys)"
shows "map fst xys = take (length xys) xs"
using assms proof (induction xys arbitrary: t xs)
case Nil
then show ?case by auto
next
case (Cons xy xys)
then have "xs  []"
by auto
then obtain x xs' where "xs = x#xs'"
using list.exhaust by auto

obtain m where *:"t = PT m"
using finite_tree.cases by blast
have "is_leaf (PT m) = False"
using Cons.prems unfolding * xs = x#xs'
by auto
have "(xy#xys)  list.set (concat (map (λ y . map ((#) (x,y)) (maximum_fst_prefixes (the (m (x,y))) xs' ys)) (filter (λ y . (m (x,y)  None)) ys)))"
using Cons.prems unfolding * xs = x#xs' is_leaf (PT m) = False maximum_fst_prefixes.simps by auto
then obtain y where "y  list.set (filter (λ y . (m (x,y)  None)) ys)"
and "(xy#xys)  list.set (map ((#) (x,y)) (maximum_fst_prefixes (the (m (x,y))) xs' ys))"
by auto
then have "xy = (x,y)" and "xys  list.set (maximum_fst_prefixes (the (m (x,y))) xs' ys)"
by auto

have **: "take (length ((x, y) # xys)) (x # xs') = x # (take (length xys) xs')"
by auto

show ?case
using Cons.IH[OF xys  list.set (maximum_fst_prefixes (the (m (x,y))) xs' ys)]
unfolding xy = (x,y) xs = x#xs' ** by auto
qed

lemma finite_tree_set_eq :
assumes "set t1 = set t2"
and     "finite_tree t1"
shows "t1 = t2"
using assms proof (induction "height t1" arbitrary: t1 t2 rule: less_induct)
case less

obtain m1 m2 where "t1 = PT m1" and "t2 = PT m2"
by (metis finite_tree.cases)

show ?case proof (cases "height t1")
case 0

have "t1 = empty"
using 0
unfolding t1 = PT m1 height.simps is_leaf.simps
then have "set t2 = {[]}"
using less Prefix_Tree.set_empty by auto
have "m2 = Map.empty"
proof
show "x. m2 x = None"
proof -
fix x show "m2 x = None"
proof (rule ccontr)
assume "m2 x  None"
then obtain t' where "m2 x = Some t'"
by blast
then have "[x]  set t2"
unfolding t2 = PT m2 set.simps by auto
then show False
using set t2 = {[]} by auto
qed
qed
qed
then show ?thesis
unfolding t1 = empty t2 = PT m2 empty_def by simp
next
case (Suc k)

show ?thesis proof (rule ccontr)
assume "t1  t2"

then have "m1  m2"
using t1 = PT m1 t2 = PT m2 by auto
then obtain x where "m1 x  m2 x"
by (meson ext)

then consider "m1 x  None  m2 x  None" | "m1 x = None  m2 x  None"
by fastforce
then show False proof cases
case 1
then obtain t1' t2' where "m1 x = Some t1'" and "m2 x = Some t2'"
by auto
then have "t1'  t2'"
using m1 x  m2 x by auto
moreover have "set t1' = set t2'"
proof -
have " io . isin t1' io = isin t1 (x#io)"
unfolding t1 = PT m1 using m1 x = Some t1' by auto
moreover have " io . isin t2' io = isin t2 (x