Theory Elliptic_Axclass

section ‹Formalization using Axiomatic Type Classes›

theory Elliptic_Axclass
imports "HOL-Decision_Procs.Reflective_Field"
begin

subsection ‹Affine Coordinates›

datatype 'a point = Infinity | Point 'a 'a

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

definition nonsingular :: "'a  'a  bool" where
  "nonsingular a b = (4 * a ^ 3 + 27 * b ^ 2  0)"

definition on_curve :: "'a  'a  'a point  bool" where
  "on_curve a b p = (case p of
       Infinity  True
     | Point x y  y ^ 2 = x ^ 3 + a * x + b)"

definition add :: "'a  'a point  'a point  'a point" where
  "add a p1 p2 = (case p1 of
       Infinity  p2
     | Point x1 y1  (case p2 of
         Infinity  p1
       | Point x2 y2 
           if x1 = x2 then
             if y1 = - y2 then Infinity
             else
               let
                 l = (3 * x1 ^ 2 + a) / (2 * y1);
                 x3 = l ^ 2 - 2 * x1
               in
                 Point x3 (- y1 - l * (x3 - x1))
           else
             let
               l = (y2 - y1) / (x2 - x1);
               x3 = l ^ 2 - x1 - x2
             in
               Point x3 (- y1 - l * (x3 - x1))))"

definition opp :: "'a point  'a point" where
  "opp p = (case p of
       Infinity  Infinity
     | Point x y  Point x (- y))"

end

lemma on_curve_infinity [simp]: "on_curve a b Infinity"
  by (simp add: on_curve_def)

lemma opp_Infinity [simp]: "opp Infinity = Infinity"
  by (simp add: opp_def)

lemma opp_Point: "opp (Point x y) = Point x (- y)"
  by (simp add: opp_def)

lemma opp_opp: "opp (opp p) = p"
  by (simp add: opp_def split: point.split)

lemma opp_closed:
  "on_curve a b p  on_curve a b (opp p)"
  by (auto simp add: on_curve_def opp_def power2_eq_square
    split: point.split)

lemma curve_elt_opp:
  assumes "p1 = Point x1 y1"
  and "p2 = Point x2 y2"
  and "on_curve a b p1"
  and "on_curve a b p2"
  and "x1 = x2"
  shows "p1 = p2  p1 = opp p2"
proof -
  from p1 = Point x1 y1 on_curve a b p1
  have "y1 ^ 2 = x1 ^ 3 + a * x1 + b"
    by (simp_all add: on_curve_def)
  moreover from p2 = Point x2 y2 on_curve a b p2 x1 = x2
  have "x1 ^ 3 + a * x1 + b = y2 ^ 2"
    by (simp_all add: on_curve_def)
  ultimately have "y1 = y2  y1 = - y2"
    by (simp add: square_eq_iff power2_eq_square)
  with p1 = Point x1 y1 p2 = Point x2 y2 x1 = x2 show ?thesis
    by (auto simp add: opp_def)
qed

lemma add_closed:
  assumes "on_curve a b p1" and "on_curve a b p2"
  shows "on_curve a b (add a p1 p2)"
proof (cases p1)
  case (Point x1 y1)
  note Point' = this
  show ?thesis
  proof (cases p2)
    case (Point x2 y2)
    show ?thesis
    proof (cases "x1 = x2")
      case True
      note True' = this
      show ?thesis
      proof (cases "y1 = - y2")
        case True
        with True' Point Point'
        show ?thesis
          by (simp add: on_curve_def add_def)
      next
        case False
        note on_curve1 = on_curve a b p1 [simplified Point' on_curve_def True', simplified]
        from False True' Point Point' assms
        have "y1  0" by (auto simp add: on_curve_def)
        with False True' Point Point' assms
        show ?thesis
          apply (simp add: on_curve_def add_def Let_def)
          apply (field on_curve1)
          apply (simp add: two_not_zero)
          done
      qed
    next
      case False
      note on_curve1 = on_curve a b p1 [simplified Point' on_curve_def, simplified]
      note on_curve2 = on_curve a b p2 [simplified Point on_curve_def, simplified]
      from assms show ?thesis
        apply (simp add: on_curve_def add_def Let_def False Point Point')
        apply (field on_curve1 on_curve2)
        apply (simp add: False [symmetric])
        done
    qed
  next
    case Infinity
    with Point on_curve a b p1 show ?thesis
      by (simp add: add_def)
  qed
next
  case Infinity
  with on_curve a b p2 show ?thesis
    by (simp add: add_def)
qed

lemma add_case [consumes 2, case_names InfL InfR Opp Tan Gen]:
  assumes p: "on_curve a b p"
  and q: "on_curve a b q"
  and R1: "p. P Infinity p p"
  and R2: "p. P p Infinity p"
  and R3: "p. on_curve a b p  P p (opp p) Infinity"
  and R4: "p1 x1 y1 p2 x2 y2 l.
    p1 = Point x1 y1  p2 = Point x2 y2 
    p2 = add a p1 p1  y1  0 
    l = (3 * x1 ^ 2 + a) / (2 * y1) 
    x2 = l ^ 2 - 2 * x1 
    y2 = - y1 - l * (x2 - x1) 
    P p1 p1 p2"
  and R5: "p1 x1 y1 p2 x2 y2 p3 x3 y3 l.
    p1 = Point x1 y1  p2 = Point x2 y2  p3 = Point x3 y3 
    p3 = add a p1 p2  x1  x2 
    l = (y2 - y1) / (x2 - x1) 
    x3 = l ^ 2 - x1 - x2 
    y3 = - y1 - l * (x3 - x1) 
    P p1 p2 p3"
  shows "P p q (add a p q)"
proof (cases p)
  case Infinity
  then show ?thesis
    by (simp add: add_def R1)
next
  case (Point x1 y1)
  note Point' = this
  show ?thesis
  proof (cases q)
    case Infinity
    with Point show ?thesis
      by (simp add: add_def R2)
  next
    case (Point x2 y2)
    show ?thesis
    proof (cases "x1 = x2")
      case True
      note True' = this
      show ?thesis
      proof (cases "y1 = - y2")
        case True
        with p Point Point' True' R3 [of p] show ?thesis
          by (simp add: add_def opp_def)
      next
        case False
        from True' Point Point' p q have "(y1 - y2) * (y1 + y2) = 0"
          by (simp add: on_curve_def ring_distribs power2_eq_square)
        with False have "y1 = y2"
          by (simp add: eq_neg_iff_add_eq_0)
        with False True' Point Point' show ?thesis
          apply simp
          apply (rule R4)
          apply (auto simp add: add_def Let_def)
          done
      qed
    next
      case False
      with Point Point' show ?thesis
        apply -
        apply (rule R5)
        apply (auto simp add: add_def Let_def)
        done
    qed
  qed
qed

lemma eq_opp_is_zero: "((x::'a::ell_field) = - x) = (x = 0)"
proof
  assume "x = - x"
  have "2 * x = x + x" by simp
  also from x = - x
  have " = - x + x" by simp
  also have " = 0" by simp
  finally have "2 * x = 0" .
  with two_not_zero [where 'a='a] show "x = 0"
    by simp
qed simp

lemma add_casew [consumes 2, case_names InfL InfR Opp Gen]:
  assumes p: "on_curve a b p"
  and q: "on_curve a b q"
  and R1: "p. P Infinity p p"
  and R2: "p. P p Infinity p"
  and R3: "p. on_curve a b p  P p (opp p) Infinity"
  and R4: "p1 x1 y1 p2 x2 y2 p3 x3 y3 l.
    p1 = Point x1 y1  p2 = Point x2 y2  p3 = Point x3 y3 
    p3 = add a p1 p2  p1  opp p2 
    x1 = x2  y1 = y2  l = (3 * x1 ^ 2 + a) / (2 * y1) 
    x1  x2  l = (y2 - y1) / (x2 - x1) 
    x3 = l ^ 2 - x1 - x2 
    y3 = - y1 - l * (x3 - x1) 
    P p1 p2 p3"
  shows "P p q (add a p q)"
  using p q
  apply (rule add_case)
  apply (rule R1)
  apply (rule R2)
  apply (rule R3)
  apply assumption
  apply (rule R4)
  apply assumption+
  apply (simp add: opp_def eq_opp_is_zero)
  apply simp
  apply simp
  apply simp
  apply (rule R4)
  apply assumption+
  apply (simp add: opp_def)
  apply simp
  apply assumption+
  done

definition
  "is_tangent p q = (p  Infinity  p = q  p  opp q)"

definition
  "is_generic p q =
     (p  Infinity  q  Infinity 
      p  q  p  opp q)"

lemma diff_neq0:
  "(a::'a::ring)  b  a - b  0"
  "a  b  b - a  0"
  by simp_all

lemma minus2_not0: "(-2::'a::ell_field)  0"
  using two_not_zero [where 'a='a]
  by simp

lemmas [simp] = minus2_not0 [simplified]

declare two_not_zero [simplified, simp add]

lemma spec1_assoc:
  assumes p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and "is_generic p1 p2"
  and "is_generic p2 p3"
  and "is_generic (add a p1 p2) p3"
  and "is_generic p1 (add a p2 p3)"
  shows "add a p1 (add a p2 p3) = add a (add a p1 p2) p3"
  using p1 p2 assms
proof (induct rule: add_case)
  case InfL
  show ?case by (simp add: add_def)
next
  case InfR
  show ?case by (simp add: add_def)
next
  case Opp
  then show ?case by (simp add: is_generic_def)
next
  case Tan
  then show ?case by (simp add: is_generic_def)
next
  case (Gen p1 x1 y1 p2 x2 y2 p4 x4 y4 l)
  with on_curve a b p2 on_curve a b p3
  show ?case
  proof (induct rule: add_case)
    case InfL
    then show ?case by (simp add: is_generic_def)
  next
    case InfR
    then show ?case by (simp add: is_generic_def)
  next
    case Opp
    then show ?case by (simp add: is_generic_def)
  next
    case Tan
    then show ?case by (simp add: is_generic_def)
  next
    case (Gen p2 x2' y2' p3 x3 y3 p5 x5 y5 l1)
    from on_curve a b p2 on_curve a b p3 p5 = add a p2 p3
    have "on_curve a b p5" by (simp add: add_closed)
    with on_curve a b p1 show ?case using Gen [simplified p2 = Point x2' y2']
    proof (induct rule: add_case)
      case InfL
      then show ?case by (simp add: is_generic_def)
    next
      case InfR
      then show ?case by (simp add: is_generic_def)
    next
      case (Opp p)
      from is_generic p (opp p)
      show ?case by (simp add: is_generic_def opp_opp)
    next
      case Tan
      then show ?case by (simp add: is_generic_def)
    next
      case (Gen p1 x1' y1' p5' x5' y5' p6 x6 y6 l2)
      from on_curve a b p1 on_curve a b (Point x2' y2')
        p4 = add a p1 (Point x2' y2')
      have "on_curve a b p4" by (simp add: add_closed)
      then show ?case using on_curve a b p3 Gen
      proof (induct rule: add_case)
        case InfL
        then show ?case by (simp add: is_generic_def)
      next
        case InfR
        then show ?case by (simp add: is_generic_def)
      next
        case (Opp p)
        from is_generic p (opp p)
        show ?case by (simp add: is_generic_def opp_opp)
      next
        case Tan
        then show ?case by (simp add: is_generic_def)
      next
        case (Gen p4' x4' y4' p3' x3' y3' p7 x7 y7 l3)
        from p4' = Point x4' y4' p4' = Point x4 y4
        have p4: "x4' = x4" "y4' = y4" by simp_all
        from p3' = Point x3' y3' p3' = Point x3 y3
        have p3: "x3' = x3" "y3' = y3" by simp_all
        from p1 = Point x1' y1' p1 = Point x1 y1
        have p1: "x1' = x1" "y1' = y1" by simp_all
        from p5' = Point x5' y5' p5' = Point x5 y5
        have p5: "x5' = x5" "y5' = y5" by simp_all
        from Point x2' y2' = Point x2 y2
        have p2: "x2' = x2" "y2' = y2" by simp_all
        note ps = p1 p2 p3 p4 p5
        note ps' =
          on_curve a b p1 [simplified p1 = Point x1 y1 on_curve_def, simplified]
          on_curve a b p2 [simplified p2 = Point x2 y2 on_curve_def, simplified]
          on_curve a b p3 [simplified p3 = Point x3 y3 on_curve_def, simplified]
        show ?case
          apply (simp add: p6 = Point x6 y6 p7 = Point x7 y7)
          apply (simp only: ps
            x6 = l22 - x1' - x5' x7 = l32 - x4' - x3'
            y6 = - y1' - l2 * (x6 - x1') y7 = - y4' - l3 * (x7 - x4')
            l2 = (y5' - y1') / (x5' - x1') l3 = (y3' - y4') / (x3' - x4')
            l1 = (y3 - y2') / (x3 - x2') l = (y2 - y1) / (x2 - x1)
            x5 = l12 - x2' - x3 y5 = - y2' - l1 * (x5 - x2')
            x4 = l2 - x1 - x2 y4 = - y1 - l * (x4 - x1))
          apply (rule conjI)
          apply (field ps')
          apply (rule conjI)
          apply (simp add: x2'  x3 [simplified x2' = x2, symmetric])
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) ps'(1-2))
          apply (cut_tac x1'  x5' [simplified x5' = x5 x1' = x1 x5 = l12 - x2' - x3
            l1 = (y3 - y2') / (x3 - x2') y2' = y2 x2' = x2])
          apply (erule notE)
          apply (rule sym)
          apply (field ps'(1-2))
          apply (simp add: x2'  x3 [simplified x2' = x2, symmetric])
          apply (rule conjI)
          apply (simp add: x1  x2 [symmetric])
          apply (rule notI)
          apply (ring (prems) ps'(1-2))
          apply (cut_tac x4'  x3' [simplified x4' = x4 x3' = x3 x4 = l2 - x1 - x2
            l = (y2 - y1) / (x2 - x1)])
          apply (erule notE)
          apply (rule sym)
          apply (field ps'(1-2))
          apply (simp add: x1  x2 [symmetric])
          apply (field ps')
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) ps'(1-2))
          apply (cut_tac x1'  x5' [simplified x5' = x5 x1' = x1 x5 = l12 - x2' - x3
            l1 = (y3 - y2') / (x3 - x2') y2' = y2 x2' = x2])
          apply (erule notE)
          apply (rule sym)
          apply (field ps'(1-2))
          apply (simp add: x2'  x3 [simplified x2' = x2, symmetric])
          apply (rule conjI)
          apply (simp add: x2'  x3 [simplified x2' = x2, symmetric])
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) ps'(1-2))
          apply (cut_tac x4'  x3' [simplified x4' = x4 x3' = x3 x4 = l2 - x1 - x2
            l = (y2 - y1) / (x2 - x1)])
          apply (erule notE)
          apply (rule sym)
          apply (field ps'(1-2))
          apply (simp_all add: x1  x2 [symmetric])
          done
      qed
    qed
  qed
qed

lemma spec2_assoc:
  assumes p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and "is_generic p1 p2"
  and "is_tangent p2 p3"
  and "is_generic (add a p1 p2) p3"
  and "is_generic p1 (add a p2 p3)"
  shows "add a p1 (add a p2 p3) = add a (add a p1 p2) p3"
  using p1 p2 assms
proof (induct rule: add_case)
  case InfL
  show ?case by (simp add: add_def)
next
  case InfR
  show ?case by (simp add: add_def)
next
  case Opp
  then show ?case by (simp add: is_generic_def)
next
  case Tan
  then show ?case by (simp add: is_generic_def)
next
  case (Gen p1 x1 y1 p2 x2 y2 p4 x4 y4 l)
  with on_curve a b p2 on_curve a b p3
  show ?case
  proof (induct rule: add_case)
    case InfL
    then show ?case by (simp add: is_generic_def)
  next
    case InfR
    then show ?case by (simp add: is_generic_def)
  next
    case Opp
    then show ?case by (simp add: is_generic_def)
  next
    case (Tan p2 x2' y2' p5 x5 y5 l1)
    from on_curve a b p2 p5 = add a p2 p2
    have "on_curve a b p5" by (simp add: add_closed)
    with on_curve a b p1 show ?case using Tan
    proof (induct rule: add_case)
      case InfL
      then show ?case by (simp add: is_generic_def)
    next
      case InfR
      then show ?case by (simp add: is_generic_def)
    next
      case (Opp p)
      from is_generic p (opp p) on_curve a b p
      show ?case by (simp add: is_generic_def opp_opp)
    next
      case Tan
      then show ?case by (simp add: is_generic_def)
    next
      case (Gen p1 x1' y1' p5' x5' y5' p6 x6 y6 l2)
      from on_curve a b p1 on_curve a b p2 p4 = add a p1 p2
      have "on_curve a b p4" by (simp add: add_closed)
      then show ?case using on_curve a b p2 Gen
      proof (induct rule: add_case)
        case InfL
        then show ?case by (simp add: is_generic_def)
      next
        case InfR
        then show ?case by (simp add: is_generic_def)
      next
        case (Opp p)
        from is_generic p (opp p)
        show ?case by (simp add: is_generic_def opp_opp)
      next
        case Tan
        then show ?case by (simp add: is_generic_def)
      next
        case (Gen p4' x4' y4' p3' x3' y3' p7 x7 y7 l3)
        from
          on_curve a b p1 p1 = Point x1 y1
          on_curve a b p2 p2 = Point x2 y2
        have
          y1: "y1 ^ 2 = x1 ^ 3 + a * x1 + b" and
          y2: "y2 ^ 2 = x2 ^ 3 + a * x2 + b"
          by (simp_all add: on_curve_def)
        from
          p5' = Point x5' y5'
          p5' = Point x5 y5
          p4' = Point x4' y4'
          p4' = Point x4 y4
          p3' = Point x2' y2'
          p3' = Point x2 y2
          p3' = Point x3' y3'
          p1 = Point x1' y1'
          p1 = Point x1 y1
        have ps:
          "x5' = x5" "y5' = y5"
          "x4' = x4" "y4' = y4" "x3' = x2" "y3' = y2" "x2' = x2" "y2' = y2"
          "x1' = x1" "y1' = y1"
          by simp_all
        show ?case
          apply (simp add: p6 = Point x6 y6 p7 = Point x7 y7)
          apply (simp only: ps
            x7 = l3 ^ 2 - x4' - x3'
            y7 = - y4' - l3 * (x7 - x4')
            l3 = (y3' - y4') / (x3' - x4')
            x6 = l2 ^ 2 - x1' - x5'
            y6 = - y1' - l2 * (x6 - x1')
            l2 = (y5' - y1') / (x5' - x1')
            x5 = l1 ^ 2 - 2 * x2'
            y5 = - y2' - l1 * (x5 - x2')
            l1 = (3 * x2' ^ 2 + a) / (2 * y2')
            x4 = l ^ 2 - x1 - x2
            y4 = - y1 - l * (x4 - x1)
            l = (y2 - y1) / (x2 - x1))
          apply (rule conjI)
          apply (field y1 y2)
          apply (intro conjI)
          apply (simp add: y2'  0 [simplified y2' = y2])
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (rule notE [OF x1'  x5' [simplified
            x5 = l1 ^ 2 - 2 * x2'
            l1 = (3 * x2' ^ 2 + a) / (2 * y2')
            x1' = x1 x2' = x2 y2' = y2 x5' = x5]])
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: y2'  0 [simplified y2' = y2])
          apply (simp add: x1  x2 [symmetric])
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (rule notE [OF x4'  x3' [simplified
            x4 = l ^ 2 - x1 - x2
            l = (y2 - y1) / (x2 - x1)
            x4' = x4 x3' = x2]])
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: x1  x2 [symmetric])
          apply (field y1 y2)
          apply (intro conjI)
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (rule notE [OF x1'  x5' [simplified
            x5 = l1 ^ 2 - 2 * x2'
            l1 = (3 * x2' ^ 2 + a) / (2 * y2')
            x1' = x1 x2' = x2 y2' = y2 x5' = x5]])
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: y2'  0 [simplified y2' = y2])
          apply (simp add: y2'  0 [simplified y2' = y2])
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (rule notE [OF x4'  x3' [simplified
            x4 = l ^ 2 - x1 - x2
            l = (y2 - y1) / (x2 - x1)
            x4' = x4 x3' = x2]])
          apply (rule sym)
          apply (field y1 y2)
          apply (simp_all add: x1  x2 [symmetric])
          done
      qed
    qed
  next
    case (Gen p3 x3 y3 p5 x5 y5 p6 x6 y6 l1)
    then show ?case by (simp add: is_tangent_def)
  qed
qed

lemma spec3_assoc:
  assumes p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and "is_generic p1 p2"
  and "is_tangent p2 p3"
  and "is_generic (add a p1 p2) p3"
  and "is_tangent p1 (add a p2 p3)"
  shows "add a p1 (add a p2 p3) = add a (add a p1 p2) p3"
  using p1 p2 assms
proof (induct rule: add_case)
  case InfL
  then show ?case by (simp add: is_generic_def)
next
  case InfR
  then show ?case by (simp add: is_generic_def)
next
  case Opp
  then show ?case by (simp add: is_generic_def)
next
  case Tan
  then show ?case by (simp add: is_generic_def)
next
  case (Gen p1 x1 y1 p2 x2 y2 p4 x4 y4 l)
  with on_curve a b p2 on_curve a b p3
  show ?case
  proof (induct rule: add_case)
    case InfL
    then show ?case by (simp add: is_generic_def)
  next
    case InfR
    then show ?case by (simp add: is_generic_def)
  next
    case Opp
    then show ?case by (simp add: is_tangent_def opp_opp)
  next
    case (Tan p2 x2' y2' p5 x5 y5 l1)
    from on_curve a b p2 p5 = add a p2 p2
    have "on_curve a b p5" by (simp add: add_closed)
    with on_curve a b p1 show ?case using Tan
    proof (induct rule: add_case)
      case InfL
      then show ?case by (simp add: is_generic_def)
    next
      case InfR
      then show ?case by (simp add: is_generic_def)
    next
      case Opp
      then show ?case by (simp add: is_tangent_def opp_opp)
    next
      case (Tan p1 x1' y1' p6 x6 y6 l2)
      from on_curve a b p1 on_curve a b p2 p4 = add a p1 p2
      have "on_curve a b p4" by (simp add: add_closed)
      then show ?case using on_curve a b p2 Tan
      proof (induct rule: add_case)
        case InfL
        then show ?case by (simp add: is_generic_def)
      next
        case InfR
        then show ?case by (simp add: is_generic_def)
      next
        case (Opp p)
        from is_generic p (opp p)
        show ?case by (simp add: is_generic_def opp_opp)
      next
        case Tan
        then show ?case by (simp add: is_generic_def)
      next
        case (Gen p4' x4' y4' p2' x2'' y2'' p7 x7 y7 l3)
        from
          on_curve a b p1 p1 = Point x1 y1
          on_curve a b p2 p2 = Point x2 y2
        have
          y1: "y1 ^ 2 = x1 ^ 3 + a * x1 + b" and
          y2: "y2 ^ 2 = x2 ^ 3 + a * x2 + b"
          by (simp_all add: on_curve_def)
        from
          p4' = Point x4' y4'
          p4' = Point x4 y4
          p2' = Point x2' y2'
          p2' = Point x2 y2
          p2' = Point x2'' y2''
          p1 = Point x1' y1'
          p1 = Point x1 y1
          p1 = Point x5 y5
        have ps:
          "x4' = x4" "y4' = y4" "x2' = x2" "y2' = y2" "x2'' = x2" "y2'' = y2"
          "x1' = x5" "y1' = y5" "x1 = x5" "y1 = y5"
          by simp_all
        note qs =
          x7 = l3 ^ 2 - x4' - x2''
          y7 = - y4' - l3 * (x7 - x4')
          l3 = (y2'' - y4') / (x2'' - x4')
          x6 = l2 ^ 2 - 2 * x1'
          y6 = - y1' - l2 * (x6 - x1')
          x5 = l1 ^ 2 - 2 * x2'
          y5 = - y2' - l1 * (x5 - x2')
          l1 = (3 * x2' ^ 2 + a) / (2 * y2')
          l2 = (3 * x1' ^ 2 + a) / (2 * y1')
          x4 = l ^ 2 - x1 - x2
          y4 = - y1 - l * (x4 - x1)
          l = (y2 - y1) / (x2 - x1)
        from y2'  0 y2' = y2
        have "2 * y2  0" by simp
        show ?case
          apply (simp add: p6 = Point x6 y6 p7 = Point x7 y7)
          apply (simp only: ps qs)
          apply (rule conjI)
          apply (field y2)
          apply (intro conjI)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF y1'  0])
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x1  x2])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          apply (rule 2 * y2  0)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x4'  x2''])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (intro conjI)
          apply (rule 2 * y2  0)
          apply (erule thin_rl)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x1  x2])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          apply (field y2)
          apply (intro conjI)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF y1'  0])
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x4'  x2''])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (erule thin_rl)
          apply (rule conjI)
          apply (rule 2 * y2  0)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x1  x2])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          apply (rule 2 * y2  0)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF x1  x2])
          apply (rule sym)
          apply (simp only: ps qs)
          apply field
          apply (rule 2 * y2  0)
          done
      qed
    next
      case Gen
      then show ?case by (simp add: is_tangent_def)
    qed
  next
    case Gen
    then show ?case by (simp add: is_tangent_def)
  qed
qed

lemma add_0_l: "add a Infinity p = p"
  by (simp add: add_def)

lemma add_0_r: "add a p Infinity = p"
  by (simp add: add_def split: point.split)

lemma add_opp: "on_curve a b p  add a p (opp p) = Infinity"
  by (simp add: add_def opp_def on_curve_def split: point.split_asm)

lemma add_comm:
  assumes "on_curve a b p1" "on_curve a b p2"
  shows "add a p1 p2 = add a p2 p1"
proof (cases p1)
  case Infinity
  then show ?thesis by (simp add: add_0_l add_0_r)
next
  case (Point x1 y1)
  note Point' = this
  with on_curve a b p1
  have y1: "y1 ^ 2 = x1 ^ 3 + a * x1 + b"
    by (simp add: on_curve_def)
  show ?thesis
  proof (cases p2)
    case Infinity
    then show ?thesis by (simp add: add_0_l add_0_r)
  next
    case (Point x2 y2)
    with on_curve a b p2
    have y2: "y2 ^ 2 = x2 ^ 3 + a * x2 + b"
      by (simp add: on_curve_def)
    show ?thesis
    proof (cases "x1 = x2")
      case True
      show ?thesis
      proof (cases "y1 = - y2")
        case True
        with Point Point' x1 = x2 show ?thesis
          by (simp add: add_def)
      next
        case False
        with y1 y2 [symmetric] x1 = x2 Point Point'
        show ?thesis
          by (simp add: power2_eq_square square_eq_iff)
      qed
    next
      case False
      with Point Point' show ?thesis
        apply (simp add: add_def Let_def)
        apply (rule conjI)
        apply field
        apply simp
        apply field
        apply simp
        done
    qed
  qed
qed

lemma uniq_opp:
  assumes "add a p1 p2 = Infinity"
  shows "p2 = opp p1"
  using assms
  by (auto simp add: add_def opp_def Let_def
    split: point.split_asm if_split_asm)

lemma uniq_zero:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and add: "add a p1 p2 = p2"
  shows "p1 = Infinity"
  using p1 p2 assms
proof (induct rule: add_case)
  case InfL
  show ?case ..
next
  case InfR
  then show ?case by simp
next
  case Opp
  then show ?case by (simp add: opp_def split: point.split_asm)
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  from p1 = Point x1 y1 p2 = Point x2 y2 p2 = p1
  have "x2 = x1" "y2 = y1" by simp_all
  with y2 = - y1 - l * (x2 - x1) y1  0
  have "- y1 = y1" by simp
  with y1  0
  show ?case by simp
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then have y1: "y1 ^ 2 = x1 ^ 3 + a * x1 + b"
    and y2: "y2 ^ 2 = x2 ^ 3 + a * x2 + b"
    by (simp_all add: on_curve_def)
  from p3 = p2 p2 = Point x2 y2 p3 = Point x3 y3
  have ps: "x3 = x2" "y3 = y2" by simp_all
  with y3 = - y1 - l * (x3 - x1)
  have "y2 = - y1 - l * (x2 - x1)" by simp
  also from l = (y2 - y1) / (x2 - x1) x1  x2
  have "l * (x2 - x1) = y2 - y1"
    by simp
  also have "- y1 - (y2 - y1) = (- y1 + y1) + - y2"
    by simp
  finally have "y2 = 0" by simp
  with p2 = Point x2 y2 on_curve a b p2
  have x2: "x2 ^ 3 = - (a * x2 + b)"
    by (simp add: on_curve_def eq_neg_iff_add_eq_0 add.assoc del: minus_add_distrib)
  from x3 = l ^ 2 - x1 - x2 x3 = x2
  have "l ^ 2 - x1 - x2 - x2 = x2 - x2" by simp
  then have "l ^ 2 - x1 - 2 * x2 = 0" by simp
  then have "x2 * (l ^ 2 - x1 - 2 * x2) = x2 * 0" by simp
  then have "(x2 - x1) * (2 * a * x2 + 3 * b) = 0"
    apply (simp only: l = (y2 - y1) / (x2 - x1) y2 = 0)
    apply (field (prems) y1 x2)
    apply (ring y1 x2)
    apply (simp add: x1  x2 [symmetric])
    done
  with x1  x2 have "2 * a * x2 + 3 * b = 0" by simp
  then have "2 * a * x2 = - (3 * b)"
    by (simp add: eq_neg_iff_add_eq_0)
  from y2 [symmetric] y2 = 0
  have "(- (2 * a)) ^ 3 * (x2 ^ 3 + a * x2 + b) = 0"
    by simp
  then have "b * (4 * a ^ 3 + 27 * b ^ 2) = 0"
    apply (ring (prems) 2 * a * x2 = - (3 * b))
    apply (ring 2 * a * x2 = - (3 * b))
    done
  with ab have "b = 0" by (simp add: nonsingular_def)
  with 2 * a * x2 + 3 * b = 0 ab
  have "x2 = 0" by (simp add: nonsingular_def)
  from l ^ 2 - x1 - 2 * x2 = 0
  show ?case
    apply (simp add: x2 = 0 y2 = 0 l = (y2 - y1) / (x2 - x1))
    apply (field (prems) y1 b = 0)
    apply (insert ab b = 0 x1  x2 x2 = 0)
    apply (simp add: nonsingular_def)
    apply simp
    done
qed

lemma opp_add:
  assumes p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  shows "opp (add a p1 p2) = add a (opp p1) (opp p2)"
proof (cases p1)
  case Infinity
  then show ?thesis by (simp add: add_def opp_def)
next
  case (Point x1 y1)
  show ?thesis
  proof (cases p2)
    case Infinity
    with p1 = Point x1 y1 show ?thesis
      by (simp add: add_def opp_def)
  next
    case (Point x2 y2)
    with p1 = Point x1 y1 p1 p2
    have "x1 ^ 3 + a * x1 + b = y1 ^ 2"
      "x2 ^ 3 + a * x2 + b = y2 ^ 2"
      by (simp_all add: on_curve_def)
    with Point p1 = Point x1 y1 show ?thesis
      apply (cases "x1 = x2")
      apply (cases "y1 = - y2")
      apply (simp add: add_def opp_def Let_def)
      apply (simp add: add_def opp_def Let_def trans [OF minus_equation_iff eq_commute])
      apply (simp add: add_def opp_def Let_def)
      apply (rule conjI)
      apply field
      apply simp
      apply field
      apply simp
      done
  qed
qed

lemma compat_add_opp:
  assumes p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and "add a p1 p2 = add a p1 (opp p2)"
  and "p1  opp p1"
  shows "p2 = opp p2"
  using p1 p2 assms
proof (induct rule: add_case)
  case InfL
  then show ?case by (simp add: add_0_l)
next
  case InfR
  then show ?case by (simp add: opp_def add_0_r)
next
  case (Opp p)
  then have "add a p p = Infinity" by (simp add: opp_opp)
  then have "p = opp p" by (rule uniq_opp)
  with p  opp p show ?case ..
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  then have "add a p1 p1 = Infinity"
    by (simp add: add_opp)
  then have "p1 = opp p1" by (rule uniq_opp)
  with p1  opp p1 show ?case ..
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  have "(2::'a) * 2  0"
    by (simp only: mult_eq_0_iff) simp
  then have "(4::'a)  0" by simp
  from Gen have "((- y2 - y1) / (x2 - x1)) ^ 2 - x1 - x2 =
    ((y2 - y1) / (x2 - x1)) ^ 2 - x1 - x2"
    by (simp add: add_def opp_def Let_def)
  then show ?case
    apply (field (prems))
    apply (insert p1  opp p1
      p1 = Point x1 y1 p2 = Point x2 y2 4  0)[1]
    apply (simp add: opp_def eq_neg_iff_add_eq_0)
    apply (simp add: x1  x2 [symmetric])
    done
qed

lemma compat_add_triple:
  assumes ab: "nonsingular a b"
  and p: "on_curve a b p"
  and "p  opp p"
  and "add a p p  opp p"
  shows "add a (add a p p) (opp p) = p"
  using add_closed [OF p p] opp_closed [OF p] assms
proof (induct "add a p p" "opp p" rule: add_case)
  case InfL
  from p  opp p uniq_opp [OF Infinity = add a p p [symmetric]]
  show ?case ..
next
  case InfR
  then show ?case by (simp add: opp_def split: point.split_asm)
next
  case Opp
  then have "opp (opp (add a p p)) = opp (opp p)" by simp
  then have "add a p p = p" by (simp add: opp_opp)
  with uniq_zero [OF ab p p] p  opp p
  show ?case by (simp add: opp_def)
next
  case Tan
  then show ?case by simp
next
  case (Gen x1 y1 x2 y2 p3 x3 y3 l)
  from opp p = Point x2 y2
  have "p = Point x2 (- y2)"
    by (auto simp add: opp_def split: point.split_asm)
  with add a p p = Point x1 y1 [symmetric]
  obtain l' where l':
    "l' = (3 * x2 ^ 2 + a) / (2 * - y2)"
    and xy: "x1 = l' ^ 2 - 2 * x2"
    "y1 = - (- y2) - l' * (x1 - x2)"
    and y2: "- y2  - (- y2)"
    by (simp add: add_def Let_def split: if_split_asm)
  have "x3 = x2"
    apply (simp add: xy
      l = (y2 - y1) / (x2 - x1) x3 = l ^ 2 - x1 - x2)
    apply field
    apply (insert x1  x2)
    apply (simp add: xy)
    done
  then have "p3 = p  p3 = opp p"
    by (rule curve_elt_opp [OF p3 = Point x3 y3 p = Point x2 (- y2)
      add_closed [OF add_closed [OF p p] opp_closed [OF p],
        folded p3 = add a (add a p p) (opp p)]
     on_curve a b p])
  then show ?case
  proof
    assume "p3 = p"
    with p3 = add a (add a p p) (opp p)
    show ?thesis by simp
  next
    assume "p3 = opp p"
    with p3 = add a (add a p p) (opp p)
    have "add a (add a p p) (opp p) = opp p" by simp
    with ab add_closed [OF p p] opp_closed [OF p]
    have "add a p p = Infinity" by (rule uniq_zero)
    with add a p p = Point x1 y1 show ?thesis by simp
  qed
qed

lemma add_opp_double_opp:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and "add a p1 p2 = opp p1"
  shows "p2 = add a (opp p1) (opp p1)"
proof (cases "p1 = opp p1")
  case True
  with assms have "add a p2 p1 = p1" by (simp add: add_comm)
  with ab p2 p1 have "p2 = Infinity" by (rule uniq_zero)
  also from on_curve a b p1 have " = add a p1 (opp p1)"
    by (simp add: add_opp)
  also from True have " = add a (opp p1) (opp p1)" by simp
  finally show ?thesis .
next
  case False
  from p1 p2 False assms show ?thesis
  proof (induct rule: add_case)
    case InfL
    then show ?case by simp
  next
    case InfR
    then show ?case by simp
  next
    case Opp
    then show ?case by (simp add: add_0_l)
  next
    case (Tan p1 x1 y1 p2 x2 y2 l)
    from p2 = opp p1 on_curve a b p1
    have "p1 = opp p2" by (simp add: opp_opp)
    also note p2 = add a p1 p1
    finally show ?case using on_curve a b p1
      by (simp add: opp_add)
  next
    case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
    from on_curve a b p1 p1 = Point x1 y1
    have y1: "y1 ^ 2 = x1 ^ 3 + a * x1 + b"
      by (simp add: on_curve_def)
    from on_curve a b p2 p2 = Point x2 y2
    have y2: "y2 ^ 2 = x2 ^ 3 + a * x2 + b"
      by (simp add: on_curve_def)
    from p1 = Point x1 y1 p1  opp p1
    have "y1  0"
      by (simp add: opp_Point)
    from Gen have "x1 = ((y2 - y1) / (x2 - x1)) ^ 2 - x1 - x2"
      by (simp add: opp_Point)
    then have "2 * y2 * y1 = a * x2 + 3 * x2 * x1 ^ 2 + a * x1 -
      x1 ^ 3 + 2 * b"
      apply (field (prems) y1 y2)
      apply (field y1 y2)
      apply simp
      apply (simp add: x1  x2 [symmetric])
      done
    then have "(x2 - (((3 * x1 ^ 2 + a) / (2 * (- y1))) ^ 2 -
      2 * x1)) * (x2 - x1) ^ 2 = 0"
      apply (drule_tac f="λx. x ^ 2" in arg_cong)
      apply (field (prems) y1 y2)
      apply (field y1 y2)
      apply (simp_all add: y1  0)
      done
    with x1  x2
    have "x2 = ((3 * x1 ^ 2 + a) / (2 * (- y1))) ^ 2 - 2 * x1"
      by simp
    with p2 = Point x2 y2 _ on_curve a b p2
      add_closed [OF
        opp_closed [OF on_curve a b p1] opp_closed [OF on_curve a b p1]]
    have "p2 = add a (opp p1) (opp p1)  p2 = opp (add a (opp p1) (opp p1))"
      apply (rule curve_elt_opp)
      apply (simp add: add_def opp_Point Let_def p1 = Point x1 y1 y1  0)
      done
    then show ?case
    proof
      assume "p2 = opp (add a (opp p1) (opp p1))"
      with on_curve a b p1
      have "p2 = add a p1 p1"
        by (simp add: opp_add [of a b] opp_opp opp_closed)
      show ?case
      proof (cases "add a p1 p1 = opp p1")
        case True
        from on_curve a b p1
        show ?thesis
          apply (simp add: opp_add [symmetric] p2 = add a p1 p1 True)
          apply (simp add: p3 = add a p1 p2 [simplified p3 = opp p1])
          apply (simp add: p2 = add a p1 p1 True add_opp)
          done
      next
        case False
        from on_curve a b p1
        have "add a p1 (opp p2) = opp (add a (add a p1 p1) (opp p1))"
          by (simp add: p2 = add a p1 p1
            opp_add [of a b] add_closed opp_closed opp_opp add_comm [of a b])
        with ab on_curve a b p1 p1  opp p1 False
        have "add a p1 (opp p2) = opp p1"
          by (simp add: compat_add_triple)
        with p3 = add a p1 p2 p3 = opp p1
        have "add a p1 p2 = add a p1 (opp p2)" by simp
        with on_curve a b p1 on_curve a b p2
        have "p2 = opp p2" using p1  opp p1
          by (rule compat_add_opp)
        with on_curve a b p1 p2 = add a p1 p1
        show ?thesis by (simp add: opp_add)
      qed
    qed
  qed
qed

lemma cancel:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and eq: "add a p1 p2 = add a p1 p3"
  shows "p2 = p3"
  using p1 p2 p1 p2 eq
proof (induct rule: add_casew)
  case InfL
  then show ?case by (simp add: add_0_l)
next
  case (InfR p)
  with p3 have "add a p3 p = p" by (simp add: add_comm)
  with ab p3 on_curve a b p
  show ?case by (rule uniq_zero [symmetric])
next
  case (Opp p)
  from Infinity = add a p p3 [symmetric]
  show ?case by (rule uniq_opp [symmetric])
next
  case (Gen p1 x1 y1 p2 x2 y2 p4 x4 y4 l)
  from on_curve a b p1 p3 on_curve a b p1 p3 p1 = Point x1 y1
    p4 = add a p1 p2 p4 = add a p1 p3 p1  opp p2
  show ?case
  proof (induct rule: add_casew)
    case InfL
    then show ?case by (simp add: add_0_l)
  next
    case (InfR p)
    with on_curve a b p2
    have "add a p2 p = p" by (simp add: add_comm)
    with ab on_curve a b p2 on_curve a b p
    show ?case by (rule uniq_zero)
  next
    case (Opp p)
    then have "add a p p2 = Infinity" by simp
    then show ?case by (rule uniq_opp)
  next
    case (Gen p1 x1' y1' p3 x3 y3 p5 x5 y5 l')
    from p4 = p5 p4 = Point x4 y4 p5 = Point x5 y5
      p1 = Point x1' y1' p1 = Point x1 y1
      y4 = - y1 - l * (x4 - x1) y5 = - y1' - l' * (x5 - x1')
    have "0 = - y1 - l * (x4 - x1) - (- y1 - l' * (x4 - x1))"
      by auto
    then have "l' = l  x4 = x1" by auto
    then show ?case
    proof
      assume "l' = l"
      with p4 = p5 p4 = Point x4 y4 p5 = Point x5 y5
        p1 = Point x1' y1' p1 = Point x1 y1
        x4 = l ^ 2 - x1 - x2 x5 = l' ^ 2 - x1' - x3
      have "0 = l ^ 2 - x1 - x2 - (l ^ 2 - x1 - x3)"
        by simp
      then have "x2 = x3" by simp
      with p2 = Point x2 y2 p3 = Point x3 y3 on_curve a b p2 on_curve a b p3
      have "p2 = p3  p2 = opp p3" by (rule curve_elt_opp)
      then show ?case
      proof
        assume "p2 = opp p3"
        with on_curve a b p3 have "opp p2 = p3"
          by (simp add: opp_opp)
        with p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
        have "add a p1 p2 = add a p1 (opp p2)" by simp
        show ?case
        proof (cases "p1 = opp p1")
          case True
          with p1  opp p2 p1  opp p3
          have "p1  p2" "p1  p3" by auto
          with l' = l x1 = x2  _ _ x1' = x3  _  _
            p1 = Point x1 y1 p1 = Point x1' y1'
            p2 = Point x2 y2 p3 = Point x3 y3
            p2 = opp p3
          have eq: "(y2 - y1) / (x2 - x1) = (y3 - y1) / (x2 - x1)" and "x1  x2"
            by (auto simp add: opp_Point)
          from eq have "y2 = y3"
            apply (field (prems))
            apply (simp_all add: x1  x2 [symmetric])
            done
          with p2 = opp p3 p2 = Point x2 y2 p3 = Point x3 y3
          show ?thesis by (simp add: opp_Point)
        next
          case False
          with on_curve a b p1 on_curve a b p2
            add a p1 p2 = add a p1 (opp p2)
          have "p2 = opp p2" by (rule compat_add_opp)
          with opp p2 = p3 show ?thesis by simp
        qed
      qed
    next
      assume "x4 = x1"
      with p4 = Point x4 y4 [simplified p4 = add a p1 p2]
        p1 = Point x1 y1
        add_closed [OF on_curve a b p1 on_curve a b p2]
        on_curve a b p1
      have "add a p1 p2 = p1  add a p1 p2 = opp p1" by (rule curve_elt_opp)
      then show ?case
      proof
        assume "add a p1 p2 = p1"
        with on_curve a b p1 on_curve a b p2
        have "add a p2 p1 = p1" by (simp add: add_comm)
        with ab on_curve a b p2 on_curve a b p1
        have "p2 = Infinity" by (rule uniq_zero)
        moreover from add a p1 p2 = p1
          p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
          on_curve a b p1 on_curve a b p3
        have "add a p3 p1 = p1" by (simp add: add_comm)
        with ab on_curve a b p3 on_curve a b p1
        have "p3 = Infinity" by (rule uniq_zero)
        ultimately show ?case by simp
      next
        assume "add a p1 p2 = opp p1"
        with ab on_curve a b p1 on_curve a b p2
        have "p2 = add a (opp p1) (opp p1)" by (rule add_opp_double_opp)
        moreover from add a p1 p2 = opp p1
          p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
        have "add a p1 p3 = opp p1" by simp
        with ab on_curve a b p1 on_curve a b p3
        have "p3 = add a (opp p1) (opp p1)" by (rule add_opp_double_opp)
        ultimately show ?case by simp
      qed
    qed
  qed
qed

lemma add_minus_id:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  shows "add a (add a p1 p2) (opp p2) = p1"
proof (cases "add a p1 p2 = opp p2")
  case True
  then have "add a (add a p1 p2) (opp p2) = add a (opp p2) (opp p2)"
    by simp
  also from p1 p2 True have "add a p2 p1 = opp p2"
    by (simp add: add_comm)
  with ab p2 p1 have "add a (opp p2) (opp p2) = p1"
    by (rule add_opp_double_opp [symmetric])
  finally show ?thesis .
next
  case False
  from p1 p2 p1 p2 False show ?thesis
  proof (induct rule: add_case)
    case InfL
    then show ?case by (simp add: add_opp)
  next
    case InfR
    show ?case by (simp add: add_0_r)
  next
    case Opp
    then show ?case by (simp add: opp_opp add_0_l)
  next
    case (Tan p1 x1 y1 p2 x2 y2 l)
    note ab on_curve a b p1
    moreover from y1  0 p1 = Point x1 y1
    have "p1  opp p1" by (simp add: opp_Point)
    moreover from p2 = add a p1 p1 p2  opp p1
    have "add a p1 p1  opp p1" by simp
    ultimately have "add a (add a p1 p1) (opp p1) = p1"
      by (rule compat_add_triple)
    with p2 = add a p1 p1 show ?case by simp
  next
    case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
    from p3 = add a p1 p2 on_curve a b p2
    have "p3 = add a p1 (opp (opp p2))" by (simp add: opp_opp)
    with
      add_closed [OF on_curve a b p1 on_curve a b p2,
        folded p3 = add a p1 p2]
      opp_closed [OF on_curve a b p2]
      opp_closed [OF on_curve a b p2]
      opp_opp [of p2]
      Gen
    show ?case
    proof (induct rule: add_case)
      case InfL
      then show ?case by simp
    next
      case InfR
      then show ?case by (simp add: add_0_r)
    next
      case (Opp p)
      from p = add a p1 (opp (opp p))
      have "add a p1 p = p" by (simp add: opp_opp)
      with ab on_curve a b p1 on_curve a b p
      show ?case by (rule uniq_zero [symmetric])
    next
      case Tan
      then show ?case by simp
    next
      case (Gen p4 x4 y4 p5 x5 y5 p6 x6 y6 l')
      from on_curve a b p5 opp p5 = p2
        p2 = Point x2 y2 p5 = Point x5 y5
      have "y5 = - y2" "x5 = x2"
        by (auto simp add: opp_Point on_curve_def)
      from p4 = Point x3 y3 p4 = Point x4 y4
      have "x4 = x3" "y4 = y3" by simp_all
      from x4  x5 show ?case
        apply (simp add:
          y5 = - y2 x5 = x2
          x4 = x3 y4 = y3
          p6 = Point x6 y6 p1 = Point x1 y1
          x6 = l' ^ 2 - x4 - x5 y6 = - y4 - l' * (x6 - x4)
          l' = (y5 - y4) / (x5 - x4)
          x3 = l ^ 2 - x1 - x2 y3 = - y1 - l * (x3 - x1)
          l = (y2 - y1) / (x2 - x1))
        apply (rule conjI)
        apply field
        apply (rule conjI)
        apply (rule notI)
        apply (erule notE)
        apply (ring (prems))
        apply (rule sym)
        apply field
        apply (simp_all add: x1  x2 [symmetric])
        apply field
        apply (rule conjI)
        apply (rule notI)
        apply (erule notE)
        apply (ring (prems))
        apply (rule sym)
        apply field
        apply (simp_all add: x1  x2 [symmetric])
        done
    qed
  qed
qed

lemma add_shift_minus:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and eq: "add a p1 p2 = p3"
  shows "p1 = add a p3 (opp p2)"
proof -
  note eq
  also from add_minus_id [OF ab p3 opp_closed [OF p2]] p2
  have "p3 = add a (add a p3 (opp p2)) p2" by (simp add: opp_opp)
  finally have "add a p2 p1 = add a p2 (add a p3 (opp p2))"
    using p1 p2 p3
    by (simp add: add_comm [of a b] add_closed opp_closed)
  with ab p2 p1 add_closed [OF p3 opp_closed [OF p2]]
  show ?thesis by (rule cancel)
qed

lemma degen_assoc:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and H:
    "(p1 = Infinity  p2 = Infinity  p3 = Infinity) 
     (p1 = opp p2  p2 = opp p3) 
     (opp p1 = add a p2 p3  opp p3 = add a p1 p2)"
  shows "add a p1 (add a p2 p3) = add a (add a p1 p2) p3"
  using H
proof (elim disjE)
  assume "p1 = Infinity"
  then show ?thesis by (simp add: add_0_l)
next
  assume "p2 = Infinity"
  then show ?thesis by (simp add: add_0_l add_0_r)
next
  assume "p3 = Infinity"
  then show ?thesis by (simp add: add_0_r)
next
  assume "p1 = opp p2"
  from p2 p3
  have "add a (opp p2) (add a p2 p3) = add a (add a p3 p2) (opp p2)"
    by (simp add: add_comm [of a b] add_closed opp_closed)
  also from ab p3 p2 have " = p3" by (rule add_minus_id)
  also have " = add a Infinity p3" by (simp add: add_0_l)
  also from p2 have " = add a (add a p2 (opp p2)) p3"
    by (simp add: add_opp)
  also from p2 have " = add a (add a (opp p2) p2) p3"
    by (simp add: add_comm [of a b] opp_closed)
  finally show ?thesis using p1 = opp p2 by simp
next
  assume "p2 = opp p3"
  from p3
  have "add a p1 (add a (opp p3) p3) = add a p1 (add a p3 (opp p3))"
    by (simp add: add_comm [of a b] opp_closed)
  also from ab p1 p3
  have " = add a (add a p1 (opp p3)) (opp (opp p3))"
    by (simp add: add_opp add_minus_id add_0_r opp_closed)
  finally show ?thesis using p3 p2 = opp p3
    by (simp add: opp_opp)
next
  assume eq: "opp p1 = add a p2 p3"
  from eq [symmetric] p1
  have "add a p1 (add a p2 p3) = Infinity" by (simp add: add_opp)
  also from p3 have " = add a p3 (opp p3)" by (simp add: add_opp)
  also from p3 have " = add a (opp p3) p3"
    by (simp add: add_comm [of a b] opp_closed)
  also from ab p2 p3
  have " = add a (add a (add a (opp p3) (opp p2)) (opp (opp p2))) p3"
    by (simp add: add_minus_id opp_closed)
  also from p2 p3
  have " = add a (add a (add a (opp p2) (opp p3)) p2) p3"
    by (simp add: add_comm [of a b] opp_opp opp_closed)
  finally show ?thesis
    using opp_add [OF p2 p3] eq [symmetric] p1
    by (simp add: opp_opp)
next
  assume eq: "opp p3 = add a p1 p2"
  from opp_add [OF p1 p2] eq [symmetric] p3
  have "add a p1 (add a p2 p3) = add a p1 (add a p2 (add a (opp p1) (opp p2)))"
    by (simp add: opp_opp)
  also from p1 p2
  have " = add a p1 (add a (add a (opp p1) (opp p2)) (opp (opp p2)))"
    by (simp add: add_comm [of a b] opp_opp add_closed opp_closed)
  also from ab p1 p2 have " = Infinity"
    by (simp add: add_minus_id add_opp opp_closed)
  also from p3 have " = add a p3 (opp p3)" by (simp add: add_opp)
  also from p3 have " = add a (opp p3) p3"
    by (simp add: add_comm [of a b] opp_closed)
  finally show ?thesis using eq [symmetric] by simp
qed

lemma spec4_assoc:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  shows "add a p1 (add a p2 p2) = add a (add a p1 p2) p2"
proof (cases "p1 = Infinity")
  case True
  from ab p1 p2 p2
  show ?thesis by (rule degen_assoc) (simp add: True)
next
  case False
  show ?thesis
  proof (cases "p2 = Infinity")
    case True
    from ab p1 p2 p2
    show ?thesis by (rule degen_assoc) (simp add: True)
  next
    case False
    show ?thesis
    proof (cases "p2 = opp p2")
      case True
      from ab p1 p2 p2
      show ?thesis by (rule degen_assoc) (simp add: True [symmetric])
    next
      case False
      show ?thesis
      proof (cases "p1 = opp p2")
        case True
        from ab p1 p2 p2
        show ?thesis by (rule degen_assoc) (simp add: True)
      next
        case False
        show ?thesis
        proof (cases "opp p1 = add a p2 p2")
          case True
          from ab p1 p2 p2
          show ?thesis by (rule degen_assoc) (simp add: True)
        next
          case False
          show ?thesis
          proof (cases "opp p2 = add a p1 p2")
            case True
            from ab p1 p2 p2
            show ?thesis by (rule degen_assoc) (simp add: True)
          next
            case False
            show ?thesis
            proof (cases "p1 = add a p2 p2")
              case True
              from p1 p2 p1  opp p2 p2  opp p2
                opp p1  add a p2 p2 opp p2  add a p1 p2
                p1  Infinity p2  Infinity
              show ?thesis
                apply (simp add: True)
                apply (rule spec3_assoc)
                apply (simp_all add: is_generic_def is_tangent_def)
                apply (rule notI)
                apply (drule uniq_zero [OF ab p2 p2])
                apply simp
                apply (intro conjI notI)
                apply (erule notE)
                apply (rule uniq_opp [of a])
                apply (simp add: add_comm [of a b] add_closed)
                apply (erule notE)
                apply (drule uniq_zero [OF ab add_closed [OF p2 p2] p2])
                apply simp
                done
            next
              case False
              show ?thesis
              proof (cases "p2 = add a p1 p2")
                case True
                from ab p1 p2 True [symmetric]
                have "p1 = Infinity" by (rule uniq_zero)
                then show ?thesis by (simp add: add_0_l)
              next
                case False
                show ?thesis
                proof (cases "p1 = p2")
                  case True
                  with p2 show ?thesis
                    by (simp add: add_comm [of a b] add_closed)
                next
                  case False
                  with p1 p2 p1  Infinity p2  Infinity
                    p1  opp p2 p2  opp p2
                    p1  add a p2 p2 p2  add a p1 p2 opp p2  add a p1 p2
                  show ?thesis
                    apply (rule_tac spec2_assoc)
                    apply (simp_all add: is_generic_def is_tangent_def)
                    apply (rule notI)
                    apply (erule notE [of "p1 = opp p2"])
                    apply (rule uniq_opp [of a])
                    apply (simp add: add_comm)
                    apply (intro conjI notI)
                    apply (erule notE [of "p2 = opp p2"])
                    apply (rule uniq_opp)
                    apply assumption+
                    apply (rule notE [OF opp p1  add a p2 p2])
                    apply (simp add: opp_opp)
                    done
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma add_assoc:
  assumes ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  shows "add a p1 (add a p2 p3) = add a (add a p1 p2) p3"
proof (cases "p1 = Infinity")
  case True
  from ab p1 p2 p3
  show ?thesis by (rule degen_assoc) (simp add: True)
next
  case False
  show ?thesis
  proof (cases "p2 = Infinity")
    case True
    from ab p1 p2 p3
    show ?thesis by (rule degen_assoc) (simp add: True)
  next
    case False
    show ?thesis
    proof (cases "p3 = Infinity")
      case True
      from ab p1 p2 p3
      show ?thesis by (rule degen_assoc) (simp add: True)
    next
      case False
      show ?thesis
      proof (cases "p1 = p2")
        case True
        from p2 p3
        have "add a p2 (add a p2 p3) = add a (add a p3 p2) p2"
          by (simp add: add_comm [of a b] add_closed)
        also from ab p3 p2 have " = add a p3 (add a p2 p2)"
          by (simp add: spec4_assoc)
        also from p2 p3
        have " = add a (add a p2 p2) p3"
          by (simp add: add_comm [of a b] add_closed)
        finally show ?thesis using True by simp
      next
        case False
        show ?thesis
        proof (cases "p1 = opp p2")
          case True
          from ab p1 p2 p3
          show ?thesis by (rule degen_assoc) (simp add: True)
        next
          case False
          show ?thesis
          proof (cases "p2 = p3")
            case True
            with ab p1 p3 show ?thesis
              by (simp add: spec4_assoc)
          next
            case False
            show ?thesis
            proof (cases "p2 = opp p3")
              case True
              from ab p1 p2 p3
              show ?thesis by (rule degen_assoc) (simp add: True)
            next
              case False
              show ?thesis
              proof (cases "opp p1 = add a p2 p3")
                case True
                from ab p1 p2 p3
                show ?thesis by (rule degen_assoc) (simp add: True)
              next
                case False
                show ?thesis
                proof (cases "opp p3 = add a p1 p2")
                  case True
                  from ab p1 p2 p3
                  show ?thesis by (rule degen_assoc) (simp add: True)
                next
                  case False
                  show ?thesis
                  proof (cases "p1 = add a p2 p3")
                    case True
                    with ab p2 p3 show ?thesis
                      apply simp
                      apply (rule cancel [OF ab opp_closed [OF p3]])
                      apply (simp_all add: add_closed)
                      apply (simp add: spec4_assoc add_closed opp_closed)
                      apply (simp add: add_comm [of a b "opp p3"]
                        add_closed opp_closed add_minus_id)
                      apply (simp add: add_comm [of a b] add_closed)
                      done
                  next
                    case False
                    show ?thesis
                    proof (cases "p3 = add a p1 p2")
                      case True
                      with ab p1 p2 show ?thesis
                        apply simp
                        apply (rule cancel [OF ab opp_closed [OF p1]])
                        apply (simp_all add: add_closed)
                        apply (simp add: spec4_assoc add_closed opp_closed)
                        apply (simp add: add_comm [of a b "opp p1"] add_comm [of a b p1]
                          add_closed opp_closed add_minus_id)
                        done
                    next
                      case False
                      with p1 p2 p3
                        p1  Infinity p2  Infinity p3  Infinity
                        p1  p2 p1  opp p2 p2  p3 p2  opp p3
                        opp p3  add a p1 p2 p1  add a p2 p3
                      show ?thesis
                        apply (rule_tac spec1_assoc [of a b])
                        apply (simp_all add: is_generic_def)
                        apply (rule notI)
                        apply (erule notE [of "p1 = opp p2"])
                        apply (rule uniq_opp [of a])
                        apply (simp add: add_comm)
                        apply (intro conjI notI)
                        apply (erule notE [of "p2 = opp p3"])
                        apply (rule uniq_opp [of a])
                        apply (simp add: add_comm)
                        apply (rule notE [OF opp p1  add a p2 p3])
                        apply (simp add: opp_opp)
                        done
                    qed
                  qed
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed
  
lemma add_comm':
  "nonsingular a b 
   on_curve a b p1  on_curve a b p2  on_curve a b p3 
   add a p2 (add a p1 p3) = add a p1 (add a p2 p3)"
   by (simp add: add_assoc add_comm)

primrec (in ell_field) point_mult :: "'a  nat  'a point  'a point"
where
    "point_mult a 0 p = Infinity"
  | "point_mult a (Suc n) p = add a p (point_mult a n p)"

lemma point_mult_closed: "on_curve a b p  on_curve a b (point_mult a n p)"
  by (induct n) (simp_all add: add_closed)

lemma point_mult_add:
  "on_curve a b p  nonsingular a b 
   point_mult a (m + n) p = add a (point_mult a m p) (point_mult a n p)"
  by (induct m) (simp_all add: add_assoc point_mult_closed add_0_l)

lemma point_mult_mult:
  "on_curve a b p  nonsingular a b 
   point_mult a (m * n) p = point_mult a n (point_mult a m p)"
   by (induct n) (simp_all add: point_mult_add)

lemma point_mult2_eq_double:
  "point_mult a 2 p = add a p p"
  by (simp add: numeral_2_eq_2 add_0_r)

subsection ‹Projective Coordinates›

type_synonym 'a ppoint = "'a × 'a × 'a"

context ell_field begin

definition pdouble :: "'a  'a ppoint  'a ppoint" where
  "pdouble a p =
     (let (x, y, z) = p
      in
        if z = 0 then p
        else
          let
            l = 2 * y * z;
            m = 3 * x ^ 2 + a * z ^ 2
          in
            (l * (m ^ 2 - 4 * x * y * l),
             m * (6 * x * y * l - m ^ 2) -
             2 * y ^ 2 * l ^ 2,
             l ^ 3))"

definition padd :: "'a  'a ppoint  'a ppoint  'a ppoint" where
  "padd a p1 p2 =
     (let
        (x1, y1, z1) = p1;
        (x2, y2, z2) = p2
      in
        if z1 = 0 then p2
        else if z2 = 0 then p1
        else
          let
            d1 = x2 * z1;
            d2 = x1 * z2;
            l = d1 - d2;
            m = y2 * z1 - y1 * z2
          in
            if l = 0 then
              if m = 0 then pdouble a p1
              else (0, 0, 0)
            else
              let h = m ^ 2 * z1 * z2 - (d1 + d2) * l ^ 2
              in
                (l * h,
                 (d2 * l ^ 2 - h) * m - l ^ 3 * y1 * z2,
                 l ^ 3 * z1 * z2))"

definition make_affine :: "'a ppoint  'a point" where
  "make_affine p =
     (let (x, y, z) = p
      in if z = 0 then Infinity else Point (x / z) (y / z))"

definition on_curvep :: "'a  'a  'a ppoint  bool" where
  "on_curvep a b = (λ(x, y, z). z  0 
     y ^ 2 * z = x ^ 3 + a * x * z ^ 2 + b * z ^ 3)"

end

lemma on_curvep_infinity [simp]: "on_curvep a b (x, y, 0)"
  by (simp add: on_curvep_def)

lemma make_affine_infinity [simp]: "make_affine (x, y, 0) = Infinity"
  by (simp add: make_affine_def)

lemma on_curvep_iff_on_curve:
  "on_curvep a b p = on_curve a b (make_affine p)"
proof (induct p rule: prod_induct3)
  case (fields x y z)
  show "on_curvep a b (x, y, z) = on_curve a b (make_affine (x, y, z))"
  proof
    assume H: "on_curvep a b (x, y, z)"
    then have yz: "z  0  y ^ 2 * z = x ^ 3 + a * x * z ^ 2 + b * z ^ 3"
      by (simp_all add: on_curvep_def)
    show "on_curve a b (make_affine (x, y, z))"
    proof (cases "z = 0")
      case True
      then show ?thesis by (simp add: on_curve_def make_affine_def)
    next
      case False
      then show ?thesis
        apply (simp add: on_curve_def make_affine_def)
        apply (field yz [OF False])
        apply assumption
        done
    qed
  next
    assume H: "on_curve a b (make_affine (x, y, z))"
    show "on_curvep a b (x, y, z)"
    proof (cases "z = 0")
      case True
      then show ?thesis
        by (simp add: on_curvep_def)
    next
      case False
      from H show ?thesis
        apply (simp add: on_curve_def on_curvep_def make_affine_def False)
        apply (field (prems))
        apply field
        apply (simp_all add: False)
        done
    qed
  qed
qed

lemma pdouble_infinity [simp]: "pdouble a (x, y, 0) = (x, y, 0)"
  by (simp add: pdouble_def)

lemma padd_infinity_l [simp]: "padd a (x, y, 0) p = p"
  by (simp add: padd_def)

lemma pdouble_correct:
  "make_affine (pdouble a p) = add a (make_affine p) (make_affine p)"
proof (induct p rule: prod_induct3)
  case (fields x y z)
  then show ?case
    apply (auto simp add: add_def pdouble_def make_affine_def eq_opp_is_zero Let_def)
    apply field
    apply simp
    apply field
    apply simp
    done
qed

lemma padd_correct:
  assumes p1: "on_curvep a b p1" and p2: "on_curvep a b p2"
  shows "make_affine (padd a p1 p2) = add a (make_affine p1) (make_affine p2)"
  using p1
proof (induct p1 rule: prod_induct3)
  case (fields x1 y1 z1)
  note p1' = fields
  from p2 show ?case
  proof (induct p2 rule: prod_induct3)
    case (fields x2 y2 z2)
    then have
      yz2: "z2  0  y2 ^ 2 * z2 * z1 ^ 3 =
        (x2 ^ 3 + a * x2 * z2 ^ 2 + b * z2 ^ 3) * z1 ^ 3"
      by (simp_all add: on_curvep_def)
    from p1' have
      yz1: "z1  0  y1 ^ 2 * z1 * z2 ^ 3 =
        (x1 ^ 3 + a * x1 * z1 ^ 2 + b * z1 ^ 3) * z2 ^ 3"
      by (simp_all add: on_curvep_def)
    show ?case
    proof (cases "z1 = 0")
      case True
      then show ?thesis
        by (simp add: add_def padd_def make_affine_def)
    next
      case False
      show ?thesis
      proof (cases "z2 = 0")
        case True
        then show ?thesis
          by (simp add: add_def padd_def make_affine_def)
      next
        case False
        show ?thesis
        proof (cases "x2 * z1 - x1 * z2 = 0")
          case True
          note x = this
          then have x': "x2 * z1 = x1 * z2" by simp
          show ?thesis
          proof (cases "y2 * z1 - y1 * z2 = 0")
            case True
            then have y: "y2 * z1 = y1 * z2" by simp
            from z1  0 z2  0 x
            have "make_affine (x2, y2, z2) = make_affine (x1, y1, z1)"
              apply (simp add: make_affine_def)
              apply (rule conjI)
              apply (field x')
              apply simp
              apply (field y)
              apply simp
              done
            with True x z1  0 z2  0 p1' fields show ?thesis
              by (simp add: padd_def pdouble_correct)
          next
            case False
            have "y2 ^ 2 * z1 ^ 3 * z2 = y1 ^ 2 * z1 * z2 ^ 3"
              by (ring yz1 [OF z1  0] yz2 [OF z2  0] x')
            then have "y2 ^ 2 * z1 ^ 3 * z2 / z1 / z2 =
              y1 ^ 2 * z1 * z2 ^ 3 / z1 / z2"
              by simp
            then have "(y2 * z1) * (y2 * z1) = (y1 * z2) * (y1 * z2)"
              apply (field (prems))
              apply (field)
              apply (rule TrueI)
              apply (simp add: z1  0 z2  0)
              done
            with False
            have y2z1: "y2 * z1 = - (y1 * z2)"
              by (simp add: square_eq_iff)
            from x False z1  0 z2  0 show ?thesis
              apply (simp add: padd_def add_def make_affine_def Let_def)
              apply (rule conjI)
              apply (rule impI)
              apply (field x')
              apply simp
              apply (field y2z1)
              apply simp
              done
          qed
        next
          case False
          then have "x1 / z1  x2 / z2"
            apply (rule_tac notI)
            apply (erule notE)
            apply (drule sym)
            apply (field (prems))
            apply ring
            apply (simp add: z1  0 z2  0)
            done
          with False z1  0 z2  0
          show ?thesis
            apply (auto simp add: padd_def add_def make_affine_def Let_def)
            apply field
            apply simp
            apply field
            apply simp
            done
        qed
      qed
    qed
  qed
qed

lemma pdouble_closed:
  "on_curvep a b p  on_curvep a b (pdouble a p)"
  by (simp add: on_curvep_iff_on_curve pdouble_correct add_closed)

lemma padd_closed:
  "on_curvep a b p1  on_curvep a b p2  on_curvep a b (padd a p1 p2)"
  by (simp add: on_curvep_iff_on_curve padd_correct add_closed)

primrec (in ell_field) ppoint_mult :: "'a  nat  'a ppoint  'a ppoint"
where
    "ppoint_mult a 0 p = (0, 0, 0)"
  | "ppoint_mult a (Suc n) p = padd a p (ppoint_mult a n p)"

lemma ppoint_mult_closed [simp]:
  "on_curvep a b p  on_curvep a b (ppoint_mult a n p)"
  by (induct n) (simp_all add: padd_closed)

lemma ppoint_mult_correct: "on_curvep a b p 
  make_affine (ppoint_mult a n p) = point_mult a n (make_affine p)"
  by (induct n) (simp_all add: padd_correct)

context ell_field begin

definition proj_eq :: "'a ppoint  'a ppoint  bool" where
  "proj_eq = (λ(x1, y1, z1) (x2, y2, z2).
     (z1 = 0) = (z2 = 0)  x1 * z2 = x2 * z1  y1 * z2 = y2 * z1)"

end

lemma proj_eq_refl: "proj_eq p p"
  by (auto simp add: proj_eq_def)

lemma proj_eq_sym: "proj_eq p p'  proj_eq p' p"
  by (auto simp add: proj_eq_def)

lemma proj_eq_trans:
  "in_carrierp p  in_carrierp p'  in_carrierp p'' 
   proj_eq p p'  proj_eq p' p''  proj_eq p p''"
proof (induct p rule: prod_induct3)
  case (fields x y z)
  then show ?case
  proof (induct p' rule: prod_induct3)
    case (fields x' y' z')
    then show ?case
    proof (induct p'' rule: prod_induct3)
      case (fields x'' y'' z'')
      then have
        z: "(z = 0) = (z' = 0)" "(z' = 0) = (z'' = 0)" and
        "x * z' * z'' = x' * z * z''"
        "y * z' * z'' = y' * z * z''"
        and xy:
        "x' * z'' = x'' * z'"
        "y' * z'' = y'' * z'"
        by (simp_all add: proj_eq_def)
      from x * z' * z'' = x' * z * z''
      have "(x * z'') * z' = (x'' * z) * z'"
        by (ring (prems) xy) (ring xy)
      moreover from y * z' * z'' = y' * z * z''
      have "(y * z'') * z' = (y'' * z) * z'"
        by (ring (prems) xy) (ring xy)
      ultimately show ?case using z
        by (auto simp add: proj_eq_def)
    qed
  qed
qed

lemma make_affine_proj_eq_iff:
  "proj_eq p p' = (make_affine p = make_affine p')"
proof (induct p rule: prod_induct3)
  case (fields x y z)
  then show ?case
  proof (induct p' rule: prod_induct3)
    case (fields x' y' z')
    show ?case
    proof
      assume "proj_eq (x, y, z) (x', y', z')"
      then have "(z = 0) = (z' = 0)"
        and xy: "x * z' = x' * z" "y * z' = y' * z"
        by (simp_all add: proj_eq_def)
      then show "make_affine (x, y, z) = make_affine (x', y', z')"
        apply (auto simp add: make_affine_def)
        apply (field xy)
        apply simp
        apply (field xy)
        apply simp
        done
    next
      assume H: "make_affine (x, y, z) = make_affine (x', y', z')"
      show "proj_eq (x, y, z) (x', y', z')"
      proof (cases "z = 0")
        case True
        with H have "z' = 0" by (simp add: make_affine_def split: if_split_asm)
        with True show ?thesis by (simp add: proj_eq_def)
      next
        case False
        with H have "z'  0" "x / z = x' / z'" "y / z = y' / z'"
          by (simp_all add: make_affine_def split: if_split_asm)
        from x / z = x' / z'
        have "x * z' = x' * z"
          apply (field (prems))
          apply field
          apply (simp_all add: z  0 z'  0)
          done
        moreover from y / z = y' / z'
        have "y * z' = y' * z"
          apply (field (prems))
          apply field
          apply (simp_all add: z  0 z'  0)
          done
        ultimately show ?thesis
          by (simp add: proj_eq_def z  0 z'  0)
      qed
    qed
  qed
qed

lemma pdouble_proj_eq_cong:
  "proj_eq p p'  proj_eq (pdouble a p) (pdouble a p')"
  by (simp add: make_affine_proj_eq_iff pdouble_correct)

lemma padd_proj_eq_cong:
  "on_curvep a b p1  on_curvep a b p1'  on_curvep a b p2  on_curvep a b p2' 
   proj_eq p1 p1'  proj_eq p2 p2'  proj_eq (padd a p1 p2) (padd a p1' p2')"
  by (simp add: make_affine_proj_eq_iff padd_correct)

end