[STATEMENT]
theorem equiv_rels:
  assumes "equiv {..<n} r"
  shows "count_list (equiv_rels n) r = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
obtain y where y_def: "rgf y" "length y = n" "kernel_of y = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>rgf y; length y = n; kernel_of y = r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rgf_exists assms
[PROOF STATE]
proof (prove)
using this:
equiv {..<?n} ?r \<Longrightarrow> \<exists>x. rgf x \<and> length x = ?n \<and> kernel_of x = ?r
equiv {..<n} r

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>rgf y; length y = n; kernel_of y = r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rgf y
length y = n
kernel_of y = r

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have a: "\<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y=x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y = x)
[PROOF STEP]
using enum_rgfs_returns_rgfs y_def(1,2) enum_rgfs_len inj_onD[OF kernel_of_inj_on_rgfs]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (enum_rgfs ?n) \<Longrightarrow> rgf ?x
rgf y
length y = n
?x \<in> set (enum_rgfs ?n) \<Longrightarrow> length ?x = ?n
\<lbrakk>kernel_of ?x = kernel_of ?y; ?x \<in> {x. rgf x}; ?y \<in> {x. rgf x}\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y = x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of ?x) = (y = ?x)

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "count_list (equiv_rels n) r = 
    length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))
[PROOF STEP]
by (simp add:equiv_rels_def count_list_expand length_filter comp_def)
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))
[PROOF STEP]
using y_def(3)
[PROOF STATE]
proof (prove)
using this:
kernel_of y = r

goal (1 subgoal):
 1. length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = length (filter (\<lambda>x. y = x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of ?x) = (y = ?x)

goal (1 subgoal):
 1. length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))
[PROOF STEP]
by (simp cong:filter_cong)
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = count_list (enum_rgfs n) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y
[PROOF STEP]
by (simp add:count_list_expand length_filter)
[PROOF STATE]
proof (state)
this:
length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (enum_rgfs n) y = 1
[PROOF STEP]
using equiv_rels_enum y_def(1,2)
[PROOF STATE]
proof (prove)
using this:
rgf ?x \<Longrightarrow> count_list (enum_rgfs (length ?x)) ?x = 1
rgf y
length y = n

goal (1 subgoal):
 1. count_list (enum_rgfs n) y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
count_list (enum_rgfs n) y = 1

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count_list (equiv_rels n) r = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count_list (equiv_rels n) r = 1

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = 1

goal:
No subgoals!
[PROOF STEP]
qed