[STATEMENT]
lemma vals_meld_distinct:
  "distinct (dfs val xs) \<Longrightarrow> distinct (dfs val ys) \<Longrightarrow>
   set (dfs val xs) \<inter> set (dfs val ys) = {} \<Longrightarrow>
   distinct (dfs val (meld xs 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> distinct (vals (meld xs 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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>xs y ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
 4. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (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> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (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> distinct (vals (meld xs 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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>xs y ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
 4. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (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> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}

goal (1 subgoal):
 1. distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
proof (cases y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = None\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
 2. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
y = None

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = None\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
 2. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
with "3"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
y = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
y = None

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
case (Some t)
[PROOF STATE]
proof (state)
this:
y = Some t

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
from "3"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
[PROOF STEP]
have A: "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> distinct (vals (meld xs 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> distinct (vals (meld xs 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. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (None # xs)); distinct (vals (y # ys)); set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}; y = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
with "3" Some
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
y = Some t
set (bt_dfs val t) \<inter> set (vals (meld xs ys)) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (None # xs))
distinct (vals (y # ys))
set (vals (None # xs)) \<inter> set (vals (y # ys)) = {}
y = Some t
set (bt_dfs val t) \<inter> set (vals (meld xs ys)) = {}

goal (1 subgoal):
 1. distinct (vals (meld (None # xs) (y # ys)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (vals (meld (None # xs) (y # ys)))

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

goal (4 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (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> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (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> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (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> distinct (vals (meld xs 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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>x xs ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (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> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}

goal (1 subgoal):
 1. distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = None\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
 2. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
x = None

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = None\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
 2. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
with "4"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
x = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
x = None

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

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
from "4"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs 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> distinct (vals (meld xs 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> distinct (vals (meld xs 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. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (x # xs)); distinct (vals (None # ys)); set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}; x = Some a\<rbrakk> \<Longrightarrow> distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
with "4" Some
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
x = Some t
set (bt_dfs val t) \<inter> set (vals (meld xs ys)) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (x # xs))
distinct (vals (None # ys))
set (vals (x # xs)) \<inter> set (vals (None # ys)) = {}
x = Some t
set (bt_dfs val t) \<inter> set (vals (meld xs ys)) = {}

goal (1 subgoal):
 1. distinct (vals (meld (x # xs) (None # ys)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (vals (meld (x # xs) (None # ys)))

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

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (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> distinct (vals (meld xs 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> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs 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 (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> distinct (vals (meld xs 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 (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
by (auto simp add: set_dfs_Cons)
[PROOF STATE]
proof (state)
this:
set (vals xs) \<inter> set (vals ys) = {}

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
with "5"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys))
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
set (vals xs) \<inter> set (vals ys) = {}
[PROOF STEP]
have "distinct (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> distinct (vals (meld xs ys))
distinct (vals (Some x # xs))
distinct (vals (Some y # ys))
set (vals (Some x # xs)) \<inter> set (vals (Some y # ys)) = {}
set (vals xs) \<inter> set (vals ys) = {}

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

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

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
from "5"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs 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 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> distinct (vals (meld xs 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
[PROOF STATE]
proof (state)
this:
set (bt_dfs val x) \<inter> set (bt_dfs val y) = {}

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
with "5"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs 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> distinct (vals (meld xs 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 (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val (merge x y))

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>distinct (vals []); distinct (vals ys); set (vals []) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld [] ys))
 2. \<And>xs. \<lbrakk>distinct (vals xs); distinct (vals []); set (vals xs) \<inter> set (vals []) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs []))
 3. \<And>t xs r ys. \<lbrakk>\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs ys)); distinct (vals (Some t # xs)); distinct (vals (Some r # ys)); set (vals (Some t # xs)) \<inter> set (vals (Some r # ys)) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld (Some t # xs) (Some r # ys)))
[PROOF STEP]
from "5"
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals ys); set (vals xs) \<inter> set (vals ys) = {}\<rbrakk> \<Longrightarrow> distinct (vals (meld xs 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 (vals (meld xs ys)) \<inter> set (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> distinct (vals (meld xs 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 (vals (meld xs ys)) \<inter> set (bt_dfs val (merge x y)) = {}
[PROOF STEP]
by (auto simp add: vals_meld)
[PROOF STATE]
proof (state)
this:
set (vals (meld xs ys)) \<inter> set (bt_dfs val (merge x y)) = {}

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

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

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


[STATEMENT]
lemma bt_augment_alist_subset:
  "set (PQ.alist_of q) \<subseteq> set (PQ.alist_of (bt_augment t q))"
  "set (PQ.alist_of q) \<subseteq> set (PQ.alist_of (bts_augment ts q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment t q)) &&& set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment ts q))
[PROOF STEP]
proof (induct t and ts arbitrary: q and q rule: bt_augment.induct bts_augment.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2 x3 q. (\<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment x3 q))) \<Longrightarrow> set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment (Node x1 x2 x3) q))
 2. \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment [] q))
 3. \<And>x1 x2 q. \<lbrakk>\<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment x1 q)); \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment x2 q))\<rbrakk> \<Longrightarrow> set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
case (Node a v rs)
[PROOF STATE]
proof (state)
this:
set (pq.alist_of ?q) \<subseteq> set (pq.alist_of (bts_augment rs ?q))

goal (3 subgoals):
 1. \<And>x1 x2 x3 q. (\<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment x3 q))) \<Longrightarrow> set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment (Node x1 x2 x3) q))
 2. \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment [] q))
 3. \<And>x1 x2 q. \<lbrakk>\<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment x1 q)); \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment x2 q))\<rbrakk> \<Longrightarrow> set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment (Node a v rs) q))
[PROOF STEP]
using Node[of q]
[PROOF STATE]
proof (prove)
using this:
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment rs q))

goal (1 subgoal):
 1. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment (Node a v rs) q))
[PROOF STEP]
by (auto simp add: bt_augment_simp set_insort_key)
[PROOF STATE]
proof (state)
this:
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment (Node a v rs) q))

goal (2 subgoals):
 1. \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment [] q))
 2. \<And>x1 x2 q. \<lbrakk>\<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment x1 q)); \<And>q. set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment x2 q))\<rbrakk> \<Longrightarrow> set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
qed auto


[STATEMENT]
lemma bt_augment_alist_in:
  "(v,a) \<in> set (PQ.alist_of q) \<Longrightarrow> (v,a) \<in> set (PQ.alist_of (bt_augment t q))"
  "(v,a) \<in> set (PQ.alist_of q) \<Longrightarrow> (v,a) \<in> set (PQ.alist_of (bts_augment ts q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v, a) \<in> set (pq.alist_of q) \<Longrightarrow> (v, a) \<in> set (pq.alist_of (bt_augment t q))) &&& ((v, a) \<in> set (pq.alist_of q) \<Longrightarrow> (v, a) \<in> set (pq.alist_of (bts_augment ts q)))
[PROOF STEP]
using bt_augment_alist_subset[of q]
[PROOF STATE]
proof (prove)
using this:
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment ?t q))
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment ?ts q))

goal (1 subgoal):
 1. ((v, a) \<in> set (pq.alist_of q) \<Longrightarrow> (v, a) \<in> set (pq.alist_of (bt_augment t q))) &&& ((v, a) \<in> set (pq.alist_of q) \<Longrightarrow> (v, a) \<in> set (pq.alist_of (bts_augment ts q)))
[PROOF STEP]
by auto


[STATEMENT]
lemma bt_augment_alist_union:
  "distinct (bts_dfs val (r # [t])) \<Longrightarrow>
   set (bts_dfs val (r # [t])) \<inter> set |q| = {} \<Longrightarrow>
   set (PQ.alist_of (bt_augment t (bt_augment r q))) =
     set (PQ.alist_of (bt_augment t q)) \<union> set (PQ.alist_of (bt_augment r q))"

  "distinct (bts_dfs val (r # ts)) \<Longrightarrow>
   set (bts_dfs val (r # ts)) \<inter> set |q| = {} \<Longrightarrow>
   set (PQ.alist_of (bts_augment ts (bt_augment r q))) =
     set (PQ.alist_of (bts_augment ts q)) \<union> set (PQ.alist_of (bt_augment r q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>distinct (bts_dfs val [r, t]); set (bts_dfs val [r, t]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment t (bt_augment r q))) = set (pq.alist_of (bt_augment t q)) \<union> set (pq.alist_of (bt_augment r q))) &&& (\<lbrakk>distinct (bts_dfs val (r # ts)); set (bts_dfs val (r # ts)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment ts (bt_augment r q))) = set (pq.alist_of (bts_augment ts q)) \<union> set (pq.alist_of (bt_augment r q)))
[PROOF STEP]
proof (induct t and ts arbitrary: q r and q r rule: bt_augment.induct bts_augment.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>q r. \<lbrakk>distinct (bts_dfs val [r]); set (bts_dfs val [r]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment [] (bt_augment r q))) = set (pq.alist_of (bts_augment [] q)) \<union> set (pq.alist_of (bt_augment r q))
 3. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
case Nil_bintree
[PROOF STATE]
proof (state)
this:
distinct (bts_dfs val [r])
set (bts_dfs val [r]) \<inter> set |q| = {}

goal (3 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>q r. \<lbrakk>distinct (bts_dfs val [r]); set (bts_dfs val [r]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment [] (bt_augment r q))) = set (pq.alist_of (bts_augment [] q)) \<union> set (pq.alist_of (bt_augment r q))
 3. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
from bt_augment_alist_subset[of q]
[PROOF STATE]
proof (chain)
picking this:
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment ?t q))
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment ?ts q))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bt_augment ?t q))
set (pq.alist_of q) \<subseteq> set (pq.alist_of (bts_augment ?ts q))

goal (1 subgoal):
 1. set (pq.alist_of (bts_augment [] (bt_augment r q))) = set (pq.alist_of (bts_augment [] q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (bts_augment [] (bt_augment r q))) = set (pq.alist_of (bts_augment [] q)) \<union> set (pq.alist_of (bt_augment r q))

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
case (Node a v rs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (bts_dfs val (?r # rs)); set (bts_dfs val (?r # rs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment rs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment rs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bts_dfs val (?r # rs)); set (bts_dfs val (?r # rs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment rs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment rs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}
[PROOF STEP]
have
    "set (PQ.alist_of (bts_augment rs (bt_augment r q))) =
     set (PQ.alist_of (bts_augment rs q)) \<union> set (PQ.alist_of (bt_augment r q))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val (?r # rs)); set (bts_dfs val (?r # rs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment rs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment rs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}

goal (1 subgoal):
 1. set (pq.alist_of (bts_augment rs (bt_augment r q))) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (bts_augment rs (bt_augment r q))) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (bts_augment rs (bt_augment r q))) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
from Node.prems
[PROOF STATE]
proof (chain)
picking this:
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}
[PROOF STEP]
have *: "v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|"
[PROOF STATE]
proof (prove)
using this:
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}

goal (1 subgoal):
 1. v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|
[PROOF STEP]
unfolding bt_val_augment[symmetric]
[PROOF STATE]
proof (prove)
using this:
distinct (bts_dfs val [r, Node a v rs])
set (bts_dfs val [r, Node a v rs]) \<inter> set |q| = {}

goal (1 subgoal):
 1. v \<notin> set (bts_dfs val rs) \<union> set |q| \<union> (set (bt_dfs val r) \<union> set |q|)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
hence "v \<notin> set |bts_augment rs (bt_augment r q)|"
[PROOF STATE]
proof (prove)
using this:
v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|

goal (1 subgoal):
 1. v \<notin> set |bts_augment rs (bt_augment r q)|
[PROOF STEP]
by (unfold bt_augment_v_union)
[PROOF STATE]
proof (state)
this:
v \<notin> set |bts_augment rs (bt_augment r q)|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<notin> set |bts_augment rs (bt_augment r q)|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|
[PROOF STEP]
have "v \<notin> set |bts_augment rs q|"
[PROOF STATE]
proof (prove)
using this:
v \<notin> set |bts_augment rs q| \<union> set |bt_augment r q|

goal (1 subgoal):
 1. v \<notin> set |bts_augment rs q|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<notin> set |bts_augment rs q|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val (r # x3)); set (bts_dfs val (r # x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x3 (bt_augment r q))) = set (pq.alist_of (bts_augment x3 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val [r, Node x1 x2 x3]); set (bts_dfs val [r, Node x1 x2 x3]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment (Node x1 x2 x3) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q)) \<union> set (pq.alist_of (bt_augment r q))
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (pq.alist_of (bts_augment rs (bt_augment r q))) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))
v \<notin> set |bts_augment rs (bt_augment r q)|
v \<notin> set |bts_augment rs q|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (pq.alist_of (bts_augment rs (bt_augment r q))) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))
v \<notin> set |bts_augment rs (bt_augment r q)|
v \<notin> set |bts_augment rs q|

goal (1 subgoal):
 1. set (pq.alist_of (bt_augment (Node a v rs) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node a v rs) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
by (simp add: set_insort_key)
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (bt_augment (Node a v rs) (bt_augment r q))) = set (pq.alist_of (bt_augment (Node a v rs) q)) \<union> set (pq.alist_of (bt_augment r q))

goal (1 subgoal):
 1. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
case (Cons_bintree x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (r # x # xs))
set (bts_dfs val (r # x # xs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (r # x # xs))
set (bts_dfs val (r # x # xs)) \<inter> set |q| = {}
[PROOF STEP]
have \<comment> \<open>FIXME: ugly... and slow\<close>
    "distinct (bts_dfs val (x # xs))" and
    "distinct (bts_dfs val (r # xs))" and
    "distinct (bts_dfs val [r,x])" and
    "set (bts_dfs val (x # xs)) \<inter> set |bt_augment r q| = {}" and
    "set (bts_dfs val (x # xs)) \<inter> set |q| = {}" and
    "set (bts_dfs val [r, x]) \<inter> set |q| = {}" and
    "set (bts_dfs val (r # xs)) \<inter> set |q| = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (r # x # xs))
set (bts_dfs val (r # x # xs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. (distinct (bts_dfs val (x # xs)) &&& distinct (bts_dfs val (r # xs)) &&& distinct (bts_dfs val [r, x])) &&& (set (bts_dfs val (x # xs)) \<inter> set |bt_augment r q| = {} &&& set (bts_dfs val (x # xs)) \<inter> set |q| = {}) &&& set (bts_dfs val [r, x]) \<inter> set |q| = {} &&& set (bts_dfs val (r # xs)) \<inter> set |q| = {}
[PROOF STEP]
unfolding bt_val_augment[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (r # x # xs))
set (bts_dfs val (r # x # xs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. (distinct (bts_dfs val (x # xs)) &&& distinct (bts_dfs val (r # xs)) &&& distinct (bts_dfs val [r, x])) &&& (set (bts_dfs val (x # xs)) \<inter> (set (bt_dfs val r) \<union> set |q|) = {} &&& set (bts_dfs val (x # xs)) \<inter> set |q| = {}) &&& set (bts_dfs val [r, x]) \<inter> set |q| = {} &&& set (bts_dfs val (r # xs)) \<inter> set |q| = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (bts_dfs val (x # xs))
distinct (bts_dfs val (r # xs))
distinct (bts_dfs val [r, x])
set (bts_dfs val (x # xs)) \<inter> set |bt_augment r q| = {}
set (bts_dfs val (x # xs)) \<inter> set |q| = {}
set (bts_dfs val [r, x]) \<inter> set |q| = {}
set (bts_dfs val (r # xs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. \<And>x1 x2 q r. \<lbrakk>\<And>q r. \<lbrakk>distinct (bts_dfs val [r, x1]); set (bts_dfs val [r, x1]) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x1 (bt_augment r q))) = set (pq.alist_of (bt_augment x1 q)) \<union> set (pq.alist_of (bt_augment r q)); \<And>q r. \<lbrakk>distinct (bts_dfs val (r # x2)); set (bts_dfs val (r # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment x2 (bt_augment r q))) = set (pq.alist_of (bts_augment x2 q)) \<union> set (pq.alist_of (bt_augment r q)); distinct (bts_dfs val (r # x1 # x2)); set (bts_dfs val (r # x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment (x1 # x2) (bt_augment r q))) = set (pq.alist_of (bts_augment (x1 # x2) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
with Cons_bintree.hyps
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (x # xs))
distinct (bts_dfs val (r # xs))
distinct (bts_dfs val [r, x])
set (bts_dfs val (x # xs)) \<inter> set |bt_augment r q| = {}
set (bts_dfs val (x # xs)) \<inter> set |q| = {}
set (bts_dfs val [r, x]) \<inter> set |q| = {}
set (bts_dfs val (r # xs)) \<inter> set |q| = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val [?r, x]); set (bts_dfs val [?r, x]) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bt_augment x (bt_augment ?r ?q))) = set (pq.alist_of (bt_augment x ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
\<lbrakk>distinct (bts_dfs val (?r # xs)); set (bts_dfs val (?r # xs)) \<inter> set |?q| = {}\<rbrakk> \<Longrightarrow> set (pq.alist_of (bts_augment xs (bt_augment ?r ?q))) = set (pq.alist_of (bts_augment xs ?q)) \<union> set (pq.alist_of (bt_augment ?r ?q))
distinct (bts_dfs val (x # xs))
distinct (bts_dfs val (r # xs))
distinct (bts_dfs val [r, x])
set (bts_dfs val (x # xs)) \<inter> set |bt_augment r q| = {}
set (bts_dfs val (x # xs)) \<inter> set |q| = {}
set (bts_dfs val [r, x]) \<inter> set |q| = {}
set (bts_dfs val (r # xs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. set (pq.alist_of (bts_augment (x # xs) (bt_augment r q))) = set (pq.alist_of (bts_augment (x # xs) q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (bts_augment (x # xs) (bt_augment r q))) = set (pq.alist_of (bts_augment (x # xs) q)) \<union> set (pq.alist_of (bt_augment r q))

goal:
No subgoals!
[PROOF STEP]
qed