A quick way to arrive to the abelian group of order eight in Isabelle

I'm formalizing this article in Isabelle. In section 4.1 it describes the following setting:

context 
  fixes c d :: real
  assumes "c ≠ 0" "∃ b. c = b^2" "∃ b'. d = b'^2"
begin
  definition t where "t = sqrt(d/c)"
  definition e' where "e' x y = x^2 + y^2 - 1 - t^2 * x^2 * y^2"

  definition ρ where "ρ x y = (-y,x)"
  definition τ where "τ x y = (1/(t*x),1/(t*y))"

It then defines G to be the abelian group of order eight generated by ρ and τ.

Is there an easy way of:

Stating that ρ and τ generate a group.
Since ρ and τ have order 2 and commute I think that all the rest commute and maybe there is a built-in theorem saying that this has to correspond to an abelian group of order 8?

Solution

I did make an attempt to solve the problem and came up with a slightly forceful method for its solution:

context 
  fixes c d :: real
  assumes "c ≠ 0" "∃b. c = b^2" "∃b'. d = b'^2"
begin

definition t where "t = sqrt(d/c)"
definition e' where "e' x y = x^2 + y^2 - 1 - t^2 * x^2 * y^2"

context
  assumes nz_t: "t ≠ 0"
begin

definition ρ :: "real × real ⇒ real × real" where 
  "ρ z = (-snd z, fst z)"
definition τ :: "real × real ⇒ real × real" where 
  "τ z = (1/(t*fst z), 1/(t*snd z))"
definition S where
  "S ≡ 
    {
      id,
      (λz. (-snd z, fst z)),
      (λz. (-fst z, -snd z)),
      (λz. (snd z, -fst z)),
      (λz. (1/(t*fst z), 1/(t*snd z))),
      (λz. (-1/(t*snd z), 1/(t*fst z))),
      (λz. (-1/(t*fst z), -1/(t*snd z))),
      (λz. (1/(t*snd z), -1/(t*fst z)))
    }"
definition ρS where
  "ρS ≡ 
    {id, (λz. (-snd z, fst z)), (λz. (-fst z, -snd z)), (λz. (snd z, -fst z))}"
definition τS where
  "τS ≡ {id, (λz. (1/(t*fst z), 1/(t*snd z)))}"

definition BIJ where "BIJ = ⦇carrier = {f. bij f}, mult = comp, one = id⦈"

interpretation bij: group BIJ
  unfolding BIJ_def
  apply unfold_locales
  subgoal by (simp add: bij_comp)
  subgoal by (simp add: comp_assoc)
  subgoal by simp
  subgoal by simp
  subgoal by simp
  subgoal 
    unfolding Units_def
    by clarsimp 
      (metis inj_iff bij_betw_def bij_betw_inv_into inv_o_cancel surj_iff)
  done

(*the proof may take quite a few seconds*)
lemma comp_S: "x ∈ S ⟹ y ∈ S ⟹ x ∘ y ∈ S"
  unfolding comp_apply S_def Set.insert_iff by (elim disjE) fastforce+ 

lemma comm_S: "x ∈ S ⟹ y ∈ S ⟹ x ∘ y = y ∘ x"
  unfolding comp_apply S_def Set.insert_iff by (elim disjE) fastforce+ 

lemma bij_ρ: "bij ρ"
  unfolding bij_def inj_def surj_def ρ_def 
  by clarsimp (metis add.inverse_inverse)

lemma bij_τ: "bij τ"
  unfolding bij_def inj_def surj_def τ_def 
proof(simp add: nz_t, intro allI, intro exI)
  fix a show "a = 1 / (t * (1/(a*t)))" using nz_t by simp
qed

lemma generate_ρτ: "generate BIJ {ρ, τ} = S"
proof(standard; intro subsetI)
  have inv_τ: "inv⇘BIJ⇙ τ = τ"
    unfolding m_inv_def
  proof(standard)
    show "τ ∈ carrier BIJ ∧ τ ⊗⇘BIJ⇙ τ = 𝟭⇘BIJ⇙ ∧ τ ⊗⇘BIJ⇙ τ = 𝟭⇘BIJ⇙"
      unfolding BIJ_def apply(intro conjI)
      subgoal using bij_τ by simp
      subgoal unfolding τ_def using nz_t by auto 
      subgoal unfolding τ_def using nz_t by auto 
      done
    then show 
      "y ∈ carrier BIJ ∧ τ ⊗⇘BIJ⇙ y = 𝟭⇘BIJ⇙ ∧ y ⊗⇘BIJ⇙ τ = 𝟭⇘BIJ⇙ ⟹ y = τ" 
      for y
      unfolding BIJ_def by (auto intro: left_right_inverse_eq)
  qed
  define ρ' :: "real × real ⇒ real × real" where "ρ' = (λz. (snd z, -fst z))"
  have bij_ρ': "bij ρ'"
    unfolding bij_def inj_def surj_def ρ'_def
    by simp (metis add.inverse_inverse)
  have inv_ρ: "inv⇘BIJ⇙ ρ = ρ'"
    unfolding m_inv_def
  proof(standard)
    show "ρ' ∈ carrier BIJ ∧ ρ ⊗⇘BIJ⇙ ρ' = 𝟭⇘BIJ⇙ ∧ ρ' ⊗⇘BIJ⇙ ρ = 𝟭⇘BIJ⇙"
      unfolding BIJ_def apply(intro conjI)
      subgoal using bij_ρ' by auto
      subgoal unfolding ρ_def ρ'_def by auto 
      subgoal unfolding ρ_def ρ'_def by auto 
      done
    then show 
      "y ∈ carrier BIJ ∧ ρ ⊗⇘BIJ⇙ y = 𝟭⇘BIJ⇙ ∧ y ⊗⇘BIJ⇙ ρ = 𝟭⇘BIJ⇙ ⟹ y = ρ'" 
      for y
      unfolding BIJ_def by (auto intro: left_right_inverse_eq)
  qed
  have ττ: "τ ⊗⇘BIJ⇙ τ = 𝟭⇘BIJ⇙" 
    unfolding BIJ_def τ_def comp_def by (auto simp: nz_t)
  show "x ∈ generate BIJ {ρ, τ} ⟹ x ∈ S" for x
    apply(induction rule: generate.induct)
    subgoal unfolding BIJ_def S_def by auto
    subgoal unfolding BIJ_def S_def ρ_def τ_def by auto
    subgoal 
      unfolding Set.insert_iff apply(elim disjE)
      subgoal using inv_ρ unfolding BIJ_def S_def ρ_def ρ'_def by simp    
      subgoal using inv_τ unfolding BIJ_def S_def τ_def by simp
      subgoal by simp
      done
    subgoal unfolding BIJ_def by (metis monoid.select_convs(1) comp_S)
    done
  show "x ∈ S ⟹ x ∈ generate BIJ {ρ, τ}" for x
    unfolding S_def Set.insert_iff
  proof(elim disjE; clarsimp)
    show "id ∈ generate BIJ {ρ, τ}"
      unfolding BIJ_def using generate.simps by fastforce
    show ρ_gen: "(λz. (- snd z, fst z)) ∈ generate BIJ {ρ, τ}"
      by (fold ρ_def, rule generate.simps[THEN iffD2]) simp
    show τ_gen: "(λz. (1 / (t * fst z), 1 / (t * snd z))) ∈ generate BIJ {ρ, τ}"
      by (fold τ_def) (simp add: generate.incl)
    from inv_ρ show inv_ρ_gen: "(λz. (snd z, - fst z)) ∈ generate BIJ {ρ, τ}"
      by (fold ρ'_def) (auto simp: generate.inv insertI1)
    show ρρ_gen: "(λz. (- fst z, - snd z)) ∈ generate BIJ {ρ, τ}"
    proof-
      have ρρ: "(λz. (- fst z, - snd z)) = ρ ⊗⇘BIJ⇙ ρ"
        unfolding ρ_def BIJ_def by auto
      show ?thesis 
        apply(rule generate.simps[THEN iffD2])
        using ρρ ρ_gen[folded ρ_def] by auto
    qed
    show "(λz. (- (1 / (t * snd z)), 1 / (t * fst z))) ∈ generate BIJ {ρ, τ}"
    proof-
      have ρτ: "(λz. (- (1 / (t * snd z)), 1 / (t * fst z))) = ρ ⊗⇘BIJ⇙ τ"
        unfolding ρ_def τ_def BIJ_def by auto
      show ?thesis 
        apply(rule generate.simps[THEN iffD2])
        using ρτ ρ_gen[folded ρ_def] τ_gen[folded τ_def] by auto
    qed
    show 
      "(λz. (- (1 / (t * fst z)), - (1 / (t * snd z)))) ∈ generate BIJ {ρ, τ}"
    proof-
      have ρρτ: 
        "(λz. (- (1 / (t * fst z)), - (1 / (t * snd z)))) = 
        (λz. (- fst z, - snd z)) ⊗⇘BIJ⇙ τ"
        unfolding τ_def BIJ_def by auto
      show ?thesis 
        apply(rule generate.simps[THEN iffD2])
        using ρρτ ρρ_gen τ_gen[folded τ_def] by auto
    qed
    show "(λz. (1 / (t * snd z), - (1 / (t * fst z)))) ∈ generate BIJ {ρ, τ}"
    proof-
      have inv_ρ_τ: 
        "(λz. (1 / (t * snd z), - (1 / (t * fst z)))) = 
        (λz. (snd z, - fst z)) ⊗⇘BIJ⇙ τ"
        unfolding τ_def BIJ_def by auto
      show ?thesis 
        apply(rule generate.simps[THEN iffD2])
        using inv_ρ_τ inv_ρ_gen τ_gen[folded τ_def] by auto
    qed
  qed 
qed

lemma "comm_group (BIJ⦇carrier := (generate BIJ {ρ, τ})⦈)" 
proof-
  have ρτ_ss_BIJ: "{ρ, τ} ⊆ carrier BIJ" 
    using bij_ρ bij_τ unfolding BIJ_def by simp
  interpret ρτ_sg: subgroup "(generate BIJ {ρ, τ})" BIJ 
    using ρτ_ss_BIJ by (rule bij.generate_is_subgroup)
  interpret ρτ_g: group "BIJ⦇carrier := (generate BIJ {ρ, τ})⦈"
    by (rule ρτ_sg.subgroup_is_group[OF bij.group_axioms])
  have car_S: "carrier (BIJ⦇carrier := S⦈) = S" by simp
  have BIJ_comp: "x ⊗⇘BIJ⦇carrier := S⦈⇙ y = x ∘ y" for x y
    unfolding BIJ_def by auto
  from ρτ_g.group_comm_groupI[
      unfolded generate_ρτ car_S BIJ_comp, OF comm_S, simplified
      ]
  show ?thesis unfolding generate_ρτ by assumption 
qed

lemma id_pair_def: "(λx. x) = (λz. (fst z, snd z))" by simp

lemma distinct_single: "distinct [x] = True" by simp

lemma ne_ff'_gg'_imp_ne_fgf'g':
  assumes "f ≠ f' ∨ g ≠ g'"
  shows 
    "(λz. (f (fst z) (snd z), g (fst z) (snd z))) ≠ 
    (λz. (f' (fst z) (snd z), g' (fst z) (snd z)))"
  using assms
proof(rule disjE)
  assume "f ≠ f'"
  then obtain x y where "f x y ≠ f' x y" by blast  
  then show ?thesis by (metis (hide_lams) fst_eqD snd_eqD)
next
  assume "g ≠ g'"
  then obtain x y where "g x y ≠ g' x y" by blast  
  then show ?thesis by (metis (hide_lams) fst_eqD snd_eqD)
qed

lemma id_ne_hyp: "(λa. a) ≠ (λa. 1/(t*a))" 
proof(rule ccontr, simp)
  assume id_eq_hyp: "(λa. a) = (λa. 1/(t*a))"
  {
    fix a :: real assume "a > 0"
    define b where "b = sqrt(a)"
    from ‹a > 0› have "a = b*b" and "b > 0" unfolding b_def by auto
    from id_eq_hyp have "b = 1/(t*b)" by metis
    with ‹b > 0› have "b div b =(1/(t*b)) div b" by simp
    with ‹b > 0› have "1 = (1/(t*a))" unfolding ‹a = b*b› by simp
    with ‹a > 0› nz_t have "t*a = 1" by simp
  }
  note ta_eq_one = this
  define t2 where "t2 = (if t > 0 then 2/t else -2/t)" 
  with nz_t have "t2 > 0" unfolding t2_def by auto
  from nz_t have "t*t2 = 2 ∨ t*t2 = -2" unfolding t2_def by auto
  from ta_eq_one ‹t2 > 0› this show False by auto
qed

lemma id_ne_mhyp: "(λa. a) ≠ (λa. -1/(t*a))"
proof(rule ccontr, simp)
  assume id_eq_hyp: "(λa. a) = (λa. -(1/(t*a)))"
  {
    fix a :: real assume "a > 0"
    define b where "b = sqrt(a)"
    from ‹a > 0› have "a = b*b" and "b > 0" unfolding b_def by auto
    from id_eq_hyp have "b = -(1/(t*b))" by metis
    with ‹b > 0› have "b div b =-1/(t*b) div b" by simp
    with ‹b > 0› have "1 = -1/(t*a)" unfolding ‹a = b*b› by simp
    with ‹a > 0› nz_t have "t*a = -1" by (metis divide_eq_1_iff)
  }
  note ta_eq_one = this
  define t2 where "t2 = (if t > 0 then 2/t else -2/t)" 
  with nz_t have "t2 > 0" unfolding t2_def by auto
  from nz_t have "t*t2 = 2 ∨ t*t2 = -2" unfolding t2_def by auto
  from ta_eq_one ‹t2 > 0› this show False by auto
qed

lemma mid_ne_hyp: "(λa. -a) ≠ (λa. 1 / (t*a))"
  using id_ne_mhyp by (metis minus_divide_left minus_equation_iff)

lemma mid_ne_mhyp: "(λa. -a) ≠ (λa. -1 / (t*a))"
  using id_ne_hyp by (metis divide_minus_left minus_equation_iff)

lemma hyp_neq_hyp_1: "(λa. - 1/(t*a)) ≠ (λa. 1/(t*a))"
  using nz_t 
  by (metis divide_cancel_right id_ne_mhyp mult_cancel_right1 mult_left_cancel 
      one_neq_neg_one)

lemma distinct:
  "distinct 
    [
      id,
      (λz. (-snd z, fst z)),
      (λz. (-fst z, -snd z)),
      (λz. (snd z, -fst z)),
      (λz. (1/(t*fst z), 1/(t*snd z))),
      (λz. (-1/(t*snd z), 1/(t*fst z))),
      (λz. (-1/(t*fst z), -1/(t*snd z))),
      (λz. (1/(t*snd z), -1/(t*fst z)))
    ]"
  apply(unfold distinct_length_2_or_more)+
  unfolding 
    distinct_length_2_or_more
    distinct_single
    id_def id_pair_def
    HOL.simp_thms(21)
  by 
    (intro conjI) 
    (
      rule ne_ff'_gg'_imp_ne_fgf'g', 
      metis one_neq_neg_one id_ne_hyp id_ne_mhyp
      mid_ne_hyp mid_ne_mhyp hyp_neq_hyp_1
    )+ 

lemma "card S = 8"
  using distinct unfolding S_def using card_empty card_insert_disjoint by auto

end

end

Remarks

I relied on sledgehammer for many parts of the proofs and there is some unnecessary code duplication. Therefore, just like most of my answers on SO, this answer is far from perfect from the perspective of the coding style.
I would be interested to know if there is a better overall approach for the solution. Somehow, I came to believe that most of the more thoughtful approaches (e.g. using theorems about cyclic groups to determine the order of ρ and τ and then using |HK|=|H||K|/|H∩K| to determine the order of G) would require proving quite a number of additional theorems for HOL-Algebra, but I did not check with the AFP before making this remark and I do not use HOL-Algebra on a regular basis. Therefore, I may have missed something.