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"

locale curve_addition =  
  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
 "add (x1,y1) (x2,y2) =
    ((x1*x2 - c*y1*y2) div (1-d*x1*y1*x2*y2), 
     (x1*y2+y1*x2) div (1+d*x1*y1*x2*y2))"

lemma commutativity: "add z1 z2 = add z2 z1"
  by(cases "z1",cases "z2",simp add: algebra_simps)

lemma add_closure: 
  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
    apply(simp add: divide_simps assms)    
    unfolding delta_plus_def delta_minus_def 
    by algebra
  then show "e x3 y3 = 0" 
    using assms 
    by (simp add: delta_def)
qed

lemma associativity: 
  assumes "z1' = (x1',y1')" "z3' = (x3',y3')"
  assumes "z1' = add (x1,y1) (x2,y2)" "z3' = add (x2,y2) (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" 
  shows "add (add (x1,y1) (x2,y2)) (x3,y3) = add (x1,y1) (add (x2,y2) (x3,y3))" 
proof -
  define e1 where "e1 = e x1 y1"
  define e2 where "e2 = e x2 y2"
  define e3 where "e3 = e x3 y3"
  define Deltax where "Deltax = 
   (delta_minus x1' y1' x3 y3)*(delta_minus x1 y1 x3' y3')*
   (delta x1 y1 x2 y2)*(delta x2 y2 x3 y3)" 
  define Deltay where "Deltay =
   (delta_plus x1' y1' x3 y3)*(delta_plus x1 y1 x3' y3')*
   (delta x1 y1 x2 y2)*(delta x2 y2 x3 y3)" 
  define gx where "gx = fst(add z1' (x3,y3)) - fst(add (x1,y1) z3')"
  define gy where "gy = snd(add z1' (x3,y3)) - snd(add (x1,y1) z3')"
  define gxpoly where "gxpoly = gx * Deltax"
  define gypoly where "gypoly = gy * Deltay"

  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
  
  have non_unfolded_adds:
      "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
    by(simp add: divide_simps assms(5-8))

  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
    by(simp add: divide_simps assms(5-8))

  have " r1 r2 r3. gxpoly = r1 * e1 + r2 * e2 + r3 * e3"
    unfolding gxpoly_def gx_def Deltax_def 
    apply(simp add: assms(1,2))
    apply(rewrite in "_ / " delta_minus_def[symmetric])+
    apply(simp add: divide_simps assms(9,11))
    apply(rewrite left_diff_distrib)
    apply(simp add: simp1gx simp2gx)
    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 "Deltax  0" 
    using Deltax_def delta_def assms(7-11) non_unfolded_adds by auto
  then have "gx = 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
    by(simp add: divide_simps assms(5-8))
    
  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
    by(simp add: divide_simps assms(5-8))

  have " r1 r2 r3. gypoly = r1 * e1 + r2 * e2 + r3 * e3"
    unfolding gypoly_def gy_def Deltay_def 
    apply(simp add: assms(1,2))
    apply(rewrite in "_ / " delta_plus_def[symmetric])+
    apply(simp add: divide_simps assms(10,12))
    apply(rewrite left_diff_distrib)
    apply(simp add: simp1gy simp2gy)
    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 "Deltay  0" 
    using Deltay_def delta_def assms(7-12) non_unfolded_adds by auto
  then have "gy = 0" 
    using gypoly = 0 gypoly_def by auto

  show ?thesis 
    using gy = 0 gx = 0 
    unfolding gx_def gy_def assms(3,4)
    by (simp add: prod_eq_iff)
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 
  apply(simp add: delta_plus_def e_def) 
  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)"
   apply(simp add: divide_simps)
   by (metis 1 / (c * d) = b2  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 ?gy  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)"
          "(x3',y3') = add (x2,y2) (x3,y3)"
   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)

  have "add (add (x1,y1) (x2,y2)) (x3,y3) =
        add (x1,y1) (local.add (x2,y2) (x3,y3))"
    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 ?gy ?gz = x ?g(y ?gz)" by auto
next
  show "𝟭?g carrier ?g" by (simp add: e_def)
next
  show "x. x  carrier ?g  𝟭?g?gx = x"
    by (simp add: commutativity neutral)
next
  show "x. x  carrier ?g  x ?g𝟭?g= x"
    by (simp add: neutral)
next
  show "x y. x  carrier ?g  y  carrier ?g 
           x ?gy = y ?gx"
    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›

locale ext_curve_addition = curve_addition +
  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 
  by(simp split: prod.splits add: add.commute)

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) 
  apply(simp add: divide_simps t_nz)
  unfolding e'_aff_def e'_def
  apply(simp split: prod.splits) 
  apply(simp add: divide_simps t_nz)
  by(simp add: algebra_simps)

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
  by(auto simp add: semiring_normalization_rules(16) add.commute)
 
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 add: semiring_normalization_rules(16))
  apply(simp)
  by(simp add: add_eq_0_iff equation_minus_iff semiring_normalization_rules(16))

lemma tau_not_id: "τ  id"
  apply(simp add: fun_eq_iff) 
  apply(simp add: divide_simps t_nz) 
  apply(simp add: field_simps)
  apply(rule exI[of _ "1"])
  by(simp add: t_n1)

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(simp_all add: divide_simps )
     apply(rule exI[of _ "1"])
     apply (simp add: t_n1)
    apply(rule exI[of _ "1"])
    apply(simp add: d_nz)  
  apply blast
    apply(rule exI[of _ "1"])
   apply(simp add: d_nz)
  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
  by(simp add: fun.map_comp)+

subsection ‹Extended addition›

fun ext_add :: "'a × 'a  'a × 'a  'a × 'a" where
 "ext_add (x1,y1) (x2,y2) =
    ((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 }"

lemma ext_add_comm:
  "ext_add (x1,y1) (x2,y2) = ext_add (x2,y2) (x1,y1)"
  by(simp add: divide_simps,algebra) 

lemma ext_add_comm_points:
  "ext_add z1 z2 = ext_add z2 z1"
  using ext_add_comm 
  apply(subst (1 3 4 6) surjective_pairing)
  by presburger

lemma ext_add_inverse:
  "x  0  y  0  ext_add (x,y) (i (x,y)) = (1,0)"
  by(simp add: two_not_zero)

lemma ext_add_deltas:
  "ext_add (x1,y1) (x2,y2) =
    ((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" 
  shows "add (τ (x1,y1)) (x2,y2) = add (x1,y1) (τ (x2,y2))"
  apply(simp)
  apply(subst c_eq_1)+
  apply(simp add: algebra_simps)
  apply(subst power2_eq_square[symmetric])+
  apply(subst t_expr)+
  apply(rule conjI)
  apply(simp_all add: divide_simps assms t_nz d_nz)
  by(simp_all add: algebra_simps)



lemma inversion_invariance_2:
  assumes "x1  0" "y1  0" "x2  0" "y2  0" 
  shows "ext_add (τ (x1,y1)) (x2,y2) = ext_add (x1,y1) (τ (x2,y2))"
  apply(simp add: divide_simps t_nz assms) 
  by algebra

lemma rho_invariance_1: 
  "add (ρ (x1,y1)) (x2,y2) = ρ (add (x1,y1) (x2,y2))"
  apply(simp)
  apply(subst c_eq_1)+
  apply(simp add: divide_simps)
  by(simp add: algebra_simps)

lemma rho_invariance_1_points:
  "add (ρ p1) p2 = ρ (add p1 p2)"
  using rho_invariance_1 
  apply(subst (2 4 6 8) surjective_pairing)
  by blast

lemma rho_invariance_2: 
  "ext_add (ρ (x1,y1)) (x2,y2) = 
   ρ (ext_add (x1,y1) (x2,y2))"
  apply(simp add: divide_simps)
  by(simp add: algebra_simps)

lemma rho_invariance_2_points:
  "ext_add (ρ p1) p2 = ρ (ext_add p1 p2)"
  using rho_invariance_2
  apply(subst (2 4 6 8) surjective_pairing)
  by blast

lemma rotation_invariance_1: 
  assumes "r  rotations"
  shows "add (r (x1,y1)) (x2,y2) = r (add (x1,y1) (x2,y2))"
  using rho_invariance_1_points assms unfolding rotations_def
  apply(safe)
  apply(simp)
  apply(simp)
  apply(simp add: divide_simps)
  apply(simp add: divide_simps)
  apply(simp add: algebra_simps)
  by (simp add: c_eq_1)

lemma rotation_invariance_1_points: 
  assumes "r  rotations"
  shows "add (r p1) p2 = r (add p1 p2)"
  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"
  shows "ext_add (r (x1,y1)) (x2,y2) = r (ext_add (x1,y1) (x2,y2))"
  using rho_invariance_2_points assms unfolding rotations_def
  apply(safe)
  apply(simp,simp) 
  apply(simp add: divide_simps)
  apply(simp add: algebra_simps)
  apply (simp add: add_eq_0_iff)
  apply(simp add: divide_simps)
  apply(simp add: algebra_simps)
  using neg_eq_iff_add_eq_0 by blast

lemma rotation_invariance_2_points: 
  assumes "r  rotations"
  shows "ext_add (r p1) p2 = r (ext_add p1 p2)"
  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"
  by(simp add: delta_def delta_plus_def delta_minus_def,algebra)

lemma rotation_invariance_4: 
  "delta' x1 y1 (fst (ρ (x2,y2))) (snd (ρ (x2,y2))) = - delta' x1 y1 x2 y2"
  by(simp add: delta'_def delta_x_def delta_y_def,algebra)

lemma rotation_invariance_5: 
  "delta' (fst (ρ (x1,y1))) (snd (ρ (x1,y1))) x2 y2 = - delta' x1 y1 x2 y2"
  by(simp add: delta'_def delta_x_def delta_y_def,algebra)

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:
  "i (add (x1,y1) (x2,y2)) = add (i (x1,y1)) (i (x2,y2))"
  by(simp add: divide_simps)
lemma inverse_rule_4:
  "i (ext_add (x1,y1) (x2,y2)) = ext_add (i (x1,y1)) (i (x2,y2))"
  apply(simp add: divide_simps)
  by(simp add: algebra_simps)

(* 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.
*)
lemma add_ext_add:
  assumes "x1  0" "y1  0" 
  shows "ext_add (x1,y1) (x2,y2) = τ (add (τ (x1,y1)) (x2,y2))"
  apply(simp)
  apply(rule conjI)
  apply(simp add: c_eq_1)
  apply(simp add: divide_simps t_nz power2_eq_square[symmetric] assms t_expr(1) d_nz)
  apply(simp add: algebra_simps power2_eq_square[symmetric] t_expr(1)) 
  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)
  apply(simp add: algebra_simps power2_eq_square[symmetric] t_expr(1))  
  by (simp add: power2_eq_square t_intro)

corollary add_ext_add_2:
  assumes "x1  0" "y1  0" 
  shows "add (x1,y1) (x2,y2) = τ (ext_add (τ (x1,y1)) (x2,y2))"
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
  have "add (x1,y1) (x2,y2) = add (τ (x1', y1')) (x2, y2)"
    using c_eq_1 tau_expr tau_idemp_point by auto
  also have "... = τ (ext_add (x1', y1') (x2, y2))"
    using add_ext_add[OF p_nz] tau_idemp by simp
  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 *
         (fst (ext_add (x1,y1) (x2,y2)) - fst (add (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])
  apply(simp add: c_eq_1 assms(1,2) divide_simps)
  unfolding delta_minus_def delta_x_def e'_def
  apply(simp add: t_expr)
  by(simp add: power2_eq_square field_simps)  
  
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 *
         (snd (ext_add (x1,y1) (x2,y2)) - snd (add (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])
  apply(simp add: c_eq_1 assms(1,2) divide_simps)
  unfolding delta_plus_def delta_y_def e'_def
  apply(subst t_expr)+
  by(simp add: power2_eq_square  field_simps)
  
lemma coherence:
  assumes "delta x1 y1 x2 y2  0" "delta' x1 y1 x2 y2  0" 
  assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
  shows "ext_add (x1,y1) (x2,y2) = add (x1,y1) (x2,y2)"
  using coherence_1 coherence_2 delta_def delta'_def assms by auto

lemma ext_add_closure:
  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
    apply(simp add: divide_simps) 
    by algebra

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

lemma ext_add_closure_points:
  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"
  using ext_add_closure assms 
  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


lemma add_closure_points:
  assumes "delta x y x' y'  0"
          "(x,y)  e'_aff" "(x',y')  e'_aff"
  shows "add (x,y) (x',y')  e'_aff"
  using add_closure assms e_e'_iff
  unfolding delta_def e'_aff_def by auto

lemma add_self:
  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(simp add: t_expr two_not_zero)
    apply(safe)
    apply(simp_all add: algebra_simps) 
    by(simp add: semiring_normalization_rules(18) semiring_normalization_rules(29) two_not_zero)+

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)
  apply(simp add: t_nz algebra_simps)
  apply(simp add: power2_eq_square[symmetric] t_expr d_nz)
  apply(simp add: divide_simps t_nz)
  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)
  apply(simp add: t_nz algebra_simps)
  apply(simp add: power2_eq_square[symmetric] t_expr d_nz)
  apply(simp add: divide_simps t_nz)
  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)
  apply(simp add: t_nz algebra_simps)
  apply(simp add: power2_eq_square[symmetric] t_expr d_nz)
  apply(simp add: divide_simps)
  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 add: t_expr)
  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 add: t_expr)
  apply(simp split: if_splits add: divide_simps t_nz) 
  apply fastforce
  apply algebra
  by algebra

lemma delta_add_delta'_1: 
  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
  apply(simp add: divide_simps t_expr)
  apply(simp add: c_eq_1 algebra_simps)
  by algebra

lemma delta'_add_delta_1: 
  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)
  apply(simp add: c_eq_1 algebra_simps)
  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) * y22) * (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) * x22) * (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 
    x12 + y12 - 1 = d * x12 * y12 
    x22 + y22 - 1 = d * x22 * y22   False"
  by algebra

lemma delta_add_delta'_2: 
  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)
  apply(simp add: c_eq_1 divide_simps)
  using in_aff unfolding e'_aff_def e'_def
  apply(simp add: t_expr power_mult_distrib[symmetric])
  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) * x22) * (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) * y22) * (x1 * x2 + y1 * y2)) *
    (x2 * y1 - x1 * y2) 
    x12 + y12 - 1 = d * x12 * y12 
    x22 + y22 - 1 = d * x22 * y22  False"
  by algebra

lemma delta'_add_delta_2: 
  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(simp add: t_expr)
  apply(rule funny_field_lemma_2)
  by (simp add: power_mult_distrib)


lemma delta'_add_delta_not_add: 
  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" 
  assumes add_nz: "fst (ext_add (x1,y1) (x2,y2))  0"  "snd (ext_add (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: divide_simps t_nz 1)
  apply(simp add: algebra_simps power2_eq_square[symmetric] t_expr d_nz)
  using add_nz d_nz apply(simp) 
  using d_nz by algebra

lemma not_add_self:
  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(simp add: t_expr two_not_zero)
    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) 
      apply(auto simp add: field_simps two_not_zero)
      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 
      by(simp add: field_simps,algebra)
    then have "e' x y  0" 
      using t_dneq2 t_n1
      by(auto simp add: field_simps t_nz) 
    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 *