[STATEMENT]
lemma bt_alist_augment:
  "distinct (bt_dfs val t) \<Longrightarrow>
   set (bt_dfs val t) \<inter> set |q| = {} \<Longrightarrow>
   set (bt_dfs alist t) \<union> set (PQ.alist_of q) = set (PQ.alist_of (bt_augment t q))"

  "distinct (bts_dfs val ts) \<Longrightarrow>
   set (bts_dfs val ts) \<inter> set |q| = {} \<Longrightarrow>
   set (bts_dfs alist ts) \<union> set (PQ.alist_of q) =
     set (PQ.alist_of (bts_augment ts q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>distinct (bt_dfs val t); set (bt_dfs val t) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist t) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment t q))) &&& (\<lbrakk>distinct (bts_dfs val ts); set (bts_dfs val ts) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist ts) \<union> set (pq.alist_of q) = set (pq.alist_of (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. \<lbrakk>\<lbrakk>distinct (bts_dfs val x3); set (bts_dfs val x3) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x3) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x3 q)); distinct (bt_dfs val (Node x1 x2 x3)); set (bt_dfs val (Node x1 x2 x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist (Node x1 x2 x3)) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q))
 2. \<lbrakk>distinct (bts_dfs val []); set (bts_dfs val []) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist []) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment [] q))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk>distinct (bt_dfs val x1); set (bt_dfs val x1) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist x1) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment x1 q)); \<lbrakk>distinct (bts_dfs val x2); set (bts_dfs val x2) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x2) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x2 q)); distinct (bts_dfs val (x1 # x2)); set (bts_dfs val (x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist (x1 # x2)) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
case Nil_bintree
[PROOF STATE]
proof (state)
this:
distinct (bts_dfs val [])
set (bts_dfs val []) \<inter> set |q| = {}

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

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

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

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

goal (1 subgoal):
 1. v \<notin> set |bts_augment rs q|
[PROOF STEP]
unfolding bt_val_augment[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bt_dfs val (Node a v rs))
set (bt_dfs val (Node a v rs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. v \<notin> set (bts_dfs val rs) \<union> set |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. \<lbrakk>\<lbrakk>distinct (bts_dfs val x3); set (bts_dfs val x3) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x3) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x3 q)); distinct (bt_dfs val (Node x1 x2 x3)); set (bt_dfs val (Node x1 x2 x3)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist (Node x1 x2 x3)) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment (Node x1 x2 x3) q))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk>distinct (bt_dfs val x1); set (bt_dfs val x1) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist x1) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment x1 q)); \<lbrakk>distinct (bts_dfs val x2); set (bts_dfs val x2) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x2) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x2 q)); distinct (bts_dfs val (x1 # x2)); set (bts_dfs val (x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist (x1 # x2)) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
with Node
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bt_dfs val (Node a v rs))
set (bt_dfs val (Node a v rs)) \<inter> set |q| = {}
v \<notin> set |bts_augment rs q|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bt_dfs val (Node a v rs))
set (bt_dfs val (Node a v rs)) \<inter> set |q| = {}
v \<notin> set |bts_augment rs q|

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

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

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>distinct (bt_dfs val x1); set (bt_dfs val x1) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist x1) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment x1 q)); \<lbrakk>distinct (bts_dfs val x2); set (bts_dfs val x2) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x2) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x2 q)); distinct (bts_dfs val (x1 # x2)); set (bts_dfs val (x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist (x1 # x2)) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bt_dfs val r); set (bt_dfs val r) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist r) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment r q))
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bts_dfs val (r # rs))
set (bts_dfs val (r # rs)) \<inter> set |q| = {}
[PROOF STEP]
have "set (PQ.alist_of (bts_augment (r # rs) 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 (bt_dfs val r); set (bt_dfs val r) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist r) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment r q))
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bts_dfs val (r # rs))
set (bts_dfs val (r # rs)) \<inter> set |q| = {}

goal (1 subgoal):
 1. set (pq.alist_of (bts_augment (r # rs) q)) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
using bt_augment_alist_union
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bt_dfs val r); set (bt_dfs val r) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist r) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment r q))
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bts_dfs val (r # rs))
set (bts_dfs val (r # rs)) \<inter> set |q| = {}
\<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))

goal (1 subgoal):
 1. set (pq.alist_of (bts_augment (r # rs) 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 (r # rs) q)) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk>distinct (bt_dfs val x1); set (bt_dfs val x1) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist x1) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment x1 q)); \<lbrakk>distinct (bts_dfs val x2); set (bts_dfs val x2) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist x2) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment x2 q)); distinct (bts_dfs val (x1 # x2)); set (bts_dfs val (x1 # x2)) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist (x1 # x2)) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment (x1 # x2) q))
[PROOF STEP]
with Cons_bintree bt_augment_alist_subset
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (bt_dfs val r); set (bt_dfs val r) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist r) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment r q))
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bts_dfs val (r # rs))
set (bts_dfs val (r # rs)) \<inter> set |q| = {}
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))
set (pq.alist_of (bts_augment (r # rs) q)) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (bt_dfs val r); set (bt_dfs val r) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bt_dfs alist r) \<union> set (pq.alist_of q) = set (pq.alist_of (bt_augment r q))
\<lbrakk>distinct (bts_dfs val rs); set (bts_dfs val rs) \<inter> set |q| = {}\<rbrakk> \<Longrightarrow> set (bts_dfs alist rs) \<union> set (pq.alist_of q) = set (pq.alist_of (bts_augment rs q))
distinct (bts_dfs val (r # rs))
set (bts_dfs val (r # rs)) \<inter> set |q| = {}
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))
set (pq.alist_of (bts_augment (r # rs) q)) = set (pq.alist_of (bts_augment rs q)) \<union> set (pq.alist_of (bt_augment r q))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alist_pqueue:
  "distinct (vals xs) \<Longrightarrow> set (dfs alist xs) = set (PQ.alist_of (pqueue xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (vals xs) \<Longrightarrow> set (elements xs) = set (pq.alist_of (pqueue xs))
[PROOF STEP]
by (induct xs) (simp_all add: vals_pqueue bt_alist_augment)


[STATEMENT]
lemma alist_pqueue_priority:
  "distinct (vals xs) \<Longrightarrow> (v, a) \<in> set (dfs alist xs)
    \<Longrightarrow> PQ.priority (pqueue xs) v = Some a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (vals xs); (v, a) \<in> set (elements xs)\<rbrakk> \<Longrightarrow> PQ.priority (pqueue xs) v = Some a
[PROOF STEP]
by (simp add: alist_pqueue PQ.priority_def)


[STATEMENT]
lemma prios_pqueue:
  "distinct (vals xs) \<Longrightarrow> set (prios xs) = set \<parallel>pqueue xs\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (vals xs) \<Longrightarrow> set (prios xs) = set \<parallel>pqueue xs\<parallel>
[PROOF STEP]
by (auto simp add: alist_pqueue priorities_set alist_split_set)


[STATEMENT]
lemma alist_merge [simp]:
  "distinct (bt_dfs val t) \<Longrightarrow> distinct (bt_dfs val r) \<Longrightarrow>
   set (bt_dfs val t) \<inter> set (bt_dfs val r) = {} \<Longrightarrow>
   set (bt_dfs alist (merge t r)) = set (bt_dfs alist t) \<union> set (bt_dfs alist 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> set (bt_dfs alist (merge t r)) = set (bt_dfs alist t) \<union> set (bt_dfs alist r)
[PROOF STEP]
by (auto simp add: bt_dfs_simp merge_def alist_split)


[STATEMENT]
lemma alist_add_Cons:
  assumes "distinct (vals (x#xs))"
  shows "set (dfs alist (add x xs)) = set (dfs alist (x # xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (add x xs)) = set (elements (x # xs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (vals (x # xs))

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

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

goal (1 subgoal):
 1. set (elements (add x [])) = set (elements [x])
[PROOF STEP]
by (cases x) simp_all
[PROOF STATE]
proof (state)
this:
set (elements (add x [])) = set (elements [x])

goal (2 subgoals):
 1. \<And>xs x. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (x # None # xs))\<rbrakk> \<Longrightarrow> set (elements (add x (None # xs))) = set (elements (x # None # xs))
 2. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs x. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (x # None # xs))\<rbrakk> \<Longrightarrow> set (elements (add x (None # xs))) = set (elements (x # None # xs))
 2. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
distinct (vals (?x # xs_)) \<Longrightarrow> set (elements (add ?x xs_)) = set (elements (?x # xs_))
distinct (vals (x # None # xs_))

goal (2 subgoals):
 1. \<And>xs x. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (x # None # xs))\<rbrakk> \<Longrightarrow> set (elements (add x (None # xs))) = set (elements (x # None # xs))
 2. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (?x # xs_)) \<Longrightarrow> set (elements (add ?x xs_)) = set (elements (?x # xs_))
distinct (vals (x # None # xs_))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (vals (?x # xs_)) \<Longrightarrow> set (elements (add ?x xs_)) = set (elements (?x # xs_))
distinct (vals (x # None # xs_))

goal (1 subgoal):
 1. set (elements (add x (None # xs_))) = set (elements (x # None # xs_))
[PROOF STEP]
by (cases x) simp_all
[PROOF STATE]
proof (state)
this:
set (elements (add x (None # xs_))) = set (elements (x # None # xs_))

goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
case (Some y ys)
[PROOF STATE]
proof (state)
this:
distinct (vals (?x # ys)) \<Longrightarrow> set (elements (add ?x ys)) = set (elements (?x # ys))
distinct (vals (x # Some y # ys))

goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. distinct (vals (x # xs)) \<Longrightarrow> set (elements (add x xs)) = set (elements (x # xs)); distinct (vals (xa # Some x # xs))\<rbrakk> \<Longrightarrow> set (elements (add xa (Some x # xs))) = set (elements (xa # Some x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (?x # ys)) \<Longrightarrow> set (elements (add ?x ys)) = set (elements (?x # ys))
distinct (vals (x # Some y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (vals (?x # ys)) \<Longrightarrow> set (elements (add ?x ys)) = set (elements (?x # ys))
distinct (vals (x # Some y # ys))

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

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
note prem = Some.prems Some
[PROOF STATE]
proof (state)
this:
distinct (vals (x # Some y # ys))
x = Some t

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
from prem
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (x # Some y # ys))
x = Some t
[PROOF STEP]
have "distinct (bt_dfs val (merge t y))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals (x # Some y # ys))
x = Some t

goal (1 subgoal):
 1. distinct (bt_dfs val (merge t y))
[PROOF STEP]
by (auto simp add: bt_dfs_simp merge_def)
[PROOF STATE]
proof (state)
this:
distinct (bt_dfs val (merge t y))

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
with prem
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (x # Some y # ys))
x = Some t
distinct (bt_dfs val (merge t y))
[PROOF STEP]
have "distinct (vals (Some (merge t y) # ys))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals (x # Some y # ys))
x = Some t
distinct (bt_dfs val (merge t y))

goal (1 subgoal):
 1. distinct (vals (Some (merge t y) # ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (vals (Some (merge t y) # ys))

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
with prem Some.hyps
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (x # Some y # ys))
x = Some t
distinct (vals (?x # ys)) \<Longrightarrow> set (elements (add ?x ys)) = set (elements (?x # ys))
distinct (vals (Some (merge t y) # ys))
[PROOF STEP]
have "set (dfs alist (add (Some (merge t y)) ys)) =
        set (dfs alist (Some (merge t y) # ys))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals (x # Some y # ys))
x = Some t
distinct (vals (?x # ys)) \<Longrightarrow> set (elements (add ?x ys)) = set (elements (?x # ys))
distinct (vals (Some (merge t y) # ys))

goal (1 subgoal):
 1. set (elements (add (Some (merge t y)) ys)) = set (elements (Some (merge t y) # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (add (Some (merge t y)) ys)) = set (elements (Some (merge t y) # ys))

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (elements (add (Some (merge t y)) ys)) = set (elements (Some (merge t y) # ys))

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

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

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
with prem
[PROOF STATE]
proof (chain)
picking this:
distinct (vals (x # Some y # ys))
x = Some t
set (bt_dfs val t) \<inter> set (bt_dfs val y) = {}
[PROOF STEP]
have "set (bt_dfs alist (merge t y)) =
        set (bt_dfs alist t) \<union> set (bt_dfs alist y)"
[PROOF STATE]
proof (prove)
using this:
distinct (vals (x # Some y # ys))
x = Some t
set (bt_dfs val t) \<inter> set (bt_dfs val y) = {}

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

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (bt_dfs alist (merge t y)) = set (bt_dfs alist t) \<union> set (bt_dfs alist y)

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
note prem and Un_assoc
[PROOF STATE]
proof (state)
this:
distinct (vals (x # Some y # ys))
x = Some t
?A \<union> ?B \<union> ?C = ?A \<union> (?B \<union> ?C)

goal (2 subgoals):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
 2. \<And>a. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = Some a\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (elements (add (Some (merge t y)) ys)) = set (elements (Some (merge t y) # ys))
set (bt_dfs alist (merge t y)) = set (bt_dfs alist t) \<union> set (bt_dfs alist y)
distinct (vals (x # Some y # ys))
x = Some t
?A \<union> ?B \<union> ?C = ?A \<union> (?B \<union> ?C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (elements (add (Some (merge t y)) ys)) = set (elements (Some (merge t y) # ys))
set (bt_dfs alist (merge t y)) = set (bt_dfs alist t) \<union> set (bt_dfs alist y)
distinct (vals (x # Some y # ys))
x = Some t
?A \<union> ?B \<union> ?C = ?A \<union> (?B \<union> ?C)

goal (1 subgoal):
 1. set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))

goal (1 subgoal):
 1. \<lbrakk>\<And>x. distinct (vals (x # ys)) \<Longrightarrow> set (elements (add x ys)) = set (elements (x # ys)); distinct (vals (x # Some y # ys)); x = None\<rbrakk> \<Longrightarrow> set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
set (elements (add x (Some y # ys))) = set (elements (x # Some y # ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alist_insert [simp]:
  "distinct (vals xs) \<Longrightarrow>
   v \<notin> set (vals xs) \<Longrightarrow>
   set (dfs alist (insert a v xs)) = set (dfs alist xs) \<union> {(v,a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (vals xs); v \<notin> set (vals xs)\<rbrakk> \<Longrightarrow> set (elements (Binomial_Queue.insert a v xs)) = set (elements xs) \<union> {(v, a)}
[PROOF STEP]
by (simp add: insert_def alist_add_Cons)


[STATEMENT]
lemma insert_push:
  "distinct (vals xs) \<Longrightarrow>
   v \<notin> set (vals xs) \<Longrightarrow>
   set (dfs alist (insert a v xs)) = set (PQ.alist_of (PQ.push v a (pqueue xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (vals xs); v \<notin> set (vals xs)\<rbrakk> \<Longrightarrow> set (elements (Binomial_Queue.insert a v xs)) = set (pq.alist_of (PQ.push v a (pqueue xs)))
[PROOF STEP]
by (simp add: alist_pqueue vals_pqueue set_insort_key)


[STATEMENT]
lemma insert_p_push:
  assumes "distinct (vals xs)"
  and "v \<notin> set (vals xs)"
  shows "set (prios (insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (prios (Binomial_Queue.insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (prios (Binomial_Queue.insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
v \<notin> set (vals xs)
[PROOF STEP]
have "set (dfs alist (insert a v xs)) =
      set (PQ.alist_of (PQ.push v a (pqueue xs)))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
v \<notin> set (vals xs)

goal (1 subgoal):
 1. set (elements (Binomial_Queue.insert a v xs)) = set (pq.alist_of (PQ.push v a (pqueue xs)))
[PROOF STEP]
by (rule insert_push)
[PROOF STATE]
proof (state)
this:
set (elements (Binomial_Queue.insert a v xs)) = set (pq.alist_of (PQ.push v a (pqueue xs)))

goal (1 subgoal):
 1. set (prios (Binomial_Queue.insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (elements (Binomial_Queue.insert a v xs)) = set (pq.alist_of (PQ.push v a (pqueue xs)))

goal (1 subgoal):
 1. set (prios (Binomial_Queue.insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>
[PROOF STEP]
by (simp add: alist_split_set priorities_set)
[PROOF STATE]
proof (state)
this:
set (prios (Binomial_Queue.insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_empty:
  "normalized xs \<Longrightarrow> xs = empty \<longleftrightarrow> PQ.is_empty (pqueue xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized xs \<Longrightarrow> (xs = []) = PQ.is_empty (pqueue xs)
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>normalized xs; xs = []\<rbrakk> \<Longrightarrow> PQ.is_empty (pqueue xs)
 2. \<lbrakk>normalized xs; PQ.is_empty (pqueue xs)\<rbrakk> \<Longrightarrow> xs = []
[PROOF STEP]
assume "xs = []"
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. \<lbrakk>normalized xs; xs = []\<rbrakk> \<Longrightarrow> PQ.is_empty (pqueue xs)
 2. \<lbrakk>normalized xs; PQ.is_empty (pqueue xs)\<rbrakk> \<Longrightarrow> xs = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
show "PQ.is_empty (pqueue xs)"
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. PQ.is_empty (pqueue xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. \<lbrakk>normalized xs; PQ.is_empty (pqueue xs)\<rbrakk> \<Longrightarrow> xs = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>normalized xs; PQ.is_empty (pqueue xs)\<rbrakk> \<Longrightarrow> xs = []
[PROOF STEP]
assume N: "normalized xs" and E: "PQ.is_empty (pqueue xs)"
[PROOF STATE]
proof (state)
this:
normalized xs
PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. \<lbrakk>normalized xs; PQ.is_empty (pqueue xs)\<rbrakk> \<Longrightarrow> xs = []
[PROOF STEP]
show "xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = []
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "xs \<noteq> []"
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
with N
[PROOF STATE]
proof (chain)
picking this:
normalized xs
xs \<noteq> []
[PROOF STEP]
have "set (vals xs) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
normalized xs
xs \<noteq> []

goal (1 subgoal):
 1. set (vals xs) \<noteq> {}
[PROOF STEP]
by (induct xs) (simp_all add: bt_dfs_simp dfs_append)
[PROOF STATE]
proof (state)
this:
set (vals xs) \<noteq> {}

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
hence "set |pqueue xs| \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
set (vals xs) \<noteq> {}

goal (1 subgoal):
 1. set |pqueue xs| \<noteq> {}
[PROOF STEP]
by (simp add: vals_pqueue)
[PROOF STATE]
proof (state)
this:
set |pqueue xs| \<noteq> {}

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set |pqueue xs| \<noteq> {}

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
from E
[PROOF STATE]
proof (chain)
picking this:
PQ.is_empty (pqueue xs)
[PROOF STEP]
have "set |pqueue xs| = {}"
[PROOF STATE]
proof (prove)
using this:
PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. set |pqueue xs| = {}
[PROOF STEP]
by (simp add: is_empty_empty)
[PROOF STATE]
proof (state)
this:
set |pqueue xs| = {}

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set |pqueue xs| \<noteq> {}
set |pqueue xs| = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
set |pqueue xs| \<noteq> {}
set |pqueue xs| = {}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bt_dfs_Min_priority:
  assumes "is_heap t"
  shows "priority t = Min (set (bt_dfs priority t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. priority t = Min (set (bt_dfs priority t))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_heap_list (priority t) (children t)

goal (1 subgoal):
 1. priority t = Min (set (bt_dfs priority t))
[PROOF STEP]
proof (induct "priority t" "children t" arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. [] = children t \<Longrightarrow> priority t = Min (set (bt_dfs priority t))
 2. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
case is_heap_list_Nil
[PROOF STATE]
proof (state)
this:
[] = children t

goal (2 subgoals):
 1. \<And>t. [] = children t \<Longrightarrow> priority t = Min (set (bt_dfs priority t))
 2. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] = children t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] = children t

goal (1 subgoal):
 1. priority t = Min (set (bt_dfs priority t))
[PROOF STEP]
by (simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
priority t = Min (set (bt_dfs priority t))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
case (is_heap_list_Cons rs r t)
[PROOF STATE]
proof (state)
this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
note cons = this
[PROOF STATE]
proof (state)
this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
let ?M = "Min (set (bt_dfs priority t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
obtain t' where "t' = Node (priority t) (val t) rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'. t' = Node (priority t) (val t) rs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t' = Node (priority t) (val t) rs

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
hence ot: "rs = children t'" "priority t' = priority t"
[PROOF STATE]
proof (prove)
using this:
t' = Node (priority t) (val t) rs

goal (1 subgoal):
 1. rs = children t' &&& priority t' = priority t
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
rs = children t'
priority t' = priority t

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
with is_heap_list_Cons
[PROOF STATE]
proof (chain)
picking this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t
rs = children t'
priority t' = priority t
[PROOF STEP]
have "priority t = Min (set (bt_dfs priority t'))"
[PROOF STATE]
proof (prove)
using this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t
rs = children t'
priority t' = priority t

goal (1 subgoal):
 1. priority t = Min (set (bt_dfs priority t'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
priority t = Min (set (bt_dfs priority t'))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
with ot
[PROOF STATE]
proof (chain)
picking this:
rs = children t'
priority t' = priority t
priority t = Min (set (bt_dfs priority t'))
[PROOF STEP]
have "priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))"
[PROOF STATE]
proof (prove)
using this:
rs = children t'
priority t' = priority t
priority t = Min (set (bt_dfs priority t'))

goal (1 subgoal):
 1. priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))
[PROOF STEP]
by (simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
from cons
[PROOF STATE]
proof (chain)
picking this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t
[PROOF STEP]
have "priority r = Min (set (bt_dfs priority r))"
[PROOF STATE]
proof (prove)
using this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t

goal (1 subgoal):
 1. priority r = Min (set (bt_dfs priority r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
priority r = Min (set (bt_dfs priority r))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
priority r = Min (set (bt_dfs priority r))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
from cons
[PROOF STATE]
proof (chain)
picking this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t
[PROOF STEP]
have "children t = r # rs"
[PROOF STATE]
proof (prove)
using this:
is_heap_list (priority t) rs
\<lbrakk>priority t = priority ?t; rs = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
is_heap_list (priority r) (children r)
\<lbrakk>priority r = priority ?t; children r = children ?t\<rbrakk> \<Longrightarrow> priority ?t = Min (set (bt_dfs priority ?t))
priority t \<le> priority r
r # rs = children t

goal (1 subgoal):
 1. children t = r # rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
children t = r # rs

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
children t = r # rs
[PROOF STEP]
have "bts_dfs priority (children t) =
    (bt_dfs priority r) @ (bts_dfs priority rs)"
[PROOF STATE]
proof (prove)
using this:
children t = r # rs

goal (1 subgoal):
 1. bts_dfs priority (children t) = bt_dfs priority r @ bts_dfs priority rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bts_dfs priority (children t) = bt_dfs priority r @ bts_dfs priority rs

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
hence "bt_dfs priority t =
    priority t # (bt_dfs priority r @ bts_dfs priority rs)"
[PROOF STATE]
proof (prove)
using this:
bts_dfs priority (children t) = bt_dfs priority r @ bts_dfs priority rs

goal (1 subgoal):
 1. bt_dfs priority t = priority t # bt_dfs priority r @ bts_dfs priority rs
[PROOF STEP]
by (simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
bt_dfs priority t = priority t # bt_dfs priority r @ bts_dfs priority rs

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
hence A: "?M = Min
    (Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)))"
[PROOF STATE]
proof (prove)
using this:
bt_dfs priority t = priority t # bt_dfs priority r @ bts_dfs priority rs

goal (1 subgoal):
 1. Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
have "Set.insert (priority t) (set (bt_dfs priority r)
    \<union> set (bts_dfs priority rs)) =
    Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)) = Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)) = Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)))
Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)) = Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)
[PROOF STEP]
have "?M = Min
    (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r))"
[PROOF STATE]
proof (prove)
using this:
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)))
Set.insert (priority t) (set (bt_dfs priority r) \<union> set (bts_dfs priority rs)) = Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)

goal (1 subgoal):
 1. Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
with Min_Un
    [of "Set.insert (priority t) (set (bts_dfs priority rs))" "set (bt_dfs priority r)"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (Set.insert (priority t) (set (bts_dfs priority rs))); Set.insert (priority t) (set (bts_dfs priority rs)) \<noteq> {}; finite (set (bt_dfs priority r)); set (bt_dfs priority r) \<noteq> {}\<rbrakk> \<Longrightarrow> Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r))
[PROOF STEP]
have "?M =
    ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs))))
      (Min (set (bt_dfs priority r)))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (Set.insert (priority t) (set (bts_dfs priority rs))); Set.insert (priority t) (set (bts_dfs priority rs)) \<noteq> {}; finite (set (bt_dfs priority r)); set (bt_dfs priority r) \<noteq> {}\<rbrakk> \<Longrightarrow> Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))
Min (set (bt_dfs priority t)) = Min (Set.insert (priority t) (set (bts_dfs priority rs)) \<union> set (bt_dfs priority r))

goal (1 subgoal):
 1. Min (set (bt_dfs priority t)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))
[PROOF STEP]
by (auto simp add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
Min (set (bt_dfs priority t)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))
priority r = Min (set (bt_dfs priority r))
Min (set (bt_dfs priority t)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))
[PROOF STEP]
have "?M = ord_class.min (priority t) (priority r)"
[PROOF STATE]
proof (prove)
using this:
priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))
priority r = Min (set (bt_dfs priority r))
Min (set (bt_dfs priority t)) = ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs)))) (Min (set (bt_dfs priority r)))

goal (1 subgoal):
 1. Min (set (bt_dfs priority t)) = ord_class.min (priority t) (priority r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min (set (bt_dfs priority t)) = ord_class.min (priority t) (priority r)

goal (1 subgoal):
 1. \<And>ts t ta. \<lbrakk>is_heap_list (priority ta) ts; \<And>t. \<lbrakk>priority ta = priority t; ts = children t\<rbrakk> \<Longrightarrow> priority t = Min (set (bt_dfs priority t)); is_heap_list (priority t) (children t); \<And>ta. \<lbrakk>priority t = priority ta; children t = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta)); priority ta \<le> priority t; t # ts = children ta\<rbrakk> \<Longrightarrow> priority ta = Min (set (bt_dfs priority ta))
[PROOF STEP]
with \<open>priority t \<le> priority r\<close>
[PROOF STATE]
proof (chain)
picking this:
priority t \<le> priority r
Min (set (bt_dfs priority t)) = ord_class.min (priority t) (priority r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
priority t \<le> priority r
Min (set (bt_dfs priority t)) = ord_class.min (priority t) (priority r)

goal (1 subgoal):
 1. priority t = Min (set (bt_dfs priority t))
[PROOF STEP]
by (auto simp add: ord_class.min_def)
[PROOF STATE]
proof (state)
this:
priority t = Min (set (bt_dfs priority t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_binqueue_min_Min_prios:
  assumes "is_binqueue l xs"
  and "normalized xs"
  and "xs \<noteq> []"
  shows "min xs = Some (Min (set (prios xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Binomial_Queue.min xs = Some (Min (set (prios xs)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
normalized xs
xs \<noteq> []

goal (1 subgoal):
 1. Binomial_Queue.min xs = Some (Min (set (prios xs)))
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>normalized []; [] \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min [] = Some (Min (set (prios [])))
 2. \<And>l xs. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); normalized (None # xs); None # xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (None # xs) = Some (Min (set (prios (None # xs))))
 3. \<And>l xs t. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children t); is_heap_list (priority t) (children t); normalized (Some t # xs); Some t # xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some t # xs) = Some (Min (set (prios (Some t # xs))))
[PROOF STEP]
case (Some l xs x)
[PROOF STATE]
proof (state)
this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []

goal (3 subgoals):
 1. \<And>l. \<lbrakk>normalized []; [] \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min [] = Some (Min (set (prios [])))
 2. \<And>l xs. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); normalized (None # xs); None # xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (None # xs) = Some (Min (set (prios (None # xs))))
 3. \<And>l xs t. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children t); is_heap_list (priority t) (children t); normalized (Some t # xs); Some t # xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some t # xs) = Some (Min (set (prios (Some t # xs))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
proof (cases "xs \<noteq> []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
 2. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; \<not> xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> xs \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
 2. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; \<not> xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
with Some
[PROOF STATE]
proof (chain)
picking this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
\<not> xs \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
\<not> xs \<noteq> []

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
using bt_dfs_Min_priority[of x]
[PROOF STATE]
proof (prove)
using this:
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
\<not> xs \<noteq> []
is_heap_list (priority x) (children x) \<Longrightarrow> priority x = Min (set (bt_dfs priority x))

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
by (simp add: min_single)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))

goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
note T = this Some
[PROOF STATE]
proof (state)
this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
from T
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
[PROOF STEP]
have "normalized xs"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []

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

goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
with \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
normalized xs
[PROOF STEP]
have "prios xs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
normalized xs

goal (1 subgoal):
 1. prios xs \<noteq> []
[PROOF STEP]
by (induct xs) (simp_all add: bt_dfs_simp)
[PROOF STATE]
proof (state)
this:
prios xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); is_bintree_list l (children x); is_heap_list (priority x) (children x); normalized (Some x # xs); Some x # xs \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
with T
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
prios xs \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
prios xs \<noteq> []

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
using Min_Un[of "set (bt_dfs priority x)" "set (prios xs)"]
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
prios xs \<noteq> []
\<lbrakk>finite (set (bt_dfs priority x)); set (bt_dfs priority x) \<noteq> {}; finite (set (prios xs)); set (prios xs) \<noteq> {}\<rbrakk> \<Longrightarrow> Min (set (bt_dfs priority x) \<union> set (prios xs)) = ord_class.min (Min (set (bt_dfs priority x))) (Min (set (prios xs)))

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
using bt_dfs_Min_priority[of x]
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
is_binqueue (Suc l) xs
\<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs)))
is_bintree_list l (children x)
is_heap_list (priority x) (children x)
normalized (Some x # xs)
Some x # xs \<noteq> []
prios xs \<noteq> []
\<lbrakk>finite (set (bt_dfs priority x)); set (bt_dfs priority x) \<noteq> {}; finite (set (prios xs)); set (prios xs) \<noteq> {}\<rbrakk> \<Longrightarrow> Min (set (bt_dfs priority x) \<union> set (prios xs)) = ord_class.min (Min (set (bt_dfs priority x))) (Min (set (prios xs)))
is_heap_list (priority x) (children x) \<Longrightarrow> priority x = Min (set (bt_dfs priority x))

goal (1 subgoal):
 1. Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))
[PROOF STEP]
by (auto simp add: bt_dfs_simp ord_class.min_def)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min (Some x # xs) = Some (Min (set (prios (Some x # xs))))

goal (2 subgoals):
 1. \<And>l. \<lbrakk>normalized []; [] \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min [] = Some (Min (set (prios [])))
 2. \<And>l xs. \<lbrakk>is_binqueue (Suc l) xs; \<lbrakk>normalized xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min xs = Some (Min (set (prios xs))); normalized (None # xs); None # xs \<noteq> []\<rbrakk> \<Longrightarrow> Binomial_Queue.min (None # xs) = Some (Min (set (prios (None # xs))))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma min_p_min:
  assumes "is_binqueue l xs"
  and "xs \<noteq> []"
  and "normalized xs"
  and "distinct (vals xs)"
  and "distinct (prios xs)"
  shows "min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
from \<open>xs \<noteq> []\<close> \<open>normalized xs\<close>
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
normalized xs
[PROOF STEP]
have "\<not> PQ.is_empty (pqueue xs)"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
normalized xs

goal (1 subgoal):
 1. \<not> PQ.is_empty (pqueue xs)
[PROOF STEP]
by (simp add: empty_empty)
[PROOF STATE]
proof (state)
this:
\<not> PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)
[PROOF STEP]
have "min xs = Some (Min (set (prios xs)))"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs = Some (Min (set (prios xs)))
[PROOF STEP]
by (simp add: is_binqueue_min_Min_prios)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs = Some (Min (set (prios xs)))

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
with \<open>distinct (vals xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct (vals xs)
Binomial_Queue.min xs = Some (Min (set (prios xs)))
[PROOF STEP]
have "min xs = Some (Min (set \<parallel>pqueue xs\<parallel> ))"
[PROOF STATE]
proof (prove)
using this:
distinct (vals xs)
Binomial_Queue.min xs = Some (Min (set (prios xs)))

goal (1 subgoal):
 1. Binomial_Queue.min xs = Some (Min (set \<parallel>pqueue xs\<parallel>))
[PROOF STEP]
by (simp add: prios_pqueue)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs = Some (Min (set \<parallel>pqueue xs\<parallel>))

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> PQ.is_empty (pqueue xs)
Binomial_Queue.min xs = Some (Min (set \<parallel>pqueue xs\<parallel>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> PQ.is_empty (pqueue xs)
Binomial_Queue.min xs = Some (Min (set \<parallel>pqueue xs\<parallel>))

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
by (simp add: priority_Min_priorities [where q = "pqueue xs"] )
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_min_p_min:
  assumes "is_binqueue l xs"
  and "xs \<noteq> []"
  and "normalized xs"
  and "distinct (vals xs)"
  and "distinct (prios xs)"
  shows "priority (the (find_min xs)) =
    the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)
[PROOF STEP]
have "min xs \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs \<noteq> None
[PROOF STEP]
by (simp add: normalized_min_not_None)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs \<noteq> None

goal (1 subgoal):
 1. priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)
[PROOF STEP]
have "min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
by (simp add: min_p_min)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))

goal (1 subgoal):
 1. priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
with \<open>min xs \<noteq> None\<close>
[PROOF STATE]
proof (chain)
picking this:
Binomial_Queue.min xs \<noteq> None
Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Binomial_Queue.min xs \<noteq> None
Binomial_Queue.min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))

goal (1 subgoal):
 1. priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
by (auto simp add: min_eq_find_min_Some)
[PROOF STATE]
proof (state)
this:
priority (the (find_min xs)) = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_min_v_min:
  assumes "is_binqueue l xs"
  and "xs \<noteq> []"
  and "normalized xs"
  and "distinct (vals xs)"
  and "distinct (prios xs)"
  shows "val (the (find_min xs)) = PQ.min (pqueue xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)
[PROOF STEP]
have "min xs \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)

goal (1 subgoal):
 1. Binomial_Queue.min xs \<noteq> None
[PROOF STEP]
by (simp add: normalized_min_not_None)
[PROOF STATE]
proof (state)
this:
Binomial_Queue.min xs \<noteq> None

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Binomial_Queue.min xs \<noteq> None
[PROOF STEP]
obtain a where oa: "Some a = min xs"
[PROOF STATE]
proof (prove)
using this:
Binomial_Queue.min xs \<noteq> None

goal (1 subgoal):
 1. (\<And>a. Some a = Binomial_Queue.min xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some a = Binomial_Queue.min xs

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some a = Binomial_Queue.min xs
[PROOF STEP]
obtain t where ot: "find_min xs = Some t" "priority t = a"
[PROOF STATE]
proof (prove)
using this:
Some a = Binomial_Queue.min xs

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>find_min xs = Some t; priority t = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using min_eq_find_min_Some [of xs a]
[PROOF STATE]
proof (prove)
using this:
Some a = Binomial_Queue.min xs
(Binomial_Queue.min xs = Some a) = (\<exists>t. find_min xs = Some t \<and> priority t = a)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>find_min xs = Some t; priority t = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_min xs = Some t
priority t = a

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
hence *: "(val t, a) \<in> set (dfs alist xs)"
[PROOF STATE]
proof (prove)
using this:
find_min xs = Some t
priority t = a

goal (1 subgoal):
 1. (val t, a) \<in> set (elements xs)
[PROOF STEP]
by (auto simp add: find_min_exist in_set_in_alist)
[PROOF STATE]
proof (state)
this:
(val t, a) \<in> set (elements xs)

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
have "PQ.min (pqueue xs) = val t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PQ.min (pqueue xs) = val t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
assume A: "PQ.min (pqueue xs) \<noteq> val t"
[PROOF STATE]
proof (state)
this:
PQ.min (pqueue xs) \<noteq> val t

goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
PQ.min (pqueue xs) \<noteq> val t
[PROOF STEP]
obtain t' where ot':"PQ.min (pqueue xs) = t'"
[PROOF STATE]
proof (prove)
using this:
PQ.min (pqueue xs) \<noteq> val t

goal (1 subgoal):
 1. (\<And>t'. PQ.min (pqueue xs) = t' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
PQ.min (pqueue xs) = t'

goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
PQ.min (pqueue xs) \<noteq> val t
PQ.min (pqueue xs) = t'
[PROOF STEP]
have NE: "val t \<noteq> t'"
[PROOF STATE]
proof (prove)
using this:
PQ.min (pqueue xs) \<noteq> val t
PQ.min (pqueue xs) = t'

goal (1 subgoal):
 1. val t \<noteq> t'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val t \<noteq> t'

goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
from ot' oa assms
[PROOF STATE]
proof (chain)
picking this:
PQ.min (pqueue xs) = t'
Some a = Binomial_Queue.min xs
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)
[PROOF STEP]
have "(t', a) \<in> set (dfs alist xs)"
[PROOF STATE]
proof (prove)
using this:
PQ.min (pqueue xs) = t'
Some a = Binomial_Queue.min xs
is_binqueue l xs
xs \<noteq> []
normalized xs
distinct (vals xs)
distinct (prios xs)

goal (1 subgoal):
 1. (t', a) \<in> set (elements xs)
[PROOF STEP]
by (simp add: alist_pqueue PQ.priority_def min_p_min)
[PROOF STATE]
proof (state)
this:
(t', a) \<in> set (elements xs)

goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
with * NE
[PROOF STATE]
proof (chain)
picking this:
(val t, a) \<in> set (elements xs)
val t \<noteq> t'
(t', a) \<in> set (elements xs)
[PROOF STEP]
have "\<not> distinct (prios xs)"
[PROOF STATE]
proof (prove)
using this:
(val t, a) \<in> set (elements xs)
val t \<noteq> t'
(t', a) \<in> set (elements xs)

goal (1 subgoal):
 1. \<not> distinct (prios xs)
[PROOF STEP]
unfolding alist_split(2)
[PROOF STATE]
proof (prove)
using this:
(val t, a) \<in> set (elements xs)
val t \<noteq> t'
(t', a) \<in> set (elements xs)

goal (1 subgoal):
 1. \<not> distinct (dfs (snd \<circ> alist) xs)
[PROOF STEP]
unfolding dfs_comp
[PROOF STATE]
proof (prove)
using this:
(val t, a) \<in> set (elements xs)
val t \<noteq> t'
(t', a) \<in> set (elements xs)

goal (1 subgoal):
 1. \<not> distinct (map snd (elements xs))
[PROOF STEP]
by (induct ("dfs alist xs")) (auto simp add: rev_image_eqI)
[PROOF STATE]
proof (state)
this:
\<not> distinct (prios xs)

goal (1 subgoal):
 1. PQ.min (pqueue xs) \<noteq> val t \<Longrightarrow> False
[PROOF STEP]
with \<open>distinct (prios xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct (prios xs)
\<not> distinct (prios xs)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
distinct (prios xs)
\<not> distinct (prios xs)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
PQ.min (pqueue xs) = val t

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
with ot
[PROOF STATE]
proof (chain)
picking this:
find_min xs = Some t
priority t = a
PQ.min (pqueue xs) = val t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_min xs = Some t
priority t = a
PQ.min (pqueue xs) = val t

goal (1 subgoal):
 1. val (the (find_min xs)) = PQ.min (pqueue xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val (the (find_min xs)) = PQ.min (pqueue xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alist_normalize_idem:
  "dfs alist (normalize xs) = dfs alist xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elements (Binomial_Queue.normalize xs) = elements xs
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elements (rev (normalize' (rev xs))) = elements xs
[PROOF STEP]
proof (induct xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. elements (rev (normalize' (rev []))) = elements []
 2. \<And>x xs. elements (rev (normalize' (rev xs))) = elements xs \<Longrightarrow> elements (rev (normalize' (rev (xs @ [x])))) = elements (xs @ [x])
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
elements (rev (normalize' (rev xs))) = elements xs

goal (2 subgoals):
 1. elements (rev (normalize' (rev []))) = elements []
 2. \<And>x xs. elements (rev (normalize' (rev xs))) = elements xs \<Longrightarrow> elements (rev (normalize' (rev (xs @ [x])))) = elements (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elements (rev (normalize' (rev xs))) = elements xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
elements (rev (normalize' (rev xs))) = elements xs

goal (1 subgoal):
 1. elements (rev (normalize' (rev (xs @ [x])))) = elements (xs @ [x])
[PROOF STEP]
by (cases x) (simp_all add: dfs_append)
[PROOF STATE]
proof (state)
this:
elements (rev (normalize' (rev (xs @ [x])))) = elements (xs @ [x])

goal (1 subgoal):
 1. elements (rev (normalize' (rev []))) = elements []
[PROOF STEP]
qed simp


[STATEMENT]
lemma dfs_match_not_in:
  "(\<forall> t. Some t \<in> set xs \<longrightarrow> priority t \<noteq> a) \<Longrightarrow>
    set (dfs f (map (match a) xs)) = set (dfs f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. Some t \<in> set xs \<longrightarrow> priority t \<noteq> a \<Longrightarrow> set (dfs f (map (match a) xs)) = set (dfs f xs)
[PROOF STEP]
by (induct xs) simp_all


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

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

goal (1 subgoal):
 1. set (dfs f (map (match a) (x # xs))) \<subseteq> set (dfs f (x # xs))
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (state)
this:
set (dfs f (map (match a) (x # xs))) \<subseteq> set (dfs f (x # xs))

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