# Theory Tetrahedron

```chapter "Rotational Symmetries of the Tetrahedron"

theory Tetrahedron
imports Orbit_Stabiliser
begin

section "Definition of the Tetrahedron and its Rotations"

text ‹
In this section we will use the orbit-stabiliser theorem to count the number of rotational symmetries
of a tetrahedron.

The tetrahedron will be defined as a set of four vertices, labelled A, B, C, and D. A rotation
is defined as a function between the vertices.
›

datatype Vertex = A | B | C | D
definition vertices :: "Vertex set" where
"vertices = {A, B, C, D}"

type_synonym Rotation = "(Vertex ⇒ Vertex)"

text ‹
We define four primitive rotations explicitly. The axis of each rotation is the line through a vertex
that is perpendicular to the face opposite to the vertex. Every rotation is by 120 degrees counter clockwise.

We also define the identity as a possible rotation.
›

definition rotate_A :: Rotation where
"rotate_A = (λv. (case v of A ⇒ A | B ⇒ C | C ⇒ D | D ⇒ B))"
definition rotate_B :: Rotation where
"rotate_B = (λv. (case v of A ⇒ D | B ⇒ B | C ⇒ A | D ⇒ C))"
definition rotate_C :: Rotation where
"rotate_C = (λv. (case v of A ⇒ B | B ⇒ D | C ⇒ C | D ⇒ A))"
definition rotate_D :: Rotation where
"rotate_D = (λv. (case v of A ⇒ C | B ⇒ A | C ⇒ B | D ⇒ D))"

named_theorems simple_rotations
declare rotate_A_def [simple_rotations] rotate_B_def [simple_rotations] rotate_C_def [simple_rotations] rotate_D_def [simple_rotations]

definition simple_rotations :: "Rotation set" where
"simple_rotations = {id, rotate_A, rotate_B, rotate_C, rotate_D}"

text ‹
All other rotations are combinations of the previously defined simple rotations. We define these
inductively.
›
inductive_set complex_rotations :: "Rotation set" where
simp: "r ∈ simple_rotations ⟹ r ∈ complex_rotations" |
comp: "r ∈ simple_rotations ⟹ s ∈ complex_rotations ⟹ (r ∘ s) ∈ complex_rotations"

section "Properties of Rotations"

text ‹
In this section we prove some basic properties of rotations that will be useful later.
We begin by showing that rotations are bijections.
›

lemma simple_rotations_inj:
assumes r:"r ∈ simple_rotations"
shows "inj r"
using r unfolding simple_rotations_def
by safe
(rule injI; rename_tac a b; case_tac a; case_tac b;
)+

lemma simple_rotations_surj:
assumes r:"r ∈ simple_rotations"
shows "surj r"
using r unfolding simple_rotations_def
by safe
(rename_tac a; case_tac a;
)+

lemma simple_rotations_bij:
assumes r:"r ∈ simple_rotations"
shows "bij r"
by (simp add: r bij_def simple_rotations_surj simple_rotations_inj)

lemma complex_rotations_bij: "r ∈ complex_rotations ⟹ bij r"
proof(induction r rule: complex_rotations.induct)
case (simp r) then show ?case using simple_rotations_bij by simp
next
case (comp r s) then show ?case using bij_comp simple_rotations_bij by blast
qed

lemma simple_rotation_bij_corollary: "r ∈ simple_rotations ⟹ r x ≠ r y ⟷ x ≠ y"
using bij_def simple_rotations_bij inj_eq by metis

lemma rotation_bij_corollary: "r ∈ complex_rotations ⟹ r x ≠ r y ⟷ x ≠ y"
using bij_def complex_rotations_bij inj_eq by metis

lemma complex_rotations_comp:
"r ∈ complex_rotations ⟹ s ∈ complex_rotations ⟹ (r ∘ s) ∈ complex_rotations"
apply(induction arbitrary: s rule: complex_rotations.induct)
done

text ‹
Next, we show that simple rotations (except the identity) keep exactly one vertex fixed.
›

lemma simple_rotations_fix:
assumes r:"r ∈ simple_rotations"
shows "∃v. r v = v"
using r unfolding simple_rotations_def
by (auto simp add: simple_rotations split: Vertex.split)

lemma simple_rotations_fix_unique:
assumes r:"r ∈ simple_rotations"
shows "r ≠ id ⟹ r v = v ⟹ r w = w ⟹ v = w"
using r unfolding simple_rotations_def
by safe
(case_tac v; case_tac w;
)+

text ‹
We also show that simple rotations do not contain cycles of length 2.
›

lemma simple_rotations_cycle:
assumes r:"r ∈ simple_rotations"
shows "r ≠ id ⟹ r v = w ⟹ v ≠ w ⟹ r w ≠ v"
using r unfolding simple_rotations_def
by safe
(case_tac v;
)+

text ‹
The following lemmas are all variations on the fact that any property that holds for 4 distinct
vertices holds for all vertices. This is necessary to avoid having to use Vertex.exhaust as much
as possible.
›

lemma distinct_vertices: "distinct[(a::Vertex),b,c,d] ⟹ (∀ e. e ∈ {a,b,c,d})"
apply(safe)
apply(case_tac a)
apply(metis Vertex.exhaust)+
done

lemma distinct_map: "r ∈ complex_rotations ⟹ distinct[a,b,c,d] ⟹ (∀ e ∈ {a,b,c}. r e ≠ f) ⟹ r d = f"
proof -
assume r:"r ∈ complex_rotations" and dist:"distinct [a,b,c,d]" and notf:"∀ e ∈ {a,b,c}. r e ≠ f"
then have 1:"(∀ v. v ∈ {a,b,c,d})" using distinct_vertices by simp
from complex_rotations_bij have "∃ v. r v = f" using r bij_pointE by metis
then have "∃ v ∈ {a,b,c,d}. r v = f" using 1 by blast
then show "r d = f" using notf by simp
qed

lemma distinct_map': "r ∈ complex_rotations ⟹ distinct[a,b,c,d] ⟹ (∀ e ∈ {a,b,c}. r f ≠ e) ⟹ r f = d"
proof -
assume r:"r ∈ complex_rotations" and dist:"distinct [a,b,c,d]" and notf:"∀ e ∈ {a,b,c}. r f ≠ e"
then have 1:"(∀ v. v ∈ {a,b,c,d})" using distinct_vertices by simp
have "∃ v. r f = v" by simp
then have "∃ v ∈ {a,b,c,d}. r f = v" using 1 by blast
then show "r f = d" using notf by simp
qed

lemma cycle_map: "r ∈ complex_rotations ⟹ distinct[a,b,c,d] ⟹
r a = b ⟹ r b = a ⟹ r c = d ⟹ r d = c ⟹ ∀ v w. r v = w ⟶ r w = v"
using distinct_map' rotation_bij_corollary by fastforce

lemma simple_distinct_map: "r ∈ simple_rotations ⟹ distinct[a,b,c,d] ⟹ (∀ e ∈ {a,b,c}. r e ≠ f) ⟹ r d = f"
using complex_rotations.simp distinct_map by simp

lemma simple_distinct_map': "r ∈ simple_rotations ⟹ distinct[a,b,c,d] ⟹ (∀ e ∈ {a,b,c}. r f ≠ e) ⟹ r f = d"
using complex_rotations.simp distinct_map' by simp

lemma simple_distinct_ident: "r ∈ simple_rotations ⟹ distinct[a,b,c,d] ⟹ (∀ e ∈ {a,b,c}. r e ≠ e) ⟹ r d = d"
using simple_rotations_fix simple_distinct_map' by metis

lemma id_decomp:
assumes distinct:"distinct [(a::Vertex),b,c,d]" and ident:"(∀ x ∈ {a,b,c,d}. r x = x)"
shows "r = id"
proof -
from distinct_vertices have "∀ e. e ∈ set [a,b,c,d]" using distinct by simp
then have "∀ e. r e = e" using ident by auto
then show "r = id" by auto
qed

text ‹
Here we show that two invariants hold for rotations. Firstly, any rotation that does not fix a vertex consists
of 2-cycles. Secondly, the only rotation that fixes more than one vertex is the identity.

This proof is very long in part because both invariants have to be proved simultaneously because
they depend on each other.
›

lemma complex_rotations_invariants:
"r ∈ complex_rotations ⟹ (((∀ v. r v ≠ v) ⟶ r v = w ⟶ r w = v) ∧ (r v = v ⟶ r w = w ⟶ v ≠ w ⟶ r = id)) "
proof(induction r arbitrary: v w rule: complex_rotations.induct)
case (simp r)
assume r:"r ∈ simple_rotations"
show ?case
proof
have "∃ v. r v = v" using simple_rotations_fix r by simp
then have "¬ (∀ v. r v ≠ v)" by simp
then show "(∀ v. r v ≠ v) ⟶ r v = w ⟶ r w = v" by blast

show "r v = v ⟶ r w = w ⟶ v ≠ w ⟶ r = id" using simple_rotations_fix_unique simp by blast
qed
next
case (comp r s)
assume r:"r ∈ simple_rotations"
assume s:"s ∈ complex_rotations"
have fix_unique:"∀ v w. s v = v ⟶ s w = w ⟶ v ≠ w ⟶ s = id" using comp by blast
show ?case
proof
show "(∀x. (r ∘ s) x ≠ x) ⟶ (r ∘ s) v = w ⟶ (r ∘ s) w = v"
proof (rule impI)+
assume nofixrs:"∀ x.(r ∘ s) x ≠ x"
assume "(r ∘ s) v = w"
show "(r ∘ s) w = v"
proof (cases "∀ x. s x ≠ x")
assume nofixs:"∀ x. s x ≠ x"
then have cycle:"∀ x y. (s x = y ⟶ s y = x)" using comp.IH by blast
then show ?thesis
proof (cases "r = id")
assume id:"r = id"
then have "s v = w" using  ‹(r ∘ s) v = w› by simp
then have "s w = v" using cycle by blast
then show "(r ∘ s) w = v" using id by simp
next
assume notid:"r ≠ id"
obtain a where "s v = a" and "s a = v" and "a ≠ v" using comp.IH nofixs by blast
obtain b where "s w = b" and "s b = w" and "b ≠ w" using comp.IH nofixs by blast
have "v ≠ w" using ‹(r ∘ s) v = w› nofixrs by blast
then have "a ≠ b" using comp.hyps rotation_bij_corollary ‹s a = v› ‹s b = w› by auto
have "r a = w" using ‹s v = a› ‹(r ∘ s) v = w› by auto
then show ?thesis
proof (cases "a = w")
assume "a = w"
then have "r a = a" using ‹r a = w› by simp
then have "s v = w" using ‹a = w› ‹s v = a› by simp
then have "b = v" using ‹s b = w› rotation_bij_corollary comp.hyps by blast
then have "s w = v" using ‹s w = b› by simp
then have "r v ≠ v" using simple_rotations_fix_unique notid ‹r a = a› ‹a ≠ v›
comp.hyps(1) by auto
obtain c d where "s c = d" and "c ≠ v" and "c ≠ w"
using ‹a ≠ v› ‹r a = w› ‹r v ≠ v› comp.hyps(1) simple_rotation_bij_corollary by blast
then have "d ≠ v" and "d ≠ w"
using ‹s w = v› ‹c ≠ v› ‹s c = d› ‹s v = w› comp.hyps(2) rotation_bij_corollary by auto
then have "s d = c" using ‹s c = d› comp.IH nofixs by blast
then have "c ≠ d" using nofixs by auto
then show ?thesis
proof(cases "r v = c")
assume "r v = c"
then have "r c ≠ v" using ‹c ≠ v› simple_rotations_cycle comp.hyps(1) notid by simp
have "r c ≠ w"
using ‹r a = a› ‹c ≠ w› ‹r a = w› simple_rotation_bij_corollary comp.hyps(1) by auto
have "r c ≠ c" using ‹a = w› ‹c ≠ w› ‹r a = a›
comp.hyps(1) simple_rotations_fix_unique notid by blast
have dist:"distinct [v,w,c,d]" using ‹c ≠ v› ‹c ≠ w› ‹c ≠ d› ‹d ≠ v› ‹d ≠ w› ‹v ≠ w› by simp
then have "∀ v ∈ {v,w,c}. r c ≠ v" using ‹r c ≠ c› ‹r c ≠ v› ‹r c ≠ w› by auto
then have "r c = d" using simple_distinct_map' comp.hyps(1) dist by auto
then have "(r ∘ s) d = d" using ‹s d = c› by simp
then have False using nofixrs by blast
then show ?thesis by simp
next
assume "r v ≠ c"
then have "r v ≠ w"
using ‹r a = a› ‹v ≠ w› ‹r a = w› simple_rotation_bij_corollary comp.hyps(1) by auto
then have "r v ≠ v" using ‹a = w› ‹r a = a›
comp.hyps(1) simple_rotations_fix_unique notid by blast
have dist:"distinct [w,c,v,d]" using ‹c ≠ v› ‹c ≠ w› ‹c ≠ d› ‹d ≠ v› ‹d ≠ w› ‹v ≠ w› by simp
then have "∀ x ∈ {w,c,v}. r v ≠ x" using ‹r v ≠ c› ‹r v ≠ v› ‹r v ≠ w› by auto
then have "r v = d" using simple_distinct_map' comp.hyps(1) dist by auto
then have "r d ≠ v" using ‹d ≠ v› simple_rotations_cycle comp.hyps(1) notid by simp
have "r d ≠ w"
using ‹r a = a› ‹d ≠ w› ‹r a = w› simple_rotation_bij_corollary comp.hyps(1) by auto
have "r d ≠ d" using ‹a = w› ‹d ≠ w› ‹r a = a›
comp.hyps(1) simple_rotations_fix_unique notid by blast
have dist':"distinct [w,v,d,c]" using ‹c ≠ v› ‹c ≠ w› ‹c ≠ d› ‹d ≠ v› ‹d ≠ w› ‹v ≠ w› by simp
then have "∀ v ∈ {w,v,d}. r d ≠ v" using ‹r d ≠ d› ‹r d ≠ w› ‹r d ≠ v› by auto
then have "r d = c" using simple_distinct_map' comp.hyps(1) dist' by auto
then have "(r ∘ s) c = c" using ‹s c = d› by simp
then have False using nofixrs by blast
then show ?thesis by simp
qed
next
assume "a ≠ w"
then have "r a ≠ a" using ‹r a = w› by simp
have "b ≠ v" using ‹a ≠ w› ‹s b = w› ‹s v = a› by auto
have "r w ≠ w" using ‹a ≠ w› ‹r a = w› comp.hyps(1) simple_rotation_bij_corollary by auto
from nofixs have "s w ≠ w" by simp
then have "r v ≠ w" using ‹a ≠ v› ‹r a = w› comp.hyps simple_rotation_bij_corollary by blast
have "s v ≠ w" using ‹r a = w› ‹r a ≠ a› ‹s v = a› by blast
then show ?thesis
proof (cases "r b = b")
assume "r b = b"
then have "r b ≠ a" using ‹a ≠ b› by simp
have "r w ≠ a" using ‹r a = w› ‹r w ≠ w› comp.hyps(1) notid simple_rotations_cycle by blast
have dist:"distinct [a,b,w,v]" using ‹a ≠ w› ‹a ≠ b› ‹a ≠ v› ‹b ≠ w› ‹b ≠ v› ‹v ≠ w› by simp
then have "∀ x ∈ {a,b,w}. r x ≠ a" using ‹r a ≠ a› ‹r b ≠ a› ‹r w ≠ a› by auto
then have "r v = a" using simple_distinct_map comp.hyps(1) dist by auto
then show ?thesis using ‹s a = v› nofixrs comp_apply by metis
next
assume "r b ≠ b"
have dist:"distinct [w,a,b,v]" using ‹a ≠ w› ‹a ≠ b› ‹a ≠ v› ‹b ≠ w› ‹b ≠ v› ‹v ≠ w› by simp
then have "∀ x ∈ {w,a,b}. r x ≠ x" using ‹r w ≠ w› ‹r a ≠ a› ‹r b ≠ b› by auto
then have "r v = v" using simple_distinct_ident comp.hyps(1) dist by auto
have "r w ≠ a" using ‹a ≠ w› simple_rotations_cycle comp.hyps(1) notid ‹r a = w› by simp
have "r w ≠ v" using ‹r v = v› ‹v ≠ w› comp.hyps(1) simple_rotation_bij_corollary by blast
have dist':"distinct [a,v,w,b]" using ‹a ≠ w› ‹a ≠ b› ‹a ≠ v› ‹b ≠ w› ‹b ≠ v› ‹v ≠ w› by simp
then have "∀ x ∈ {a,v,w}. r w ≠ x" using ‹r w ≠ a› ‹r w ≠ v› ‹r w ≠ w› by auto
then have "r w = b" using simple_distinct_map' comp.hyps(1) dist' by auto
then show ?thesis using ‹s b = w› nofixrs comp_apply by metis
qed
qed
qed
next
assume "¬ (∀ v. s v ≠ v)"
then have fix1:"∃ v. s v = v" by blast
then obtain a where a:"s a = a" by blast
then show ?thesis
proof (cases "r = id")
assume id:"r = id"
then have "(r ∘ s) a = a" using a by simp
then have False using nofixrs by auto
then show ?thesis by simp
next
assume notid: "r ≠ id"
then have fix1:"∃ v. r v = v" using simple_rotations_fix comp.hyps by simp
then obtain b where b:"r b = b" by blast
then show ?thesis
proof (cases "a = b")
assume "a = b"
then have "(r ∘ s) a = a" using a b by simp
then have False using nofixrs by blast
then show ?thesis by simp
next
assume "a ≠ b"
have "r a ≠ a" using ‹a ≠ b› b comp.hyps(1) notid simple_rotations_fix_unique by blast
have "r a ≠ b" using ‹a ≠ b› b comp.hyps(1) simple_rotation_bij_corollary by auto
then obtain c where "r a = c" and "a ≠ c" and "b ≠ c" using ‹r a ≠ a› by auto
have "s b ≠ a" using ‹a ≠ b› a comp.hyps(2) rotation_bij_corollary by blast
have "s b ≠ b" using b nofixrs comp_apply by metis
then obtain d where "s b = d" and "a ≠ d" and "b ≠ d" using ‹s b ≠ a› by auto
have "r c ≠ a" using simple_rotations_cycle ‹a ≠ c› ‹r a = c› comp.hyps(1) notid by blast
have "r c ≠ b" using ‹b ≠ c› b comp.hyps(1) simple_rotation_bij_corollary by blast
have "r c ≠ c" using ‹b ≠ c› b comp.hyps(1) notid simple_rotations_fix_unique by blast
then show ?thesis
proof (cases "c = d")
assume "c = d"
then have "s c ≠ c" using ‹b ≠ c› ‹s b = d› rotation_bij_corollary s by auto
obtain e where "r c = e" and "a ≠ e" and "b ≠ e" and "c ≠ e" and "d ≠ e"
using ‹r c ≠ a› ‹r c ≠ b› ‹r c ≠ c› ‹c = d› by auto
have "r e ≠ b" using ‹b ≠ e› b r simple_rotation_bij_corollary by blast
have "r e ≠ c" using ‹a ≠ e› ‹r a = c› r simple_rotation_bij_corollary by blast
have "r e ≠ e" using ‹b ≠ e› b notid r simple_rotations_fix_unique by blast
then have dist:"distinct [b,c,e,a]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ e› ‹b ≠ c› ‹b ≠ e› ‹c ≠ e› by simp
then have "∀ x ∈ {b,c,e}. r e ≠ x" using ‹r e ≠ b› ‹r e ≠ c› ‹r e ≠ e› by auto
then have "r e = a" using simple_distinct_map' comp.hyps(1) dist by auto
have dist:"distinct [a,b,c,e]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ e› ‹b ≠ c› ‹b ≠ e› ‹c ≠ e› by simp
then have "∀ x ∈ {a,b,c}. r c ≠ x" using ‹r c ≠ a› ‹r c ≠ b› ‹r c ≠ c› by auto
then have "r c = e" using simple_distinct_map' comp.hyps(1) dist by auto
have "s e ≠ a" using ‹a ≠ e› a rotation_bij_corollary s by blast
have "s e ≠ c" using ‹b ≠ e› ‹c = d› ‹s b = d› rotation_bij_corollary s by blast
have "s e ≠ e" using ‹a ≠ e› ‹s b ≠ b› a fix_unique by fastforce
then have dist:"distinct [a,c,e,b]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ e› ‹b ≠ c› ‹b ≠ e› ‹c ≠ e› by simp
then have "∀ x ∈ {a,c,e}. s e ≠ x" using ‹s e ≠ a› ‹s e ≠ c› ‹s e ≠ e› by auto
then have "s e = b" using distinct_map' comp.hyps(2) dist by auto
have "s c ≠ a" using ‹a ≠ c› a rotation_bij_corollary s by blast
have "s c ≠ b" using ‹c ≠ e› ‹s e = b› rotation_bij_corollary s by blast
then have dist:"distinct [a,b,c,e]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ e› ‹b ≠ c› ‹b ≠ e› ‹c ≠ e› by simp
then have "∀ x ∈ {a,b,c}. s c ≠ x" using ‹s c ≠ a› ‹s c ≠ b› ‹s c ≠ c› by auto
then have "s c = e" using distinct_map' comp.hyps(2) dist by auto

have rsa:"(r ∘ s) a = c" using  ‹r a = c› a by simp
have rsb:"(r ∘ s) b = e" using ‹c = d› ‹r c = e› ‹s b = d› by auto
have rsc:"(r ∘ s) c = a" using ‹r e = a› ‹s c = e› by auto
have rse:"(r ∘ s) e = b" using ‹s e = b› b by simp
then have dist:"distinct [a,c,b,e]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ e› ‹b ≠ c› ‹b ≠ e› ‹c ≠ e› by simp
have comprs:"r ∘ s ∈ complex_rotations" using complex_rotations.comp r s by simp
show ?thesis using cycle_map[OF comprs dist rsa rsc rsb rse] ‹(r ∘ s) v = w› by blast
next
assume "c ≠ d"
then have dist:"distinct [a,b,c,d]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ d› ‹b ≠ c› ‹b ≠ d› ‹c ≠ d› by simp
then have "∀ x ∈ {a,b,c}. r c ≠ x" using ‹r c ≠ a› ‹r c ≠ b› ‹r c ≠ c› by auto
then have "r c = d" using simple_distinct_map' comp.hyps(1) dist by auto
have "r d ≠ b" using ‹b ≠ d› b comp.hyps(1) simple_rotation_bij_corollary by blast
have "r d ≠ c" using ‹c ≠ d› ‹r c = d› comp.hyps(1) notid simple_rotations_cycle by blast
have "r d ≠ d" using ‹c ≠ d› ‹r c = d› comp.hyps(1) simple_rotation_bij_corollary by auto
have dist:"distinct [b,c,d,a]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ d› ‹b ≠ c› ‹b ≠ d› ‹c ≠ d› by simp
then have "∀ x ∈ {b,c,d}. r d ≠ x" using ‹r d ≠ b› ‹r d ≠ c› ‹r d ≠ d› by auto
then have "r d = a" using simple_distinct_map' comp.hyps(1) dist by auto
have "s d ≠ a" using ‹a ≠ d› a comp.hyps(2) rotation_bij_corollary by blast
have "s d ≠ c" using nofixrs ‹r c = d› ‹c ≠ d› comp_apply by metis
have "s d ≠ d" using ‹b ≠ d› ‹s b = d› comp.hyps(2) rotation_bij_corollary by auto
have dist:"distinct [a,c,d,b]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ d› ‹b ≠ c› ‹b ≠ d› ‹c ≠ d› by simp
then have "∀ x ∈ {a,c,d}. s d ≠ x" using ‹s d ≠ a› ‹s d ≠ c› ‹s d ≠ d› by auto
then have "s d = b" using distinct_map' comp.hyps(2) dist by auto
have "s c ≠ a" using ‹a ≠ c› a comp.hyps(2) rotation_bij_corollary by blast
have "s c ≠ b" using ‹c ≠ d› ‹s d = b› comp.hyps(2) rotation_bij_corollary by blast
have "s c ≠ d" using ‹b ≠ c› ‹s b = d› comp.hyps(2) rotation_bij_corollary by blast
have dist:"distinct [a,b,d,c]" using ‹a ≠ b› ‹a ≠ c› ‹a ≠ d› ‹b ≠ c› ‹b ≠ d› ‹c ≠ d› by simp
then have "∀ x ∈ {a,b,d}. s c ≠ x" using ‹s c ≠ a› ‹s c ≠ b› ‹s c ≠ d› by auto
then have "s c = c" using distinct_map' comp.hyps(2) dist by auto
then have False using fix_unique ‹s d ≠ d› ‹a ≠ c› a by fastforce
then show ?thesis by simp
qed
qed
qed
qed
qed
next
show "(r ∘ s) v = v ⟶ (r ∘ s) w = w ⟶ v ≠ w ⟶ r ∘ s = id"
proof(rule impI)+
assume rsv:"(r ∘ s) v = v" and rsw:"(r ∘ s) w = w" and "v ≠ w"
show "r ∘ s = id"
proof(cases "s = id")
assume sid:"s = id"
then have "s v = v" and "s w = w" by auto
then have "r = id" using simple_rotations_fix_unique rsv rsw ‹v ≠ w› r  by auto
with sid show ?thesis by simp
next
assume snotid:"s ≠ id"
then show ?thesis
proof(cases "r = id")
assume rid:"r = id"
then have "s v = v" and "s w = w" using rsv rsw by auto
then have "s = id" using ‹v ≠ w› fix_unique by blast
with rid show ?thesis by simp
next
assume rnotid:"r ≠ id"
from simple_rotations_fix_unique[OF comp.hyps(1) rnotid] have
r_fix_forall:"∀v w. r v = v ∧ r w = w ⟶ v = w" by blast
from comp.IH snotid have
s_fix_forall:"∀v w. s v = v ∧ s w = w ⟶ v = w" by blast
have fixes_two: "∃a b. (r ∘ s) a = a ∧ (r ∘ s) b = b ∧ a ≠ b" using ‹v ≠ w› rsv rsw by blast
then show ?thesis
proof (cases "∀ x. s x ≠ x")
assume sfix':"∀ x. s x ≠ x"
from simple_rotations_fix obtain a where a:"r a = a" using r by blast
from sfix' have "s a ≠ a" by blast
then have "(r ∘ s) a ≠ a" using a simple_rotation_bij_corollary r by fastforce
with fixes_two obtain b where "(r ∘ s) b = b" and "b ≠ a" by blast
with fixes_two obtain c where "(r ∘ s) c = c" and "c ≠ a" and "c ≠ b"
using ‹(r ∘ s) a ≠ a› by blast

have "s b ≠ a" using a ‹(r ∘ s) b = b› sfix' by force
have "s c ≠ a" using a ‹(r ∘ s) c = c› sfix' by force

then obtain d where "s d = a" and "d ≠ a" and "d ≠ b" and "d ≠ c"
using ‹s a ≠ a› ‹s b ≠ a› ‹s c ≠ a› complex_rotations_bij s bij_pointE by metis
have "(r ∘ s) d = a" using a ‹s d = a› by simp

have "r b ≠ a" using a r simple_rotation_bij_corollary ‹b ≠ a› by auto
have "r c ≠ a" using a r simple_rotation_bij_corollary ‹c ≠ a› by auto
have "r d ≠ a" using a r simple_rotation_bij_corollary ‹d ≠ a› by auto
have "r b ≠ b" using a r simple_rotations_fix_unique rnotid ‹b ≠ a› by blast
have "r c ≠ c" using a r simple_rotations_fix_unique rnotid ‹c ≠ a› by blast
have "r d ≠ d" using a r simple_rotations_fix_unique rnotid ‹d ≠ a› by blast

then have False using sfix'
proof (cases "r b = c")
assume "r b = c"
then have "r c ≠ c" using r simple_rotation_bij_corollary ‹c ≠ b› by auto
then have "r c ≠ b" using r rnotid simple_rotations_cycle ‹r b = c› by auto
have dist:"distinct [a,b,c,d]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹d ≠ b› ‹c ≠ b› ‹b ≠ a› by simp
then have "∀ v ∈ {a,b,c}. r c ≠ v" using ‹r c ≠ c› ‹r c ≠ a› ‹r c ≠ b› by auto
then have "r c = d" using simple_distinct_map' r dist by auto

have "r d ≠ c" using r simple_rotation_bij_corollary ‹d ≠ b› ‹r b = c› by auto
have "r d ≠ d" using r a ‹d ≠ a› ‹r d ≠ d› by simp
have dist':"distinct [a,c,d,b]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹d ≠ b› ‹c ≠ b› ‹b ≠ a› by simp
then have "∀ v ∈ {a,c,d}. r d ≠ v" using ‹r d ≠ c› ‹r d ≠ a› ‹r d ≠ d› by auto
then have "r d = b" using simple_distinct_map' r dist' by auto

then have "s b = d" using ‹(r ∘ s) b = b› r simple_rotation_bij_corollary by auto
have "s c = b" using ‹(r ∘ s) c = c› ‹r b = c› r simple_rotation_bij_corollary by auto

then have "s b ≠ c" using ‹s b = d› ‹d ≠ c› by simp
then show False using s sfix' ‹s c = b› comp(3) by blast
next
assume "r b ≠ c"
have dist':"distinct [a,b,c,d]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹d ≠ b› ‹c ≠ b› ‹b ≠ a› by simp
then have "∀ v ∈ {a,b,c}. r b ≠ v" using ‹r b ≠ a› ‹r b ≠ b› ‹r b ≠ c› by auto
then have "r b = d" using simple_distinct_map' r dist' by auto

then have "r c ≠ d" using r simple_rotation_bij_corollary ‹c ≠ b› by auto
have dist'':"distinct [a,c,d,b]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹d ≠ b› ‹c ≠ b› ‹b ≠ a› by simp
then have "∀ v ∈ {a,c,d}. r c ≠ v" using ‹r c ≠ a› ‹r c ≠ c› ‹r c ≠ d› by auto
then have "r c = b" using simple_distinct_map' r dist'' by auto

then have "r d ≠ b" using r simple_rotation_bij_corollary ‹d ≠ c› by auto
have dist''':"distinct [a,b,d,c]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹d ≠ b› ‹c ≠ b› ‹b ≠ a› by simp
then have "∀ v ∈ {a,b,d}. r d ≠ v" using ‹r d ≠ a› ‹r d ≠ b› ‹r d ≠ d› by auto
then have "r d = c" using simple_distinct_map' r dist''' by auto

then have "s b = c" using ‹r c = b› ‹(r ∘ s) b = b› r simple_rotation_bij_corollary by auto
have "s c = d" using ‹(r ∘ s) c = c› ‹r d = c› r simple_rotation_bij_corollary by auto

then have "s c ≠ b" using ‹d ≠ b› by simp
then have False using comp(3) s sfix' ‹s b = c› by blast
then show ?thesis by simp
qed
then show ?thesis by simp
next
assume "¬ (∀ x. s x ≠ x)"
then have "∃ x. s x = x" by simp
then obtain a where a:"s a = a" by blast
from simple_rotations_fix obtain b where b:"r b = b" using r by blast
then show ?thesis
proof (cases "a = b")
assume "a ≠ b"
with a b have "r a ≠ a" using r rnotid simple_rotations_fix_unique by blast
then have "(r ∘ s) a ≠ a" using a by simp
have "s b ≠ b" using a ‹a ≠ b› s_fix_forall by blast
then have "(r ∘ s) b ≠ b" using b simple_rotations_inj r
complex_rotations.simp rotation_bij_corollary by fastforce
with fixes_two obtain c where "(r ∘ s) c = c" and "c ≠ a" and "c ≠ b" using ‹(r ∘ s) a ≠ a› by blast
from fixes_two obtain d where "(r ∘ s) d = d" and "d ≠ a" and "d ≠ b" and "d ≠ c"
using ‹(r ∘ s) a ≠ a› ‹(r ∘ s) b ≠ b› by blast

have "s c ≠ a" using a ‹c ≠ a› rotation_bij_corollary s by force
have "s d ≠ a" using a ‹d ≠ a› rotation_bij_corollary s by force

have "r a ≠ c" using ‹s c ≠ a› ‹(r ∘ s) c = c› ‹c ≠ a› r simple_rotation_bij_corollary by auto
have "r a ≠ d" using ‹s d ≠ a› ‹(r ∘ s) d = d› ‹d ≠ a› r simple_rotation_bij_corollary by auto
have "r a ≠ b" using b simple_rotation_bij_corollary ‹a ≠ b› r by auto

have dist:"distinct [b,c,d,a]" using ‹c ≠ a› ‹d ≠ a› ‹c ≠ b› ‹a ≠ b› ‹d ≠ c› ‹d ≠ b› by simp
then have "∀ v ∈ {b,c,d}. r a ≠ v" using ‹r a ≠ b› ‹r a ≠ c› ‹r a ≠ d› by auto
then have "r a = a" using simple_distinct_map' r dist by simp
then have False using ‹r a ≠ a› by simp
then show ?thesis by simp
next
assume "a = b"
with a b have "(r ∘ s) a = a" by simp
from fixes_two obtain c where rsc:"(r ∘ s) c = c" and "c ≠ a" by blast
then have "r c ≠ c" using b ‹a = b›r rnotid simple_rotations_fix_unique by blast
then have "s c ≠ c" using rsc by auto
then obtain d where "s c = d" and "d ≠ c" by blast
then have "d ≠ a" using a s rotation_bij_corollary by blast
have "s d ≠ d" using a using ‹d ≠ a› s_fix_forall by blast
have "r d = c" using rsc ‹s c = d› by simp
then have "r c ≠ d" using ‹d ≠ c› simple_rotations_cycle r rnotid by auto
then obtain e where "r c = e" and "e ≠ d" by blast
then have "e ≠ a" using b ‹a = b› simple_rotation_bij_corollary ‹c ≠ a› r by auto
then have "e ≠ c" using b ‹a = b› ‹r c = e› ‹r c ≠ c› by blast
then have "r e ≠ c" using ‹r c = e› simple_rotations_cycle r rnotid by auto
have "r e ≠ a" using b ‹a = b› ‹e ≠ a› simple_rotation_bij_corollary r by auto
then have "r e ≠ e" using ‹e ≠ c› ‹r c = e› r simple_rotation_bij_corollary by blast
have dist:"distinct [a,c,d,e]" using ‹c ≠ a› ‹d ≠ a› ‹d ≠ c› ‹e ≠ a› ‹e ≠ c› ‹e ≠ d› by simp
then have "∀ v ∈ {a,c,d}. r v ≠ d" using ‹r b = b› ‹a = b› ‹r d = c› ‹r c = e› by auto
then have "r e = d" using simple_distinct_map r dist by auto

have dist':"distinct [a,c,e,d]" using dist by auto
have "s e ≠ e" using  ‹e ≠ a› a s_fix_forall by blast
then have "∀ v ∈ {a,c,e}. s v ≠ e" using ‹s a = a› ‹s c = d› dist by auto
then have "s d = e" using distinct_map s dist' by auto
then have "∀ v ∈ {a,c,d}. s v ≠ c" using ‹s a = a › ‹s c = d› dist by auto
then have "s e = c" using distinct_map s dist by auto
then have "(r ∘ s) d = d" using ‹s d = e› ‹r e = d› by auto
then have "(r ∘ s) e = e" using ‹s e = c› ‹r c = e› by auto
then show "(r ∘ s) = id" using ‹(r ∘ s) d = d›  ‹(r ∘ s) a = a› ‹(r ∘ s) c = c› dist id_decomp by auto
qed
qed
qed
qed
qed
qed
qed

text ‹
This lemma is a simple corollary of the previous result. It is the main result necessary to
count stabilisers.
›

corollary complex_rotations_fix: "r ∈ complex_rotations ⟹ r a = a ⟹ r b = b ⟹ a ≠ b ⟹ r = id"
using complex_rotations_invariants by blast

section "Inversions"
text ‹
In this section we show that inverses exist for each rotation, which we will need to show that
the rotations we defined indeed form a group.
›

lemma simple_rotations_rotate_id:
assumes r:"r ∈ simple_rotations"
shows "r ∘ r ∘ r = id"
using r unfolding simple_rotations_def
by safe
(rule ext; rename_tac a; case_tac a;
)+

lemma simple_rotations_inverses:
assumes r:"r ∈ simple_rotations"
shows "∃y∈complex_rotations. y ∘ r = id"
proof
let ?y = "r ∘ r"
from r show y:"?y ∈ complex_rotations" using complex_rotations.intros by simp
from simple_rotations_rotate_id show "?y ∘ r = id" using r by auto
qed

lemma complex_rotations_inverses:
"r ∈ complex_rotations ⟹ ∃y∈complex_rotations. y ∘ r = id"
proof (induction r rule: complex_rotations.induct)
case (simp r) then show ?case using simple_rotations_inverses by blast
next
case (comp r s)
obtain r' where r'_comp:"r'∈complex_rotations" and r'_inv:"r' ∘ r = id"
using simple_rotations_inverses comp.hyps  by auto
obtain y where y_comp:"y∈complex_rotations" and y_inv:"y ∘ s = id" using comp.IH by blast
from complex_rotations_comp have yr':"y ∘ r' ∈ complex_rotations" using r'_comp y_comp by simp
have "r' ∘ (r ∘ s) = r' ∘ r ∘ s" using comp_assoc by metis
then have "r' ∘ (r ∘ s) = s" using r'_inv by simp
then have "y ∘ r' ∘ (r ∘ s) = id" using y_inv comp_assoc by metis
then show ?case using yr' by metis
qed

section "The Tetrahedral Group"

text ‹
We can now define the group of rotational symmetries of a tetrahedron. Since we modeled rotations
as functions, the group operation is functional composition and the identity element of the group is
the identity function
›

definition tetrahedral_group :: "Rotation monoid" where
"tetrahedral_group = ⦇carrier = complex_rotations, mult = (∘), one = id⦈"

text ‹
We now prove that this indeed forms a group. Most of the subgoals are trivial, the last goal uses
our results from the previous section about inverses.
›

lemma is_tetrahedral_group: "group tetrahedral_group"
proof(rule groupI)
show "𝟭⇘tetrahedral_group⇙ ∈ carrier tetrahedral_group"
by (simp add: complex_rotations.intros(1) simple_rotations_def tetrahedral_group_def)
next
fix x
assume "x ∈ carrier tetrahedral_group"
show "𝟭⇘tetrahedral_group⇙ ⊗⇘tetrahedral_group⇙ x = x"
unfolding id_comp tetrahedral_group_def monoid.select_convs(1) monoid.select_convs(2) ..
next
fix x y z
assume "x ∈ carrier tetrahedral_group" and
"y ∈ carrier tetrahedral_group" and
"z ∈ carrier tetrahedral_group"
then show "x ⊗⇘tetrahedral_group⇙ y ⊗⇘tetrahedral_group⇙ z =
x ⊗⇘tetrahedral_group⇙ (y ⊗⇘tetrahedral_group⇙ z)"
unfolding tetrahedral_group_def monoid.select_convs(1) by auto
next
fix x y
assume "x ∈ carrier tetrahedral_group" and
"y ∈ carrier tetrahedral_group"
then show "x ⊗⇘tetrahedral_group⇙ y ∈ carrier tetrahedral_group"
by (simp add: complex_rotations.intros(2) tetrahedral_group_def complex_rotations_comp)
next
fix x
assume "x ∈ carrier tetrahedral_group"
then show "∃y∈carrier tetrahedral_group.
y ⊗⇘tetrahedral_group⇙ x = 𝟭⇘tetrahedral_group⇙"
using complex_rotations_inverses by (simp add: tetrahedral_group_def)
qed

text ‹
Having proved that our definition forms a group we can now instantiate our orbit-stabiliser locale.
The group action is the application of a rotation.
›

fun apply_rotation :: "Rotation ⇒ Vertex ⇒ Vertex" where "apply_rotation r v = r v"

interpretation tetrahedral: orbit_stabiliser "tetrahedral_group" "apply_rotation :: Rotation ⇒ Vertex ⇒ Vertex"
proof intro_locales
show "Group.monoid tetrahedral_group" using is_tetrahedral_group by (simp add: group.is_monoid)
show "group_axioms tetrahedral_group" using is_tetrahedral_group by (simp add: group_def)
show "orbit_stabiliser_axioms tetrahedral_group apply_rotation"
proof
fix x
show "apply_rotation 𝟭⇘tetrahedral_group⇙ x = x" by (simp add: tetrahedral_group_def)
next
fix g h x
show "g ∈ carrier tetrahedral_group ∧ h ∈ carrier tetrahedral_group
⟶ apply_rotation g (apply_rotation h x) = apply_rotation (g ⊗⇘tetrahedral_group⇙ h) x"
qed
qed

section "Counting Orbits"
text ‹
We now prove that there is an orbit for each vertex. That is, the group action is transitive.
›
lemma orbit_is_transitive: "tetrahedral.orbit A = vertices"
proof
show "tetrahedral.orbit A ⊆ vertices" unfolding vertices_def using Vertex.exhaust by blast
have "id ∈ complex_rotations" using complex_rotations.intros simple_rotations_def by auto
then have "id ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1).
moreover have "apply_rotation id A = A" by simp
ultimately have A:"A ∈ (tetrahedral.orbit A)"
using tetrahedral.orbit_def mem_Collect_eq by fastforce

have "rotate_C ∈ simple_rotations"
using simple_rotations_def insert_subset subset_insertI by blast
then have "rotate_C ∈ complex_rotations" using complex_rotations.intros(1) by simp
then have "rotate_C ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1).
moreover have "apply_rotation rotate_C A = B" by (simp add: rotate_C_def)
ultimately have B:"B ∈ (tetrahedral.orbit A)"
using tetrahedral.orbit_def mem_Collect_eq by fastforce

have "rotate_D ∈ simple_rotations"
using simple_rotations_def insert_subset subset_insertI by blast
then have "rotate_D ∈ complex_rotations" using complex_rotations.intros(1) by simp
then have "rotate_D ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1).
moreover have "apply_rotation rotate_D A = C" by (simp add: rotate_D_def)
ultimately have C:"C ∈ (tetrahedral.orbit A)"
using tetrahedral.orbit_def mem_Collect_eq by fastforce

have "rotate_B ∈ simple_rotations"
using simple_rotations_def insert_subset subset_insertI by blast
then have "rotate_B ∈ complex_rotations" using complex_rotations.intros(1) by simp
then have "rotate_B ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1).
moreover have "apply_rotation rotate_B A = D" by (simp add: rotate_B_def)
ultimately have D:"D ∈ (tetrahedral.orbit A)"
using tetrahedral.orbit_def mem_Collect_eq by fastforce

from A B C D show "vertices ⊆ tetrahedral.orbit A" by (simp add: vertices_def subsetI)
qed

text ‹
It follows from the previous lemma, that the cardinality of the set of orbits for a particular vertex is 4.
›
lemma card_orbit: "card (tetrahedral.orbit A) = 4"
proof -
from card.empty card_insert_if have "card vertices = 4" unfolding vertices_def by auto
with orbit_is_transitive show "card (tetrahedral.orbit A) = 4" by simp
qed

section "Counting Stabilisers"

text ‹
Each vertex has three elements in its stabiliser - the identity, a rotation around its axis by 120 degrees,
and a rotation around its axis by 240 degrees. We will prove this next.
›
definition stabiliser_A :: "Rotation set" where
"stabiliser_A = {id, rotate_A, rotate_A ∘ rotate_A}"

text ‹
This lemma shows that our conjectured stabiliser is correct.
›
lemma is_stabiliser: "tetrahedral.stabiliser A = stabiliser_A"
proof
show "stabiliser_A ⊆ tetrahedral.stabiliser A"
proof -
have "id ∈ complex_rotations" using complex_rotations.intros simple_rotations_def by auto
then have "id ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1) by simp
moreover have "apply_rotation id A = A" by simp
ultimately have id:"id ∈ (tetrahedral.stabiliser A)"
using tetrahedral.stabiliser_def mem_Collect_eq by fastforce

have "rotate_A ∈ simple_rotations"
using simple_rotations_def insert_subset subset_insertI by blast
then have "rotate_A ∈ complex_rotations" using complex_rotations.intros(1) by simp
then have "rotate_A ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1) by simp
moreover have "apply_rotation rotate_A A = A" by (simp add: rotate_A_def)
ultimately have A:"rotate_A ∈ (tetrahedral.stabiliser A)"
using tetrahedral.stabiliser_def mem_Collect_eq by fastforce

have "rotate_A ∈ simple_rotations"
using simple_rotations_def insert_subset subset_insertI by blast
then have "rotate_A ∘ rotate_A ∈ complex_rotations" using complex_rotations.intros by simp
then have "rotate_A ∘ rotate_A ∈ carrier tetrahedral_group"
unfolding tetrahedral_group_def partial_object.select_convs(1) by simp
moreover have "apply_rotation (rotate_A ∘ rotate_A) A = A" by (simp add: rotate_A_def)
ultimately have AA:"(rotate_A ∘ rotate_A) ∈ (tetrahedral.stabiliser A)"
using tetrahedral.stabiliser_def mem_Collect_eq by fastforce

from id A AA show "stabiliser_A ⊆ tetrahedral.stabiliser A"
qed
show "tetrahedral.stabiliser A ⊆ stabiliser_A"
proof
fix x
assume a:"x ∈ tetrahedral.stabiliser A"
with tetrahedral.stabiliser_def have "apply_rotation x A = A" by simp
with apply_rotation.simps have xA:"x A = A" by simp
from a have "x ∈ carrier tetrahedral_group"
using subgroup.mem_carrier[of "tetrahedral.stabiliser A"] tetrahedral.stabiliser_subgroup by auto
then have xC:"x ∈ complex_rotations"
unfolding tetrahedral_group_def partial_object.select_convs(1) by simp
have "x B ≠ A" using xA xC rotation_bij_corollary by fastforce
then have "x ∈ complex_rotations ⟹ x A = A ⟹ x ∈ stabiliser_A"
proof (cases "x B", simp)
assume "x B = B"
then have "x = id" using complex_rotations_fix xC xA by simp
then show ?thesis using stabiliser_A_def by auto
next
assume "x B = C"
then have "x ≠ id" by auto
then have "x D ≠ D" using complex_rotations_fix xC xA by blast
have "x D ≠ C" using xC ‹x B = C› rotation_bij_corollary by fastforce
have "x D ≠ A" using xC xA rotation_bij_corollary by fastforce
then have "x D = B" using ‹x D ≠ C›  ‹x D ≠ D› Vertex.exhaust by blast

have "x C ≠ A" using xC xA rotation_bij_corollary by fastforce
have "x C ≠ B" using xC ‹x D = B› rotation_bij_corollary by fastforce
have "x C ≠ C" using complex_rotations_fix xC xA ‹x ≠ id› by blast
then have "x C = D" using ‹x C ≠ A› ‹x C ≠ B› Vertex.exhaust by blast

have "∀ v. x v = rotate_A v"
using xA ‹x B = C› ‹x D = B› ‹x C = D› Vertex.exhaust rotate_A_def Vertex.simps by metis
then have "x = rotate_A" by auto
then show ?thesis using stabiliser_A_def by auto
next
assume "x B = D"
then have "x ≠ id" by auto
then have "x C ≠ C" using complex_rotations_fix xC xA by blast
have "x C ≠ D" using xC ‹x B = D› rotation_bij_corollary by fastforce
have "x C ≠ A" using xC xA rotation_bij_corollary by fastforce
then have "x C = B" using ‹x C ≠ D›  ‹x C ≠ C› Vertex.exhaust by blast

have "x D ≠ A" using xC xA rotation_bij_corollary by fastforce
have "x D ≠ B" using xC ‹x C = B› rotation_bij_corollary by fastforce
have "x D ≠ D" using complex_rotations_fix xC xA ‹x ≠ id› by blast
then have "x D = C" using ‹x D ≠ A› ‹x D ≠ B› Vertex.exhaust by blast

have "∀ v. x v = (rotate_A ∘ rotate_A) v"
using xA ‹x B = D› ‹x C = B› ‹x D = C› Vertex.exhaust rotate_A_def Vertex.simps comp_apply by metis
then have "x = rotate_A ∘ rotate_A" by auto
then show ?thesis using stabiliser_A_def by auto
qed
then show "x ∈ stabiliser_A" using xA xC by simp
qed
qed

text ‹
Using the previous result, we can now show that the cardinality of the stabiliser is 3.
›
lemma card_stabiliser_help: "card stabiliser_A = 3"
proof -
have idA:"id ≠ rotate_A"
proof -
have "id B = B" by simp
moreover have "rotate_A B = C" by (simp add: rotate_A_def)
ultimately show "id ≠ rotate_A" by force
qed
have idAA:"id ≠ rotate_A ∘ rotate_A"
proof -
have "id B = B" by simp
moreover have "(rotate_A ∘ rotate_A) B = D" by (simp add: rotate_A_def)
ultimately show "id ≠ rotate_A ∘ rotate_A" by force
qed
have AAA:"rotate_A ≠ rotate_A ∘ rotate_A"
proof -
have "rotate_A B = C" by (simp add: rotate_A_def)
moreover have "(rotate_A ∘ rotate_A) B = D" by (simp add: rotate_A_def)
ultimately show "rotate_A ≠ rotate_A ∘ rotate_A" by force
qed
from idA idAA AAA card.empty card_insert_if show
"(card stabiliser_A) = 3" unfolding stabiliser_A_def by auto
qed

lemma card_stabiliser: "card (tetrahedral.stabiliser A) = 3"
using is_stabiliser card_stabiliser_help by simp

section "Proving Finiteness"

text ‹
In order to apply the orbit-stabiliser theorem, we need to prove that the set of rotations is
finite. We first prove that the set of vertices is finite.
›
lemma vertex_set: "(UNIV::Vertex set) = {A, B, C, D}"
by(auto, metis Vertex.exhaust)

lemma vertex_finite: "finite (UNIV :: Vertex set)"

text ‹
Next we need instantiate Vertex as an element of the type class of finite sets in
HOL/Finite\_Set.thy. This will allow us to use the lemma that functions between finite sets
are finite themselves.
›

instantiation Vertex :: finite
begin
instance proof
show "finite (UNIV :: Vertex set)" by (simp add: vertex_set)
qed

text ‹
Now we can show that the set of rotations is finite.
›
lemma finite_carrier: "finite (carrier tetrahedral_group)"
proof -
(* This follows from the instantiation above *)
have "finite (UNIV :: (Vertex ⇒ Vertex) set)" by simp
moreover have "complex_rotations ⊆ (UNIV :: (Vertex ⇒ Vertex) set)" by simp
ultimately show "finite (carrier tetrahedral_group)" using finite_subset top_greatest by blast
qed

section "Order of the Group"

text ‹
We can now finally apply the orbit-stabiliser theorem.
Since we have orbits of cardinality 4 and stabilisers of cardinality 3, the order of the tetrahedral group,
and with it the number of rotational symmetries of the tetrahedron, is 12.
›
theorem "order tetrahedral_group = 12"
proof -
have "card (tetrahedral.orbit A) * card (tetrahedral.stabiliser A) = 12"
using card_stabiliser card_orbit by simp
with tetrahedral.orbit_stabiliser[OF finite_carrier]
show "order tetrahedral_group = 12" by simp
qed

end

end
```