[STATEMENT]
theorem unwinding_implies_NI_indirect_sources:
shows NI_indirect_sources
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
fix execs a n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
from iunwinding_implies_view_partitioned1
[PROOF STATE]
proof (chain)
picking this:
iview_partitioned
[PROOF STEP]
have vp: iview_partitioned
[PROOF STATE]
proof (prove)
using this:
iview_partitioned

goal (1 subgoal):
 1. iview_partitioned
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
iview_partitioned

goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
from vp and vpeq_reflexive
[PROOF STATE]
proof (chain)
picking this:
iview_partitioned
\<forall>a u. vpeq u a a
[PROOF STEP]
have 1: "\<forall> u . run n (Some s0) (ipurge_l execs u) \<parallel> run n (Some s0) (ipurge_r execs u)  \<rightharpoonup> (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)"
[PROOF STATE]
proof (prove)
using this:
iview_partitioned
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. \<forall>u. B2 (run n (Some s0) (ipurge_l execs u)) (run n (Some s0) (ipurge_r execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
unfolding iview_partitioned_def
[PROOF STATE]
proof (prove)
using this:
\<forall>execs ms mt n u. iequivalent_states ms mt u \<longrightarrow> B2 (run n ms (ipurge_l execs u)) (run n mt (ipurge_r execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
\<forall>a u. vpeq u a a

goal (1 subgoal):
 1. \<forall>u. B2 (run n (Some s0) (ipurge_l execs u)) (run n (Some s0) (ipurge_r execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u. B2 (run n (Some s0) (ipurge_l execs u)) (run n (Some s0) (ipurge_r execs u)) (\<lambda>rs rt. vpeq u rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
have "run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. run n (Some s0) (ipurge_l execs (current s_f))  \<parallel>
                                           run n (Some s0) (ipurge_r execs (current s_f)) \<rightharpoonup>
                                           (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
proof(cases "run n (Some s0) execs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. run n (Some s0) execs = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs = None

goal (2 subgoals):
 1. run n (Some s0) execs = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = None

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = None

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> B2 (run n (Some s0) (ipurge_l execs (current aa))) (run n (Some s0) (ipurge_r execs (current aa))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case (Some s_f)
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs = Some s_f

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) execs = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
proof(cases "run n (Some s0) (ipurge_l execs (current s_f))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = None\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
run n (Some s0) (ipurge_l execs (current s_f)) = None

goal (2 subgoals):
 1. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = None\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from Some this
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = None

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = None

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> B2 (run n (Some s0) (ipurge_l execs (current aa))) (run n (Some s0) (ipurge_r execs (current aa))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case (Some s_ipurge_l)
[PROOF STATE]
proof (state)
this:
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l

goal (1 subgoal):
 1. \<And>aa. \<lbrakk>run n (Some s0) execs = Some s_f; run n (Some s0) (ipurge_l execs (current s_f)) = Some aa\<rbrakk> \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
proof(cases "run n (Some s0) (ipurge_r execs (current s_f))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. run n (Some s0) (ipurge_r execs (current s_f)) = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
run n (Some s0) (ipurge_r execs (current s_f)) = None

goal (2 subgoals):
 1. run n (Some s0) (ipurge_r execs (current s_f)) = None \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
 2. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from \<open>run n (Some s0) execs = Some s_f\<close> Some this
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = None

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = None

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> B2 (run n (Some s0) (ipurge_l execs (current aa))) (run n (Some s0) (ipurge_r execs (current aa))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
case (Some s_ipurge_r)
[PROOF STATE]
proof (state)
this:
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from cswitch_independent_of_state
                \<open>run n (Some s0) execs = Some s_f\<close> \<open>run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l\<close>
                current_independent_of_domain_actions[where n=n and s="Some s0" and t="Some s0" and execs=execs and ?execs2.0="(ipurge_l execs (current s_f))"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>n s t. current s = current t \<longrightarrow> current (cswitch n s) = current (cswitch n t)
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
mcurrents (Some s0) (Some s0) \<Longrightarrow> mcurrents (run n (Some s0) execs) (run n (Some s0) (ipurge_l execs (current s_f)))
[PROOF STEP]
have 2: "current s_ipurge_l = current s_f"
[PROOF STATE]
proof (prove)
using this:
\<forall>n s t. current s = current t \<longrightarrow> current (cswitch n s) = current (cswitch n t)
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
mcurrents (Some s0) (Some s0) \<Longrightarrow> mcurrents (run n (Some s0) execs) (run n (Some s0) (ipurge_l execs (current s_f)))

goal (1 subgoal):
 1. current s_ipurge_l = current s_f
[PROOF STEP]
unfolding mcurrents_def B_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n s t. current s = current t \<longrightarrow> current (cswitch n s) = current (cswitch n t)
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
B2 (Some s0) (Some s0) (\<lambda>s t. current s = current t) \<Longrightarrow> B2 (run n (Some s0) execs) (run n (Some s0) (ipurge_l execs (current s_f))) (\<lambda>s t. current s = current t)

goal (1 subgoal):
 1. current s_ipurge_l = current s_f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
current s_ipurge_l = current s_f

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from \<open>run n (Some s0) execs = Some s_f\<close>  \<open>run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l\<close>
                Some 1[THEN spec,where x="current s_f"]
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r
B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>rs rt. vpeq (current s_f) rs rt \<and> current rs = current rt)
[PROOF STEP]
have "vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r"
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r
B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>rs rt. vpeq (current s_f) rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r
B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>rs rt. vpeq (current s_f) rs rt \<and> current rs = current rt)

goal (1 subgoal):
 1. vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from this 2
[PROOF STATE]
proof (chain)
picking this:
vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r
current s_ipurge_l = current s_f
[PROOF STEP]
have "output_f s_ipurge_l a = output_f s_ipurge_r a"
[PROOF STATE]
proof (prove)
using this:
vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r
current s_ipurge_l = current s_f

goal (1 subgoal):
 1. output_f s_ipurge_l a = output_f s_ipurge_r a
[PROOF STEP]
using output_consistent
[PROOF STATE]
proof (prove)
using this:
vpeq (current s_f) s_ipurge_l s_ipurge_r \<and> current s_ipurge_l = current s_ipurge_r
current s_ipurge_l = current s_f
\<forall>a s t. vpeq (current s) s t \<and> current s = current t \<longrightarrow> output_f s a = output_f t a

goal (1 subgoal):
 1. output_f s_ipurge_l a = output_f s_ipurge_r a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
output_f s_ipurge_l a = output_f s_ipurge_r a

goal (1 subgoal):
 1. \<And>aa. run n (Some s0) (ipurge_r execs (current s_f)) = Some aa \<Longrightarrow> run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
from \<open>run n (Some s0) execs = Some s_f\<close>  \<open>run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l\<close>
                this Some
[PROOF STATE]
proof (chain)
picking this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
output_f s_ipurge_l a = output_f s_ipurge_r a
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
output_f s_ipurge_l a = output_f s_ipurge_r a
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r

goal (1 subgoal):
 1. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
run n (Some s0) execs = Some s_f
run n (Some s0) (ipurge_l execs (current s_f)) = Some s_ipurge_l
output_f s_ipurge_l a = output_f s_ipurge_r a
run n (Some s0) (ipurge_r execs (current s_f)) = Some s_ipurge_r

goal (1 subgoal):
 1. case run n (Some s0) execs of None \<Rightarrow> True | Some aa \<Rightarrow> B2 (run n (Some s0) (ipurge_l execs (current aa))) (run n (Some s0) (ipurge_r execs (current aa))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))

goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. B2 (run ?n2 (Some s0) (ipurge_l ?execs2 (current s_f))) (run ?n2 (Some s0) (ipurge_r ?execs2 (current s_f))) (\<lambda>s_l s_r. output_f s_l ?a2 = output_f s_r ?a2))

goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. B2 (run ?n2 (Some s0) (ipurge_l ?execs2 (current s_f))) (run ?n2 (Some s0) (ipurge_r ?execs2 (current s_f))) (\<lambda>s_l s_r. output_f s_l ?a2 = output_f s_r ?a2))

goal (1 subgoal):
 1. NI_indirect_sources
[PROOF STEP]
unfolding NI_indirect_sources_def
[PROOF STATE]
proof (prove)
using this:
run ?n2 (Some s0) ?execs2 \<rightharpoonup> (\<lambda>s_f. B2 (run ?n2 (Some s0) (ipurge_l ?execs2 (current s_f))) (run ?n2 (Some s0) (ipurge_r ?execs2 (current s_f))) (\<lambda>s_l s_r. output_f s_l ?a2 = output_f s_r ?a2))

goal (1 subgoal):
 1. \<forall>execs a n. run n (Some s0) execs \<rightharpoonup> (\<lambda>s_f. B2 (run n (Some s0) (ipurge_l execs (current s_f))) (run n (Some s0) (ipurge_r execs (current s_f))) (\<lambda>s_l s_r. output_f s_l a = output_f s_r a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
NI_indirect_sources

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem unwinding_implies_isecure:
shows isecure
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isecure
[PROOF STEP]
using unwinding_implies_NI_indirect_sources  unwinding_implies_NI_unrelated
[PROOF STATE]
proof (prove)
using this:
NI_indirect_sources
NI_unrelated

goal (1 subgoal):
 1. isecure
[PROOF STEP]
unfolding isecure_def
[PROOF STATE]
proof (prove)
using this:
NI_indirect_sources
NI_unrelated

goal (1 subgoal):
 1. NI_indirect_sources \<and> NI_unrelated
[PROOF STEP]
by(auto)


[STATEMENT]
lemma bts_dfs_append [simp]:
  "bts_dfs f (ts @ rs) = bts_dfs f ts @ bts_dfs f rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bts_dfs f (ts @ rs) = bts_dfs f ts @ bts_dfs f rs
[PROOF STEP]
by (induct ts) simp_all


[STATEMENT]
lemma set_bts_dfs_rev:
  "set (bts_dfs f (rev ts)) = set (bts_dfs f ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (bts_dfs f (rev ts)) = set (bts_dfs f ts)
[PROOF STEP]
by (induct ts) auto


[STATEMENT]
lemma bts_dfs_rev_distinct:
  "distinct (bts_dfs f ts) \<Longrightarrow> distinct (bts_dfs f (rev ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (bts_dfs f ts) \<Longrightarrow> distinct (bts_dfs f (rev ts))
[PROOF STEP]
by (induct ts) (auto simp add: set_bts_dfs_rev)


[STATEMENT]
lemma bt_dfs_comp:
  "bt_dfs (f \<circ> g) t = map f (bt_dfs g t)"
  "bts_dfs (f \<circ> g) ts = map f (bts_dfs g ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bt_dfs (f \<circ> g) t = map f (bt_dfs g t) &&& bts_dfs (f \<circ> g) ts = map f (bts_dfs g ts)
[PROOF STEP]
by (induct t and ts rule: bt_dfs.induct bts_dfs.induct) simp_all


[STATEMENT]
lemma bt_dfs_comp_distinct:
  "distinct (bt_dfs (f \<circ> g) t) \<Longrightarrow> distinct (bt_dfs g t)"
  "distinct (bts_dfs (f \<circ> g) ts) \<Longrightarrow> distinct (bts_dfs g ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (bt_dfs (f \<circ> g) t) \<Longrightarrow> distinct (bt_dfs g t)) &&& (distinct (bts_dfs (f \<circ> g) ts) \<Longrightarrow> distinct (bts_dfs g ts))
[PROOF STEP]
by (simp_all add: bt_dfs_comp distinct_map [of f])


[STATEMENT]
lemma bt_dfs_distinct_children:
  "distinct (bt_dfs f x) \<Longrightarrow> distinct (bts_dfs f (children x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (bt_dfs f x) \<Longrightarrow> distinct (bts_dfs f (children x))
[PROOF STEP]
by (cases x) simp


[STATEMENT]
lemma dfs_append:
  "dfs f (xs @ ys) = (dfs f xs) @ (dfs f ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs f (xs @ ys) = dfs f xs @ dfs f ys
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma set_dfs_rev:
  "set (dfs f (rev xs)) = set (dfs f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (dfs f (rev xs)) = set (dfs f xs)
[PROOF STEP]
by (induct xs) (auto simp add: dfs_append)


[STATEMENT]
lemma set_dfs_Cons:
  "set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])
[PROOF STEP]
have "set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))
[PROOF STEP]
using set_dfs_rev[of f "rev xs @ [x]"]
[PROOF STATE]
proof (prove)
using this:
set (dfs f (rev (rev xs @ [x]))) = set (dfs f (rev xs @ [x]))

goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))

goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))

goal (1 subgoal):
 1. set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])
[PROOF STEP]
by (simp add: dfs_append set_dfs_rev)
[PROOF STATE]
proof (state)
this:
set (dfs f (x # xs)) = set (dfs f xs) \<union> set (dfs f [x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dfs_comp:
  "dfs (f \<circ> g) xs = map f (dfs g xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs (f \<circ> g) xs = map f (dfs g xs)
[PROOF STEP]
by (induct xs) (simp_all add: bt_dfs_comp del: o_apply)


[STATEMENT]
lemma dfs_comp_distinct:
  "distinct (dfs (f \<circ> g) xs) \<Longrightarrow> distinct (dfs g xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (dfs (f \<circ> g) xs) \<Longrightarrow> distinct (dfs g xs)
[PROOF STEP]
by (simp add: dfs_comp distinct_map[of f])


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

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

goal (1 subgoal):
 1. distinct (bt_dfs f t)
[PROOF STEP]
by (cases "t = r") simp_all
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs f t)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct (dfs f []); Some x \<in> set []\<rbrakk> \<Longrightarrow> distinct (bt_dfs f x)
 2. \<And>xs x. \<lbrakk>\<And>x. \<lbrakk>distinct (dfs f xs); Some x \<in> set xs\<rbrakk> \<Longrightarrow> distinct (bt_dfs f x); distinct (dfs f (None # xs)); Some x \<in> set (None # xs)\<rbrakk> \<Longrightarrow> distinct (bt_dfs f x)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dfs_map_Some_idem:
  "dfs f (map Some xs) = bts_dfs f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs f (map Some xs) = bts_dfs f xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma alist_split_pre:
  "val t = (fst \<circ> alist) t"
  "priority t = (snd \<circ> alist) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val t = (fst \<circ> alist) t &&& priority t = (snd \<circ> alist) t
[PROOF STEP]
by (cases t, simp)+


[STATEMENT]
lemma alist_split:
  "val = fst \<circ> alist"
  "priority = snd \<circ> alist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val = fst \<circ> alist &&& priority = snd \<circ> alist
[PROOF STEP]
by (auto intro!: ext simp add: alist_split_pre)


[STATEMENT]
lemma alist_split_set:
  "set (dfs val xs) = fst ` set (dfs alist xs)"
  "set (dfs priority xs) = snd ` set (dfs alist xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (dfs val xs) = fst ` set (dfs alist xs) &&& set (dfs priority xs) = snd ` set (dfs alist xs)
[PROOF STEP]
by (auto simp add: dfs_comp alist_split)


[STATEMENT]
lemma in_set_in_alist:
  assumes "Some t \<in> set xs"
  shows "(val t, priority t) \<in> set (dfs alist xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (val t, priority t) \<in> set (dfs alist xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Some t \<in> set xs

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

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

goal (1 subgoal):
 1. (val t, priority t) \<in> set (dfs alist (Some x # xs))
[PROOF STEP]
proof (cases "Some t \<in> set xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (Some x # xs); Some t \<in> set xs\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (Some x # xs))
 2. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (Some x # xs); Some t \<notin> set xs\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (Some x # xs))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Some t \<notin> set xs

goal (2 subgoals):
 1. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (Some x # xs); Some t \<in> set xs\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (Some x # xs))
 2. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (Some x # xs); Some t \<notin> set xs\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (Some x # xs))
[PROOF STEP]
with Some
[PROOF STATE]
proof (chain)
picking this:
Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs)
Some t \<in> set (Some x # xs)
Some t \<notin> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs)
Some t \<in> set (Some x # xs)
Some t \<notin> set xs

goal (1 subgoal):
 1. (val t, priority t) \<in> set (dfs alist (Some x # xs))
[PROOF STEP]
by (cases t) (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
(val t, priority t) \<in> set (dfs alist (Some x # xs))

goal (1 subgoal):
 1. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (Some x # xs); Some t \<in> set xs\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (Some x # xs))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(val t, priority t) \<in> set (dfs alist (Some x # xs))

goal (2 subgoals):
 1. Some t \<in> set [] \<Longrightarrow> (val t, priority t) \<in> set (dfs alist [])
 2. \<And>xs. \<lbrakk>Some t \<in> set xs \<Longrightarrow> (val t, priority t) \<in> set (dfs alist xs); Some t \<in> set (None # xs)\<rbrakk> \<Longrightarrow> (val t, priority t) \<in> set (dfs alist (None # xs))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma bts_augment [simp]:
  "bts_augment = fold bt_augment"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bts_augment = fold bt_augment
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bts_augment x = fold bt_augment x
[PROOF STEP]
fix ts :: "('a, 'b) bintree list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bts_augment x = fold bt_augment x
[PROOF STEP]
show "bts_augment ts = fold bt_augment ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bts_augment ts = fold bt_augment ts
[PROOF STEP]
by (induct ts) simp_all
[PROOF STATE]
proof (state)
this:
bts_augment ts = fold bt_augment ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bt_augment_Node [simp]:
  "bt_augment (Node a v ts) q = PQ.push v a (fold bt_augment ts q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bt_augment (Node a v ts) q = PQ.push v a (fold bt_augment ts q)
[PROOF STEP]
by (simp add: bts_augment)


[STATEMENT]
lemma bt_augment_simp:
  "bt_augment t q = PQ.push (val t) (priority t) (fold bt_augment (children t) q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bt_augment t q = PQ.push (val t) (priority t) (fold bt_augment (children t) q)
[PROOF STEP]
by (cases t) (simp_all add: bts_augment)


[STATEMENT]
lemma bt_augment_v_subset:
  "set |q| \<subseteq> set |bt_augment t q|"
  "set |q| \<subseteq> set |bts_augment ts q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |q| \<subseteq> set |bt_augment t q| &&& set |q| \<subseteq> set |bts_augment ts q|
[PROOF STEP]
by (induct t and ts arbitrary: q and q rule: bt_augment.induct bts_augment.induct) auto


[STATEMENT]
lemma bt_augment_v_in:
  "v \<in> set |q| \<Longrightarrow> v \<in> set |bt_augment t q|"
  "v \<in> set |q| \<Longrightarrow> v \<in> set |bts_augment ts q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> set |q| \<Longrightarrow> v \<in> set |bt_augment t q|) &&& (v \<in> set |q| \<Longrightarrow> v \<in> set |bts_augment ts q|)
[PROOF STEP]
using bt_augment_v_subset[of q]
[PROOF STATE]
proof (prove)
using this:
set |q| \<subseteq> set |bt_augment ?t q|
set |q| \<subseteq> set |bts_augment ?ts q|

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


[STATEMENT]
lemma bt_augment_v_union:
  "set |bt_augment t (bt_augment r q)| =
    set |bt_augment t q| \<union> set |bt_augment r q|"
  "set |bts_augment ts (bt_augment r q)| =
    set |bts_augment ts q| \<union> set |bt_augment r q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t (bt_augment r q)| = set |bt_augment t q| \<union> set |bt_augment r q| &&& set |bts_augment ts (bt_augment r q)| = set |bts_augment ts q| \<union> set |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. (\<And>q r. set |bts_augment x3 (bt_augment r q)| = set |bts_augment x3 q| \<union> set |bt_augment r q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bt_augment r q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bt_augment r q|
 2. \<And>q r. set |bts_augment [] (bt_augment r q)| = set |bts_augment [] q| \<union> set |bt_augment r q|
 3. \<And>x1 x2 q r. \<lbrakk>\<And>q r. set |bt_augment x1 (bt_augment r q)| = set |bt_augment x1 q| \<union> set |bt_augment r q|; \<And>q r. set |bts_augment x2 (bt_augment r q)| = set |bts_augment x2 q| \<union> set |bt_augment r q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bt_augment r q)| = set |bts_augment (x1 # x2) q| \<union> set |bt_augment r q|
[PROOF STEP]
case Nil_bintree
[PROOF STATE]
proof (state)
this:

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

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

goal (2 subgoals):
 1. \<And>x1 x2 x3 q r. (\<And>q r. set |bts_augment x3 (bt_augment r q)| = set |bts_augment x3 q| \<union> set |bt_augment r q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bt_augment r q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bt_augment r q|
 2. \<And>x1 x2 q r. \<lbrakk>\<And>q r. set |bt_augment x1 (bt_augment r q)| = set |bt_augment x1 q| \<union> set |bt_augment r q|; \<And>q r. set |bts_augment x2 (bt_augment r q)| = set |bts_augment x2 q| \<union> set |bt_augment r q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bt_augment r q)| = set |bts_augment (x1 # x2) q| \<union> set |bt_augment r q|
[PROOF STEP]
qed auto


[STATEMENT]
lemma bt_val_augment:
  shows "set (bt_dfs val t) \<union> set |q| = set |bt_augment t q|"
  and   "set (bts_dfs val ts) \<union> set |q| = set |bts_augment ts q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (bt_dfs val t) \<union> set |q| = set |bt_augment t q| &&& set (bts_dfs val ts) \<union> set |q| = set |bts_augment ts q|
[PROOF STEP]
proof (induct t and ts rule: bt_augment.induct bts_augment.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2 x3. set (bts_dfs val x3) \<union> set |q| = set |bts_augment x3 q| \<Longrightarrow> set (bt_dfs val (Node x1 x2 x3)) \<union> set |q| = set |bt_augment (Node x1 x2 x3) q|
 2. set (bts_dfs val []) \<union> set |q| = set |bts_augment [] q|
 3. \<And>x1 x2. \<lbrakk>set (bt_dfs val x1) \<union> set |q| = set |bt_augment x1 q|; set (bts_dfs val x2) \<union> set |q| = set |bts_augment x2 q|\<rbrakk> \<Longrightarrow> set (bts_dfs val (x1 # x2)) \<union> set |q| = set |bts_augment (x1 # x2) q|
[PROOF STEP]
case (Cons_bintree r rs)
[PROOF STATE]
proof (state)
this:
set (bt_dfs val r) \<union> set |q| = set |bt_augment r q|
set (bts_dfs val rs) \<union> set |q| = set |bts_augment rs q|

goal (3 subgoals):
 1. \<And>x1 x2 x3. set (bts_dfs val x3) \<union> set |q| = set |bts_augment x3 q| \<Longrightarrow> set (bt_dfs val (Node x1 x2 x3)) \<union> set |q| = set |bt_augment (Node x1 x2 x3) q|
 2. set (bts_dfs val []) \<union> set |q| = set |bts_augment [] q|
 3. \<And>x1 x2. \<lbrakk>set (bt_dfs val x1) \<union> set |q| = set |bt_augment x1 q|; set (bts_dfs val x2) \<union> set |q| = set |bts_augment x2 q|\<rbrakk> \<Longrightarrow> set (bts_dfs val (x1 # x2)) \<union> set |q| = set |bts_augment (x1 # x2) q|
[PROOF STEP]
have "set |bts_augment rs (bt_augment r q)| =
    set |bts_augment rs q| \<union> set |bt_augment r q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q|
[PROOF STEP]
by (simp only: bt_augment_v_union)
[PROOF STATE]
proof (state)
this:
set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q|

goal (3 subgoals):
 1. \<And>x1 x2 x3. set (bts_dfs val x3) \<union> set |q| = set |bts_augment x3 q| \<Longrightarrow> set (bt_dfs val (Node x1 x2 x3)) \<union> set |q| = set |bt_augment (Node x1 x2 x3) q|
 2. set (bts_dfs val []) \<union> set |q| = set |bts_augment [] q|
 3. \<And>x1 x2. \<lbrakk>set (bt_dfs val x1) \<union> set |q| = set |bt_augment x1 q|; set (bts_dfs val x2) \<union> set |q| = set |bts_augment x2 q|\<rbrakk> \<Longrightarrow> set (bts_dfs val (x1 # x2)) \<union> set |q| = set |bts_augment (x1 # x2) q|
[PROOF STEP]
with bt_augment_v_subset[of q]
[PROOF STATE]
proof (chain)
picking this:
set |q| \<subseteq> set |bt_augment ?t q|
set |q| \<subseteq> set |bts_augment ?ts q|
set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q|
[PROOF STEP]
have "set |bts_augment rs (bt_augment r q)| =
      set |bts_augment rs q| \<union> set |bt_augment r q| \<union> set |q|"
[PROOF STATE]
proof (prove)
using this:
set |q| \<subseteq> set |bt_augment ?t q|
set |q| \<subseteq> set |bts_augment ?ts q|
set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q|

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

goal (3 subgoals):
 1. \<And>x1 x2 x3. set (bts_dfs val x3) \<union> set |q| = set |bts_augment x3 q| \<Longrightarrow> set (bt_dfs val (Node x1 x2 x3)) \<union> set |q| = set |bt_augment (Node x1 x2 x3) q|
 2. set (bts_dfs val []) \<union> set |q| = set |bts_augment [] q|
 3. \<And>x1 x2. \<lbrakk>set (bt_dfs val x1) \<union> set |q| = set |bt_augment x1 q|; set (bts_dfs val x2) \<union> set |q| = set |bts_augment x2 q|\<rbrakk> \<Longrightarrow> set (bts_dfs val (x1 # x2)) \<union> set |q| = set |bts_augment (x1 # x2) q|
[PROOF STEP]
with Cons_bintree
[PROOF STATE]
proof (chain)
picking this:
set (bt_dfs val r) \<union> set |q| = set |bt_augment r q|
set (bts_dfs val rs) \<union> set |q| = set |bts_augment rs q|
set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q| \<union> set |q|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (bt_dfs val r) \<union> set |q| = set |bt_augment r q|
set (bts_dfs val rs) \<union> set |q| = set |bts_augment rs q|
set |bts_augment rs (bt_augment r q)| = set |bts_augment rs q| \<union> set |bt_augment r q| \<union> set |q|

goal (1 subgoal):
 1. set (bts_dfs val (r # rs)) \<union> set |q| = set |bts_augment (r # rs) q|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (bts_dfs val (r # rs)) \<union> set |q| = set |bts_augment (r # rs) q|

goal (2 subgoals):
 1. \<And>x1 x2 x3. set (bts_dfs val x3) \<union> set |q| = set |bts_augment x3 q| \<Longrightarrow> set (bt_dfs val (Node x1 x2 x3)) \<union> set |q| = set |bt_augment (Node x1 x2 x3) q|
 2. set (bts_dfs val []) \<union> set |q| = set |bts_augment [] q|
[PROOF STEP]
qed auto


[STATEMENT]
lemma vals_pqueue:
  "set (vals xs) = set |pqueue xs|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vals xs) = set |pqueue xs|
[PROOF STEP]
by (induct xs) (simp_all add: bt_val_augment)


[STATEMENT]
lemma bt_augment_v_push:
  "set |bt_augment t (PQ.push v a q)| = set |bt_augment t q| \<union> {v}"
  "set |bts_augment ts (PQ.push v a q)| = set |bts_augment ts q| \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t (PQ.push v a q)| = set |bt_augment t q| \<union> {v} &&& set |bts_augment ts (PQ.push v a q)| = set |bts_augment ts q| \<union> {v}
[PROOF STEP]
using bt_val_augment[where q = "PQ.push v a q"]
[PROOF STATE]
proof (prove)
using this:
set (bt_dfs val ?t) \<union> set |PQ.push v a q| = set |bt_augment ?t (PQ.push v a q)|
set (bts_dfs val ?ts) \<union> set |PQ.push v a q| = set |bts_augment ?ts (PQ.push v a q)|

goal (1 subgoal):
 1. set |bt_augment t (PQ.push v a q)| = set |bt_augment t q| \<union> {v} &&& set |bts_augment ts (PQ.push v a q)| = set |bts_augment ts q| \<union> {v}
[PROOF STEP]
by (simp_all add: bt_val_augment)


[STATEMENT]
lemma bt_augment_v_push_commute:
  "set |bt_augment t (PQ.push v a q)| = set |PQ.push v a (bt_augment t q)|"
  "set |bts_augment ts (PQ.push v a q)| = set |PQ.push v a (bts_augment ts q)|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t (PQ.push v a q)| = set |PQ.push v a (bt_augment t q)| &&& set |bts_augment ts (PQ.push v a q)| = set |PQ.push v a (bts_augment ts q)|
[PROOF STEP]
by (simp_all add: bt_augment_v_push del: bts_augment)


[STATEMENT]
lemma bts_augment_v_union:
  "set |bt_augment t (bts_augment rs q)| =
    set |bt_augment t q| \<union> set |bts_augment rs q|"
  "set |bts_augment ts (bts_augment rs q)| =
    set |bts_augment ts q| \<union> set |bts_augment rs q|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t (bts_augment rs q)| = set |bt_augment t q| \<union> set |bts_augment rs q| &&& set |bts_augment ts (bts_augment rs q)| = set |bts_augment ts q| \<union> set |bts_augment rs q|
[PROOF STEP]
proof (induct t and ts arbitrary: q rs and q rs rule: bt_augment.induct bts_augment.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>q rs. set |bts_augment [] (bts_augment rs q)| = set |bts_augment [] q| \<union> set |bts_augment rs q|
 3. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
case Nil_bintree
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>q rs. set |bts_augment [] (bts_augment rs q)| = set |bts_augment [] q| \<union> set |bts_augment rs q|
 3. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
from bt_augment_v_subset[of q]
[PROOF STATE]
proof (chain)
picking this:
set |q| \<subseteq> set |bt_augment ?t q|
set |q| \<subseteq> set |bts_augment ?ts q|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set |q| \<subseteq> set |bt_augment ?t q|
set |q| \<subseteq> set |bts_augment ?ts q|

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

goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
case (Cons_bintree x xs)
[PROOF STATE]
proof (state)
this:
set |bt_augment x (bts_augment ?rs ?q)| = set |bt_augment x ?q| \<union> set |bts_augment ?rs ?q|
set |bts_augment xs (bts_augment ?rs ?q)| = set |bts_augment xs ?q| \<union> set |bts_augment ?rs ?q|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
let ?L = "set |bts_augment xs (bt_augment x (bts_augment rs q))|"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
from bt_augment_v_union
[PROOF STATE]
proof (chain)
picking this:
set |bt_augment ?t (bt_augment ?r ?q)| = set |bt_augment ?t ?q| \<union> set |bt_augment ?r ?q|
set |bts_augment ?ts (bt_augment ?r ?q)| = set |bts_augment ?ts ?q| \<union> set |bt_augment ?r ?q|
[PROOF STEP]
have *: "\<And> q. set |bts_augment xs (bt_augment x q)| =
      set |bts_augment xs q| \<union> set |bt_augment x q|"
[PROOF STATE]
proof (prove)
using this:
set |bt_augment ?t (bt_augment ?r ?q)| = set |bt_augment ?t ?q| \<union> set |bt_augment ?r ?q|
set |bts_augment ?ts (bt_augment ?r ?q)| = set |bts_augment ?ts ?q| \<union> set |bt_augment ?r ?q|

goal (1 subgoal):
 1. \<And>q. set |bts_augment xs (bt_augment x q)| = set |bts_augment xs q| \<union> set |bt_augment x q|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set |bts_augment xs (bt_augment x ?q)| = set |bts_augment xs ?q| \<union> set |bt_augment x ?q|

goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
with Cons_bintree
[PROOF STATE]
proof (chain)
picking this:
set |bt_augment x (bts_augment ?rs ?q)| = set |bt_augment x ?q| \<union> set |bts_augment ?rs ?q|
set |bts_augment xs (bts_augment ?rs ?q)| = set |bts_augment xs ?q| \<union> set |bts_augment ?rs ?q|
set |bts_augment xs (bt_augment x ?q)| = set |bts_augment xs ?q| \<union> set |bt_augment x ?q|
[PROOF STEP]
have "?L =
      set |bts_augment xs q| \<union> set |bts_augment rs q| \<union> set |bt_augment x q|"
[PROOF STATE]
proof (prove)
using this:
set |bt_augment x (bts_augment ?rs ?q)| = set |bt_augment x ?q| \<union> set |bts_augment ?rs ?q|
set |bts_augment xs (bts_augment ?rs ?q)| = set |bts_augment xs ?q| \<union> set |bts_augment ?rs ?q|
set |bts_augment xs (bt_augment x ?q)| = set |bts_augment xs ?q| \<union> set |bt_augment x ?q|

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

goal (2 subgoals):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
 2. \<And>x1 x2 q rs. \<lbrakk>\<And>q rs. set |bt_augment x1 (bts_augment rs q)| = set |bt_augment x1 q| \<union> set |bts_augment rs q|; \<And>q rs. set |bts_augment x2 (bts_augment rs q)| = set |bts_augment x2 q| \<union> set |bts_augment rs q|\<rbrakk> \<Longrightarrow> set |bts_augment (x1 # x2) (bts_augment rs q)| = set |bts_augment (x1 # x2) q| \<union> set |bts_augment rs q|
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
set |bts_augment xs (bt_augment x ?q)| = set |bts_augment xs ?q| \<union> set |bt_augment x ?q|
set |bts_augment xs (bt_augment x (bts_augment rs q))| = set |bts_augment xs q| \<union> set |bts_augment rs q| \<union> set |bt_augment x q|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set |bts_augment xs (bt_augment x ?q)| = set |bts_augment xs ?q| \<union> set |bt_augment x ?q|
set |bts_augment xs (bt_augment x (bts_augment rs q))| = set |bts_augment xs q| \<union> set |bts_augment rs q| \<union> set |bt_augment x q|

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

goal (1 subgoal):
 1. \<And>x1 x2 x3 q rs. (\<And>q rs. set |bts_augment x3 (bts_augment rs q)| = set |bts_augment x3 q| \<union> set |bts_augment rs q|) \<Longrightarrow> set |bt_augment (Node x1 x2 x3) (bts_augment rs q)| = set |bt_augment (Node x1 x2 x3) q| \<union> set |bts_augment rs q|
[PROOF STEP]
qed simp


[STATEMENT]
lemma bt_augment_v_commute:
  "set |bt_augment t (bt_augment r q)| = set |bt_augment r (bt_augment t q)|"
  "set |bt_augment t (bts_augment rs q)| = set |bts_augment rs (bt_augment t q)|"
  "set |bts_augment ts (bts_augment rs q)| =
    set |bts_augment rs (bts_augment ts q)|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t (bt_augment r q)| = set |bt_augment r (bt_augment t q)| &&& set |bt_augment t (bts_augment rs q)| = set |bts_augment rs (bt_augment t q)| &&& set |bts_augment ts (bts_augment rs q)| = set |bts_augment rs (bts_augment ts q)|
[PROOF STEP]
unfolding bts_augment_v_union bt_augment_v_union
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment t q| \<union> set |bt_augment r q| = set |bt_augment r q| \<union> set |bt_augment t q| &&& set |bt_augment t q| \<union> set |bts_augment rs q| = set |bts_augment rs q| \<union> set |bt_augment t q| &&& set |bts_augment ts q| \<union> set |bts_augment rs q| = set |bts_augment rs q| \<union> set |bts_augment ts q|
[PROOF STEP]
by auto


[STATEMENT]
lemma bt_augment_v_merge:
  "set |bt_augment (merge t r) q| = set |bt_augment t (bt_augment r q)|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set |bt_augment (merge t r) q| = set |bt_augment t (bt_augment r q)|
[PROOF STEP]
by (simp add: bt_augment_simp [symmetric] bt_augment_v_push
    bt_augment_v_commute merge_def)


[STATEMENT]
lemma vals_merge [simp]:
  "set (bt_dfs val (merge t r)) = set (bt_dfs val t) \<union> set (bt_dfs val r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (bt_dfs val (merge t r)) = set (bt_dfs val t) \<union> set (bt_dfs val r)
[PROOF STEP]
by (auto simp add: bt_dfs_simp merge_def)


[STATEMENT]
lemma vals_merge_distinct:
  "distinct (bt_dfs val t) \<Longrightarrow> distinct (bt_dfs val r) \<Longrightarrow>
   set (bt_dfs val t) \<inter> set (bt_dfs val r) = {} \<Longrightarrow>
   distinct (bt_dfs val (merge t r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (bt_dfs val t); distinct (bt_dfs val r); set (bt_dfs val t) \<inter> set (bt_dfs val r) = {}\<rbrakk> \<Longrightarrow> distinct (bt_dfs val (merge t r))
[PROOF STEP]
by (auto simp add: bt_dfs_simp merge_def)


[STATEMENT]
lemma vals_add_Cons:
  "set (vals (add x xs)) = set (vals (x # xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vals (add x xs)) = set (vals (x # xs))
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = None \<Longrightarrow> set (vals (add x xs)) = set (vals (x # xs))
 2. \<And>a. x = Some a \<Longrightarrow> set (vals (add x xs)) = set (vals (x # xs))
[PROOF STEP]
case (Some t)
[PROOF STATE]
proof (state)
this:
x = Some t

goal (2 subgoals):
 1. x = None \<Longrightarrow> set (vals (add x xs)) = set (vals (x # xs))
 2. \<And>a. x = Some a \<Longrightarrow> set (vals (add x xs)) = set (vals (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Some t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Some t

goal (1 subgoal):
 1. set (vals (add x xs)) = set (vals (x # xs))
[PROOF STEP]
by (induct xs arbitrary: x t) auto
[PROOF STATE]
proof (state)
this:
set (vals (add x xs)) = set (vals (x # xs))

goal (1 subgoal):
 1. x = None \<Longrightarrow> set (vals (add x xs)) = set (vals (x # xs))
[PROOF STEP]
qed simp


[STATEMENT]
lemma vals_add_distinct:
  assumes "distinct (vals xs)"
  and "distinct (dfs val [x])"
  and "set (vals xs) \<inter> set (dfs val [x]) = {}"
  shows "distinct (vals (add x xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (vals (add x xs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
distinct (vals [x])
set (vals xs) \<inter> set (vals [x]) = {}

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

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

goal (1 subgoal):
 1. distinct (vals (add x xs))
[PROOF STEP]
proof (induct xs arbitrary: x t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x t. \<lbrakk>distinct (vals []); distinct (vals [x]); set (vals []) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x []))
 2. \<And>xs x t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (None # xs)); distinct (vals [x]); set (vals (None # xs)) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x (None # xs)))
 3. \<And>x xs xa t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (Some x # xs)); distinct (vals [xa]); set (vals (Some x # xs)) \<inter> set (vals [xa]) = {}; xa = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add xa (Some x # xs)))
[PROOF STEP]
case (Some r xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t

goal (3 subgoals):
 1. \<And>x t. \<lbrakk>distinct (vals []); distinct (vals [x]); set (vals []) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x []))
 2. \<And>xs x t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (None # xs)); distinct (vals [x]); set (vals (None # xs)) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x (None # xs)))
 3. \<And>x xs xa t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (Some x # xs)); distinct (vals [xa]); set (vals (Some x # xs)) \<inter> set (vals [xa]) = {}; xa = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add xa (Some x # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t
[PROOF STEP]
have "set (bt_dfs val t) \<inter> set (bt_dfs val r) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t

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

goal (3 subgoals):
 1. \<And>x t. \<lbrakk>distinct (vals []); distinct (vals [x]); set (vals []) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x []))
 2. \<And>xs x t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (None # xs)); distinct (vals [x]); set (vals (None # xs)) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x (None # xs)))
 3. \<And>x xs xa t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (Some x # xs)); distinct (vals [xa]); set (vals (Some x # xs)) \<inter> set (vals [xa]) = {}; xa = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add xa (Some x # xs)))
[PROOF STEP]
with Some
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t
set (bt_dfs val t) \<inter> set (bt_dfs val r) = {}
[PROOF STEP]
have "distinct (bt_dfs val (merge t r))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t
set (bt_dfs val t) \<inter> set (bt_dfs val r) = {}

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

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

goal (3 subgoals):
 1. \<And>x t. \<lbrakk>distinct (vals []); distinct (vals [x]); set (vals []) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x []))
 2. \<And>xs x t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (None # xs)); distinct (vals [x]); set (vals (None # xs)) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x (None # xs)))
 3. \<And>x xs xa t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (Some x # xs)); distinct (vals [xa]); set (vals (Some x # xs)) \<inter> set (vals [xa]) = {}; xa = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add xa (Some x # xs)))
[PROOF STEP]
with Some
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t
distinct (bt_dfs val (merge t r))
[PROOF STEP]
have "set (vals xs) \<inter> set (bt_dfs val (merge t r)) = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (vals xs); distinct (vals [?x]); set (vals xs) \<inter> set (vals [?x]) = {}; ?x = Some ?t\<rbrakk> \<Longrightarrow> distinct (vals (add ?x xs))
distinct (vals (Some r # xs))
distinct (vals [x])
set (vals (Some r # xs)) \<inter> set (vals [x]) = {}
x = Some t
distinct (bt_dfs val (merge t r))

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

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

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

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

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

goal (2 subgoals):
 1. \<And>x t. \<lbrakk>distinct (vals []); distinct (vals [x]); set (vals []) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x []))
 2. \<And>xs x t. \<lbrakk>\<And>x t. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x xs)); distinct (vals (None # xs)); distinct (vals [x]); set (vals (None # xs)) \<inter> set (vals [x]) = {}; x = Some t\<rbrakk> \<Longrightarrow> distinct (vals (add x (None # xs)))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
distinct (vals (add x xs))

goal (1 subgoal):
 1. \<lbrakk>distinct (vals xs); distinct (vals [x]); set (vals xs) \<inter> set (vals [x]) = {}; x = None\<rbrakk> \<Longrightarrow> distinct (vals (add x xs))
[PROOF STEP]
qed simp


[STATEMENT]
lemma vals_insert [simp]:
  "set (vals (insert a v xs)) = set (vals xs) \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vals (Binomial_Queue.insert a v xs)) = set (vals xs) \<union> {v}
[PROOF STEP]
by (simp add: insert_def vals_add_Cons)


[STATEMENT]
lemma insert_v_push:
  "set (vals (insert a v xs)) = set |PQ.push v a (pqueue xs)|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vals (Binomial_Queue.insert a v xs)) = set |PQ.push v a (pqueue xs)|
[PROOF STEP]
by (simp add: vals_pqueue[symmetric])


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

goal (5 subgoals):
 1. \<And>ys. set (vals (meld [] ys)) = set (vals []) \<union> set (vals ys)
 2. \<And>xs. set (vals (meld xs [])) = set (vals xs) \<union> set (vals [])
 3. \<And>xs y ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (None # xs) (y # ys))) = set (vals (None # xs)) \<union> set (vals (y # ys))
 4. \<And>x xs ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (x # xs) (None # ys))) = set (vals (x # xs)) \<union> set (vals (None # ys))
 5. \<And>t xs r ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (Some t # xs) (Some r # ys))) = set (vals (Some t # xs)) \<union> set (vals (Some r # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)

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

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

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

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

goal (4 subgoals):
 1. \<And>ys. set (vals (meld [] ys)) = set (vals []) \<union> set (vals ys)
 2. \<And>xs. set (vals (meld xs [])) = set (vals xs) \<union> set (vals [])
 3. \<And>x xs ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (x # xs) (None # ys))) = set (vals (x # xs)) \<union> set (vals (None # ys))
 4. \<And>t xs r ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (Some t # xs) (Some r # ys))) = set (vals (Some t # xs)) \<union> set (vals (Some r # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)

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

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

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

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

goal (3 subgoals):
 1. \<And>ys. set (vals (meld [] ys)) = set (vals []) \<union> set (vals ys)
 2. \<And>xs. set (vals (meld xs [])) = set (vals xs) \<union> set (vals [])
 3. \<And>t xs r ys. set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys) \<Longrightarrow> set (vals (meld (Some t # xs) (Some r # ys))) = set (vals (Some t # xs)) \<union> set (vals (Some r # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (vals (meld xs ys)) = set (vals xs) \<union> set (vals ys)

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

goal (2 subgoals):
 1. \<And>ys. set (vals (meld [] ys)) = set (vals []) \<union> set (vals ys)
 2. \<And>xs. set (vals (meld xs [])) = set (vals xs) \<union> set (vals [])
[PROOF STEP]
qed simp_all