[STATEMENT]
lemma forall_unique_repr:
  "\<forall> x \<in> G // K. \<exists>! k \<in> \<phi> ` (G // K). x = k \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Partition. \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
assume hx: "x \<in> G // K"
[PROOF STATE]
proof (state)
this:
x \<in> Partition

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Partition
[PROOF STEP]
have "\<phi> x \<cdot>| K = x"
[PROOF STATE]
proof (prove)
using this:
x \<in> Partition

goal (1 subgoal):
 1. \<phi> x \<cdot>| K = x
[PROOF STEP]
by (metis Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset representant_exists)
[PROOF STATE]
proof (state)
this:
\<phi> x \<cdot>| K = x

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> x \<cdot>| K = x
[PROOF STEP]
have hex: "\<exists> k \<in> \<phi> ` (G // K). x = k \<cdot>| K"
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<cdot>| K = x

goal (1 subgoal):
 1. \<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K
[PROOF STEP]
using hx
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<cdot>| K = x
x \<in> Partition

goal (1 subgoal):
 1. \<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
have "\<And> a b. a \<in> \<phi> ` (G // K) \<Longrightarrow> x = a \<cdot>| K \<Longrightarrow> b \<in> \<phi> ` (G // K) \<Longrightarrow> x = b \<cdot>| K \<Longrightarrow>
    a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; x = a \<cdot>| K; b \<in> \<phi> ` Partition; x = b \<cdot>| K\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; x = a \<cdot>| K; b \<in> \<phi> ` Partition; x = b \<cdot>| K\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; x = a \<cdot>| K; b \<in> \<phi> ` Partition; x = b \<cdot>| K\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
assume "a \<in> \<phi> ` (G // K)" and hxa: "x = a \<cdot>| K" and "b \<in> \<phi> ` (G // K)" and
      hxb: "x = b \<cdot>| K"
[PROOF STATE]
proof (state)
this:
a \<in> \<phi> ` Partition
x = a \<cdot>| K
b \<in> \<phi> ` Partition
x = b \<cdot>| K

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; x = a \<cdot>| K; b \<in> \<phi> ` Partition; x = b \<cdot>| K\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<phi> ` Partition
x = a \<cdot>| K
b \<in> \<phi> ` Partition
x = b \<cdot>| K
[PROOF STEP]
obtain z w where "a = \<phi> (z \<cdot>| K)" and "b = \<phi> (w \<cdot>| K)" and "z \<in> G" and "w \<in> G"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` Partition
x = a \<cdot>| K
b \<in> \<phi> ` Partition
x = b \<cdot>| K

goal (1 subgoal):
 1. (\<And>z w. \<lbrakk>a = \<phi> (z \<cdot>| K); b = \<phi> (w \<cdot>| K); z \<in> G; w \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using representant_exists Left_Coset_Class_unit
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` Partition
x = a \<cdot>| K
b \<in> \<phi> ` Partition
x = b \<cdot>| K
?A \<in> Partition \<Longrightarrow> \<exists>a\<in>G. a \<in> ?A \<and> ?A = Class a
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g

goal (1 subgoal):
 1. (\<And>z w. \<lbrakk>a = \<phi> (z \<cdot>| K); b = \<phi> (w \<cdot>| K); z \<in> G; w \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = \<phi> (z \<cdot>| K)
b = \<phi> (w \<cdot>| K)
z \<in> G
w \<in> G

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; x = a \<cdot>| K; b \<in> \<phi> ` Partition; x = b \<cdot>| K\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = \<phi> (z \<cdot>| K)
b = \<phi> (w \<cdot>| K)
z \<in> G
w \<in> G
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
a = \<phi> (z \<cdot>| K)
b = \<phi> (w \<cdot>| K)
z \<in> G
w \<in> G

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using hxa hxb
[PROOF STATE]
proof (prove)
using this:
a = \<phi> (z \<cdot>| K)
b = \<phi> (w \<cdot>| K)
z \<in> G
w \<in> G
x = a \<cdot>| K
x = b \<cdot>| K

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis Class_in_Partition Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset)
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> \<phi> ` Partition; x = ?a \<cdot>| K; ?b \<in> \<phi> ` Partition; x = ?b \<cdot>| K\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K
\<lbrakk>?a \<in> \<phi> ` Partition; x = ?a \<cdot>| K; ?b \<in> \<phi> ` Partition; x = ?b \<cdot>| K\<rbrakk> \<Longrightarrow> ?a = ?b
[PROOF STEP]
show "\<exists>! k \<in> \<phi> ` (G // K). x = k \<cdot>| K"
[PROOF STATE]
proof (prove)
using this:
\<exists>k\<in>\<phi> ` Partition. x = k \<cdot>| K
\<lbrakk>?a \<in> \<phi> ` Partition; x = ?a \<cdot>| K; ?b \<in> \<phi> ` Partition; x = ?b \<cdot>| K\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. \<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>!k. k \<in> \<phi> ` Partition \<and> x = k \<cdot>| K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_inj_on:
  shows "inj_on \<phi> (G // K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on \<phi> Partition
[PROOF STEP]
proof(intro inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Partition; y \<in> Partition; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Partition; y \<in> Partition; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "x \<in> G // K" and hy: "y \<in> G // K" and hxy: "\<phi> x = \<phi> y"
[PROOF STATE]
proof (state)
this:
x \<in> Partition
y \<in> Partition
\<phi> x = \<phi> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Partition; y \<in> Partition; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Partition
y \<in> Partition
\<phi> x = \<phi> y
[PROOF STEP]
obtain a b where "x = a \<cdot>| K" and "y = b \<cdot>| K" and "a \<in> G" and "b \<in> G"
[PROOF STATE]
proof (prove)
using this:
x \<in> Partition
y \<in> Partition
\<phi> x = \<phi> y

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = a \<cdot>| K; y = b \<cdot>| K; a \<in> G; b \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using representant_exists Left_Coset_Class_unit
[PROOF STATE]
proof (prove)
using this:
x \<in> Partition
y \<in> Partition
\<phi> x = \<phi> y
?A \<in> Partition \<Longrightarrow> \<exists>a\<in>G. a \<in> ?A \<and> ?A = Class a
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = a \<cdot>| K; y = b \<cdot>| K; a \<in> G; b \<in> G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = a \<cdot>| K
y = b \<cdot>| K
a \<in> G
b \<in> G

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Partition; y \<in> Partition; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = a \<cdot>| K
y = b \<cdot>| K
a \<in> G
b \<in> G
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
x = a \<cdot>| K
y = b \<cdot>| K
a \<in> G
b \<in> G

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using hxy hy
[PROOF STATE]
proof (prove)
using this:
x = a \<cdot>| K
y = b \<cdot>| K
a \<in> G
b \<in> G
\<phi> x = \<phi> y
y \<in> Partition

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis phi_coset_mem phi_mem_coset_eq)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_coset_eq_self:
  assumes "a \<in> G // K"
  shows "\<phi> a \<cdot>| K = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> a \<cdot>| K = a
[PROOF STEP]
by (metis Class_closed Class_is_Left_Coset assms phi_coset_mem phi_eq_coset representant_exists)


[STATEMENT]
lemma phi_coset_comp_eq:
  assumes "a \<in> G // K" and "b \<in> G // K"
  shows "\<phi> a \<cdot> \<phi> b \<cdot>| K = a [\<cdot>] b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> a \<cdot> \<phi> b \<cdot>| K = a [\<cdot>] b
[PROOF STEP]
using assms phi_coset_eq_self
[PROOF STATE]
proof (prove)
using this:
a \<in> Partition
b \<in> Partition
?a \<in> Partition \<Longrightarrow> \<phi> ?a \<cdot>| K = ?a

goal (1 subgoal):
 1. \<phi> a \<cdot> \<phi> b \<cdot>| K = a [\<cdot>] b
[PROOF STEP]
by (metis Class_is_Left_Coset block_closed factor_composition phi_coset_mem representant_exists)


[STATEMENT]
lemma phi_comp_eq:
  assumes "a \<in> G // K" and "b \<in> G // K"
  shows "\<phi> (a [\<cdot>] b) = quot_comp_alt (\<phi> a) (\<phi> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (a [\<cdot>] b) = quot_comp_alt (\<phi> a) (\<phi> b)
[PROOF STEP]
using phi_coset_comp_eq quot_comp_alt_def assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> Partition; ?b \<in> Partition\<rbrakk> \<Longrightarrow> \<phi> ?a \<cdot> \<phi> ?b \<cdot>| K = ?a [\<cdot>] ?b
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
a \<in> Partition
b \<in> Partition

goal (1 subgoal):
 1. \<phi> (a [\<cdot>] b) = quot_comp_alt (\<phi> a) (\<phi> b)
[PROOF STEP]
by auto


[STATEMENT]
lemma phi_image_subset:
  "\<phi> ` (G // K) \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` Partition \<subseteq> G
[PROOF STEP]
proof(intro image_subsetI, simp add: \<phi>_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> (SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> (SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G
[PROOF STEP]
assume "x \<in> G // K"
[PROOF STATE]
proof (state)
this:
x \<in> Partition

goal (1 subgoal):
 1. \<And>x. x \<in> Partition \<Longrightarrow> (SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Partition
[PROOF STEP]
show "(SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G"
[PROOF STATE]
proof (prove)
using this:
x \<in> Partition

goal (1 subgoal):
 1. (SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G
[PROOF STEP]
using Left_Coset_Class_unit representant_exists someI_ex
[PROOF STATE]
proof (prove)
using this:
x \<in> Partition
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
?A \<in> Partition \<Longrightarrow> \<exists>a\<in>G. a \<in> ?A \<and> ?A = Class a
\<exists>x. ?P x \<Longrightarrow> ?P (SOME x. ?P x)

goal (1 subgoal):
 1. (SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
(SOME a. a \<in> G \<and> x = a \<cdot>| K) \<in> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_image_group:
  "Group_Theory.group (\<phi> ` (G // K)) quot_comp_alt (\<phi> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
have hmonoid: "Group_Theory.monoid (\<phi> ` (G // K)) quot_comp_alt (\<phi> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt a b \<in> \<phi> ` Partition
 2. \<phi> K \<in> \<phi> ` Partition
 3. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
 4. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 5. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
show "\<And>a b. a \<in> \<phi> ` (G // K) \<Longrightarrow> b \<in> \<phi> ` (G // K) \<Longrightarrow>
      quot_comp_alt a b \<in> \<phi> ` (G // K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt a b \<in> \<phi> ` Partition
[PROOF STEP]
using quot_comp_alt_def imageI phi_image_subset
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt a b \<in> \<phi> ` Partition
[PROOF STEP]
by (metis Class_in_Partition Left_Coset_Class_unit composition_closed subset_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> \<phi> ` Partition; ?b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt ?a ?b \<in> \<phi> ` Partition

goal (4 subgoals):
 1. \<phi> K \<in> \<phi> ` Partition
 2. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
 3. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 4. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<phi> K \<in> \<phi> ` Partition
 2. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
 3. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 4. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
show "(\<phi> K) \<in> \<phi> ` (G // K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> K \<in> \<phi> ` Partition
[PROOF STEP]
using \<phi>_def Left_Coset_Class_unit imageI Normal_def
[PROOF STATE]
proof (prove)
using this:
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A
K = Class \<one>

goal (1 subgoal):
 1. \<phi> K \<in> \<phi> ` Partition
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> K \<in> \<phi> ` Partition

goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
 2. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 3. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
 2. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 3. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
show "\<And>a b c. a \<in> \<phi> ` Partition \<Longrightarrow> b \<in> \<phi> ` Partition \<Longrightarrow> c \<in> \<phi> ` Partition \<Longrightarrow>
        quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
assume ha: "a \<in> \<phi> ` (G // K)" and hb: "b \<in> \<phi> ` (G // K)" and hc: "c \<in> \<phi> ` (G // K)"
[PROOF STATE]
proof (state)
this:
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
have habc: "a \<cdot> b \<cdot> c \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b \<cdot> c \<in> G
[PROOF STEP]
using ha hb hc composition_closed phi_image_subset
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> G
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. a \<cdot> b \<cdot> c \<in> G
[PROOF STEP]
by (meson subsetD)
[PROOF STATE]
proof (state)
this:
a \<cdot> b \<cdot> c \<in> G

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
have hab: "quot_comp_alt a b \<in> (a \<cdot> b) \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K
[PROOF STEP]
using phi_image_subset quot_comp_alt_def ha hb
[PROOF STATE]
proof (prove)
using this:
\<phi> ` Partition \<subseteq> G
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition

goal (1 subgoal):
 1. quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K
[PROOF STEP]
by (metis composition_closed phi_coset_mem subsetD)
[PROOF STATE]
proof (state)
this:
quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K
[PROOF STEP]
have "quot_comp_alt (quot_comp_alt a b) c \<in> (a \<cdot> b \<cdot> c) \<cdot>| K"
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K

goal (1 subgoal):
 1. quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K
[PROOF STEP]
using quot_comp_alt_def phi_image_subset ha hb hc
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt a b \<in> a \<cdot> b \<cdot>| K
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
\<phi> ` Partition \<subseteq> G
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition

goal (1 subgoal):
 1. quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K
[PROOF STEP]
by (smt (z3) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit composition_closed
          natural.commutes_with_composition phi_coset_mem subset_iff)
[PROOF STATE]
proof (state)
this:
quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
have hbc: "quot_comp_alt b c \<in> (b \<cdot> c) \<cdot>| K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
[PROOF STEP]
using hb hc phi_image_subset quot_comp_alt_def
[PROOF STATE]
proof (prove)
using this:
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition
\<phi> ` Partition \<subseteq> G
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)

goal (1 subgoal):
 1. quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
[PROOF STEP]
by (metis composition_closed phi_coset_mem subset_iff)
[PROOF STATE]
proof (state)
this:
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
hence "quot_comp_alt a (quot_comp_alt b c) \<in> (a \<cdot> b \<cdot> c) \<cdot>| K"
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K
[PROOF STEP]
using quot_comp_alt_def phi_image_subset ha hb hc
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
\<phi> ` Partition \<subseteq> G
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition

goal (1 subgoal):
 1. quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K
[PROOF STEP]
by (smt (verit, del_insts) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit
          associative composition_closed natural.commutes_with_composition phi_coset_mem subset_iff)
[PROOF STATE]
proof (state)
this:
quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
have "a \<cdot> (quot_comp_alt b c) \<cdot>| K \<in> G // K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition
[PROOF STEP]
using ha hb hc phi_image_subset
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition
[PROOF STEP]
by (metis Class_closed Class_in_Partition Class_is_Left_Coset hbc composition_closed in_mono subset_eq)
[PROOF STATE]
proof (state)
this:
a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
have "(quot_comp_alt a b) \<cdot> c \<cdot>| K \<in> G // K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition
[PROOF STEP]
using ha hb hc phi_image_subset
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` Partition
b \<in> \<phi> ` Partition
c \<in> \<phi> ` Partition
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition
[PROOF STEP]
by (metis Class_closed Class_in_Partition Left_Coset_Class_unit hab composition_closed in_mono)
[PROOF STATE]
proof (state)
this:
quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a \<in> \<phi> ` Partition; b \<in> \<phi> ` Partition; c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K
a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition
quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition
[PROOF STEP]
show "quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)"
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K
a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition
quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition

goal (1 subgoal):
 1. quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
using phi_mem_coset_eq[OF _ habc] quot_comp_alt_def
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt (quot_comp_alt a b) c \<in> a \<cdot> b \<cdot> c \<cdot>| K
quot_comp_alt b c \<in> b \<cdot> c \<cdot>| K
quot_comp_alt a (quot_comp_alt b c) \<in> a \<cdot> b \<cdot> c \<cdot>| K
a \<cdot> quot_comp_alt b c \<cdot>| K \<in> Partition
quot_comp_alt a b \<cdot> c \<cdot>| K \<in> Partition
\<lbrakk>?a \<in> Partition; \<phi> ?a \<in> a \<cdot> b \<cdot> c \<cdot>| K\<rbrakk> \<Longrightarrow> ?a = a \<cdot> b \<cdot> c \<cdot>| K
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)

goal (1 subgoal):
 1. quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> \<phi> ` Partition; ?b \<in> \<phi> ` Partition; ?c \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt (quot_comp_alt ?a ?b) ?c = quot_comp_alt ?a (quot_comp_alt ?b ?c)

goal (2 subgoals):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 2. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
 2. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
show "\<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
[PROOF STEP]
using quot_comp_alt_def \<phi>_def
        phi_image_subset image_iff phi_coset_eq subsetD
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
\<phi> ` Partition \<subseteq> G
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)
\<lbrakk>?a \<in> G; \<phi> ?x = ?a; ?x \<in> Partition\<rbrakk> \<Longrightarrow> \<phi> (?a \<cdot>| K) = ?a
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) a = a
[PROOF STEP]
by (smt (z3) Normal_def Partition_def
        natural.image.sub_unit_closed phi_comp_eq quotient.left_unit)
[PROOF STATE]
proof (state)
this:
?a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt (\<phi> K) ?a = ?a

goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
show "\<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
using quot_comp_alt_def \<phi>_def
        phi_image_subset image_iff phi_coset_eq subsetD
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt ?a ?b = \<phi> (?a \<cdot> ?b \<cdot>| K)
\<phi> = (\<lambda>x. if x \<in> Partition then SOME a. a \<in> G \<and> x = a \<cdot>| K else undefined)
\<phi> ` Partition \<subseteq> G
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)
\<lbrakk>?a \<in> G; \<phi> ?x = ?a; ?x \<in> Partition\<rbrakk> \<Longrightarrow> \<phi> (?a \<cdot>| K) = ?a
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. \<And>a. a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt a (\<phi> K) = a
[PROOF STEP]
by (smt (verit) Normal_def
        factor_composition factor_unit normal_subgroup.phi_coset_eq_self normal_subgroup_axioms
        quotient.unit_closed right_unit unit_closed)
[PROOF STATE]
proof (state)
this:
?a \<in> \<phi> ` Partition \<Longrightarrow> quot_comp_alt ?a (\<phi> K) = ?a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal (1 subgoal):
 1. Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal (1 subgoal):
 1. Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
show "Group_Theory.group (\<phi> ` (G // K)) quot_comp_alt (\<phi> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
proof(simp add: group_def group_axioms_def hmonoid)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>u. u \<in> \<phi> ` Partition \<longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
show "\<forall>u. u \<in> \<phi> ` Partition \<longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. u \<in> \<phi> ` Partition \<longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
proof(intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
assume hg: "g \<in> \<phi> ` (G // K)"
[PROOF STATE]
proof (state)
this:
g \<in> \<phi> ` Partition

goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> \<phi> ` Partition
[PROOF STEP]
have "quot_comp_alt g (\<phi> ((inverse g) \<cdot>| K)) = (\<phi> K)"
        and "quot_comp_alt (\<phi> ((inverse g) \<cdot>| K)) g = (\<phi> K)"
[PROOF STATE]
proof (prove)
using this:
g \<in> \<phi> ` Partition

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K &&& quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
using phi_image_subset phi_inverse_right phi_inverse_left
[PROOF STATE]
proof (prove)
using this:
g \<in> \<phi> ` Partition
\<phi> ` Partition \<subseteq> G
?g \<in> G \<Longrightarrow> quot_comp_alt ?g (\<phi> (local.inverse ?g \<cdot>| K)) = \<phi> K
?g \<in> G \<Longrightarrow> quot_comp_alt (\<phi> (local.inverse ?g \<cdot>| K)) ?g = \<phi> K

goal (1 subgoal):
 1. quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K &&& quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K

goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K

goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
have "\<phi> ((inverse g) \<cdot>| K) \<in> \<phi> ` (G // K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition
[PROOF STEP]
using imageI hg phi_image_subset
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A
g \<in> \<phi> ` Partition
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. \<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition
[PROOF STEP]
by (metis (no_types, opaque_lifting) Class_in_Partition Left_Coset_Class_unit in_mono
        invertible invertible_inverse_closed)
[PROOF STATE]
proof (state)
this:
\<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition

goal (1 subgoal):
 1. \<And>u. u \<in> \<phi> ` Partition \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
\<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition
[PROOF STEP]
show "monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) g"
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
\<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition

goal (1 subgoal):
 1. monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) g
[PROOF STEP]
using monoid.invertibleI[OF hmonoid] hg
[PROOF STATE]
proof (prove)
using this:
quot_comp_alt g (\<phi> (local.inverse g \<cdot>| K)) = \<phi> K
quot_comp_alt (\<phi> (local.inverse g \<cdot>| K)) g = \<phi> K
\<phi> (local.inverse g \<cdot>| K) \<in> \<phi> ` Partition
\<lbrakk>quot_comp_alt ?u ?v = \<phi> K; quot_comp_alt ?v ?u = \<phi> K; ?u \<in> \<phi> ` Partition; ?v \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) ?u
g \<in> \<phi> ` Partition

goal (1 subgoal):
 1. monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) g
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u. u \<in> \<phi> ` Partition \<longrightarrow> monoid.invertible (\<phi> ` Partition) quot_comp_alt (\<phi> K) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_map: "Set_Theory.map \<phi> Partition (\<phi> ` Partition)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map \<phi> Partition (\<phi> ` Partition)
[PROOF STEP]
by (auto simp add: Set_Theory.map_def \<phi>_def)


[STATEMENT]
lemma phi_image_isomorphic:
  "group_isomorphism \<phi> (G // K) ([\<cdot>]) (Class \<one>) (\<phi> ` (G // K)) quot_comp_alt (\<phi> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
have "bijective_map \<phi> Partition (\<phi> ` Partition)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bijective_map \<phi> Partition (\<phi> ` Partition)
[PROOF STEP]
using bijective_map_def bijective_def bij_betw_def phi_inj_on phi_map
[PROOF STATE]
proof (prove)
using this:
bijective_map ?\<alpha> ?S ?T \<equiv> Set_Theory.map ?\<alpha> ?S ?T \<and> bijective ?\<alpha> ?S ?T
bijective ?\<alpha> ?S ?T \<equiv> bij_betw ?\<alpha> ?S ?T
bij_betw ?f ?A ?B = (inj_on ?f ?A \<and> ?f ` ?A = ?B)
inj_on \<phi> Partition
Set_Theory.map \<phi> Partition (\<phi> ` Partition)

goal (1 subgoal):
 1. bijective_map \<phi> Partition (\<phi> ` Partition)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bijective_map \<phi> Partition (\<phi> ` Partition)

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bijective_map \<phi> Partition (\<phi> ` Partition)

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
have "Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
using phi_image_group group_def
[PROOF STATE]
proof (prove)
using this:
Group_Theory.group (\<phi> ` Partition) quot_comp_alt (\<phi> K)
Group_Theory.group ?G ?composition ?unit \<equiv> Group_Theory.monoid ?G ?composition ?unit \<and> Group_Theory.group_axioms ?G ?composition ?unit

goal (1 subgoal):
 1. Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
have "\<phi> (Class \<one>) = \<phi> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Class \<one>) = \<phi> K
[PROOF STEP]
using Left_Coset_Class_unit Normal_def
[PROOF STATE]
proof (prove)
using this:
?g \<in> G \<Longrightarrow> ?g \<cdot>| K = Class ?g
K = Class \<one>

goal (1 subgoal):
 1. \<phi> (Class \<one>) = \<phi> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (Class \<one>) = \<phi> K

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bijective_map \<phi> Partition (\<phi> ` Partition)
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)
\<phi> (Class \<one>) = \<phi> K
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bijective_map \<phi> Partition (\<phi> ` Partition)
Group_Theory.monoid (\<phi> ` Partition) quot_comp_alt (\<phi> K)
\<phi> (Class \<one>) = \<phi> K

goal (1 subgoal):
 1. group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)
[PROOF STEP]
by (auto simp add: group_isomorphism_def group_homomorphism_def monoid_homomorphism_def
    phi_image_group quotient.monoid_axioms quotient.group_axioms monoid_homomorphism_axioms_def
    phi_comp_eq phi_map)
[PROOF STATE]
proof (state)
this:
group_isomorphism \<phi> Partition ([\<cdot>]) (Class \<one>) (\<phi> ` Partition) quot_comp_alt (\<phi> K)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Union_Coset_card_eq:
  assumes hSG: "S \<subseteq> G" and hSU: "(\<Union> (Class ` S)) = S"
  shows "card S = card H * card (Class ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
proof(cases "finite H")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
case hH: True
[PROOF STATE]
proof (state)
this:
finite H

goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have hfin: "\<And>A. A \<in> Class ` S \<Longrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. A \<in> Class ` S \<Longrightarrow> finite A
[PROOF STEP]
using hSG Right_Coset_Class_unit
    Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> G
?g \<in> G \<Longrightarrow> Right_Coset H ?g = Class ?g
?x \<in> G \<Longrightarrow> card (Right_Coset H ?x) = card H
finite H
(card ?A = 0) = (?A = {} \<or> infinite ?A)
(?c \<in> {}) = False
\<zero> \<in> H
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. \<And>A. A \<in> Class ` S \<Longrightarrow> finite A
[PROOF STEP]
by (smt (verit, del_insts) imageE)
[PROOF STATE]
proof (state)
this:
?A \<in> Class ` S \<Longrightarrow> finite ?A

goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have "card S = card H * card (Class ` S)" when hS: "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
have hdisj: "pairwise (\<lambda>s t. disjnt s t) (Class ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairwise disjnt (Class ` S)
[PROOF STEP]
proof (intro pairwiseI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Class ` S; y \<in> Class ` S; x \<noteq> y\<rbrakk> \<Longrightarrow> disjnt x y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Class ` S; y \<in> Class ` S; x \<noteq> y\<rbrakk> \<Longrightarrow> disjnt x y
[PROOF STEP]
assume "x \<in> Class ` S" and "y \<in> Class ` S" and hxy: "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<in> Class ` S
y \<in> Class ` S
x \<noteq> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Class ` S; y \<in> Class ` S; x \<noteq> y\<rbrakk> \<Longrightarrow> disjnt x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Class ` S
y \<in> Class ` S
x \<noteq> y
[PROOF STEP]
obtain a b where "x = Class a" and "y = Class b" and
        "a \<in> S" and "b \<in> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> Class ` S
y \<in> Class ` S
x \<noteq> y

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = Class a; y = Class b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = Class a
y = Class b
a \<in> S
b \<in> S

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Class ` S; y \<in> Class ` S; x \<noteq> y\<rbrakk> \<Longrightarrow> disjnt x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Class a
y = Class b
a \<in> S
b \<in> S
[PROOF STEP]
show "disjnt x y"
[PROOF STATE]
proof (prove)
using this:
x = Class a
y = Class b
a \<in> S
b \<in> S

goal (1 subgoal):
 1. disjnt x y
[PROOF STEP]
using disjnt_def hxy
[PROOF STATE]
proof (prove)
using this:
x = Class a
y = Class b
a \<in> S
b \<in> S
disjnt ?A ?B = (?A \<inter> ?B = {})
x \<noteq> y

goal (1 subgoal):
 1. disjnt x y
[PROOF STEP]
by (smt (verit, ccfv_threshold) not_disjoint_implies_equal hSG subsetD)
[PROOF STATE]
proof (state)
this:
disjnt x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pairwise disjnt (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pairwise disjnt (Class ` S)
[PROOF STEP]
have "card (\<Union> (Class ` S)) = sum card (Class ` S)"
[PROOF STATE]
proof (prove)
using this:
pairwise disjnt (Class ` S)

goal (1 subgoal):
 1. card (\<Union> (Class ` S)) = sum card (Class ` S)
[PROOF STEP]
using card_Union_disjoint hfin
[PROOF STATE]
proof (prove)
using this:
pairwise disjnt (Class ` S)
\<lbrakk>pairwise disjnt ?C; \<And>A. A \<in> ?C \<Longrightarrow> finite A\<rbrakk> \<Longrightarrow> card (\<Union> ?C) = sum card ?C
?A \<in> Class ` S \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. card (\<Union> (Class ` S)) = sum card (Class ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union> (Class ` S)) = sum card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (\<Union> (Class ` S)) = sum card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
have "finite (Class ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Class ` S)
[PROOF STEP]
using hS
[PROOF STATE]
proof (prove)
using this:
finite S

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

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
finite (Class ` S)
[PROOF STEP]
have "card (\<Union> (Class ` S)) = (\<Sum> a \<in> Class ` S. card a)"
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
finite (Class ` S)

goal (1 subgoal):
 1. card (\<Union> (Class ` S)) = sum card (Class ` S)
[PROOF STEP]
using sum_card_image hdisj
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
finite (Class ` S)
\<lbrakk>finite ?A; pairwise (\<lambda>s t. disjnt (?f s) (?f t)) ?A\<rbrakk> \<Longrightarrow> sum card (?f ` ?A) = (\<Sum>a\<in>?A. card (?f a))
pairwise disjnt (Class ` S)

goal (1 subgoal):
 1. card (\<Union> (Class ` S)) = sum card (Class ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union> (Class ` S)) = sum card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (\<Union> (Class ` S)) = sum card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
have "\<And> a. a \<in> Class ` S \<Longrightarrow> card a = card H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> Class ` S \<Longrightarrow> card a = card H
[PROOF STEP]
using hSG Right_Coset_Class_unit Right_Coset_cardinality
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> G
?g \<in> G \<Longrightarrow> Right_Coset H ?g = Class ?g
?x \<in> G \<Longrightarrow> card (Right_Coset H ?x) = card H

goal (1 subgoal):
 1. \<And>a. a \<in> Class ` S \<Longrightarrow> card a = card H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?a \<in> Class ` S \<Longrightarrow> card ?a = card H

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
?a \<in> Class ` S \<Longrightarrow> card ?a = card H
[PROOF STEP]
show "card S = card H * card (Class ` S)"
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
?a \<in> Class ` S \<Longrightarrow> card ?a = card H

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
using hSU
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (Class ` S)) = sum card (Class ` S)
?a \<in> Class ` S \<Longrightarrow> card ?a = card H
\<Union> (Class ` S) = S

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card S = card H * card (Class ` S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite S \<Longrightarrow> card S = card H * card (Class ` S)

goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite S \<Longrightarrow> card S = card H * card (Class ` S)

goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have "card S = card H * card (Class ` S)" when hS: "\<not> finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
using finite_Union hfin hS hSU
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; \<And>M. M \<in> ?A \<Longrightarrow> finite M\<rbrakk> \<Longrightarrow> finite (\<Union> ?A)
?A \<in> Class ` S \<Longrightarrow> finite ?A
infinite S
\<Union> (Class ` S) = S

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by (metis card_eq_0_iff mult_0_right)
[PROOF STATE]
proof (state)
this:
infinite S \<Longrightarrow> card S = card H * card (Class ` S)

goal (2 subgoals):
 1. finite H \<Longrightarrow> card S = card H * card (Class ` S)
 2. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite S \<Longrightarrow> card S = card H * card (Class ` S)
infinite S \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite S \<Longrightarrow> card S = card H * card (Class ` S)
infinite S \<Longrightarrow> card S = card H * card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card S = card H * card (Class ` S)

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
case hH: False
[PROOF STATE]
proof (state)
this:
infinite H

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have "card S = card H * card (Class ` S)" when "S = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by (simp add: that)
[PROOF STATE]
proof (state)
this:
S = {} \<Longrightarrow> card S = card H * card (Class ` S)

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S = {} \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have hinf: "\<And> A. A \<in> Class ` S \<Longrightarrow> infinite A"
[PROOF STATE]
proof (prove)
using this:
S = {} \<Longrightarrow> card S = card H * card (Class ` S)

goal (1 subgoal):
 1. \<And>A. A \<in> Class ` S \<Longrightarrow> infinite A
[PROOF STEP]
using hSG Right_Coset_Class_unit
    Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD
[PROOF STATE]
proof (prove)
using this:
S = {} \<Longrightarrow> card S = card H * card (Class ` S)
S \<subseteq> G
?g \<in> G \<Longrightarrow> Right_Coset H ?g = Class ?g
?x \<in> G \<Longrightarrow> card (Right_Coset H ?x) = card H
infinite H
(card ?A = 0) = (?A = {} \<or> infinite ?A)
(?c \<in> {}) = False
\<zero> \<in> H
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. \<And>A. A \<in> Class ` S \<Longrightarrow> infinite A
[PROOF STEP]
by (smt (verit) Class_self imageE)
[PROOF STATE]
proof (state)
this:
?A \<in> Class ` S \<Longrightarrow> infinite ?A

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?A \<in> Class ` S \<Longrightarrow> infinite ?A

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
have "card S = card H * card (Class ` S)" when "S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
using hSU
[PROOF STATE]
proof (prove)
using this:
\<Union> (Class ` S) = S

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by (metis Class_closed2
    Normal_def card.infinite card_sumset_0_iff hH hSG mult_is_0 sumset_subgroup_eq_Class_Union unit_closed)
[PROOF STATE]
proof (state)
this:
S \<noteq> {} \<Longrightarrow> card S = card H * card (Class ` S)

goal (1 subgoal):
 1. infinite H \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?A \<in> Class ` S \<Longrightarrow> infinite ?A
S \<noteq> {} \<Longrightarrow> card S = card H * card (Class ` S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?A \<in> Class ` S \<Longrightarrow> infinite ?A
S \<noteq> {} \<Longrightarrow> card S = card H * card (Class ` S)

goal (1 subgoal):
 1. card S = card H * card (Class ` S)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card S = card H * card (Class ` S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_image_sumset_eq:
  assumes "A \<subseteq> G // H" and "B \<subseteq> G // H"
  shows "\<phi> ` (GH.sumset A B) = GH_repr.sumset (\<phi> ` A) (\<phi> ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` GH.sumset A B = GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
[PROOF STEP]
proof(intro subset_antisym image_subsetI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> GH.sumset A B \<Longrightarrow> \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
 2. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> GH.sumset A B \<Longrightarrow> \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
 2. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
assume "x \<in> GH.sumset A B"
[PROOF STATE]
proof (state)
this:
x \<in> GH.sumset A B

goal (2 subgoals):
 1. \<And>x. x \<in> GH.sumset A B \<Longrightarrow> \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
 2. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> GH.sumset A B
[PROOF STEP]
obtain c d where "x = quotient_composition c d" and hc: "c \<in> A" and hd: "d \<in> B"
[PROOF STATE]
proof (prove)
using this:
x \<in> GH.sumset A B

goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>x = c [\<cdot>] d; c \<in> A; d \<in> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GH.sumset.cases
[PROOF STATE]
proof (prove)
using this:
x \<in> GH.sumset A B
\<lbrakk>?a \<in> GH.sumset ?A ?B; \<And>a b. \<lbrakk>?a = a [\<cdot>] b; a \<in> ?A; a \<in> Partition; b \<in> ?B; b \<in> Partition\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>x = c [\<cdot>] d; c \<in> A; d \<in> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = c [\<cdot>] d
c \<in> A
d \<in> B

goal (2 subgoals):
 1. \<And>x. x \<in> GH.sumset A B \<Longrightarrow> \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
 2. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = c [\<cdot>] d
c \<in> A
d \<in> B
[PROOF STEP]
have "\<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)"
[PROOF STATE]
proof (prove)
using this:
x = c [\<cdot>] d
c \<in> A
d \<in> B

goal (1 subgoal):
 1. \<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)
[PROOF STEP]
using phi_comp_eq assms subsetD
[PROOF STATE]
proof (prove)
using this:
x = c [\<cdot>] d
c \<in> A
d \<in> B
\<lbrakk>?a \<in> Partition; ?b \<in> Partition\<rbrakk> \<Longrightarrow> \<phi> (?a [\<cdot>] ?b) = quot_comp_alt (\<phi> ?a) (\<phi> ?b)
A \<subseteq> Partition
B \<subseteq> Partition
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. \<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)

goal (2 subgoals):
 1. \<And>x. x \<in> GH.sumset A B \<Longrightarrow> \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
 2. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)
[PROOF STEP]
show "\<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)"
[PROOF STATE]
proof (prove)
using this:
\<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)

goal (1 subgoal):
 1. \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
[PROOF STEP]
using hc hd assms subsetD GH_repr.sumsetI imageI
[PROOF STATE]
proof (prove)
using this:
\<phi> x = quot_comp_alt (\<phi> c) (\<phi> d)
c \<in> A
d \<in> B
A \<subseteq> Partition
B \<subseteq> Partition
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
\<lbrakk>?a \<in> ?A; ?a \<in> \<phi> ` Partition; ?b \<in> ?B; ?b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> quot_comp_alt ?a ?b \<in> GH_repr.sumset ?A ?B
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A

goal (1 subgoal):
 1. \<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
assume "x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)"
[PROOF STATE]
proof (state)
this:
x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
[PROOF STEP]
obtain a b where "x = quot_comp_alt a b" and ha: "a \<in> \<phi> ` A" and hb: "b \<in> \<phi> ` B"
[PROOF STATE]
proof (prove)
using this:
x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = quot_comp_alt a b; a \<in> \<phi> ` A; b \<in> \<phi> ` B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GH_repr.sumset.cases
[PROOF STATE]
proof (prove)
using this:
x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B)
\<lbrakk>?a \<in> GH_repr.sumset ?A ?B; \<And>a b. \<lbrakk>?a = quot_comp_alt a b; a \<in> ?A; a \<in> \<phi> ` Partition; b \<in> ?B; b \<in> \<phi> ` Partition\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>x = quot_comp_alt a b; a \<in> \<phi> ` A; b \<in> \<phi> ` B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = quot_comp_alt a b
a \<in> \<phi> ` A
b \<in> \<phi> ` B

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = quot_comp_alt a b
a \<in> \<phi> ` A
b \<in> \<phi> ` B

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
obtain c d where "a = \<phi> c" and "b = \<phi> d" and "c \<in> A" and "d \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>a = \<phi> c; b = \<phi> d; c \<in> A; d \<in> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ha hb
[PROOF STATE]
proof (prove)
using this:
a \<in> \<phi> ` A
b \<in> \<phi> ` B

goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>a = \<phi> c; b = \<phi> d; c \<in> A; d \<in> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = \<phi> c
b = \<phi> d
c \<in> A
d \<in> B

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.sumset (\<phi> ` A) (\<phi> ` B) \<Longrightarrow> x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = quot_comp_alt a b
a \<in> \<phi> ` A
b \<in> \<phi> ` B
a = \<phi> c
b = \<phi> d
c \<in> A
d \<in> B
[PROOF STEP]
show "x \<in> \<phi> ` GH.sumset A B"
[PROOF STATE]
proof (prove)
using this:
x = quot_comp_alt a b
a \<in> \<phi> ` A
b \<in> \<phi> ` B
a = \<phi> c
b = \<phi> d
c \<in> A
d \<in> B

goal (1 subgoal):
 1. x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
using phi_comp_eq assms imageI GH.sumsetI
[PROOF STATE]
proof (prove)
using this:
x = quot_comp_alt a b
a \<in> \<phi> ` A
b \<in> \<phi> ` B
a = \<phi> c
b = \<phi> d
c \<in> A
d \<in> B
\<lbrakk>?a \<in> Partition; ?b \<in> Partition\<rbrakk> \<Longrightarrow> \<phi> (?a [\<cdot>] ?b) = quot_comp_alt (\<phi> ?a) (\<phi> ?b)
A \<subseteq> Partition
B \<subseteq> Partition
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A
\<lbrakk>?a \<in> ?A; ?a \<in> Partition; ?b \<in> ?B; ?b \<in> Partition\<rbrakk> \<Longrightarrow> ?a [\<cdot>] ?b \<in> GH.sumset ?A ?B

goal (1 subgoal):
 1. x \<in> \<phi> ` GH.sumset A B
[PROOF STEP]
by (smt (verit, del_insts) subsetD)
[PROOF STATE]
proof (state)
this:
x \<in> \<phi> ` GH.sumset A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_image_stabilizer_eq:
  assumes "A \<subseteq> G // H"
  shows "\<phi> ` (GH.stabilizer A) = GH_repr.stabilizer (\<phi> ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` GH.stabilizer A = GH_repr.stabilizer (\<phi> ` A)
[PROOF STEP]
proof(intro subset_antisym image_subsetI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> GH.stabilizer A \<Longrightarrow> \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
 2. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> GH.stabilizer A \<Longrightarrow> \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
 2. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
assume "x \<in> GH.stabilizer A"
[PROOF STATE]
proof (state)
this:
x \<in> GH.stabilizer A

goal (2 subgoals):
 1. \<And>x. x \<in> GH.stabilizer A \<Longrightarrow> \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
 2. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> GH.stabilizer A
[PROOF STEP]
have "GH.sumset {x} A = A" and hx: "x \<in> G // H"
[PROOF STATE]
proof (prove)
using this:
x \<in> GH.stabilizer A

goal (1 subgoal):
 1. GH.sumset {x} A = A &&& x \<in> Partition
[PROOF STEP]
using GH.stabilizer_def assms
[PROOF STATE]
proof (prove)
using this:
x \<in> GH.stabilizer A
GH.stabilizer ?S \<equiv> {x \<in> Partition. GH.sumset {x} (?S \<inter> Partition) = ?S \<inter> Partition}
A \<subseteq> Partition

goal (1 subgoal):
 1. GH.sumset {x} A = A &&& x \<in> Partition
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
GH.sumset {x} A = A
x \<in> Partition

goal (2 subgoals):
 1. \<And>x. x \<in> GH.stabilizer A \<Longrightarrow> \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
 2. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GH.sumset {x} A = A
x \<in> Partition
[PROOF STEP]
have "GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A"
[PROOF STATE]
proof (prove)
using this:
GH.sumset {x} A = A
x \<in> Partition

goal (1 subgoal):
 1. GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
using assms phi_image_sumset_eq
[PROOF STATE]
proof (prove)
using this:
GH.sumset {x} A = A
x \<in> Partition
A \<subseteq> Partition
\<lbrakk>?A \<subseteq> Partition; ?B \<subseteq> Partition\<rbrakk> \<Longrightarrow> \<phi> ` GH.sumset ?A ?B = GH_repr.sumset (\<phi> ` ?A) (\<phi> ` ?B)

goal (1 subgoal):
 1. GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
by (metis empty_subsetI insert_subset)
[PROOF STATE]
proof (state)
this:
GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A

goal (2 subgoals):
 1. \<And>x. x \<in> GH.stabilizer A \<Longrightarrow> \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
 2. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
show "\<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)"
[PROOF STATE]
proof (prove)
using this:
GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A

goal (1 subgoal):
 1. \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
[PROOF STEP]
using GH_repr.stabilizer_def assms
[PROOF STATE]
proof (prove)
using this:
GH_repr.sumset (\<phi> ` {x}) (\<phi> ` A) = \<phi> ` A
GH_repr.stabilizer ?S \<equiv> {x \<in> \<phi> ` Partition. GH_repr.sumset {x} (?S \<inter> \<phi> ` Partition) = ?S \<inter> \<phi> ` Partition}
A \<subseteq> Partition

goal (1 subgoal):
 1. \<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)
[PROOF STEP]
by (smt (z3) GH_repr.sumset_Int_carrier hx image_empty image_eqI image_insert mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<phi> x \<in> GH_repr.stabilizer (\<phi> ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
assume "x \<in> GH_repr.stabilizer (\<phi> ` A)"
[PROOF STATE]
proof (state)
this:
x \<in> GH_repr.stabilizer (\<phi> ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> GH_repr.stabilizer (\<phi> ` A)
[PROOF STEP]
have hstab: "GH_repr.sumset {x} (\<phi> ` A) = (\<phi> ` A)" and hx: "x \<in> \<phi> ` (G // H)"
[PROOF STATE]
proof (prove)
using this:
x \<in> GH_repr.stabilizer (\<phi> ` A)

goal (1 subgoal):
 1. GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A &&& x \<in> \<phi> ` Partition
[PROOF STEP]
using GH_repr.stabilizer_def assms phi_image_subset
[PROOF STATE]
proof (prove)
using this:
x \<in> GH_repr.stabilizer (\<phi> ` A)
GH_repr.stabilizer ?S \<equiv> {x \<in> \<phi> ` Partition. GH_repr.sumset {x} (?S \<inter> \<phi> ` Partition) = ?S \<inter> \<phi> ` Partition}
A \<subseteq> Partition
\<phi> ` Partition \<subseteq> G

goal (1 subgoal):
 1. GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A &&& x \<in> \<phi> ` Partition
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A
x \<in> \<phi> ` Partition

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A
x \<in> \<phi> ` Partition
[PROOF STEP]
obtain B where hB: "B \<in> G // H" and hBx: "\<phi> B = x"
[PROOF STATE]
proof (prove)
using this:
GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A
x \<in> \<phi> ` Partition

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

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> Partition
\<phi> B = x
[PROOF STEP]
have "GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A"
[PROOF STATE]
proof (prove)
using this:
B \<in> Partition
\<phi> B = x

goal (1 subgoal):
 1. GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
using hstab
[PROOF STATE]
proof (prove)
using this:
B \<in> Partition
\<phi> B = x
GH_repr.sumset {x} (\<phi> ` A) = \<phi> ` A

goal (1 subgoal):
 1. GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A
[PROOF STEP]
have "GH.sumset {B} A = A"
[PROOF STATE]
proof (prove)
using this:
GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A

goal (1 subgoal):
 1. GH.sumset {B} A = A
[PROOF STEP]
using phi_image_sumset_eq phi_inj_on assms hB
    GH.sumset_subset_carrier
[PROOF STATE]
proof (prove)
using this:
GH_repr.sumset (\<phi> ` {B}) (\<phi> ` A) = \<phi> ` A
\<lbrakk>?A \<subseteq> Partition; ?B \<subseteq> Partition\<rbrakk> \<Longrightarrow> \<phi> ` GH.sumset ?A ?B = GH_repr.sumset (\<phi> ` ?A) (\<phi> ` ?B)
inj_on \<phi> Partition
A \<subseteq> Partition
B \<in> Partition
GH.sumset ?A ?B \<subseteq> Partition

goal (1 subgoal):
 1. GH.sumset {B} A = A
[PROOF STEP]
by (smt (z3) GH.sumset_singletons_eq inj_on_image_eq_iff
    quotient.right_unit quotient.unit_closed)
[PROOF STATE]
proof (state)
this:
GH.sumset {B} A = A

goal (1 subgoal):
 1. \<And>x. x \<in> GH_repr.stabilizer (\<phi> ` A) \<Longrightarrow> x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GH.sumset {B} A = A
[PROOF STEP]
show "x \<in> \<phi> ` (GH.stabilizer A)"
[PROOF STATE]
proof (prove)
using this:
GH.sumset {B} A = A

goal (1 subgoal):
 1. x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
using assms hBx GH.stabilizer_def
[PROOF STATE]
proof (prove)
using this:
GH.sumset {B} A = A
A \<subseteq> Partition
\<phi> B = x
GH.stabilizer ?S \<equiv> {x \<in> Partition. GH.sumset {x} (?S \<inter> Partition) = ?S \<inter> Partition}

goal (1 subgoal):
 1. x \<in> \<phi> ` GH.stabilizer A
[PROOF STEP]
by (smt (z3) GH.sumset_Int_carrier hB image_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
x \<in> \<phi> ` GH.stabilizer A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma residue_group: "abelian_group {0..(m :: nat)-1} (\<lambda> x y. ((x + y) mod m)) (0 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
proof(cases "m > 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
case hm: True
[PROOF STATE]
proof (state)
this:
1 < m

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < m
[PROOF STEP]
have hmonoid: "Group_Theory.monoid {0..m-1} (\<lambda> x y. ((x + y) mod m)) (0 :: int)"
[PROOF STATE]
proof (prove)
using this:
1 < m

goal (1 subgoal):
 1. Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
by (unfold_locales, auto simp add: of_nat_diff, presburger)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
have "monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u" if "u \<in> {0..int (m - 1)}" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
proof(cases "u = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
 2. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = 0

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
 2. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = 0

goal (1 subgoal):
 1. monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
using monoid.invertible_def[OF hmonoid that] monoid.unit_invertible[OF hmonoid]
[PROOF STATE]
proof (prove)
using this:
u = 0
monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u = (\<exists>v\<in>{0..int (m - 1)}. (u + v) mod int m = 0 \<and> (v + u) mod int m = 0)
monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 0

goal (1 subgoal):
 1. monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
case hx: False
[PROOF STATE]
proof (state)
this:
u \<noteq> 0

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
[PROOF STEP]
have "((m - u) + u) mod m = 0" and "(u + (m - u)) mod m = 0" and "m - u \<in> {0..int(m-1)}"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0

goal (1 subgoal):
 1. (int m - u + u) mod int m = 0 &&& (u + (int m - u)) mod int m = 0 &&& int m - u \<in> {0..int (m - 1)}
[PROOF STEP]
using atLeastAtMost_iff hx that
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
u \<noteq> 0
u \<in> {0..int (m - 1)}

goal (1 subgoal):
 1. (int m - u + u) mod int m = 0 &&& (u + (int m - u)) mod int m = 0 &&& int m - u \<in> {0..int (m - 1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(int m - u + u) mod int m = 0
(u + (int m - u)) mod int m = 0
int m - u \<in> {0..int (m - 1)}

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(int m - u + u) mod int m = 0
(u + (int m - u)) mod int m = 0
int m - u \<in> {0..int (m - 1)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(int m - u + u) mod int m = 0
(u + (int m - u)) mod int m = 0
int m - u \<in> {0..int (m - 1)}

goal (1 subgoal):
 1. monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
using monoid.invertible_def[OF hmonoid that]
[PROOF STATE]
proof (prove)
using this:
(int m - u + u) mod int m = 0
(u + (int m - u)) mod int m = 0
int m - u \<in> {0..int (m - 1)}
monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u = (\<exists>v\<in>{0..int (m - 1)}. (u + v) mod int m = 0 \<and> (v + u) mod int m = 0)

goal (1 subgoal):
 1. monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?u \<in> {0..int (m - 1)} \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 ?u

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?u \<in> {0..int (m - 1)} \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 ?u

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
have "commutative_monoid {0..m-1} (\<lambda> x y. ((x + y) mod m)) (0 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. commutative_monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
using hmonoid commutative_monoid_def commutative_monoid_axioms_def
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
commutative_monoid ?M ?composition ?unit \<equiv> Group_Theory.monoid ?M ?composition ?unit \<and> commutative_monoid_axioms ?M ?composition
commutative_monoid_axioms ?M ?composition \<equiv> \<forall>x y. x \<in> ?M \<longrightarrow> y \<in> ?M \<longrightarrow> ?composition x y = ?composition y x

goal (1 subgoal):
 1. commutative_monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
by (smt (verit))
[PROOF STATE]
proof (state)
this:
commutative_monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal (2 subgoals):
 1. 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
 2. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
?u \<in> {0..int (m - 1)} \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 ?u
commutative_monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Group_Theory.monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
?u \<in> {0..int (m - 1)} \<Longrightarrow> monoid.invertible {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0 ?u
commutative_monoid {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal (1 subgoal):
 1. abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
by (simp add: abelian_group_def group_def group_axioms_def
      hmonoid)
[PROOF STATE]
proof (state)
this:
abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
case hm: False
[PROOF STATE]
proof (state)
this:
\<not> 1 < m

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 1 < m

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
have hmonoid: "Group_Theory.monoid {0} (\<lambda> x y. ((x + y) mod m)) (0 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid {0} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
by (unfold_locales, auto)
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid {0} (\<lambda>x y. (x + y) mod int m) 0

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid {0} (\<lambda>x y. (x + y) mod int m) 0

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
have "monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0
[PROOF STEP]
using monoid.invertible_def[OF hmonoid]
    monoid.unit_invertible[OF hmonoid] hm
[PROOF STATE]
proof (prove)
using this:
?u \<in> {0} \<Longrightarrow> monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 ?u = (\<exists>v\<in>{0}. (?u + v) mod int m = 0 \<and> (v + ?u) mod int m = 0)
monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0
\<not> 1 < m

goal (1 subgoal):
 1. monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0

goal (1 subgoal):
 1. \<not> 1 < m \<Longrightarrow> abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> 1 < m
Group_Theory.monoid {0} (\<lambda>x y. (x + y) mod int m) 0
monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < m
Group_Theory.monoid {0} (\<lambda>x y. (x + y) mod int m) 0
monoid.invertible {0} (\<lambda>x y. (x + y) mod int m) 0 0

goal (1 subgoal):
 1. abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0
[PROOF STEP]
by (unfold_locales, auto)
[PROOF STATE]
proof (state)
this:
abelian_group {0..int (m - 1)} (\<lambda>x y. (x + y) mod int m) 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in subgroup_of_group) prime_order_simple:
  assumes "prime (card G)"
  shows "H = {\<one>} \<or> H = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
have "card H dvd card G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H dvd card G
[PROOF STEP]
using lagrange assms card.infinite dvdI not_prime_0
[PROOF STATE]
proof (prove)
using this:
finite G \<Longrightarrow> card G = card H * index
prime (card G)
infinite ?A \<Longrightarrow> card ?A = 0
?a = ?b * ?k \<Longrightarrow> ?b dvd ?a
\<not> prime (0::?'a)

goal (1 subgoal):
 1. card H dvd card G
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card H dvd card G

goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card H dvd card G
[PROOF STEP]
have "card H = 1 \<or> card H = card G"
[PROOF STATE]
proof (prove)
using this:
card H dvd card G

goal (1 subgoal):
 1. card H = 1 \<or> card H = card G
[PROOF STEP]
using assms prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
card H dvd card G
prime (card G)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. card H = 1 \<or> card H = card G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card H = 1 \<or> card H = card G

goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card H = 1 \<or> card H = card G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card H = 1 \<or> card H = card G

goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
using card_1_singletonE sub_unit_closed card.infinite card_subset_eq sub
    assms not_prime_0 subsetI insertE empty_iff
[PROOF STATE]
proof (prove)
using this:
card H = 1 \<or> card H = card G
\<lbrakk>card ?A = 1; \<And>x. ?A = {x} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<one> \<in> H
infinite ?A \<Longrightarrow> card ?A = 0
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> ?A = ?B
?a \<in> H \<Longrightarrow> ?a \<in> G
prime (card G)
\<not> prime (0::?'a)
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
\<lbrakk>?a \<in> insert ?b ?A; ?a = ?b \<Longrightarrow> ?P; ?a \<in> ?A \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(?c \<in> {}) = False

goal (1 subgoal):
 1. H = {\<one>} \<or> H = G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
H = {\<one>} \<or> H = G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma residue_group_simple:
  assumes "prime p" and "subgroup H {0..(p :: nat)-1} (\<lambda> x y. ((x + y) mod p)) (0 :: int)"
  shows "H = {0} \<or> H = {0..int(p-1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
have hprime: "prime (card {0..int(p-1)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (card {0..int (p - 1)})
[PROOF STEP]
using card_atLeastAtMost_int assms int_ops
[PROOF STATE]
proof (prove)
using this:
card {?l..?u} = nat (?u - ?l + 1)
prime p
subgroup H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
int 0 = 0
int 1 = 1
int (numeral ?n) = numeral ?n
int (Suc ?a) = int ?a + 1
int (?a + ?b) = int ?a + int ?b
int (?a - ?b) = (if int ?a < int ?b then 0 else int ?a - int ?b)
int (?a * ?b) = int ?a * int ?b
int (?a div ?b) = int ?a div int ?b
int (?a mod ?b) = int ?a mod int ?b

goal (1 subgoal):
 1. prime (card {0..int (p - 1)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime (card {0..int (p - 1)})

goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime (card {0..int (p - 1)})

goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
have hsub:"subgroup_of_group H {0..(p :: nat)-1} (\<lambda> x y. ((x + y) mod p)) (0 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
[PROOF STEP]
using subgroup_of_group_def assms abelian_group_def residue_group
[PROOF STATE]
proof (prove)
using this:
subgroup_of_group ?H ?G ?composition ?unit \<equiv> subgroup ?H ?G ?composition ?unit \<and> Group_Theory.group ?G ?composition ?unit
prime p
subgroup H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
abelian_group ?G ?composition ?unit \<equiv> Group_Theory.group ?G ?composition ?unit \<and> commutative_monoid ?G ?composition ?unit
abelian_group {0..int (?m - 1)} (\<lambda>x y. (x + y) mod int ?m) 0

goal (1 subgoal):
 1. subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0

goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime (card {0..int (p - 1)})
subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime (card {0..int (p - 1)})
subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0

goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
using assms subgroup_of_group.prime_order_simple[OF hsub hprime]
[PROOF STATE]
proof (prove)
using this:
prime (card {0..int (p - 1)})
subgroup_of_group H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
prime p
subgroup H {0..int (p - 1)} (\<lambda>x y. (x + y) mod int p) 0
H = {0} \<or> H = {0..int (p - 1)}

goal (1 subgoal):
 1. H = {0} \<or> H = {0..int (p - 1)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H = {0} \<or> H = {0..int (p - 1)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "monitor \<phi>\<^sub>e\<^sub>x \<pi>\<^sub>e\<^sub>x = {(0, [Some ''e''])}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monitor.monitor \<phi>\<^sub>e\<^sub>x \<pi>\<^sub>e\<^sub>x = {(0, [Some ''e''])}
[PROOF STEP]
by eval


[STATEMENT]
lemma "fst m1 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst m1 = {}
[PROOF STEP]
by eval


[STATEMENT]
lemma "fst m2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst m2 = {}
[PROOF STEP]
by eval


[STATEMENT]
lemma "fst m3 = {(0, [Some ''e''])}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst m3 = {(0, [Some ''e''])}
[PROOF STEP]
by eval


[STATEMENT]
lemma "minit \<phi>\<^sub>e\<^sub>x = \<lparr>
  mstate_i = 0,
  mstate_m =
    MAnd (MPred ''A'' [MFOTL.Var 0]) False
     (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
       ([], []) [] [])
     ([], []),
  mstate_n = 1\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minit \<phi>\<^sub>e\<^sub>x = \<lparr>mstate_i = 0, mstate_m = MAnd (MPred ''A'' [trm.Var 0]) False (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [trm.Var 1, trm.Var 0])) ([], []) [] []) ([], []), mstate_n = 1\<rparr>
[PROOF STEP]
by eval


[STATEMENT]
lemma "mstate_m (snd m1) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
    ([], []) [] [(1, {[None]}, {})])
  ([{[Some ''d''], [Some ''e'']}], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mstate_m (snd m1) = MAnd (MPred ''A'' [trm.Var 0]) False (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [trm.Var 1, trm.Var 0])) ([], []) [] [(1, {[None]}, {})]) ([{[Some ''d''], [Some ''e'']}], [])
[PROOF STEP]
by eval


[STATEMENT]
lemma "mstate_m (snd m2) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
   ([], []) [] [(1, {[None]}, {[Some ''d'']}), (2, {[None]}, {})])
  ([{[Some ''d''], [Some ''e'']}, {}], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mstate_m (snd m2) = MAnd (MPred ''A'' [trm.Var 0]) False (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [trm.Var 1, trm.Var 0])) ([], []) [] [(1, {[None]}, {[Some ''d'']}), (2, {[None]}, {})]) ([{[Some ''d''], [Some ''e'']}, {}], [])
[PROOF STEP]
by eval


[STATEMENT]
lemma "mstate_m (snd m3) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
    ([], []) [] [(5, {[None]}, {})])
  ([{}], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mstate_m (snd m3) = MAnd (MPred ''A'' [trm.Var 0]) False (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [trm.Var 1, trm.Var 0])) ([], []) [] [(5, {[None]}, {})]) ([{}], [])
[PROOF STEP]
by eval


[STATEMENT]
lemma Ball_subset_right:
  assumes "T \<subseteq> S" "\<forall>x\<in>S-T. P x"
  shows   "(\<forall>x\<in>S. P x) = (\<forall>x\<in>T. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>S. P x) = (\<forall>x\<in>T. P x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> S
\<forall>x\<in>S - T. P x

goal (1 subgoal):
 1. (\<forall>x\<in>S. P x) = (\<forall>x\<in>T. P x)
[PROOF STEP]
by auto