[STATEMENT]
lemma equiv_domain_and_range_permutation:
  "equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
[PROOF STEP]
proof (rule equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. refl_on (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
 2. sym (domain_and_range_permutation A B)
 3. trans (domain_and_range_permutation A B)
[PROOF STEP]
show "refl_on (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
[PROOF STEP]
proof (rule refl_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. domain_and_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> domain_and_range_permutation A B
[PROOF STEP]
show "domain_and_range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_and_range_permutation A B \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))} \<subseteq> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain_and_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> domain_and_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> domain_and_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> domain_and_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> domain_and_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> domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B

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

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

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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(f, f) \<in> domain_and_range_permutation A B

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

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

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

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_and_range_permutation A B \<Longrightarrow> (b, a) \<in> domain_and_range_permutation A B
[PROOF STEP]
from \<open>(f, f') \<in> domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_and_range_permutation A B
[PROOF STEP]
have f: "f \<in> A \<rightarrow>\<^sub>E B" "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_and_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 domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A 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_and_range_permutation A B \<Longrightarrow> (b, a) \<in> domain_and_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> domain_and_range_permutation A B \<Longrightarrow> (b, a) \<in> domain_and_range_permutation A B
[PROOF STEP]
from \<open>p\<^sub>A permutes A\<close> \<open>p\<^sub>B permutes B\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>A permutes A
p\<^sub>B permutes B
[PROOF STEP]
have "inv p\<^sub>A permutes A" "inv p\<^sub>B permutes B"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A
p\<^sub>B permutes B

goal (1 subgoal):
 1. inv p\<^sub>A permutes A &&& inv p\<^sub>B permutes B
[PROOF STEP]
by (auto simp add: permutes_inv)
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A permutes A
inv p\<^sub>B permutes B

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

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

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

goal (1 subgoal):
 1. \<forall>x\<in>A. f' x = inv p\<^sub>B (f (inv p\<^sub>A x))
[PROOF STEP]
by (metis (no_types, lifting) bij_betwE bij_inv_eq_iff permutes_bij permutes_imp_bij)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f' x = inv p\<^sub>B (f (inv p\<^sub>A x))

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> domain_and_range_permutation A B \<Longrightarrow> (b, a) \<in> domain_and_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\<^sub>A permutes A
inv p\<^sub>B permutes B
\<forall>x\<in>A. f' x = inv p\<^sub>B (f (inv p\<^sub>A x))
[PROOF STEP]
show "(f', f) \<in> domain_and_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\<^sub>A permutes A
inv p\<^sub>B permutes B
\<forall>x\<in>A. f' x = inv p\<^sub>B (f (inv p\<^sub>A x))

goal (1 subgoal):
 1. (f', f) \<in> domain_and_range_permutation A B
[PROOF STEP]
unfolding domain_and_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\<^sub>A permutes A
inv p\<^sub>B permutes B
\<forall>x\<in>A. f' x = inv p\<^sub>B (f (inv p\<^sub>A 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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f', f) \<in> domain_and_range_permutation A B

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

goal (1 subgoal):
 1. trans (domain_and_range_permutation A B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (domain_and_range_permutation A B)
[PROOF STEP]
show "trans (domain_and_range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (domain_and_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> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_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> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_range_permutation A B
[PROOF STEP]
assume "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_range_permutation A B
[PROOF STEP]
assume "(f', f'') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f', f'') \<in> domain_and_range_permutation A B

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

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

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

goal (1 subgoal):
 1. (\<And>p'\<^sub>A p'\<^sub>B. \<lbrakk>p'\<^sub>A permutes A; p'\<^sub>B permutes B; \<forall>x\<in>A. f' x = p'\<^sub>B (f'' (p'\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

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

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A 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_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_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> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_range_permutation A B
[PROOF STEP]
from \<open>(f', f'') \<in> domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f', f'') \<in> domain_and_range_permutation A B
[PROOF STEP]
have "f'' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f', f'') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. f'' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A 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_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_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> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_range_permutation A B
[PROOF STEP]
from \<open>p\<^sub>A permutes A\<close> \<open>p'\<^sub>A permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>A permutes A
p'\<^sub>A permutes A
[PROOF STEP]
have "(p'\<^sub>A \<circ> p\<^sub>A) permutes A"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A
p'\<^sub>A permutes A

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> domain_and_range_permutation A B; (y, z) \<in> domain_and_range_permutation A B\<rbrakk> \<Longrightarrow> (x, z) \<in> domain_and_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'\<^sub>A \<circ> p\<^sub>A permutes A
p\<^sub>B \<circ> p'\<^sub>B permutes B
\<forall>x\<in>A. f x = (p\<^sub>B \<circ> p'\<^sub>B) (f'' ((p'\<^sub>A \<circ> p\<^sub>A) x))
[PROOF STEP]
show "(f, f'') \<in> domain_and_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'\<^sub>A \<circ> p\<^sub>A permutes A
p\<^sub>B \<circ> p'\<^sub>B permutes B
\<forall>x\<in>A. f x = (p\<^sub>B \<circ> p'\<^sub>B) (f'' ((p'\<^sub>A \<circ> p\<^sub>A) x))

goal (1 subgoal):
 1. (f, f'') \<in> domain_and_range_permutation A B
[PROOF STEP]
unfolding domain_and_range_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
f'' \<in> A \<rightarrow>\<^sub>E B
p'\<^sub>A \<circ> p\<^sub>A permutes A
p\<^sub>B \<circ> p'\<^sub>B permutes B
\<forall>x\<in>A. f x = (p\<^sub>B \<circ> p'\<^sub>B) (f'' ((p'\<^sub>A \<circ> p\<^sub>A) 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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(f, f'') \<in> domain_and_range_permutation A B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_respects_domain_and_range_permutation:
  "(\<lambda>f. inj_on f A) respects domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. inj_on f A) respects domain_and_range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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> domain_and_range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
assume "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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> domain_and_range_permutation A B
[PROOF STEP]
obtain p\<^sub>A p\<^sub>B where "p\<^sub>A permutes A" "p\<^sub>B permutes B" and "\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from \<open>(f, f') \<in> domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_and_range_permutation A B
[PROOF STEP]
have "f' ` A \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. f' ` A \<subseteq> B
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from \<open>p\<^sub>A permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>A permutes A
[PROOF STEP]
have "p\<^sub>A ` A = A"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A

goal (1 subgoal):
 1. p\<^sub>A ` A = A
[PROOF STEP]
by (auto simp add: permutes_image)
[PROOF STATE]
proof (state)
this:
p\<^sub>A ` A = A

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from \<open>p\<^sub>A permutes A\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>A permutes A
[PROOF STEP]
have "inj_on p\<^sub>A A"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A

goal (1 subgoal):
 1. inj_on p\<^sub>A A
[PROOF STEP]
using bij_betw_imp_inj_on permutes_imp_bij
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A
bij_betw ?f ?A ?B \<Longrightarrow> inj_on ?f ?A
?p permutes ?S \<Longrightarrow> bij_betw ?p ?S ?S

goal (1 subgoal):
 1. inj_on p\<^sub>A A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on p\<^sub>A A

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> inj_on y A = inj_on z A
[PROOF STEP]
from \<open>p\<^sub>B permutes B\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>B permutes B
[PROOF STEP]
have "inj_on p\<^sub>B B"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>B permutes B

goal (1 subgoal):
 1. inj_on p\<^sub>B B
[PROOF STEP]
using bij_betw_imp_inj_on permutes_imp_bij
[PROOF STATE]
proof (prove)
using this:
p\<^sub>B permutes B
bij_betw ?f ?A ?B \<Longrightarrow> inj_on ?f ?A
?p permutes ?S \<Longrightarrow> bij_betw ?p ?S ?S

goal (1 subgoal):
 1. inj_on p\<^sub>B B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on p\<^sub>B B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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 (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
have "inj_on f A \<longleftrightarrow> inj_on (\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A = inj_on (\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) A
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close> inj_on_cong comp_apply
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))
(\<And>a. a \<in> ?A \<Longrightarrow> ?f a = ?g a) \<Longrightarrow> inj_on ?f ?A = inj_on ?g ?A
(?f \<circ> ?g) ?x = ?f (?g ?x)

goal (1 subgoal):
 1. inj_on f A = inj_on (\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inj_on f A = inj_on (\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
have "inj_on f A \<longleftrightarrow> inj_on (p\<^sub>B o f' o p\<^sub>A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A = inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A
[PROOF STEP]
by (simp add: \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close> inj_on_def)
[PROOF STATE]
proof (state)
this:
inj_on f A = inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inj_on f A = inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
have "inj_on (p\<^sub>B o f' o p\<^sub>A) A \<longleftrightarrow> inj_on (p\<^sub>B o f') A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A = inj_on (p\<^sub>B \<circ> f') A
[PROOF STEP]
using \<open>inj_on p\<^sub>A A\<close> \<open>p\<^sub>A ` A = A\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on p\<^sub>A A
p\<^sub>A ` A = A

goal (1 subgoal):
 1. inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A = inj_on (p\<^sub>B \<circ> f') A
[PROOF STEP]
by (auto dest: inj_on_imageI intro: comp_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A = inj_on (p\<^sub>B \<circ> f') A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inj_on (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A = inj_on (p\<^sub>B \<circ> f') A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
have "inj_on (p\<^sub>B o f') A \<longleftrightarrow> inj_on f' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (p\<^sub>B \<circ> f') A = inj_on f' A
[PROOF STEP]
using \<open>inj_on p\<^sub>B B\<close> \<open>f' ` A \<subseteq> B\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on p\<^sub>B B
f' ` A \<subseteq> B

goal (1 subgoal):
 1. inj_on (p\<^sub>B \<circ> f') A = inj_on f' A
[PROOF STEP]
by (auto dest: inj_on_imageI2 intro: comp_inj_on subset_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on (p\<^sub>B \<circ> f') A = inj_on f' A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inj_on f A = inj_on f' A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on f A = inj_on f' A

goal (1 subgoal):
 1. inj_on f A = inj_on f' A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
inj_on f A = 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 surjective_respects_domain_and_range_permutation:
  "(\<lambda>f. f ` A = B) respects domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. f ` A = B) respects domain_and_range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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> domain_and_range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
assume "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_and_range_permutation A B

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

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

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

goal (1 subgoal):
 1. p\<^sub>A ` A = A &&& p\<^sub>B ` B = B
[PROOF STEP]
by (auto simp add: permutes_image)
[PROOF STATE]
proof (state)
this:
p\<^sub>A ` A = A
p\<^sub>B ` B = B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
from \<open>p\<^sub>B permutes B\<close>
[PROOF STATE]
proof (chain)
picking this:
p\<^sub>B permutes B
[PROOF STEP]
have "inj p\<^sub>B"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>B permutes B

goal (1 subgoal):
 1. inj p\<^sub>B
[PROOF STEP]
by (simp add: permutes_inj)
[PROOF STATE]
proof (state)
this:
inj p\<^sub>B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> (y ` A = B) = (z ` A = B)
[PROOF STEP]
show "(f ` A = B) \<longleftrightarrow> (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 (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
have "f ` A = B \<longleftrightarrow> (\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ` A = B) = ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B)
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))

goal (1 subgoal):
 1. (f ` A = B) = ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B)
[PROOF STEP]
by (metis (mono_tags, lifting) image_cong)
[PROOF STATE]
proof (state)
this:
(f ` A = B) = ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f ` A = B) = ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
have "(\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B \<longleftrightarrow> (\<lambda>x. p\<^sub>B (f' x)) ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B) = ((\<lambda>x. p\<^sub>B (f' x)) ` A = B)
[PROOF STEP]
using \<open>p\<^sub>A ` A = A\<close>
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A ` A = A

goal (1 subgoal):
 1. ((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B) = ((\<lambda>x. p\<^sub>B (f' x)) ` A = B)
[PROOF STEP]
by (metis image_image)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B) = ((\<lambda>x. p\<^sub>B (f' x)) ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. p\<^sub>B (f' (p\<^sub>A x))) ` A = B) = ((\<lambda>x. p\<^sub>B (f' x)) ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
have "(\<lambda>x. p\<^sub>B (f' x)) ` A = B \<longleftrightarrow> (f' ` A = B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. p\<^sub>B (f' x)) ` A = B) = (f' ` A = B)
[PROOF STEP]
using \<open>p\<^sub>B ` B = B\<close> \<open>inj p\<^sub>B\<close>
[PROOF STATE]
proof (prove)
using this:
p\<^sub>B ` B = B
inj p\<^sub>B

goal (1 subgoal):
 1. ((\<lambda>x. p\<^sub>B (f' x)) ` A = B) = (f' ` A = B)
[PROOF STEP]
by (metis image_image image_inv_f_f)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. p\<^sub>B (f' x)) ` A = B) = (f' ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f ` A = B) = (f' ` A = B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f ` A = B) = (f' ` A = B)

goal (1 subgoal):
 1. (f ` A = B) = (f' ` A = B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f ` A = B) = (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_domain_and_range_permutation:
  "(\<lambda>f. bij_betw f A B) respects domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. bij_betw f A B) respects domain_and_range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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> domain_and_range_permutation A B \<Longrightarrow> bij_betw y A B = bij_betw z A B
[PROOF STEP]
assume "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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> domain_and_range_permutation A B
[PROOF STEP]
obtain p\<^sub>A p\<^sub>B where "p\<^sub>A permutes A" "p\<^sub>B permutes B"
    and "\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))" and "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x)); f' \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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\<^sub>B o f' o p\<^sub>A) A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B = bij_betw (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A B
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close> bij_betw_congI
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))
\<lbrakk>bij_betw ?f ?A ?A'; \<forall>a\<in>?A. ?f a = ?g a\<rbrakk> \<Longrightarrow> bij_betw ?g ?A ?A'

goal (1 subgoal):
 1. bij_betw f A B = bij_betw (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bij_betw f A B = bij_betw (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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\<^sub>B \<circ> f' \<circ> p\<^sub>A) A B

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

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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 (p\<^sub>B \<circ> f' \<circ> p\<^sub>A) A B = bij_betw (p\<^sub>B \<circ> f') A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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\<^sub>B \<circ> f') A B = bij_betw f' A B
[PROOF STEP]
using \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close> \<open>p\<^sub>B permutes B\<close>
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
p\<^sub>B permutes B

goal (1 subgoal):
 1. bij_betw (p\<^sub>B \<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\<^sub>B \<circ> f') A B = bij_betw f' A B

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_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 count_image_mset':
  "count (image_mset f A) x = sum (count A) {x' \<in> set_mset A. f x' = x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
have "count (image_mset f A) x = sum (count A) (f -` {x} \<inter> set_mset A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) (f -` {x} \<inter> set_mset A)
[PROOF STEP]
unfolding count_image_mset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) (f -` {x} \<inter> set_mset A)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
count (image_mset f A) x = sum (count A) (f -` {x} \<inter> set_mset A)

goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count (image_mset f A) x = sum (count A) (f -` {x} \<inter> set_mset A)

goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
have "\<dots> = sum (count A) {x' \<in> set_mset A. f x' = x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
have "(f -` {x} \<inter> set_mset A) = {x' \<in> set_mset A. f x' = x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` {x} \<inter> set_mset A = {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f -` {x} \<inter> set_mset A = {x'. x' \<in># A \<and> f x' = x}

goal (1 subgoal):
 1. sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f -` {x} \<inter> set_mset A = {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f -` {x} \<inter> set_mset A = {x'. x' \<in># A \<and> f x' = x}

goal (1 subgoal):
 1. sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (count A) (f -` {x} \<inter> set_mset A) = sum (count A) {x'. x' \<in># A \<and> f x' = x}

goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}

goal (1 subgoal):
 1. count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
count (image_mset f A) x = sum (count A) {x'. x' \<in># A \<and> f x' = x}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiset_of_partition_cards_respects_domain_and_range_permutation:
  assumes "finite B"
  shows "(\<lambda>f. image_mset (\<lambda>X. card X) (mset_set (((\<lambda>b. {x \<in> A. f x = b})) ` B - {{}}))) respects domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) respects domain_and_range_permutation A B
[PROOF STEP]
proof (rule congruentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> image_mset card (mset_set ((\<lambda>b. {x \<in> A. y x = b}) ` B - {{}})) = image_mset card (mset_set ((\<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> domain_and_range_permutation A B \<Longrightarrow> image_mset card (mset_set ((\<lambda>b. {x \<in> A. y x = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}))
[PROOF STEP]
assume "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
(f, f') \<in> domain_and_range_permutation A B

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

goal (1 subgoal):
 1. (\<And>p\<^sub>A p\<^sub>B. \<lbrakk>p\<^sub>A permutes A; p\<^sub>B permutes B; \<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_and_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\<^sub>A p\<^sub>B. p\<^sub>A permutes A \<and> p\<^sub>B permutes B \<and> (\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))))}

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> image_mset card (mset_set ((\<lambda>b. {x \<in> A. y x = b}) ` B - {{}})) = image_mset card (mset_set ((\<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\<^sub>B (f' (p\<^sub>A 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\<^sub>B (f' (p\<^sub>A x)) = b}) ` B
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p\<^sub>B (f' (p\<^sub>A x))

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B = (\<lambda>b. {x \<in> A. p\<^sub>B (f' (p\<^sub>A 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\<^sub>B (f' (p\<^sub>A x)) = b}) ` B

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>y z. (y, z) \<in> domain_and_range_permutation A B \<Longrightarrow> image_mset card (mset_set ((\<lambda>b. {x \<in> A. y x = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. z x = b}) ` B - {{}}))
[PROOF STEP]
have "image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}})) =
    image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))
[PROOF STEP]
proof (rule multiset_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) x = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) x
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) x = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) x
[PROOF STEP]
have "bij_betw (\<lambda>X. p\<^sub>A ` X) {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ((`) p\<^sub>A) {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
proof (rule bij_betw_byWitness)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}. ?f' (p\<^sub>A ` a) = a
 2. \<forall>a'\<in>{X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}. p\<^sub>A ` ?f' a' = a'
 3. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
 4. ?f' ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
show "\<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}. inv p\<^sub>A ` p\<^sub>A ` X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}. inv p\<^sub>A ` p\<^sub>A ` X = X
[PROOF STEP]
by (meson \<open>p\<^sub>A permutes A\<close> image_inv_f_f permutes_inj)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}. inv p\<^sub>A ` p\<^sub>A ` X = X

goal (3 subgoals):
 1. \<forall>a'\<in>{X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}. p\<^sub>A ` inv p\<^sub>A ` a' = a'
 2. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
 3. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
show "\<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}. p\<^sub>A ` inv p\<^sub>A ` X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}. p\<^sub>A ` inv p\<^sub>A ` X = X
[PROOF STEP]
by (meson \<open>p\<^sub>A permutes A\<close> image_f_inv_f permutes_surj)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}. p\<^sub>A ` inv p\<^sub>A ` X = X

goal (2 subgoals):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
 2. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
show "(\<lambda>X. p\<^sub>A ` X) ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
have "card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
have "inj_on p\<^sub>A {x \<in> A. f' (p\<^sub>A x) = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on p\<^sub>A {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
by (metis (no_types, lifting) \<open>p\<^sub>A permutes A\<close> injD inj_onI permutes_inj)
[PROOF STATE]
proof (state)
this:
inj_on p\<^sub>A {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
inj_on p\<^sub>A {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on p\<^sub>A {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
by (simp add: card_image)
[PROOF STATE]
proof (state)
this:
card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}) = card {x \<in> A. f' (p\<^sub>A x) = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b}) = card {x \<in> A. f' (p\<^sub>A x) = ?b}

goal (1 subgoal):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b}) = card {x \<in> A. f' (p\<^sub>A x) = ?b}

goal (1 subgoal):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
have "p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} = {x \<in> A. f' x = b}" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} = {x \<in> A. f' x = b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> {x \<in> A. f' x = b}
 2. {x \<in> A. f' x = b} \<subseteq> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
show "p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> {x \<in> A. f' x = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> {x \<in> A. f' x = b}
[PROOF STEP]
by (auto simp add: \<open>p\<^sub>A permutes A\<close> permutes_in_image)
[PROOF STATE]
proof (state)
this:
p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> {x \<in> A. f' x = b}

goal (1 subgoal):
 1. {x \<in> A. f' x = b} \<subseteq> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
show "{x \<in> A. f' x = b} \<subseteq> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. f' x = b} \<subseteq> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
assume "x \<in> {x \<in> A. f' x = b}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> A. f' x = b}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
have "p\<^sub>A (inv p\<^sub>A x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>A (inv p\<^sub>A x) = x
[PROOF STEP]
using \<open>p\<^sub>A permutes A\<close> permutes_inverses(1)
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A
?p permutes ?S \<Longrightarrow> ?p (inv ?p ?x) = ?x

goal (1 subgoal):
 1. p\<^sub>A (inv p\<^sub>A x) = x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p\<^sub>A (inv p\<^sub>A x) = x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p\<^sub>A (inv p\<^sub>A x) = x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
from \<open>x \<in> {x \<in> A. f' x = b}\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x \<in> A. f' x = b}
[PROOF STEP]
have "inv p\<^sub>A x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> A. f' x = b}

goal (1 subgoal):
 1. inv p\<^sub>A x \<in> A
[PROOF STEP]
by (simp add: \<open>p\<^sub>A permutes A\<close> permutes_in_image permutes_inv)
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' x = b} \<Longrightarrow> x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x \<in> A. f' x = b}
p\<^sub>A (inv p\<^sub>A x) = x
inv p\<^sub>A x \<in> A
[PROOF STEP]
show "x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> A. f' x = b}
p\<^sub>A (inv p\<^sub>A x) = x
inv p\<^sub>A x \<in> A

goal (1 subgoal):
 1. x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
by (auto intro: image_eqI[where x="inv p\<^sub>A x"])
[PROOF STATE]
proof (state)
this:
x \<in> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x \<in> A. f' x = b} \<subseteq> p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b} = {x \<in> A. f' x = ?b}

goal (1 subgoal):
 1. (`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b}) = card {x \<in> A. f' (p\<^sub>A x) = ?b}
p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b} = {x \<in> A. f' x = ?b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b}) = card {x \<in> A. f' (p\<^sub>A x) = ?b}
p\<^sub>A ` {x \<in> A. f' (p\<^sub>A x) = ?b} = {x \<in> A. f' x = ?b}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(`) p\<^sub>A ` {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}

goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
show "(\<lambda>X. inv p\<^sub>A ` X) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
have "card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}
[PROOF STEP]
have "inj_on (inv p\<^sub>A) {x \<in> A. f' x = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (inv p\<^sub>A) {x \<in> A. f' x = b}
[PROOF STEP]
by (metis (no_types, lifting) \<open>p\<^sub>A permutes A\<close> injD inj_onI permutes_surj surj_imp_inj_inv)
[PROOF STATE]
proof (state)
this:
inj_on (inv p\<^sub>A) {x \<in> A. f' x = b}

goal (1 subgoal):
 1. card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
inj_on (inv p\<^sub>A) {x \<in> A. f' x = b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (inv p\<^sub>A) {x \<in> A. f' x = b}

goal (1 subgoal):
 1. card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}
[PROOF STEP]
by (simp add: card_image)
[PROOF STATE]
proof (state)
this:
card (inv p\<^sub>A ` {x \<in> A. f' x = b}) = card {x \<in> A. f' x = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (inv p\<^sub>A ` {x \<in> A. f' x = ?b}) = card {x \<in> A. f' x = ?b}

goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (inv p\<^sub>A ` {x \<in> A. f' x = ?b}) = card {x \<in> A. f' x = ?b}

goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
have "inv p\<^sub>A ` {x \<in> A. f' x = b} = {x \<in> A. f' (p\<^sub>A x) = b}" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv p\<^sub>A ` {x \<in> A. f' x = b} = {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inv p\<^sub>A ` {x \<in> A. f' x = b} \<subseteq> {x \<in> A. f' (p\<^sub>A x) = b}
 2. {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
show "inv p\<^sub>A ` {x \<in> A. f' x = b} \<subseteq> {x \<in> A. f' (p\<^sub>A x) = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv p\<^sub>A ` {x \<in> A. f' x = b} \<subseteq> {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
using \<open>p\<^sub>A permutes A\<close>
[PROOF STATE]
proof (prove)
using this:
p\<^sub>A permutes A

goal (1 subgoal):
 1. inv p\<^sub>A ` {x \<in> A. f' x = b} \<subseteq> {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
by (auto simp add: permutes_in_image permutes_inv permutes_inverses(1))
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A ` {x \<in> A. f' x = b} \<subseteq> {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
show "{x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> inv p\<^sub>A ` {x \<in> A. f' x = b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
assume "x \<in> {x \<in> A. f' (p\<^sub>A x) = b}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
have "inv p\<^sub>A (p\<^sub>A x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv p\<^sub>A (p\<^sub>A x) = x
[PROOF STEP]
by (meson \<open>p\<^sub>A permutes A\<close> permutes_inverses(2))
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A (p\<^sub>A x) = x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A (p\<^sub>A x) = x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
from \<open>x \<in> {x \<in> A. f' (p\<^sub>A x) = b}\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}
[PROOF STEP]
have "p\<^sub>A x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}

goal (1 subgoal):
 1. p\<^sub>A x \<in> A
[PROOF STEP]
by (simp add: \<open>p\<^sub>A permutes A\<close> permutes_in_image)
[PROOF STATE]
proof (state)
this:
p\<^sub>A x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> A. f' (p\<^sub>A x) = b} \<Longrightarrow> x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}
inv p\<^sub>A (p\<^sub>A x) = x
p\<^sub>A x \<in> A
[PROOF STEP]
show "x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> A. f' (p\<^sub>A x) = b}
inv p\<^sub>A (p\<^sub>A x) = x
p\<^sub>A x \<in> A

goal (1 subgoal):
 1. x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}
[PROOF STEP]
by (auto intro: image_eqI[where x="p\<^sub>A x"])
[PROOF STATE]
proof (state)
this:
x \<in> inv p\<^sub>A ` {x \<in> A. f' x = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x \<in> A. f' (p\<^sub>A x) = b} \<subseteq> inv p\<^sub>A ` {x \<in> A. f' x = b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv p\<^sub>A ` {x \<in> A. f' x = ?b} = {x \<in> A. f' (p\<^sub>A x) = ?b}

goal (1 subgoal):
 1. (`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (inv p\<^sub>A ` {x \<in> A. f' x = ?b}) = card {x \<in> A. f' x = ?b}
inv p\<^sub>A ` {x \<in> A. f' x = ?b} = {x \<in> A. f' (p\<^sub>A x) = ?b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (inv p\<^sub>A ` {x \<in> A. f' x = ?b}) = card {x \<in> A. f' x = ?b}
inv p\<^sub>A ` {x \<in> A. f' x = ?b} = {x \<in> A. f' (p\<^sub>A x) = ?b}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(`) (inv p\<^sub>A) ` {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n} \<subseteq> {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bij_betw ((`) p\<^sub>A) {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}

goal (1 subgoal):
 1. \<And>x. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) x = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw ((`) p\<^sub>A) {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}
[PROOF STEP]
have "card {x' \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card x' = n} = card {x' \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card x' = n}"
[PROOF STATE]
proof (prove)
using this:
bij_betw ((`) p\<^sub>A) {X \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card X = n} {X \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card X = n}

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

goal (1 subgoal):
 1. \<And>x. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) x = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
card {x' \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card x' = n} = card {x' \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card x' = n}
[PROOF STEP]
show "count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) n =
      count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) n"
[PROOF STATE]
proof (prove)
using this:
card {x' \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card x' = n} = card {x' \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card x' = n}

goal (1 subgoal):
 1. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) n = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) n
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
card {x' \<in> (\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}. card x' = n} = card {x' \<in> (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}. card x' = n}
finite B

goal (1 subgoal):
 1. count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) n = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) n
[PROOF STEP]
by (simp add: count_image_mset')
[PROOF STATE]
proof (state)
this:
count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}}))) n = count (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' (p\<^sub>A x) = b}) ` B - {{}})) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvtRelI:
  fixes Rel  :: "('a::pt_name \<times> 'a) set"
  and   P    :: 'a
  and   Q    :: 'a
  and   perm :: "name prm"

  assumes "eqvt Rel"
  and     "(P, Q) \<in> Rel"

  shows "(perm \<bullet> P, perm \<bullet> Q) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (perm \<bullet> P, perm \<bullet> Q) \<in> Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P, Q) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> P, perm \<bullet> Q) \<in> Rel
[PROOF STEP]
by(auto simp add: eqvt_def)


[STATEMENT]
lemma eqvtRelE:
  fixes Rel  :: "('a::pt_name \<times> 'a) set"
  and   P    :: 'a
  and   Q    :: 'a
  and   perm :: "name prm"

  assumes "eqvt Rel"
  and     "(perm \<bullet> P, perm \<bullet> Q) \<in> Rel"

  shows "(P, Q) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
have "rev perm \<bullet> (perm \<bullet> P) = P" and "rev perm \<bullet> (perm \<bullet> Q) = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev perm \<bullet> perm \<bullet> P = P &&& rev perm \<bullet> perm \<bullet> Q = Q
[PROOF STEP]
by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])+
[PROOF STATE]
proof (state)
this:
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> Q = Q

goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(perm \<bullet> P, perm \<bullet> Q) \<in> Rel
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> Q = Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(perm \<bullet> P, perm \<bullet> Q) \<in> Rel
rev perm \<bullet> perm \<bullet> P = P
rev perm \<bullet> perm \<bullet> Q = Q

goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
by(force dest: eqvtRelI[of _ _ _ "rev perm"])
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvtTrans[intro]:
  fixes Rel  :: "('a::pt_name \<times> 'a) set"
  and   Rel' :: "('a \<times> 'a) set"

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

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

goal (1 subgoal):
 1. eqvt (Rel O Rel')
[PROOF STEP]
by(force simp add: eqvt_def)


[STATEMENT]
lemma eqvtUnion[intro]:
  fixes Rel  :: "('a::pt_name \<times> 'a) set"
  and   Rel' :: "('a \<times> 'a) 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 eqvtSubstClosed:
  fixes Rel :: "(pi \<times> pi) set"

  assumes eqvtRel: "eqvt Rel"

  shows "eqvt (substClosed Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (substClosed Rel)
[PROOF STEP]
proof(simp add: eqvt_def substClosed_def, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b perma \<sigma>. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> ((perma \<bullet> a)[<\<sigma>>], (perma \<bullet> b)[<\<sigma>>]) \<in> Rel
[PROOF STEP]
fix P Q perm s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b perma \<sigma>. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> ((perma \<bullet> a)[<\<sigma>>], (perma \<bullet> b)[<\<sigma>>]) \<in> Rel
[PROOF STEP]
assume "\<forall>s. (P[<s>], Q[<s>]) \<in> Rel"
[PROOF STATE]
proof (state)
this:
\<forall>s. (P[<s>], Q[<s>]) \<in> Rel

goal (1 subgoal):
 1. \<And>a b perma \<sigma>. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> ((perma \<bullet> a)[<\<sigma>>], (perma \<bullet> b)[<\<sigma>>]) \<in> Rel
[PROOF STEP]
hence "(P[<(rev (perm::name prm) \<bullet> s)>], Q[<(rev perm \<bullet> s)>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. (P[<s>], Q[<s>]) \<in> Rel

goal (1 subgoal):
 1. (P[<(rev perm \<bullet> s)>], Q[<(rev perm \<bullet> s)>]) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P[<(rev perm \<bullet> s)>], Q[<(rev perm \<bullet> s)>]) \<in> Rel

goal (1 subgoal):
 1. \<And>a b perma \<sigma>. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> ((perma \<bullet> a)[<\<sigma>>], (perma \<bullet> b)[<\<sigma>>]) \<in> Rel
[PROOF STEP]
with eqvtRel
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P[<(rev perm \<bullet> s)>], Q[<(rev perm \<bullet> s)>]) \<in> Rel
[PROOF STEP]
have "(perm \<bullet> (P[<(rev perm \<bullet> s)>]), perm \<bullet> (Q[<(rev perm \<bullet> s)>])) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P[<(rev perm \<bullet> s)>], Q[<(rev perm \<bullet> s)>]) \<in> Rel

goal (1 subgoal):
 1. (perm \<bullet> P[<(rev perm \<bullet> s)>], perm \<bullet> Q[<(rev perm \<bullet> s)>]) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
(perm \<bullet> P[<(rev perm \<bullet> s)>], perm \<bullet> Q[<(rev perm \<bullet> s)>]) \<in> Rel

goal (1 subgoal):
 1. \<And>a b perma \<sigma>. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> ((perma \<bullet> a)[<\<sigma>>], (perma \<bullet> b)[<\<sigma>>]) \<in> Rel
[PROOF STEP]
thus "((perm \<bullet> P)[<s>], (perm \<bullet> Q)[<s>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(perm \<bullet> P[<(rev perm \<bullet> s)>], perm \<bullet> Q[<(rev perm \<bullet> s)>]) \<in> Rel

goal (1 subgoal):
 1. ((perm \<bullet> P)[<s>], (perm \<bullet> Q)[<s>]) \<in> Rel
[PROOF STEP]
by(simp add: name_per_rev)
[PROOF STATE]
proof (state)
this:
((perm \<bullet> P)[<s>], (perm \<bullet> Q)[<s>]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma substClosedSubset:
  fixes Rel  :: "(pi \<times> pi) set"

  shows "substClosed Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. substClosed Rel \<subseteq> Rel
[PROOF STEP]
proof(auto simp add: substClosed_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> (a, b) \<in> Rel
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> (a, b) \<in> Rel
[PROOF STEP]
assume "\<forall>s. (P[<s>], Q[<s>]) \<in> Rel"
[PROOF STATE]
proof (state)
this:
\<forall>s. (P[<s>], Q[<s>]) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> (a, b) \<in> Rel
[PROOF STEP]
hence "(P[<[]>], Q[<[]>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. (P[<s>], Q[<s>]) \<in> Rel

goal (1 subgoal):
 1. (P[<[]>], Q[<[]>]) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[<[]>], Q[<[]>]) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. (a[<\<sigma>>], b[<\<sigma>>]) \<in> Rel \<Longrightarrow> (a, b) \<in> Rel
[PROOF STEP]
thus "(P, Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P[<[]>], Q[<[]>]) \<in> Rel

goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partUnfold:
  fixes P   :: pi
  and   Q   :: pi
  and   \<sigma>   :: "(name \<times> name) list"
  and   Rel :: "(pi \<times> pi) set"

  assumes "(P, Q) \<in> substClosed Rel"

  shows "(P[<\<sigma>>], Q[<\<sigma>>]) \<in> substClosed Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> substClosed Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> substClosed Rel

goal (1 subgoal):
 1. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> substClosed Rel
[PROOF STEP]
proof(auto simp add: substClosed_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel \<Longrightarrow> (P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
fix \<sigma>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel \<Longrightarrow> (P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
assume "\<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel"
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. \<And>\<sigma>'. \<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel \<Longrightarrow> (P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
hence "(P[<(\<sigma>@\<sigma>')>], Q[<(\<sigma>@\<sigma>')>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. (P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel

goal (1 subgoal):
 1. \<And>\<sigma>'. \<forall>\<sigma>. (P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel \<Longrightarrow> (P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
thus "((P[<\<sigma>>])[<\<sigma>'>], (Q[<\<sigma>>])[<\<sigma>'>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel

goal (1 subgoal):
 1. (P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed