Session Elliptic_Curves_Group_Law

Theory Elliptic_Axclass

section ‹Formalization using Axiomatic Type Classes›

theory Elliptic_Axclass
imports "HOL-Decision_Procs.Reflective_Field"
begin

subsection ‹Affine Coordinates›

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

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

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

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

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

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

end

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemmas [simp] = minus2_not0 [simplified]

declare two_not_zero [simplified, simp add]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Projective Coordinates›

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

context ell_field begin

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

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

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

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

end

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

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

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

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

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

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

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

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

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

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

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

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

context ell_field begin

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

end

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

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

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

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

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

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

end

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)"