[STATEMENT]
lemma Union_supports_set:
  fixes X::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (supp ` X) supports X
[PROOF STEP]
apply(simp add: supports_def fresh_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(rule allI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<Longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(simp add: perm_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x\<rbrakk> \<Longrightarrow> {[(a, b)] \<bullet> x |x. x \<in> X} = X
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa \<in> X
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X; [(a, b)] \<bullet> xa = xa\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa \<in> X
 2. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa = xa
 3. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa = xa
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(rule pt_fresh_fresh[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> a \<sharp> xa
 2. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> xa
 3. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> xa
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(rule_tac x="x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> x = [(a, b)] \<bullet> x \<and> x \<in> X
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> x = [(a, b)] \<bullet> x
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> x = x
[PROOF STEP]
apply(rule pt_fresh_fresh[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> a \<sharp> x
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> x
[PROOF STEP]
apply(force)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done