[STATEMENT]
lemma fresh_abs_funI2:
  fixes a :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "a\<sharp>([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "\<exists>c::'x. c\<sharp>(a,x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<sharp> (a, x)
[PROOF STEP]
by  (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
[PROOF STATE]
proof (state)
this:
\<exists>c. c \<sharp> (a, x)

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<sharp> (a, x)
[PROOF STEP]
obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 
                and   fr2: "c\<sharp>x"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<sharp> (a, x)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>a \<noteq> c; c \<noteq> a; c \<sharp> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp add: fresh_prod at_fresh[OF at])
[PROOF STATE]
proof (state)
this:
a \<noteq> c
c \<noteq> a
c \<sharp> x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "c\<sharp>([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sharp> [a].x
[PROOF STEP]
using f fr1 fr2
[PROOF STATE]
proof (prove)
using this:
finite (supp x)
a \<noteq> c
c \<sharp> x

goal (1 subgoal):
 1. c \<sharp> [a].x
[PROOF STEP]
by (simp add: fresh_abs_funI1[OF pt, OF at])
[PROOF STATE]
proof (state)
this:
c \<sharp> [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))"
[PROOF STATE]
proof (prove)
using this:
c \<sharp> [a].x

goal (1 subgoal):
 1. [(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
[PROOF STEP]
using fr1
[PROOF STATE]
proof (prove)
using this:
c \<sharp> [a].x
a \<noteq> c

goal (1 subgoal):
 1. [(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
[PROOF STEP]
by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
[PROOF STATE]
proof (state)
this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))"
[PROOF STATE]
proof (prove)
using this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x

goal (1 subgoal):
 1. a \<sharp> [c].([(c, a)] \<bullet> x)
[PROOF STEP]
using fr1_sym
[PROOF STATE]
proof (prove)
using this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
c \<noteq> a

goal (1 subgoal):
 1. a \<sharp> [c].([(c, a)] \<bullet> x)
[PROOF STEP]
by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
[PROOF STATE]
proof (state)
this:
a \<sharp> [c].([(c, a)] \<bullet> x)

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "[c].([(c,a)]\<bullet>x) = ([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [c].([(c, a)] \<bullet> x) = [a].x
[PROOF STEP]
using fr1_sym fr2
[PROOF STATE]
proof (prove)
using this:
c \<noteq> a
c \<sharp> x

goal (1 subgoal):
 1. [c].([(c, a)] \<bullet> x) = [a].x
[PROOF STEP]
by (simp add: abs_fun_eq[OF pt, OF at])
[PROOF STATE]
proof (state)
this:
[c].([(c, a)] \<bullet> x) = [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[c].([(c, a)] \<bullet> x) = [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
[c].([(c, a)] \<bullet> x) = [a].x
a \<sharp> [c].([(c, a)] \<bullet> x)

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sharp> [a].x

goal:
No subgoals!
[PROOF STEP]
qed