[STATEMENT]
lemma dfs_match_distinct:
  "distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))
[PROOF STEP]
proof (induct xs rule: list.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct (dfs f []) \<Longrightarrow> distinct (dfs f (map (match a) []))
 2. \<And>x1 x2. \<lbrakk>distinct (dfs f x2) \<Longrightarrow> distinct (dfs f (map (match a) x2)); distinct (dfs f (x1 # x2))\<rbrakk> \<Longrightarrow> distinct (dfs f (map (match a) (x1 # x2)))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))
distinct (dfs f (x # xs))

goal (2 subgoals):
 1. distinct (dfs f []) \<Longrightarrow> distinct (dfs f (map (match a) []))
 2. \<And>x1 x2. \<lbrakk>distinct (dfs f x2) \<Longrightarrow> distinct (dfs f (map (match a) x2)); distinct (dfs f (x1 # x2))\<rbrakk> \<Longrightarrow> distinct (dfs f (map (match a) (x1 # x2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))
distinct (dfs f (x # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))
distinct (dfs f (x # xs))

goal (1 subgoal):
 1. distinct (dfs f (map (match a) (x # xs)))
[PROOF STEP]
using dfs_match_subset[of f a xs]
[PROOF STATE]
proof (prove)
using this:
distinct (dfs f xs) \<Longrightarrow> distinct (dfs f (map (match a) xs))
distinct (dfs f (x # xs))
set (dfs f (map (match a) xs)) \<subseteq> set (dfs f xs)

goal (1 subgoal):
 1. distinct (dfs f (map (match a) (x # xs)))
[PROOF STEP]
by (cases x, auto)
[PROOF STATE]
proof (state)
this:
distinct (dfs f (map (match a) (x # xs)))

goal (1 subgoal):
 1. distinct (dfs f []) \<Longrightarrow> distinct (dfs f (map (match a) []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma dfs_match:
  "distinct (prios xs) \<Longrightarrow>
   distinct (dfs f xs) \<Longrightarrow>
   Some t \<in> set xs \<Longrightarrow>
   priority t = a \<Longrightarrow>
   set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)
[PROOF STEP]
proof (induct xs arbitrary: t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>distinct (prios []); distinct (dfs f []); Some t \<in> set []; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) [])) = set (dfs f []) - set (bt_dfs f t)
 2. \<And>xs t. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (None # xs)); distinct (dfs f (None # xs)); Some t \<in> set (None # xs); priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (None # xs))) = set (dfs f (None # xs)) - set (bt_dfs f t)
 3. \<And>x xs t. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some x # xs)); distinct (dfs f (Some x # xs)); Some t \<in> set (Some x # xs); priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some x # xs))) = set (dfs f (Some x # xs)) - set (bt_dfs f t)
[PROOF STEP]
case (Some r xs t)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a

goal (3 subgoals):
 1. \<And>t. \<lbrakk>distinct (prios []); distinct (dfs f []); Some t \<in> set []; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) [])) = set (dfs f []) - set (bt_dfs f t)
 2. \<And>xs t. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (None # xs)); distinct (dfs f (None # xs)); Some t \<in> set (None # xs); priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (None # xs))) = set (dfs f (None # xs)) - set (bt_dfs f t)
 3. \<And>x xs t. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some x # xs)); distinct (dfs f (Some x # xs)); Some t \<in> set (Some x # xs); priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some x # xs))) = set (dfs f (Some x # xs)) - set (bt_dfs f t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a

goal (1 subgoal):
 1. set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
proof (cases "t = r")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
t = r

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
from Some
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
[PROOF STEP]
have "priority r \<notin> set (prios xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a

goal (1 subgoal):
 1. priority r \<notin> set (prios xs)
[PROOF STEP]
by (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
priority r \<notin> set (prios xs)

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
with Some True
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t = r
priority r \<notin> set (prios xs)
[PROOF STEP]
have "a \<notin> set (prios xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t = r
priority r \<notin> set (prios xs)

goal (1 subgoal):
 1. a \<notin> set (prios xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<notin> set (prios xs)

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
hence "\<forall> s. Some s \<in> set xs \<longrightarrow> priority s \<noteq> a"
[PROOF STATE]
proof (prove)
using this:
a \<notin> set (prios xs)

goal (1 subgoal):
 1. \<forall>s. Some s \<in> set xs \<longrightarrow> priority s \<noteq> a
[PROOF STEP]
by (induct xs) (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
\<forall>s. Some s \<in> set xs \<longrightarrow> priority s \<noteq> a

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
hence "set (dfs f (map (match a) xs)) = set (dfs f xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. Some s \<in> set xs \<longrightarrow> priority s \<noteq> a

goal (1 subgoal):
 1. set (dfs f (map (match a) xs)) = set (dfs f xs)
[PROOF STEP]
by (simp add: dfs_match_not_in)
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) xs)) = set (dfs f xs)

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t = r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
 2. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
with True Some
[PROOF STATE]
proof (chain)
picking this:
t = r
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
set (dfs f (map (match a) xs)) = set (dfs f xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = r
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
set (dfs f (map (match a) xs)) = set (dfs f xs)

goal (1 subgoal):
 1. set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
t \<noteq> r

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
with Some.prems
[PROOF STATE]
proof (chain)
picking this:
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r
[PROOF STEP]
have "Some t \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r

goal (1 subgoal):
 1. Some t \<in> set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some t \<in> set xs

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
with \<open>priority t = a\<close>
[PROOF STATE]
proof (chain)
picking this:
priority t = a
Some t \<in> set xs
[PROOF STEP]
have "a \<in> set (prios xs)"
[PROOF STATE]
proof (prove)
using this:
priority t = a
Some t \<in> set xs

goal (1 subgoal):
 1. a \<in> set (prios xs)
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>priority t = a; Some t \<in> set []\<rbrakk> \<Longrightarrow> a \<in> set (prios [])
 2. \<And>xs. \<lbrakk>\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs); priority t = a; Some t \<in> set (None # xs)\<rbrakk> \<Longrightarrow> a \<in> set (prios (None # xs))
 3. \<And>x xs. \<lbrakk>\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs); priority t = a; Some t \<in> set (Some x # xs)\<rbrakk> \<Longrightarrow> a \<in> set (prios (Some x # xs))
[PROOF STEP]
case (Some x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs)
priority t = a
Some t \<in> set (Some x # xs)

goal (3 subgoals):
 1. \<lbrakk>priority t = a; Some t \<in> set []\<rbrakk> \<Longrightarrow> a \<in> set (prios [])
 2. \<And>xs. \<lbrakk>\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs); priority t = a; Some t \<in> set (None # xs)\<rbrakk> \<Longrightarrow> a \<in> set (prios (None # xs))
 3. \<And>x xs. \<lbrakk>\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs); priority t = a; Some t \<in> set (Some x # xs)\<rbrakk> \<Longrightarrow> a \<in> set (prios (Some x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs)
priority t = a
Some t \<in> set (Some x # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs)
priority t = a
Some t \<in> set (Some x # xs)

goal (1 subgoal):
 1. a \<in> set (prios (Some x # xs))
[PROOF STEP]
by (cases "t = x") (simp_all add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
a \<in> set (prios (Some x # xs))

goal (2 subgoals):
 1. \<lbrakk>priority t = a; Some t \<in> set []\<rbrakk> \<Longrightarrow> a \<in> set (prios [])
 2. \<And>xs. \<lbrakk>\<lbrakk>priority t = a; Some t \<in> set xs\<rbrakk> \<Longrightarrow> a \<in> set (prios xs); priority t = a; Some t \<in> set (None # xs)\<rbrakk> \<Longrightarrow> a \<in> set (prios (None # xs))
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
a \<in> set (prios xs)

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
with False Some
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> r
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
a \<in> set (prios xs)
[PROOF STEP]
have "priority r \<noteq> a"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> r
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
a \<in> set (prios xs)

goal (1 subgoal):
 1. priority r \<noteq> a
[PROOF STEP]
by (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
priority r \<noteq> a

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
priority r \<noteq> a

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
from Some False
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r
[PROOF STEP]
have "set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (prios xs); distinct (dfs f xs); Some ?t \<in> set xs; priority ?t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f ?t)
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r

goal (1 subgoal):
 1. set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
from Some.prems False
[PROOF STATE]
proof (chain)
picking this:
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r
[PROOF STEP]
have "set (bt_dfs f t) \<inter> set (bt_dfs f r) = {}"
[PROOF STATE]
proof (prove)
using this:
distinct (prios (Some r # xs))
distinct (dfs f (Some r # xs))
Some t \<in> set (Some r # xs)
priority t = a
t \<noteq> r

goal (1 subgoal):
 1. set (bt_dfs f t) \<inter> set (bt_dfs f r) = {}
[PROOF STEP]
by (induct xs) auto
[PROOF STATE]
proof (state)
this:
set (bt_dfs f t) \<inter> set (bt_dfs f r) = {}

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
hence "set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)"
[PROOF STATE]
proof (prove)
using this:
set (bt_dfs f t) \<inter> set (bt_dfs f r) = {}

goal (1 subgoal):
 1. set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (Some r # xs)); distinct (dfs f (Some r # xs)); Some t \<in> set (Some r # xs); priority t = a; t \<noteq> r\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
priority r \<noteq> a
set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)
set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
priority r \<noteq> a
set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)
set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)

goal (1 subgoal):
 1. set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) (Some r # xs))) = set (dfs f (Some r # xs)) - set (bt_dfs f t)

goal (2 subgoals):
 1. \<And>t. \<lbrakk>distinct (prios []); distinct (dfs f []); Some t \<in> set []; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) [])) = set (dfs f []) - set (bt_dfs f t)
 2. \<And>xs t. \<lbrakk>\<And>t. \<lbrakk>distinct (prios xs); distinct (dfs f xs); Some t \<in> set xs; priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t); distinct (prios (None # xs)); distinct (dfs f (None # xs)); Some t \<in> set (None # xs); priority t = a\<rbrakk> \<Longrightarrow> set (dfs f (map (match a) (None # xs))) = set (dfs f (None # xs)) - set (bt_dfs f t)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma alist_meld:
  "distinct (dfs val xs) \<Longrightarrow> distinct (dfs val ys) \<Longrightarrow>
   set (dfs val xs) \<inter> set (dfs val ys) = {} \<Longrightarrow>
   set (dfs alist (meld xs ys)) = set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
[PROOF STEP]
proof (induct xs ys rule: meld.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>xs y ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (None # xs) (y # ys))) = set (elements (None # xs)) \<union> set (elements (y # ys))
 4. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 5. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
case (3 xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (5 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>xs y ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (None # xs) (y # ys))) = set (elements (None # xs)) \<union> set (elements (y # ys))
 4. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 5. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
have "set (dfs alist (y # meld xs ys)) =
    set (dfs alist xs) \<union> set (dfs alist (y # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
note assms = "3"
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
have "set (vals xs) \<inter> set (vals ys) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
using set_dfs_Cons[of val y ys]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
set (vals (y # ys)) = set (vals ys) \<union> set (vals [y])

goal (1 subgoal):
 1. set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
have "distinct (vals ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. distinct (vals ys)
[PROOF STEP]
by (cases y) simp_all
[PROOF STATE]
proof (state)
this:
distinct (vals ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
have "distinct (vals xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. distinct (vals xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (vals xs)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals xs)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
note assms
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (vals xs) \<inter> set (vals ys) = {}
distinct (vals ys)
distinct (vals xs)
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
have "set (dfs alist (meld xs ys)) =
      set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
using this:
set (vals xs) \<inter> set (vals ys) = {}
distinct (vals ys)
distinct (vals xs)
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
hence "set (dfs alist (y # meld xs ys)) =
      set (dfs alist [y]) \<union> set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
using this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
using set_dfs_Cons[of alist y "meld xs ys"]
[PROOF STATE]
proof (prove)
using this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
set (elements (y # meld xs ys)) = set (elements (meld xs ys)) \<union> set (elements [y])

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
using set_dfs_Cons[of alist y ys]
[PROOF STATE]
proof (prove)
using this:
set (elements (y # meld xs ys)) = set (elements [y]) \<union> set (elements xs) \<union> set (elements ys)
set (elements (y # ys)) = set (elements ys) \<union> set (elements [y])

goal (1 subgoal):
 1. set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))

goal (5 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>xs y ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (None # xs) (y # ys))) = set (elements (None # xs)) \<union> set (elements (y # ys))
 4. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 5. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (elements (y # meld xs ys)) = set (elements xs) \<union> set (elements (y # ys))

goal (1 subgoal):
 1. set (elements (meld (None # xs) (y # ys))) = set (elements (None # xs)) \<union> set (elements (y # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (meld (None # xs) (y # ys))) = set (elements (None # xs)) \<union> set (elements (y # ys))

goal (4 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 4. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 4. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
case (4 x xs ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (4 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 4. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
have "set (dfs alist (x # meld xs ys)) =
    set (dfs alist (x # xs)) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
(* this is the same as for 3 minus some renaming *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
note assms = "4"
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
[PROOF STEP]
have "set (vals xs) \<inter> set (vals ys) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
using set_dfs_Cons[of val x xs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
set (vals (x # xs)) = set (vals xs) \<union> set (vals [x])

goal (1 subgoal):
 1. set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
[PROOF STEP]
have "distinct (vals xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. distinct (vals xs)
[PROOF STEP]
by (cases x) simp_all
[PROOF STATE]
proof (state)
this:
distinct (vals xs)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals xs)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
[PROOF STEP]
have "distinct (vals ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. distinct (vals ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (vals ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
note assms
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (vals xs) \<inter> set (vals ys) = {}
distinct (vals xs)
distinct (vals ys)
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
[PROOF STEP]
have "set (dfs alist (meld xs ys)) =
      set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
using this:
set (vals xs) \<inter> set (vals ys) = {}
distinct (vals xs)
distinct (vals ys)
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
hence "set (dfs alist (x # meld xs ys)) =
      set (dfs alist [x]) \<union> set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
using this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
using set_dfs_Cons[of alist x "meld xs ys"]
[PROOF STATE]
proof (prove)
using this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
set (elements (x # meld xs ys)) = set (elements (meld xs ys)) \<union> set (elements [x])

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
using set_dfs_Cons[of alist x xs]
[PROOF STATE]
proof (prove)
using this:
set (elements (x # meld xs ys)) = set (elements [x]) \<union> set (elements xs) \<union> set (elements ys)
set (elements (x # xs)) = set (elements xs) \<union> set (elements [x])

goal (1 subgoal):
 1. set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)

goal (4 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
 4. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (elements (x # meld xs ys)) = set (elements (x # xs)) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (meld (x # xs) (None # ys))) = set (elements (x # xs)) \<union> set (elements (None # ys))

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
case (5 x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
have "set (dfs alist (add (Some (merge x y)) (meld xs ys))) =
    set (bt_dfs alist x) \<union> set (dfs alist xs)
    \<union> set (bt_dfs alist y) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
note assms = "5"
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have "distinct (bt_dfs val x)" "distinct (bt_dfs val y)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. distinct (bt_dfs val x) &&& distinct (bt_dfs val y)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val x)
distinct (bt_dfs val y)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val x)
distinct (bt_dfs val y)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have xyint:
      "set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}
[PROOF STEP]
by (auto simp add: set_dfs_Cons)
[PROOF STATE]
proof (state)
this:
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (bt_dfs val x)
distinct (bt_dfs val y)
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}
[PROOF STEP]
have *: "set (dfs alist [Some (merge x y)]) =
      set (bt_dfs alist x) \<union> set (bt_dfs alist y)"
[PROOF STATE]
proof (prove)
using this:
distinct (bt_dfs val x)
distinct (bt_dfs val y)
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}

goal (1 subgoal):
 1. set (elements [Some (merge x y)]) = set (bt_dfs alist x) \<union> set (bt_dfs alist y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements [Some (merge x y)]) = set (bt_dfs alist x) \<union> set (bt_dfs alist y)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (elements [Some (merge x y)]) = set (bt_dfs alist x) \<union> set (bt_dfs alist y)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have **: "set (dfs alist (meld xs ys)) = set (dfs alist xs) \<union> set (dfs alist ys)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
[PROOF STEP]
by (auto simp add: set_dfs_Cons)
[PROOF STATE]
proof (state)
this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have "distinct (vals (Some (merge x y) # meld xs ys))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
from assms xyint
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}
[PROOF STEP]
have "distinct (bt_dfs val (merge x y))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}

goal (1 subgoal):
 1. distinct (bt_dfs val (merge x y))
[PROOF STEP]
by (simp add: vals_merge_distinct)
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val (merge x y))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val (merge x y))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have
        "distinct (vals xs)"
        and "distinct (vals ys)"
        and "set (vals xs) \<inter> set (vals ys) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. distinct (vals xs) &&& distinct (vals ys) &&& set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
by (auto simp add: set_dfs_Cons)
[PROOF STATE]
proof (state)
this:
distinct (vals xs)
distinct (vals ys)
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
hence "distinct (vals (meld xs ys))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (vals ys)
set (vals xs) \<inter> set (vals ys) = {}

goal (1 subgoal):
 1. distinct (vals (meld xs ys))
[PROOF STEP]
by (rule vals_meld_distinct)
[PROOF STATE]
proof (state)
this:
distinct (vals (meld xs ys))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals (meld xs ys))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
[PROOF STEP]
have "set (bt_dfs val (merge x y)) \<inter> set (vals (meld xs ys)) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}

goal (1 subgoal):
 1. set (bt_dfs val (merge x y)) \<inter> set (vals (meld xs ys)) = {}
[PROOF STEP]
by (auto simp add: vals_meld)
[PROOF STATE]
proof (state)
this:
set (bt_dfs val (merge x y)) \<inter> set (vals (meld xs ys)) = {}

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some x # xs)); distinct (vals (Some y # ys)); set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (bt_dfs val (merge x y))
distinct (vals (meld xs ys))
set (bt_dfs val (merge x y)) \<inter> set (vals (meld xs ys)) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (bt_dfs val (merge x y))
distinct (vals (meld xs ys))
set (bt_dfs val (merge x y)) \<inter> set (vals (meld xs ys)) = {}

goal (1 subgoal):
 1. distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (vals (Some (merge x y) # meld xs ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (vals (Some (merge x y) # meld xs ys))

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (elements [Some (merge x y)]) = set (bt_dfs alist x) \<union> set (bt_dfs alist y)
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some (merge x y) # meld xs ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (elements [Some (merge x y)]) = set (bt_dfs alist x) \<union> set (bt_dfs alist y)
set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys)
distinct (vals (Some (merge x y) # meld xs ys))

goal (1 subgoal):
 1. set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)
[PROOF STEP]
by (auto simp add: alist_add_Cons)
[PROOF STATE]
proof (state)
this:
set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs ys)) = set (elements xs) \<union> set (elements ys); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> set (elements (meld (Some t # xs) (Some r # ys))) = set (elements (Some t # xs)) \<union> set (elements (Some r # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (elements (add (Some (merge x y)) (meld xs ys))) = set (bt_dfs alist x) \<union> set (elements xs) \<union> set (bt_dfs alist y) \<union> set (elements ys)

goal (1 subgoal):
 1. set (elements (meld (Some x # xs) (Some y # ys))) = set (elements (Some x # xs)) \<union> set (elements (Some y # ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (meld (Some x # xs) (Some y # ys))) = set (elements (Some x # xs)) \<union> set (elements (Some y # ys))

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld [] ys)) = set (elements []) \<union> set (elements ys)
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> set (elements (meld xs [])) = set (elements xs) \<union> set (elements [])
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma alist_delete_min:
  assumes "distinct (vals xs)"
  and "distinct (prios xs)"
  and "find_min xs = Some (Node a v ts)"
  shows "set (dfs alist (delete_min xs)) = set (dfs alist xs) - {(v, a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from \<open>distinct (vals xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
[PROOF STEP]
have d: "distinct (dfs alist xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)

goal (1 subgoal):
 1. distinct (elements xs)
[PROOF STEP]
using dfs_comp_distinct[of fst alist "xs"]
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (dfs (fst \<circ> alist) xs) \<Longrightarrow> distinct (elements xs)

goal (1 subgoal):
 1. distinct (elements xs)
[PROOF STEP]
by (simp only: alist_split)
[PROOF STATE]
proof (state)
this:
distinct (elements xs)

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
[PROOF STEP]
have IN: "Some (Node a v ts) \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)

goal (1 subgoal):
 1. Some (Node a v ts) \<in> set xs
[PROOF STEP]
by (simp add: find_min_exist)
[PROOF STATE]
proof (state)
this:
Some (Node a v ts) \<in> set xs

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
hence sub: "set (bts_dfs alist ts) \<subseteq> set (dfs alist xs)"
[PROOF STATE]
proof (prove)
using this:
Some (Node a v ts) \<in> set xs

goal (1 subgoal):
 1. set (bts_dfs alist ts) \<subseteq> set (elements xs)
[PROOF STEP]
by (induct xs) (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
set (bts_dfs alist ts) \<subseteq> set (elements xs)

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from d IN
[PROOF STATE]
proof (chain)
picking this:
distinct (elements xs)
Some (Node a v ts) \<in> set xs
[PROOF STEP]
have "(v,a) \<notin> set (bts_dfs alist ts)"
[PROOF STATE]
proof (prove)
using this:
distinct (elements xs)
Some (Node a v ts) \<in> set xs

goal (1 subgoal):
 1. (v, a) \<notin> set (bts_dfs alist ts)
[PROOF STEP]
using dfs_distinct_member[of alist xs "Node a v ts"]
[PROOF STATE]
proof (prove)
using this:
distinct (elements xs)
Some (Node a v ts) \<in> set xs
\<lbrakk>distinct (elements xs); Some (Node a v ts) \<in> set xs\<rbrakk> \<Longrightarrow> distinct (bt_dfs alist (Node a v ts))

goal (1 subgoal):
 1. (v, a) \<notin> set (bts_dfs alist ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v, a) \<notin> set (bts_dfs alist ts)

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
with sub
[PROOF STATE]
proof (chain)
picking this:
set (bts_dfs alist ts) \<subseteq> set (elements xs)
(v, a) \<notin> set (bts_dfs alist ts)
[PROOF STEP]
have "set (bts_dfs alist ts) \<subseteq> set (dfs alist xs) - {(v,a)}"
[PROOF STATE]
proof (prove)
using this:
set (bts_dfs alist ts) \<subseteq> set (elements xs)
(v, a) \<notin> set (bts_dfs alist ts)

goal (1 subgoal):
 1. set (bts_dfs alist ts) \<subseteq> set (elements xs) - {(v, a)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (bts_dfs alist ts) \<subseteq> set (elements xs) - {(v, a)}

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
hence nu: "set (bts_dfs alist ts) \<union> (set (dfs alist xs) - {(v,a)}) =
    set (dfs alist xs) - {(v,a)}"
[PROOF STATE]
proof (prove)
using this:
set (bts_dfs alist ts) \<subseteq> set (elements xs) - {(v, a)}

goal (1 subgoal):
 1. set (bts_dfs alist ts) \<union> (set (elements xs) - {(v, a)}) = set (elements xs) - {(v, a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (bts_dfs alist ts) \<union> (set (elements xs) - {(v, a)}) = set (elements xs) - {(v, a)}

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
[PROOF STEP]
have "distinct (vals (map (match a) xs))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)

goal (1 subgoal):
 1. distinct (vals (map (match a) xs))
[PROOF STEP]
by (simp add: dfs_match_distinct)
[PROOF STATE]
proof (state)
this:
distinct (vals (map (match a) xs))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals (map (match a) xs))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from IN assms
[PROOF STATE]
proof (chain)
picking this:
Some (Node a v ts) \<in> set xs
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
[PROOF STEP]
have "distinct (bts_dfs val ts)"
[PROOF STATE]
proof (prove)
using this:
Some (Node a v ts) \<in> set xs
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)

goal (1 subgoal):
 1. distinct (bts_dfs val ts)
[PROOF STEP]
using dfs_distinct_member[of val xs "Node a v ts"]
[PROOF STATE]
proof (prove)
using this:
Some (Node a v ts) \<in> set xs
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
\<lbrakk>distinct (vals xs); Some (Node a v ts) \<in> set xs\<rbrakk> \<Longrightarrow> distinct (bt_dfs val (Node a v ts))

goal (1 subgoal):
 1. distinct (bts_dfs val ts)
[PROOF STEP]
by (simp add: bt_dfs_distinct_children)
[PROOF STATE]
proof (state)
this:
distinct (bts_dfs val ts)

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
hence "distinct (vals (map Some (rev ts)))"
[PROOF STATE]
proof (prove)
using this:
distinct (bts_dfs val ts)

goal (1 subgoal):
 1. distinct (vals (map Some (rev ts)))
[PROOF STEP]
by (simp add: bts_dfs_rev_distinct dfs_map_Some_idem)
[PROOF STATE]
proof (state)
this:
distinct (vals (map Some (rev ts)))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (vals (map Some (rev ts)))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
from assms IN
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
Some (Node a v ts) \<in> set xs
[PROOF STEP]
have "set (dfs val (map (match a) xs)) =
    set (dfs val xs) - set (bt_dfs val (Node a v ts))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
Some (Node a v ts) \<in> set xs

goal (1 subgoal):
 1. set (vals (map (match a) xs)) = set (vals xs) - set (bt_dfs val (Node a v ts))
[PROOF STEP]
by (simp add: dfs_match)
[PROOF STATE]
proof (state)
this:
set (vals (map (match a) xs)) = set (vals xs) - set (bt_dfs val (Node a v ts))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
hence "set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}"
[PROOF STATE]
proof (prove)
using this:
set (vals (map (match a) xs)) = set (vals xs) - set (bt_dfs val (Node a v ts))

goal (1 subgoal):
 1. set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}
[PROOF STEP]
by (auto simp add: dfs_map_Some_idem set_bts_dfs_rev)
[PROOF STATE]
proof (state)
this:
set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (map (match a) xs))
distinct (vals (map Some (rev ts)))
set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}
[PROOF STEP]
have "set (dfs alist (meld (map Some (rev ts)) (map (match a) xs))) =
    set (dfs alist (map Some (rev ts))) \<union> set (dfs alist (map (match a) xs))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals (map (match a) xs))
distinct (vals (map Some (rev ts)))
set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}

goal (1 subgoal):
 1. set (elements (meld (map Some (rev ts)) (map (match a) xs))) = set (elements (map Some (rev ts))) \<union> set (elements (map (match a) xs))
[PROOF STEP]
using alist_meld
[PROOF STATE]
proof (prove)
using this:
distinct (vals (map (match a) xs))
distinct (vals (map Some (rev ts)))
set (vals (map (match a) xs)) \<inter> set (vals (map Some (rev ts))) = {}
\<lbrakk>distinct (vals ?xs); distinct (vals ?ys); set (vals ?xs) \<inter> set (vals ?ys) = {}\<rbrakk> \<Longrightarrow> set (elements (meld ?xs ?ys)) = set (elements ?xs) \<union> set (elements ?ys)

goal (1 subgoal):
 1. set (elements (meld (map Some (rev ts)) (map (match a) xs))) = set (elements (map Some (rev ts))) \<union> set (elements (map (match a) xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (elements (meld (map Some (rev ts)) (map (match a) xs))) = set (elements (map Some (rev ts))) \<union> set (elements (map (match a) xs))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
with assms d IN nu
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
distinct (elements xs)
Some (Node a v ts) \<in> set xs
set (bts_dfs alist ts) \<union> (set (elements xs) - {(v, a)}) = set (elements xs) - {(v, a)}
set (elements (meld (map Some (rev ts)) (map (match a) xs))) = set (elements (map Some (rev ts))) \<union> set (elements (map (match a) xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (prios xs)
find_min xs = Some (Node a v ts)
distinct (elements xs)
Some (Node a v ts) \<in> set xs
set (bts_dfs alist ts) \<union> (set (elements xs) - {(v, a)}) = set (elements xs) - {(v, a)}
set (elements (meld (map Some (rev ts)) (map (match a) xs))) = set (elements (map Some (rev ts))) \<union> set (elements (map (match a) xs))

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
by (simp add: delete_min_def alist_normalize_idem set_bts_dfs_rev dfs_map_Some_idem
     dfs_match Diff_insert2 [of "set (dfs alist xs)" "(v,a)" "set (bts_dfs alist ts)"])
[PROOF STATE]
proof (state)
this:
set (elements (delete_min xs)) = set (elements xs) - {(v, a)}

goal:
No subgoals!
[PROOF STEP]
qed