Theory Elliptic_Curves_Group_Law.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