[STATEMENT]
lemma list_set_UNION_autoref[autoref_rules]:
      assumes "PRIO_TAG_OPTIMIZATION"
      assumes "SIDE_PRECOND_OPT (\<forall> x \<in> S. \<forall> y \<in> S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {})"
      assumes "(xs, S) \<in> \<langle>A\<rangle> list_set_rel" "(f, g) \<in> A \<rightarrow> \<langle>B\<rangle> list_set_rel"
      shows "(xs \<bind> f,
        (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle> list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle> list_set_rel) \<rightarrow> \<langle>B\<rangle> list_set_rel) $ S $ g) \<in>
        \<langle>B\<rangle> list_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<bind> f, (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle>list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle>list_set_rel) \<rightarrow> \<langle>B\<rangle>list_set_rel) $ S $ g) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
using assms list_set_bind
[PROOF STATE]
proof (prove)
using this:
PRIO_TAG_OPTIMIZATION
SIDE_PRECOND_OPT (\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {})
(xs, S) \<in> \<langle>A\<rangle>list_set_rel
(f, g) \<in> A \<rightarrow> \<langle>B\<rangle>list_set_rel
\<lbrakk>\<And>x y. \<lbrakk>x \<in> ?S; y \<in> ?S; x \<noteq> y\<rbrakk> \<Longrightarrow> ?g x \<inter> ?g y = {}; (?xs, ?S) \<in> \<langle>?A\<rangle>list_set_rel; (?f, ?g) \<in> ?A \<rightarrow> \<langle>?B\<rangle>list_set_rel\<rbrakk> \<Longrightarrow> (?xs \<bind> ?f, ?S \<bind> ?g) \<in> \<langle>?B\<rangle>list_set_rel

goal (1 subgoal):
 1. (xs \<bind> f, (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle>list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle>list_set_rel) \<rightarrow> \<langle>B\<rangle>list_set_rel) $ S $ g) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
unfolding bind_UNION autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
PRIO_TAG_OPTIMIZATION
\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {}
(xs, S) \<in> \<langle>A\<rangle>list_set_rel
(f, g) \<in> A \<rightarrow> \<langle>B\<rangle>list_set_rel
\<lbrakk>\<And>x y. \<lbrakk>x \<in> ?S; y \<in> ?S; x \<noteq> y\<rbrakk> \<Longrightarrow> ?g x \<inter> ?g y = {}; (?xs, ?S) \<in> \<langle>?A\<rangle>list_set_rel; (?f, ?g) \<in> ?A \<rightarrow> \<langle>?B\<rangle>list_set_rel\<rbrakk> \<Longrightarrow> (?xs \<bind> ?f, \<Union> (?g ` ?S)) \<in> \<langle>?B\<rangle>list_set_rel

goal (1 subgoal):
 1. (xs \<bind> f, \<Union> (g ` S)) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
by metis