Theory Elliptic_Curves_Group_Law.Elliptic_Locale

section ‹Formalization using Locales›

theory Elliptic_Locale
imports "HOL-Decision_Procs.Reflective_Field"
begin

subsection ‹Affine Coordinates›

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

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

declare two_not_zero [simplified, simp add]

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

lemmas equal_neg_zero = trans [OF eq_commute neg_equal_zero]

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

definition on_curve :: "'a  'a  'a point  bool" where
  "on_curve a b p = (case p of
       Infinity  True
     | Point x y  x  carrier R  y  carrier R 
         y [^] (2::nat) = x [^] (3::nat)  a  x  b)"

definition add :: "'a  'a point  'a point  'a point" where
  "add a p1 p2 = (case p1 of
       Infinity  p2
     | Point x1 y1  (case p2 of
         Infinity  p1
       | Point x2 y2 
           if x1 = x2 then
             if y1 =  y2 then Infinity
             else
               let
                 l = («3»  x1 [^] (2::nat)  a)  («2»  y1);
                 x3 = l [^] (2::nat)  «2»  x1
               in
                 Point x3 ( y1  l  (x3  x1))
           else
             let
               l = (y2  y1)  (x2  x1);
               x3 = l [^] (2::nat)  x1  x2
             in
               Point x3 ( y1  l  (x3  x1))))"

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

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

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

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

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

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

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

lemma add_closed:
  assumes "a  carrier R" and "b  carrier R"
  and "on_curve a b p1" and "on_curve a b p2"
  shows "on_curve a b (add a p1 p2)"
proof (cases p1)
  case (Point x1 y1)
  note Point' = this
  show ?thesis
  proof (cases p2)
    case (Point x2 y2)
    show ?thesis
    proof (cases "x1 = x2")
      case True
      note True' = this
      show ?thesis
      proof (cases "y1 =  y2")
        case True
        with True' Point Point'
        show ?thesis
          by (simp add: on_curve_def add_def)
      next
        case False
        from on_curve a b p1 Point' True'
        have "x2  carrier R" "y1  carrier R" and
          on_curve1: "y1 [^] (2::nat) = x2 [^] (3::nat)  a  x2  b"
          by (simp_all add: on_curve_def)
        from False True' Point Point' assms
        have "y1  𝟬"
          apply (auto simp add: on_curve_def nat_pow_zero)
          apply (drule sym [of 𝟬])
          apply simp
          done
        with False True' Point Point' assms
        show ?thesis
          apply (simp add: on_curve_def add_def Let_def integral_iff)
          apply (field on_curve1)
          apply (simp add: integral_iff)
          done
      qed
    next
      case False
      from on_curve a b p1 Point'
      have  "x1  carrier R" "y1  carrier R"
        and on_curve1: "y1 [^] (2::nat) = x1 [^] (3::nat)  a  x1  b"
        by (simp_all add: on_curve_def)
      from on_curve a b p2 Point
      have "x2  carrier R" "y2  carrier R"
        and on_curve2: "y2 [^] (2::nat) = x2 [^] (3::nat)  a  x2  b"
        by (simp_all add: on_curve_def)
      from assms not_sym [OF False] show ?thesis
        apply (simp add: on_curve_def add_def Let_def False Point Point' eq_diff0)
        apply (field on_curve1 on_curve2)
        apply (simp add: eq_diff0)
        done
    qed
  next
    case Infinity
    with Point on_curve a b p1 show ?thesis
      by (simp add: add_def)
  qed
next
  case Infinity
  with on_curve a b p2 show ?thesis
    by (simp add: add_def)
qed

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

lemma add_casew [consumes 4, case_names InfL InfR Opp Gen]:
  assumes a: "a  carrier R"
  and b: "b  carrier R"
  and p: "on_curve a b p"
  and q: "on_curve a b q"
  and R1: "p. P Infinity p p"
  and R2: "p. P p Infinity p"
  and R3: "p. on_curve a b p  P p (opp p) Infinity"
  and R4: "p1 x1 y1 p2 x2 y2 p3 x3 y3 l.
    p1 = Point x1 y1  p2 = Point x2 y2  p3 = Point x3 y3 
    p3 = add a p1 p2  p1  opp p2 
    x1 = x2  y1 = y2  l = («3»  x1 [^] (2::nat)  a)  («2»  y1) 
    x1  x2  l = (y2  y1)  (x2  x1) 
    x3 = l [^] (2::nat)  x1  x2 
    y3 =  y1  l  (x3  x1) 
    P p1 p2 p3"
  shows "P p q (add a p q)"
  using a b p q p q
proof (induct rule: add_case)
  case InfL
  show ?case by (rule R1)
next
  case InfR
  show ?case by (rule R2)
next
  case (Opp p)
  from on_curve a b p show ?case by (rule R3)
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  with a b show ?case
    apply (rule_tac R4)
    apply assumption+
    apply (simp add: opp_Point equal_neg_zero on_curve_def)
    apply simp
    apply (simp add: minus_eq mult2 integral_iff a_assoc r_minus on_curve_def)
    apply simp
    done
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then show ?case
    apply (rule_tac R4)
    apply assumption+
    apply (simp add: opp_Point)
    apply simp_all
    done
qed

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

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

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

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

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

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

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

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

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

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

lemma uniq_zero:
  assumes a: "a  carrier R"
  and b: "b  carrier R"
  and ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and add: "add a p1 p2 = p2"
  shows "p1 = Infinity"
  using a b p1 p2 assms
proof (induct rule: add_case)
  case InfL
  show ?case ..
next
  case InfR
  then show ?case by simp
next
  case Opp
  then show ?case by (simp add: opp_def split: point.split_asm)
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  from on_curve a b p1 p1 = Point x1 y1
  have "x1  carrier R" "y1  carrier R" by (simp_all add: on_curve_def)
  with a l = («3»  x1 [^] 2  a)  («2»  y1) y1  𝟬
  have "l  carrier R" by (simp add: integral_iff)
  from p1 = Point x1 y1 p2 = Point x2 y2 p2 = p1
  have "x2 = x1" "y2 = y1" by simp_all
  with x1  carrier R y1  carrier R l  carrier R y2 =  y1  l  (x2  x1) y1  𝟬
  have " y1 = y1" by (simp add: r_neg minus_eq)
  with y1  carrier R y1  𝟬
  show ?case by (simp add: neg_equal_zero)
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then have "x1  carrier R" "y1  carrier R" "x2  carrier R" "y2  carrier R"
    and y1: "y1 [^] (2::nat) = x1 [^] (3::nat)  a  x1  b"
    and y2: "y2 [^] (2::nat) = x2 [^] (3::nat)  a  x2  b"
    by (simp_all add: on_curve_def)
  with l = (y2  y1)  (x2  x1) x1  x2
  have "l  carrier R" by (simp add: eq_diff0)
  from p3 = p2 p2 = Point x2 y2 p3 = Point x3 y3
  have ps: "x3 = x2" "y3 = y2" by simp_all
  with y3 =  y1  l  (x3  x1)
  have "y2 =  y1  l  (x2  x1)" by simp
  also from l = (y2  y1)  (x2  x1) x1  x2
    x1  carrier R x2  carrier R y1  carrier R y2  carrier R
  have "l  (x2  x1) = y2  y1"
    by (simp add: m_div_def m_assoc eq_diff0)
  also from y1  carrier R y2  carrier R
  have " y1  (y2  y1) = ( y1  y1)   y2"
    by (simp add: minus_eq minus_add a_ac)
  finally have "y2 = 𝟬" using y1  carrier R y2  carrier R
    by (simp add: l_neg equal_neg_zero)
  with p2 = Point x2 y2 on_curve a b p2
    a  carrier R b  carrier R x2  carrier R
  have x2: "x2 [^] (3::nat) =  (a  x2  b)"
    by (simp add: on_curve_def nat_pow_zero eq_neg_iff_add_eq_0 a_assoc)
  from x3 = l [^] 2  x1  x2 x3 = x2
  have "l [^] (2::nat)  x1  x2  x2 = x2  x2" by simp
  with x1  carrier R x2  carrier R l  carrier R
  have "l [^] (2::nat)  x1  «2»  x2 = 𝟬"
    by (simp add: of_int_2 l_distr minus_eq a_ac minus_add r_neg)
  then have "x2  (l [^] (2::nat)  x1  «2»  x2) = x2  𝟬" by simp
  then have "(x2  x1)  («2»  a  x2  «3»  b) = 𝟬"
    apply (simp add: l = (y2  y1)  (x2  x1) y2 = 𝟬)
    apply (field (prems) y1 x2)
    apply (ring y1 x2)
    apply (simp add: eq_diff0 x2  carrier R x1  carrier R not_sym [OF x1  x2])
    done
  with not_sym [OF x1  x2]
    x2  carrier R x1  carrier R a  carrier R b  carrier R
  have "«2»  a  x2  «3»  b = 𝟬"
    by (simp add: integral_iff eq_diff0)
  with a  carrier R b  carrier R x2  carrier R
  have "«2»  a  x2 =  («3»  b)"
    by (simp add: eq_neg_iff_add_eq_0)
  from y2 [symmetric] y2 = 𝟬 a  carrier R
  have " («2»  a) [^] (3::nat)  (x2 [^] (3::nat)  a  x2  b) = 𝟬"
    by (simp add: nat_pow_zero)
  then have "b  («4»  a [^] (3::nat)  «27»  b [^] (2::nat)) = 𝟬"
    apply (ring (prems) «2»  a  x2 =  («3»  b))
    apply (ring «2»  a  x2 =  («3»  b))
    done
  with ab a b have "b = 𝟬" by (simp add: nonsingular_def integral_iff)
  with «2»  a  x2  «3»  b = 𝟬 ab a b x2  carrier R
  have "x2 = 𝟬" by (simp add: nonsingular_def nat_pow_zero integral_iff)
  from l [^] (2::nat)  x1  «2»  x2 = 𝟬
  show ?case
    apply (simp add: x2 = 𝟬 y2 = 𝟬 l = (y2  y1)  (x2  x1))
    apply (field (prems) y1 b = 𝟬)
    apply (insert a b ab x1  carrier R b = 𝟬 x1  x2 x2 = 𝟬)
    apply (simp add: nonsingular_def nat_pow_zero integral_iff)
    apply (simp add: trans [OF eq_commute eq_neg_iff_add_eq_0])
    done
qed

lemma opp_add:
  assumes a: "a  carrier R"
  and b: "b  carrier R"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  shows "opp (add a p1 p2) = add a (opp p1) (opp p2)"
proof (cases p1)
  case Infinity
  then show ?thesis by (simp add: add_def opp_def)
next
  case (Point x1 y1)
  show ?thesis
  proof (cases p2)
    case Infinity
    with p1 = Point x1 y1 show ?thesis
      by (simp add: add_def opp_def)
  next
    case (Point x2 y2)
    with p1 = Point x1 y1 p1 p2
    have "x1  carrier R" "y1  carrier R" "x1 [^] (3::nat)  a  x1  b = y1 [^] (2::nat)"
      "x2  carrier R" "y2  carrier R" "x2 [^] (3::nat)  a  x2  b = y2 [^] (2::nat)"
      by (simp_all add: on_curve_def)
    with Point p1 = Point x1 y1 show ?thesis
      apply (cases "x1 = x2")
      apply (cases "y1 =  y2")
      apply (simp add: add_def opp_def Let_def)
      apply (simp add: add_def opp_def Let_def neg_equal_swap)
      apply (rule conjI)
      apply field
      apply (auto simp add: integral_iff nat_pow_zero
        trans [OF eq_commute eq_neg_iff_add_eq_0])[1]
      apply field
      apply (auto simp add: integral_iff nat_pow_zero
        trans [OF eq_commute eq_neg_iff_add_eq_0])[1]
      apply (simp add: add_def opp_def Let_def)
      apply (rule conjI)
      apply field
      apply (simp add: eq_diff0)
      apply field
      apply (simp add: eq_diff0)
      done
  qed
qed

lemma compat_add_opp:
  assumes a: "a  carrier R"
  and b: "b  carrier R"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and "add a p1 p2 = add a p1 (opp p2)"
  and "p1  opp p1"
  shows "p2 = opp p2"
  using a b p1 p2 assms
proof (induct rule: add_case)
  case InfL
  then show ?case by (simp add: add_0_l)
next
  case InfR
  then show ?case by (simp add: opp_def add_0_r)
next
  case (Opp p)
  then have "add a p p = Infinity" by (simp add: opp_opp)
  with on_curve a b p have "p = opp p" by (rule uniq_opp)
  with p  opp p show ?case ..
next
  case (Tan p1 x1 y1 p2 x2 y2 l)
  then have "add a p1 p1 = Infinity"
    by (simp add: add_opp)
  with on_curve a b p1 have "p1 = opp p1" by (rule uniq_opp)
  with p1  opp p1 show ?case ..
next
  case (Gen p1 x1 y1 p2 x2 y2 p3 x3 y3 l)
  then have "x1  carrier R" "y1  carrier R" "x2  carrier R" "y2  carrier R"
    by (simp_all add: on_curve_def)
  have "«2»  «2»  𝟬"
    by (simp add: integral_iff)
  then have "«4»  𝟬" by (simp add: of_int_mult [symmetric])
  from Gen have "(( y2  y1)  (x2  x1)) [^] (2::nat)  x1  x2 =
    ((y2  y1)  (x2  x1)) [^] (2::nat)  x1  x2"
    by (simp add: add_def opp_def Let_def)
  then show ?case
    apply (field (prems))
    apply (insert y1  carrier R y2  carrier R p1  opp p1
      p1 = Point x1 y1 p2 = Point x2 y2 «4»  𝟬)[1]
    apply (simp add: integral_iff opp_def eq_neg_iff_add_eq_0 mult2)
    apply (insert x1  carrier R x2  carrier R x1  x2)
    apply (simp add: eq_diff0)
    done
qed

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

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

lemma cancel:
  assumes a: "a  carrier R"
  and b: "b  carrier R"
  and ab: "nonsingular a b"
  and p1: "on_curve a b p1"
  and p2: "on_curve a b p2"
  and p3: "on_curve a b p3"
  and eq: "add a p1 p2 = add a p1 p3"
  shows "p2 = p3"
  using a b p1 p2 p1 p2 eq
proof (induct rule: add_casew)
  case InfL
  then show ?case by (simp add: add_0_l)
next
  case (InfR p)
  with a b p3 have "add a p3 p = p" by (simp add: add_comm)
  with a b ab p3 on_curve a b p
  show ?case by (rule uniq_zero [symmetric])
next
  case (Opp p)
  from p3 Infinity = add a p p3 [symmetric]
  show ?case by (rule uniq_opp [symmetric])
next
  case (Gen p1 x1 y1 p2 x2 y2 p4 x4 y4 l)
  from on_curve a b p1 p1 = Point x1 y1
  have "x1  carrier R" "y1  carrier R"
    by (simp_all add: on_curve_def)
  from on_curve a b p2 p2 = Point x2 y2
  have "x2  carrier R" "y2  carrier R"
    by (simp_all add: on_curve_def)
  from add_closed [OF a b on_curve a b p1 on_curve a b p2]
    p4 = add a p1 p2 [symmetric] p4 = Point x4 y4
  have "x4  carrier R" "y4  carrier R"
    by (simp_all add: on_curve_def)
  from _  _ a p1  opp p2 p1 = Point x1 y1 p2 = Point x2 y2
    x1  carrier R y1  carrier R
    x2  carrier R y2  carrier R
  have "l  carrier R"
    by (auto simp add: opp_Point equal_neg_zero integral_iff eq_diff0)
  from a b on_curve a b p1 p3 on_curve a b p1 p3 p1 = Point x1 y1
    p4 = add a p1 p2 p4 = add a p1 p3 p1  opp p2
  show ?case
  proof (induct rule: add_casew)
    case InfL
    then show ?case by (simp add: add_0_l)
  next
    case (InfR p)
    with a b on_curve a b p2
    have "add a p2 p = p" by (simp add: add_comm)
    with a b ab on_curve a b p2 on_curve a b p
    show ?case by (rule uniq_zero)
  next
    case (Opp p)
    then have "add a p p2 = Infinity" by simp
    with on_curve a b p2 show ?case by (rule uniq_opp)
  next
    case (Gen p1 x1' y1' p3 x3 y3 p5 x5 y5 l')
    from on_curve a b p3 p3 = Point x3 y3
    have "x3  carrier R" "y3  carrier R"
      by (simp_all add: on_curve_def)
    from x1' = x3  _  _ a p1  opp p3
      p1 = Point x1 y1 p1 = Point x1' y1' p3 = Point x3 y3
      x1  carrier R y1  carrier R
      x3  carrier R y3  carrier R
    have "l'  carrier R"
      by (auto simp add: opp_Point equal_neg_zero integral_iff eq_diff0)
    from p4 = p5 p4 = Point x4 y4 p5 = Point x5 y5
      p1 = Point x1' y1' p1 = Point x1 y1
      y4 =  y1  l  (x4  x1) y5 =  y1'  l'  (x5  x1')
      x1  carrier R y1  carrier R x4  carrier R l'  carrier R
    have "𝟬 =  y1  l  (x4  x1)  ( y1  l'  (x4  x1))"
      by (auto simp add: trans [OF eq_commute eq_diff0])
    with x1  carrier R y1  carrier R x4  carrier R
      l  carrier R l'  carrier R
    have "(l'  l)  (x4  x1) = 𝟬"
      apply simp
      apply (rule eq_diff0 [THEN iffD1])
      apply simp
      apply simp
      apply ring
      done
    with x1  carrier R x4  carrier R l  carrier R l'  carrier R
    have "l' = l  x4 = x1"
      by (simp add: integral_iff eq_diff0)
    then show ?case
    proof
      assume "l' = l"
      with p4 = p5 p4 = Point x4 y4 p5 = Point x5 y5
        p1 = Point x1' y1' p1 = Point x1 y1
        x4 = l [^] 2  x1  x2 x5 = l' [^] 2  x1'  x3
        x1  carrier R x3  carrier R l  carrier R
      have "𝟬 = l [^] (2::nat)  x1  x2  (l [^] (2::nat)  x1  x3)"
        by (simp add: trans [OF eq_commute eq_diff0])
      with x1  carrier R x2  carrier R x3  carrier R l  carrier R
      have "x2 = x3"
        apply (rule_tac eq_diff0 [THEN iffD1, THEN sym])
        apply simp_all
        apply (rule eq_diff0 [THEN iffD1])
        apply simp_all[2]
        apply ring
        done
      with p2 = Point x2 y2 p3 = Point x3 y3 on_curve a b p2 on_curve a b p3
      have "p2 = p3  p2 = opp p3" by (rule curve_elt_opp)
      then show ?case
      proof
        assume "p2 = opp p3"
        with on_curve a b p3 have "opp p2 = p3"
          by (simp add: opp_opp)
        with p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
        have "add a p1 p2 = add a p1 (opp p2)" by simp
        show ?case
        proof (cases "p1 = opp p1")
          case True
          with p1  opp p2 p1  opp p3
          have "p1  p2" "p1  p3" by auto
          with l' = l x1 = x2  _ _ x1' = x3  _  _
            p1 = Point x1 y1 p1 = Point x1' y1'
            p2 = Point x2 y2 p3 = Point x3 y3
            p2 = opp p3
          have eq: "(y2  y1)  (x2  x1) = (y3  y1)  (x2  x1)" and "x1  x2"
            by (auto simp add: opp_Point)
          from eq have "y2 = y3"
            apply (field (prems))
            apply (rule eq_diff0 [THEN iffD1])
            apply (insert x1  x2 x1  carrier R y1  carrier R
              x2  carrier R y2  carrier R y3  carrier R)
            apply simp_all
            apply (erule subst)
            apply (rule eq_diff0 [THEN iffD1])
            apply simp_all
            apply ring
            apply (simp add: eq_diff0)
            done
          with p2 = opp p3 p2 = Point x2 y2 p3 = Point x3 y3
          show ?thesis by (simp add: opp_Point)
        next
          case False
          with a b on_curve a b p1 on_curve a b p2
            add a p1 p2 = add a p1 (opp p2)
          have "p2 = opp p2" by (rule compat_add_opp)
          with opp p2 = p3 show ?thesis by simp
        qed
      qed
    next
      assume "x4 = x1"
      with p4 = Point x4 y4 [simplified p4 = add a p1 p2]
        p1 = Point x1 y1
        add_closed [OF a b on_curve a b p1 on_curve a b p2]
        on_curve a b p1
      have "add a p1 p2 = p1  add a p1 p2 = opp p1" by (rule curve_elt_opp)
      then show ?case
      proof
        assume "add a p1 p2 = p1"
        with a b on_curve a b p1 on_curve a b p2
        have "add a p2 p1 = p1" by (simp add: add_comm)
        with a b ab on_curve a b p2 on_curve a b p1
        have "p2 = Infinity" by (rule uniq_zero)
        moreover from add a p1 p2 = p1
          p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
          a b on_curve a b p1 on_curve a b p3
        have "add a p3 p1 = p1" by (simp add: add_comm)
        with a b ab on_curve a b p3 on_curve a b p1
        have "p3 = Infinity" by (rule uniq_zero)
        ultimately show ?case by simp
      next
        assume "add a p1 p2 = opp p1"
        with a b ab on_curve a b p1 on_curve a b p2
        have "p2 = add a (opp p1) (opp p1)" by (rule add_opp_double_opp)
        moreover from add a p1 p2 = opp p1
          p4 = p5 p4 = add a p1 p2 p5 = add a p1 p3
        have "add a p1 p3 = opp p1" by simp
        with a b ab on_curve a b p1 on_curve a b p3
        have "p3 = add a (opp p1) (opp p1)" by (rule add_opp_double_opp)
        ultimately show ?case by simp
      qed
    qed
  qed
qed

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

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

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

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

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

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

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

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

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

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

end

subsection ‹Projective Coordinates›

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

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

definition (in cring) padd :: "'a  'a ppoint  'a ppoint  'a ppoint" where
  "padd a p1 p2 =
     (let
        (x1, y1, z1) = p1;
        (x2, y2, z2) = p2
      in
        if z1 = 𝟬 then p2
        else if z2 = 𝟬 then p1
        else
          let
            d1 = x2  z1;
            d2 = x1  z2;
            l = d1  d2;
            m = y2  z1  y1  z2
          in
            if l = 𝟬 then
              if m = 𝟬 then pdouble a p1
              else (𝟬, 𝟬, 𝟬)
            else
              let h = m [^] (2::nat)  z1  z2  (d1  d2)  l [^] (2::nat)
              in
                (l  h,
                 (d2  l [^] (2::nat)  h)  m  l [^] (3::nat)  y1  z2,
                 l [^] (3::nat)  z1  z2))"

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

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

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

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

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

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

lemma (in ell_field) on_curvep_iff_on_curve:
  assumes "a  carrier R" "b  carrier R" "in_carrierp p"
  shows "on_curvep a b p = on_curve a b (make_affine p)"
  using assms
proof (induct p rule: prod_induct3)
  case (fields x y z)
  show "on_curvep a b (x, y, z) = on_curve a b (make_affine (x, y, z))"
  proof
    assume H: "on_curvep a b (x, y, z)"
    then have carrier: "x  carrier R" "y  carrier R" "z  carrier R"
      and yz: "z  𝟬 
        y [^] (2::nat)  z = x [^] (3::nat)  a  x  z [^] (2::nat)  b  z [^] (3::nat)"
      by (simp_all add: on_curvep_def)
    show "on_curve a b (make_affine (x, y, z))"
    proof (cases "z = 𝟬")
      case True
      then show ?thesis by (simp add: on_curve_def make_affine_def)
    next
      case False
      then show ?thesis
        apply (simp add: on_curve_def make_affine_def carrier)
        apply (field yz [OF False])
        apply assumption
        done
    qed
  next
    assume H: "on_curve a b (make_affine (x, y, z))"
    show "on_curvep a b (x, y, z)"
    proof (cases "z = 𝟬")
      case True
      with in_carrierp (x, y, z) show ?thesis
        by (simp add: on_curvep_def in_carrierp_def)
    next
      case False
      from in_carrierp (x, y, z)
      have carrier: "x  carrier R" "y  carrier R" "z  carrier R"
        by (simp_all add: in_carrierp_def)
      from H show ?thesis
        apply (simp add: on_curve_def on_curvep_def make_affine_def carrier False)
        apply (field (prems))
        apply field
        apply (simp_all add: False)
        done
    qed
  qed
qed

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

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

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

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

lemma (in ell_field) pdouble_correct:
  "a  carrier R  in_carrierp p 
   make_affine (pdouble a p) = add a (make_affine p) (make_affine p)"
proof (induct p rule: prod_induct3)
  case (fields x y z)
  then have "x  carrier R" "y  carrier R" "z  carrier R"
    by (simp_all add: in_carrierp_def)
  then show ?case
    apply (auto simp add: add_def pdouble_def make_affine_def equal_neg_zero divide_eq_0_iff
      integral_iff Let_def simp del: minus_divide_left)
    apply field
    apply (simp add: integral_iff)
    apply field
    apply (simp add: integral_iff)
    done
qed

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

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

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

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

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

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

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

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

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

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

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

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

lemma (in ell_field) padd_proj_eq_cong:
  "a  carrier R  b  carrier R  on_curvep a b p1  on_curvep a b p1' 
   on_curvep a b p2  on_curvep a b p2'  proj_eq p1 p1'  proj_eq p2 p2' 
   proj_eq (padd a p1 p2) (padd a p1' p2')"
  by (simp add: make_affine_proj_eq_iff padd_in_carrierp padd_correct)

end