[STATEMENT]
lemma merge_ffold_fsts_in_childverts:
  "\<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (merge_f r xs) [] xs)\<rbrakk>
    \<Longrightarrow> \<exists>t1 \<in> fst `  fset xs. y \<in> dverts t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
x |\<notin>| xs
\<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> 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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> 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) [] (finsert x xs))

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
obtain t1 e1 where t1_def[simp]: "x = (t1,e1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t1 e1. x = (t1, e1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = (t1, e1)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
let ?f = "merge_f r (finsert x xs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
let ?f' = "merge_f r xs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "(t1, e1) \<in> fset (finsert x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1, e1) \<in> fset (finsert x xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t1, e1) \<in> fset (finsert x xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(t1, e1) \<in> fset (finsert x xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "(t1, e1) \<notin> fset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1, e1) \<notin> fset xs
[PROOF STEP]
using insert.hyps notin_fset
[PROOF STATE]
proof (prove)
using this:
x |\<notin>| xs
(?x |\<notin>| ?S) = (?x \<notin> fset ?S)

goal (1 subgoal):
 1. (t1, e1) \<notin> fset xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(t1, e1) \<notin> fset xs

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs
[PROOF STEP]
have xs_val:
    "(\<forall>(v,e) \<in> set (ffold ?f' [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1})"
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs

goal (1 subgoal):
 1. \<forall>(v, e)\<in>set (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) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge]
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs
\<lbrakk>(?t1.0, ?e1.0) \<in> fset (finsert x xs); (?t1.0, ?e1.0) \<notin> fset xs; (?v, ?e) \<in> set (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) [] xs)\<rbrakk> \<Longrightarrow> set ?v \<inter> dlverts ?t1.0 = {} \<and> ?v \<noteq> [] \<and> ?e \<notin> darcs ?t1.0 \<union> {?e1.0}

goal (1 subgoal):
 1. \<forall>(v, e)\<in>set (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) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(v, e)\<in>set (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) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have 0: "list_dtree (Node r xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_dtree (Node r xs)
[PROOF STEP]
using list_dtree_subset insert.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs |\<subseteq>| ?ys; list_dtree (Node ?r ?ys)\<rbrakk> \<Longrightarrow> list_dtree (Node ?r ?xs)
list_dtree (Node r (finsert x xs))

goal (1 subgoal):
 1. list_dtree (Node r xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_dtree (Node r xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_dtree (Node r xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_dtree (Node r xs)

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
proof(cases "y \<in> fst ` set (ffold (merge_f r xs) [] xs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
 2. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> fst ` set (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) [] xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
 2. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> fst ` set (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) [] xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (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) [] xs)

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
using insert.IH[OF 0]
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (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) [] xs)
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> 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) [] xs) \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> fst ` set (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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
[PROOF STEP]
using Comm.ffold_finsert[OF insert.hyps]
[PROOF STATE]
proof (prove)
using this:
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 xs) = (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 xs)

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "\<dots> = ?f x (ffold ?f' [] xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
[PROOF STEP]
using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs |\<subseteq>| finsert x xs; list_dtree (Node r (finsert x xs))\<rbrakk> \<Longrightarrow> ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs = 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) [] xs
list_dtree (Node r (finsert x xs))

goal (1 subgoal):
 1. (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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 (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
[PROOF STEP]
have "ffold ?f [] (finsert x xs)
                = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs)
[PROOF STEP]
using xs_val insert.prems
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] xs)
\<forall>(v, e)\<in>set (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) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> 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) [] (finsert x xs))

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs)
[PROOF STEP]
have "set (ffold ?f [] (finsert x xs))
          = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs))"
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs)

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs))
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs))

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs))
[PROOF STEP]
have "set (ffold ?f [] (finsert x xs))
          = (set (dtree_to_list (Node r {|x|})) \<union> set (ffold ?f' [] xs))"
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs))

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)
[PROOF STEP]
using set_merge
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (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) [] xs))
set ?xs \<union> set ?ys = set (Sorting_Algorithms.merge ?cmp ?xs ?ys)

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)
[PROOF STEP]
have "y \<in> fst ` set (dtree_to_list (Node r {|x|}))"
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)

goal (1 subgoal):
 1. y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
using False insert.prems
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x 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) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (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) [] xs)
y \<notin> fst ` set (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) [] xs)
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> 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) [] (finsert x xs))

goal (1 subgoal):
 1. y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (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) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
by (simp add: dtree_to_list_x_in_dverts)
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<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) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
[PROOF STEP]
qed (simp)


[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


[STATEMENT]
lemma denormalize_hd_root:
  assumes "root t \<noteq> []"
  shows "hd (denormalize t) = hd (root t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
proof(cases "\<forall>x. sucs t \<noteq> {|x|}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
 2. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>x. sucs t \<noteq> {|x|}

goal (2 subgoals):
 1. \<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
 2. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. sucs t \<noteq> {|x|}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. sucs t \<noteq> {|x|}

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
using denormalize.simps(2)[of "sucs t" "root t"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x. sucs t \<noteq> {|x|}
\<forall>x. sucs t \<noteq> {|x|} \<Longrightarrow> denormalize (Node (dtree.root t) (sucs t)) = dtree.root t

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (denormalize t) = hd (dtree.root t)

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})
[PROOF STEP]
obtain t1 e where "{|(t1, e)|} = sucs t"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. sucs t \<noteq> {|x|})

goal (1 subgoal):
 1. (\<And>t1 e. {|(t1, e)|} = sucs t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{|(t1, e)|} = sucs t

goal (1 subgoal):
 1. \<not> (\<forall>x. sucs t \<noteq> {|x|}) \<Longrightarrow> hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{|(t1, e)|} = sucs t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{|(t1, e)|} = sucs t

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
using denormalize.simps(1)[of "root t" t1 e] assms
[PROOF STATE]
proof (prove)
using this:
{|(t1, e)|} = sucs t
denormalize (Node (dtree.root t) {|(t1, e)|}) = dtree.root t @ denormalize t1
dtree.root t \<noteq> []

goal (1 subgoal):
 1. hd (denormalize t) = hd (dtree.root t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (denormalize t) = hd (dtree.root t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinguishing_weak_formula_is_weak:
    assumes "\<not> (P \<equiv>\<cdot> Q)"
    shows "weak_formula (distinguishing_weak_formula P Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
let ?some = "\<lambda>p. (\<some>x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
let ?B = "{- p \<bullet> ?some p|p. True}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> P \<equiv>\<cdot> Q
[PROOF STEP]
have "supp (Abs_bset ?B :: _ set['idx]) \<subseteq> supp P"
[PROOF STATE]
proof (prove)
using this:
\<not> P \<equiv>\<cdot> Q

goal (1 subgoal):
 1. supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
[PROOF STEP]
by (rule distinguishing_weak_formula_supp_aux)
[PROOF STATE]
proof (state)
this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
[PROOF STEP]
have "finite (supp (Abs_bset ?B :: _ set['idx]))"
[PROOF STATE]
proof (prove)
using this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P

goal (1 subgoal):
 1. finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
using finite_supp rev_finite_subset
[PROOF STATE]
proof (prove)
using this:
supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) \<subseteq> supp P
finite (supp ?x)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
have "set_bset (Abs_bset ?B :: _ set['idx]) = ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
using distinguishing_weak_formula_card_aux Abs_bset_inverse'
[PROOF STATE]
proof (prove)
using this:
|{- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> ?P) \<and> x distinguishes (p \<bullet> ?P) from (p \<bullet> ?Q)) |p. True}| <o natLeq +c |UNIV|
|?A| <o natLeq +c |UNIV| \<Longrightarrow> set_bset (Abs_bset ?A) = ?A

goal (1 subgoal):
 1. set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
assume "x \<in> ?B"
[PROOF STATE]
proof (state)
this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
[PROOF STEP]
obtain p where "x = -p \<bullet> ?some p"
[PROOF STATE]
proof (prove)
using this:
x \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}

goal (1 subgoal):
 1. (\<And>p. x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> P \<equiv>\<cdot> Q
[PROOF STEP]
have "\<not> (p \<bullet> P) \<equiv>\<cdot> (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
using this:
\<not> P \<equiv>\<cdot> Q

goal (1 subgoal):
 1. \<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q
[PROOF STEP]
by (metis permute_minus_cancel(2) weakly_logically_equivalent_eqvt)
[PROOF STATE]
proof (state)
this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q
[PROOF STEP]
have "weak_formula (?some p)"
[PROOF STATE]
proof (prove)
using this:
\<not> p \<bullet> P \<equiv>\<cdot> p \<bullet> Q

goal (1 subgoal):
 1. weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
[PROOF STEP]
by (metis (mono_tags, lifting) distinguished_bounded_support weakly_equivalent_iff_not_distinguished someI_ex)
[PROOF STATE]
proof (state)
this:
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
[PROOF STEP]
have "weak_formula x"
[PROOF STATE]
proof (prove)
using this:
x = - p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))
weak_formula (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q))

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

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (distinguishing_weak_formula P Q)
[PROOF STEP]
unfolding distinguishing_weak_formula_def
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9

goal (1 subgoal):
 1. weak_formula (Conj (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
using wf_Conj
[PROOF STATE]
proof (prove)
using this:
finite (supp (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
set_bset (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}) = {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}
?x9 \<in> {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True} \<Longrightarrow> weak_formula ?x9
\<lbrakk>finite (supp ?xset); \<And>x. x \<in> set_bset ?xset \<Longrightarrow> weak_formula x\<rbrakk> \<Longrightarrow> weak_formula (Conj ?xset)

goal (1 subgoal):
 1. weak_formula (Conj (Abs_bset {- p \<bullet> (SOME x. weak_formula x \<and> supp x \<subseteq> supp (p \<bullet> P) \<and> x distinguishes (p \<bullet> P) from (p \<bullet> Q)) |p. True}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
weak_formula (distinguishing_weak_formula P Q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_signed_lconjaction: "inj (signed_lconjaction s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (signed_lconjaction s)
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
assume 1: "signed_lconjaction s x = signed_lconjaction s y"
[PROOF STATE]
proof (state)
this:
signed_lconjaction s x = signed_lconjaction s y

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
signed_lconjaction s x = signed_lconjaction s y

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
obtain a1 a2 :: 'a and b1 b2 :: bool
    where xy: "x = (a1,b1)" "y = (a2,b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 b1 a2 b2. \<lbrakk>x = (a1, b1); y = (a2, b2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
x = (a1, b1)
y = (a2, b2)

goal (1 subgoal):
 1. \<And>x y. signed_lconjaction s x = signed_lconjaction s y \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)
[PROOF STEP]
show "x=y"
[PROOF STATE]
proof (prove)
using this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using injD[OF lconjby_inj, of s a1 a2] signed_lconjactionD
[PROOF STATE]
proof (prove)
using this:
signed_lconjaction s x = signed_lconjaction s y
x = (a1, b1)
y = (a2, b2)
lconjby s a1 = lconjby s a2 \<Longrightarrow> a1 = a2
signed_lconjaction ?s ?x \<equiv> map_prod (lconjby ?s) (\<lambda>b. b \<noteq> (fst ?x = ?s)) ?x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by    (cases "a1=s" "a2=s" rule: two_cases) auto
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "concat\<cdot>[a] = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat\<cdot>[a] = a
[PROOF STEP]
by auto


[STATEMENT]
lemma "catMaybes\<cdot>(map\<cdot>f\<cdot>x) = mapMaybe\<cdot>f\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. catMaybes\<cdot>(map\<cdot>f\<cdot>x) = mapMaybe\<cdot>f\<cdot>x
[PROOF STEP]
by auto


[STATEMENT]
lemma mono_const[simp, intro!]: "mono (\<lambda>_. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>_. c)
[PROOF STEP]
by (auto intro: monoI)


[STATEMENT]
lemma dual_ccpo_mono_simp: "monotone (\<ge>) (\<ge>) f \<longleftrightarrow> mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<lambda>x y. y \<le> x) (\<lambda>x y. y \<le> x) f = mono f
[PROOF STEP]
unfolding monotone_def mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y. y \<le> x \<longrightarrow> f y \<le> f x) = (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)
[PROOF STEP]
by auto