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