[STATEMENT]
lemma (in group) prime_order_simple:
  assumes prime:"prime (order G)"
  shows "simple_group G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_group G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < order G
 2. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from prime
[PROOF STATE]
proof (chain)
picking this:
prime (order G)
[PROOF STEP]
show "1 < order G"
[PROOF STATE]
proof (prove)
using this:
prime (order G)

goal (1 subgoal):
 1. 1 < order G
[PROOF STEP]
unfolding prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < order G \<and> (\<forall>m. m dvd order G \<longrightarrow> m = 1 \<or> m = order G)

goal (1 subgoal):
 1. 1 < order G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < order G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "H \<lhd> G"
[PROOF STATE]
proof (state)
this:
H \<lhd> G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence HG:"subgroup H G"
[PROOF STATE]
proof (prove)
using this:
H \<lhd> G

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
unfolding normal_def
[PROOF STATE]
proof (prove)
using this:
subgroup H G \<and> Group.group G \<and> normal_axioms H G

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subgroup H G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence "card H dvd order G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

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

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

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

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

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
thus "H = carrier G \<or> H = {\<one>}"
[PROOF STATE]
proof (prove)
using this:
card H = 1 \<or> card H = order G

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "card H = 1"
[PROOF STATE]
proof (state)
this:
card H = 1

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card H = 1

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from HG
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
have "\<one> \<in> H"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. \<one> \<in> H
[PROOF STEP]
by (metis subgroup.one_closed)
[PROOF STATE]
proof (state)
this:
\<one> \<in> H

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card H = 1
\<one> \<in> H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card H = 1
\<one> \<in> H

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

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "card H = order G"
[PROOF STATE]
proof (state)
this:
card H = order G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card H = order G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from HG
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
have "H \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
unfolding subgroup_def
[PROOF STATE]
proof (prove)
using this:
(H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes> y \<in> H)) \<and> \<one> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv x \<in> H)

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

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

goal (1 subgoal):
 1. 1 < card (carrier G)
[PROOF STEP]
unfolding order_def prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < card (carrier G) \<and> (\<forall>m. m dvd card (carrier G) \<longrightarrow> m = 1 \<or> m = card (carrier G))

goal (1 subgoal):
 1. 1 < card (carrier G)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
1 < card (carrier G)

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence "finite (carrier G)"
[PROOF STATE]
proof (prove)
using this:
1 < card (carrier G)

goal (1 subgoal):
 1. finite (carrier G)
[PROOF STEP]
by (auto simp:card_ge_0_finite)
[PROOF STATE]
proof (state)
this:
finite (carrier G)

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

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card H = card (carrier G)
H \<subseteq> carrier G
finite (carrier G)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
H = carrier G \<or> H = {\<one>}

goal:
No subgoals!
[PROOF STEP]
qed