# Theory Edwards_Elliptic_Curves_Group

```theory Edwards_Elliptic_Curves_Group
imports  "HOL-Algebra.Group" "HOL-Library.Rewrite"
begin

section‹Affine Edwards curves›

class ell_field = field +
assumes two_not_zero: "2 ≠ 0"

fixes c d :: "'a::ell_field"
begin

definition e :: "'a ⇒ 'a ⇒ 'a" where
"e x y = x^2 + c * y^2 - 1 - d * x^2 * y^2"

definition delta_plus :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta_plus x1 y1 x2 y2 = 1 + d * x1 * y1 * x2 * y2"

definition delta_minus :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta_minus x1 y1 x2 y2 = 1 - d * x1 * y1 * x2 * y2"

definition delta :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta x1 y1 x2 y2 = (delta_plus x1 y1 x2 y2) *
(delta_minus x1 y1 x2 y2)"

lemma delta_com:
"(delta x0 y0 x1 y1 = 0) = (delta x1 y1 x0 y0 = 0)"
unfolding delta_def delta_plus_def delta_minus_def
apply algebra
done

fun add :: "'a × 'a ⇒ 'a × 'a ⇒ 'a × 'a" where
((x1*x2 - c*y1*y2) div (1-d*x1*y1*x2*y2),
(x1*y2+y1*x2) div (1+d*x1*y1*x2*y2))"

assumes "z3 = (x3,y3)" "z3 = add (x1,y1) (x2,y2)"
assumes "delta_minus x1 y1 x2 y2 ≠ 0" "delta_plus x1 y1 x2 y2 ≠ 0"
assumes "e x1 y1 = 0" "e x2 y2 = 0"
shows "e x3 y3 = 0"
proof -
have x3_expr: "x3 = (x1*x2 - c*y1*y2) div (delta_minus x1 y1 x2 y2)"
using assms delta_minus_def by auto
have y3_expr: "y3 = (x1*y2+y1*x2) div (delta_plus x1 y1 x2 y2)"
using assms delta_plus_def by auto

have "∃ r1 r2. (e x3 y3)*(delta x1 y1 x2 y2)⇧2 - (r1 * e x1 y1 + r2 * e x2 y2) = 0"
unfolding e_def x3_expr y3_expr delta_def
unfolding delta_plus_def delta_minus_def
by algebra
then show "e x3 y3 = 0"
using assms
qed

lemma associativity:
assumes "z1' = (x1',y1')" "z3' = (x3',y3')"
assumes "delta_minus x1 y1 x2 y2 ≠ 0" "delta_plus x1 y1 x2 y2 ≠ 0"
"delta_minus x2 y2 x3 y3 ≠ 0" "delta_plus x2 y2 x3 y3 ≠ 0"
"delta_minus x1' y1' x3 y3 ≠ 0" "delta_plus x1' y1' x3 y3 ≠ 0"
"delta_minus x1 y1 x3' y3' ≠ 0" "delta_plus x1 y1 x3' y3' ≠ 0"
assumes "e x1 y1 = 0" "e x2 y2 = 0" "e x3 y3 = 0"
proof -
define e1 where "e1 = e x1 y1"
define e2 where "e2 = e x2 y2"
define e3 where "e3 = e x3 y3"
define Delta⇩x where "Delta⇩x =
(delta_minus x1' y1' x3 y3)*(delta_minus x1 y1 x3' y3')*
(delta x1 y1 x2 y2)*(delta x2 y2 x3 y3)"
define Delta⇩y where "Delta⇩y =
(delta_plus x1' y1' x3 y3)*(delta_plus x1 y1 x3' y3')*
(delta x1 y1 x2 y2)*(delta x2 y2 x3 y3)"
define g⇩x where "g⇩x = fst(add z1' (x3,y3)) - fst(add (x1,y1) z3')"
define g⇩y where "g⇩y = snd(add z1' (x3,y3)) - snd(add (x1,y1) z3')"
define gxpoly where "gxpoly = g⇩x * Delta⇩x"
define gypoly where "gypoly = g⇩y * Delta⇩y"

have x1'_expr: "x1' = (x1 * x2 - c * y1 * y2) / (1 - d * x1 * y1 * x2 * y2)"
using assms(1,3) by simp
have y1'_expr: "y1' = (x1 * y2 + y1 * x2) / (1 + d * x1 * y1 * x2 * y2)"
using assms(1,3) by simp
have x3'_expr: "x3' = (x2 * x3 - c * y2 * y3) / (1 - d * x2 * y2 * x3 * y3)"
using assms(2,4) by simp
have y3'_expr: "y3' = (x2 * y3 + y2 * x3) / (1 + d * x2 * y2 * x3 * y3)"
using assms(2,4) by simp

"delta x1 y1 x2 y2 ≠ 0" using delta_def assms(5,6) by auto

have simp1gx: "
(x1' * x3 - c * y1' * y3) * delta_minus x1 y1 x3' y3' *
(delta x1 y1 x2 y2 * delta x2 y2 x3 y3) =
((x1 * x2 - c * y1 * y2) * x3 * delta_plus x1 y1 x2 y2 -
c * (x1 * y2 + y1 * x2) * y3 * delta_minus x1 y1 x2 y2) *
(delta_minus x2 y2 x3 y3 * delta_plus x2 y2 x3 y3 -
d * x1 * y1 * (x2 * x3 - c * y2 * y3) * (x2 * y3 + y2 * x3))
"
apply(rewrite x1'_expr y1'_expr x3'_expr y3'_expr)+
apply(rewrite delta_minus_def)
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric] delta_plus_def[symmetric])+
unfolding delta_def

have simp2gx:
"(x1 * x3' - c * y1 * y3') * delta_minus x1' y1' x3 y3 *
(delta x1 y1 x2 y2 * delta x2 y2 x3 y3) =
(x1 * (x2 * x3 - c * y2 * y3) * delta_plus x2 y2 x3 y3 -
c * y1 * (x2 * y3 + y2 * x3) * delta_minus x2 y2 x3 y3) *
(delta_minus x1 y1 x2 y2 * delta_plus x1 y1 x2 y2 -
d * (x1 * x2 - c * y1 * y2) * (x1 * y2 + y1 * x2) * x3 * y3)"
apply(rewrite x1'_expr y1'_expr x3'_expr y3'_expr)+
apply(rewrite delta_minus_def)
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric] delta_plus_def[symmetric])+
unfolding delta_def

have "∃ r1 r2 r3. gxpoly = r1 * e1 + r2 * e2 + r3 * e3"
unfolding gxpoly_def g⇩x_def Delta⇩x_def
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric])+
apply(rewrite left_diff_distrib)
unfolding delta_plus_def delta_minus_def
e1_def e2_def e3_def e_def
by algebra

then have "gxpoly = 0"
using e1_def assms(13-15) e2_def e3_def by auto
have "Delta⇩x ≠ 0"
using Delta⇩x_def delta_def assms(7-11) non_unfolded_adds by auto
then have "g⇩x = 0"
using ‹gxpoly = 0› gxpoly_def by auto

have simp1gy: "(x1' * y3 + y1' * x3) * delta_plus x1 y1 x3' y3' * (delta x1 y1 x2 y2 * delta x2 y2 x3 y3) =
((x1 * x2 - c * y1 * y2) * y3 * delta_plus x1 y1 x2 y2 + (x1 * y2 + y1 * x2) * x3 * delta_minus x1 y1 x2 y2) *
(delta_minus x2 y2 x3 y3 * delta_plus x2 y2 x3 y3 + d * x1 * y1 * (x2 * x3 - c * y2 * y3) * (x2 * y3 + y2 * x3))"
apply(rewrite x1'_expr y1'_expr x3'_expr y3'_expr)+
apply(rewrite delta_plus_def)
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric] delta_plus_def[symmetric])+
unfolding delta_def

have simp2gy: "(x1 * y3' + y1 * x3') * delta_plus x1' y1' x3 y3 * (delta x1 y1 x2 y2 * delta x2 y2 x3 y3) =
(x1 * (x2 * y3 + y2 * x3) * delta_minus x2 y2 x3 y3 + y1 * (x2 * x3 - c * y2 * y3) * delta_plus x2 y2 x3 y3) *
(delta_minus x1 y1 x2 y2 * delta_plus x1 y1 x2 y2 + d * (x1 * x2 - c * y1 * y2) * (x1 * y2 + y1 * x2) * x3 * y3)"
apply(rewrite x1'_expr y1'_expr x3'_expr y3'_expr)+
apply(rewrite delta_plus_def)
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric] delta_plus_def[symmetric])+
unfolding delta_def

have "∃ r1 r2 r3. gypoly = r1 * e1 + r2 * e2 + r3 * e3"
unfolding gypoly_def g⇩y_def Delta⇩y_def
apply(rewrite in "_ / ⌑" delta_plus_def[symmetric])+
apply(rewrite left_diff_distrib)
unfolding delta_plus_def delta_minus_def
e1_def e2_def e3_def e_def
by algebra

then have "gypoly = 0"
using e1_def assms(13-15) e2_def e3_def by auto
have "Delta⇩y ≠ 0"
using Delta⇩y_def delta_def assms(7-12) non_unfolded_adds by auto
then have "g⇩y = 0"
using ‹gypoly = 0› gypoly_def by auto

show ?thesis
using ‹g⇩y = 0› ‹g⇩x = 0›
unfolding g⇩x_def g⇩y_def assms(3,4)
qed

lemma neutral: "add z (1,0) = z" by(cases "z",simp)

lemma inverse:
assumes "e a b = 0" "delta_plus a b a b ≠ 0"
shows "add (a,b) (a,-b) = (1,0)"
using assms
by algebra

lemma affine_closure:
assumes "delta x1 y1 x2 y2 = 0" "e x1 y1 = 0" "e x2 y2 = 0"
shows "∃ b. (1/d = b^2 ∧ 1/d ≠ 0) ∨ (1/(c*d) = b^2 ∧ 1/(c*d) ≠ 0)"
proof -
define r where "r = (1 - c*d*y1^2*y2^2) * (1 - d*y1^2*x2^2)"
define e1 where "e1 = e x1 y1"
define e2 where "e2 = e x2 y2"
have "r = d^2 * y1^2 * y2^2 * x2^2 * e1 + (1 - d * y1^2) * delta x1 y1 x2 y2 - d * y1^2 * e2"
unfolding r_def e1_def e2_def delta_def delta_plus_def delta_minus_def e_def
by algebra
then have "r = 0"
using assms e1_def e2_def by simp
then have cases: "(1 - c*d*y1^2*y2^2) = 0 ∨ (1 - d*y1^2*x2^2) = 0"
using r_def by auto
have "d ≠ 0" using ‹r = 0› r_def by auto
{
assume "(1 - d*y1^2*x2^2) = 0"
then have "1/d = y1^2*x2^2" "1/d ≠ 0"
apply(auto simp add: divide_simps ‹d ≠ 0›)
by algebra
}
note case1 = this
{assume "(1 - c*d*y1^2*y2^2) = 0" "(1 - d*y1^2*x2^2) ≠ 0"
then have "c ≠ 0" by auto
then have "1/(c*d) = y1^2*y2^2" "1/(c*d) ≠ 0"
apply(simp add: divide_simps ‹d ≠ 0› ‹c ≠ 0›)
using ‹(1 - c*d*y1^2*y2^2) = 0› apply algebra
using ‹c ≠ 0› ‹d ≠ 0› by auto
}
note case2 = this

show "∃ b. (1/d = b^2 ∧ 1/d ≠ 0) ∨ (1/(c*d) = b^2 ∧ 1/(c*d) ≠ 0)"
using cases case1 case2 by (metis power_mult_distrib)
qed

lemma delta_non_zero:
fixes x1 y1 x2 y2
assumes "e x1 y1 = 0" "e x2 y2 = 0"
assumes "∃ b. 1/c = b^2" "¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)"
shows "delta x1 y1 x2 y2 ≠ 0"
proof(rule ccontr)
assume "¬ delta x1 y1 x2 y2 ≠ 0"
then have "delta x1 y1 x2 y2 = 0" by blast
then have "∃ b. (1/d = b^2 ∧ 1/d ≠ 0) ∨ (1/(c*d) = b^2 ∧ 1/(c*d) ≠ 0)"
using affine_closure[OF ‹delta x1 y1 x2 y2 = 0›
‹e x1 y1 = 0› ‹e x2 y2 = 0›] by blast
then obtain b where "(1/(c*d) = b^2 ∧ 1/(c*d) ≠ 0)"
using ‹¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)› by fastforce
then have "1/c ≠ 0" "c ≠ 0" "d ≠ 0" "1/d ≠ 0" by simp+
then have "1/d = b^2 / (1/c)"
by (metis ‹1 / (c * d) = b⇧2 ∧ 1 / (c * d) ≠ 0› eq_divide_eq semiring_normalization_rules(18))
then have "∃ b. b ≠ 0 ∧ 1/d = b^2"
using assms(3)
by (metis ‹1 / d ≠ 0› power_divide zero_power2)
then show "False"
using ‹¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)› by blast
qed

lemma group_law:
assumes "∃ b. 1/c = b^2" "¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)"
shows "comm_group ⦇carrier = {(x,y). e x y = 0}, mult = add, one = (1,0)⦈"
(is "comm_group ?g")
proof(unfold_locales)
{fix x1 y1 x2 y2
assume "e x1 y1 = 0" "e x2 y2 = 0"
have "e (fst (add (x1,y1) (x2,y2))) (snd (add (x1,y1) (x2,y2))) = 0"
apply(simp)
using add_closure delta_non_zero[OF ‹e x1 y1 = 0› ‹e x2 y2 = 0› assms(1) assms(2)]
delta_def ‹e x1 y1 = 0› ‹e x2 y2 = 0› by auto}
then show "
⋀x y. x ∈ carrier ?g ⟹ y ∈ carrier ?g ⟹
x ⊗⇘?g⇙ y ∈ carrier ?g" by auto
next
{fix x1 y1 x2 y2 x3 y3
assume "e x1 y1 = 0" "e x2 y2 = 0" "e x3 y3 = 0"
then have "delta x1 y1 x2 y2 ≠ 0" "delta x2 y2 x3 y3 ≠ 0"
using assms(1,2) delta_non_zero by blast+
fix x1' y1' x3' y3'
assume "(x1',y1') = add (x1,y1) (x2,y2)"
then have "e x1' y1' = 0" "e x3' y3' = 0"
using add_closure ‹delta x1 y1 x2 y2 ≠ 0› ‹delta x2 y2 x3 y3 ≠ 0›
‹e x1 y1 = 0› ‹e x2 y2 = 0› ‹e x3 y3 = 0› delta_def by fastforce+
then have "delta x1' y1' x3 y3 ≠ 0" "delta x1 y1 x3' y3' ≠ 0"
using assms delta_non_zero ‹e x3 y3 = 0› apply blast
by (simp add: ‹e x1 y1 = 0› ‹e x3' y3' = 0› assms delta_non_zero)

using associativity
by (metis ‹(x1', y1') = add (x1, y1) (x2, y2)› ‹(x3', y3') = add (x2, y2) (x3, y3)› ‹delta x1 y1 x2 y2 ≠ 0›
‹delta x1 y1 x3' y3' ≠ 0› ‹delta x1' y1' x3 y3 ≠ 0› ‹delta x2 y2 x3 y3 ≠ 0› ‹e x1 y1 = 0›
‹e x2 y2 = 0› ‹e x3 y3 = 0› delta_def mult_eq_0_iff)}

then show "
⋀x y z.
x ∈ carrier ?g ⟹ y ∈ carrier ?g ⟹ z ∈ carrier ?g ⟹
x ⊗⇘?g⇙ y ⊗⇘?g⇙ z = x ⊗⇘?g⇙ (y ⊗⇘?g⇙ z)" by auto
next
show "𝟭⇘?g⇙ ∈ carrier ?g" by (simp add: e_def)
next
show "⋀x. x ∈ carrier ?g ⟹ 𝟭⇘?g⇙ ⊗⇘?g⇙ x = x"
next
show "⋀x. x ∈ carrier ?g ⟹ x ⊗⇘?g⇙ 𝟭⇘?g⇙ = x"
next
show "⋀x y. x ∈ carrier ?g ⟹ y ∈ carrier ?g ⟹
x ⊗⇘?g⇙ y = y ⊗⇘?g⇙ x"
using commutativity by auto
next
show "carrier ?g ⊆ Units ?g"
proof(simp,standard)
fix z
assume "z ∈ {(x, y). local.e x y = 0}"
show "z ∈ Units ?g"
unfolding Units_def
proof(simp, cases "z", rule conjI)
fix x y
assume "z = (x,y)"
from this ‹z ∈ {(x, y). local.e x y = 0}›
show "case z of (x, y) ⇒ local.e x y = 0" by blast
then obtain x y where "z = (x,y)" "e x y = 0" by blast
have "e x (-y) = 0"
using ‹e x y = 0› unfolding e_def by simp
have "add (x,y) (x,-y) = (1,0)"
using inverse[OF ‹e x y = 0› ] delta_non_zero[OF ‹e x y = 0› ‹e x y = 0› assms] delta_def by fastforce
then have "add (x,-y) (x,y) = (1,0)" by simp
show "∃a b. e a b = 0 ∧
add (a, b) z = (1, 0) ∧
add z (a, b) = (1, 0)"
using ‹add (x, y) (x, - y) = (1, 0)›
‹e x (- y) = 0› ‹z = (x, y)› by fastforce
qed
qed
qed

end

section‹Extension›

fixes t' :: "'a::ell_field"
assumes c_eq_1: "c = 1"
assumes t_intro: "d = t'^2"
assumes t_ineq: "t'^2 ≠ 1" "t' ≠ 0"
begin

subsection ‹Change of variables›

definition t where "t = t'"

lemma t_nz: "t ≠ 0" using t_ineq(2) t_def by auto

lemma d_nz: "d ≠ 0" using t_nz t_ineq t_intro by simp

lemma t_expr: "t^2 = d" "t^4 = d^2" using t_intro t_def by auto

lemma t_sq_n1: "t^2 ≠ 1"  using t_ineq(1) t_def by simp

lemma t_nm1: "t ≠ -1" using t_sq_n1 by fastforce

lemma d_n1: "d ≠ 1" using t_sq_n1 t_expr by blast

lemma t_n1: "t ≠ 1" using t_sq_n1 by fastforce

lemma t_dneq2: "2*t ≠ -2"
proof(rule ccontr)
assume "¬ 2 * t ≠ - 2"
then have "2*t = -2" by auto
then have "t = -1"
using two_not_zero mult_cancel_left by fastforce
then show "False"
using t_nm1 t_def by argo
qed

subsection ‹New points›

definition e' where "e' x y = x^2 + y^2 - 1 - t^2 * x^2 * y^2"

definition "e'_aff = {(x,y). e' x y = 0}"
definition "e_circ = {(x,y). x ≠ 0 ∧ y ≠ 0 ∧ (x,y) ∈ e'_aff}"

lemma e_e'_iff: "e x y = 0 ⟷ e' x y = 0"
unfolding e_def e'_def using c_eq_1 t_expr(1) t_def by simp

lemma circ_to_aff: "p ∈ e_circ ⟹ p ∈ e'_aff"
unfolding e_circ_def by auto

text‹The case \<^text>‹t^2 = 1› corresponds to a product of intersecting lines
which cannot be a group›

lemma t_2_1_lines:
"t^2 = 1 ⟹ e' x y = - (1 - x^2) * (1 - y^2)"
unfolding e'_def by algebra

text‹The case \<^text>‹t = 0› corresponds to a circle which has been treated before›

lemma t_0_circle:
"t = 0 ⟹ e' x y = x^2 + y^2 - 1"
unfolding e'_def by auto

subsection ‹Group transformations and inversions›

fun ρ :: "'a × 'a ⇒ 'a × 'a" where
"ρ (x,y) = (-y,x)"
fun τ :: "'a × 'a ⇒ 'a × 'a" where
"τ (x,y) = (1/(t*x),1/(t*y))"

definition G where
"G ≡ {id,ρ,ρ ∘ ρ,ρ ∘ ρ ∘ ρ,τ,τ ∘ ρ,τ ∘ ρ ∘ ρ,τ ∘ ρ ∘ ρ ∘ ρ}"

definition symmetries where
"symmetries = {τ,τ ∘ ρ,τ ∘ ρ ∘ ρ,τ ∘ ρ ∘ ρ ∘ ρ}"

definition rotations where
"rotations = {id,ρ,ρ ∘ ρ,ρ ∘ ρ ∘ ρ}"

lemma G_partition: "G = rotations ∪ symmetries"
unfolding G_def rotations_def symmetries_def by fastforce

lemma tau_sq: "(τ ∘ τ) (x,y) = (x,y)" by(simp add: t_nz)

lemma tau_idemp: "τ ∘ τ = id"
using t_nz comp_def by auto

lemma tau_idemp_explicit: "τ(τ(x,y)) = (x,y)"
using tau_idemp pointfree_idE by fast

lemma tau_idemp_point: "τ(τ p) = p"
using o_apply[symmetric, of τ τ p] tau_idemp by simp

fun i :: "'a × 'a ⇒ 'a × 'a" where
"i (a,b) = (a,-b)"

lemma i_idemp: "i ∘ i = id"
using comp_def by auto

lemma i_idemp_explicit: "i(i(x,y)) = (x,y)"
using i_idemp pointfree_idE by fast

lemma tau_rot_sym:
assumes "r ∈ rotations"
shows "τ ∘ r ∈ symmetries"
using assms unfolding rotations_def symmetries_def by auto

lemma tau_rho_com:
"τ ∘ ρ = ρ ∘ τ" by auto

lemma tau_rot_com:
assumes "r ∈ rotations"
shows "τ ∘ r = r ∘ τ"
using assms unfolding rotations_def by fastforce

lemma rho_order_4:
"ρ ∘ ρ ∘ ρ ∘ ρ = id" by auto

lemma rho_i_com_inverses:
"i (id (x,y)) = id (i (x,y))"
"i (ρ (x,y)) = (ρ ∘ ρ ∘ ρ) (i (x,y))"
"i ((ρ ∘ ρ) (x,y)) = (ρ ∘ ρ) (i (x,y))"
"i ((ρ ∘ ρ ∘ ρ) (x,y)) = ρ (i (x,y))"
by(simp)+

lemma rotations_i_inverse:
assumes "tr ∈ rotations"
shows "∃ tr' ∈ rotations. (tr ∘ i) (x,y) = (i ∘ tr') (x,y) ∧ tr ∘ tr' = id"
using assms rho_i_com_inverses unfolding rotations_def by fastforce

lemma tau_i_com_inverses:
"(i ∘ τ) (x,y) = (τ ∘ i) (x,y)"
"(i ∘ τ ∘ ρ) (x,y) = (τ ∘ ρ ∘ ρ ∘ ρ ∘ i) (x,y)"
"(i ∘ τ ∘ ρ ∘ ρ) (x,y) = (τ ∘ ρ ∘ ρ ∘ i) (x,y)"
"(i ∘ τ ∘ ρ ∘ ρ ∘ ρ) (x,y) = (τ ∘ ρ ∘ i) (x,y)"
by(simp)+

lemma rho_circ:
assumes "p ∈ e_circ"
shows "ρ p ∈ e_circ"
using assms unfolding e_circ_def e'_aff_def e'_def

lemma i_aff:
assumes "p ∈ e'_aff"
shows "i p ∈ e'_aff"
using assms unfolding e'_aff_def e'_def by auto

lemma i_circ:
assumes "(x,y) ∈ e_circ"
shows "i (x,y) ∈ e_circ"
using assms unfolding e_circ_def e'_aff_def e'_def by auto

lemma i_circ_points:
assumes "p ∈ e_circ"
shows "i p ∈ e_circ"
using assms unfolding e_circ_def e'_aff_def e'_def by auto

lemma rot_circ:
assumes "p ∈ e_circ" "tr ∈ rotations"
shows "tr p ∈ e_circ"
proof -
consider (1) "tr = id" | (2) "tr = ρ"  | (3) "tr = ρ ∘ ρ" | (4) "tr = ρ ∘ ρ ∘ ρ"
using assms(2) unfolding rotations_def by blast
then show ?thesis by(cases,auto simp add: assms(1) rho_circ)
qed

lemma τ_circ:
assumes "p ∈ e_circ"
shows "τ p ∈ e_circ"
using assms unfolding e_circ_def
apply(simp split: prod.splits)
unfolding e'_aff_def e'_def
apply(simp split: prod.splits)

lemma rot_comp:
assumes "t1 ∈ rotations" "t2 ∈ rotations"
shows "t1 ∘ t2 ∈ rotations"
using assms unfolding rotations_def by auto

lemma rot_tau_com:
assumes "tr ∈ rotations"
shows "tr ∘ τ = τ ∘ tr"
using assms unfolding rotations_def by(auto)

lemma tau_i_com:
"τ ∘ i = i ∘ τ" by auto

lemma rot_com:
assumes "r ∈ rotations" "r' ∈ rotations"
shows "r' ∘ r = r ∘ r'"
using assms unfolding rotations_def by force

lemma rot_inv:
assumes "r ∈ rotations"
shows "∃ r' ∈ rotations. r' ∘ r = id"
using assms unfolding rotations_def by force

lemma rot_aff:
assumes "r ∈ rotations" "p ∈ e'_aff"
shows "r p ∈ e'_aff"
using assms unfolding rotations_def e'_aff_def e'_def

lemma rot_delta:
assumes "r ∈ rotations" "delta x1 y1 x2 y2 ≠ 0"
shows "delta (fst (r (x1,y1))) (snd (r (x1,y1))) x2 y2 ≠ 0"
using assms unfolding rotations_def delta_def delta_plus_def delta_minus_def
apply(safe)
apply(simp)
apply(simp)

lemma tau_not_id: "τ ≠ id"
apply(rule exI[of _ "1"])

lemma sym_not_id:
assumes "r ∈ rotations"
shows "τ ∘ r ≠ id"
using assms unfolding rotations_def
apply(subst fun_eq_iff,simp)
apply(safe)
apply(auto)
apply(rule exI[of _ "1"])
apply(rule exI[of _ "1"])
apply blast
apply(rule exI[of _ "1"])
using t_nm1 apply presburger
using t_ineq(2) by blast

lemma sym_decomp:
assumes "g ∈ symmetries"
shows "∃ r ∈ rotations. g = τ ∘ r"
using assms unfolding symmetries_def rotations_def by auto

lemma symmetries_i_inverse:
assumes "tr ∈ symmetries"
shows "∃ tr' ∈ symmetries. (tr ∘ i) (x,y) = (i ∘ tr') (x,y) ∧ tr ∘ tr' = id"
proof -
consider (1) "tr = τ" |
(2) "tr = τ ∘ ρ" |
(3) "tr = τ ∘ ρ ∘ ρ" |
(4) "tr = τ ∘ ρ ∘ ρ ∘ ρ"
using assms unfolding symmetries_def by blast
then show ?thesis
proof(cases)
case 1
define tr' where "tr' = τ"
have "(tr ∘ i) (x, y) = (i ∘ tr') (x, y) ∧ tr ∘ tr' = id" "tr' ∈ symmetries"
using tr'_def 1 tau_idemp symmetries_def by simp+
then show ?thesis by blast
next
case 2
define tr' where "tr' = τ ∘ ρ ∘ ρ ∘ ρ"
have "(tr ∘ i) (x, y) = (i ∘ tr') (x, y) ∧ tr ∘ tr' = id" "tr' ∈ symmetries"
using tr'_def 2
apply(simp)
using tau_idemp_point apply fastforce
using symmetries_def tr'_def by simp
then show ?thesis by blast
next
case 3
define tr' where "tr' = τ ∘ ρ ∘ ρ"
have "(tr ∘ i) (x, y) = (i ∘ tr') (x, y) ∧ tr ∘ tr' = id" "tr' ∈ symmetries"
using tr'_def 3
apply(simp)
using tau_idemp_point apply fastforce
using symmetries_def tr'_def by simp
then show ?thesis by blast
next
case 4
define tr' where "tr' = τ ∘ ρ"
have "(tr ∘ i) (x, y) = (i ∘ tr') (x, y) ∧ tr ∘ tr' = id" "tr' ∈ symmetries"
using tr'_def 4
apply(simp)
using tau_idemp_point apply fastforce
using symmetries_def tr'_def by simp
then show ?thesis by blast
qed
qed

lemma sym_to_rot: "g ∈ symmetries ⟹ τ ∘ g ∈ rotations"
using tau_idemp unfolding symmetries_def rotations_def
apply(simp)
apply(elim disjE)
apply fast

fun ext_add :: "'a × 'a ⇒ 'a × 'a ⇒ 'a × 'a" where
((x1*y1-x2*y2) div (x2*y1-x1*y2),
(x1*y1+x2*y2) div (x1*x2+y1*y2))"

definition delta_x :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta_x x1 y1 x2 y2 = x2*y1 - x1*y2"
definition delta_y :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta_y x1 y1 x2 y2 = x1*x2 + y1*y2"
definition delta' :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"delta' x1 y1 x2 y2 = delta_x x1 y1 x2 y2 * delta_y x1 y1 x2 y2"

lemma delta'_com: "(delta' x0 y0 x1 y1 = 0) = (delta' x1 y1 x0 y0 = 0)"
unfolding delta'_def delta_x_def delta_y_def
by algebra

definition e'_aff_0 where
"e'_aff_0 = {((x1,y1),(x2,y2)). (x1,y1) ∈ e'_aff ∧
(x2,y2) ∈ e'_aff ∧
delta x1 y1 x2 y2 ≠ 0 }"

definition e'_aff_1 where
"e'_aff_1 = {((x1,y1),(x2,y2)). (x1,y1) ∈ e'_aff ∧
(x2,y2) ∈ e'_aff ∧
delta' x1 y1 x2 y2 ≠ 0 }"

apply(subst (1 3 4 6) surjective_pairing)
by presburger

"x ≠ 0 ⟹ y ≠ 0 ⟹ ext_add (x,y) (i (x,y)) = (1,0)"

((delta_x x2 y1 x1 y2) div (delta_x x1 y1 x2 y2),
(delta_y x1 x2 y1 y2) div (delta_y x1 y1 x2 y2))"
unfolding delta_x_def delta_y_def by simp

subsubsection ‹Inversion and rotation invariance›

lemma inversion_invariance_1:
assumes "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
apply(simp)
apply(subst c_eq_1)+
apply(subst power2_eq_square[symmetric])+
apply(subst t_expr)+
apply(rule conjI)
apply(simp_all add: divide_simps assms t_nz d_nz)

lemma inversion_invariance_2:
assumes "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
by algebra

lemma rho_invariance_1:
apply(simp)
apply(subst c_eq_1)+

lemma rho_invariance_1_points:
using rho_invariance_1
apply(subst (2 4 6 8) surjective_pairing)
by blast

lemma rho_invariance_2:

lemma rho_invariance_2_points:
using rho_invariance_2
apply(subst (2 4 6 8) surjective_pairing)
by blast

lemma rotation_invariance_1:
assumes "r ∈ rotations"
using rho_invariance_1_points assms unfolding rotations_def
apply(safe)
apply(simp)
apply(simp)

lemma rotation_invariance_1_points:
assumes "r ∈ rotations"
using rotation_invariance_1 assms
unfolding rotations_def
apply(safe)
apply(simp,simp)
using rho_invariance_1_points by auto

lemma rotation_invariance_2:
assumes "r ∈ rotations"
using rho_invariance_2_points assms unfolding rotations_def
apply(safe)
apply(simp,simp)

lemma rotation_invariance_2_points:
assumes "r ∈ rotations"
using rotation_invariance_2 assms
unfolding rotations_def
apply(safe)
apply(simp,simp)
using rho_invariance_2_points by auto

lemma rotation_invariance_3:
"delta x1 y1 (fst (ρ (x2,y2))) (snd (ρ (x2,y2))) =
delta x1 y1 x2 y2"

lemma rotation_invariance_4:
"delta' x1 y1 (fst (ρ (x2,y2))) (snd (ρ (x2,y2))) = - delta' x1 y1 x2 y2"

lemma rotation_invariance_5:
"delta' (fst (ρ (x1,y1))) (snd (ρ (x1,y1))) x2 y2 = - delta' x1 y1 x2 y2"

lemma rotation_invariance_6:
"delta (fst (ρ (x1,y1))) (snd (ρ (x1,y1))) x2 y2 = delta x1 y1 x2 y2"
by(simp add: delta_def delta_plus_def delta_minus_def, algebra)

lemma inverse_rule_1:
"(τ ∘ i ∘ τ) (x,y) = i (x,y)" by (simp add: t_nz)
lemma inverse_rule_2:
"(ρ ∘ i ∘ ρ) (x,y) = i (x,y)" by simp
lemma inverse_rule_3:
lemma inverse_rule_4:

(* This kind of lemma may vary with different fields *)
lemma e'_aff_x0:
assumes "x = 0" "(x,y) ∈ e'_aff"
shows "y = 1 ∨ y = -1"
using assms unfolding e'_aff_def e'_def
by(simp,algebra)

lemma e'_aff_y0:
assumes "y = 0" "(x,y) ∈ e'_aff"
shows "x = 1 ∨ x = -1"
using assms unfolding e'_aff_def e'_def
by(simp,algebra)

(*
Note that this proof does not go through in the general case (as written in the paper)
thus, dichotomy will have to rule out some cases.
*)
assumes "x1 ≠ 0" "y1 ≠ 0"
apply(simp)
apply(rule conjI)
apply(simp add: divide_simps t_nz power2_eq_square[symmetric] assms t_expr(1) d_nz)
apply (simp add: semiring_normalization_rules(18) semiring_normalization_rules(29) t_intro)
apply(simp add: divide_simps t_nz power2_eq_square[symmetric] assms t_expr(1) d_nz)

assumes "x1 ≠ 0" "y1 ≠ 0"
proof -
obtain x1' y1' where tau_expr: "τ (x1,y1) = (x1',y1')" by simp
then have p_nz: "x1' ≠ 0" "y1' ≠ 0"
using assms(1) tau_sq apply auto[1]
using ‹τ (x1, y1) = (x1', y1')› assms(2) tau_sq by auto
using c_eq_1 tau_expr tau_idemp_point by auto
also have "... = τ (ext_add (x1', y1') (x2, y2))"
also have "... = τ (ext_add (τ (x1, y1)) (x2, y2))"
using tau_expr tau_idemp by auto
finally show ?thesis by blast
qed

subsubsection ‹Coherence and closure›

lemma coherence_1:
assumes "delta_x x1 y1 x2 y2 ≠ 0" "delta_minus x1 y1 x2 y2 ≠ 0"
assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
shows "delta_x x1 y1 x2 y2 * delta_minus x1 y1 x2 y2 *
= x2 * y2 * e' x1 y1 - x1 * y1 * e' x2 y2"
apply(simp)
apply(rewrite in "_ / ⌑" delta_x_def[symmetric])
apply(rewrite in "_ / ⌑" delta_minus_def[symmetric])
unfolding delta_minus_def delta_x_def e'_def

lemma coherence_2:
assumes "delta_y x1 y1 x2 y2 ≠ 0" "delta_plus x1 y1 x2 y2 ≠ 0"
assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
shows "delta_y x1 y1 x2 y2 * delta_plus x1 y1 x2 y2 *
= - x2 * y2 * e' x1 y1 - x1 * y1 * e' x2 y2"
apply(simp)
apply(rewrite in "_ / ⌑" delta_y_def[symmetric])
apply(rewrite in "_ / ⌑" delta_plus_def[symmetric])
unfolding delta_plus_def delta_y_def e'_def
apply(subst t_expr)+

lemma coherence:
assumes "delta x1 y1 x2 y2 ≠ 0" "delta' x1 y1 x2 y2 ≠ 0"
assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
using coherence_1 coherence_2 delta_def delta'_def assms by auto

assumes "delta' x1 y1 x2 y2 ≠ 0"
assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
assumes "(x3,y3) = ext_add (x1,y1) (x2,y2)"
shows "e' x3 y3 = 0"
proof -
have deltas_nz: "delta_x x1 y1 x2 y2 ≠ 0"
"delta_y x1 y1 x2 y2 ≠ 0"
using assms(1) delta'_def by auto

have v3: "x3 = fst (ext_add (x1,y1) (x2,y2))"
"y3 = snd (ext_add (x1,y1) (x2,y2))"
using assms(4) by simp+

have "∃ a b. t^4 * (delta_x x1 y1 x2 y2)^2 * (delta_y x1 y1 x2 y2)^2 * e' x3 y3 =
a * e' x1 y1 + b * e' x2 y2"
using deltas_nz
unfolding e'_def v3 delta_x_def delta_y_def
by algebra

then show "e' x3 y3 = 0"
using assms(2,3) deltas_nz t_nz by auto
qed

assumes "delta' x1 y1 x2 y2 ≠ 0"
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
shows "ext_add (x1,y1) (x2,y2) ∈ e'_aff"
unfolding e'_aff_def by auto

subsubsection ‹Useful lemmas in the extension›

lemma inverse_generalized:
assumes "(a,b) ∈ e'_aff" "delta_plus a b a b ≠ 0"
shows "add (a,b) (a,-b) = (1,0)"
using inverse assms
unfolding e'_aff_def
using e_e'_iff
by(simp)

lemma inverse_generalized_points:
assumes "p ∈ e'_aff" "delta_plus (fst p) (snd p) (fst p) (snd p) ≠ 0"
shows "add p (i p) = (1,0)"
using inverse assms
unfolding e'_aff_def
using e_e'_iff e'_aff_def by auto

assumes "delta x y x' y' ≠ 0"
"(x,y) ∈ e'_aff" "(x',y') ∈ e'_aff"
shows "add (x,y) (x',y') ∈ e'_aff"
unfolding delta_def e'_aff_def by auto

assumes in_aff: "(x,y) ∈ e'_aff"
shows "delta x y x (-y) ≠ 0 ∨ delta' x y x (-y) ≠ 0 "
using in_aff d_n1
unfolding delta_def delta_plus_def delta_minus_def
delta'_def delta_x_def delta_y_def
e'_aff_def e'_def
apply(safe)

subsection ‹Delta arithmetic›

lemma mix_tau:
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff" "x2 ≠ 0" "y2 ≠ 0"
assumes "delta' x1 y1 x2 y2 ≠ 0" "delta' x1 y1 (fst (τ (x2,y2))) (snd (τ (x2,y2))) ≠ 0"
shows "delta x1 y1 x2 y2 ≠ 0"
using assms
unfolding e'_aff_def e'_def delta_def delta_plus_def delta_minus_def delta'_def delta_y_def delta_x_def
apply(simp)
by algebra

lemma mix_tau_0:
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff" "x2 ≠ 0" "y2 ≠ 0"
assumes "delta x1 y1 x2 y2 = 0"
shows "delta' x1 y1 x2 y2 = 0 ∨ delta' x1 y1 (fst (τ (x2,y2))) (snd (τ (x2,y2))) = 0"
using assms
unfolding e'_aff_def e'_def delta_def delta_plus_def delta_minus_def delta'_def delta_y_def delta_x_def
apply(simp)
by algebra

lemma mix_tau_prime:
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff" "x2 ≠ 0" "y2 ≠ 0"
assumes "delta x1 y1 x2 y2 ≠ 0" "delta x1 y1 (fst (τ (x2,y2))) (snd (τ (x2,y2))) ≠ 0"
shows "delta' x1 y1 x2 y2 ≠ 0"
using assms
unfolding e'_aff_def e'_def delta_def delta_plus_def delta_minus_def delta'_def delta_y_def delta_x_def
apply(simp)
by algebra

lemma tau_tau_d:
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes "delta (fst (τ (x1,y1))) (snd (τ (x1,y1))) (fst (τ (x2,y2))) (snd (τ (x2,y2))) ≠ 0"
shows "delta x1 y1 x2 y2 ≠ 0"
using assms
unfolding e'_aff_def e'_def delta_def delta_plus_def delta_minus_def delta'_def delta_y_def delta_x_def
apply(simp)
apply(simp split: if_splits add: divide_simps t_nz)
apply(simp_all add: t_nz algebra_simps power2_eq_square[symmetric] t_expr d_nz)
apply algebra
by algebra

lemma tau_tau_d':
assumes "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes "delta' (fst (τ (x1,y1))) (snd (τ (x1,y1))) (fst (τ (x2,y2))) (snd (τ (x2,y2))) ≠ 0"
shows "delta' x1 y1 x2 y2 ≠ 0"
using assms
unfolding e'_aff_def e'_def delta_def delta_plus_def delta_minus_def delta'_def delta_y_def delta_x_def
apply(simp)
apply(simp split: if_splits add: divide_simps t_nz)
apply fastforce
apply algebra
by algebra

assumes 1: "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
assumes r_expr: "rx = fst (add (x1,y1) (x2,y2))" "ry = snd (add (x1,y1) (x2,y2))"
assumes in_aff: "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes pd: "delta x1 y1 x2 y2 ≠ 0"
assumes pd': "delta rx ry (fst (τ (i (x2,y2)))) (snd (τ (i (x2,y2)))) ≠ 0"
shows "delta' rx ry (fst (i (x2,y2))) (snd (i (x2,y2))) ≠ 0"
using pd' unfolding delta_def delta_minus_def delta_plus_def
delta'_def delta_x_def delta_y_def
apply(simp split: if_splits add: field_simps t_nz 1 power2_eq_square[symmetric] t_expr d_nz)
using pd in_aff unfolding r_expr delta_def delta_minus_def delta_plus_def
e'_aff_def e'_def
by algebra

assumes 1: "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
assumes r_expr: "rx = fst (ext_add (x1,y1) (x2,y2))" "ry = snd (ext_add (x1,y1) (x2,y2))"
assumes in_aff: "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes pd': "delta' rx ry (fst (τ (i (x2,y2)))) (snd (τ (i (x2,y2)))) ≠ 0"
shows "delta rx ry (fst (i (x2,y2))) (snd (i (x2,y2))) ≠ 0"
using pd' unfolding delta_def delta_minus_def delta_plus_def
delta'_def delta_x_def delta_y_def
apply(simp split: if_splits add: field_simps t_nz 1 power2_eq_square[symmetric] t_expr d_nz)
using in_aff unfolding r_expr delta_def delta_minus_def delta_plus_def
e'_aff_def e'_def
apply(simp split: if_splits add: divide_simps t_expr)
by algebra

(* These lemmas are needed in the general field setting.
Funnily enough, if we drop assumptions the goal is proven, but
with more assumptions as in delta_add_delta', is not*)
lemma funny_field_lemma_1:
"((x1 * x2 - y1 * y2) * ((x1 * x2 - y1 * y2) * (x2 * (y2 * (1 + d * x1 * y1 * x2 * y2)))) +
(x1 * x2 - y1 * y2) * ((x1 * y2 + y1 * x2) * y2⇧2) * (1 - d * x1 * y1 * x2 * y2)) *
(1 + d * x1 * y1 * x2 * y2) ≠
((x1 * y2 + y1 * x2) * ((x1 * y2 + y1 * x2) * (x2 * (y2 * (1 - d * x1 * y1 * x2 * y2)))) +
(x1 * x2 - y1 * y2) * ((x1 * y2 + y1 * x2) * x2⇧2) * (1 + d * x1 * y1 * x2 * y2)) *
(1 - d * x1 * y1 * x2 * y2) ⟹
(d * ((x1 * x2 - y1 * y2) * ((x1 * y2 + y1 * x2) * (x2 * y2))))⇧2 =
((1 - d * x1 * y1 * x2 * y2) * (1 + d * x1 * y1 * x2 * y2))⇧2 ⟹
x1⇧2 + y1⇧2 - 1 = d * x1⇧2 * y1⇧2 ⟹
x2⇧2 + y2⇧2 - 1 = d * x2⇧2 * y2⇧2  ⟹ False"
by algebra

assumes 1: "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
assumes r_expr: "rx = fst (add (x1,y1) (x2,y2))" "ry = snd (add (x1,y1) (x2,y2))"
assumes in_aff: "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes pd: "delta x1 y1 x2 y2 ≠ 0"
assumes pd': "delta' rx ry (fst (τ (i (x2,y2)))) (snd (τ (i (x2,y2)))) ≠ 0"
shows "delta rx ry (fst (i (x2,y2))) (snd (i (x2,y2))) ≠ 0"
using pd' unfolding delta_def delta_minus_def delta_plus_def
delta'_def delta_x_def delta_y_def
apply(simp split: if_splits add: algebra_simps divide_simps t_nz 1 power2_eq_square[symmetric] t_expr d_nz)
apply safe
using pd unfolding r_expr delta_def delta_minus_def delta_plus_def
apply(simp)
using in_aff unfolding e'_aff_def e'_def
apply(rule funny_field_lemma_1)
by simp

(* These lemmas are needed in the general field setting.
Funnily enough, if we drop assumptions the goal is proven, but
with more assumptions as in delta_add_delta', is not*)
lemma funny_field_lemma_2: " (x2 * y2)⇧2 * ((x2 * y1 - x1 * y2) * (x1 * x2 + y1 * y2))⇧2 ≠ ((x1 * y1 - x2 * y2) * (x1 * y1 + x2 * y2))⇧2 ⟹
((x1 * y1 - x2 * y2) * ((x1 * y1 - x2 * y2) * (x2 * (y2 * (x1 * x2 + y1 * y2)))) +
(x1 * y1 - x2 * y2) * ((x1 * y1 + x2 * y2) * x2⇧2) * (x2 * y1 - x1 * y2)) *
(x1 * x2 + y1 * y2) =
((x1 * y1 + x2 * y2) * ((x1 * y1 + x2 * y2) * (x2 * (y2 * (x2 * y1 - x1 * y2)))) +
(x1 * y1 - x2 * y2) * ((x1 * y1 + x2 * y2) * y2⇧2) * (x1 * x2 + y1 * y2)) *
(x2 * y1 - x1 * y2) ⟹
x1⇧2 + y1⇧2 - 1 = d * x1⇧2 * y1⇧2 ⟹
x2⇧2 + y2⇧2 - 1 = d * x2⇧2 * y2⇧2 ⟹ False"
by algebra

assumes 1: "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
assumes r_expr: "rx = fst (ext_add (x1,y1) (x2,y2))" "ry = snd (ext_add (x1,y1) (x2,y2))"
assumes in_aff: "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes pd: "delta' x1 y1 x2 y2 ≠ 0"
assumes pd': "delta rx ry (fst (τ (i (x2,y2)))) (snd (τ (i (x2,y2)))) ≠ 0"
shows "delta' rx ry (fst (i (x2,y2))) (snd (i (x2,y2))) ≠ 0"
using pd' unfolding delta_def delta_minus_def delta_plus_def
delta'_def delta_x_def delta_y_def
apply(simp split: if_splits add: algebra_simps divide_simps t_nz 1 power2_eq_square[symmetric] t_expr d_nz)
apply safe
using pd unfolding r_expr delta'_def delta_x_def delta_y_def
apply(simp)
apply(simp split: if_splits add: c_eq_1 divide_simps)
using in_aff unfolding e'_aff_def e'_def
apply(rule funny_field_lemma_2)

assumes 1: "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
assumes in_aff: "(x1,y1) ∈ e'_aff" "(x2,y2) ∈ e'_aff"
assumes pd: "delta' x1 y1 x2 y2 ≠ 0"
shows pd': "delta (fst (τ (x1,y1))) (snd (τ (x1,y1))) x2 y2 ≠ 0"
unfolding delta_def delta_minus_def delta_plus_def
apply(simp add: algebra_simps power2_eq_square[symmetric] t_expr d_nz)
using d_nz by algebra

assumes in_aff: "(x,y) ∈ e'_aff" "x ≠ 0" "y ≠ 0"
shows "delta x y (fst (τ (i (x,y)))) (snd (τ (i (x,y)))) = 0"
"delta' x y (fst (τ (i (x,y)))) (snd (τ (i (x,y)))) = 0"
using in_aff d_n1
unfolding delta_def delta_plus_def delta_minus_def
delta'_def delta_x_def delta_y_def
e'_aff_def e'_def
apply(safe)
by(simp_all add: algebra_simps t_nz power2_eq_square[symmetric] t_expr)

section ‹Projective Edwards curves›

subsection ‹No fixed-point lemma and dichotomies›

lemma g_no_fp:
assumes "g ∈ G" "p ∈ e_circ" "g p = p"
shows "g = id"
proof -
obtain x y where p_def: "p = (x,y)" by fastforce
have nz: "x ≠ 0" "y ≠ 0" using assms p_def  unfolding e_circ_def by auto

consider (id) "g = id" | (rot) "g ∈ rotations" "g ≠ id" | (sym) "g ∈ symmetries" "g ≠ id"
using G_partition assms by blast
then show ?thesis
proof(cases)
case id then show ?thesis by simp
next
case rot
then have "x = 0"
using assms(3) two_not_zero
unfolding rotations_def p_def
by auto
then have "False"
using nz by blast
then show ?thesis by blast
next
case sym
then have "t*x*y = 0 ∨ (t*x^2 ∈ {-1,1} ∧ t*y^2 ∈ {-1,1} ∧ t*x^2 = t*y^2)"
using assms(3) two_not_zero
unfolding symmetries_def p_def power2_eq_square
apply(safe)
using two_not_zero by metis+
then have "e' x y = 2 * (1 - t) / t ∨ e' x y = 2 * (-1 - t) / t"
using nz t_nz unfolding e'_def
then have "e' x y ≠ 0"
using t_dneq2 t_n1
then have "False"
using assms nz p_def unfolding e_circ_def e'_aff_def by fastforce
then show ?thesis by simp
qed
qed

lemma dichotomy_1:
assumes "p ∈ e'_aff" "q ∈ e'_aff"
shows "(p ∈ e_circ ∧ (∃ g ∈ symmetries. q = (g ∘ i) p)) ∨
(p,q) ∈ e'_aff_0 ∨ (p,q) ∈ e'_aff_1"
proof -
obtain x1 y1 where p_def: "p = (x1,y1)" by fastforce
obtain x2 y2 where q_def: "q = (x2,y2)" by fastforce

consider (1) "(p,q) ∈ e'_aff_0" |
(2) "(p,q) ∈ e'_aff_1" |
(3) "(p,q) ∉ e'_aff_0 ∧ (p,q) ∉ e'_aff_1" by blast
then show ?thesis
proof(cases)
case 1 then show ?thesis by blast
next
case 2 then show ?thesis by simp
next
case 3
then have "delta x1 y1 x2 y2 = 0" "delta' x1 y1 x2 y2 = 0"
unfolding p_def q_def e'_aff_0_def e'_aff_1_def using assms
by (simp add: assms p_def q_def)+
have "x1 ≠ 0" "y1 ≠ 0" "x2 ≠ 0" "y2 ≠ 0"
using ‹delta x1 y1 x2 y2 = 0›
unfolding delta_def delta_plus_def delta_minus_def by auto
then have "p ∈ e_circ" "q ∈ e_circ"
unfolding e_circ_def using assms p_def q_def by blast+

obtain a0 b0 where tq_expr: "τ q = (a0,b0)" by fastforce
obtain a1 b1 where p_expr: "p = (a1,b1)" by fastforce
from tq_expr have q_expr: "q = τ (a0,b0)" using tau_idemp_explicit q_def by auto

have a0_nz: "a0 ≠ 0" "b0 ≠ 0"
using ‹τ q = (a0, b0)› ‹x2 ≠ 0› ‹y2 ≠ 0› comp_apply q_def tau_sq by auto

have a1_nz: "a1 ≠ 0" "b1 ≠ 0"
using ‹p = (a1, b1)› ‹x1 ≠ 0› ‹y1 ≠ 0› p_def by auto

have in_aff: "(a0,b0) ∈ e'_aff" "(a1,b1) ∈ e'_aff"
using ‹q ∈ e_circ› τ_circ circ_to_aff tq_expr apply fastforce
using assms(1) p_expr by auto

define δ' :: "'a ⇒ 'a ⇒ 'a" where
"δ'= (λ x0 y0. x0 * y0 * ```