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 "HOL-Library.Mapping" "HOL-Library.List_Lexorder" 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 "Map.empty x ≠ None" 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 by (simp add: "0.prems"(3)) 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' by (simp add: take_tl) 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' by (simp add: take_tl) 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 by (simp add: combine_options_def) 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 "from_list [] = empty" 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 "finite_tree_dom a" 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" by (simp add: ran_def) then show "finite_tree_dom x" 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 [] (⋃x∈dom 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 by (simp add: finite_subset) moreover have "inj ((#) x)" by auto ultimately have "finite (set t)" by (simp add: finite_image_iff) 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 : "finite_tree empty" 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 "sorted_list_of_maximal_sequences_in_tree_dom a" 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 "[] ∈ list.set (sorted_list_of_maximal_sequences_in_tree t)" 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› by (simp add: Prefix_Tree.empty_def) 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 "xs ∈ list.set (sorted_list_of_maximal_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 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 "xs ∈ list.set (sorted_list_of_maximal_sequences_in_tree t')" using ‹xs ∈ list.set (sorted_list_of_maximal_sequences_in_tree (the (m x)))› 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 "xs ∈ list.set (sorted_list_of_maximal_sequences_in_tree t')" 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 "xs@xs' ∈ list.set (sorted_list_of_maximal_sequences_in_tree T)" 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 "xs@xs'' ∈ list.set (sorted_list_of_maximal_sequences_in_tree T)" 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 "sorted_list_of_sequences_in_tree_dom a" 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 "list.set (sorted_list_of_sequences_in_tree t) = 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 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 "xs ∈ list.set (sorted_list_of_sequences_in_tree t')" 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 "xs ∈ list.set (sorted_list_of_sequences_in_tree t')" 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" by (simp add: ran_def) 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" by (simp add: ran_def) then show "height_over_dom (xs, x)" using PT.IH by blast qed then show ?case using height_over.domintros by (simp add: height_over.domintros ranI) qed } then show ?thesis by auto qed lemma height_over_empty : "height_over xs empty = 1" 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 by (simp add: "*" Some) 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] by (simp add: "*" None) ultimately show ?thesis by (simp add: "*" None) 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 by (simp add: "*" Some) 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 by (metis add_is_0 zero_neq_one) 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