[STATEMENT]
lemma at_set_avoiding_aux':
  fixes Xs::"'a set"
  and   As::"'a set"
  assumes at: "at TYPE('a)"
  and     a: "finite Xs"
  and     b: "Xs \<subseteq> As"
  and     c: "finite As"
  and     d: "finite ((supp c)::'a set)"
  shows "\<exists>(Ys::'a set) (pi::'a prm). Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> (pi\<bullet>Xs=Ys) \<and>
          set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> (distinctPerm pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
using a b c
[PROOF STATE]
proof (prove)
using this:
finite Xs
Xs \<subseteq> As
finite As

goal (1 subgoal):
 1. \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> As
finite As

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "({}::'a set)\<sharp>*c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<sharp>* c
[PROOF STEP]
by (simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
{} \<sharp>* c

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{} \<sharp>* c

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "({}::'a set) \<inter> As = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<inter> As = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<inter> As = {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{} \<inter> As = {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "([]::'a prm)\<bullet>{} = ({}::'a set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<bullet> {} = {}
[PROOF STEP]
by(rule pt1) (metis Nominal.pt_set_inst at at_pt_inst)
[PROOF STATE]
proof (state)
this:
[] \<bullet> {} = {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[] \<bullet> {} = {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "set ([]::'a prm) \<subseteq> {} \<times> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set [] \<subseteq> {} \<times> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> {} \<times> {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> {} \<times> {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "finite ({}::'a set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "distinctPerm([]::'a prm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinctPerm []
[PROOF STEP]
by(simp add: distinctPerm_def)
[PROOF STATE]
proof (state)
this:
distinctPerm []

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{} \<sharp>* c
{} \<inter> As = {}
[] \<bullet> {} = {}
set [] \<subseteq> {} \<times> {}
finite {}
distinctPerm []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<sharp>* c
{} \<inter> As = {}
[] \<bullet> {} = {}
set [] \<subseteq> {} \<times> {}
finite {}
distinctPerm []

goal (1 subgoal):
 1. \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> {} = Ys \<and> set pi \<subseteq> {} \<times> Ys \<and> finite Ys \<and> distinctPerm pi

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
case (insert x Xs)
[PROOF STATE]
proof (state)
this:
finite Xs
x \<notin> Xs
\<lbrakk>Xs \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
insert x Xs \<subseteq> As
finite As

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite Xs
x \<notin> Xs
\<lbrakk>Xs \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
insert x Xs \<subseteq> As
finite As
[PROOF STEP]
have ih: "\<exists>Ys pi. Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> pi\<bullet>Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi"
[PROOF STATE]
proof (prove)
using this:
finite Xs
x \<notin> Xs
\<lbrakk>Xs \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
insert x Xs \<subseteq> As
finite As

goal (1 subgoal):
 1. \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
obtain Ys pi where a1: "Ys\<sharp>*c" and a2: "Ys \<inter> As = {}" and a3: "(pi::'a prm)\<bullet>Xs = Ys" and
                          a4: "set pi \<subseteq> Xs \<times> Ys" and a5: "finite Ys"
                      and a6: "distinctPerm pi"
[PROOF STATE]
proof (prove)
using this:
\<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi

goal (1 subgoal):
 1. (\<And>Ys pi. \<lbrakk>Ys \<sharp>* c; Ys \<inter> As = {}; pi \<bullet> Xs = Ys; set pi \<subseteq> Xs \<times> Ys; finite Ys; distinctPerm pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ys \<sharp>* c
Ys \<inter> As = {}
pi \<bullet> Xs = Ys
set pi \<subseteq> Xs \<times> Ys
finite Ys
distinctPerm pi

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have b: "x\<notin>Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> Xs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x \<notin> Xs

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have d1: "finite As"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite As
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
finite As

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have d2: "finite Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Xs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
finite Xs

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have d3: "insert x Xs \<subseteq> As"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x Xs \<subseteq> As
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
insert x Xs \<subseteq> As

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have d4: "finite((supp pi)::'a set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp pi)
[PROOF STEP]
by(induct pi)
      (auto simp add: supp_list_nil supp_prod at_fin_set_supp[OF at]
                      supp_list_cons at_supp[OF at])
[PROOF STATE]
proof (state)
this:
finite (supp pi)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "\<exists>y::'a. y\<sharp>(c,x,Ys,As,pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<sharp> (c, x, Ys, As, pi)
[PROOF STEP]
using d d1 a5 d4
[PROOF STATE]
proof (prove)
using this:
finite (supp c)
finite As
finite Ys
finite (supp pi)

goal (1 subgoal):
 1. \<exists>y. y \<sharp> (c, x, Ys, As, pi)
[PROOF STEP]
by (rule_tac at_exists_fresh'[OF at])
       (simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at])
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<sharp> (c, x, Ys, As, pi)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. y \<sharp> (c, x, Ys, As, pi)
[PROOF STEP]
obtain y::"'a" where  e: "y\<sharp>(c,x,Ys,As,pi)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. y \<sharp> (c, x, Ys, As, pi)

goal (1 subgoal):
 1. (\<And>y. y \<sharp> (c, x, Ys, As, pi) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<sharp> (c, x, Ys, As, pi)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "({y}\<union>Ys)\<sharp>*c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({y} \<union> Ys) \<sharp>* c
[PROOF STEP]
using a1 e
[PROOF STATE]
proof (prove)
using this:
Ys \<sharp>* c
y \<sharp> (c, x, Ys, As, pi)

goal (1 subgoal):
 1. ({y} \<union> Ys) \<sharp>* c
[PROOF STEP]
by (simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
({y} \<union> Ys) \<sharp>* c

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
({y} \<union> Ys) \<sharp>* c

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "({y}\<union>Ys)\<inter>As = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({y} \<union> Ys) \<inter> As = {}
[PROOF STEP]
using a2 d1 e
[PROOF STATE]
proof (prove)
using this:
Ys \<inter> As = {}
finite As
y \<sharp> (c, x, Ys, As, pi)

goal (1 subgoal):
 1. ({y} \<union> Ys) \<inter> As = {}
[PROOF STEP]
by (simp add: fresh_prod at_fin_set_fresh[OF at])
[PROOF STATE]
proof (state)
this:
({y} \<union> Ys) \<inter> As = {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
({y} \<union> Ys) \<inter> As = {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
have eq: "[(pi\<bullet>x,y)]\<bullet>Ys = Ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
have "(pi\<bullet>x)\<sharp>Ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> x \<sharp> Ys
[PROOF STEP]
using a3[symmetric] b d2
[PROOF STATE]
proof (prove)
using this:
Ys = pi \<bullet> Xs
x \<notin> Xs
finite Xs

goal (1 subgoal):
 1. pi \<bullet> x \<sharp> Ys
[PROOF STEP]
by(simp add: pt_fresh_bij[OF pt_set_inst, OF at_pt_inst[OF at], OF at, OF at]
                     at_fin_set_fresh[OF at d2])
[PROOF STATE]
proof (state)
this:
pi \<bullet> x \<sharp> Ys

goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pi \<bullet> x \<sharp> Ys

goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
have "y\<sharp>Ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sharp> Ys
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
y \<sharp> (c, x, Ys, As, pi)

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

goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pi \<bullet> x \<sharp> Ys
y \<sharp> Ys
[PROOF STEP]
show "[(pi\<bullet>x,y)]\<bullet>Ys = Ys"
[PROOF STATE]
proof (prove)
using this:
pi \<bullet> x \<sharp> Ys
y \<sharp> Ys

goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> Ys = Ys
[PROOF STEP]
by (simp add: pt_fresh_fresh[OF pt_set_inst, OF at_pt_inst[OF at], OF at, OF at])
[PROOF STATE]
proof (state)
this:
[(pi \<bullet> x, y)] \<bullet> Ys = Ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(pi \<bullet> x, y)] \<bullet> Ys = Ys

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> ({x} \<union> Xs) = [(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs)
[PROOF STEP]
by (simp add: pt2[symmetric, OF pt_set_inst, OF at_pt_inst[OF at], OF at])
[PROOF STATE]
proof (state)
this:
((pi \<bullet> x, y) # pi) \<bullet> ({x} \<union> Xs) = [(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs)

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((pi \<bullet> x, y) # pi) \<bullet> ({x} \<union> Xs) = [(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs)

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs) = {y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs
[PROOF STEP]
by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
[PROOF STATE]
proof (state)
this:
[(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs) = {y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[(pi \<bullet> x, y)] \<bullet> pi \<bullet> ({x} \<union> Xs) = {y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>Ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs = {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys
[PROOF STEP]
using a3
[PROOF STATE]
proof (prove)
using this:
pi \<bullet> Xs = Ys

goal (1 subgoal):
 1. {y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs = {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs = {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y} \<union> [(pi \<bullet> x, y)] \<bullet> pi \<bullet> Xs = {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
have "\<dots> = {y}\<union>Ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys = {y} \<union> Ys
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
[(pi \<bullet> x, y)] \<bullet> Ys = Ys

goal (1 subgoal):
 1. {y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys = {y} \<union> Ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{y} \<union> [(pi \<bullet> x, y)] \<bullet> Ys = {y} \<union> Ys

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((pi \<bullet> x, y) # pi) \<bullet> ({x} \<union> Xs) = {y} \<union> Ys
[PROOF STEP]
show "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys"
[PROOF STATE]
proof (prove)
using this:
((pi \<bullet> x, y) # pi) \<bullet> ({x} \<union> Xs) = {y} \<union> Ys

goal (1 subgoal):
 1. ((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "pi\<bullet>x=x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> x = x
[PROOF STEP]
using a4 b a2 a3 d3
[PROOF STATE]
proof (prove)
using this:
set pi \<subseteq> Xs \<times> Ys
x \<notin> Xs
Ys \<inter> As = {}
pi \<bullet> Xs = Ys
insert x Xs \<subseteq> As

goal (1 subgoal):
 1. pi \<bullet> x = x
[PROOF STEP]
by (rule_tac at_prm_fresh2[OF at]) (auto)
[PROOF STATE]
proof (state)
this:
pi \<bullet> x = x

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pi \<bullet> x = x
[PROOF STEP]
have "set ((pi\<bullet>x,y)#pi) \<subseteq> (insert x Xs) \<times> ({y}\<union>Ys)"
[PROOF STATE]
proof (prove)
using this:
pi \<bullet> x = x

goal (1 subgoal):
 1. set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)
[PROOF STEP]
using a4
[PROOF STATE]
proof (prove)
using this:
pi \<bullet> x = x
set pi \<subseteq> Xs \<times> Ys

goal (1 subgoal):
 1. set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
have "finite ({y}\<union>Ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({y} \<union> Ys)
[PROOF STEP]
using a5
[PROOF STATE]
proof (prove)
using this:
finite Ys

goal (1 subgoal):
 1. finite ({y} \<union> Ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite ({y} \<union> Ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite ({y} \<union> Ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
from \<open>Ys \<inter> As = {}\<close> \<open>(insert x Xs) \<subseteq> As\<close> \<open>finite Ys\<close>
[PROOF STATE]
proof (chain)
picking this:
Ys \<inter> As = {}
insert x Xs \<subseteq> As
finite Ys
[PROOF STEP]
have "x \<notin> Ys"
[PROOF STATE]
proof (prove)
using this:
Ys \<inter> As = {}
insert x Xs \<subseteq> As
finite Ys

goal (1 subgoal):
 1. x \<notin> Ys
[PROOF STEP]
by(auto simp add: fresh_def at_fin_set_supp[OF at])
[PROOF STATE]
proof (state)
this:
x \<notin> Ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
with a6 \<open>pi \<bullet> x = x\<close> \<open>x \<notin> Xs\<close> \<open>(set pi) \<subseteq> Xs \<times> Ys\<close> e
[PROOF STATE]
proof (chain)
picking this:
distinctPerm pi
pi \<bullet> x = x
x \<notin> Xs
set pi \<subseteq> Xs \<times> Ys
y \<sharp> (c, x, Ys, As, pi)
x \<notin> Ys
[PROOF STEP]
have "distinctPerm((pi \<bullet> x, y)#pi)"
[PROOF STATE]
proof (prove)
using this:
distinctPerm pi
pi \<bullet> x = x
x \<notin> Xs
set pi \<subseteq> Xs \<times> Ys
y \<sharp> (c, x, Ys, As, pi)
x \<notin> Ys

goal (1 subgoal):
 1. distinctPerm ((pi \<bullet> x, y) # pi)
[PROOF STEP]
apply(auto simp add: distinctPerm_def fresh_prod at_fresh[OF at])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (a, y) \<in> set pi\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (a, y) \<in> set pi\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (a, y) \<in> set pi\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "b \<sharp> pi" and "(a, b) \<in> set pi"
[PROOF STATE]
proof (state)
this:
b \<sharp> pi
(a, b) \<in> set pi

goal (2 subgoals):
 1. \<And>a. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (a, y) \<in> set pi\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
b \<sharp> pi
(a, b) \<in> set pi

goal (1 subgoal):
 1. False
[PROOF STEP]
by(induct pi)
          (auto simp add: supp_list_cons supp_prod at_supp[OF at] fresh_list_cons fresh_prod at_fresh[OF at])
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a \<sharp> pi" and "(a, b) \<in> set pi"
[PROOF STATE]
proof (state)
this:
a \<sharp> pi
(a, b) \<in> set pi

goal (1 subgoal):
 1. \<And>b. \<lbrakk>pi \<bullet> x = x; x \<notin> Xs; set pi \<subseteq> Xs \<times> Ys; x \<notin> Ys; distinct (map fst pi); y \<sharp> c; distinct (map snd pi); fst ` set pi \<inter> snd ` set pi = {}; y \<noteq> x; y \<sharp> Ys; y \<sharp> As; y \<sharp> pi; (y, b) \<in> set pi\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
a \<sharp> pi
(a, b) \<in> set pi

goal (1 subgoal):
 1. False
[PROOF STEP]
by(induct pi)
          (auto simp add: supp_list_cons supp_prod at_supp[OF at] fresh_list_cons fresh_prod at_fresh[OF at])
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinctPerm ((pi \<bullet> x, y) # pi)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> F = Ys \<and> set pi \<subseteq> F \<times> Ys \<and> finite Ys \<and> distinctPerm pi; insert x F \<subseteq> As; finite As\<rbrakk> \<Longrightarrow> \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x F = Ys \<and> set pi \<subseteq> insert x F \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
({y} \<union> Ys) \<sharp>* c
({y} \<union> Ys) \<inter> As = {}
((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)
finite ({y} \<union> Ys)
distinctPerm ((pi \<bullet> x, y) # pi)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
({y} \<union> Ys) \<sharp>* c
({y} \<union> Ys) \<inter> As = {}
((pi \<bullet> x, y) # pi) \<bullet> insert x Xs = {y} \<union> Ys
set ((pi \<bullet> x, y) # pi) \<subseteq> insert x Xs \<times> ({y} \<union> Ys)
finite ({y} \<union> Ys)
distinctPerm ((pi \<bullet> x, y) # pi)

goal (1 subgoal):
 1. \<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x Xs = Ys \<and> set pi \<subseteq> insert x Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Ys pi. Ys \<sharp>* c \<and> Ys \<inter> As = {} \<and> pi \<bullet> insert x Xs = Ys \<and> set pi \<subseteq> insert x Xs \<times> Ys \<and> finite Ys \<and> distinctPerm pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma at_set_avoiding:
  fixes Xs::"'a set"
  assumes at: "at TYPE('a)"
  and     a: "finite Xs"
  and     b: "finite ((supp c)::'a set)"
  obtains pi::"'a prm" where "(pi \<bullet> Xs) \<sharp>* c" and "set pi \<subseteq> Xs \<times> (pi \<bullet> Xs)" and "distinctPerm pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pi. \<lbrakk>(pi \<bullet> Xs) \<sharp>* c; set pi \<subseteq> Xs \<times> pi \<bullet> Xs; distinctPerm pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
finite Xs
finite (supp c)

goal (1 subgoal):
 1. (\<And>pi. \<lbrakk>(pi \<bullet> Xs) \<sharp>* c; set pi \<subseteq> Xs \<times> pi \<bullet> Xs; distinctPerm pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (frule_tac As="Xs" in at_set_avoiding_aux'[OF at]) auto


[STATEMENT]
lemma pt_swap:
  fixes x :: 'a
  and a :: 'x
  and b :: 'x

  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"

  shows "[(a, b)] \<bullet> x = [(b, a)] \<bullet> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(a, b)] \<bullet> x = [(b, a)] \<bullet> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(a, b)] \<bullet> x = [(b, a)] \<bullet> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(a, b)] \<bullet> x = [(b, a)] \<bullet> x
[PROOF STEP]
by(simp add: pt3[OF pt] at_ds5[OF at])
[PROOF STATE]
proof (state)
this:
[(a, b)] \<bullet> x = [(b, a)] \<bullet> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_subset:
  fixes Xs :: "'a::fs_name set"
  and   Ys :: "'a::fs_name set"

  assumes "Xs \<subseteq> Ys"
  and     "finite Xs"
  and     "finite Ys"

  shows "(supp Xs) \<subseteq> ((supp Ys)::name set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp Xs \<subseteq> supp Ys
[PROOF STEP]
proof(rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> supp Xs \<Longrightarrow> x \<in> supp Ys
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> supp Xs \<Longrightarrow> x \<in> supp Ys
[PROOF STEP]
assume "x \<in> ((supp Xs)::name set)"
[PROOF STATE]
proof (state)
this:
x \<in> supp Xs

goal (1 subgoal):
 1. \<And>x. x \<in> supp Xs \<Longrightarrow> x \<in> supp Ys
[PROOF STEP]
with \<open>finite Xs\<close>
[PROOF STATE]
proof (chain)
picking this:
finite Xs
x \<in> supp Xs
[PROOF STEP]
obtain X where "X \<in> Xs" and "x \<in> supp X"
[PROOF STATE]
proof (prove)
using this:
finite Xs
x \<in> supp Xs

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<in> Xs; x \<in> supp X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule supp_member[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
[PROOF STATE]
proof (state)
this:
X \<in> Xs
x \<in> supp X

goal (1 subgoal):
 1. \<And>x. x \<in> supp Xs \<Longrightarrow> x \<in> supp Ys
[PROOF STEP]
from \<open>X \<in> Xs\<close> \<open>Xs \<subseteq> Ys\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<in> Xs
Xs \<subseteq> Ys
[PROOF STEP]
have "X \<in> Ys"
[PROOF STATE]
proof (prove)
using this:
X \<in> Xs
Xs \<subseteq> Ys

goal (1 subgoal):
 1. X \<in> Ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<in> Ys

goal (1 subgoal):
 1. \<And>x. x \<in> supp Xs \<Longrightarrow> x \<in> supp Ys
[PROOF STEP]
with \<open>finite Ys\<close> \<open>x \<in> supp X\<close>
[PROOF STATE]
proof (chain)
picking this:
finite Ys
x \<in> supp X
X \<in> Ys
[PROOF STEP]
show "x \<in> supp Ys"
[PROOF STATE]
proof (prove)
using this:
finite Ys
x \<in> supp X
X \<in> Ys

goal (1 subgoal):
 1. x \<in> supp Ys
[PROOF STEP]
by(induct rule: finite_induct)
      (auto simp add: supp_fin_insert[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
[PROOF STATE]
proof (state)
this:
x \<in> supp Ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memFresh:
  fixes x :: name
  and   p :: "'a::fs_name"
  and   l :: "('a::fs_name) list"

  assumes "x \<sharp> l"
  and     "p mem l"

  shows "x \<sharp> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> l
p mem l

goal (1 subgoal):
 1. x \<sharp> p
[PROOF STEP]
by(induct l, auto simp add: fresh_list_cons)


[STATEMENT]
lemma memFreshChain:
  fixes xvec :: "name list"
  and   p    :: "'a::fs_name"
  and   l    :: "'a::fs_name list"
  and   Xs   :: "name set"

  assumes "p mem l"

  shows "xvec \<sharp>* l \<Longrightarrow> xvec \<sharp>* p"
  and   "Xs \<sharp>* l \<Longrightarrow> Xs \<sharp>* p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xvec \<sharp>* l \<Longrightarrow> xvec \<sharp>* p) &&& (Xs \<sharp>* l \<Longrightarrow> Xs \<sharp>* p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p mem l

goal (1 subgoal):
 1. (xvec \<sharp>* l \<Longrightarrow> xvec \<sharp>* p) &&& (Xs \<sharp>* l \<Longrightarrow> Xs \<sharp>* p)
[PROOF STEP]
by(auto simp add: fresh_star_def intro: memFresh)


[STATEMENT]
lemma fresh_star_list_append[simp]:
  fixes A :: "name list"
  and   B :: "name list"
  and   C :: "name list"

  shows "(A \<sharp>* (B @ C)) = ((A \<sharp>* B) \<and> (A \<sharp>* C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sharp>* (B @ C) = (A \<sharp>* B \<and> A \<sharp>* C)
[PROOF STEP]
by(auto simp add: fresh_star_def fresh_list_append)


[STATEMENT]
lemma unionSimps[simp]:
  fixes Xs :: "name set"
  and   Ys :: "name set"
  and   C  :: "'a::fs_name"

  shows "((Xs \<union> Ys) \<sharp>* C) = ((Xs \<sharp>* C) \<and> (Ys \<sharp>* C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Xs \<union> Ys) \<sharp>* C = (Xs \<sharp>* C \<and> Ys \<sharp>* C)
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma substFreshAux[simp]:
  fixes C    :: "'a::fs_name"
  and   xvec :: "name list"

  shows "xvec \<sharp>* (supp C - set xvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* (supp C - set xvec)
[PROOF STEP]
by(auto simp add: fresh_star_def fresh_def at_fin_set_supp[OF at_name_inst] fs_name1)


[STATEMENT]
lemma fresh_star_perm_app[simp]:
  fixes Xs :: "name set"
  and   xvec :: "name list"
  and   p  :: "name prm"
  and   C  :: "'d::fs_name"

  shows "\<lbrakk>Xs \<sharp>* p; Xs \<sharp>* C\<rbrakk> \<Longrightarrow> Xs \<sharp>* (p \<bullet> C)"
  and   "\<lbrakk>xvec \<sharp>* p; xvec \<sharp>* C\<rbrakk> \<Longrightarrow> xvec \<sharp>* (p \<bullet> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>Xs \<sharp>* p; Xs \<sharp>* C\<rbrakk> \<Longrightarrow> Xs \<sharp>* (p \<bullet> C)) &&& (\<lbrakk>xvec \<sharp>* p; xvec \<sharp>* C\<rbrakk> \<Longrightarrow> xvec \<sharp>* (p \<bullet> C))
[PROOF STEP]
by(auto simp add: fresh_star_def fresh_perm_app)


[STATEMENT]
lemma freshSets[simp]:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   X    :: "name set"
  and   C    :: 'a

  shows "([]::name list) \<sharp>* C"
  and   "([]::name list) \<sharp>* [y].C"
  and   "({}::name set) \<sharp>* C"
  and   "({}::name set) \<sharp>* [y].C"
  and   "((x#xvec) \<sharp>* C) = (x \<sharp> C \<and> xvec \<sharp>* C)"
  and   "((x#xvec) \<sharp>* ([y].C)) = (x \<sharp> ([y].C) \<and> xvec \<sharp>* ([y].C))"
  and   "((insert x X) \<sharp>* C) = (x \<sharp> C \<and> X \<sharp>* C)"
  and   "((insert x X) \<sharp>* ([y].C)) = (x \<sharp> ([y].C) \<and> X \<sharp>* ([y].C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (([] \<sharp>* C &&& [] \<sharp>* [y].C) &&& {} \<sharp>* C &&& {} \<sharp>* [y].C) &&& ((x # xvec) \<sharp>* C = (x \<sharp> C \<and> xvec \<sharp>* C) &&& (x # xvec) \<sharp>* [y].C = (x \<sharp> [y].C \<and> xvec \<sharp>* [y].C)) &&& insert x X \<sharp>* C = (x \<sharp> C \<and> X \<sharp>* C) &&& insert x X \<sharp>* [y].C = (x \<sharp> [y].C \<and> X \<sharp>* [y].C)
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma freshStarAtom[simp]: "(xvec::name list) \<sharp>* (x::name) = x \<sharp> xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* x = x \<sharp> xvec
[PROOF STEP]
by(induct xvec)
  (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)


[STATEMENT]
lemma name_list_set_fresh[simp]:
  fixes xvec :: "name list"
  and   x    :: "'a::fs_name"

  shows "(set xvec) \<sharp>* x = xvec \<sharp>* x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xvec \<sharp>* x = xvec \<sharp>* x
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma name_list_supp:
  fixes xvec :: "name list"

  shows "set xvec = supp xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
have "set xvec = supp(set xvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xvec = supp (set xvec)
[PROOF STEP]
by(simp add: at_fin_set_supp[OF at_name_inst])
[PROOF STATE]
proof (state)
this:
set xvec = supp (set xvec)

goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xvec = supp (set xvec)

goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
have "\<dots> = supp xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (set xvec) = supp xvec
[PROOF STEP]
by(simp add: pt_list_set_supp[OF pt_name_inst, OF at_name_inst, OF fs_name_inst])
[PROOF STATE]
proof (state)
this:
supp (set xvec) = supp xvec

goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set xvec = supp (set xvec)
supp (set xvec) = supp xvec
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set xvec = supp (set xvec)
supp (set xvec) = supp xvec

goal (1 subgoal):
 1. set xvec = supp xvec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set xvec = supp xvec

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_fresh_list_star:
  fixes xvec :: "name list"
  and   a    :: name
  and   P    :: "'a::fs_name"

  shows "(xvec \<sharp>* [a].P) = ((set xvec) - {a}) \<sharp>* P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* [a].P = (set xvec - {a}) \<sharp>* P
[PROOF STEP]
by(induct xvec) (auto simp add: fresh_star_def abs_fresh)


[STATEMENT]
lemma abs_fresh_set_star:
  fixes X :: "name set"
  and   a :: name
  and   P :: "'a::fs_name"

  shows "(X \<sharp>* [a].P) = (X - {a}) \<sharp>* P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<sharp>* [a].P = (X - {a}) \<sharp>* P
[PROOF STEP]
by(auto simp add: fresh_star_def abs_fresh)


[STATEMENT]
lemma abs_fresh_list_star'[simp]:
  fixes xvec :: "name list"
  and   a    :: name
  and   P    :: "'a::fs_name"

  assumes "a \<sharp> xvec"

  shows "xvec \<sharp>* [a].P = xvec \<sharp>* P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* [a].P = xvec \<sharp>* P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<sharp> xvec

goal (1 subgoal):
 1. xvec \<sharp>* [a].P = xvec \<sharp>* P
[PROOF STEP]
by(induct xvec) (auto simp add: abs_fresh fresh_list_cons fresh_atm)


[STATEMENT]
lemma freshChainSym[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"

  shows   "xvec \<sharp>* yvec = yvec \<sharp>* xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* yvec = yvec \<sharp>* xvec
[PROOF STEP]
by(auto simp add: fresh_star_def fresh_def name_list_supp)


[STATEMENT]
lemma name_set_avoiding:
  fixes c :: "'a::fs_name"
  and   X :: "name set"

  assumes "finite X"
  and     "\<And>pi::name prm. \<lbrakk>(pi \<bullet> X) \<sharp>* c; distinctPerm pi; set pi \<subseteq> X \<times> (pi \<bullet> X)\<rbrakk> \<Longrightarrow> thesis"

  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
\<lbrakk>(?pi \<bullet> X) \<sharp>* c; distinctPerm ?pi; set ?pi \<subseteq> X \<times> ?pi \<bullet> X\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule_tac c=c in at_set_avoiding[OF at_name_inst]) (simp_all add: fs_name1)


[STATEMENT]
lemma eqvtUnion[intro]:
  fixes Rel  :: "('d::fs_name) set"
  and   Rel' :: "'d set"

  assumes EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

  shows "eqvt (Rel \<union> Rel')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (Rel \<union> Rel')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
eqvt Rel'

goal (1 subgoal):
 1. eqvt (Rel \<union> Rel')
[PROOF STEP]
by(force simp add: eqvt_def)


[STATEMENT]
lemma eqvtPerm[simp]:
  fixes X :: "('d::fs_name) set"
  and   x :: name
  and   y :: name

  assumes "eqvt X"

  shows "([(x, y)] \<bullet> X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<bullet> X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqvt X

goal (1 subgoal):
 1. [(x, y)] \<bullet> X = X
[PROOF STEP]
apply(auto simp add: eqvt_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> [(x, y)] \<bullet> X\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(erule_tac x="[(x, y)] \<bullet> xa" in ballE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> [(x, y)] \<bullet> X; \<forall>p. p \<bullet> [(x, y)] \<bullet> xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa. \<lbrakk>xa \<in> [(x, y)] \<bullet> X; [(x, y)] \<bullet> xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> X
 3. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(erule_tac x="[(x, y)]" in allE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> [(x, y)] \<bullet> X; [(x, y)] \<bullet> [(x, y)] \<bullet> xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa. \<lbrakk>xa \<in> [(x, y)] \<bullet> X; [(x, y)] \<bullet> xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> X
 3. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> [(x, y)] \<bullet> X; [(x, y)] \<bullet> xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>[(x, y)] \<bullet> xa \<notin> X; [(x, y)] \<bullet> xa \<in> [(x, y)] \<bullet> [(x, y)] \<bullet> X\<rbrakk> \<Longrightarrow> xa \<in> X
 2. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>x\<in>X. \<forall>p. p \<bullet> x \<in> X; xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(erule_tac x=xa in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> X; \<forall>p. p \<bullet> xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
 2. \<And>xa. \<lbrakk>xa \<in> X; xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(erule_tac x="[(x, y)]" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> X; [(x, y)] \<bullet> xa \<in> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
 2. \<And>xa. \<lbrakk>xa \<in> X; xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply(drule_tac pi="[(x, y)]" and x="[(x, y)] \<bullet> xa" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> X; [(x, y)] \<bullet> [(x, y)] \<bullet> xa \<in> [(x, y)] \<bullet> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
 2. \<And>xa. \<lbrakk>xa \<in> X; xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> X; xa \<notin> X\<rbrakk> \<Longrightarrow> xa \<in> [(x, y)] \<bullet> X
[PROOF STEP]
by simp


[STATEMENT]
lemma eqvtI:
  fixes X :: "'d::fs_name set"
  and   x :: 'd
  and   p :: "name prm"

  assumes "eqvt X"
  and     "x \<in> X"

  shows "(p \<bullet> x) \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> x \<in> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqvt X
x \<in> X

goal (1 subgoal):
 1. p \<bullet> x \<in> X
[PROOF STEP]
by(unfold eqvt_def) auto


[STATEMENT]
lemma fresh_star_list_nil[simp]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"

  shows "xvec \<sharp>* []"
  and   "Xs \<sharp>* []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* [] &&& Xs \<sharp>* []
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma fresh_star_list_cons[simp]:
  fixes xvec :: "name list"
  and   Xs   :: "name set"
  and   x    :: "'a::fs_name"
  and   xs   :: "'a list"

  shows "(xvec \<sharp>* (x#xs)) = ((xvec \<sharp>* x) \<and> xvec \<sharp>* xs)"
  and   "(Xs \<sharp>* (x#xs)) = ((Xs \<sharp>* x) \<and> (Xs \<sharp>* xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* (x # xs) = (xvec \<sharp>* x \<and> xvec \<sharp>* xs) &&& Xs \<sharp>* (x # xs) = (Xs \<sharp>* x \<and> Xs \<sharp>* xs)
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma freshStarPair[simp]:
  fixes X    :: "name set"
  and   xvec :: "name list"
  and   x    :: "'a::fs_name"
  and   y    :: "'b::fs_name"

  shows "(X \<sharp>* (x, y)) = (X \<sharp>* x \<and> X \<sharp>* y)"
  and   "(xvec \<sharp>* (x, y)) = (xvec \<sharp>* x \<and> xvec \<sharp>* y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<sharp>* (x, y) = (X \<sharp>* x \<and> X \<sharp>* y) &&& xvec \<sharp>* (x, y) = (xvec \<sharp>* x \<and> xvec \<sharp>* y)
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma name_list_avoiding:
  fixes c    :: "'a::fs_name"
  and   xvec :: "name list"

  assumes "\<And>pi::name prm. \<lbrakk>(pi \<bullet> xvec) \<sharp>* c; distinctPerm pi; set pi \<subseteq> (set xvec) \<times> (set (pi \<bullet> xvec))\<rbrakk> \<Longrightarrow> thesis"

  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
have "finite(set xvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set xvec)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (set xvec)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (set xvec)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (set xvec)
\<lbrakk>(?pi \<bullet> xvec) \<sharp>* c; distinctPerm ?pi; set ?pi \<subseteq> set xvec \<times> set (?pi \<bullet> xvec)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule name_set_avoiding) (auto simp add: eqvts fresh_star_def)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinctPermSimps[simp]:
  fixes p :: "name prm"
  and   a :: name
  and   b :: name

  shows "distinctPerm([]::name prm)"
  and   "(distinctPerm((a, b)#p)) = (distinctPerm p \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinctPerm [] &&& distinctPerm ((a, b) # p) = (distinctPerm p \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p)
[PROOF STEP]
apply(simp add: distinctPerm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinctPerm ((a, b) # p) = (distinctPerm p \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p)
[PROOF STEP]
apply(induct p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinctPerm [(a, b)] = (distinctPerm [] \<and> a \<noteq> b \<and> a \<sharp> [] \<and> b \<sharp> [])
 2. \<And>aa p. distinctPerm ((a, b) # p) = (distinctPerm p \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p) \<Longrightarrow> distinctPerm ((a, b) # aa # p) = (distinctPerm (aa # p) \<and> a \<noteq> b \<and> a \<sharp> (aa # p) \<and> b \<sharp> (aa # p))
[PROOF STEP]
apply(unfold distinctPerm_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct (map fst [(a, b)] @ map snd [(a, b)]) = (distinct (map fst [] @ map snd []) \<and> a \<noteq> b \<and> a \<sharp> [] \<and> b \<sharp> [])
 2. \<And>aa p. distinct (map fst ((a, b) # p) @ map snd ((a, b) # p)) = (distinct (map fst p @ map snd p) \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p) \<Longrightarrow> distinct (map fst ((a, b) # aa # p) @ map snd ((a, b) # aa # p)) = (distinct (map fst (aa # p) @ map snd (aa # p)) \<and> a \<noteq> b \<and> a \<sharp> (aa # p) \<and> b \<sharp> (aa # p))
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa p. distinct (map fst ((a, b) # p) @ map snd ((a, b) # p)) = (distinct (map fst p @ map snd p) \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p) \<Longrightarrow> distinct (map fst ((a, b) # aa # p) @ map snd ((a, b) # aa # p)) = (distinct (map fst (aa # p) @ map snd (aa # p)) \<and> a \<noteq> b \<and> a \<sharp> (aa # p) \<and> b \<sharp> (aa # p))
[PROOF STEP]
apply(rule iffI, erule iffE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa p. \<lbrakk>distinct (map fst ((a, b) # aa # p) @ map snd ((a, b) # aa # p)); distinct (map fst ((a, b) # p) @ map snd ((a, b) # p)) \<longrightarrow> distinct (map fst p @ map snd p) \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p; distinct (map fst p @ map snd p) \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p \<longrightarrow> distinct (map fst ((a, b) # p) @ map snd ((a, b) # p))\<rbrakk> \<Longrightarrow> distinct (map fst (aa # p) @ map snd (aa # p)) \<and> a \<noteq> b \<and> a \<sharp> (aa # p) \<and> b \<sharp> (aa # p)
 2. \<And>aa p. \<lbrakk>distinct (map fst ((a, b) # p) @ map snd ((a, b) # p)) = (distinct (map fst p @ map snd p) \<and> a \<noteq> b \<and> a \<sharp> p \<and> b \<sharp> p); distinct (map fst (aa # p) @ map snd (aa # p)) \<and> a \<noteq> b \<and> a \<sharp> (aa # p) \<and> b \<sharp> (aa # p)\<rbrakk> \<Longrightarrow> distinct (map fst ((a, b) # aa # p) @ map snd ((a, b) # aa # p))
[PROOF STEP]
by(clarsimp)+


[STATEMENT]
lemma map_eqvt[eqvt]:
  fixes p   :: "name prm"
  and   lst :: "'a::pt_name list"

  shows "(p \<bullet> (map f lst)) = map (p \<bullet> f) (p \<bullet> lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> map f lst = map (p \<bullet> f) (p \<bullet> lst)
[PROOF STEP]
apply(induct lst, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a lst. p \<bullet> map f lst = map (p \<bullet> f) (p \<bullet> lst) \<Longrightarrow> p \<bullet> f a = (p \<bullet> f) (p \<bullet> a)
[PROOF STEP]
by(simp add: pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])


[STATEMENT]
lemma consPerm:
  fixes x :: name
  and   y :: name
  and   p :: "name prm"
  and   C :: "'a::pt_name"

  shows "((x, y)#p) \<bullet> C = [(x, y)] \<bullet> p \<bullet> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) # p) \<bullet> C = [(x, y)] \<bullet> p \<bullet> C
[PROOF STEP]
by(simp add: pt2[OF pt_name_inst, THEN sym])


[STATEMENT]
lemma distinctEqvt[eqvt]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "(p \<bullet> (distinct xs)) = distinct (p \<bullet> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> distinct xs = distinct (p \<bullet> xs)
[PROOF STEP]
by(induct xs) (auto simp add: eqvts)


[STATEMENT]
lemma distinctClosed[simp]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "distinct (p \<bullet> xs) = distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (p \<bullet> xs) = distinct xs
[PROOF STEP]
apply(induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct (p \<bullet> []) = distinct []
 2. \<And>a xs. distinct (p \<bullet> xs) = distinct xs \<Longrightarrow> distinct (p \<bullet> (a # xs)) = distinct (a # xs)
[PROOF STEP]
apply(auto simp add: eqvts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); p \<bullet> a \<notin> set (p \<bullet> xs); distinct xs; a mem xs\<rbrakk> \<Longrightarrow> False
 2. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); a \<notin> set xs; distinct xs; p \<bullet> a mem p \<bullet> xs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule_tac pi=p in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); p \<bullet> a \<notin> set (p \<bullet> xs); distinct xs; p \<bullet> a \<in> p \<bullet> set xs\<rbrakk> \<Longrightarrow> False
 2. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); a \<notin> set xs; distinct xs; p \<bullet> a mem p \<bullet> xs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add: eqvts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); a \<notin> set xs; distinct xs; p \<bullet> a mem p \<bullet> xs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule_tac pi="rev p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>distinct (p \<bullet> xs); a \<notin> set xs; distinct xs; rev p \<bullet> p \<bullet> a \<in> rev p \<bullet> set (p \<bullet> xs)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(simp add: eqvts)


[STATEMENT]
lemma lengthEqvt[eqvt]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> length xs = length (p \<bullet> xs)
[PROOF STEP]
by(induct xs) (auto simp add: eqvts)


[STATEMENT]
lemma lengthClosed[simp]:
  fixes p  :: "name prm"
  and   xs :: "'a::pt_name list"

  shows "length (p \<bullet> xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (p \<bullet> xs) = length xs
[PROOF STEP]
by(induct xs) (auto simp add: eqvts)


[STATEMENT]
lemma subsetEqvt[eqvt]:
  fixes p :: "name prm"
  and   S :: "('a::pt_name) set"
  and   T :: "('a::pt_name) set"

  shows "(p \<bullet> (S \<subseteq> T)) = ((p \<bullet> S) \<subseteq> (p \<bullet> T))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> (S \<subseteq> T) = (p \<bullet> S \<subseteq> p \<bullet> T)
[PROOF STEP]
by(rule pt_subseteq_eqvt[OF pt_name_inst, OF at_name_inst])


[STATEMENT]
lemma subsetClosed[simp]:
  fixes p :: "name prm"
  and   S :: "('a::pt_name) set"
  and   T :: "('a::pt_name) set"

  shows "((p \<bullet> S) \<subseteq> (p \<bullet> T)) = (S \<subseteq> T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> S \<subseteq> p \<bullet> T) = (S \<subseteq> T)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>p \<bullet> S \<subseteq> p \<bullet> T; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> T
 2. \<And>x. \<lbrakk>S \<subseteq> T; x \<in> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(drule_tac pi=p in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>p \<bullet> S \<subseteq> p \<bullet> T; p \<bullet> x \<in> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> T
 2. \<And>x. \<lbrakk>S \<subseteq> T; x \<in> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(insert pt_set_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>p \<bullet> S \<subseteq> p \<bullet> T; p \<bullet> x \<in> p \<bullet> S; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X)\<rbrakk> \<Longrightarrow> x \<in> T
 2. \<And>x. \<lbrakk>S \<subseteq> T; x \<in> p \<bullet> S; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X)\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; x \<in> p \<bullet> S; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X)\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(drule_tac pi="rev p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> rev p \<bullet> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(subgoal_tac "rev p \<bullet> x \<in> T")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> S; rev p \<bullet> x \<in> T\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
 2. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> S\<rbrakk> \<Longrightarrow> rev p \<bullet> x \<in> T
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> S; rev p \<bullet> x \<in> T\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(drule_tac pi="p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> T; p \<bullet> rev p \<bullet> x \<in> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); rev p \<bullet> x \<in> T; x \<in> p \<bullet> S\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
apply(drule_tac pi="p" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>S \<subseteq> T; \<And>pi x X. (pi \<bullet> x \<in> pi \<bullet> X) = (x \<in> X); x \<in> p \<bullet> S; p \<bullet> rev p \<bullet> x \<in> p \<bullet> T\<rbrakk> \<Longrightarrow> x \<in> p \<bullet> T
[PROOF STEP]
by auto


[STATEMENT]
lemma subsetClosed'[simp]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   P    :: "'a::fs_name"

  shows "(set (p \<bullet> xvec) \<subseteq> supp (p \<bullet> P)) = (set xvec \<subseteq> supp P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (p \<bullet> xvec) \<subseteq> supp (p \<bullet> P)) = (set xvec \<subseteq> supp P)
[PROOF STEP]
by(simp add: eqvts[THEN sym])


[STATEMENT]
lemma memEqvt[eqvt]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   xs :: "('a::pt_name) list"

  shows "(p \<bullet> (x mem xs)) = ((p \<bullet> x) mem (p \<bullet> xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> x mem xs = p \<bullet> x mem p \<bullet> xs
[PROOF STEP]
by(induct xs)
  (auto simp add: pt_bij[OF pt_name_inst, OF at_name_inst] eqvts)


[STATEMENT]
lemma memClosed[simp]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   xs :: "('a::pt_name) list"

  shows "(p \<bullet> x) mem (p \<bullet> xs) = (x mem xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> x mem p \<bullet> xs = x mem xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<bullet> x mem p \<bullet> xs = x mem xs
[PROOF STEP]
have "x mem xs = p \<bullet> (x mem xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mem xs = p \<bullet> x mem xs
[PROOF STEP]
by(case_tac "x mem xs") auto
[PROOF STATE]
proof (state)
this:
x mem xs = p \<bullet> x mem xs

goal (1 subgoal):
 1. p \<bullet> x mem p \<bullet> xs = x mem xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x mem xs = p \<bullet> x mem xs

goal (1 subgoal):
 1. p \<bullet> x mem p \<bullet> xs = x mem xs
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> x mem p \<bullet> xs = x mem xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memClosed'[simp]:
  fixes p  :: "name prm"
  and   x  :: "'a::pt_name"
  and   y  :: "'b::pt_name"
  and   xs :: "('a \<times>  'b) list"

  shows "((p \<bullet> x, p \<bullet> y) mem (p \<bullet> xs)) = ((x, y) mem xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> x, p \<bullet> y) mem p \<bullet> xs = (x, y) mem xs
[PROOF STEP]
apply(subgoal_tac "((x, y) mem xs) = (p \<bullet> (x, y)) mem (p \<bullet> xs)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x, y) mem xs = p \<bullet> (x, y) mem p \<bullet> xs \<Longrightarrow> (p \<bullet> x, p \<bullet> y) mem p \<bullet> xs = (x, y) mem xs
 2. (x, y) mem xs = p \<bullet> (x, y) mem p \<bullet> xs
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) mem xs = p \<bullet> (x, y) mem p \<bullet> xs
[PROOF STEP]
by(force simp del: eqvts)


[STATEMENT]
lemma freshPerm:
  fixes x :: name
  and   p :: "name prm"

  assumes "x \<sharp> p"

  shows "p \<bullet> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> x = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> p

goal (1 subgoal):
 1. p \<bullet> x = x
[PROOF STEP]
apply(rule_tac pt_pi_fresh_fresh[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> p \<Longrightarrow> \<forall>(a, b)\<in>set p. a \<sharp> x \<and> b \<sharp> x
[PROOF STEP]
by(induct p, auto simp add: fresh_list_cons fresh_prod)


[STATEMENT]
lemma freshChainPermSimp:
  fixes xvec :: "name list"
  and   p    :: "name prm"

  assumes "xvec \<sharp>* p"

  shows "p \<bullet> xvec = xvec"
  and   "rev p \<bullet> xvec = xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> xvec = xvec &&& rev p \<bullet> xvec = xvec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* p

goal (1 subgoal):
 1. p \<bullet> xvec = xvec &&& rev p \<bullet> xvec = xvec
[PROOF STEP]
by(induct xvec) (auto simp add: freshPerm pt_bij1[OF pt_name_inst, OF at_name_inst, THEN sym])


[STATEMENT]
lemma freshChainAppend[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   C    :: "'a::fs_name"

  shows "(xvec@yvec) \<sharp>* C = ((xvec \<sharp>* C) \<and> (yvec \<sharp>* C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xvec @ yvec) \<sharp>* C = (xvec \<sharp>* C \<and> yvec \<sharp>* C)
[PROOF STEP]
by(force simp add: fresh_star_def)


[STATEMENT]
lemma subsetFresh:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   C    :: "'d::fs_name"

  assumes "set xvec \<subseteq> set yvec"
  and     "yvec \<sharp>* C"

  shows "xvec \<sharp>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set xvec \<subseteq> set yvec
yvec \<sharp>* C

goal (1 subgoal):
 1. xvec \<sharp>* C
[PROOF STEP]
by(auto simp add: fresh_star_def)


[STATEMENT]
lemma distinctPermCancel[simp]:
  fixes p :: "name prm"
  and   T :: "'a::pt_name"

  assumes "distinctPerm p"

  shows "(p \<bullet> (p \<bullet> T)) = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> p \<bullet> T = T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinctPerm p

goal (1 subgoal):
 1. p \<bullet> p \<bullet> T = T
[PROOF STEP]
proof(induct p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinctPerm [] \<Longrightarrow> [] \<bullet> [] \<bullet> T = T
 2. \<And>a p. \<lbrakk>distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T; distinctPerm (a # p)\<rbrakk> \<Longrightarrow> (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distinctPerm []

goal (2 subgoals):
 1. distinctPerm [] \<Longrightarrow> [] \<bullet> [] \<bullet> T = T
 2. \<And>a p. \<lbrakk>distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T; distinctPerm (a # p)\<rbrakk> \<Longrightarrow> (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<bullet> [] \<bullet> T = T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<bullet> [] \<bullet> T = T

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T; distinctPerm (a # p)\<rbrakk> \<Longrightarrow> (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. \<lbrakk>distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T; distinctPerm (a # p)\<rbrakk> \<Longrightarrow> (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
case(Cons a p)
[PROOF STATE]
proof (state)
this:
distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T
distinctPerm (a # p)

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T; distinctPerm (a # p)\<rbrakk> \<Longrightarrow> (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinctPerm p \<Longrightarrow> p \<bullet> p \<bullet> T = T
distinctPerm (a # p)

goal (1 subgoal):
 1. (a # p) \<bullet> (a # p) \<bullet> T = T
[PROOF STEP]
proof(case_tac a, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>a = (aa, b); p \<bullet> p \<bullet> T = T; distinctPerm p; aa \<noteq> b; aa \<sharp> p; b \<sharp> p\<rbrakk> \<Longrightarrow> [(aa, b)] \<bullet> p \<bullet> [(aa, b)] \<bullet> p \<bullet> T = T
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>a__ = (aa, b); p \<bullet> p \<bullet> T = T; distinctPerm p; aa \<noteq> b; aa \<sharp> p; b \<sharp> p\<rbrakk> \<Longrightarrow> [(aa, b)] \<bullet> p \<bullet> [(aa, b)] \<bullet> p \<bullet> T = T
[PROOF STEP]
assume "(a::name) \<sharp> (p::name prm)" "b \<sharp> p" "p \<bullet> p \<bullet> T = T" "a \<noteq> b"
[PROOF STATE]
proof (state)
this:
a \<sharp> p
b \<sharp> p
p \<bullet> p \<bullet> T = T
a \<noteq> b

goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>a__ = (aa, b); p \<bullet> p \<bullet> T = T; distinctPerm p; aa \<noteq> b; aa \<sharp> p; b \<sharp> p\<rbrakk> \<Longrightarrow> [(aa, b)] \<bullet> p \<bullet> [(aa, b)] \<bullet> p \<bullet> T = T
[PROOF STEP]
thus "[(a, b)] \<bullet> p \<bullet> [(a, b)] \<bullet> p \<bullet> T = T"
[PROOF STATE]
proof (prove)
using this:
a \<sharp> p
b \<sharp> p
p \<bullet> p \<bullet> T = T
a \<noteq> b

goal (1 subgoal):
 1. [(a, b)] \<bullet> p \<bullet> [(a, b)] \<bullet> p \<bullet> T = T
[PROOF STEP]
by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst]) simp
[PROOF STATE]
proof (state)
this:
[(a, b)] \<bullet> p \<bullet> [(a, b)] \<bullet> p \<bullet> T = T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a # p) \<bullet> (a # p) \<bullet> T = T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma composePermInduct[consumes 1, case_names cBase cStep]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   P    :: "name list \<Rightarrow> name list \<Rightarrow> bool"

  assumes L: "length xvec = length yvec"
  and     rBase: "P [] []"
  and     rStep: "\<And>x xvec y yvec. \<lbrakk>length xvec = length yvec; P xvec yvec\<rbrakk> \<Longrightarrow> P (x # xvec) (y # yvec)"

  shows "P xvec yvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xvec yvec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
P [] []
\<lbrakk>length ?xvec = length ?yvec; P ?xvec ?yvec\<rbrakk> \<Longrightarrow> P (?x # ?xvec) (?y # ?yvec)

goal (1 subgoal):
 1. P xvec yvec
[PROOF STEP]
by(induct rule: composePerm.induct) auto


[STATEMENT]
lemma composePermEqvt[eqvt]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   yvec :: "name list"

  shows "(p \<bullet> (composePerm xvec yvec)) = composePerm (p \<bullet> xvec) (p \<bullet> yvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> composePerm xvec yvec = composePerm (p \<bullet> xvec) (p \<bullet> yvec)
[PROOF STEP]
by(induct xvec yvec rule: composePerm.induct) auto


[STATEMENT]
lemma permChainSimps[simp]:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   perm :: "name prm"
  and   p    :: "'a::pt_name"

  shows "((composePerm xvec yvec) @ perm) \<bullet> p = [xvec yvec] \<bullet>\<^sub>v (perm \<bullet> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (composePerm xvec yvec @ perm) \<bullet> p = [xvec yvec] \<bullet>\<^sub>v perm \<bullet> p
[PROOF STEP]
by(simp add: pt2[OF pt_name_inst])


[STATEMENT]
lemma permChainEqvt[eqvt]:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: "'a::pt_name"

  shows "(p \<bullet> ([xvec yvec] \<bullet>\<^sub>v x)) = [(p \<bullet> xvec) (p \<bullet> yvec)] \<bullet>\<^sub>v (p \<bullet> x)"
  and   "(p \<bullet> ([xvec yvec]\<^sup>- \<bullet>\<^sub>v x)) = [(p \<bullet> xvec) (p \<bullet> yvec)]\<^sup>- \<bullet>\<^sub>v (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> [xvec yvec] \<bullet>\<^sub>v x = [p \<bullet> xvec p \<bullet> yvec] \<bullet>\<^sub>v p \<bullet> x &&& p \<bullet> [xvec yvec]\<^sup>- \<bullet>\<^sub>v x = [p \<bullet> xvec p \<bullet> yvec]\<^sup>- \<bullet>\<^sub>v p \<bullet> x
[PROOF STEP]
by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst], simp add: eqvts rev_eqvt)+


[STATEMENT]
lemma permChainBij:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"
  and   q    :: "'a::pt_name"

  assumes "length xvec = length yvec"

  shows "(([xvec yvec] \<bullet>\<^sub>v p) = ([xvec yvec] \<bullet>\<^sub>v q)) = (p = q)"
  and   "(([xvec yvec]\<^sup>- \<bullet>\<^sub>v p) = ([xvec yvec]\<^sup>- \<bullet>\<^sub>v q)) = (p = q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([xvec yvec] \<bullet>\<^sub>v p = [xvec yvec] \<bullet>\<^sub>v q) = (p = q) &&& ([xvec yvec]\<^sup>- \<bullet>\<^sub>v p = [xvec yvec]\<^sup>- \<bullet>\<^sub>v q) = (p = q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec

goal (1 subgoal):
 1. ([xvec yvec] \<bullet>\<^sub>v p = [xvec yvec] \<bullet>\<^sub>v q) = (p = q) &&& ([xvec yvec]\<^sup>- \<bullet>\<^sub>v p = [xvec yvec]\<^sup>- \<bullet>\<^sub>v q) = (p = q)
[PROOF STEP]
by(induct rule: composePermInduct)
  (auto simp add: pt_bij[OF pt_name_inst, OF at_name_inst])


[STATEMENT]
lemma permChainAppend:
  fixes xvec1 :: "name list"
  and   yvec1 :: "name list"
  and   xvec2 :: "name list"
  and   yvec2 :: "name list"
  and   p     :: "'a::pt_name"

  assumes "length xvec1 = length yvec1"

  shows "([(xvec1@xvec2) (yvec1@yvec2)] \<bullet>\<^sub>v p) = [xvec1 yvec1] \<bullet>\<^sub>v [xvec2 yvec2] \<bullet>\<^sub>v p"
  and   "([(xvec1@xvec2) (yvec1@yvec2)]\<^sup>- \<bullet>\<^sub>v p) = [xvec2 yvec2]\<^sup>- \<bullet>\<^sub>v [xvec1 yvec1]\<^sup>- \<bullet>\<^sub>v p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(xvec1 @ xvec2) (yvec1 @ yvec2)] \<bullet>\<^sub>v p = [xvec1 yvec1] \<bullet>\<^sub>v [xvec2 yvec2] \<bullet>\<^sub>v p &&& [(xvec1 @ xvec2) (yvec1 @ yvec2)]\<^sup>- \<bullet>\<^sub>v p = [xvec2 yvec2]\<^sup>- \<bullet>\<^sub>v [xvec1 yvec1]\<^sup>- \<bullet>\<^sub>v p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec1 = length yvec1

goal (1 subgoal):
 1. [(xvec1 @ xvec2) (yvec1 @ yvec2)] \<bullet>\<^sub>v p = [xvec1 yvec1] \<bullet>\<^sub>v [xvec2 yvec2] \<bullet>\<^sub>v p &&& [(xvec1 @ xvec2) (yvec1 @ yvec2)]\<^sup>- \<bullet>\<^sub>v p = [xvec2 yvec2]\<^sup>- \<bullet>\<^sub>v [xvec1 yvec1]\<^sup>- \<bullet>\<^sub>v p
[PROOF STEP]
by(induct arbitrary: p rule: composePermInduct, auto) (simp add: pt2[OF pt_name_inst])


[STATEMENT]
lemma calcChainAtom:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name

  assumes "length xvec = length yvec"
  and     "x \<sharp> xvec"
  and     "x \<sharp> yvec"

  shows "[xvec yvec] \<bullet>\<^sub>v x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v x = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
x \<sharp> xvec
x \<sharp> yvec

goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v x = x
[PROOF STEP]
by(induct rule: composePermInduct, auto)


[STATEMENT]
lemma calcChainAtomRev:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   x    :: name

  assumes "length xvec = length yvec"
  and     "x \<sharp> xvec"
  and     "x \<sharp> yvec"

  shows "[xvec yvec]\<^sup>- \<bullet>\<^sub>v x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [xvec yvec]\<^sup>- \<bullet>\<^sub>v x = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xvec = length yvec
x \<sharp> xvec
x \<sharp> yvec

goal (1 subgoal):
 1. [xvec yvec]\<^sup>- \<bullet>\<^sub>v x = x
[PROOF STEP]
by(induct rule: composePermInduct, auto)
  (auto simp add: pt2[OF pt_name_inst] fresh_list_cons calc_atm)


[STATEMENT]
lemma chainFreshFresh:
  fixes x    :: name
  and   y    :: name
  and   xvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "x \<sharp> xvec"
  and     "y \<sharp> xvec"

  shows "xvec \<sharp>* ([(x, y)] \<bullet> p) = (xvec \<sharp>* p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> p) = xvec \<sharp>* p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> xvec
y \<sharp> xvec

goal (1 subgoal):
 1. xvec \<sharp>* ([(x, y)] \<bullet> p) = xvec \<sharp>* p
[PROOF STEP]
by(induct xvec) (auto simp add: fresh_list_cons fresh_left)


[STATEMENT]
lemma permChainFreshFresh:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "xvec \<sharp>* p"
  and     "yvec \<sharp>* p"
  and     "length xvec = length yvec"

  shows "[xvec yvec] \<bullet>\<^sub>v p = p"
  and   "[xvec yvec]\<^sup>- \<bullet>\<^sub>v p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v p = p &&& [xvec yvec]\<^sup>- \<bullet>\<^sub>v p = p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* p
yvec \<sharp>* p
length xvec = length yvec

goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v p = p &&& [xvec yvec]\<^sup>- \<bullet>\<^sub>v p = p
[PROOF STEP]
by(induct rule: composePerm.induct, auto) (simp add: pt2[OF pt_name_inst])


[STATEMENT]
lemma setFresh[simp]:
  fixes x    :: name
  and   xvec :: "name list"

  shows "x \<notin> set xvec = x \<sharp> xvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> set xvec) = x \<sharp> xvec
[PROOF STEP]
by(simp add: name_list_supp fresh_def)


[STATEMENT]
lemma calcChain:
  fixes xvec :: "name list"
  and   yvec :: "name list"

  assumes "yvec \<sharp>* xvec"
  and     "length xvec = length yvec"
  and     "distinct xvec"
  and     "distinct yvec"

  shows "[xvec yvec] \<bullet>\<^sub>v xvec = yvec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v xvec = yvec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* xvec
length xvec = length yvec
distinct xvec
distinct yvec

goal (1 subgoal):
 1. [xvec yvec] \<bullet>\<^sub>v xvec = yvec
[PROOF STEP]
by(induct xvec yvec rule: composePerm.induct, auto)
  (subst consPerm, simp add: calcChainAtom calc_atm name_list_supp fresh_def[symmetric])+