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;
      simp add: simple_rotations
     )+

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;
      auto simp add: simple_rotations Vertex.split
     )+

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)
apply(auto simp add: comp_assoc complex_rotations.comp)
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; 
      auto simp add: simple_rotations
     )+
   
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;
      auto simp add: simple_rotations
     )+ 

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(auto simp add: distinct_def)
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;
      simp add: simple_rotations
     )+

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"
      by (simp add: tetrahedral_group_def)
  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"
      by (simp add: stabiliser_A_def subsetI)
  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)"
  by (simp add: 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