[STATEMENT]
lemma Disjoint_fresh_iff [simp]: "a \<sharp> Disjoint t u \<longleftrightarrow> a \<sharp> t \<and> a \<sharp> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
obtain j::name where j: "atom j \<sharp> (a,t,u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. atom j \<sharp> (a, t, u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (a, t, u)

goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (a, t, u)

goal (1 subgoal):
 1. a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)
[PROOF STEP]
by (auto simp: Disjoint.simps [of j])
[PROOF STATE]
proof (state)
this:
a \<sharp> Disjoint t u = (a \<sharp> t \<and> a \<sharp> u)

goal:
No subgoals!
[PROOF STEP]
qed