[STATEMENT]
lemma is_binqueue_delete_min:
  assumes "is_binqueue 0 xs"
  shows "is_binqueue 0 (delete_min xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
proof (cases "find_min xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
case (Some t)
[PROOF STATE]
proof (state)
this:
find_min xs = Some t

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
[PROOF STEP]
have "is_binqueue 0 (map (match (priority t)) xs)"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs

goal (1 subgoal):
 1. is_binqueue 0 (map (match (priority t)) xs)
[PROOF STEP]
by (induct xs) simp_all
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map (match (priority t)) xs)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map (match (priority t)) xs)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
from Some
[PROOF STATE]
proof (chain)
picking this:
find_min xs = Some t
[PROOF STEP]
have "Some t \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
find_min xs = Some t

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

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
Some t \<in> set xs
[PROOF STEP]
have "\<exists>l. is_bintree l t" and "is_heap t"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
Some t \<in> set xs

goal (1 subgoal):
 1. \<exists>l. is_bintree_list l (children t) &&& is_heap_list (priority t) (children t)
[PROOF STEP]
using is_binqueue_select[of 0 xs t]
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
Some t \<in> set xs
\<lbrakk>is_binqueue 0 xs; Some t \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>k. is_bintree_list k (children t) \<and> is_heap_list (priority t) (children t)

goal (1 subgoal):
 1. \<exists>l. is_bintree_list l (children t) &&& is_heap_list (priority t) (children t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)
[PROOF STEP]
have "is_binqueue 0 (map Some (rev (children t)))"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)

goal (1 subgoal):
 1. is_binqueue 0 (map Some (rev (children t)))
[PROOF STEP]
by (auto simp add: is_binqueue_children)
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map Some (rev (children t)))

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))

goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
using Some
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))
find_min xs = Some t

goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
by (auto simp add: is_binqueue_meld delete_min_def is_binqueue_normalize
      split: bintree.split)
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (delete_min xs)

goal (1 subgoal):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
qed (simp add: delete_min_def)