[STATEMENT]
lemma equiv_domain_permutation:
  "equiv (A \<rightarrow>\<^sub>E B) (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv (A \<rightarrow>\<^sub>E B) (domain_permutation A B)
[PROOF STEP]
proof (rule equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. refl_on (A \<rightarrow>\<^sub>E B) (domain_permutation A B)
 2. sym (domain_permutation A B)
 3. trans (domain_permutation A B)
[PROOF STEP]
show "refl_on (A \<rightarrow>\<^sub>E B) (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on (A \<rightarrow>\<^sub>E B) (domain_permutation A B)
[PROOF STEP]
proof (rule refl_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. domain_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
 2. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> domain_permutation A B
[PROOF STEP]
show "domain_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))} \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)

goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> domain_permutation A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> domain_permutation A B
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> domain_permutation A B
[PROOF STEP]
assume "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> domain_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "(f, f) \<in> domain_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. (f, f) \<in> domain_permutation A B
[PROOF STEP]
using permutes_id
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
id permutes ?S

goal (1 subgoal):
 1. (f, f) \<in> domain_permutation A B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
id permutes ?S

goal (1 subgoal):
 1. (f, f) \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(f, f) \<in> domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
refl_on (A \<rightarrow>\<^sub>E B) (domain_permutation A B)

goal (2 subgoals):
 1. sym (domain_permutation A B)
 2. trans (domain_permutation A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sym (domain_permutation A B)
 2. trans (domain_permutation A B)
[PROOF STEP]
show "sym (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (domain_permutation A B)
[PROOF STEP]
proof (rule symI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> domain_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B" "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
from \<open>p permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes A
[PROOF STEP]
have "inv p permutes A"
[PROOF STATE]
proof (prove)
using this:
p permutes A

goal (1 subgoal):
 1. inv p permutes A
[PROOF STEP]
by (simp add: permutes_inv)
[PROOF STATE]
proof (state)
this:
inv p permutes A

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv p permutes A

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
from \<open>p permutes A\<close> \<open>\<forall>x\<in>A. f x = f' (p x)\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
[PROOF STEP]
have "\<forall>x\<in>A. f' x = f (inv p x)"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
using permutes_in_image permutes_inverses(1)
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
?p permutes ?S \<Longrightarrow> (?p ?x \<in> ?S) = (?x \<in> ?S)
?p permutes ?S \<Longrightarrow> ?p (inv ?p ?x) = ?x

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_permutation A B \<Longrightarrow> (b, a) \<in> domain_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes A
\<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
show "(f', f) \<in> domain_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes A
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. (f', f) \<in> domain_permutation A B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes A
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. (f', f) \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f', f) \<in> domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sym (domain_permutation A B)

goal (1 subgoal):
 1. trans (domain_permutation A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (domain_permutation A B)
[PROOF STEP]
show "trans (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (domain_permutation A B)
[PROOF STEP]
proof (rule transI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
fix f f' f''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B" "(f', f'') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B
(f', f'') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
from \<open>(f', f'') \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
(f', f'') \<in> domain_permutation A B
[PROOF STEP]
obtain p' where "p' permutes A" and "\<forall>x\<in>A. f' x = f'' (p' x)"
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' permutes A; \<forall>x\<in>A. f' x = f'' (p' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' permutes A; \<forall>x\<in>A. f' x = f'' (p' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' permutes A
\<forall>x\<in>A. f' x = f'' (p' x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> domain_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
from \<open>(f', f'') \<in> domain_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f', f'') \<in> domain_permutation A B
[PROOF STEP]
have "f'' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> domain_permutation A B

goal (1 subgoal):
 1. f'' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. f'' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f'' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f'' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
from \<open>p permutes A\<close> \<open>p' permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes A
p' permutes A
[PROOF STEP]
have "(p' \<circ> p) permutes A"
[PROOF STATE]
proof (prove)
using this:
p permutes A
p' permutes A

goal (1 subgoal):
 1. p' \<circ> p permutes A
[PROOF STEP]
by (simp add: permutes_compose)
[PROOF STATE]
proof (state)
this:
p' \<circ> p permutes A

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p' \<circ> p permutes A

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
have "\<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = f' (p x)\<close> \<open>\<forall>x\<in>A. f' x = f'' (p' x)\<close> \<open>p permutes A\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = f' (p x)
\<forall>x\<in>A. f' x = f'' (p' x)
p permutes A

goal (1 subgoal):
 1. \<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)
[PROOF STEP]
by (simp add: permutes_in_image)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_permutation A B; (y, z) \<in> domain_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p' \<circ> p permutes A
\<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)
[PROOF STEP]
show "(f, f'') \<in> domain_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p' \<circ> p permutes A
\<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)

goal (1 subgoal):
 1. (f, f'') \<in> domain_permutation A B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p' \<circ> p permutes A
\<forall>x\<in>A. f x = f'' ((p' \<circ> p) x)

goal (1 subgoal):
 1. (f, f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f, f'') \<in> domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trans (domain_permutation A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_respects_domain_permutation:
  "(\<lambda>f. inj_on f A) respects domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. inj_on f A) respects domain_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where p: "p permutes A" "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
have inv_p: "\<forall>x\<in>A. f' x = f (inv p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
by (metis permutes_inverses(1) permutes_not_in)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
show "inj_on f A \<longleftrightarrow> inj_on f' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f A \<Longrightarrow> inj_on f' A
 2. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
assume "inj_on f A"
[PROOF STATE]
proof (state)
this:
inj_on f A

goal (2 subgoals):
 1. inj_on f A \<Longrightarrow> inj_on f' A
 2. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
show "inj_on f' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f' A
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a a'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "a \<in> A" "a' \<in> A" "f' a = f' a'"
[PROOF STATE]
proof (state)
this:
a \<in> A
a' \<in> A
f' a = f' a'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from this \<open>p permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
a' \<in> A
f' a = f' a'
p permutes A
[PROOF STEP]
have "inv p a \<in> A" "inv p a' \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
a' \<in> A
f' a = f' a'
p permutes A

goal (1 subgoal):
 1. inv p a \<in> A &&& inv p a' \<in> A
[PROOF STEP]
by (simp add:  permutes_in_image permutes_inv)+
[PROOF STATE]
proof (state)
this:
inv p a \<in> A
inv p a' \<in> A

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "f (inv p a) = f (inv p a')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (inv p a) = f (inv p a')
[PROOF STEP]
using \<open>f' a = f' a'\<close> \<open>a \<in> A\<close> \<open>a' \<in> A\<close> inv_p
[PROOF STATE]
proof (prove)
using this:
f' a = f' a'
a \<in> A
a' \<in> A
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. f (inv p a) = f (inv p a')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (inv p a) = f (inv p a')

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from \<open>inj_on f A\<close> this \<open>inv p a \<in> A\<close> \<open>inv p a' \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on f A
f (inv p a) = f (inv p a')
inv p a \<in> A
inv p a' \<in> A
[PROOF STEP]
have "inv p a = inv p a'"
[PROOF STATE]
proof (prove)
using this:
inj_on f A
f (inv p a) = f (inv p a')
inv p a \<in> A
inv p a' \<in> A

goal (1 subgoal):
 1. inv p a = inv p a'
[PROOF STEP]
using inj_on_contraD
[PROOF STATE]
proof (prove)
using this:
inj_on f A
f (inv p a) = f (inv p a')
inv p a \<in> A
inv p a' \<in> A
\<lbrakk>inj_on ?f ?A; ?x \<noteq> ?y; ?x \<in> ?A; ?y \<in> ?A\<rbrakk> \<Longrightarrow> ?f ?x \<noteq> ?f ?y

goal (1 subgoal):
 1. inv p a = inv p a'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv p a = inv p a'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; f' x = f' y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
inv p a = inv p a'
[PROOF STEP]
show "a = a'"
[PROOF STATE]
proof (prove)
using this:
inv p a = inv p a'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
by (metis \<open>p permutes A\<close> permutes_inverses(1))
[PROOF STATE]
proof (state)
this:
a = a'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on f' A

goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
assume "inj_on f' A"
[PROOF STATE]
proof (state)
this:
inj_on f' A

goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
from this p
[PROOF STATE]
proof (chain)
picking this:
inj_on f' A
p permutes A
\<forall>x\<in>A. f x = f' (p x)
[PROOF STEP]
show "inj_on f A"
[PROOF STATE]
proof (prove)
using this:
inj_on f' A
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. inj_on f A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. f' x = f' y \<longrightarrow> x = y
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by (metis inj_on_contraD permutes_in_image permutes_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on f A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on f A = inj_on f' A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma image_respects_domain_permutation:
  "(\<lambda>f. f ` A) respects (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. f ` A) respects domain_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> y ` A = z ` A
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> y ` A = z ` A
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> y ` A = z ` A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where p: "p permutes A" and f_eq: "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> y ` A = z ` A
[PROOF STEP]
show "f ` A = f' ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = f' ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` A \<subseteq> f' ` A
 2. f' ` A \<subseteq> f ` A
[PROOF STEP]
from p f_eq
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
[PROOF STEP]
show "f ` A \<subseteq> f' ` A"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. f ` A \<subseteq> f' ` A
[PROOF STEP]
by (auto simp add: permutes_in_image)
[PROOF STATE]
proof (state)
this:
f ` A \<subseteq> f' ` A

goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
from \<open>p permutes A\<close> \<open>\<forall>x\<in>A. f x = f' (p x)\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
[PROOF STEP]
have "\<forall>x\<in>A. f' x = f (inv p x)"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
using permutes_in_image permutes_inverses(1)
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
?p permutes ?S \<Longrightarrow> (?p ?x \<in> ?S) = (?x \<in> ?S)
?p permutes ?S \<Longrightarrow> ?p (inv ?p ?x) = ?x

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>A. f' x = f (inv p x)
[PROOF STEP]
show "f' ` A \<subseteq> f ` A"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f' x = f (inv p x)

goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
using \<open>p permutes A\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f' x = f (inv p x)
p permutes A

goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
by (auto simp add: permutes_inv permutes_in_image)
[PROOF STATE]
proof (state)
this:
f' ` A \<subseteq> f ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ` A = f' ` A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surjective_respects_domain_permutation:
  "(\<lambda>f. f ` A = B) respects domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. f ` A = B) respects domain_permutation A B
[PROOF STEP]
by (metis image_respects_domain_permutation congruentD congruentI)


[STATEMENT]
lemma bij_betw_respects_domain_permutation:
  "(\<lambda>f. bij_betw f A B) respects domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. bij_betw f A B) respects domain_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
have "bij_betw f A B \<longleftrightarrow> bij_betw (f' o p) A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B = bij_betw (f' \<circ> p) A B
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = f' (p x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. bij_betw f A B = bij_betw (f' \<circ> p) A B
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) bij_betw_cong comp_apply)
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw (f' \<circ> p) A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw (f' \<circ> p) A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
have "... \<longleftrightarrow> bij_betw f' A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (f' \<circ> p) A B = bij_betw f' A B
[PROOF STEP]
using \<open>p permutes A\<close>
[PROOF STATE]
proof (prove)
using this:
p permutes A

goal (1 subgoal):
 1. bij_betw (f' \<circ> p) A B = bij_betw f' A B
[PROOF STEP]
by (auto intro!: bij_betw_comp_iff[symmetric] permutes_imp_bij)
[PROOF STATE]
proof (state)
this:
bij_betw (f' \<circ> p) A B = bij_betw f' A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bij_betw f A B = bij_betw f' A B
[PROOF STEP]
show "bij_betw f A B \<longleftrightarrow> bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw f A B = bij_betw f' A B

goal (1 subgoal):
 1. bij_betw f A B = bij_betw f' A B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw f' A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma image_mset_respects_domain_permutation:
  shows "(\<lambda>f. image_mset f (mset_set A)) respects (domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. image_mset f (mset_set A)) respects domain_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> image_mset y (mset_set A) = image_mset z (mset_set A)
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> image_mset y (mset_set A) = image_mset z (mset_set A)
[PROOF STEP]
assume "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> image_mset y (mset_set A) = image_mset z (mset_set A)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
obtain p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_permutation A B \<Longrightarrow> image_mset y (mset_set A) = image_mset z (mset_set A)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
[PROOF STEP]
show "image_mset f (mset_set A) = image_mset f' (mset_set A)"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. image_mset f (mset_set A) = image_mset f' (mset_set A)
[PROOF STEP]
using permutes_implies_image_mset_eq
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
\<lbrakk>?p permutes ?A; \<And>x. x \<in> ?A \<Longrightarrow> ?f x = ?f' (?p x)\<rbrakk> \<Longrightarrow> image_mset ?f' (mset_set ?A) = image_mset ?f (mset_set ?A)

goal (1 subgoal):
 1. image_mset f (mset_set A) = image_mset f' (mset_set A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
image_mset f (mset_set A) = image_mset f' (mset_set A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equiv_range_permutation:
  "equiv (A \<rightarrow>\<^sub>E B) (range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv (A \<rightarrow>\<^sub>E B) (range_permutation A B)
[PROOF STEP]
proof (rule equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. refl_on (A \<rightarrow>\<^sub>E B) (range_permutation A B)
 2. sym (range_permutation A B)
 3. trans (range_permutation A B)
[PROOF STEP]
show "refl_on (A \<rightarrow>\<^sub>E B) (range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on (A \<rightarrow>\<^sub>E B) (range_permutation A B)
[PROOF STEP]
proof (rule refl_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
 2. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> range_permutation A B
[PROOF STEP]
show "range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))} \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)

goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> range_permutation A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> range_permutation A B
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> range_permutation A B
[PROOF STEP]
assume "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> A \<rightarrow>\<^sub>E B \<Longrightarrow> (x, x) \<in> range_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "(f, f) \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. (f, f) \<in> range_permutation A B
[PROOF STEP]
using permutes_id
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
id permutes ?S

goal (1 subgoal):
 1. (f, f) \<in> range_permutation A B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
id permutes ?S

goal (1 subgoal):
 1. (f, f) \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(f, f) \<in> range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
refl_on (A \<rightarrow>\<^sub>E B) (range_permutation A B)

goal (2 subgoals):
 1. sym (range_permutation A B)
 2. trans (range_permutation A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sym (range_permutation A B)
 2. trans (range_permutation A B)
[PROOF STEP]
show "sym (range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (range_permutation A B)
[PROOF STEP]
proof (rule symI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
assume "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where "p permutes B" and "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B" "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
from \<open>p permutes B\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes B
[PROOF STEP]
have "inv p permutes B"
[PROOF STATE]
proof (prove)
using this:
p permutes B

goal (1 subgoal):
 1. inv p permutes B
[PROOF STEP]
by (simp add: permutes_inv)
[PROOF STATE]
proof (state)
this:
inv p permutes B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv p permutes B

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
from \<open>p permutes B\<close> \<open>\<forall>x\<in>A. f x = p (f' x)\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)
[PROOF STEP]
have "\<forall>x\<in>A. f' x = inv p (f x)"
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = inv p (f x)
[PROOF STEP]
by (simp add: permutes_inverses(2))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> range_permutation A B \<Longrightarrow> (b, a) \<in> range_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes B
\<forall>x\<in>A. f' x = inv p (f x)
[PROOF STEP]
show "(f', f) \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes B
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. (f', f) \<in> range_permutation A B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
inv p permutes B
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. (f', f) \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f', f) \<in> range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sym (range_permutation A B)

goal (1 subgoal):
 1. trans (range_permutation A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (range_permutation A B)
[PROOF STEP]
show "trans (range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (range_permutation A B)
[PROOF STEP]
proof (rule transI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
fix f f' f''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
assume "(f, f') \<in> range_permutation A B" "(f', f'') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B
(f', f'') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where "p permutes B" and "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
from \<open>(f', f'') \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
(f', f'') \<in> range_permutation A B
[PROOF STEP]
obtain p' where "p' permutes B" and "\<forall>x\<in>A. f' x = p' (f'' x)"
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' permutes B; \<forall>x\<in>A. f' x = p' (f'' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' permutes B; \<forall>x\<in>A. f' x = p' (f'' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' permutes B
\<forall>x\<in>A. f' x = p' (f'' x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
from \<open>(f', f'') \<in> range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f', f'') \<in> range_permutation A B
[PROOF STEP]
have "f'' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> range_permutation A B

goal (1 subgoal):
 1. f'' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. f'' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f'' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f'' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
from \<open>p permutes B\<close> \<open>p' permutes B\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes B
p' permutes B
[PROOF STEP]
have "(p \<circ> p') permutes B"
[PROOF STATE]
proof (prove)
using this:
p permutes B
p' permutes B

goal (1 subgoal):
 1. p \<circ> p' permutes B
[PROOF STEP]
by (simp add: permutes_compose)
[PROOF STATE]
proof (state)
this:
p \<circ> p' permutes B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<circ> p' permutes B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
have "\<forall>x\<in>A. f x = (p \<circ> p') (f'' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. f x = (p \<circ> p') (f'' x)
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p (f' x)\<close> \<open>\<forall>x\<in>A. f' x = p' (f'' x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p (f' x)
\<forall>x\<in>A. f' x = p' (f'' x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f x = (p \<circ> p') (f'' x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f x = (p \<circ> p') (f'' x)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> range_permutation A B; (y, z) \<in> range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> range_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p \<circ> p' permutes B
\<forall>x\<in>A. f x = (p \<circ> p') (f'' x)
[PROOF STEP]
show "(f, f'') \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p \<circ> p' permutes B
\<forall>x\<in>A. f x = (p \<circ> p') (f'' x)

goal (1 subgoal):
 1. (f, f'') \<in> range_permutation A B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p \<circ> p' permutes B
\<forall>x\<in>A. f x = (p \<circ> p') (f'' x)

goal (1 subgoal):
 1. (f, f'') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f, f'') \<in> range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trans (range_permutation A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_respects_range_permutation:
  "(\<lambda>f. inj_on f A) respects range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. inj_on f A) respects range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
assume "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where p: "p permutes B" "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
have inv_p: "\<forall>x\<in>A. f' x = inv p (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = inv p (f x)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = inv p (f x)
[PROOF STEP]
by (simp add: permutes_inverses(2))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
show "inj_on f A \<longleftrightarrow> inj_on f' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on f A \<Longrightarrow> inj_on f' A
 2. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
assume "inj_on f A"
[PROOF STATE]
proof (state)
this:
inj_on f A

goal (2 subgoals):
 1. inj_on f A \<Longrightarrow> inj_on f' A
 2. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
from this p
[PROOF STATE]
proof (chain)
picking this:
inj_on f A
p permutes B
\<forall>x\<in>A. f x = p (f' x)
[PROOF STEP]
show "inj_on f' A"
[PROOF STATE]
proof (prove)
using this:
inj_on f A
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. inj_on f' A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. f' x = f' y \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on f' A

goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
assume "inj_on f' A"
[PROOF STATE]
proof (state)
this:
inj_on f' A

goal (1 subgoal):
 1. inj_on f' A \<Longrightarrow> inj_on f A
[PROOF STEP]
from this inv_p
[PROOF STATE]
proof (chain)
picking this:
inj_on f' A
\<forall>x\<in>A. f' x = inv p (f x)
[PROOF STEP]
show "inj_on f A"
[PROOF STATE]
proof (prove)
using this:
inj_on f' A
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. inj_on f A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. f' x = f' y \<longrightarrow> x = y
\<forall>x\<in>A. f' x = inv p (f x)

goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on f A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on f A = inj_on f' A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surj_on_respects_range_permutation:
  "(\<lambda>f. f ` A = B) respects range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. f ` A = B) respects range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
assume a: "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B" "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where p: "p permutes B" "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
have 1: "f ` A = (\<lambda>x. p (f' x)) ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = (\<lambda>x. p (f' x)) ` A
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. f ` A = (\<lambda>x. p (f' x)) ` A
[PROOF STEP]
by (meson image_cong)
[PROOF STATE]
proof (state)
this:
f ` A = (\<lambda>x. p (f' x)) ` A

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
have 2: "inv p ` ((\<lambda>x. p (f' x)) ` A) = f' ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
[PROOF STEP]
by (simp add: image_image image_inv_f_f permutes_inj)
[PROOF STATE]
proof (state)
this:
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
show "(f ` A = B) = (f' ` A = B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` A = B \<Longrightarrow> f' ` A = B
 2. f' ` A = B \<Longrightarrow> f ` A = B
[PROOF STEP]
assume "f ` A = B"
[PROOF STATE]
proof (state)
this:
f ` A = B

goal (2 subgoals):
 1. f ` A = B \<Longrightarrow> f' ` A = B
 2. f' ` A = B \<Longrightarrow> f ` A = B
[PROOF STEP]
from this 1 2
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
[PROOF STEP]
show "f' ` A = B"
[PROOF STATE]
proof (prove)
using this:
f ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A

goal (1 subgoal):
 1. f' ` A = B
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
f ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. f' ` A = B
[PROOF STEP]
by (simp add: permutes_image permutes_inv)
[PROOF STATE]
proof (state)
this:
f' ` A = B

goal (1 subgoal):
 1. f' ` A = B \<Longrightarrow> f ` A = B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f' ` A = B \<Longrightarrow> f ` A = B
[PROOF STEP]
assume "f' ` A = B"
[PROOF STATE]
proof (state)
this:
f' ` A = B

goal (1 subgoal):
 1. f' ` A = B \<Longrightarrow> f ` A = B
[PROOF STEP]
from this 1 2
[PROOF STATE]
proof (chain)
picking this:
f' ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
[PROOF STEP]
show "f ` A = B"
[PROOF STATE]
proof (prove)
using this:
f' ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
f' ` A = B
f ` A = (\<lambda>x. p (f' x)) ` A
inv p ` (\<lambda>x. p (f' x)) ` A = f' ` A
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by (metis image_image permutes_image)
[PROOF STATE]
proof (state)
this:
f ` A = B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f ` A = B) = (f' ` A = B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_respects_range_permutation:
  "(\<lambda>f. bij_betw f A B) respects range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. bij_betw f A B) respects range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
assume "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where "p permutes B" and "\<forall>x\<in>A. f x = p (f' x)"
    and "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x); f' \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x); f' \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
have "bij_betw f A B \<longleftrightarrow> bij_betw (p o f') A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B = bij_betw (p \<circ> f') A B
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p (f' x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. bij_betw f A B = bij_betw (p \<circ> f') A B
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) bij_betw_cong comp_apply)
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw (p \<circ> f') A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw (p \<circ> f') A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
have "... \<longleftrightarrow> bij_betw f' A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (p \<circ> f') A B = bij_betw f' A B
[PROOF STEP]
using \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close> \<open>p permutes B\<close>
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
p permutes B

goal (1 subgoal):
 1. bij_betw (p \<circ> f') A B = bij_betw f' A B
[PROOF STEP]
by (auto intro!: bij_betw_comp_iff2[symmetric] permutes_imp_bij)
[PROOF STATE]
proof (state)
this:
bij_betw (p \<circ> f') A B = bij_betw f' A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bij_betw f A B = bij_betw f' A B
[PROOF STEP]
show "bij_betw f A B \<longleftrightarrow> bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw f A B = bij_betw f' A B

goal (1 subgoal):
 1. bij_betw f A B = bij_betw f' A B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw f' A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma domain_partitions_respects_range_permutation:
  "(\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) respects range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) respects range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
assume "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
obtain p where p: "p permutes B" "\<forall>x \<in> A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes B; \<forall>x\<in>A. f x = p (f' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
have "{} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B \<longleftrightarrow> \<not> (\<forall>b \<in> B. \<exists>x \<in> A. f' x = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = (\<not> (\<forall>b\<in>B. \<exists>x\<in>A. f' x = b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = (\<not> (\<forall>b\<in>B. \<exists>x\<in>A. f' x = b))

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = (\<not> (\<forall>b\<in>B. \<exists>x\<in>A. f' x = b))

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
have "(\<forall>b \<in> B. \<exists>x \<in> A. f' x = b) \<longleftrightarrow> (\<forall>b \<in> B. \<exists>x \<in> A. p (f' x) = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>b\<in>B. \<exists>x\<in>A. f' x = b) = (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>b\<in>B. \<exists>x\<in>A. f' x = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
 2. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
assume "\<forall>b\<in>B. \<exists>x\<in>A. f' x = b"
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b

goal (2 subgoals):
 1. \<forall>b\<in>B. \<exists>x\<in>A. f' x = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
 2. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
show "\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b"
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
[PROOF STEP]
using \<open>p permutes B\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b
p permutes B

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
[PROOF STEP]
unfolding permutes_def
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b
(\<forall>x. x \<notin> B \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
assume "\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b"
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b \<Longrightarrow> \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
[PROOF STEP]
show "\<forall>b\<in>B. \<exists>x\<in>A. f' x = b"
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
using \<open>p permutes B\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b
p permutes B

goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>x\<in>A. f' x = b
[PROOF STEP]
by (metis bij_betwE permutes_imp_bij permutes_inverses(2))
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>B. \<exists>x\<in>A. f' x = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>b\<in>B. \<exists>x\<in>A. f' x = b) = (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>b\<in>B. \<exists>x\<in>A. f' x = b) = (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
have "\<not> (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b) \<longleftrightarrow> {} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b)) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> (\<forall>b\<in>B. \<exists>x\<in>A. p (f' x) = b)) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)
[PROOF STEP]
have "{} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B \<longleftrightarrow> {} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B"
[PROOF STATE]
proof (prove)
using this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)

goal (1 subgoal):
 1. ({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
have "(\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B
[PROOF STEP]
using \<open>p permutes B\<close> permutes_implies_inv_image_on_eq
[PROOF STATE]
proof (prove)
using this:
p permutes B
?p permutes ?B \<Longrightarrow> (\<lambda>b. {x \<in> ?A. ?p (?f x) = b}) ` ?B = (\<lambda>b. {x \<in> ?A. ?f x = b}) ` ?B

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)
(\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B
[PROOF STEP]
have "(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
using this:
({} \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B) = ({} \<in> (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B)
(\<lambda>b. {x \<in> A. f' x = b}) ` B = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
have "\<dots> = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
using \<open>\<forall>x \<in> A. f x = p (f' x)\<close> Collect_cong image_cong
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p (f' x)
(\<And>x. ?P x = ?Q x) \<Longrightarrow> {x. ?P x} = {x. ?Q x}
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> range_permutation A B \<Longrightarrow> (\<lambda>b. {x \<in> A. y x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
show "(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}

goal:
No subgoals!
[PROOF STEP]
qed