[STATEMENT]
lemma option_rel_constraint[simp]:
  "(x,x)\<in>\<langle>UNIV\<times>C\<rangle>option_rel \<longleftrightarrow> (\<forall>v. x=Some v \<longrightarrow> v\<in>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, x) \<in> \<langle>UNIV \<times> C\<rangle>option_rel) = (\<forall>v. x = Some v \<longrightarrow> v \<in> C)
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma sum_rel_sv[relator_props]:
  "\<lbrakk>single_valued Rl; single_valued Rr\<rbrakk> \<Longrightarrow> single_valued (\<langle>Rl,Rr\<rangle>sum_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued Rl; single_valued Rr\<rbrakk> \<Longrightarrow> single_valued (\<langle>Rl, Rr\<rangle>sum_rel)
[PROOF STEP]
by (auto intro: single_valuedI dest: single_valuedD simp: sum_rel_def)


[STATEMENT]
lemma sum_rel_id[relator_props]: "\<lbrakk>Rl=Id; Rr=Id\<rbrakk> \<Longrightarrow> \<langle>Rl,Rr\<rangle>sum_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rl = Id; Rr = Id\<rbrakk> \<Longrightarrow> \<langle>Rl, Rr\<rangle>sum_rel = Id
[PROOF STEP]
apply (auto elim: sum_relE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>Rl = Id; Rr = Id\<rbrakk> \<Longrightarrow> (b, b) \<in> \<langle>Id, Id\<rangle>sum_rel
[PROOF STEP]
apply (case_tac b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b a. \<lbrakk>Rl = Id; Rr = Id; b = Inl a\<rbrakk> \<Longrightarrow> (b, b) \<in> \<langle>Id, Id\<rangle>sum_rel
 2. \<And>b ba. \<lbrakk>Rl = Id; Rr = Id; b = Inr ba\<rbrakk> \<Longrightarrow> (b, b) \<in> \<langle>Id, Id\<rangle>sum_rel
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_rel_id_simp[simp]: "\<langle>Id,Id\<rangle>sum_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id, Id\<rangle>sum_rel = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma sum_rel_mono[relator_props]:
  "\<lbrakk> Rl\<subseteq>Rl'; Rr\<subseteq>Rr' \<rbrakk> \<Longrightarrow> \<langle>Rl,Rr\<rangle>sum_rel \<subseteq> \<langle>Rl',Rr'\<rangle>sum_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rl \<subseteq> Rl'; Rr \<subseteq> Rr'\<rbrakk> \<Longrightarrow> \<langle>Rl, Rr\<rangle>sum_rel \<subseteq> \<langle>Rl', Rr'\<rangle>sum_rel
[PROOF STEP]
by (auto simp: sum_rel_def)


[STATEMENT]
lemma sum_rel_range[relator_props]:
  "\<lbrakk> Range Rl=UNIV; Range Rr=UNIV \<rbrakk> \<Longrightarrow> Range (\<langle>Rl,Rr\<rangle>sum_rel) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Range Rl = UNIV; Range Rr = UNIV\<rbrakk> \<Longrightarrow> Range (\<langle>Rl, Rr\<rangle>sum_rel) = UNIV
[PROOF STEP]
apply (auto simp: sum_rel_def Range_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Range Rl = UNIV; Range Rr = UNIV\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a. y = Inl a \<and> (\<exists>a'. x = Inl a' \<and> (a, a') \<in> Rl)) \<or> (\<exists>a. y = Inr a \<and> (\<exists>a'. x = Inr a' \<and> (a, a') \<in> Rr))
[PROOF STEP]
by (metis Range_iff UNIV_I sumE)


[STATEMENT]
lemma list_rel_sv_iff:
  "single_valued (\<langle>R\<rangle>list_rel) \<longleftrightarrow> single_valued R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (\<langle>R\<rangle>list_rel) = single_valued R
[PROOF STEP]
apply (intro iffI[rotated] single_valuedI allI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; (x, y) \<in> \<langle>R\<rangle>list_rel; (x, z) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
apply (clarsimp simp: list_rel_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; list_all2 (\<lambda>x x'. (x, x') \<in> R) x y; list_all2 (\<lambda>x x'. (x, x') \<in> R) x z\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; list_all2 (\<lambda>x x'. (x, x') \<in> R) x y; list_all2 (\<lambda>x x'. (x, x') \<in> R) x z\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; list_all2 (\<lambda>x x'. (x, x') \<in> R) x y; list_all2 (\<lambda>x x'. (x, x') \<in> R) x z\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
assume SV: "single_valued R"
[PROOF STATE]
proof (state)
this:
single_valued R

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; list_all2 (\<lambda>x x'. (x, x') \<in> R) x y; list_all2 (\<lambda>x x'. (x, x') \<in> R) x z\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
assume "list_all2 (\<lambda>x x'. (x, x') \<in> R) x y" and
    "list_all2 (\<lambda>x x'. (x, x') \<in> R) x z"
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>x x'. (x, x') \<in> R) x y
list_all2 (\<lambda>x x'. (x, x') \<in> R) x z

goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>single_valued R; list_all2 (\<lambda>x x'. (x, x') \<in> R) x y; list_all2 (\<lambda>x x'. (x, x') \<in> R) x z\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
thus "y=z"
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x x'. (x, x') \<in> R) x y
list_all2 (\<lambda>x x'. (x, x') \<in> R) x z

goal (1 subgoal):
 1. y = z
[PROOF STEP]
apply (induct arbitrary: z rule: list_all2_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) [] z \<Longrightarrow> [] = z
 2. \<And>x x' ls ls' z. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) ls ls'; \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) ls z \<Longrightarrow> ls' = z; list_all2 (\<lambda>x x'. (x, x') \<in> R) (x # ls) z\<rbrakk> \<Longrightarrow> x' # ls' = z
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x' ls ls' z. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) ls ls'; \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) ls z \<Longrightarrow> ls' = z; list_all2 (\<lambda>x x'. (x, x') \<in> R) (x # ls) z\<rbrakk> \<Longrightarrow> x' # ls' = z
[PROOF STEP]
apply (case_tac z)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x' ls ls' z. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) ls ls'; \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) ls z \<Longrightarrow> ls' = z; list_all2 (\<lambda>x x'. (x, x') \<in> R) (x # ls) z; z = []\<rbrakk> \<Longrightarrow> x' # ls' = z
 2. \<And>x x' ls ls' z a list. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) ls ls'; \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) ls z \<Longrightarrow> ls' = z; list_all2 (\<lambda>x x'. (x, x') \<in> R) (x # ls) z; z = a # list\<rbrakk> \<Longrightarrow> x' # ls' = z
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x' ls ls' z a list. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) ls ls'; \<And>z. list_all2 (\<lambda>x x'. (x, x') \<in> R) ls z \<Longrightarrow> ls' = z; list_all2 (\<lambda>x x'. (x, x') \<in> R) (x # ls) z; z = a # list\<rbrakk> \<Longrightarrow> x' # ls' = z
[PROOF STEP]
apply (force intro: single_valuedD[OF SV])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
y = z

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
assume SV: "single_valued (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (state)
this:
single_valued (\<langle>R\<rangle>list_rel)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
assume "(x,y)\<in>R" "(x,z)\<in>R"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R
(x, z) \<in> R

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
hence "([x],[y])\<in>\<langle>R\<rangle>list_rel" and "([x],[z])\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> R
(x, z) \<in> R

goal (1 subgoal):
 1. ([x], [y]) \<in> \<langle>R\<rangle>list_rel &&& ([x], [z]) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
by (auto simp: list_rel_def)
[PROOF STATE]
proof (state)
this:
([x], [y]) \<in> \<langle>R\<rangle>list_rel
([x], [z]) \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>single_valued (\<langle>R\<rangle>list_rel); (x, y) \<in> R; (x, z) \<in> R\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
with single_valuedD[OF SV]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?x, ?y) \<in> \<langle>R\<rangle>list_rel; (?x, ?z) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> ?y = ?z
([x], [y]) \<in> \<langle>R\<rangle>list_rel
([x], [z]) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
show "y=z"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x, ?y) \<in> \<langle>R\<rangle>list_rel; (?x, ?z) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> ?y = ?z
([x], [y]) \<in> \<langle>R\<rangle>list_rel
([x], [z]) \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. y = z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y = z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_rel_sv[relator_props]:
  "single_valued R \<Longrightarrow> single_valued (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> single_valued (\<langle>R\<rangle>list_rel)
[PROOF STEP]
by (simp add: list_rel_sv_iff)


[STATEMENT]
lemma list_rel_id[relator_props]: "\<lbrakk>R=Id\<rbrakk> \<Longrightarrow> \<langle>R\<rangle>list_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = Id \<Longrightarrow> \<langle>R\<rangle>list_rel = Id
[PROOF STEP]
by (auto simp add: list_rel_def list_all2_eq[symmetric])


[STATEMENT]
lemma list_rel_id_simp[simp]: "\<langle>Id\<rangle>list_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id\<rangle>list_rel = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma list_rel_mono[relator_props]:
  assumes A: "R\<subseteq>R'"
  shows "\<langle>R\<rangle>list_rel \<subseteq> \<langle>R'\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>list_rel \<subseteq> \<langle>R'\<rangle>list_rel
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> (a, b) \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
fix l l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> (a, b) \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
assume "(l,l')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (state)
this:
(l, l') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> (a, b) \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
thus "(l,l')\<in>\<langle>R'\<rangle>list_rel"
[PROOF STATE]
proof (prove)
using this:
(l, l') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. (l, l') \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ([], []) \<in> \<langle>R'\<rangle>list_rel
 2. \<And>x x' l l'. \<lbrakk>(x, x') \<in> R; (l, l') \<in> \<langle>R\<rangle>list_rel; (l, l') \<in> \<langle>R'\<rangle>list_rel\<rbrakk> \<Longrightarrow> (x # l, x' # l') \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> R'

goal (2 subgoals):
 1. ([], []) \<in> \<langle>R'\<rangle>list_rel
 2. \<And>x x' l l'. \<lbrakk>(x, x') \<in> R; (l, l') \<in> \<langle>R\<rangle>list_rel; (l, l') \<in> \<langle>R'\<rangle>list_rel\<rbrakk> \<Longrightarrow> (x # l, x' # l') \<in> \<langle>R'\<rangle>list_rel
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, l') \<in> \<langle>R'\<rangle>list_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_rel_range[relator_props]:
  assumes A: "Range R = UNIV"
  shows "Range (\<langle>R\<rangle>list_rel) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (\<langle>R\<rangle>list_rel) = UNIV
[PROOF STEP]
proof (clarsimp simp: eq_UNIV_iff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Range (\<langle>R\<rangle>list_rel)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Range (\<langle>R\<rangle>list_rel)
[PROOF STEP]
show "l\<in>Range (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> Range (\<langle>R\<rangle>list_rel)
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [] \<in> Range (\<langle>R\<rangle>list_rel)
 2. \<And>a l. l \<in> Range (\<langle>R\<rangle>list_rel) \<Longrightarrow> a # l \<in> Range (\<langle>R\<rangle>list_rel)
[PROOF STEP]
using A[unfolded eq_UNIV_iff]
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> Range R

goal (2 subgoals):
 1. [] \<in> Range (\<langle>R\<rangle>list_rel)
 2. \<And>a l. l \<in> Range (\<langle>R\<rangle>list_rel) \<Longrightarrow> a # l \<in> Range (\<langle>R\<rangle>list_rel)
[PROOF STEP]
by (auto simp: Range_iff intro: list_relI)
[PROOF STATE]
proof (state)
this:
l \<in> Range (\<langle>R\<rangle>list_rel)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bijective_imp_sv:
  "bijective R \<Longrightarrow> single_valued R"
  "bijective R \<Longrightarrow> single_valued (R\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bijective R \<Longrightarrow> single_valued R) &&& (bijective R \<Longrightarrow> single_valued (R\<inverse>))
[PROOF STEP]
by (simp_all add: bijective_alt)


[STATEMENT]
lemma set_rel_sv[relator_props]:
  "single_valued R \<Longrightarrow> single_valued (\<langle>R\<rangle>set_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> single_valued (\<langle>R\<rangle>set_rel)
[PROOF STEP]
unfolding single_valued_def set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> R \<longrightarrow> (\<forall>z. (x, z) \<in> R \<longrightarrow> y = z) \<Longrightarrow> \<forall>x y. (x, y) \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)} \<longrightarrow> (\<forall>z. (x, z) \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)} \<longrightarrow> y = z)
[PROOF STEP]
by blast


[STATEMENT]
lemma set_rel_id[relator_props]: "R=Id \<Longrightarrow> \<langle>R\<rangle>set_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = Id \<Longrightarrow> \<langle>R\<rangle>set_rel = Id
[PROOF STEP]
by (auto simp add: set_rel_def)


[STATEMENT]
lemma set_rel_id_simp[simp]: "\<langle>Id\<rangle>set_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id\<rangle>set_rel = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma set_rel_csv[relator_props]:
  "\<lbrakk> single_valued (R\<inverse>) \<rbrakk>
  \<Longrightarrow> single_valued ((\<langle>R\<rangle>set_rel)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (R\<inverse>) \<Longrightarrow> single_valued ((\<langle>R\<rangle>set_rel)\<inverse>)
[PROOF STEP]
unfolding single_valued_def set_rel_def converse_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (y, x) \<in> R \<longrightarrow> (\<forall>z. (z, x) \<in> R \<longrightarrow> y = z) \<Longrightarrow> \<forall>x y. (y, x) \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)} \<longrightarrow> (\<forall>z. (z, x) \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)} \<longrightarrow> y = z)
[PROOF STEP]
by fast


[STATEMENT]
lemma in_br_conv: "(c,a)\<in>br \<alpha> I \<longleftrightarrow> a=\<alpha> c \<and> I c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((c, a) \<in> br \<alpha> I) = (a = \<alpha> c \<and> I c)
[PROOF STEP]
by (auto simp: br_def)


[STATEMENT]
lemma brI[intro?]: "\<lbrakk> a=\<alpha> c; I c \<rbrakk> \<Longrightarrow> (c,a)\<in>br \<alpha> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = \<alpha> c; I c\<rbrakk> \<Longrightarrow> (c, a) \<in> br \<alpha> I
[PROOF STEP]
by (simp add: br_def)


[STATEMENT]
lemma br_id[simp]: "br id (\<lambda>_. True) = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. br id (\<lambda>_. True) = Id
[PROOF STEP]
unfolding build_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c, a). a = id c \<and> True} = Id
[PROOF STEP]
by auto


[STATEMENT]
lemma br_chain:
  "(build_rel \<beta> J) O (build_rel \<alpha> I) = build_rel (\<alpha>\<circ>\<beta>) (\<lambda>s. J s \<and> I (\<beta> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. br \<beta> J O br \<alpha> I = br (\<alpha> \<circ> \<beta>) (\<lambda>s. J s \<and> I (\<beta> s))
[PROOF STEP]
unfolding build_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c, a). a = \<beta> c \<and> J c} O {(c, a). a = \<alpha> c \<and> I c} = {(c, a). a = (\<alpha> \<circ> \<beta>) c \<and> J c \<and> I (\<beta> c)}
[PROOF STEP]
by auto


[STATEMENT]
lemma br_sv[simp, intro!,relator_props]: "single_valued (br \<alpha> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (br \<alpha> I)
[PROOF STEP]
unfolding build_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued {(c, a). a = \<alpha> c \<and> I c}
[PROOF STEP]
apply (rule single_valuedI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> {(c, a). a = \<alpha> c \<and> I c}; (x, z) \<in> {(c, a). a = \<alpha> c \<and> I c}\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma converse_br_sv_iff[simp]:
  "single_valued (converse (br \<alpha> I)) \<longleftrightarrow> inj_on \<alpha> (Collect I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued ((br \<alpha> I)\<inverse>) = inj_on \<alpha> (Collect I)
[PROOF STEP]
by (auto intro!: inj_onI single_valuedI dest: single_valuedD inj_onD
    simp: br_def) []


[STATEMENT]
lemma br_comp_alt: "br \<alpha> I O R = { (c,a) . I c \<and> (\<alpha> c,a)\<in>R }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. br \<alpha> I O R = {(c, a). I c \<and> (\<alpha> c, a) \<in> R}
[PROOF STEP]
by (auto simp add: br_def)


[STATEMENT]
lemma br_comp_alt':
  "{(c,a) . a=\<alpha> c \<and> I c} O R = { (c,a) . I c \<and> (\<alpha> c,a)\<in>R }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c, a). a = \<alpha> c \<and> I c} O R = {(c, a). I c \<and> (\<alpha> c, a) \<in> R}
[PROOF STEP]
by auto


[STATEMENT]
lemma single_valued_as_brE:
  assumes "single_valued R"
  obtains \<alpha> invar where "R=br \<alpha> invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha> invar. R = br \<alpha> invar \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule that[of "\<lambda>x. THE y. (x,y)\<in>R" "\<lambda>x. x\<in>Domain R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha> invar. R = br \<alpha> invar \<Longrightarrow> thesis) \<Longrightarrow> R = br (\<lambda>x. THE y. (x, y) \<in> R) (\<lambda>x. x \<in> Domain R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
single_valued R

goal (1 subgoal):
 1. (\<And>\<alpha> invar. R = br \<alpha> invar \<Longrightarrow> thesis) \<Longrightarrow> R = br (\<lambda>x. THE y. (x, y) \<in> R) (\<lambda>x. x \<in> Domain R)
[PROOF STEP]
unfolding br_def
[PROOF STATE]
proof (prove)
using this:
single_valued R

goal (1 subgoal):
 1. (\<And>\<alpha> invar. R = {(c, a). a = \<alpha> c \<and> invar c} \<Longrightarrow> thesis) \<Longrightarrow> R = {(c, a). a = (THE y. (c, y) \<in> R) \<and> c \<in> Domain R}
[PROOF STEP]
by (auto dest: single_valuedD
    intro: the_equality[symmetric] theI)


[STATEMENT]
lemma sv_add_invar:
  "single_valued R \<Longrightarrow> single_valued {(c, a). (c, a) \<in> R \<and> I c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> single_valued {(c, a). (c, a) \<in> R \<and> I c}
[PROOF STEP]
by (auto dest: single_valuedD intro: single_valuedI)


[STATEMENT]
lemma br_Image_conv[simp]: "br \<alpha> I `` S = {\<alpha> x | x. x\<in>S \<and> I x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. br \<alpha> I `` S = {\<alpha> x |x. x \<in> S \<and> I x}
[PROOF STEP]
by (auto simp: br_def)


[STATEMENT]
lemma rel_cong: "(f,g)\<in>Id \<Longrightarrow> (x,y)\<in>Id \<Longrightarrow> (f x, g y)\<in>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> Id; (x, y) \<in> Id\<rbrakk> \<Longrightarrow> (f x, g y) \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_fun_cong: "(f,g)\<in>Id \<Longrightarrow> (f x, g x)\<in>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> Id \<Longrightarrow> (f x, g x) \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_arg_cong: "(x,y)\<in>Id \<Longrightarrow> (f x, f y)\<in>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> Id \<Longrightarrow> (f x, f y) \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma rel2pD: "\<lbrakk>rel2p R a b\<rbrakk> \<Longrightarrow> (a,b)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p R a b \<Longrightarrow> (a, b) \<in> R
[PROOF STEP]
by (auto simp: rel2p_def)


[STATEMENT]
lemma p2relD: "\<lbrakk>(a,b) \<in> p2rel R\<rbrakk> \<Longrightarrow> R a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> p2rel R \<Longrightarrow> R a b
[PROOF STEP]
by (auto simp: p2rel_def)


[STATEMENT]
lemma rel2p_inv[simp]:
  "rel2p (p2rel P) = P"
  "p2rel (rel2p R) = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p (p2rel P) = P &&& p2rel (rel2p R) = R
[PROOF STEP]
by (auto simp: rel2p_def[abs_def] p2rel_def)


[STATEMENT]
lemma rel2p_dflt[rel2p]:
  "rel2p Id = (=)"
  "rel2p (A\<rightarrow>B) = rel_fun (rel2p A) (rel2p B)"
  "rel2p (A\<times>\<^sub>rB) = rel_prod (rel2p A) (rel2p B)"
  "rel2p (\<langle>A,B\<rangle>sum_rel) = rel_sum (rel2p A) (rel2p B)"
  "rel2p (\<langle>A\<rangle>option_rel) = rel_option (rel2p A)"
  "rel2p (\<langle>A\<rangle>list_rel) = list_all2 (rel2p A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel2p Id = (=) &&& rel2p (A \<rightarrow> B) = rel_fun (rel2p A) (rel2p B) &&& rel2p (A \<times>\<^sub>r B) = rel_prod (rel2p A) (rel2p B)) &&& rel2p (\<langle>A, B\<rangle>sum_rel) = rel_sum (rel2p A) (rel2p B) &&& rel2p (\<langle>A\<rangle>option_rel) = rel_option (rel2p A) &&& rel2p (\<langle>A\<rangle>list_rel) = list_all2 (rel2p A)
[PROOF STEP]
by (auto
    simp: rel2p_def[abs_def]
    intro!: ext
    simp: fun_rel_def rel_fun_def
    simp: sum_rel_def elim: rel_sum.cases
    simp: option_rel_def elim: option.rel_cases
    simp: list_rel_def
    simp: set_rel_def rel_set_def Image_def
    )


[STATEMENT]
lemma p2rel_dflt[p2rel]:
  "p2rel (=) = Id"
  "p2rel (rel_fun A B) = p2rel A \<rightarrow> p2rel B"
  "p2rel (rel_prod A B) = p2rel A \<times>\<^sub>r p2rel B"
  "p2rel (rel_sum A B) = \<langle>p2rel A, p2rel B\<rangle>sum_rel"
  "p2rel (rel_option A) = \<langle>p2rel A\<rangle>option_rel"
  "p2rel (list_all2 A) = \<langle>p2rel A\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p2rel (=) = Id &&& p2rel (rel_fun A B) = p2rel A \<rightarrow> p2rel B &&& p2rel (rel_prod A B) = p2rel A \<times>\<^sub>r p2rel B) &&& p2rel (rel_sum A B) = \<langle>p2rel A, p2rel B\<rangle>sum_rel &&& p2rel (rel_option A) = \<langle>p2rel A\<rangle>option_rel &&& p2rel (list_all2 A) = \<langle>p2rel A\<rangle>list_rel
[PROOF STEP]
by (auto
    simp: p2rel_def[abs_def]
    simp: fun_rel_def rel_fun_def
    simp: sum_rel_def elim: rel_sum.cases
    simp: option_rel_def elim: option.rel_cases
    simp: list_rel_def
    )


[STATEMENT]
lemma [rel2p]: "rel2p (\<langle>A\<rangle>set_rel) = rel_set (rel2p A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p (\<langle>A\<rangle>set_rel) = rel_set (rel2p A)
[PROOF STEP]
unfolding set_rel_def rel_set_def rel2p_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x, y) \<in> {(Aa, B). (\<forall>x\<in>Aa. \<exists>y\<in>B. (x, y) \<in> A) \<and> (\<forall>y\<in>B. \<exists>x\<in>Aa. (x, y) \<in> A)}) = (\<lambda>Aa B. (\<forall>x\<in>Aa. \<exists>y\<in>B. (x, y) \<in> A) \<and> (\<forall>y\<in>B. \<exists>x\<in>Aa. (x, y) \<in> A))
[PROOF STEP]
by blast


[STATEMENT]
lemma [p2rel]: "left_unique A \<Longrightarrow> p2rel (rel_set A) = (\<langle>p2rel A\<rangle>set_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique A \<Longrightarrow> p2rel (rel_set A) = \<langle>p2rel A\<rangle>set_rel
[PROOF STEP]
unfolding set_rel_def rel_set_def p2rel_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique A \<Longrightarrow> {(Aa, B). (\<forall>x\<in>Aa. Bex B (A x)) \<and> (\<forall>y\<in>B. \<exists>x\<in>Aa. A x y)} = {(Aa, B). (\<forall>x\<in>Aa. \<exists>y\<in>B. (x, y) \<in> {(x, y). A x y}) \<and> (\<forall>y\<in>B. \<exists>x\<in>Aa. (x, y) \<in> {(x, y). A x y})}
[PROOF STEP]
by blast


[STATEMENT]
lemma rel2p_comp: "rel2p A OO rel2p B = rel2p (A O B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p A OO rel2p B = rel2p (A O B)
[PROOF STEP]
by (auto simp: rel2p_def[abs_def] intro!: ext)


[STATEMENT]
lemma rel2p_inj[simp]: "rel2p A = rel2p B \<longleftrightarrow> A=B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel2p A = rel2p B) = (A = B)
[PROOF STEP]
by (auto simp: rel2p_def[abs_def]; meson)


[STATEMENT]
lemma list_rel_compp: "\<langle>A O B\<rangle>list_rel = \<langle>A\<rangle>list_rel O \<langle>B\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A O B\<rangle>list_rel = \<langle>A\<rangle>list_rel O \<langle>B\<rangle>list_rel
[PROOF STEP]
using list.rel_compp[of "rel2p A" "rel2p B"]
[PROOF STATE]
proof (prove)
using this:
list_all2 (rel2p A OO rel2p B) = list_all2 (rel2p A) OO list_all2 (rel2p B)

goal (1 subgoal):
 1. \<langle>A O B\<rangle>list_rel = \<langle>A\<rangle>list_rel O \<langle>B\<rangle>list_rel
[PROOF STEP]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp)


[STATEMENT]
lemma option_rel_compp: "\<langle>A O B\<rangle>option_rel = \<langle>A\<rangle>option_rel O \<langle>B\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A O B\<rangle>option_rel = \<langle>A\<rangle>option_rel O \<langle>B\<rangle>option_rel
[PROOF STEP]
using option.rel_compp[of "rel2p A" "rel2p B"]
[PROOF STATE]
proof (prove)
using this:
rel_option (rel2p A OO rel2p B) = rel_option (rel2p A) OO rel_option (rel2p B)

goal (1 subgoal):
 1. \<langle>A O B\<rangle>option_rel = \<langle>A\<rangle>option_rel O \<langle>B\<rangle>option_rel
[PROOF STEP]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp)


[STATEMENT]
lemma prod_rel_compp: "\<langle>A O B, C O D\<rangle>prod_rel = \<langle>A,C\<rangle>prod_rel O \<langle>B,D\<rangle>prod_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A O B \<times>\<^sub>r C O D = (A \<times>\<^sub>r C) O (B \<times>\<^sub>r D)
[PROOF STEP]
using prod.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"]
[PROOF STATE]
proof (prove)
using this:
rel_prod (rel2p A OO rel2p B) (rel2p C OO rel2p D) = rel_prod (rel2p A) (rel2p C) OO rel_prod (rel2p B) (rel2p D)

goal (1 subgoal):
 1. A O B \<times>\<^sub>r C O D = (A \<times>\<^sub>r C) O (B \<times>\<^sub>r D)
[PROOF STEP]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp)


[STATEMENT]
lemma sum_rel_compp: "\<langle>A O B, C O D\<rangle>sum_rel = \<langle>A,C\<rangle>sum_rel O \<langle>B,D\<rangle>sum_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A O B, C O D\<rangle>sum_rel = \<langle>A, C\<rangle>sum_rel O \<langle>B, D\<rangle>sum_rel
[PROOF STEP]
using sum.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"]
[PROOF STATE]
proof (prove)
using this:
rel_sum (rel2p A OO rel2p B) (rel2p C OO rel2p D) = rel_sum (rel2p A) (rel2p C) OO rel_sum (rel2p B) (rel2p D)

goal (1 subgoal):
 1. \<langle>A O B, C O D\<rangle>sum_rel = \<langle>A, C\<rangle>sum_rel O \<langle>B, D\<rangle>sum_rel
[PROOF STEP]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp)


[STATEMENT]
lemma set_rel_compp: "\<langle>A O B\<rangle>set_rel = \<langle>A\<rangle>set_rel O \<langle>B\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A O B\<rangle>set_rel = \<langle>A\<rangle>set_rel O \<langle>B\<rangle>set_rel
[PROOF STEP]
using rel_set_OO[of "rel2p A" "rel2p B"]
[PROOF STATE]
proof (prove)
using this:
rel_set (rel2p A) OO rel_set (rel2p B) = rel_set (rel2p A OO rel2p B)

goal (1 subgoal):
 1. \<langle>A O B\<rangle>set_rel = \<langle>A\<rangle>set_rel O \<langle>B\<rangle>set_rel
[PROOF STEP]
by (auto simp: rel2p(2-)[symmetric] rel2p_comp)


[STATEMENT]
lemma map_in_list_rel_conv:
  shows "(l, map \<alpha> l) \<in> \<langle>br \<alpha> I\<rangle>list_rel \<longleftrightarrow> (\<forall>x\<in>set l. I x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l, map \<alpha> l) \<in> \<langle>br \<alpha> I\<rangle>list_rel) = (\<forall>x\<in>set l. I x)
[PROOF STEP]
by (induction l) (auto simp: in_br_conv)


[STATEMENT]
lemma br_set_rel_alt: "(s',s)\<in>\<langle>br \<alpha> I\<rangle>set_rel \<longleftrightarrow> (s=\<alpha>`s' \<and> (\<forall>x\<in>s'. I x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((s', s) \<in> \<langle>br \<alpha> I\<rangle>set_rel) = (s = \<alpha> ` s' \<and> (\<forall>x\<in>s'. I x))
[PROOF STEP]
by (auto simp: set_rel_def br_def)


[STATEMENT]
lemma finite_Image_sv: "single_valued R \<Longrightarrow> finite s \<Longrightarrow> finite (R``s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued R; finite s\<rbrakk> \<Longrightarrow> finite (R `` s)
[PROOF STEP]
by (erule single_valued_as_brE) simp


[STATEMENT]
lemma finite_set_rel_transfer: "\<lbrakk>(s,s')\<in>\<langle>R\<rangle>set_rel; single_valued R; finite s\<rbrakk> \<Longrightarrow> finite s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> \<langle>R\<rangle>set_rel; single_valued R; finite s\<rbrakk> \<Longrightarrow> finite s'
[PROOF STEP]
unfolding set_rel_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> {(A, B). A \<subseteq> R\<inverse> `` B \<and> B \<subseteq> R `` A}; single_valued R; finite s\<rbrakk> \<Longrightarrow> finite s'
[PROOF STEP]
by (blast intro: finite_subset[OF _ finite_Image_sv])


[STATEMENT]
lemma finite_set_rel_transfer_back: "\<lbrakk>(s,s')\<in>\<langle>R\<rangle>set_rel; single_valued (R\<inverse>); finite s'\<rbrakk> \<Longrightarrow> finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> \<langle>R\<rangle>set_rel; single_valued (R\<inverse>); finite s'\<rbrakk> \<Longrightarrow> finite s
[PROOF STEP]
unfolding set_rel_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> {(A, B). A \<subseteq> R\<inverse> `` B \<and> B \<subseteq> R `` A}; single_valued (R\<inverse>); finite s'\<rbrakk> \<Longrightarrow> finite s
[PROOF STEP]
by (blast intro: finite_subset[OF _ finite_Image_sv])


[STATEMENT]
lemma partitions_of:
  assumes "finite B"
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
  shows "card (partitions_of A B F) \<le> card B"
  and "partition_on A (partitions_of A B F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B &&& partition_on A (partitions_of A B F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
have "partitions_of A B F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F
[PROOF STEP]
unfolding partitions_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
partitions_of A B F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
partitions_of A B F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
have "\<dots> = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})
[PROOF STEP]
unfolding F_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
have "\<dots> = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}) = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
using equiv_range_permutation domain_partitions_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
(\<lambda>f. (\<lambda>b. {x \<in> ?A. f x = b}) ` ?B - {{}}) respects range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

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

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
partitions_of A B F = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
have partitions_of_eq: "partitions_of A B F = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
using this:
partitions_of A B F = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}

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

goal (2 subgoals):
 1. card (partitions_of A B F) \<le> card B
 2. partition_on A (partitions_of A B F)
[PROOF STEP]
show "card (partitions_of A B F) \<le> card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
have "card (partitions_of A B F) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (partitions_of A B F) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
unfolding partitions_of_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

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

goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
have "\<dots> \<le> card ((\<lambda>b. {x \<in> A. f x = b}) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

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

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

goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
have "\<dots> \<le> card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

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

goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (partitions_of A B F) \<le> card B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (partitions_of A B F) \<le> card B

goal (1 subgoal):
 1. card (partitions_of A B F) \<le> card B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) \<le> card B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) \<le> card B

goal (1 subgoal):
 1. partition_on A (partitions_of A B F)
[PROOF STEP]
show "partition_on A (partitions_of A B F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A (partitions_of A B F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_on A (partitions_of A B F)
[PROOF STEP]
have "partition_on A ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B

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

goal (1 subgoal):
 1. partition_on A (partitions_of A B F)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on A ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partition_on A ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

goal (1 subgoal):
 1. partition_on A (partitions_of A B F)
[PROOF STEP]
unfolding partitions_of_eq
[PROOF STATE]
proof (prove)
using this:
partition_on A ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
partition_on A (partitions_of A B F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of:
  assumes "finite A" "finite B"
  assumes "partition_on A P"
  assumes "card P \<le> card B"
  shows "functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and r1: "(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_function_with_partition[OF \<open>finite A\<close> \<open>finite B\<close> \<open>partition_on A P\<close> \<open>card P \<le> card B\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

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

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of P A B \<Longrightarrow> x \<in> range_permutation A B `` {f}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> functions_of P A B
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B" and r2: "(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = P"
[PROOF STATE]
proof (prove)
using this:
f' \<in> functions_of P A B

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B &&& (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = P
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P}

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

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

goal (1 subgoal):
 1. (\<And>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using partitions_eq_implies_permutes[OF \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>] \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = P
\<lbrakk>finite B; (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}\<rbrakk> \<Longrightarrow> \<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x))
finite B

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

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of P A B \<Longrightarrow> x \<in> range_permutation A B `` {f}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x))
[PROOF STEP]
show "f' \<in> range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x))

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
functions_of P A B \<subseteq> range_permutation A B `` {f}

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

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of P A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> range_permutation A B `` {f}
[PROOF STEP]
have "(f, f') \<in> range_permutation A B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> range_permutation A B `` {f}

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

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

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

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

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

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
[PROOF STEP]
using congruentD[OF domain_partitions_respects_range_permutation]
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> range_permutation A B
(?y, ?z) \<in> range_permutation ?A1 ?B1 \<Longrightarrow> (\<lambda>b. {x \<in> ?A1. ?y x = b}) ` ?B1 - {{}} = (\<lambda>b. {x \<in> ?A1. ?z x = b}) ` ?B1 - {{}}

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

goal (1 subgoal):
 1. \<And>x. x \<in> range_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of P A B
[PROOF STEP]
from \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close> this r1
[PROOF STATE]
proof (chain)
picking this:
f' \<in> A \<rightarrow>\<^sub>E B
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
show "f' \<in> functions_of P A B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

goal (1 subgoal):
 1. f' \<in> functions_of P A B
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range_permutation A B `` {f} \<subseteq> functions_of P A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
functions_of P A B = range_permutation A B `` {f}

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

goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
by (auto intro: quotientI)
[PROOF STATE]
proof (state)
this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of_partitions_of:
  assumes "finite B"
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
  shows "functions_of (partitions_of A B F) A B = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
have partitions_of_eq: "partitions_of A B F = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B F = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
unfolding partitions_of_def F_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}) = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
using equiv_range_permutation domain_partitions_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
(\<lambda>f. (\<lambda>b. {x \<in> ?A. f x = b}) ` ?B - {{}}) respects range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

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

goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. functions_of (partitions_of A B F) A B \<subseteq> F
 2. F \<subseteq> functions_of (partitions_of A B F) A B
[PROOF STEP]
show "functions_of (partitions_of A B F) A B \<subseteq> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of (partitions_of A B F) A B \<subseteq> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> functions_of (partitions_of A B F) A B \<Longrightarrow> x \<in> F
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> functions_of (partitions_of A B F) A B \<Longrightarrow> x \<in> F
[PROOF STEP]
assume f': "f' \<in> functions_of (partitions_of A B F) A B"
[PROOF STATE]
proof (state)
this:
f' \<in> functions_of (partitions_of A B F) A B

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of (partitions_of A B F) A B \<Longrightarrow> x \<in> F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
have "(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
using this:
f' \<in> functions_of (partitions_of A B F) A B

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = partitions_of A B F}

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

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

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

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

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = partitions_of A B F}

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

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of (partitions_of A B F) A B \<Longrightarrow> x \<in> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of (partitions_of A B F) A B \<Longrightarrow> x \<in> F
[PROOF STEP]
obtain p where "p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using partitions_eq_implies_permutes[OF \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close> \<open>finite B\<close>
          \<open>(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}}\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>p. p permutes B \<and> (\<forall>x\<in>A. f x = p (f' x))

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
functions_of (partitions_of A B F) A B \<subseteq> F

goal (1 subgoal):
 1. F \<subseteq> functions_of (partitions_of A B F) A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F \<subseteq> functions_of (partitions_of A B F) A B
[PROOF STEP]
show "F \<subseteq> functions_of (partitions_of A B F) A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<subseteq> functions_of (partitions_of A B F) A B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> x \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> x \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
assume "f' \<in> F"
[PROOF STATE]
proof (state)
this:
f' \<in> F

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> x \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
from \<open>f' \<in> F\<close>
[PROOF STATE]
proof (chain)
picking this:
f' \<in> F
[PROOF STEP]
obtain p where "p permutes B" "\<forall>x\<in>A. f x = p (f' x)"
[PROOF STATE]
proof (prove)
using this:
f' \<in> F

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> x \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
have eq: "(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
have "(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}}
[PROOF STEP]
using permutes_implies_inv_image_on_eq[OF \<open>p permutes B\<close>, of A f']
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. p (f' x) = b}) ` B = (\<lambda>b. {x \<in> A. f' x = b}) ` B

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

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

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
have "\<dots> =  (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. p (f' x) = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
using \<open>\<forall>x\<in>A. f x = p (f' x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. f x = p (f' x)

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> x \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
from this \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f' \<in> functions_of (partitions_of A B F) A B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> functions_of (partitions_of A B F) A B
[PROOF STEP]
unfolding functions_of_def partitions_of_eq
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f' x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> {fa \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. fa x = b}) ` B - {{}} = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> functions_of (partitions_of A B F) A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F \<subseteq> functions_of (partitions_of A B F) A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
functions_of (partitions_of A B F) A B = F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partitions_of_functions_of:
  assumes "finite A" "finite B"
  assumes "partition_on A P"
  assumes "card P \<le> card B"
  shows "partitions_of A B (functions_of P A B) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
have "functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close> \<open>partition_on A P\<close> \<open>card P \<le> card B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
partition_on A P
card P \<le> card B

goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
by (rule functions_of)
[PROOF STATE]
proof (state)
this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B" and functions_of_eq: "functions_of P A B = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; functions_of P A B = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
from functions_of_eq \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
functions_of P A B = range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
have "f \<in> functions_of P A B"
[PROOF STATE]
proof (prove)
using this:
functions_of P A B = range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f \<in> functions_of P A B
[PROOF STEP]
using equiv_range_permutation equiv_class_self
[PROOF STATE]
proof (prove)
using this:
functions_of P A B = range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
\<lbrakk>equiv ?A ?r; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<in> ?r `` {?a}

goal (1 subgoal):
 1. f \<in> functions_of P A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<in> functions_of P A B

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
have "partitions_of A B (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B)
[PROOF STEP]
unfolding partitions_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
partitions_of A B (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B)

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

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
have "\<dots> = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})
[PROOF STEP]
unfolding \<open>functions_of P A B = range_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (functions_of P A B) = univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})

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

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
have "\<dots> = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}) = (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}
[PROOF STEP]
using equiv_range_permutation domain_partitions_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
(\<lambda>f. (\<lambda>b. {x \<in> ?A. f x = b}) ` ?B - {{}}) respects range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

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

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

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
have "(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
using \<open>f \<in> functions_of P A B\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> functions_of P A B

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P}

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

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

goal (1 subgoal):
 1. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
partitions_of A B (functions_of P A B) = P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_partitions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (partitions_of A B) ((A \<rightarrow>\<^sub>E B) // range_permutation A B) {P. partition_on A P \<and> card P \<le> card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (partitions_of A B) ((A \<rightarrow>\<^sub>E B) // range_permutation A B) {P. partition_on A P \<and> card P \<le> card B}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="\<lambda>P. functions_of P A B"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>(A \<rightarrow>\<^sub>E B) // range_permutation A B. functions_of (partitions_of A B a) A B = a
 2. \<forall>a'\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of a' A B) = a'
 3. partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}
 4. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
show "\<forall>F\<in>(A \<rightarrow>\<^sub>E B) // range_permutation A B. functions_of (partitions_of A B F) A B = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>(A \<rightarrow>\<^sub>E B) // range_permutation A B. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. \<forall>F\<in>(A \<rightarrow>\<^sub>E B) // range_permutation A B. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
by (simp add: functions_of_partitions_of)
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>(A \<rightarrow>\<^sub>E B) // range_permutation A B. functions_of (partitions_of A B F) A B = F

goal (3 subgoals):
 1. \<forall>a'\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of a' A B) = a'
 2. partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}
 3. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
show "\<forall>P\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of P A B) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
by (auto simp add: partitions_of_functions_of)
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>{P. partition_on A P \<and> card P \<le> card B}. partitions_of A B (functions_of P A B) = P

goal (2 subgoals):
 1. partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}
 2. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
show "partitions_of A B ` ((A \<rightarrow>\<^sub>E B) // range_permutation A B) \<subseteq> {P. partition_on A P \<and> card P \<le> card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}
[PROOF STEP]
using \<open>finite B\<close> partitions_of
[PROOF STATE]
proof (prove)
using this:
finite B
\<lbrakk>finite ?B; ?F \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B\<rbrakk> \<Longrightarrow> card (partitions_of ?A ?B ?F) \<le> card ?B
\<lbrakk>finite ?B; ?F \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B\<rbrakk> \<Longrightarrow> partition_on ?A (partitions_of ?A ?B ?F)

goal (1 subgoal):
 1. partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partitions_of A B ` (A \<rightarrow>\<^sub>E B) // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P \<le> card B}

goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
show "(\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
using functions_of \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B; partition_on ?A ?P; card ?P \<le> card ?B\<rbrakk> \<Longrightarrow> functions_of ?P ?A ?B \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B
finite A
finite B

goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P \<le> card B} \<subseteq> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_ad [simp]: "r (ad p) = ad p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (ad p) = ad p
[PROOF STEP]
using a_closure addual.ars_r_def am_d_def domrangefix
[PROOF STATE]
proof (prove)
using this:
am_d (ad ?x) = ad ?x
d ?x = ad (ad ?x)
am_d ?x = ad (ad ?x)
(d ?x = ?x) = (r ?x = ?x)

goal (1 subgoal):
 1. r (ad p) = ad p
[PROOF STEP]
by auto


[STATEMENT]
lemma bdia_export2: "r p \<cdot> \<langle>x| q = \<langle>x \<cdot> r p| q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r p \<cdot> \<langle>x| q = \<langle>x \<cdot> r p| q
[PROOF STEP]
using ardual.ads_d_def ardual.am2 ardual.fdia_export_2 bdia_def
[PROOF STATE]
proof (prove)
using this:
r ?x = ar ar ?x
ar ?y \<cdot> ar ?x = ar ?x \<cdot> ar ?y
\<langle>?x| ?z \<cdot> ar ?y = \<langle>?x \<cdot> ar ?y| ?z
\<langle>?x| ?y = ar ar (?y \<cdot> ?x)

goal (1 subgoal):
 1. r p \<cdot> \<langle>x| q = \<langle>x \<cdot> r p| q
[PROOF STEP]
by auto


[STATEMENT]
lemma bdia_seq [simp]: "\<langle>x \<cdot> y| q = \<langle>y| \<langle>x| q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x \<cdot> y| q = \<langle>y| \<langle>x| q
[PROOF STEP]
by (simp add: ardual.ds.fdia_mult)


[STATEMENT]
lemma bdia_seq_var: "\<langle>x| p \<le> p' \<Longrightarrow> \<langle>y| p' \<le> q \<Longrightarrow> \<langle>x \<cdot> y| p \<le> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>x| p \<le> p'; \<langle>y| p' \<le> q\<rbrakk> \<Longrightarrow> \<langle>x \<cdot> y| p \<le> q
[PROOF STEP]
by (metis ardual.ds.fd_subdist_1 ardual.ds.fdia_mult dual_order.trans join.sup_absorb2)


[STATEMENT]
lemma bdia_cond_var [simp]: "\<langle>if p then x else y fi| q = \<langle>x| (d p \<cdot> r q) + \<langle>y| (ad p \<cdot> r q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>if p then x else y fi| q = \<langle>x| (d p \<cdot> r q) + \<langle>y| (ad p \<cdot> r q)
[PROOF STEP]
by (metis (no_types, lifting) bdia_export1 a4' a_de_morgan a_de_morgan_var_3 a_subid_aux1' ardual.ds.fdia_add2 dka.dnso1 dka.dsg4 domrange dpdz.dnso1 cond_def join.sup.absorb_iff1 rangedom)


[STATEMENT]
lemma bdia_while: "\<langle>x| (d t \<cdot> r p) \<le> r p  \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
assume "\<langle>x| (d t \<cdot> r p) \<le> r p"
[PROOF STATE]
proof (state)
this:
\<langle>x| (d t \<cdot> r p) \<le> r p

goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
hence "\<langle>d t \<cdot> x| p \<le> r p"
[PROOF STATE]
proof (prove)
using this:
\<langle>x| (d t \<cdot> r p) \<le> r p

goal (1 subgoal):
 1. \<langle>d t \<cdot> x| p \<le> r p
[PROOF STEP]
by (metis bdia_export1 dka.dsg4 domrange rangedom)
[PROOF STATE]
proof (state)
this:
\<langle>d t \<cdot> x| p \<le> r p

goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
hence "\<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p"
[PROOF STATE]
proof (prove)
using this:
\<langle>d t \<cdot> x| p \<le> r p

goal (1 subgoal):
 1. \<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p
[PROOF STEP]
by (meson ardual.fdemodalisation22 ardual.kat_2_equiv_opp star_sim1)
[PROOF STATE]
proof (state)
this:
\<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p

goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
hence "r (ad t) \<cdot> \<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p \<cdot> ad t"
[PROOF STATE]
proof (prove)
using this:
\<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p

goal (1 subgoal):
 1. r (ad t) \<cdot> \<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p \<cdot> ad t
[PROOF STEP]
by (metis ardual.dpdz.dsg4 ars_r_def mult_isol r_ad)
[PROOF STATE]
proof (state)
this:
r (ad t) \<cdot> \<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p \<cdot> ad t

goal (1 subgoal):
 1. \<langle>x| (d t \<cdot> r p) \<le> r p \<Longrightarrow> \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r (ad t) \<cdot> \<langle>(d t \<cdot> x)\<^sup>\<star>| p \<le> r p \<cdot> ad t

goal (1 subgoal):
 1. \<langle>while t do x od| p \<le> r p \<cdot> ad t
[PROOF STEP]
by (metis bdia_export2 while_def r_ad)
[PROOF STATE]
proof (state)
this:
\<langle>while t do x od| p \<le> r p \<cdot> ad t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bdia_whilei: "r p \<le> r i \<Longrightarrow> r i \<cdot> ad t \<le> r q \<Longrightarrow> \<langle>x| (d t \<cdot> r i) \<le> r i \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
assume a1: "r p \<le> r i" and a2: "r i \<cdot> ad t \<le> r q" and "\<langle>x| (d t \<cdot> r i) \<le> r i"
[PROOF STATE]
proof (state)
this:
r p \<le> r i
r i \<cdot> ad t \<le> r q
\<langle>x| (d t \<cdot> r i) \<le> r i

goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
hence "\<langle>while t inv i do x od| i \<le> r i \<cdot> ad t"
[PROOF STATE]
proof (prove)
using this:
r p \<le> r i
r i \<cdot> ad t \<le> r q
\<langle>x| (d t \<cdot> r i) \<le> r i

goal (1 subgoal):
 1. \<langle>while t inv i do x od| i \<le> r i \<cdot> ad t
[PROOF STEP]
by (simp add: bdia_while whilei_def)
[PROOF STATE]
proof (state)
this:
\<langle>while t inv i do x od| i \<le> r i \<cdot> ad t

goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
hence "\<langle>while t inv i do x od| i \<le> r q"
[PROOF STATE]
proof (prove)
using this:
\<langle>while t inv i do x od| i \<le> r i \<cdot> ad t

goal (1 subgoal):
 1. \<langle>while t inv i do x od| i \<le> r q
[PROOF STEP]
using a2 dual_order.trans
[PROOF STATE]
proof (prove)
using this:
\<langle>while t inv i do x od| i \<le> r i \<cdot> ad t
r i \<cdot> ad t \<le> r q
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. \<langle>while t inv i do x od| i \<le> r q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>while t inv i do x od| i \<le> r q

goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
hence "r i \<le> |while t inv i do x od] r q"
[PROOF STATE]
proof (prove)
using this:
\<langle>while t inv i do x od| i \<le> r q

goal (1 subgoal):
 1. r i \<le>  |while t inv i do x od] r q
[PROOF STEP]
using ars_r_def box_diamond_galois_1 domrange
[PROOF STATE]
proof (prove)
using this:
\<langle>while t inv i do x od| i \<le> r q
r ?x = ar ar ?x
\<lbrakk>d ?p = ?p; d ?q = ?q\<rbrakk> \<Longrightarrow> (\<langle>?x| ?p \<le> ?q) = (?p \<le>  |?x] ?q)
d (r ?x) = r ?x

goal (1 subgoal):
 1. r i \<le>  |while t inv i do x od] r q
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
r i \<le>  |while t inv i do x od] r q

goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
hence "r p \<le> |while t inv i do x od] r q"
[PROOF STATE]
proof (prove)
using this:
r i \<le>  |while t inv i do x od] r q

goal (1 subgoal):
 1. r p \<le>  |while t inv i do x od] r q
[PROOF STEP]
using a1 dual_order.trans
[PROOF STATE]
proof (prove)
using this:
r i \<le>  |while t inv i do x od] r q
r p \<le> r i
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. r p \<le>  |while t inv i do x od] r q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r p \<le>  |while t inv i do x od] r q

goal (1 subgoal):
 1. \<lbrakk>r p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r p \<le>  |while t inv i do x od] r q

goal (1 subgoal):
 1. \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
using ars_r_def box_diamond_galois_1 domrange
[PROOF STATE]
proof (prove)
using this:
r p \<le>  |while t inv i do x od] r q
r ?x = ar ar ?x
\<lbrakk>d ?p = ?p; d ?q = ?q\<rbrakk> \<Longrightarrow> (\<langle>?x| ?p \<le> ?q) = (?p \<le>  |?x] ?q)
d (r ?x) = r ?x

goal (1 subgoal):
 1. \<langle>while t inv i do x od| p \<le> r q
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<langle>while t inv i do x od| p \<le> r q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bdia_whilei_break: "\<langle>y| p \<le> r i \<Longrightarrow> r i \<cdot> ad t \<le> r q \<Longrightarrow> \<langle>x| (d t \<cdot> r i) \<le> r i \<Longrightarrow> \<langle>y \<cdot> (while t inv i do x od)| p \<le> r q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>y| p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>y \<cdot> (while t inv i do x od)| p \<le> r q
[PROOF STEP]
using bdia_whilei ardual.ads_d_def ardual.ds.fdia_mult bdia_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r ?p \<le> r ?i; r ?i \<cdot> ad ?t \<le> r ?q; \<langle>?x| (d ?t \<cdot> r ?i) \<le> r ?i\<rbrakk> \<Longrightarrow> \<langle>while ?t inv ?i do ?x od| ?p \<le> r ?q
r ?x = ar ar ?x
\<langle>?y \<cdot> ?x| ?z = \<langle>?x| \<langle>?y| ?z
\<langle>?x| ?y = ar ar (?y \<cdot> ?x)

goal (1 subgoal):
 1. \<lbrakk>\<langle>y| p \<le> r i; r i \<cdot> ad t \<le> r q; \<langle>x| (d t \<cdot> r i) \<le> r i\<rbrakk> \<Longrightarrow> \<langle>y \<cdot> (while t inv i do x od)| p \<le> r q
[PROOF STEP]
by auto


[STATEMENT]
lemma bdia_assign [simp]: "rel_antirange_kleene_algebra.bdia (v ::= e) \<lceil>P\<rceil> = \<lceil>\<lambda>s. \<exists>w. s v = e (s(v := w)) \<and> P (s(v:=w))\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_antirange_kleene_algebra.bdia (v ::= e) \<lceil>P\<rceil> = \<lceil>\<lambda>s. \<exists>w. s v = e (s(v := w)) \<and> P (s(v := w))\<rceil>
[PROOF STEP]
apply (simp add: rel_antirange_kleene_algebra.bdia_def gets_def p2r_def rel_ar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(y, y) |y. \<exists>x. (x, y) \<in> {(s, s) |s. P s} ; {uu_. \<exists>s. uu_ = (s, s(v := e s))}} = {(s, s) |s. \<exists>w. s v = e (s(v := w)) \<and> P (s(v := w))}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b y x xa ya z s sa. P s \<Longrightarrow> \<exists>sa. (s(v := e s), s(v := e s)) = (sa, sa) \<and> (\<exists>w. sa v = e (sa(v := w)) \<and> P (sa(v := w)))
 2. \<And>a b s w. \<lbrakk>s v = e (s(v := w)); P (s(v := w))\<rbrakk> \<Longrightarrow> \<exists>y. (s, s) = (y, y) \<and> (\<exists>x. (x, y) \<in> {(s, s) |s. P s} ; {uu_. \<exists>s. uu_ = (s, s(v := e s))})
[PROOF STEP]
by (metis fun_upd_apply fun_upd_triv fun_upd_upd, fastforce)


[STATEMENT]
lemma d_p2r [simp]: "rel_antirange_kleene_algebra.ars_r  \<lceil>P\<rceil> = \<lceil>P\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_antirange_kleene_algebra.ars_r \<lceil>P\<rceil> = \<lceil>P\<rceil>
[PROOF STEP]
by (simp add: p2r_def rel_antirange_kleene_algebra.ars_r_def rel_ar_def)