Theory Elliptic_Locale

section ‹Formalization using Locales›

theory Elliptic_Locale
imports "HOL-Decision_Procs.Reflective_Field"
begin

subsection ‹Affine Coordinates›

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

locale ell_field = field +
  assumes two_not_zero: "«2» ≠ 𝟬"
begin

declare two_not_zero [simplified, simp add]

lemma neg_equal_zero:
  assumes x: "x ∈ carrier R"
  shows "(⊖ x = x) = (x = 𝟬)"
proof
  assume "⊖ x = x"
  with x have "«2» ⊗ x = x ⊕ ⊖ x"
    by (simp add: of_int_2 l_distr)
  with x show "x = 𝟬" by (simp add: r_neg integral_iff)
qed simp

lemmas equal_neg_zero = trans [OF eq_commute neg_equal_zero]

definition nonsingular :: "'a ⇒ 'a ⇒ bool" where
  "nonsingular a b = («4» ⊗ a [^] (3::nat) ⊕ «27» ⊗ b [^] (2::nat) ≠ 𝟬)"

definition on_curve :: "'a ⇒ 'a ⇒ 'a point ⇒ bool" where
  "on_curve a b p = (case p of
       Infinity ⇒ True
     | Point x y ⇒ x ∈ carrier R ∧ y ∈ carrier R ∧
         y [^] (2::nat) = x [^] (3::nat) ⊕ 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::nat) ⊕ a) ⊘ («2» ⊗ y1);
                 x3 = l [^] (2::nat) ⊖ «2» ⊗ x1
               in
                 Point x3 (⊖ y1 ⊖ l ⊗ (x3 ⊖ x1))
           else
             let
               l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1);
               x3 = l [^] (2::nat) ⊖ 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))"

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: "on_curve a b p ⟹ opp (opp p) = p"
  by (auto simp add: opp_def on_curve_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
    l_minus r_minus 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 ∈ carrier R" "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
    by (simp_all add: on_curve_def)
  moreover from ‹p2 = Point x2 y2› ‹on_curve a b p2› ‹x1 = x2›
  have "y2 ∈ carrier R" "x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b = y2 [^] (2::nat)"
    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 "a ∈ carrier R" and "b ∈ carrier R"
  and "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
        from ‹on_curve a b p1› Point' True'
        have "x2 ∈ carrier R" "y1 ∈ carrier R" and
          on_curve1: "y1 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
          by (simp_all add: on_curve_def)
        from False True' Point Point' assms
        have "y1 ≠ 𝟬"
          apply (auto simp add: on_curve_def nat_pow_zero)
          apply (drule sym [of 𝟬])
          apply simp
          done
        with False True' Point Point' assms
        show ?thesis
          apply (simp add: on_curve_def add_def Let_def integral_iff)
          apply (field on_curve1)
          apply (simp add: integral_iff)
          done
      qed
    next
      case False
      from ‹on_curve a b p1› Point'
      have  "x1 ∈ carrier R" "y1 ∈ carrier R"
        and on_curve1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
        by (simp_all add: on_curve_def)
      from ‹on_curve a b p2› Point
      have "x2 ∈ carrier R" "y2 ∈ carrier R"
        and on_curve2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
        by (simp_all add: on_curve_def)
      from assms not_sym [OF False] show ?thesis
        apply (simp add: on_curve_def add_def Let_def False Point Point' eq_diff0)
        apply (field on_curve1 on_curve2)
        apply (simp add: eq_diff0)
        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 4, case_names InfL InfR Opp Tan Gen]:
  assumes "a ∈ carrier R"
  and "b ∈ carrier R"
  and 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 ≠ 𝟬 ⟹
    l = («3» ⊗ x1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ y1) ⟹
    x2 = l [^] (2::nat) ⊖ «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::nat) ⊖ 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
  with p have "x1 ∈ carrier R" "y1 ∈ carrier R"
    and p': "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
    by (simp_all add: on_curve_def)
  show ?thesis
  proof (cases q)
    case Infinity
    with Point show ?thesis
      by (simp add: add_def R2)
  next
    case (Point x2 y2)
    with q have "x2 ∈ carrier R" "y2 ∈ carrier R"
      and q': "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
      by (simp_all add: on_curve_def)
    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] ‹y2 ∈ carrier R› show ?thesis
          by (simp add: add_def opp_def)
      next
        case False
        have "(y1 ⊖ y2) ⊗ (y1 ⊕ y2) = 𝟬"
          by (ring True' p' q')
        with False ‹y1 ∈ carrier R› ‹y2 ∈ carrier R› have "y1 = y2"
          by (simp add: eq_neg_iff_add_eq_0 integral_iff eq_diff0)
        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 add_casew [consumes 4, case_names InfL InfR Opp Gen]:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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::nat) ⊕ a) ⊘ («2» ⊗ y1) ∨
    x1 ≠ x2 ∧ l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1) ⟹
    x3 = l [^] (2::nat) ⊖ x1 ⊖ x2 ⟹
    y3 = ⊖ y1 ⊖ l ⊗ (x3 ⊖ x1) ⟹
    P p1 p2 p3"
  shows "P p q (add a p q)"
  using a b p q p q
proof (induct rule: add_case)
  case InfL
  show ?case by (rule R1)
next
  case InfR
  show ?case by (rule R2)
next
  case (Opp p)
  from ‹on_curve a b p› show ?case by (rule R3)
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  with a b show ?case
    apply (rule_tac R4)
    apply assumption+
    apply (simp add: opp_Point equal_neg_zero on_curve_def)
    apply simp
    apply (simp add: minus_eq mult2 integral_iff a_assoc r_minus on_curve_def)
    apply simp
    done
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then show ?case
    apply (rule_tac R4)
    apply assumption+
    apply (simp add: opp_Point)
    apply simp_all
    done
qed

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 spec1_assoc:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b ‹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 a b ‹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 a b ‹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 ‹on_curve a b p› ‹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 a b ‹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)
      with a b 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 ‹on_curve a b p› ‹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
        from
          ‹on_curve a b p1› ‹p1 = Point x1 y1›
          ‹on_curve a b p2› ‹p2 = Point x2 y2›
          ‹on_curve a b p3› ‹p3 = Point x3 y3›
        have
          "x1 ∈ carrier R" "y1 ∈ carrier R" and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b" and
          "x2 ∈ carrier R" "y2 ∈ carrier R" and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b" and
          "x3 ∈ carrier R" "y3 ∈ carrier R" and y3: "y3 [^] (2::nat) = x3 [^] (3::nat) ⊕ a ⊗ x3 ⊕ b"
          by (simp_all add: on_curve_def)
        show ?case
          apply (simp add: ‹p6 = Point x6 y6› ‹p7 = Point x7 y7›)
          apply (simp only: ps
            ‹x6 = l2 [^] 2 ⊖ x1' ⊖ x5'› ‹x7 = l3 [^] 2 ⊖ 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 = l1 [^] 2 ⊖ x2' ⊖ x3› ‹y5 = ⊖ y2' ⊖ l1 ⊗ (x5 ⊖ x2')›
            ‹x4 = l [^] 2 ⊖ x1 ⊖ x2› ‹y4 = ⊖ y1 ⊖ l ⊗ (x4 ⊖ x1)›)
          apply (rule conjI)
          apply (field y1 y2 y3)
          apply (rule conjI)
          apply (simp add: eq_diff0 ‹x3 ∈ carrier R› ‹x2 ∈ carrier R›
            not_sym [OF ‹x2' ≠ x3› [simplified ‹x2' = x2›]])
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (cut_tac ‹x1' ≠ x5'› [simplified ‹x5' = x5› ‹x1' = x1› ‹x5 = l1 [^] 2 ⊖ x2' ⊖ x3›
            ‹l1 = (y3 ⊖ y2') ⊘ (x3 ⊖ x2')› ‹y2' = y2› ‹x2' = x2›])
          apply (erule notE)
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: eq_diff0 ‹x3 ∈ carrier R› ‹x2 ∈ carrier R›
            not_sym [OF ‹x2' ≠ x3› [simplified ‹x2' = x2›]])
          apply (rule conjI)
          apply (simp add: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (cut_tac ‹x4' ≠ x3'› [simplified ‹x4' = x4› ‹x3' = x3› ‹x4 = l [^] 2 ⊖ x1 ⊖ x2›
            ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)›])
          apply (erule notE)
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          apply (field y1 y2 y3)
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (cut_tac ‹x1' ≠ x5'› [simplified ‹x5' = x5› ‹x1' = x1› ‹x5 = l1 [^] 2 ⊖ x2' ⊖ x3›
            ‹l1 = (y3 ⊖ y2') ⊘ (x3 ⊖ x2')› ‹y2' = y2› ‹x2' = x2›])
          apply (erule notE)
          apply (rule sym)
          apply (field y1 y2)
          apply (simp add: eq_diff0 ‹x3 ∈ carrier R› ‹x2 ∈ carrier R›
            not_sym [OF ‹x2' ≠ x3› [simplified ‹x2' = x2›]])
          apply (rule conjI)
          apply (simp add: eq_diff0 ‹x3 ∈ carrier R› ‹x2 ∈ carrier R›
            not_sym [OF ‹x2' ≠ x3› [simplified ‹x2' = x2›]])
          apply (rule conjI)
          apply (rule notI)
          apply (ring (prems) y1 y2)
          apply (cut_tac ‹x4' ≠ x3'› [simplified ‹x4' = x4› ‹x3' = x3› ‹x4 = l [^] 2 ⊖ x1 ⊖ x2›
            ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)›])
          apply (erule notE)
          apply (rule sym)
          apply (field y1 y2)
          apply (simp_all add: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          done
      qed
    qed
  qed
qed

lemma spec2_assoc:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b ‹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 a b ‹on_curve a b p2› ‹p5 = add a p2 p2›
    have "on_curve a b p5" by (simp add: add_closed)
    with a b ‹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 a b ‹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)
      with a b 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)› ‹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 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
          "x1 ∈ carrier R" "y1 ∈ carrier R" and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b" and
          "x2 ∈ carrier R" "y2 ∈ carrier R" and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ 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: integral_iff [OF _ ‹y2 ∈ carrier R›] ‹y2' ≠ 𝟬› [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: integral_iff [OF _ ‹y2 ∈ carrier R›] ‹y2' ≠ 𝟬› [simplified ‹y2' = y2›])
          apply (simp add: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          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: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          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: integral_iff [OF _ ‹y2 ∈ carrier R›] ‹y2' ≠ 𝟬› [simplified ‹y2' = y2›])
          apply (simp add: integral_iff [OF _ ‹y2 ∈ carrier R›] ‹y2' ≠ 𝟬› [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: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
          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 a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b ‹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 a b ‹on_curve a b p2› ‹p5 = add a p2 p2›
    have "on_curve a b p5" by (simp add: add_closed)
    with a b ‹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 a b ‹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)
      with a b 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)› ‹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 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
          "x1 ∈ carrier R" "y1 ∈ carrier R" and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b" and
          "x2 ∈ carrier R" "y2 ∈ carrier R" and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ 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 ∈ carrier R› ‹y2' ≠ 𝟬› ‹y2' = y2›
        have "«2» ⊗ y2 ≠ 𝟬" by (simp add: integral_iff)
        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' ≠ 𝟬›])
          apply (simp only: ps qs)
          apply field
          apply (rule ‹«2» ⊗ y2 ≠ 𝟬›)
          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 ≠ 𝟬›)
          apply (rule ‹«2» ⊗ y2 ≠ 𝟬›)
          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 ≠ 𝟬›)
          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 ≠ 𝟬›)
          apply (field y2)
          apply (intro conjI)
          apply (rule notI)
          apply (ring (prems))
          apply (rule notE [OF ‹y1' ≠ 𝟬›])
          apply (simp only: ps qs)
          apply field
          apply (rule ‹«2» ⊗ y2 ≠ 𝟬›)
          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 ≠ 𝟬›)
          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 ≠ 𝟬›)
          apply (rule ‹«2» ⊗ y2 ≠ 𝟬›)
          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 ≠ 𝟬›)
          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 "a ∈ carrier R" "b ∈ carrier R" "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 "x1 ∈ carrier R" "y1 ∈ carrier R"
    and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
    by (simp_all 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 "x2 ∈ carrier R" "y2 ∈ carrier R"
      and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
      by (simp_all 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› ‹y2 ∈ carrier R› show ?thesis
          by (simp add: add_def)
      next
        case False
        with y1 y2 [symmetric] ‹y1 ∈ carrier R› ‹y2 ∈ carrier R› ‹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 (cut_tac ‹x1 ∈ carrier R› ‹x2 ∈ carrier R›)
        apply (simp add: eq_diff0)
        apply field
        apply (cut_tac ‹x1 ∈ carrier R› ‹x2 ∈ carrier R›)
        apply (simp add: eq_diff0)
        done
    qed
  qed
qed

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

lemma uniq_zero:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 ‹on_curve a b p1› ‹p1 = Point x1 y1›
  have "x1 ∈ carrier R" "y1 ∈ carrier R" by (simp_all add: on_curve_def)
  with a ‹l = («3» ⊗ x1 [^] 2 ⊕ a) ⊘ («2» ⊗ y1)› ‹y1 ≠ 𝟬›
  have "l ∈ carrier R" by (simp add: integral_iff)
  from ‹p1 = Point x1 y1› ‹p2 = Point x2 y2› ‹p2 = p1›
  have "x2 = x1" "y2 = y1" by simp_all
  with ‹x1 ∈ carrier R› ‹y1 ∈ carrier R› ‹l ∈ carrier R› ‹y2 = ⊖ y1 ⊖ l ⊗ (x2 ⊖ x1)› ‹y1 ≠ 𝟬›
  have "⊖ y1 = y1" by (simp add: r_neg minus_eq)
  with ‹y1 ∈ carrier R› ‹y1 ≠ 𝟬›
  show ?case by (simp add: neg_equal_zero)
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then have "x1 ∈ carrier R" "y1 ∈ carrier R" "x2 ∈ carrier R" "y2 ∈ carrier R"
    and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
    and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
    by (simp_all add: on_curve_def)
  with ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)› ‹x1 ≠ x2›
  have "l ∈ carrier R" by (simp add: eq_diff0)
  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›
    ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹y1 ∈ carrier R› ‹y2 ∈ carrier R›
  have "l ⊗ (x2 ⊖ x1) = y2 ⊖ y1"
    by (simp add: m_div_def m_assoc eq_diff0)
  also from ‹y1 ∈ carrier R› ‹y2 ∈ carrier R›
  have "⊖ y1 ⊖ (y2 ⊖ y1) = (⊖ y1 ⊕ y1) ⊕ ⊖ y2"
    by (simp add: minus_eq minus_add a_ac)
  finally have "y2 = 𝟬" using ‹y1 ∈ carrier R› ‹y2 ∈ carrier R›
    by (simp add: l_neg equal_neg_zero)
  with ‹p2 = Point x2 y2› ‹on_curve a b p2›
    ‹a ∈ carrier R› ‹b ∈ carrier R› ‹x2 ∈ carrier R›
  have x2: "x2 [^] (3::nat) = ⊖ (a ⊗ x2 ⊕ b)"
    by (simp add: on_curve_def nat_pow_zero eq_neg_iff_add_eq_0 a_assoc)
  from ‹x3 = l [^] 2 ⊖ x1 ⊖ x2› ‹x3 = x2›
  have "l [^] (2::nat) ⊖ x1 ⊖ x2 ⊖ x2 = x2 ⊖ x2" by simp
  with ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹l ∈ carrier R›
  have "l [^] (2::nat) ⊖ x1 ⊖ «2» ⊗ x2 = 𝟬"
    by (simp add: of_int_2 l_distr minus_eq a_ac minus_add r_neg)
  then have "x2 ⊗ (l [^] (2::nat) ⊖ x1 ⊖ «2» ⊗ x2) = x2 ⊗ 𝟬" by simp
  then have "(x2 ⊖ x1) ⊗ («2» ⊗ a ⊗ x2 ⊕ «3» ⊗ b) = 𝟬"
    apply (simp add: ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)› ‹y2 = 𝟬›)
    apply (field (prems) y1 x2)
    apply (ring y1 x2)
    apply (simp add: eq_diff0 ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› not_sym [OF ‹x1 ≠ x2›])
    done
  with not_sym [OF ‹x1 ≠ x2›]
    ‹x2 ∈ carrier R› ‹x1 ∈ carrier R› ‹a ∈ carrier R› ‹b ∈ carrier R›
  have "«2» ⊗ a ⊗ x2 ⊕ «3» ⊗ b = 𝟬"
    by (simp add: integral_iff eq_diff0)
  with ‹a ∈ carrier R› ‹b ∈ carrier R› ‹x2 ∈ carrier R›
  have "«2» ⊗ a ⊗ x2 = ⊖ («3» ⊗ b)"
    by (simp add: eq_neg_iff_add_eq_0)
  from y2 [symmetric] ‹y2 = 𝟬› ‹a ∈ carrier R›
  have "⊖ («2» ⊗ a) [^] (3::nat) ⊗ (x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b) = 𝟬"
    by (simp add: nat_pow_zero)
  then have "b ⊗ («4» ⊗ a [^] (3::nat) ⊕ «27» ⊗ b [^] (2::nat)) = 𝟬"
    apply (ring (prems) ‹«2» ⊗ a ⊗ x2 = ⊖ («3» ⊗ b)›)
    apply (ring ‹«2» ⊗ a ⊗ x2 = ⊖ («3» ⊗ b)›)
    done
  with ab a b have "b = 𝟬" by (simp add: nonsingular_def integral_iff)
  with ‹«2» ⊗ a ⊗ x2 ⊕ «3» ⊗ b = 𝟬› ab a b ‹x2 ∈ carrier R›
  have "x2 = 𝟬" by (simp add: nonsingular_def nat_pow_zero integral_iff)
  from ‹l [^] (2::nat) ⊖ x1 ⊖ «2» ⊗ x2 = 𝟬›
  show ?case
    apply (simp add: ‹x2 = 𝟬› ‹y2 = 𝟬› ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)›)
    apply (field (prems) y1 ‹b = 𝟬›)
    apply (insert a b ab ‹x1 ∈ carrier R› ‹b = 𝟬› ‹x1 ≠ x2› ‹x2 = 𝟬›)
    apply (simp add: nonsingular_def nat_pow_zero integral_iff)
    apply (simp add: trans [OF eq_commute eq_neg_iff_add_eq_0])
    done
qed

lemma opp_add:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 ∈ carrier R" "y1 ∈ carrier R" "x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b = y1 [^] (2::nat)"
      "x2 ∈ carrier R" "y2 ∈ carrier R" "x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b = y2 [^] (2::nat)"
      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 neg_equal_swap)
      apply (rule conjI)
      apply field
      apply (auto simp add: integral_iff nat_pow_zero
        trans [OF eq_commute eq_neg_iff_add_eq_0])[1]
      apply field
      apply (auto simp add: integral_iff nat_pow_zero
        trans [OF eq_commute eq_neg_iff_add_eq_0])[1]
      apply (simp add: add_def opp_def Let_def)
      apply (rule conjI)
      apply field
      apply (simp add: eq_diff0)
      apply field
      apply (simp add: eq_diff0)
      done
  qed
qed

lemma compat_add_opp:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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)
  with ‹on_curve a b p› 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)
  with ‹on_curve a b p1› 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)
  then have "x1 ∈ carrier R" "y1 ∈ carrier R" "x2 ∈ carrier R" "y2 ∈ carrier R"
    by (simp_all add: on_curve_def)
  have "«2» ⊗ «2» ≠ 𝟬"
    by (simp add: integral_iff)
  then have "«4» ≠ 𝟬" by (simp add: of_int_mult [symmetric])
  from Gen have "((⊖ y2 ⊖ y1) ⊘ (x2 ⊖ x1)) [^] (2::nat) ⊖ x1 ⊖ x2 =
    ((y2 ⊖ y1) ⊘ (x2 ⊖ x1)) [^] (2::nat) ⊖ x1 ⊖ x2"
    by (simp add: add_def opp_def Let_def)
  then show ?case
    apply (field (prems))
    apply (insert ‹y1 ∈ carrier R› ‹y2 ∈ carrier R› ‹p1 ≠ opp p1›
      ‹p1 = Point x1 y1› ‹p2 = Point x2 y2› ‹«4» ≠ 𝟬›)[1]
    apply (simp add: integral_iff opp_def eq_neg_iff_add_eq_0 mult2)
    apply (insert ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹x1 ≠ x2›)
    apply (simp add: eq_diff0)
    done
qed

lemma compat_add_triple:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b add_closed [OF a b 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 p ‹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
  with ‹on_curve a b (add a p p)› ‹on_curve a b p›
  have "add a p p = p" by (simp add: opp_opp)
  with uniq_zero [OF a b 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)
  with opp_closed [OF p]
  have  "x2 ∈ carrier R" "y2 ∈ carrier R"
    by (simp_all add: on_curve_def)
  from ‹opp p = Point x2 y2› p
  have "p = Point x2 (⊖ y2)"
    by (auto simp add: opp_def on_curve_def neg_equal_swap split: point.split_asm)
  with ‹add a p p = Point x1 y1› [symmetric]
  obtain l' where l':
    "l' = («3» ⊗ x2 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ ⊖ y2)"
    and xy: "x1 = l' [^] (2::nat) ⊖ «2» ⊗ x2"
    "y1 = ⊖ (⊖ y2) ⊖ l' ⊗ (x1 ⊖ x2)"
    and y2: "⊖ y2 ≠ ⊖ (⊖ y2)"
    by (simp add: add_def Let_def split: if_split_asm)
  from l' ‹x2 ∈ carrier R› ‹y2 ∈ carrier R› a y2
  have "l' ∈ carrier R" by (simp add: neg_equal_zero neg_equal_swap integral_iff)
  have "x3 = x2"
    apply (simp add: xy
      ‹l = (y2 ⊖ y1) ⊘ (x2 ⊖ x1)› ‹x3 = l [^] 2 ⊖ x1 ⊖ x2›)
    apply field
    apply (insert ‹x1 ≠ x2› ‹x2 ∈ carrier R› ‹l' ∈ carrier R›)
    apply (simp add: xy eq_diff0)
    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 a b add_closed [OF a b 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 a b ab add_closed [OF a b 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 a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b 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 a b ‹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 "x1 ∈ carrier R" "y1 ∈ carrier R"
      and y1: "y1 [^] (2::nat) = x1 [^] (3::nat) ⊕ a ⊗ x1 ⊕ b"
      by (simp_all add: on_curve_def)
    from ‹on_curve a b p2› ‹p2 = Point x2 y2›
    have "x2 ∈ carrier R" "y2 ∈ carrier R"
      and y2: "y2 [^] (2::nat) = x2 [^] (3::nat) ⊕ a ⊗ x2 ⊕ b"
      by (simp_all add: on_curve_def)
    from ‹p1 = Point x1 y1› ‹p1 ≠ opp p1› ‹y1 ∈ carrier R›
    have "y1 ≠ 𝟬"
      by (simp add: opp_Point integral_iff equal_neg_zero)
    from Gen have "x1 = ((y2 ⊖ y1) ⊘ (x2 ⊖ x1)) [^] (2::nat) ⊖ x1 ⊖ x2"
      by (simp add: opp_Point)
    then have "«2» ⊗ y2 ⊗ y1 = a ⊗ x2 ⊕ «3» ⊗ x2 ⊗ x1 [^] (2::nat) ⊕ a ⊗ x1 ⊖
      x1 [^] (3::nat) ⊕ «2» ⊗ b"
      apply (field (prems) y1 y2)
      apply (field y1 y2)
      apply simp
      apply (insert ‹x1 ≠ x2› ‹x1 ∈ carrier R› ‹x2 ∈ carrier R›)
      apply (simp add: eq_diff0)
      done
    then have "(x2 ⊖ (((«3» ⊗ x1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ (⊖ y1))) [^] (2::nat) ⊖
      «2» ⊗ x1)) ⊗ (x2 ⊖ x1) [^] (2::nat) = 𝟬"
      apply (drule_tac f="λx. x [^] (2::nat)" in arg_cong)
      apply (field (prems) y1 y2)
      apply (field y1 y2)
      apply (insert ‹y1 ≠ 𝟬› ‹y1 ∈ carrier R›)
      apply (simp_all add: integral_iff neg_equal_swap)
      done
    with a ‹x1 ∈ carrier R› ‹y1 ∈ carrier R› ‹x2 ∈ carrier R›
      ‹y1 ≠ 𝟬› ‹x1 ≠ x2›
    have "x2 = ((«3» ⊗ x1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ (⊖ y1))) [^] (2::nat) ⊖
      «2» ⊗ x1"
      by (simp add: integral_iff eq_diff0 neg_equal_swap)
    with ‹p2 = Point x2 y2› _ ‹on_curve a b p2›
      add_closed [OF a b
        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 (insert ‹y1 ∈ carrier R› ‹y1 ≠ 𝟬›)
      apply (simp add: add_def opp_Point neg_equal_zero Let_def ‹p1 = Point x1 y1›)
      done
    then show ?case
    proof
      assume "p2 = opp (add a (opp p1) (opp p1))"
      with a b ‹on_curve a b p1›
      have "p2 = add a p1 p1"
        by (simp add: opp_add opp_opp opp_closed)
      show ?case
      proof (cases "add a p1 p1 = opp p1")
        case True
        from a b ‹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 a b ‹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 add_closed opp_closed opp_opp add_comm)
        with a b 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 a b ‹on_curve a b p1› ‹on_curve a b p2›
        have "p2 = opp p2" using ‹p1 ≠ opp p1›
          by (rule compat_add_opp)
        with a b ‹on_curve a b p1› ‹p2 = add a p1 p1›
        show ?thesis by (simp add: opp_add)
      qed
    qed
  qed
qed

lemma cancel:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b p3 have "add a p3 p = p" by (simp add: add_comm)
  with a b ab p3 ‹on_curve a b p›
  show ?case by (rule uniq_zero [symmetric])
next
  case (Opp p)
  from p3 ‹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› ‹p1 = Point x1 y1›
  have "x1 ∈ carrier R" "y1 ∈ carrier R"
    by (simp_all add: on_curve_def)
  from ‹on_curve a b p2› ‹p2 = Point x2 y2›
  have "x2 ∈ carrier R" "y2 ∈ carrier R"
    by (simp_all add: on_curve_def)
  from add_closed [OF a b ‹on_curve a b p1› ‹on_curve a b p2›]
    ‹p4 = add a p1 p2› [symmetric] ‹p4 = Point x4 y4›
  have "x4 ∈ carrier R" "y4 ∈ carrier R"
    by (simp_all add: on_curve_def)
  from ‹_ ∨ _› a ‹p1 ≠ opp p2› ‹p1 = Point x1 y1› ‹p2 = Point x2 y2›
    ‹x1 ∈ carrier R› ‹y1 ∈ carrier R›
    ‹x2 ∈ carrier R› ‹y2 ∈ carrier R›
  have "l ∈ carrier R"
    by (auto simp add: opp_Point equal_neg_zero integral_iff eq_diff0)
  from a b ‹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 a b ‹on_curve a b p2›
    have "add a p2 p = p" by (simp add: add_comm)
    with a b 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
    with ‹on_curve a b p2› show ?case by (rule uniq_opp)
  next
    case (Gen p1 x1' y1' p3 x3 y3 p5 x5 y5 l')
    from ‹on_curve a b p3› ‹p3 = Point x3 y3›
    have "x3 ∈ carrier R" "y3 ∈ carrier R"
      by (simp_all add: on_curve_def)
    from ‹x1' = x3 ∧ _ ∨ _› a ‹p1 ≠ opp p3›
      ‹p1 = Point x1 y1› ‹p1 = Point x1' y1'› ‹p3 = Point x3 y3›
      ‹x1 ∈ carrier R› ‹y1 ∈ carrier R›
      ‹x3 ∈ carrier R› ‹y3 ∈ carrier R›
    have "l' ∈ carrier R"
      by (auto simp add: opp_Point equal_neg_zero integral_iff eq_diff0)
    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')›
      ‹x1 ∈ carrier R› ‹y1 ∈ carrier R› ‹x4 ∈ carrier R› ‹l' ∈ carrier R›
    have "𝟬 = ⊖ y1 ⊖ l ⊗ (x4 ⊖ x1) ⊖ (⊖ y1 ⊖ l' ⊗ (x4 ⊖ x1))"
      by (auto simp add: trans [OF eq_commute eq_diff0])
    with ‹x1 ∈ carrier R› ‹y1 ∈ carrier R› ‹x4 ∈ carrier R›
      ‹l ∈ carrier R› ‹l' ∈ carrier R›
    have "(l' ⊖ l) ⊗ (x4 ⊖ x1) = 𝟬"
      apply simp
      apply (rule eq_diff0 [THEN iffD1])
      apply simp
      apply simp
      apply ring
      done
    with ‹x1 ∈ carrier R› ‹x4 ∈ carrier R› ‹l ∈ carrier R› ‹l' ∈ carrier R›
    have "l' = l ∨ x4 = x1"
      by (simp add: integral_iff eq_diff0)
    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›
        ‹x1 ∈ carrier R› ‹x3 ∈ carrier R› ‹l ∈ carrier R›
      have "𝟬 = l [^] (2::nat) ⊖ x1 ⊖ x2 ⊖ (l [^] (2::nat) ⊖ x1 ⊖ x3)"
        by (simp add: trans [OF eq_commute eq_diff0])
      with ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹x3 ∈ carrier R› ‹l ∈ carrier R›
      have "x2 = x3"
        apply (rule_tac eq_diff0 [THEN iffD1, THEN sym])
        apply simp_all
        apply (rule eq_diff0 [THEN iffD1])
        apply simp_all[2]
        apply ring
        done
      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 (rule eq_diff0 [THEN iffD1])
            apply (insert ‹x1 ≠ x2› ‹x1 ∈ carrier R› ‹y1 ∈ carrier R›
              ‹x2 ∈ carrier R› ‹y2 ∈ carrier R› ‹y3 ∈ carrier R›)
            apply simp_all
            apply (erule subst)
            apply (rule eq_diff0 [THEN iffD1])
            apply simp_all
            apply ring
            apply (simp add: eq_diff0)
            done
          with ‹p2 = opp p3› ‹p2 = Point x2 y2› ‹p3 = Point x3 y3›
          show ?thesis by (simp add: opp_Point)
        next
          case False
          with a b ‹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 a b ‹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 a b ‹on_curve a b p1› ‹on_curve a b p2›
        have "add a p2 p1 = p1" by (simp add: add_comm)
        with a b 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›
          a b ‹on_curve a b p1› ‹on_curve a b p3›
        have "add a p3 p1 = p1" by (simp add: add_comm)
        with a b 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 a b 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 a b 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 a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b p1 p2 True have "add a p2 p1 = opp p2"
    by (simp add: add_comm)
  with a b 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 a b 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 a b ab ‹on_curve a b p1›
    moreover from ‹on_curve a b p1› ‹p1 = Point x1 y1›
    have "y1 ∈ carrier R" by (simp add: on_curve_def)
    with ‹y1 ≠ 𝟬› ‹p1 = Point x1 y1›
    have "p1 ≠ opp p1" by (simp add: opp_Point equal_neg_zero)
    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 a b
      add_closed [OF a b ‹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 ‹on_curve a b 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 ‹on_curve a b p› ‹p = add a p1 (opp (opp p))›
      have "add a p1 p = p" by (simp add: opp_opp)
      with a b 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 p1› ‹p1 = Point x1 y1›
      have "x1 ∈ carrier R" "y1 ∈ carrier R"
        by (simp_all add: on_curve_def)
      from ‹on_curve a b p2› ‹p2 = Point x2 y2›
      have "x2 ∈ carrier R" "y2 ∈ carrier R"
        by (simp_all add: on_curve_def)
      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: eq_diff0 [OF ‹x2 ∈ carrier R› ‹x1 ∈ carrier R›]
          ‹x1 ≠ x2› [THEN not_sym])
        apply field
        apply (rule conjI)
        apply (simp add: eq_diff0 [OF ‹x2 ∈ carrier R› ‹x1 ∈ carrier R›]
          ‹x1 ≠ x2› [THEN not_sym])
        apply (rule notI)
        apply (erule notE)
        apply (ring (prems))
        apply (rule sym)
        apply field
        apply (simp add: eq_diff0 [OF ‹x2 ∈ carrier R› ‹x1 ∈ carrier R›]
          ‹x1 ≠ x2› [THEN not_sym])
        done
    qed
  qed
qed

lemma add_shift_minus:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b p1 p2 p3
    by (simp add: add_comm add_closed opp_closed)
  with a b ab p2 p1 add_closed [OF a b p3 opp_closed [OF p2]]
  show ?thesis by (rule cancel)
qed

lemma degen_assoc:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b p2 p3
  have "add a (opp p2) (add a p2 p3) = add a (add a p3 p2) (opp p2)"
    by (simp add: add_comm add_closed opp_closed)
  also from a b 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 a b p2 have "… = add a (add a (opp p2) p2) p3"
    by (simp add: add_comm opp_closed)
  finally show ?thesis using ‹p1 = opp p2› by simp
next
  assume "p2 = opp p3"
  from a b p3
  have "add a p1 (add a (opp p3) p3) = add a p1 (add a p3 (opp p3))"
    by (simp add: add_comm opp_closed)
  also from a b 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 a b p3 have "… = add a (opp p3) p3"
    by (simp add: add_comm opp_closed)
  also from a b 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 a b p2 p3
  have "… = add a (add a (add a (opp p2) (opp p3)) p2) p3"
    by (simp add: add_comm opp_opp opp_closed)
  finally show ?thesis
    using opp_add [OF a b p2 p3] eq [symmetric] p1
    by (simp add: opp_opp)
next
  assume eq: "opp p3 = add a p1 p2"
  from opp_add [OF a b 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 a b p1 p2
  have "… = add a p1 (add a (add a (opp p1) (opp p2)) (opp (opp p2)))"
    by (simp add: add_comm opp_opp add_closed opp_closed)
  also from a b 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 a b p3 have "… = add a (opp p3) p3"
    by (simp add: add_comm opp_closed)
  finally show ?thesis using eq [symmetric] by simp
qed

lemma spec4_assoc:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b 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 a b 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 a b 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 a b 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 a b 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 a b 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 [OF a b])
                apply (simp_all add: is_generic_def is_tangent_def)
                apply (rule notI)
                apply (drule uniq_zero [OF a b ab p2 p2])
                apply simp
                apply (intro conjI notI)
                apply (erule notE)
                apply (rule uniq_opp [of a b])
                apply (simp_all add: add_comm add_closed)[2]
                apply (erule notE)
                apply (drule uniq_zero [OF a b ab add_closed [OF a b p2 p2] p2])
                apply simp
                done
            next
              case False
              show ?thesis
              proof (cases "p2 = add a p1 p2")
                case True
                from a b 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 a b p2 show ?thesis
                    by (simp add: add_comm add_closed)
                next
                  case False
                  with a b 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 [OF a b])
                    apply (simp_all add: is_generic_def is_tangent_def)
                    apply (rule notI)
                    apply (erule notE [of "p1 = opp p2"])
                    apply (rule uniq_opp)
                    apply assumption
                    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 [OF add_closed [OF a b p2 p2]])
                    done
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma add_assoc:
  assumes a: "a ∈ carrier R"
  and b: "b ∈ carrier R"
  and 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 a b 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 a b 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 a b 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 a b p2 p3
        have "add a p2 (add a p2 p3) = add a (add a p3 p2) p2"
          by (simp add: add_comm add_closed)
        also from a b ab p3 p2 have "… = add a p3 (add a p2 p2)"
          by (simp add: spec4_assoc)
        also from a b p2 p3
        have "… = add a (add a p2 p2) p3"
          by (simp add: add_comm add_closed)
        finally show ?thesis using True by simp
      next
        case False
        show ?thesis
        proof (cases "p1 = opp p2")
          case True
          from a b 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 a b ab p1 p3 show ?thesis
              by (simp add: spec4_assoc)
          next
            case False
            show ?thesis
            proof (cases "p2 = opp p3")
              case True
              from a b 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 a b 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 a b 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 a b ab p2 p3 show ?thesis
                      apply simp
                      apply (rule cancel [OF a b 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 add_closed)
                      done
                  next
                    case False
                    show ?thesis
                    proof (cases "p3 = add a p1 p2")
                      case True
                      with a b ab p1 p2 show ?thesis
                        apply simp
                        apply (rule cancel [OF a b 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 a b 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)
                        apply assumption
                        apply (simp add: add_comm)
                        apply (intro conjI notI)
                        apply (erule notE [of "p2 = opp p3"])
                        apply (rule uniq_opp)
                        apply assumption
                        apply (simp add: add_comm)
                        apply (rule notE [OF ‹opp p1 ≠ add a p2 p3›])
                        apply (simp add: opp_opp [OF add_closed [OF a b p2 p3]])
                        done
                    qed
                  qed
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed
  
lemma add_comm':
  "a ∈ carrier R ⟹ b ∈ carrier R ⟹ 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 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: "a ∈ carrier R ⟹ b ∈ carrier R ⟹
  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:
  "a ∈ carrier R ⟹ b ∈ carrier R ⟹ 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:
  "a ∈ carrier R ⟹ b ∈ carrier R ⟹ 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)

end

subsection ‹Projective Coordinates›

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

definition (in cring) pdouble :: "'a ⇒ 'a ppoint ⇒ 'a ppoint" where
  "pdouble a p =
     (let (x, y, z) = p
      in
        if z = 𝟬 then p
        else
          let
            l = «2» ⊗ y ⊗ z;
            m = «3» ⊗ x [^] (2::nat) ⊕ a ⊗ z [^] (2::nat)
          in
            (l ⊗ (m [^] (2::nat) ⊖ «4» ⊗ x ⊗ y ⊗ l),
             m ⊗ («6» ⊗ x ⊗ y ⊗ l ⊖ m [^] (2::nat)) ⊖
             «2» ⊗ y [^] (2::nat) ⊗ l [^] (2::nat),
             l [^] (3::nat)))"

definition (in cring) 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 = 𝟬 then p2
        else if z2 = 𝟬 then p1
        else
          let
            d1 = x2 ⊗ z1;
            d2 = x1 ⊗ z2;
            l = d1 ⊖ d2;
            m = y2 ⊗ z1 ⊖ y1 ⊗ z2
          in
            if l = 𝟬 then
              if m = 𝟬 then pdouble a p1
              else (𝟬, 𝟬, 𝟬)
            else
              let h = m [^] (2::nat) ⊗ z1 ⊗ z2 ⊖ (d1 ⊕ d2) ⊗ l [^] (2::nat)
              in
                (l ⊗ h,
                 (d2 ⊗ l [^] (2::nat) ⊖ h) ⊗ m ⊖ l [^] (3::nat) ⊗ y1 ⊗ z2,
                 l [^] (3::nat) ⊗ z1 ⊗ z2))"

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

definition (in cring) in_carrierp :: "'a ppoint ⇒ bool" where
  "in_carrierp = (λ(x, y, z). x ∈ carrier R ∧ y ∈ carrier R ∧ z ∈ carrier R)"

definition (in cring) on_curvep :: "'a ⇒ 'a ⇒ 'a ppoint ⇒ bool" where
  "on_curvep a b = (λ(x, y, z).
     x ∈ carrier R ∧ y ∈ carrier R ∧ z ∈ carrier R ∧
     (z ≠ 𝟬 ⟶
      y [^] (2::nat) ⊗ z = x [^] (3::nat) ⊕ a ⊗ x ⊗ z [^] (2::nat) ⊕ b ⊗ z [^] (3::nat)))"

lemma (in cring) on_curvep_infinity [simp]: "on_curvep a b (x, y, 𝟬) = (x ∈ carrier R ∧ y ∈ carrier R)"
  by (simp add: on_curvep_def)

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

lemma (in cring) on_curvep_imp_in_carrierp [simp]: "on_curvep a b p ⟹ in_carrierp p"
  by (auto simp add: on_curvep_def in_carrierp_def)

lemma (in ell_field) on_curvep_iff_on_curve:
  assumes "a ∈ carrier R" "b ∈ carrier R" "in_carrierp p"
  shows "on_curvep a b p = on_curve a b (make_affine p)"
  using assms
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 carrier: "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
      and yz: "z ≠ 𝟬 ⟹
        y [^] (2::nat) ⊗ z = x [^] (3::nat) ⊕ a ⊗ x ⊗ z [^] (2::nat) ⊕ b ⊗ z [^] (3::nat)"
      by (simp_all add: on_curvep_def)
    show "on_curve a b (make_affine (x, y, z))"
    proof (cases "z = 𝟬")
      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 carrier)
        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 = 𝟬")
      case True
      with ‹in_carrierp (x, y, z)› show ?thesis
        by (simp add: on_curvep_def in_carrierp_def)
    next
      case False
      from ‹in_carrierp (x, y, z)›
      have carrier: "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
        by (simp_all add: in_carrierp_def)
      from H show ?thesis
        apply (simp add: on_curve_def on_curvep_def make_affine_def carrier False)
        apply (field (prems))
        apply field
        apply (simp_all add: False)
        done
    qed
  qed
qed

lemma (in cring) pdouble_in_carrierp:
  "a ∈ carrier R ⟹ in_carrierp p ⟹ in_carrierp (pdouble a p)"
  by (auto simp add: in_carrierp_def pdouble_def Let_def split: prod.split)

lemma (in cring) padd_in_carrierp:
  "a ∈ carrier R ⟹ in_carrierp p1 ⟹ in_carrierp p2 ⟹ in_carrierp (padd a p1 p2)"
  by (auto simp add: padd_def Let_def pdouble_in_carrierp split: prod.split)
    (auto simp add: in_carrierp_def)

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

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

lemma (in ell_field) pdouble_correct:
  "a ∈ carrier R ⟹ in_carrierp p ⟹
   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 have "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
    by (simp_all add: in_carrierp_def)
  then show ?case
    apply (auto simp add: add_def pdouble_def make_affine_def equal_neg_zero divide_eq_0_iff
      integral_iff Let_def simp del: minus_divide_left)
    apply field
    apply (simp add: integral_iff)
    apply field
    apply (simp add: integral_iff)
    done
qed

lemma (in ell_field) padd_correct:
  assumes a: "a ∈ carrier R" and b: "b ∈ carrier R"
  and 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 "x2 ∈ carrier R" "y2 ∈ carrier R" "z2 ∈ carrier R" and
      yz2: "z2 ≠ 𝟬 ⟹ y2 [^] (2::nat) ⊗ z2 ⊗ z1 [^] (3::nat) =
        (x2 [^] (3::nat) ⊕ a ⊗ x2 ⊗ z2 [^] (2::nat) ⊕ b ⊗ z2 [^] (3::nat)) ⊗ z1 [^] (3::nat)"
      by (simp_all add: on_curvep_def)
    from p1' have "x1 ∈ carrier R" "y1 ∈ carrier R" "z1 ∈ carrier R" and
      yz1: "z1 ≠ 𝟬 ⟹ y1 [^] (2::nat) ⊗ z1 ⊗ z2 [^] (3::nat) =
        (x1 [^] (3::nat) ⊕ a ⊗ x1 ⊗ z1 [^] (2::nat) ⊕ b ⊗ z1 [^] (3::nat)) ⊗ z2 [^] (3::nat)"
      by (simp_all add: on_curvep_def)
    show ?case
    proof (cases "z1 = 𝟬")
      case True
      then show ?thesis
        by (simp add: add_def padd_def make_affine_def)
    next
      case False
      show ?thesis
      proof (cases "z2 = 𝟬")
        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 = 𝟬")
          case True
          note x = this
          with ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹z1 ∈ carrier R› ‹ z2 ∈ carrier R›
          have x': "x2 ⊗ z1 = x1 ⊗ z2" by (simp add: eq_diff0)
          show ?thesis
          proof (cases "y2 ⊗ z1 ⊖ y1 ⊗ z2 = 𝟬")
            case True
            with ‹y1 ∈ carrier R› ‹y2 ∈ carrier R› ‹z1 ∈ carrier R› ‹ z2 ∈ carrier R›
            have y: "y2 ⊗ z1 = y1 ⊗ z2" by (simp add: eq_diff0)
            from ‹z1 ≠ 𝟬› ‹z2 ≠ 𝟬› 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 ≠ 𝟬› ‹z2 ≠ 𝟬› p1' fields a show ?thesis
              by (simp add: padd_def pdouble_correct)
          next
            case False
            have "y2 [^] (2::nat) ⊗ z1 [^] (3::nat) ⊗ z2 =
              y1 [^] (2::nat) ⊗ z1 ⊗ z2 [^] (3::nat)"
              by (ring yz1 [OF ‹z1 ≠ 𝟬›] yz2 [OF ‹z2 ≠ 𝟬›] x')
            then have "y2 [^] (2::nat) ⊗ z1 [^] (3::nat) ⊗ z2 ⊘ z1 ⊘ z2 =
              y1 [^] (2::nat) ⊗ z1 ⊗ z2 [^] (3::nat) ⊘ 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 ≠ 𝟬› ‹z2 ≠ 𝟬›)
              done
            with False
            have y2z1: "y2 ⊗ z1 = ⊖ (y1 ⊗ z2)"
              by (simp add: square_eq_iff eq_diff0
                ‹y1 ∈ carrier R› ‹y2 ∈ carrier R› ‹z1 ∈ carrier R› ‹z2 ∈ carrier R›)
            from x False ‹z1 ≠ 𝟬› ‹z2 ≠ 𝟬› 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 ≠ 𝟬› ‹z2 ≠ 𝟬›)
            done
          with False ‹z1 ≠ 𝟬› ‹z2 ≠ 𝟬›
            ‹x1 ∈ carrier R› ‹x2 ∈ carrier R› ‹z1 ∈ carrier R› ‹z2 ∈ carrier R›
          show ?thesis
            apply (auto simp add: padd_def add_def make_affine_def Let_def integral_iff)
            apply field
            apply (simp add: integral_iff)
            apply field
            apply (simp add: integral_iff)
            done
        qed
      qed
    qed
  qed
qed

lemma (in ell_field) pdouble_closed:
  assumes "a ∈ carrier R" "b ∈ carrier R" "on_curvep a b p"
  shows "on_curvep a b (pdouble a p)"
proof -
  from ‹on_curvep a b p› have "in_carrierp p" by simp
  from assms show ?thesis
    by (simp add: on_curvep_iff_on_curve pdouble_in_carrierp pdouble_correct
      add_closed ‹in_carrierp p›)
qed

lemma (in ell_field) padd_closed:
  assumes "a ∈ carrier R" "b ∈ carrier R" "on_curvep a b p1" "on_curvep a b p2"
  shows "on_curvep a b (padd a p1 p2)"
proof -
  from ‹on_curvep a b p1› have "in_carrierp p1" by simp
  from ‹on_curvep a b p2› have "in_carrierp p2" by simp
  from assms show ?thesis
    by (simp add: on_curvep_iff_on_curve padd_in_carrierp padd_correct
      add_closed ‹in_carrierp p1› ‹in_carrierp p2›)
qed

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

lemma (in ell_field) ppoint_mult_closed [simp]:
  "a ∈ carrier R ⟹ b ∈ carrier R ⟹ on_curvep a b p ⟹ on_curvep a b (ppoint_mult a n p)"
  by (induct n) (simp_all add: padd_closed)

lemma (in ell_field) ppoint_mult_correct: "a ∈ carrier R ⟹ b ∈ carrier R ⟹ 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)

definition (in cring) proj_eq :: "'a ppoint ⇒ 'a ppoint ⇒ bool" where
  "proj_eq = (λ(x1, y1, z1) (x2, y2, z2).
     (z1 = 𝟬) = (z2 = 𝟬) ∧ x1 ⊗ z2 = x2 ⊗ z1 ∧ y1 ⊗ z2 = y2 ⊗ z1)"

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

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

lemma (in domain) 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 carrier:
        "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
        "x' ∈ carrier R" "y' ∈ carrier R" "z' ∈ carrier R"
        "x'' ∈ carrier R" "y'' ∈ carrier R" "z'' ∈ carrier R"
        and z: "(z = 𝟬) = (z' = 𝟬)" "(z' = 𝟬) = (z'' = 𝟬)" 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: in_carrierp_def 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 carrier conc)
    qed
  qed
qed

lemma (in field) make_affine_proj_eq_iff:
  "in_carrierp p ⟹ in_carrierp p' ⟹ 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')
    then have carrier:
      "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
      "x' ∈ carrier R" "y' ∈ carrier R" "z' ∈ carrier R"
      by (simp_all add: in_carrierp_def)
    show ?case
    proof
      assume "proj_eq (x, y, z) (x', y', z')"
      then have "(z = 𝟬) = (z' = 𝟬)"
        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 = 𝟬")
        case True
        with H have "z' = 𝟬" by (simp add: make_affine_def split: if_split_asm)
        with True carrier show ?thesis by (simp add: proj_eq_def)
      next
        case False
        with H have "z' ≠ 𝟬" "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 ≠ 𝟬› ‹z' ≠ 𝟬›)
          done
        moreover from ‹y ⊘ z = y' ⊘ z'›
        have "y ⊗ z' = y' ⊗ z"
          apply (field (prems))
          apply field
          apply (simp_all add: ‹z ≠ 𝟬› ‹z' ≠ 𝟬›)
          done
        ultimately show ?thesis
          by (simp add: proj_eq_def ‹z ≠ 𝟬› ‹z' ≠ 𝟬›)
      qed
    qed
  qed
qed

lemma (in ell_field) pdouble_proj_eq_cong:
  "a ∈ carrier R ⟹ in_carrierp p ⟹ in_carrierp p' ⟹ proj_eq p p' ⟹
   proj_eq (pdouble a p) (pdouble a p')"
  by (simp add: make_affine_proj_eq_iff pdouble_in_carrierp pdouble_correct)

lemma (in ell_field) padd_proj_eq_cong:
  "a ∈ carrier R ⟹ b ∈ carrier R ⟹ 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_in_carrierp padd_correct)

end