[STATEMENT]
lemma bij_betw_quotient_domain_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
 2. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
show "{{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
by (simp add: bijections_in_domain_permutation[OF assms])
[PROOF STATE]
proof (state)
this:
{{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
assume F_in: "F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B"
[PROOF STATE]
proof (state)
this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // domain_permutation A B). univ (\<lambda>f. bij_betw f A B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
using equiv_domain_permutation[of A B] bij_betw_respects_domain_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (domain_permutation A B)
(\<lambda>f. bij_betw f A B) respects domain_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B. univ (\<lambda>f. bij_betw f A B) F}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
from F_in this
[PROOF STATE]
proof (chain)
picking this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
have "F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B"
      and "univ (\<lambda>f. bij_betw f A B) F"
[PROOF STATE]
proof (prove)
using this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B. univ (\<lambda>f. bij_betw f A B) F}

goal (1 subgoal):
 1. F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B &&& univ (\<lambda>f. bij_betw f A B) F
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B

goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by (metis ImageE equiv_class_eq_iff equiv_domain_permutation quotientE)
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using univ_predicate_impl_forall[OF equiv_domain_permutation bij_betw_respects_domain_permutation]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // domain_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // domain_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1
F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. bij_betw f A B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
show "F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B

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

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
assume "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (state)
this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B" "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and "F = domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: quotientE)
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
F = domain_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
have "bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using univ_commute'[OF equiv_domain_permutation bij_betw_respects_domain_permutation]
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (domain_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1

goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>F = domain_permutation A B `` {f}\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (domain_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1
f \<in> A \<rightarrow>\<^sub>E B
F = domain_permutation A B `` {f}
univ (\<lambda>f. bij_betw f A B) F

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain p where "p permutes A" "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
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]
using obtain_domain_permutation_for_two_bijections
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?A; \<forall>a\<in>?A. ?f a = ?f' (p a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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]
using \<open>bij_betw f A B\<close> \<open>bij_betw f' A B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?A; \<forall>a\<in>?A. ?f a = ?f' (p a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
bij_betw f A B
bij_betw f' 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]
by blast
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
have "(f, f') \<in> domain_permutation A B"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. (f, f') \<in> domain_permutation A B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E 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. 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 (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> domain_permutation A B
[PROOF STEP]
show "f' \<in> F"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
using \<open>F = domain_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_permutation A B
F = domain_permutation A B `` {f}

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' \<in> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bijections_in_range_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
card A = card B
[PROOF STEP]
obtain f where f: "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
card A = card B

goal (1 subgoal):
 1. (\<And>f. f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
have proj_f: "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = range_permutation A B `` {f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> range_permutation A B `` {f}
 2. range_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> range_permutation A B `` {f}
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> {(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)))} `` {f}
[PROOF STEP]
by (auto elim: obtain_range_permutation_for_two_bijections)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> range_permutation A B `` {f}

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

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "(f', f) \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f', f) \<in> range_permutation A B
[PROOF STEP]
using \<open>f' \<in> range_permutation A B `` {f}\<close> equiv_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
f' \<in> range_permutation A B `` {f}
equiv (A \<rightarrow>\<^sub>E B) (range_permutation A B)

goal (1 subgoal):
 1. (f', f) \<in> range_permutation A B
[PROOF STEP]
by (simp add: equiv_class_eq_iff)
[PROOF STATE]
proof (state)
this:
(f', f) \<in> range_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f 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" "\<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. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p permutes B
\<forall>x\<in>A. f' x = p (f x)
[PROOF STEP]
have "bij_betw (p \<circ> f) A B"
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f' x = p (f x)

goal (1 subgoal):
 1. bij_betw (p \<circ> f) A B
[PROOF STEP]
using bij_betw_comp_iff f permutes_imp_bij
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f' x = p (f x)
bij_betw ?f ?A ?A' \<Longrightarrow> bij_betw ?f' ?A' ?A'' = bij_betw (?f' \<circ> ?f) ?A ?A''
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
?p permutes ?S \<Longrightarrow> bij_betw ?p ?S ?S

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

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (p \<circ> f) A B
[PROOF STEP]
have "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw (p \<circ> f) A B

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

goal (1 subgoal):
 1. bij_betw f' A B
[PROOF STEP]
by (metis (mono_tags, lifting) bij_betw_cong comp_apply)
[PROOF STATE]
proof (state)
this:
bij_betw f' A B

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw f' A B

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>f' \<in> range_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
f' \<in> range_permutation A B `` {f}

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
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)))} `` {f}

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. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = range_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = range_permutation A B `` {f}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = range_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
by (simp add: quotientI)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_quotient_range_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
 2. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
show "{{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
by (simp add: bijections_in_range_permutation[OF assms])
[PROOF STATE]
proof (state)
this:
{{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
assume F_in: "F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B"
[PROOF STATE]
proof (state)
this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // range_permutation A B). univ (\<lambda>f. bij_betw f A B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
using equiv_range_permutation[of A B] bij_betw_respects_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (range_permutation A B)
(\<lambda>f. bij_betw f A B) respects range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
from this F_in
[PROOF STATE]
proof (chain)
picking this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B
[PROOF STEP]
have "F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
      and "univ (\<lambda>f. bij_betw f A B) F"
[PROOF STATE]
proof (prove)
using this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B

goal (1 subgoal):
 1. F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B &&& univ (\<lambda>f. bij_betw f A B) F
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by (metis ImageE equiv_class_eq_iff equiv_range_permutation quotientE)
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using univ_predicate_impl_forall[OF equiv_range_permutation bij_betw_respects_range_permutation]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // range_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // range_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. bij_betw f A B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
show "F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B

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

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
assume "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (state)
this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B" "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and "F = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: quotientE)
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
have "bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using univ_commute'[OF equiv_range_permutation bij_betw_respects_range_permutation]
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (range_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1

goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>F = range_permutation A B `` {f}\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (range_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}
univ (\<lambda>f. bij_betw f A B) F

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain p where "p permutes B" "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
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]
using obtain_range_permutation_for_two_bijections
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?B; \<forall>a\<in>?A. ?f a = p (?f' a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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]
using \<open>bij_betw f A B\<close> \<open>bij_betw f' A B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?B; \<forall>a\<in>?A. ?f a = p (?f' a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
bij_betw f A B
bij_betw f' 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]
by blast
[PROOF STATE]
proof (state)
this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
have "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. (f, f') \<in> range_permutation A B
[PROOF STEP]
unfolding range_permutation_def
[PROOF STATE]
proof (prove)
using this:
p permutes B
\<forall>x\<in>A. f x = p (f' x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E 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. 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 (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f, f') \<in> range_permutation A B
[PROOF STEP]
show "f' \<in> F"
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
using \<open>F = range_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B
F = range_permutation A B `` {f}

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' \<in> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_bijections_range_permutation_eq_1:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B) = 1
[PROOF STEP]
using bij_betw_quotient_range_permutation_eq[OF assms]
[PROOF STATE]
proof (prove)
using this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // range_permutation A B) = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma bijections_in_domain_and_range_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
card A = card B
[PROOF STEP]
obtain f where f: "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
card A = card B

goal (1 subgoal):
 1. (\<And>f. f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
have proj_f: "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_and_range_permutation A B `` {f}
 2. domain_and_range_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "id permutes A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id permutes A
[PROOF STEP]
by (simp add: permutes_id)
[PROOF STATE]
proof (state)
this:
id permutes A

goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_and_range_permutation A B `` {f}
 2. domain_and_range_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from f this
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
id permutes A
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_and_range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
id permutes A

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

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> {(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))))} `` {f}
[PROOF STEP]
by (fastforce elim: obtain_range_permutation_for_two_bijections)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_and_range_permutation A B `` {f}

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

goal (1 subgoal):
 1. \<And>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "(f', f) \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f', f) \<in> domain_and_range_permutation A B
[PROOF STEP]
using \<open>f' \<in> domain_and_range_permutation A B `` {f}\<close> equiv_domain_and_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
f' \<in> domain_and_range_permutation A B `` {f}
equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)

goal (1 subgoal):
 1. (f', f) \<in> domain_and_range_permutation A B
[PROOF STEP]
by (simp add: equiv_class_eq_iff)
[PROOF STATE]
proof (state)
this:
(f', f) \<in> domain_and_range_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f 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>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking 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))
[PROOF STEP]
have "bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B"
[PROOF STATE]
proof (prove)
using 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. bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B
[PROOF STEP]
using bij_betw_comp_iff f permutes_imp_bij
[PROOF STATE]
proof (prove)
using 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))
bij_betw ?f ?A ?A' \<Longrightarrow> bij_betw ?f' ?A' ?A'' = bij_betw (?f' \<circ> ?f) ?A ?A''
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
?p permutes ?S \<Longrightarrow> bij_betw ?p ?S ?S

goal (1 subgoal):
 1. bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B
[PROOF STEP]
by (metis (no_types, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B
[PROOF STEP]
have "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw (p\<^sub>B \<circ> f \<circ> p\<^sub>A) A B

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw f' A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>f' \<in> domain_and_range_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
f' \<in> domain_and_range_permutation A B `` {f}

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' \<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))))} `` {f}

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. x \<in> domain_and_range_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_and_range_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
by (simp add: quotientI)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_quotient_domain_and_range_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
 2. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
show "{{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
    \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
[PROOF STEP]
using bijections_in_domain_and_range_permutation[OF assms]
[PROOF STATE]
proof (prove)
using this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B

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

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
assume F_in: "F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B"
[PROOF STATE]
proof (state)
this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B). univ (\<lambda>f. bij_betw f A B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
using equiv_domain_and_range_permutation[of A B] bij_betw_respects_domain_and_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
(\<lambda>f. bij_betw f A B) respects domain_and_range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
from F_in this
[PROOF STATE]
proof (chain)
picking this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}
[PROOF STEP]
have "F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
      and "univ (\<lambda>f. bij_betw f A B) F"
[PROOF STATE]
proof (prove)
using this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. bij_betw f A B) F}

goal (1 subgoal):
 1. F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B &&& univ (\<lambda>f. bij_betw f A B) F
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
have "F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B

goal (1 subgoal):
 1. \<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by (metis ImageE equiv_class_eq_iff equiv_domain_and_range_permutation quotientE)
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
have "\<forall>f \<in> F. bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using univ_predicate_impl_forall[OF equiv_domain_and_range_permutation bij_betw_respects_domain_and_range_permutation]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // domain_and_range_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> (?A1 \<rightarrow>\<^sub>E ?B1) // domain_and_range_permutation ?A1 ?B1; univ (\<lambda>f. bij_betw f ?A1 ?B1) ?X\<rbrakk> \<Longrightarrow> \<forall>x\<in>?X. bij_betw x ?A1 ?B1
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
univ (\<lambda>f. bij_betw f A B) F

goal (1 subgoal):
 1. \<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>F. bij_betw f A B

goal (2 subgoals):
 1. F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
 2. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B
[PROOF STEP]
show "F \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>F. f \<in> A \<rightarrow>\<^sub>E B
\<forall>f\<in>F. bij_betw f A B

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

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
assume "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (state)
this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B" "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and "F = domain_and_range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_and_range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_and_range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: quotientE)
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
F = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
have "bij_betw f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using univ_commute'[OF equiv_domain_and_range_permutation bij_betw_respects_domain_and_range_permutation]
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (domain_and_range_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1

goal (1 subgoal):
 1. bij_betw f A B
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>F = domain_and_range_permutation A B `` {f}\<close> \<open>univ (\<lambda>f. bij_betw f A B) F\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A1 \<rightarrow>\<^sub>E ?B1 \<Longrightarrow> univ (\<lambda>f. bij_betw f ?A1 ?B1) (domain_and_range_permutation ?A1 ?B1 `` {?x}) = bij_betw ?x ?A1 ?B1
f \<in> A \<rightarrow>\<^sub>E B
F = domain_and_range_permutation A B `` {f}
univ (\<lambda>f. bij_betw f A B) F

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

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain p where "p permutes A" "\<forall>x\<in>A. f x = f' (p x)"
[PROOF STATE]
proof (prove)
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]
using obtain_domain_permutation_for_two_bijections
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?A; \<forall>a\<in>?A. ?f a = ?f' (p a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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]
using \<open>bij_betw f A B\<close> \<open>bij_betw f' A B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?f' ?A ?B; \<And>p. \<lbrakk>p permutes ?A; \<forall>a\<in>?A. ?f a = ?f' (p a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
bij_betw f A B
bij_betw f' 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]
by blast
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
have "id permutes B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id permutes B
[PROOF STEP]
by (simp add: permutes_id)
[PROOF STATE]
proof (state)
this:
id permutes B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
id permutes B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
note \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> x \<in> F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
id permutes B
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
have "(f, f') \<in> domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
id permutes B
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

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

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

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
using \<open>F = domain_and_range_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> domain_and_range_permutation A B
F = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. f' \<in> F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' \<in> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. \<And>x. x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<Longrightarrow> x \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
show "F \<in> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}"
[PROOF STATE]
proof (prove)
using this:
F = {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B \<subseteq> {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_bijections_domain_and_range_permutation_eq_1:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B) = 1
[PROOF STEP]
using bij_betw_quotient_domain_and_range_permutation_eq[OF assms]
[PROOF STATE]
proof (prove)
using this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B = {{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_and_range_permutation A B) = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma normalized_src_ports_def2: "normalized_src_ports ms = normalized_n_primitive (is_Src_Ports, src_ports_sel) (\<lambda>ps. case ps of L4Ports _ pts \<Rightarrow> length pts \<le> 1) ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_src_ports ms = normalized_n_primitive (is_Src_Ports, src_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) ms
[PROOF STEP]
by(induction ms rule: normalized_src_ports.induct, simp_all)


[STATEMENT]
lemma normalized_dst_ports_def2: "normalized_dst_ports ms = normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (\<lambda>ps. case ps of L4Ports _ pts \<Rightarrow> length pts \<le> 1) ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_dst_ports ms = normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) ms
[PROOF STEP]
by(induction ms rule: normalized_dst_ports.induct, simp_all)


[STATEMENT]
lemma raw_ports_compress_src_CannotMatch:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  and c: "l4_ports_compress pss = CannotMatch"
  shows "\<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
l4_ports_compress pss = CannotMatch

goal (1 subgoal):
 1. \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
apply(induction pss rule: l4_ports_compress.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l4_ports_compress [] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [])) a p
 2. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto ps])) a p
 3. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto ps])) a p
 2. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: primitive_matcher_generic.Ports_single[OF generic] bunch_of_lemmata_about_matches split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto1 ps1 proto2 ps2 pss. proto1 \<noteq> proto2 \<Longrightarrow> p_sport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_sport p \<in> ports_to_set ps1 \<longrightarrow> proto1 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
 2. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>p_sport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<longrightarrow> proto2 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p; proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> p_sport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_sport p \<in> ports_to_set ps1 \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
apply meson
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>p_sport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<longrightarrow> proto2 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p; proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> p_sport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_sport p \<in> ports_to_set ps1 \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
by(simp add: l2wi_wi2l ports_to_set_wordinterval)


[STATEMENT]
lemma raw_ports_compress_dst_CannotMatch:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  and c: "l4_ports_compress pss = CannotMatch"
  shows "\<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
l4_ports_compress pss = CannotMatch

goal (1 subgoal):
 1. \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
apply(induction pss rule: l4_ports_compress.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l4_ports_compress [] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [])) a p
 2. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto ps])) a p
 3. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = CannotMatch \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto ps])) a p
 2. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: primitive_matcher_generic.Ports_single[OF generic] bunch_of_lemmata_about_matches split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto1 ps1 proto2 ps2 pss. proto1 \<noteq> proto2 \<Longrightarrow> p_dport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_dport p \<in> ports_to_set ps1 \<longrightarrow> proto1 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
 2. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>p_dport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<longrightarrow> proto2 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p; proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> p_dport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_dport p \<in> ports_to_set ps1 \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
apply meson
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>p_dport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<longrightarrow> proto2 = p_proto p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p; proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = CannotMatch\<rbrakk> \<Longrightarrow> p_dport p \<in> ports_to_set ps2 \<longrightarrow> proto2 = p_proto p \<longrightarrow> p_dport p \<in> ports_to_set ps1 \<longrightarrow> \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
by(simp add: l2wi_wi2l ports_to_set_wordinterval)


[STATEMENT]
lemma l4_ports_compress_length_Matchall: "length pss > 0 \<Longrightarrow> l4_ports_compress pss \<noteq> MatchesAll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length pss \<Longrightarrow> l4_ports_compress pss \<noteq> MatchesAll
[PROOF STEP]
by(induction pss rule: l4_ports_compress.induct) simp+


[STATEMENT]
lemma raw_ports_compress_MatchesAll:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  and c: "l4_ports_compress pss = MatchesAll"
  shows "matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p"
  and "matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p &&& matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
l4_ports_compress pss = MatchesAll

goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p &&& matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
apply(induction pss rule: l4_ports_compress.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. l4_ports_compress [] = MatchesAll \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [])) a p
 2. l4_ports_compress [] = MatchesAll \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [])) a p
 3. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = MatchesAll \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto ps])) a p
 4. \<And>proto ps. l4_ports_compress [L4Ports proto ps] = MatchesAll \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto ps])) a p
 5. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
 6. \<And>proto1 ps1 proto2 ps2 pss. \<lbrakk>\<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchesAll\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
by(simp add: l4_ports_compress_length_Matchall bunch_of_lemmata_about_matches split: if_split_asm)+