[STATEMENT]
lemma injectivity_subexpr1:
  assumes "a \<notin> A"
  assumes "X \<in> P \<and> X' \<in> P'"
  assumes "insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})"
  assumes "(partition_on A P \<and> card P = Suc k') \<and> (partition_on A P' \<and> card P' = Suc k')"
  shows "P = P'" and "X = X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = P' &&& X = X'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = P'
 2. X = X'
[PROOF STEP]
from assms(1, 2, 4)
[PROOF STATE]
proof (chain)
picking this:
a \<notin> A
X \<in> P \<and> X' \<in> P'
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'
[PROOF STEP]
have "a \<notin> X" "a \<notin> X'"
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
X \<in> P \<and> X' \<in> P'
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'

goal (1 subgoal):
 1. a \<notin> X &&& a \<notin> X'
[PROOF STEP]
using partition_onD1
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
X \<in> P \<and> X' \<in> P'
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. a \<notin> X &&& a \<notin> X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> X
a \<notin> X'

goal (2 subgoals):
 1. P = P'
 2. X = X'
[PROOF STEP]
from assms(1, 4)
[PROOF STATE]
proof (chain)
picking this:
a \<notin> A
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'
[PROOF STEP]
have "insert a X \<notin> P" "insert a X' \<notin> P'"
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'

goal (1 subgoal):
 1. insert a X \<notin> P &&& insert a X' \<notin> P'
[PROOF STEP]
using partition_onD1
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. insert a X \<notin> P &&& insert a X' \<notin> P'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a X \<notin> P
insert a X' \<notin> P'

goal (2 subgoals):
 1. P = P'
 2. X = X'
[PROOF STEP]
from assms(1, 3, 4)
[PROOF STATE]
proof (chain)
picking this:
a \<notin> A
insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'
[PROOF STEP]
have "insert a X = insert a X'"
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})
(partition_on A P \<and> card P = Suc k') \<and> partition_on A P' \<and> card P' = Suc k'

goal (1 subgoal):
 1. insert a X = insert a X'
[PROOF STEP]
by (metis Diff_iff insertE insertI1 mem_simps(9) partition_onD1)
[PROOF STATE]
proof (state)
this:
insert a X = insert a X'

goal (2 subgoals):
 1. P = P'
 2. X = X'
[PROOF STEP]
from this \<open>a \<notin> X'\<close> \<open>a \<notin> X\<close>
[PROOF STATE]
proof (chain)
picking this:
insert a X = insert a X'
a \<notin> X'
a \<notin> X
[PROOF STEP]
show "X = X'"
[PROOF STATE]
proof (prove)
using this:
insert a X = insert a X'
a \<notin> X'
a \<notin> X

goal (1 subgoal):
 1. X = X'
[PROOF STEP]
by (meson insert_ident)
[PROOF STATE]
proof (state)
this:
X = X'

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
from assms(2, 3)
[PROOF STATE]
proof (chain)
picking this:
X \<in> P \<and> X' \<in> P'
insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})
[PROOF STEP]
show "P = P'"
[PROOF STATE]
proof (prove)
using this:
X \<in> P \<and> X' \<in> P'
insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
using \<open>insert a X = insert a X'\<close> \<open>insert a X \<notin> P\<close> \<open>insert a X' \<notin> P'\<close>
[PROOF STATE]
proof (prove)
using this:
X \<in> P \<and> X' \<in> P'
insert (insert a X) (P - {X}) = insert (insert a X') (P' - {X'})
insert a X = insert a X'
insert a X \<notin> P
insert a X' \<notin> P'

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
by (metis insert_Diff insert_absorb insert_commute insert_ident)
[PROOF STATE]
proof (state)
this:
P = P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma injectivity_subexpr2:
  assumes "a \<notin> A"
  assumes "insert {a} P = insert {a} P'"
  assumes "(partition_on A P \<and> card P = k') \<and> partition_on A P' \<and> card P' = k'"
  shows "P = P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P = P'
[PROOF STEP]
from assms(1, 3)
[PROOF STATE]
proof (chain)
picking this:
a \<notin> A
(partition_on A P \<and> card P = k') \<and> partition_on A P' \<and> card P' = k'
[PROOF STEP]
have "{a} \<notin> P" and "{a} \<notin> P'"
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
(partition_on A P \<and> card P = k') \<and> partition_on A P' \<and> card P' = k'

goal (1 subgoal):
 1. {a} \<notin> P &&& {a} \<notin> P'
[PROOF STEP]
using partition_onD1
[PROOF STATE]
proof (prove)
using this:
a \<notin> A
(partition_on A P \<and> card P = k') \<and> partition_on A P' \<and> card P' = k'
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. {a} \<notin> P &&& {a} \<notin> P'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a} \<notin> P
{a} \<notin> P'

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
from \<open>{a} \<notin> P\<close>
[PROOF STATE]
proof (chain)
picking this:
{a} \<notin> P
[PROOF STEP]
have "P = insert {a} P - {{a}}"
[PROOF STATE]
proof (prove)
using this:
{a} \<notin> P

goal (1 subgoal):
 1. P = insert {a} P - {{a}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P = insert {a} P - {{a}}

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P = insert {a} P - {{a}}

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
from \<open>insert {a} P = insert {a} P'\<close>
[PROOF STATE]
proof (chain)
picking this:
insert {a} P = insert {a} P'
[PROOF STEP]
have "\<dots> = insert {a} P' - {{a}}"
[PROOF STATE]
proof (prove)
using this:
insert {a} P = insert {a} P'

goal (1 subgoal):
 1. insert {a} P - {{a}} = insert {a} P' - {{a}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert {a} P - {{a}} = insert {a} P' - {{a}}

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insert {a} P - {{a}} = insert {a} P' - {{a}}

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
from \<open>{a} \<notin> P'\<close>
[PROOF STATE]
proof (chain)
picking this:
{a} \<notin> P'
[PROOF STEP]
have "\<dots> = P'"
[PROOF STATE]
proof (prove)
using this:
{a} \<notin> P'

goal (1 subgoal):
 1. insert {a} P' - {{a}} = P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert {a} P' - {{a}} = P'

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

goal (1 subgoal):
 1. P = P'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P = P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem card_partition_on:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> card P = k} = Stirling (card A) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k
[PROOF STEP]
proof (induct A arbitrary: k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. card {P. partition_on {} P \<and> card P = k} = Stirling (card {}) k
 2. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>k. card {P. partition_on {} P \<and> card P = k} = Stirling (card {}) k
 2. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
have eq: "{P. P = {} \<and> card P = 0} = {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P. P = {} \<and> card P = 0} = {{}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{P. P = {} \<and> card P = 0} = {{}}

goal (2 subgoals):
 1. \<And>k. card {P. partition_on {} P \<and> card P = k} = Stirling (card {}) k
 2. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on {} P \<and> card P = k} = Stirling (card {}) k
[PROOF STEP]
by (cases k) (auto simp add: partition_on_empty eq)
[PROOF STATE]
proof (state)
this:
card {P. partition_on {} P \<and> card P = k} = Stirling (card {}) k

goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
case (insert a A)
[PROOF STATE]
proof (state)
this:
finite A
a \<notin> A
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k

goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. card {P. partition_on F P \<and> card P = k} = Stirling (card F) k\<rbrakk> \<Longrightarrow> card {P. partition_on (insert x F) P \<and> card P = k} = Stirling (card (insert x F)) k
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
finite A
a \<notin> A
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k

goal (1 subgoal):
 1. card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
proof (cases k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = 0\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
 2. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = 0\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
 2. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
from insert(1)
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have empty: "{P. partition_on (insert a A) P \<and> card P = 0} = {}"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. {P. partition_on (insert a A) P \<and> card P = 0} = {}
[PROOF STEP]
unfolding partition_on_def
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. {P. (\<Union> P = insert a A \<and> disjoint P \<and> {} \<notin> P) \<and> card P = 0} = {}
[PROOF STEP]
by (auto simp add: card_eq_0_iff finite_UnionD)
[PROOF STATE]
proof (state)
this:
{P. partition_on (insert a A) P \<and> card P = 0} = {}

goal (2 subgoals):
 1. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = 0\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
 2. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
from 0 insert
[PROOF STATE]
proof (chain)
picking this:
k = 0
finite A
a \<notin> A
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0
finite A
a \<notin> A
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k

goal (1 subgoal):
 1. card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
by (auto simp add: empty)
[PROOF STATE]
proof (state)
this:
card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
k = Suc k'

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
let ?subexpr1 = "do {
      P <- {P. partition_on A P \<and> card P = Suc k'};
      p <- P;
      {insert (insert a p) (P - {p})}
    }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
let ?subexpr2 = "do {
      P <- {P. partition_on A P \<and> card P = k'};
      {insert {a} P}
    }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
let ?expr = "?subexpr1 \<union> ?subexpr2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
have "card {P. partition_on (insert a A) P \<and> card P = k} = card ?expr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on (insert a A) P \<and> card P = k} = card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})))
[PROOF STEP]
using \<open>finite A\<close> \<open>a \<notin> A\<close> \<open>k = Suc k'\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
k = Suc k'

goal (1 subgoal):
 1. card {P. partition_on (insert a A) P \<and> card P = k} = card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})))
[PROOF STEP]
by (simp add: set_partition_on_insert_with_fixed_card_eq)
[PROOF STATE]
proof (state)
this:
card {P. partition_on (insert a A) P \<and> card P = k} = card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})))

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {P. partition_on (insert a A) P \<and> card P = k} = card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})))

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
have "card ?expr = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "finite ?subexpr1 \<and> card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
from \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "finite {P. partition_on A P \<and> card P = Suc k'}"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. finite {P. partition_on A P \<and> card P = Suc k'}
[PROOF STEP]
by (simp add: finitely_many_partition_on)
[PROOF STATE]
proof (state)
this:
finite {P. partition_on A P \<and> card P = Suc k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {P. partition_on A P \<and> card P = Suc k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))
[PROOF STEP]
using finite_elements \<open>finite A\<close> finite_bind
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; partition_on ?A ?P\<rbrakk> \<Longrightarrow> finite ?P
finite A
\<lbrakk>finite ?S; \<forall>x\<in>?S. finite (?f x)\<rbrakk> \<Longrightarrow> finite (?S \<bind> ?f)

goal (1 subgoal):
 1. \<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))
[PROOF STEP]
by (metis (no_types, lifting) finite.emptyI finite_insert mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}
[PROOF STEP]
by (injectivity_solver rule: injectivity_subexpr1(1)[OF \<open>a \<notin> A\<close>])
[PROOF STATE]
proof (state)
this:
disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'"
          if "P \<in> {P. partition_on A P \<and> card P = Suc k'}" for P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
from that \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}
finite A
[PROOF STEP]
have "finite P"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}
finite A

goal (1 subgoal):
 1. finite P
[PROOF STEP]
using finite_elements
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}
finite A
\<lbrakk>finite ?A; partition_on ?A ?P\<rbrakk> \<Longrightarrow> finite ?P

goal (1 subgoal):
 1. finite P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite P

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite P

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
have "inj_on (\<lambda>p. insert (insert a p) (P - {p})) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>p. insert (insert a p) (P - {p})) P
[PROOF STEP]
using that injectivity_subexpr1(2)[OF \<open>a \<notin> A\<close>]
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}
\<lbrakk>?X \<in> ?P \<and> ?X' \<in> ?P'; insert (insert a ?X) (?P - {?X}) = insert (insert a ?X') (?P' - {?X'}); (partition_on A ?P \<and> card ?P = Suc ?k') \<and> partition_on A ?P' \<and> card ?P' = Suc ?k'\<rbrakk> \<Longrightarrow> ?X = ?X'

goal (1 subgoal):
 1. inj_on (\<lambda>p. insert (insert a p) (P - {p})) P
[PROOF STEP]
by (simp add: inj_onI)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>p. insert (insert a p) (P - {p})) P

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>p. insert (insert a p) (P - {p})) P

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}
[PROOF STEP]
have "card P = Suc k'"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k'}

goal (1 subgoal):
 1. card P = Suc k'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card P = Suc k'

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite P
inj_on (\<lambda>p. insert (insert a p) (P - {p})) P
card P = Suc k'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite P
inj_on (\<lambda>p. insert (insert a p) (P - {p})) P
card P = Suc k'

goal (1 subgoal):
 1. card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'
[PROOF STEP]
by (simp add: card_bind_singleton)
[PROOF STATE]
proof (state)
this:
card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?P \<in> {P. partition_on A P \<and> card P = Suc k'} \<Longrightarrow> card (?P \<bind> (\<lambda>p. {insert (insert a p) (?P - {p})})) = Suc k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {P. partition_on A P \<and> card P = Suc k'}
\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))
disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}
?P \<in> {P. partition_on A P \<and> card P = Suc k'} \<Longrightarrow> card (?P \<bind> (\<lambda>p. {insert (insert a p) (?P - {p})})) = Suc k'
[PROOF STEP]
have "card ?subexpr1 = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'"
[PROOF STATE]
proof (prove)
using this:
finite {P. partition_on A P \<and> card P = Suc k'}
\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))
disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}
?P \<in> {P. partition_on A P \<and> card P = Suc k'} \<Longrightarrow> card (?P \<bind> (\<lambda>p. {insert (insert a p) (?P - {p})})) = Suc k'

goal (1 subgoal):
 1. card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'
[PROOF STEP]
by (subst card_bind_constant) simp+
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'
[PROOF STEP]
have "card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
[PROOF STATE]
proof (prove)
using this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'

goal (1 subgoal):
 1. card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
using insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k

goal (1 subgoal):
 1. card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "finite ?subexpr1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})))
[PROOF STEP]
using \<open>finite {P. partition_on A P \<and> card P = Suc k'}\<close>
          \<open>\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))\<close>
[PROOF STATE]
proof (prove)
using this:
finite {P. partition_on A P \<and> card P = Suc k'}
\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})))
[PROOF STEP]
by (auto intro: finite_bind)
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "finite ?subexpr2 \<and> card ?subexpr2 = Stirling (card A) k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
from \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "finite {P. partition_on A P \<and> card P = k'}"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. finite {P. partition_on A P \<and> card P = k'}
[PROOF STEP]
by (simp add: finitely_many_partition_on)
[PROOF STATE]
proof (state)
this:
finite {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
have " inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}
[PROOF STEP]
using injectivity_subexpr2[OF \<open>a \<notin> A\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>insert {a} ?P = insert {a} ?P'; (partition_on A ?P \<and> card ?P = ?k') \<and> partition_on A ?P' \<and> card ?P' = ?k'\<rbrakk> \<Longrightarrow> ?P = ?P'

goal (1 subgoal):
 1. inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}
[PROOF STEP]
by (simp add: inj_on_def)
[PROOF STATE]
proof (state)
this:
inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {P. partition_on A P \<and> card P = k'}
inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}
[PROOF STEP]
have "card ?subexpr2 = card {P. partition_on A P \<and> card P = k'}"
[PROOF STATE]
proof (prove)
using this:
finite {P. partition_on A P \<and> card P = k'}
inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = card {P. partition_on A P \<and> card P = k'}
[PROOF STEP]
by (simp add: card_bind_singleton)
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = card {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = card {P. partition_on A P \<and> card P = k'}

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
have "\<dots> = Stirling (card A) k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = k'} = Stirling (card A) k'
[PROOF STEP]
using insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
card {P. partition_on A P \<and> card P = ?k} = Stirling (card A) ?k

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = k'} = Stirling (card A) k'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P = k'} = Stirling (card A) k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
have "card ?subexpr2 = Stirling (card A) k'"
[PROOF STATE]
proof (prove)
using this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal (1 subgoal):
 1. card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
have "finite ?subexpr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
by (simp add: \<open>finite {P. partition_on A P \<and> card P = k'}\<close> finite_bind)
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
have "?subexpr1 \<inter> ?subexpr2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
have "\<forall>P\<in>?subexpr1. {a} \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P
[PROOF STEP]
using insert.hyps(2)
[PROOF STATE]
proof (prove)
using this:
a \<notin> A

goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P
[PROOF STEP]
by (force elim!: partition_onE)
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P

goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P

goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
have "\<forall>P\<in>?subexpr2. {a} \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}). {a} \<in> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>{P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}). {a} \<in> P

goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P
\<forall>P\<in>{P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}). {a} \<in> P
[PROOF STEP]
show "?subexpr1 \<inter> ?subexpr2 = {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>{P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})). {a} \<notin> P
\<forall>P\<in>{P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}). {a} \<in> P

goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<and> card ({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) = Stirling (card A) (Suc k') * Suc k'
finite ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) \<and> card ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = Stirling (card A) k'
({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<inter> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P})) = {}

goal (1 subgoal):
 1. card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'
[PROOF STEP]
by (simp add: card_Un_disjoint)
[PROOF STATE]
proof (state)
this:
card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (({P. partition_on A P \<and> card P = Suc k'} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k'} \<bind> (\<lambda>P. {insert {a} P}))) = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
have "\<dots> = Stirling (card (insert a A)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k' = Stirling (card (insert a A)) k
[PROOF STEP]
using insert(1, 2) \<open>k = Suc k'\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
k = Suc k'

goal (1 subgoal):
 1. Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k' = Stirling (card (insert a A)) k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k' = Stirling (card (insert a A)) k

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>finite A; a \<notin> A; \<And>k. card {P. partition_on A P \<and> card P = k} = Stirling (card A) k; k = Suc nat\<rbrakk> \<Longrightarrow> card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k

goal (1 subgoal):
 1. card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {P. partition_on (insert a A) P \<and> card P = k} = Stirling (card (insert a A)) k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem card_partition_on_at_most_size:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> card P \<le> k} = (\<Sum>j\<le>k. Stirling (card A) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
have "card {P. partition_on A P \<and> card P \<le> k} = card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j})
[PROOF STEP]
by (rule arg_cong[where f="card"]) auto
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P \<le> k} = card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j})

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P \<le> k} = card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j})

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
have "\<dots> = (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j}) = (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j})
[PROOF STEP]
by (subst card_UN_disjoint) (auto simp add: \<open>finite A\<close> finitely_many_partition_on)
[PROOF STATE]
proof (state)
this:
card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j}) = (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j})

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j}) = (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j})

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
have "(\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j}) = (\<Sum>j\<le>k. Stirling (card A) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j}) = sum (Stirling (card A)) {..k}
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j}) = sum (Stirling (card A)) {..k}
[PROOF STEP]
by (simp add: card_partition_on)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j}) = sum (Stirling (card A)) {..k}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P \<le> k} = sum (Stirling (card A)) {..k}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem partition_on_size1:
  assumes "finite A"
  shows "{P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<subseteq> {(\<lambda>a. {a}) ` A}
 2. {(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
show "{P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<subseteq> {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<subseteq> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<Longrightarrow> x \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<Longrightarrow> x \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
assume P: "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<Longrightarrow> x \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
have "P = (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = (\<lambda>a. {a}) ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<subseteq> (\<lambda>a. {a}) ` A
 2. (\<lambda>a. {a}) ` A \<subseteq> P
[PROOF STEP]
show "P \<subseteq> (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> (\<lambda>a. {a}) ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
assume "X \<in> P"
[PROOF STATE]
proof (state)
this:
X \<in> P

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
from P this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
X \<in> P
[PROOF STEP]
obtain x where "X = {x}"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
X \<in> P

goal (1 subgoal):
 1. (\<And>x. X = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: card_Suc_eq)
[PROOF STATE]
proof (state)
this:
X = {x}

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
from this \<open>X \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
X = {x}
X \<in> P
[PROOF STEP]
have "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
X = {x}
X \<in> P

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
X = {x}
X \<in> P
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
unfolding partition_on_def
[PROOF STATE]
proof (prove)
using this:
X = {x}
X \<in> P
P \<in> {P. (\<Union> P = A \<and> disjoint P \<and> {} \<notin> P) \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
from this \<open>X = {x}\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
X = {x}
[PROOF STEP]
show "X \<in>(\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
X = {x}

goal (1 subgoal):
 1. X \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<in> (\<lambda>a. {a}) ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<subseteq> (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. (\<lambda>a. {a}) ` A \<subseteq> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>a. {a}) ` A \<subseteq> P
[PROOF STEP]
show "(\<lambda>a. {a}) ` A \<subseteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. {a}) ` A \<subseteq> P
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
assume "X \<in> (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (state)
this:
X \<in> (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
X \<in> (\<lambda>a. {a}) ` A
[PROOF STEP]
obtain x where X: "X = {x}" "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>X = {x}; x \<in> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X = {x}
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
have "\<Union>P = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> P = A
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. \<Union> P = A
[PROOF STEP]
unfolding partition_on_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. (\<Union> P = A \<and> disjoint P \<and> {} \<notin> P) \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. \<Union> P = A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> P = A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
from this \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Union> P = A
x \<in> A
[PROOF STEP]
obtain X' where "x \<in> X'" and "X' \<in> P"
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A
x \<in> A

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>x \<in> X'; X' \<in> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using UnionE
[PROOF STATE]
proof (prove)
using this:
\<Union> P = A
x \<in> A
\<lbrakk>?A \<in> \<Union> ?C; \<And>X. \<lbrakk>?A \<in> X; X \<in> ?C\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>x \<in> X'; X' \<in> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> X'
X' \<in> P

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
from \<open>X' \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
X' \<in> P
[PROOF STEP]
have "card X' = 1"
[PROOF STATE]
proof (prove)
using this:
X' \<in> P

goal (1 subgoal):
 1. card X' = 1
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
X' \<in> P
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card X' = 1
[PROOF STEP]
unfolding partition_on_def
[PROOF STATE]
proof (prove)
using this:
X' \<in> P
P \<in> {P. (\<Union> P = A \<and> disjoint P \<and> {} \<notin> P) \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card X' = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card X' = 1

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
from this \<open>x \<in> X'\<close>
[PROOF STATE]
proof (chain)
picking this:
card X' = 1
x \<in> X'
[PROOF STEP]
have "X' = {x}"
[PROOF STATE]
proof (prove)
using this:
card X' = 1
x \<in> X'

goal (1 subgoal):
 1. X' = {x}
[PROOF STEP]
using card_1_singletonE
[PROOF STATE]
proof (prove)
using this:
card X' = 1
x \<in> X'
\<lbrakk>card ?A = 1; \<And>x. ?A = {x} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. X' = {x}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X' = {x}

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>a. {a}) ` A \<Longrightarrow> x \<in> P
[PROOF STEP]
from this X(1) \<open>X' \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
X' = {x}
X = {x}
X' \<in> P
[PROOF STEP]
show "X \<in> P"
[PROOF STATE]
proof (prove)
using this:
X' = {x}
X = {x}
X' \<in> P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>a. {a}) ` A \<subseteq> P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<Longrightarrow> x \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>a. {a}) ` A
[PROOF STEP]
show "P \<in> {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {(\<lambda>a. {a}) ` A}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<subseteq> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. {(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
show "{(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(\<lambda>a. {a}) ` A} \<Longrightarrow> x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(\<lambda>a. {a}) ` A} \<Longrightarrow> x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
assume "P \<in> {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (state)
this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. \<And>x. x \<in> {(\<lambda>a. {a}) ` A} \<Longrightarrow> x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
have P: "P = (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
using this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. P = (\<lambda>a. {a}) ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. \<And>x. x \<in> {(\<lambda>a. {a}) ` A} \<Longrightarrow> x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>a. {a}) ` A
[PROOF STEP]
have "partition_on A P"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. partition_on A P
[PROOF STEP]
by (auto intro: partition_onI)
[PROOF STATE]
proof (state)
this:
partition_on A P

goal (1 subgoal):
 1. \<And>x. x \<in> {(\<lambda>a. {a}) ` A} \<Longrightarrow> x \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
from P this
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>a. {a}) ` A
partition_on A P
[PROOF STEP]
show "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>a. {a}) ` A
partition_on A P

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem card_partition_on_size1:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
using assms partition_on_size1
[PROOF STATE]
proof (prove)
using this:
finite A
finite ?A \<Longrightarrow> {P. partition_on ?A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` ?A}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
by fastforce


[STATEMENT]
lemma card_partition_on_size1_eq_1:
  assumes "finite A"
  assumes "card A \<le> k"
  shows "card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
assume "partition_on A P" "\<forall>X\<in>P. card X = 1"
[PROOF STATE]
proof (state)
this:
partition_on A P
\<forall>X\<in>P. card X = 1

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on A P
\<forall>X\<in>P. card X = 1
[PROOF STEP]
have "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (prove)
using this:
partition_on A P
\<forall>X\<in>P. card X = 1

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
have "P \<in> {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
using partition_on_size1 \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
finite ?A \<Longrightarrow> {P. partition_on ?A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` ?A}
finite A

goal (1 subgoal):
 1. P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
have "P = (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
using this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. P = (\<lambda>a. {a}) ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>a. {a}) ` A
[PROOF STEP]
have "card P = card A"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. card P = card A
[PROOF STEP]
by (auto intro: card_image)
[PROOF STATE]
proof (state)
this:
card P = card A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A
[PROOF STEP]
have "{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A

goal (1 subgoal):
 1. {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
using \<open>card A \<le> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A
card A \<le> k

goal (1 subgoal):
 1. {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
finite A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1
[PROOF STEP]
by (simp only: card_partition_on_size1)
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_partition_on_size1_eq_0:
  assumes "finite A"
  assumes "k < card A"
  shows "card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
assume "partition_on A P" "\<forall>X\<in>P. card X = 1"
[PROOF STATE]
proof (state)
this:
partition_on A P
\<forall>X\<in>P. card X = 1

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on A P
\<forall>X\<in>P. card X = 1
[PROOF STEP]
have "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
[PROOF STATE]
proof (prove)
using this:
partition_on A P
\<forall>X\<in>P. card X = 1

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
[PROOF STEP]
have "P \<in> {(\<lambda>a. {a}) ` A}"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}

goal (1 subgoal):
 1. P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
using partition_on_size1 \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}
finite ?A \<Longrightarrow> {P. partition_on ?A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` ?A}
finite A

goal (1 subgoal):
 1. P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {(\<lambda>a. {a}) ` A}
[PROOF STEP]
have "P = (\<lambda>a. {a}) ` A"
[PROOF STATE]
proof (prove)
using this:
P \<in> {(\<lambda>a. {a}) ` A}

goal (1 subgoal):
 1. P = (\<lambda>a. {a}) ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>a. {a}) ` A
[PROOF STEP]
have "card P = card A"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>a. {a}) ` A

goal (1 subgoal):
 1. card P = card A
[PROOF STEP]
by (auto intro: card_image)
[PROOF STATE]
proof (state)
this:
card P = card A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A
k < card A
[PROOF STEP]
have "{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A
k < card A

goal (1 subgoal):
 1. {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}
[PROOF STEP]
using Collect_empty_eq leD
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partition_on A ?P2; \<forall>X\<in>?P2. card X = 1\<rbrakk> \<Longrightarrow> card ?P2 = card A
k < card A
(Collect ?P = {}) = (\<forall>x. \<not> ?P x)
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0
[PROOF STEP]
by (simp only: card.empty)
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_spmf_sampl_uni_units [simp]: "set_spmf (sample_uniform_units q) = {..< q} - {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (sample_uniform_units q) = {..<q} - {0}
[PROOF STEP]
by(simp add: sample_uniform_units_def)


[STATEMENT]
lemma lossless_sample_uniform_units:
  assumes "q > 1"
  shows "lossless_spmf (sample_uniform_units q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sample_uniform_units q)
[PROOF STEP]
apply(simp add: sample_uniform_units_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> {..<q} \<subseteq> {0}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. \<not> {..<q} \<subseteq> {0}
[PROOF STEP]
by auto


[STATEMENT]
lemma one_time_pad_units:
  assumes inj_on: "inj_on f ({..<q} - {0})"
    and sur: "f ` ({..<q} - {0}) = ({..<q} - {0})"
  shows "map_spmf f (sample_uniform_units q) = (sample_uniform_units q)"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
have rhs: "?rhs = spmf_of_set (({..<q} - {0}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform_units q = spmf_of_set ({..<q} - {0})
[PROOF STEP]
by(auto simp add: sample_uniform_units_def)
[PROOF STATE]
proof (state)
this:
sample_uniform_units q = spmf_of_set ({..<q} - {0})

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform_units q = spmf_of_set ({..<q} - {0})

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
have "map_spmf(\<lambda>s. f s) (spmf_of_set ({..<q} - {0})) = spmf_of_set ((\<lambda>s. f s) ` ({..<q} - {0}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf f (spmf_of_set ({..<q} - {0})) = spmf_of_set (f ` ({..<q} - {0}))
[PROOF STEP]
by(simp add: inj_on)
[PROOF STATE]
proof (state)
this:
map_spmf f (spmf_of_set ({..<q} - {0})) = spmf_of_set (f ` ({..<q} - {0}))

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf f (spmf_of_set ({..<q} - {0})) = spmf_of_set (f ` ({..<q} - {0}))

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
have "f ` ({..<q} - {0}) = ({..<q} - {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` ({..<q} - {0}) = {..<q} - {0}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite ({..<q} - {0})
 2. f ` ({..<q} - {0}) \<subseteq> {..<q} - {0}
 3. inj_on f ({..<q} - {0})
[PROOF STEP]
by(simp, simp add: sur, simp add: inj_on)
[PROOF STATE]
proof (state)
this:
f ` ({..<q} - {0}) = {..<q} - {0}

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_spmf f (sample_uniform_units q) = spmf_of_set (f ` ({..<q} - {0}))
f ` ({..<q} - {0}) = {..<q} - {0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf f (sample_uniform_units q) = spmf_of_set (f ` ({..<q} - {0}))
f ` ({..<q} - {0}) = {..<q} - {0}

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
using rhs
[PROOF STATE]
proof (prove)
using this:
map_spmf f (sample_uniform_units q) = spmf_of_set (f ` ({..<q} - {0}))
f ` ({..<q} - {0}) = {..<q} - {0}
sample_uniform_units q = spmf_of_set ({..<q} - {0})

goal (1 subgoal):
 1. map_spmf f (sample_uniform_units q) = sample_uniform_units q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_spmf f (sample_uniform_units q) = sample_uniform_units q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_time_pad:
  assumes inj_on: "inj_on f {..<q}"
    and sur: "f ` {..<q} = {..<q}"
  shows "map_spmf f (sample_uniform q) = (sample_uniform q)"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
have rhs: "?rhs = spmf_of_set ({..< q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q = spmf_of_set {..<q}
[PROOF STEP]
by(auto simp add: sample_uniform_def)
[PROOF STATE]
proof (state)
this:
sample_uniform q = spmf_of_set {..<q}

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q = spmf_of_set {..<q}

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
have "map_spmf(\<lambda>s. f s) (spmf_of_set {..<q}) = spmf_of_set ((\<lambda>s. f s) ` {..<q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf f (spmf_of_set {..<q}) = spmf_of_set (f ` {..<q})
[PROOF STEP]
by(simp add: inj_on)
[PROOF STATE]
proof (state)
this:
map_spmf f (spmf_of_set {..<q}) = spmf_of_set (f ` {..<q})

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf f (spmf_of_set {..<q}) = spmf_of_set (f ` {..<q})

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
have "f ` {..<q} = {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {..<q} = {..<q}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<q}
 2. f ` {..<q} \<subseteq> {..<q}
 3. inj_on f {..<q}
[PROOF STEP]
by(simp, simp add: sur, simp add: inj_on)
[PROOF STATE]
proof (state)
this:
f ` {..<q} = {..<q}

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_spmf f (sample_uniform q) = spmf_of_set (f ` {..<q})
f ` {..<q} = {..<q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf f (sample_uniform q) = spmf_of_set (f ` {..<q})
f ` {..<q} = {..<q}

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
using rhs
[PROOF STATE]
proof (prove)
using this:
map_spmf f (sample_uniform q) = spmf_of_set (f ` {..<q})
f ` {..<q} = {..<q}
sample_uniform q = spmf_of_set {..<q}

goal (1 subgoal):
 1. map_spmf f (sample_uniform q) = sample_uniform q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_spmf f (sample_uniform q) = sample_uniform q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_add:
  assumes x:  "x < q"
    and x': "x' < q"
    and map: "((y :: nat) + x) mod q = (y + x') mod q"
  shows "x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = x'
[PROOF STEP]
have aa: "((y :: nat) + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
have 4: "((y:: nat) + x) mod q = (y + x') mod q \<Longrightarrow> [((y:: nat) + x) = (y + x')] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> [y + x = y + x'] (mod q)
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
(y + x) mod q = (y + x') mod q \<Longrightarrow> [y + x = y + x'] (mod q)

goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
have 5: "[((y:: nat) + x) = (y + x')] (mod q) \<Longrightarrow> [x = x'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y + x = y + x'] (mod q) \<Longrightarrow> [x = x'] (mod q)
[PROOF STEP]
by (simp add: cong_add_lcancel_nat)
[PROOF STATE]
proof (state)
this:
[y + x = y + x'] (mod q) \<Longrightarrow> [x = x'] (mod q)

goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
have 6: "[x = x'] (mod q) \<Longrightarrow> x mod q = x' mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = x'] (mod q) \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[x = x'] (mod q) \<Longrightarrow> x mod q = x' mod q

goal (1 subgoal):
 1. (y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x = x'] (mod q) \<Longrightarrow> x mod q = x' mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[x = x'] (mod q) \<Longrightarrow> x mod q = x' mod q

goal (1 subgoal):
 1. x mod q = x' mod q
[PROOF STEP]
by(simp add: map 4 5 6)
[PROOF STATE]
proof (state)
this:
x mod q = x' mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
have bb: "x mod q = x' mod q \<Longrightarrow> x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod q = x' mod q \<Longrightarrow> x = x'
[PROOF STEP]
by(simp add: x x')
[PROOF STATE]
proof (state)
this:
x mod q = x' mod q \<Longrightarrow> x = x'

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
x mod q = x' mod q \<Longrightarrow> x = x'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y + x) mod q = (y + x') mod q \<Longrightarrow> x mod q = x' mod q
x mod q = x' mod q \<Longrightarrow> x = x'

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
by(simp add: map)
[PROOF STATE]
proof (state)
this:
x = x'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_uni_samp_add: "inj_on (\<lambda>(b :: nat). (y + b) mod q ) {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. (y + b) mod q) {..<q}
[PROOF STEP]
by(simp add: inj_on_def)(auto simp only: inj_add)


[STATEMENT]
lemma surj_uni_samp:
  assumes inj: "inj_on  (\<lambda>(b :: nat). (y + b) mod q ) {..<q}"
  shows "(\<lambda>(b :: nat). (y + b) mod q) ` {..< q} =  {..< q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. (y + b) mod q) ` {..<q} = {..<q}
[PROOF STEP]
apply(rule endo_inj_surj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + b) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + b) mod q) {..<q}
[PROOF STEP]
using inj
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>b. (y + b) mod q) {..<q}

goal (3 subgoals):
 1. finite {..<q}
 2. (\<lambda>b. (y + b) mod q) ` {..<q} \<subseteq> {..<q}
 3. inj_on (\<lambda>b. (y + b) mod q) {..<q}
[PROOF STEP]
by auto


[STATEMENT]
lemma samp_uni_plus_one_time_pad:
  shows "map_spmf (\<lambda>b. (y + b) mod q) (sample_uniform q) = (sample_uniform q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + b) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
using inj_uni_samp_add surj_uni_samp one_time_pad
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>b. (?y + b) mod ?q) {..<?q}
inj_on (\<lambda>b. (?y + b) mod ?q) {..<?q} \<Longrightarrow> (\<lambda>b. (?y + b) mod ?q) ` {..<?q} = {..<?q}
\<lbrakk>inj_on ?f {..<?q}; ?f ` {..<?q} = {..<?q}\<rbrakk> \<Longrightarrow> map_spmf ?f (sample_uniform ?q) = sample_uniform ?q

goal (1 subgoal):
 1. map_spmf (\<lambda>b. (y + b) mod q) (sample_uniform q) = sample_uniform q
[PROOF STEP]
by simp


[STATEMENT]
lemma inj_mult:
  assumes coprime: "coprime x (q::nat)"
    and y: "y < q"
    and y': "y' < q"
  and map: "x * y mod q = x * y' mod q"
shows "y = y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = y'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = y'
[PROOF STEP]
have "x*y mod q = x*y' mod q \<Longrightarrow> y mod q = y' mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
have "x*y mod q = x*y' mod q \<Longrightarrow> [x*y = x*y'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> [x * y = x * y'] (mod q)
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
x * y mod q = x * y' mod q \<Longrightarrow> [x * y = x * y'] (mod q)

goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y mod q = x * y' mod q \<Longrightarrow> [x * y = x * y'] (mod q)

goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
have "[x*y = x*y'] (mod q) = [y = y'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x * y = x * y'] (mod q) = [y = y'] (mod q)
[PROOF STEP]
by(simp add: cong_mult_lcancel_nat coprime)
[PROOF STATE]
proof (state)
this:
[x * y = x * y'] (mod q) = [y = y'] (mod q)

goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[x * y = x * y'] (mod q) = [y = y'] (mod q)

goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
have "[y = y'] (mod q) \<Longrightarrow> y mod q = y' mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [y = y'] (mod q) \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[y = y'] (mod q) \<Longrightarrow> y mod q = y' mod q

goal (1 subgoal):
 1. x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x * y mod q = x * y' mod q \<Longrightarrow> [y = y'] (mod q)
[y = y'] (mod q) \<Longrightarrow> y mod q = y' mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * y mod q = x * y' mod q \<Longrightarrow> [y = y'] (mod q)
[y = y'] (mod q) \<Longrightarrow> y mod q = y' mod q

goal (1 subgoal):
 1. y mod q = y' mod q
[PROOF STEP]
by(simp add: map)
[PROOF STATE]
proof (state)
this:
y mod q = y' mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
have "y mod q = y' mod q \<Longrightarrow> y = y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y mod q = y' mod q \<Longrightarrow> y = y'
[PROOF STEP]
by(simp add: y y')
[PROOF STATE]
proof (state)
this:
y mod q = y' mod q \<Longrightarrow> y = y'

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
y mod q = y' mod q \<Longrightarrow> y = y'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * y mod q = x * y' mod q \<Longrightarrow> y mod q = y' mod q
y mod q = y' mod q \<Longrightarrow> y = y'

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
by(simp add: map)
[PROOF STATE]
proof (state)
this:
y = y'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_mult:
  assumes coprime: "coprime x (q::nat)"
  shows "inj_on (\<lambda> b. x*b mod q) {..<q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>b. x * b mod q) {..<q}
[PROOF STEP]
apply(auto simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa < q; y < q; x * xa mod q = x * y mod q\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
using coprime
[PROOF STATE]
proof (prove)
using this:
coprime x q

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa < q; y < q; x * xa mod q = x * y mod q\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
by(simp only: inj_mult)