[STATEMENT]
lemma merge_ffold_singleton_if_wf:
  assumes "list_dtree (Node r {|(t1,e1)|})"
  shows "ffold (merge_f r {|(t1,e1)|}) [] {|(t1,e1)|} = dtree_to_list (Node r {|(t1,e1)|})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
interpret Comm: comp_fun_commute "merge_f r {|(t1,e1)|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_commute (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b)
[PROOF STEP]
by (rule merge_commute)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
define f where "f = merge_f r {|(t1,e1)|}"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b)

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
have "ffold f [] {|(t1,e1)|} = f (t1,e1) (ffold f [] {||})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})
[PROOF STEP]
using Comm.ffold_finsert f_def
[PROOF STATE]
proof (prove)
using this:
?x |\<notin>| ?A \<Longrightarrow> ffold (\<lambda>(t, e) b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) ?z (finsert ?x ?A) = (case ?x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) ?z ?A)
f = (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b)

goal (1 subgoal):
 1. ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
using f_def assms
[PROOF STATE]
proof (prove)
using this:
ffold f [] {|(t1, e1)|} = f (t1, e1) (ffold f [] {||})
f = (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b)
list_dtree (Node r {|(t1, e1)|})

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {|(t1, e1)|} \<and> list_dtree (Node r {|(t1, e1)|}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {|(t1, e1)|} = dtree_to_list (Node r {|(t1, e1)|})

goal:
No subgoals!
[PROOF STEP]
qed