# 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 p⇩1 p⇩2 = (case p⇩1 of
Infinity ⇒ p⇩2
| Point x⇩1 y⇩1 ⇒ (case p⇩2 of
Infinity ⇒ p⇩1
| Point x⇩2 y⇩2 ⇒
if x⇩1 = x⇩2 then
if y⇩1 = - y⇩2 then Infinity
else
let
l = (3 * x⇩1 ^ 2 + a) / (2 * y⇩1);
x⇩3 = l ^ 2 - 2 * x⇩1
in
Point x⇩3 (- y⇩1 - l * (x⇩3 - x⇩1))
else
let
l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1);
x⇩3 = l ^ 2 - x⇩1 - x⇩2
in
Point x⇩3 (- y⇩1 - l * (x⇩3 - x⇩1))))"

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"

lemma opp_Infinity [simp]: "opp Infinity = Infinity"

lemma opp_Point: "opp (Point x y) = Point x (- y)"

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 "p⇩1 = Point x⇩1 y⇩1"
and "p⇩2 = Point x⇩2 y⇩2"
and "on_curve a b p⇩1"
and "on_curve a b p⇩2"
and "x⇩1 = x⇩2"
shows "p⇩1 = p⇩2 ∨ p⇩1 = opp p⇩2"
proof -
from ‹p⇩1 = Point x⇩1 y⇩1› ‹on_curve a b p⇩1›
have "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b"
moreover from ‹p⇩2 = Point x⇩2 y⇩2› ‹on_curve a b p⇩2› ‹x⇩1 = x⇩2›
have "x⇩1 ^ 3 + a * x⇩1 + b = y⇩2 ^ 2"
ultimately have "y⇩1 = y⇩2 ∨ y⇩1 = - y⇩2"
with ‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹x⇩1 = x⇩2› show ?thesis
qed

assumes "on_curve a b p⇩1" and "on_curve a b p⇩2"
shows "on_curve a b (add a p⇩1 p⇩2)"
proof (cases p⇩1)
case (Point x⇩1 y⇩1)
note Point' = this
show ?thesis
proof (cases p⇩2)
case (Point x⇩2 y⇩2)
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
note True' = this
show ?thesis
proof (cases "y⇩1 = - y⇩2")
case True
with True' Point Point'
show ?thesis
next
case False
note on_curve1 = ‹on_curve a b p⇩1› [simplified Point' on_curve_def True', simplified]
from False True' Point Point' assms
have "y⇩1 ≠ 0" by (auto simp add: on_curve_def)
with False True' Point Point' assms
show ?thesis
apply (field on_curve1)
done
qed
next
case False
note on_curve1 = ‹on_curve a b p⇩1› [simplified Point' on_curve_def, simplified]
note on_curve2 = ‹on_curve a b p⇩2› [simplified Point on_curve_def, simplified]
from assms show ?thesis
apply (field on_curve1 on_curve2)
done
qed
next
case Infinity
with Point ‹on_curve a b p⇩1› show ?thesis
qed
next
case Infinity
with ‹on_curve a b p⇩2› show ?thesis
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: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹
p⇩2 = add a p⇩1 p⇩1 ⟹ y⇩1 ≠ 0 ⟹
l = (3 * x⇩1 ^ 2 + a) / (2 * y⇩1) ⟹
x⇩2 = l ^ 2 - 2 * x⇩1 ⟹
y⇩2 = - y⇩1 - l * (x⇩2 - x⇩1) ⟹
P p⇩1 p⇩1 p⇩2"
and R5: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹ p⇩3 = Point x⇩3 y⇩3 ⟹
p⇩3 = add a p⇩1 p⇩2 ⟹ x⇩1 ≠ x⇩2 ⟹
l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1) ⟹
x⇩3 = l ^ 2 - x⇩1 - x⇩2 ⟹
y⇩3 = - y⇩1 - l * (x⇩3 - x⇩1) ⟹
P p⇩1 p⇩2 p⇩3"
shows "P p q (add a p q)"
proof (cases p)
case Infinity
then show ?thesis
next
case (Point x⇩1 y⇩1)
note Point' = this
show ?thesis
proof (cases q)
case Infinity
with Point show ?thesis
next
case (Point x⇩2 y⇩2)
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
note True' = this
show ?thesis
proof (cases "y⇩1 = - y⇩2")
case True
with p Point Point' True' R3 [of p] show ?thesis
next
case False
from True' Point Point' p q have "(y⇩1 - y⇩2) * (y⇩1 + y⇩2) = 0"
by (simp add: on_curve_def ring_distribs power2_eq_square)
with False have "y⇩1 = y⇩2"
with False True' Point Point' show ?thesis
apply simp
apply (rule R4)
done
qed
next
case False
with Point Point' show ?thesis
apply -
apply (rule R5)
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: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹ p⇩3 = Point x⇩3 y⇩3 ⟹
p⇩3 = add a p⇩1 p⇩2 ⟹ p⇩1 ≠ opp p⇩2 ⟹
x⇩1 = x⇩2 ∧ y⇩1 = y⇩2 ∧ l = (3 * x⇩1 ^ 2 + a) / (2 * y⇩1) ∨
x⇩1 ≠ x⇩2 ∧ l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1) ⟹
x⇩3 = l ^ 2 - x⇩1 - x⇩2 ⟹
y⇩3 = - y⇩1 - l * (x⇩3 - x⇩1) ⟹
P p⇩1 p⇩2 p⇩3"
shows "P p q (add a p q)"
using p q
apply (rule R1)
apply (rule R2)
apply (rule R3)
apply assumption
apply (rule R4)
apply assumption+
apply simp
apply simp
apply simp
apply (rule R4)
apply assumption+
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]

lemma spec1_assoc:
assumes p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_generic p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_generic p⇩1 (add a p⇩2 p⇩3)"
using p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩3 x⇩3 y⇩3 p⇩5 x⇩5 y⇩5 l⇩1)
from ‹on_curve a b p⇩2› ‹on_curve a b p⇩3› ‹p⇩5 = add a p⇩2 p⇩3›
with ‹on_curve a b p⇩1› show ?case using Gen [simplified ‹p⇩2 = Point x⇩2' y⇩2'›]
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 p⇩1 x⇩1' y⇩1' p⇩5' x⇩5' y⇩5' p⇩6 x⇩6 y⇩6 l⇩2)
from ‹on_curve a b p⇩1› ‹on_curve a b (Point x⇩2' y⇩2')›
‹p⇩4 = add a p⇩1 (Point x⇩2' y⇩2')›
then show ?case using ‹on_curve a b p⇩3› Gen
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 p⇩4' x⇩4' y⇩4' p⇩3' x⇩3' y⇩3' p⇩7 x⇩7 y⇩7 l⇩3)
from ‹p⇩4' = Point x⇩4' y⇩4'› ‹p⇩4' = Point x⇩4 y⇩4›
have p⇩4: "x⇩4' = x⇩4" "y⇩4' = y⇩4" by simp_all
from ‹p⇩3' = Point x⇩3' y⇩3'› ‹p⇩3' = Point x⇩3 y⇩3›
have p⇩3: "x⇩3' = x⇩3" "y⇩3' = y⇩3" by simp_all
from ‹p⇩1 = Point x⇩1' y⇩1'› ‹p⇩1 = Point x⇩1 y⇩1›
have p⇩1: "x⇩1' = x⇩1" "y⇩1' = y⇩1" by simp_all
from ‹p⇩5' = Point x⇩5' y⇩5'› ‹p⇩5' = Point x⇩5 y⇩5›
have p⇩5: "x⇩5' = x⇩5" "y⇩5' = y⇩5" by simp_all
from ‹Point x⇩2' y⇩2' = Point x⇩2 y⇩2›
have p⇩2: "x⇩2' = x⇩2" "y⇩2' = y⇩2" by simp_all
note ps = p⇩1 p⇩2 p⇩3 p⇩4 p⇩5
note ps' =
‹on_curve a b p⇩1› [simplified ‹p⇩1 = Point x⇩1 y⇩1› on_curve_def, simplified]
‹on_curve a b p⇩2› [simplified ‹p⇩2 = Point x⇩2 y⇩2› on_curve_def, simplified]
‹on_curve a b p⇩3› [simplified ‹p⇩3 = Point x⇩3 y⇩3› on_curve_def, simplified]
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps
‹x⇩6 = l⇩2⇧2 - x⇩1' - x⇩5'› ‹x⇩7 = l⇩3⇧2 - x⇩4' - x⇩3'›
‹y⇩6 = - y⇩1' - l⇩2 * (x⇩6 - x⇩1')› ‹y⇩7 = - y⇩4' - l⇩3 * (x⇩7 - x⇩4')›
‹l⇩2 = (y⇩5' - y⇩1') / (x⇩5' - x⇩1')› ‹l⇩3 = (y⇩3' - y⇩4') / (x⇩3' - x⇩4')›
‹l⇩1 = (y⇩3 - y⇩2') / (x⇩3 - x⇩2')› ‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›
‹x⇩5 = l⇩1⇧2 - x⇩2' - x⇩3› ‹y⇩5 = - y⇩2' - l⇩1 * (x⇩5 - x⇩2')›
‹x⇩4 = l⇧2 - x⇩1 - x⇩2› ‹y⇩4 = - y⇩1 - l * (x⇩4 - x⇩1)›)
apply (rule conjI)
apply (field ps')
apply (rule conjI)
apply (simp add: ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›, symmetric])
apply (rule conjI)
apply (rule notI)
apply (ring (prems) ps'(1-2))
apply (cut_tac ‹x⇩1' ≠ x⇩5'› [simplified ‹x⇩5' = x⇩5› ‹x⇩1' = x⇩1› ‹x⇩5 = l⇩1⇧2 - x⇩2' - x⇩3›
‹l⇩1 = (y⇩3 - y⇩2') / (x⇩3 - x⇩2')› ‹y⇩2' = y⇩2› ‹x⇩2' = x⇩2›])
apply (erule notE)
apply (rule sym)
apply (field ps'(1-2))
apply (simp add: ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›, symmetric])
apply (rule conjI)
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
apply (rule notI)
apply (ring (prems) ps'(1-2))
apply (cut_tac ‹x⇩4' ≠ x⇩3'› [simplified ‹x⇩4' = x⇩4› ‹x⇩3' = x⇩3› ‹x⇩4 = l⇧2 - x⇩1 - x⇩2›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›])
apply (erule notE)
apply (rule sym)
apply (field ps'(1-2))
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
apply (field ps')
apply (rule conjI)
apply (rule notI)
apply (ring (prems) ps'(1-2))
apply (cut_tac ‹x⇩1' ≠ x⇩5'› [simplified ‹x⇩5' = x⇩5› ‹x⇩1' = x⇩1› ‹x⇩5 = l⇩1⇧2 - x⇩2' - x⇩3›
‹l⇩1 = (y⇩3 - y⇩2') / (x⇩3 - x⇩2')› ‹y⇩2' = y⇩2› ‹x⇩2' = x⇩2›])
apply (erule notE)
apply (rule sym)
apply (field ps'(1-2))
apply (simp add: ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›, symmetric])
apply (rule conjI)
apply (simp add: ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›, symmetric])
apply (rule conjI)
apply (rule notI)
apply (ring (prems) ps'(1-2))
apply (cut_tac ‹x⇩4' ≠ x⇩3'› [simplified ‹x⇩4' = x⇩4› ‹x⇩3' = x⇩3› ‹x⇩4 = l⇧2 - x⇩1 - x⇩2›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›])
apply (erule notE)
apply (rule sym)
apply (field ps'(1-2))
apply (simp_all add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
qed
qed
qed
qed

lemma spec2_assoc:
assumes p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_tangent p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_generic p⇩1 (add a p⇩2 p⇩3)"
using p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩5 x⇩5 y⇩5 l⇩1)
from ‹on_curve a b p⇩2› ‹p⇩5 = add a p⇩2 p⇩2›
with ‹on_curve a b p⇩1› show ?case using Tan
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 p⇩1 x⇩1' y⇩1' p⇩5' x⇩5' y⇩5' p⇩6 x⇩6 y⇩6 l⇩2)
from ‹on_curve a b p⇩1› ‹on_curve a b p⇩2› ‹p⇩4 = add a p⇩1 p⇩2›
then show ?case using ‹on_curve a b p⇩2› Gen
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 p⇩4' x⇩4' y⇩4' p⇩3' x⇩3' y⇩3' p⇩7 x⇩7 y⇩7 l⇩3)
from
‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
have
y1: "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b" and
y2: "y⇩2 ^ 2 = x⇩2 ^ 3 + a * x⇩2 + b"
from
‹p⇩5' = Point x⇩5' y⇩5'›
‹p⇩5' = Point x⇩5 y⇩5›
‹p⇩4' = Point x⇩4' y⇩4'›
‹p⇩4' = Point x⇩4 y⇩4›
‹p⇩3' = Point x⇩2' y⇩2'›
‹p⇩3' = Point x⇩2 y⇩2›
‹p⇩3' = Point x⇩3' y⇩3'›
‹p⇩1 = Point x⇩1' y⇩1'›
‹p⇩1 = Point x⇩1 y⇩1›
have ps:
"x⇩5' = x⇩5" "y⇩5' = y⇩5"
"x⇩4' = x⇩4" "y⇩4' = y⇩4" "x⇩3' = x⇩2" "y⇩3' = y⇩2" "x⇩2' = x⇩2" "y⇩2' = y⇩2"
"x⇩1' = x⇩1" "y⇩1' = y⇩1"
by simp_all
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps
‹x⇩7 = l⇩3 ^ 2 - x⇩4' - x⇩3'›
‹y⇩7 = - y⇩4' - l⇩3 * (x⇩7 - x⇩4')›
‹l⇩3 = (y⇩3' - y⇩4') / (x⇩3' - x⇩4')›
‹x⇩6 = l⇩2 ^ 2 - x⇩1' - x⇩5'›
‹y⇩6 = - y⇩1' - l⇩2 * (x⇩6 - x⇩1')›
‹l⇩2 = (y⇩5' - y⇩1') / (x⇩5' - x⇩1')›
‹x⇩5 = l⇩1 ^ 2 - 2 * x⇩2'›
‹y⇩5 = - y⇩2' - l⇩1 * (x⇩5 - x⇩2')›
‹l⇩1 = (3 * x⇩2' ^ 2 + a) / (2 * y⇩2')›
‹x⇩4 = l ^ 2 - x⇩1 - x⇩2›
‹y⇩4 = - y⇩1 - l * (x⇩4 - x⇩1)›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›)
apply (rule conjI)
apply (field y1 y2)
apply (intro conjI)
apply (simp add: ‹y⇩2' ≠ 0› [simplified ‹y⇩2' = y⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩1' ≠ x⇩5'› [simplified
‹x⇩5 = l⇩1 ^ 2 - 2 * x⇩2'›
‹l⇩1 = (3 * x⇩2' ^ 2 + a) / (2 * y⇩2')›
‹x⇩1' = x⇩1› ‹x⇩2' = x⇩2› ‹y⇩2' = y⇩2› ‹x⇩5' = x⇩5›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: ‹y⇩2' ≠ 0› [simplified ‹y⇩2' = y⇩2›])
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩4' ≠ x⇩3'› [simplified
‹x⇩4 = l ^ 2 - x⇩1 - x⇩2›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›
‹x⇩4' = x⇩4› ‹x⇩3' = x⇩2›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
apply (field y1 y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩1' ≠ x⇩5'› [simplified
‹x⇩5 = l⇩1 ^ 2 - 2 * x⇩2'›
‹l⇩1 = (3 * x⇩2' ^ 2 + a) / (2 * y⇩2')›
‹x⇩1' = x⇩1› ‹x⇩2' = x⇩2› ‹y⇩2' = y⇩2› ‹x⇩5' = x⇩5›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: ‹y⇩2' ≠ 0› [simplified ‹y⇩2' = y⇩2›])
apply (simp add: ‹y⇩2' ≠ 0› [simplified ‹y⇩2' = y⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩4' ≠ x⇩3'› [simplified
‹x⇩4 = l ^ 2 - x⇩1 - x⇩2›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›
‹x⇩4' = x⇩4› ‹x⇩3' = x⇩2›]])
apply (rule sym)
apply (field y1 y2)
apply (simp_all add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
qed
qed
next
case (Gen p⇩3 x⇩3 y⇩3 p⇩5 x⇩5 y⇩5 p⇩6 x⇩6 y⇩6 l⇩1)
then show ?case by (simp add: is_tangent_def)
qed
qed

lemma spec3_assoc:
assumes p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_tangent p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_tangent p⇩1 (add a p⇩2 p⇩3)"
using p⇩1 p⇩2 assms
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩5 x⇩5 y⇩5 l⇩1)
from ‹on_curve a b p⇩2› ‹p⇩5 = add a p⇩2 p⇩2›
with ‹on_curve a b p⇩1› show ?case using Tan
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 p⇩1 x⇩1' y⇩1' p⇩6 x⇩6 y⇩6 l⇩2)
from ‹on_curve a b p⇩1› ‹on_curve a b p⇩2› ‹p⇩4 = add a p⇩1 p⇩2›
then show ?case using ‹on_curve a b p⇩2› Tan
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 p⇩4' x⇩4' y⇩4' p⇩2' x⇩2'' y⇩2'' p⇩7 x⇩7 y⇩7 l⇩3)
from
‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
have
y1: "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b" and
y2: "y⇩2 ^ 2 = x⇩2 ^ 3 + a * x⇩2 + b"
from
‹p⇩4' = Point x⇩4' y⇩4'›
‹p⇩4' = Point x⇩4 y⇩4›
‹p⇩2' = Point x⇩2' y⇩2'›
‹p⇩2' = Point x⇩2 y⇩2›
‹p⇩2' = Point x⇩2'' y⇩2''›
‹p⇩1 = Point x⇩1' y⇩1'›
‹p⇩1 = Point x⇩1 y⇩1›
‹p⇩1 = Point x⇩5 y⇩5›
have ps:
"x⇩4' = x⇩4" "y⇩4' = y⇩4" "x⇩2' = x⇩2" "y⇩2' = y⇩2" "x⇩2'' = x⇩2" "y⇩2'' = y⇩2"
"x⇩1' = x⇩5" "y⇩1' = y⇩5" "x⇩1 = x⇩5" "y⇩1 = y⇩5"
by simp_all
note qs =
‹x⇩7 = l⇩3 ^ 2 - x⇩4' - x⇩2''›
‹y⇩7 = - y⇩4' - l⇩3 * (x⇩7 - x⇩4')›
‹l⇩3 = (y⇩2'' - y⇩4') / (x⇩2'' - x⇩4')›
‹x⇩6 = l⇩2 ^ 2 - 2 * x⇩1'›
‹y⇩6 = - y⇩1' - l⇩2 * (x⇩6 - x⇩1')›
‹x⇩5 = l⇩1 ^ 2 - 2 * x⇩2'›
‹y⇩5 = - y⇩2' - l⇩1 * (x⇩5 - x⇩2')›
‹l⇩1 = (3 * x⇩2' ^ 2 + a) / (2 * y⇩2')›
‹l⇩2 = (3 * x⇩1' ^ 2 + a) / (2 * y⇩1')›
‹x⇩4 = l ^ 2 - x⇩1 - x⇩2›
‹y⇩4 = - y⇩1 - l * (x⇩4 - x⇩1)›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›
from ‹y⇩2' ≠ 0› ‹y⇩2' = y⇩2›
have "2 * y⇩2 ≠ 0" by simp
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps qs)
apply (rule conjI)
apply (field y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹y⇩1' ≠ 0›])
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩4' ≠ x⇩2''›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (intro conjI)
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (erule thin_rl)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (field y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹y⇩1' ≠ 0›])
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩4' ≠ x⇩2''›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (erule thin_rl)
apply (rule conjI)
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule ‹2 * y⇩2 ≠ 0›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹2 * y⇩2 ≠ 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_opp: "on_curve a b p ⟹ add a p (opp p) = Infinity"

assumes "on_curve a b p⇩1" "on_curve a b p⇩2"
proof (cases p⇩1)
case Infinity
next
case (Point x⇩1 y⇩1)
note Point' = this
with ‹on_curve a b p⇩1›
have y1: "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b"
show ?thesis
proof (cases p⇩2)
case Infinity
next
case (Point x⇩2 y⇩2)
with ‹on_curve a b p⇩2›
have y2: "y⇩2 ^ 2 = x⇩2 ^ 3 + a * x⇩2 + b"
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
show ?thesis
proof (cases "y⇩1 = - y⇩2")
case True
with Point Point' ‹x⇩1 = x⇩2› show ?thesis
next
case False
with y1 y2 [symmetric] ‹x⇩1 = x⇩2› Point Point'
show ?thesis
qed
next
case False
with Point Point' show ?thesis
apply (rule conjI)
apply field
apply simp
apply field
apply simp
done
qed
qed
qed

lemma uniq_opp:
assumes "add a p⇩1 p⇩2 = Infinity"
shows "p⇩2 = opp p⇩1"
using assms
split: point.split_asm if_split_asm)

lemma uniq_zero:
assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
shows "p⇩1 = Infinity"
using p⇩1 p⇩2 assms
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
from ‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩2 = p⇩1›
have "x⇩2 = x⇩1" "y⇩2 = y⇩1" by simp_all
with ‹y⇩2 = - y⇩1 - l * (x⇩2 - x⇩1)› ‹y⇩1 ≠ 0›
have "- y⇩1 = y⇩1" by simp
with ‹y⇩1 ≠ 0›
show ?case by simp
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
then have y1: "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b"
and y2: "y⇩2 ^ 2 = x⇩2 ^ 3 + a * x⇩2 + b"
from ‹p⇩3 = p⇩2› ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩3 = Point x⇩3 y⇩3›
have ps: "x⇩3 = x⇩2" "y⇩3 = y⇩2" by simp_all
with ‹y⇩3 = - y⇩1 - l * (x⇩3 - x⇩1)›
have "y⇩2 = - y⇩1 - l * (x⇩2 - x⇩1)" by simp
also from ‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)› ‹x⇩1 ≠ x⇩2›
have "l * (x⇩2 - x⇩1) = y⇩2 - y⇩1"
by simp
also have "- y⇩1 - (y⇩2 - y⇩1) = (- y⇩1 + y⇩1) + - y⇩2"
by simp
finally have "y⇩2 = 0" by simp
with ‹p⇩2 = Point x⇩2 y⇩2› ‹on_curve a b p⇩2›
have x2: "x⇩2 ^ 3 = - (a * x⇩2 + b)"
from ‹x⇩3 = l ^ 2 - x⇩1 - x⇩2› ‹x⇩3 = x⇩2›
have "l ^ 2 - x⇩1 - x⇩2 - x⇩2 = x⇩2 - x⇩2" by simp
then have "l ^ 2 - x⇩1 - 2 * x⇩2 = 0" by simp
then have "x⇩2 * (l ^ 2 - x⇩1 - 2 * x⇩2) = x⇩2 * 0" by simp
then have "(x⇩2 - x⇩1) * (2 * a * x⇩2 + 3 * b) = 0"
apply (simp only: ‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)› ‹y⇩2 = 0›)
apply (field (prems) y1 x2)
apply (ring y1 x2)
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
with ‹x⇩1 ≠ x⇩2› have "2 * a * x⇩2 + 3 * b = 0" by simp
then have "2 * a * x⇩2 = - (3 * b)"
from y2 [symmetric] ‹y⇩2 = 0›
have "(- (2 * a)) ^ 3 * (x⇩2 ^ 3 + a * x⇩2 + b) = 0"
by simp
then have "b * (4 * a ^ 3 + 27 * b ^ 2) = 0"
apply (ring (prems) ‹2 * a * x⇩2 = - (3 * b)›)
apply (ring ‹2 * a * x⇩2 = - (3 * b)›)
done
with ab have "b = 0" by (simp add: nonsingular_def)
with ‹2 * a * x⇩2 + 3 * b = 0› ab
have "x⇩2 = 0" by (simp add: nonsingular_def)
from ‹l ^ 2 - x⇩1 - 2 * x⇩2 = 0›
show ?case
apply (simp add: ‹x⇩2 = 0› ‹y⇩2 = 0› ‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›)
apply (field (prems) y1 ‹b = 0›)
apply (insert ab ‹b = 0› ‹x⇩1 ≠ x⇩2› ‹x⇩2 = 0›)
apply simp
done
qed

assumes p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
shows "opp (add a p⇩1 p⇩2) = add a (opp p⇩1) (opp p⇩2)"
proof (cases p⇩1)
case Infinity
next
case (Point x⇩1 y⇩1)
show ?thesis
proof (cases p⇩2)
case Infinity
with ‹p⇩1 = Point x⇩1 y⇩1› show ?thesis
next
case (Point x⇩2 y⇩2)
with ‹p⇩1 = Point x⇩1 y⇩1› p⇩1 p⇩2
have "x⇩1 ^ 3 + a * x⇩1 + b = y⇩1 ^ 2"
"x⇩2 ^ 3 + a * x⇩2 + b = y⇩2 ^ 2"
with Point ‹p⇩1 = Point x⇩1 y⇩1› show ?thesis
apply (cases "x⇩1 = x⇩2")
apply (cases "y⇩1 = - y⇩2")
apply (rule conjI)
apply field
apply simp
apply field
apply simp
done
qed
qed

assumes p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and "p⇩1 ≠ opp p⇩1"
shows "p⇩2 = opp p⇩2"
using p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
then have "add a p⇩1 p⇩1 = Infinity"
then have "p⇩1 = opp p⇩1" by (rule uniq_opp)
with ‹p⇩1 ≠ opp p⇩1› show ?case ..
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
have "(2::'a) * 2 ≠ 0"
by (simp only: mult_eq_0_iff) simp
then have "(4::'a) ≠ 0" by simp
from Gen have "((- y⇩2 - y⇩1) / (x⇩2 - x⇩1)) ^ 2 - x⇩1 - x⇩2 =
((y⇩2 - y⇩1) / (x⇩2 - x⇩1)) ^ 2 - x⇩1 - x⇩2"
then show ?case
apply (field (prems))
apply (insert ‹p⇩1 ≠ opp p⇩1›
‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹4 ≠ 0›)[1]
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
qed

assumes ab: "nonsingular a b"
and p: "on_curve a b p"
and "p ≠ opp p"
and "add a p p ≠ opp p"
using add_closed [OF p p] opp_closed [OF p] assms
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 x⇩1 y⇩1 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
from ‹opp p = Point x⇩2 y⇩2›
have "p = Point x⇩2 (- y⇩2)"
by (auto simp add: opp_def split: point.split_asm)
with ‹add a p p = Point x⇩1 y⇩1› [symmetric]
obtain l' where l':
"l' = (3 * x⇩2 ^ 2 + a) / (2 * - y⇩2)"
and xy: "x⇩1 = l' ^ 2 - 2 * x⇩2"
"y⇩1 = - (- y⇩2) - l' * (x⇩1 - x⇩2)"
and y2: "- y⇩2 ≠ - (- y⇩2)"
have "x⇩3 = x⇩2"
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)› ‹x⇩3 = l ^ 2 - x⇩1 - x⇩2›)
apply field
apply (insert ‹x⇩1 ≠ x⇩2›)
done
then have "p⇩3 = p ∨ p⇩3 = opp p"
by (rule curve_elt_opp [OF ‹p⇩3 = Point x⇩3 y⇩3› ‹p = Point x⇩2 (- y⇩2)›
‹on_curve a b p›])
then show ?case
proof
assume "p⇩3 = p"
show ?thesis by simp
next
assume "p⇩3 = 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 x⇩1 y⇩1› show ?thesis by simp
qed
qed

assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and "add a p⇩1 p⇩2 = opp p⇩1"
shows "p⇩2 = add a (opp p⇩1) (opp p⇩1)"
proof (cases "p⇩1 = opp p⇩1")
case True
with ab p⇩2 p⇩1 have "p⇩2 = Infinity" by (rule uniq_zero)
also from ‹on_curve a b p⇩1› have "… = add a p⇩1 (opp p⇩1)"
also from True have "… = add a (opp p⇩1) (opp p⇩1)" by simp
finally show ?thesis .
next
case False
from p⇩1 p⇩2 False assms show ?thesis
case InfL
then show ?case by simp
next
case InfR
then show ?case by simp
next
case Opp
next
case (Tan p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
from ‹p⇩2 = opp p⇩1› ‹on_curve a b p⇩1›
have "p⇩1 = opp p⇩2" by (simp add: opp_opp)
also note ‹p⇩2 = add a p⇩1 p⇩1›
finally show ?case using ‹on_curve a b p⇩1›
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
from ‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
have y⇩1: "y⇩1 ^ 2 = x⇩1 ^ 3 + a * x⇩1 + b"
from ‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
have y⇩2: "y⇩2 ^ 2 = x⇩2 ^ 3 + a * x⇩2 + b"
from ‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩1 ≠ opp p⇩1›
have "y⇩1 ≠ 0"
from Gen have "x⇩1 = ((y⇩2 - y⇩1) / (x⇩2 - x⇩1)) ^ 2 - x⇩1 - x⇩2"
then have "2 * y⇩2 * y⇩1 = a * x⇩2 + 3 * x⇩2 * x⇩1 ^ 2 + a * x⇩1 -
x⇩1 ^ 3 + 2 * b"
apply (field (prems) y⇩1 y⇩2)
apply (field y⇩1 y⇩2)
apply simp
apply (simp add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
then have "(x⇩2 - (((3 * x⇩1 ^ 2 + a) / (2 * (- y⇩1))) ^ 2 -
2 * x⇩1)) * (x⇩2 - x⇩1) ^ 2 = 0"
apply (drule_tac f="λx. x ^ 2" in arg_cong)
apply (field (prems) y⇩1 y⇩2)
apply (field y⇩1 y⇩2)
apply (simp_all add: ‹y⇩1 ≠ 0›)
done
with ‹x⇩1 ≠ x⇩2›
have "x⇩2 = ((3 * x⇩1 ^ 2 + a) / (2 * (- y⇩1))) ^ 2 - 2 * x⇩1"
by simp
with ‹p⇩2 = Point x⇩2 y⇩2› _ ‹on_curve a b p⇩2›
opp_closed [OF ‹on_curve a b p⇩1›] opp_closed [OF ‹on_curve a b p⇩1›]]
have "p⇩2 = add a (opp p⇩1) (opp p⇩1) ∨ p⇩2 = opp (add a (opp p⇩1) (opp p⇩1))"
apply (rule curve_elt_opp)
apply (simp add: add_def opp_Point Let_def ‹p⇩1 = Point x⇩1 y⇩1› ‹y⇩1 ≠ 0›)
done
then show ?case
proof
assume "p⇩2 = opp (add a (opp p⇩1) (opp p⇩1))"
with ‹on_curve a b p⇩1›
have "p⇩2 = add a p⇩1 p⇩1"
show ?case
proof (cases "add a p⇩1 p⇩1 = opp p⇩1")
case True
from ‹on_curve a b p⇩1›
show ?thesis
apply (simp add: ‹p⇩3 = add a p⇩1 p⇩2› [simplified ‹p⇩3 = opp p⇩1›])
done
next
case False
from ‹on_curve a b p⇩1›
with ab ‹on_curve a b p⇩1› ‹p⇩1 ≠ opp p⇩1› False
have "add a p⇩1 (opp p⇩2) = opp p⇩1"
with ‹p⇩3 = add a p⇩1 p⇩2› ‹p⇩3 = opp p⇩1›
have "add a p⇩1 p⇩2 = add a p⇩1 (opp p⇩2)" by simp
with ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›
have "p⇩2 = opp p⇩2" using ‹p⇩1 ≠ opp p⇩1›
with ‹on_curve a b p⇩1› ‹p⇩2 = add a p⇩1 p⇩1›
qed
qed
qed
qed

lemma cancel:
assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
shows "p⇩2 = p⇩3"
using p⇩1 p⇩2 p⇩1 p⇩2 eq
case InfL
next
case (InfR p)
with ab p⇩3 ‹on_curve a b p›
show ?case by (rule uniq_zero [symmetric])
next
case (Opp p)
from ‹Infinity = add a p p⇩3› [symmetric]
show ?case by (rule uniq_opp [symmetric])
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
from ‹on_curve a b p⇩1› p⇩3 ‹on_curve a b p⇩1› p⇩3 ‹p⇩1 = Point x⇩1 y⇩1›
‹p⇩4 = add a p⇩1 p⇩2› ‹p⇩4 = add a p⇩1 p⇩3› ‹p⇩1 ≠ opp p⇩2›
show ?case
case InfL
next
case (InfR p)
with ‹on_curve a b p⇩2›
with ab ‹on_curve a b p⇩2› ‹on_curve a b p›
show ?case by (rule uniq_zero)
next
case (Opp p)
then have "add a p p⇩2 = Infinity" by simp
then show ?case by (rule uniq_opp)
next
case (Gen p⇩1 x⇩1' y⇩1' p⇩3 x⇩3 y⇩3 p⇩5 x⇩5 y⇩5 l')
from ‹p⇩4 = p⇩5› ‹p⇩4 = Point x⇩4 y⇩4› ‹p⇩5 = Point x⇩5 y⇩5›
‹p⇩1 = Point x⇩1' y⇩1'› ‹p⇩1 = Point x⇩1 y⇩1›
‹y⇩4 = - y⇩1 - l * (x⇩4 - x⇩1)› ‹y⇩5 = - y⇩1' - l' * (x⇩5 - x⇩1')›
have "0 = - y⇩1 - l * (x⇩4 - x⇩1) - (- y⇩1 - l' * (x⇩4 - x⇩1))"
by auto
then have "l' = l ∨ x⇩4 = x⇩1" by auto
then show ?case
proof
assume "l' = l"
with ‹p⇩4 = p⇩5› ‹p⇩4 = Point x⇩4 y⇩4› ‹p⇩5 = Point x⇩5 y⇩5›
‹p⇩1 = Point x⇩1' y⇩1'› ‹p⇩1 = Point x⇩1 y⇩1›
‹x⇩4 = l ^ 2 - x⇩1 - x⇩2› ‹x⇩5 = l' ^ 2 - x⇩1' - x⇩3›
have "0 = l ^ 2 - x⇩1 - x⇩2 - (l ^ 2 - x⇩1 - x⇩3)"
by simp
then have "x⇩2 = x⇩3" by simp
with ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩3 = Point x⇩3 y⇩3› ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
have "p⇩2 = p⇩3 ∨ p⇩2 = opp p⇩3" by (rule curve_elt_opp)
then show ?case
proof
assume "p⇩2 = opp p⇩3"
with ‹on_curve a b p⇩3› have "opp p⇩2 = p⇩3"
with ‹p⇩4 = p⇩5› ‹p⇩4 = add a p⇩1 p⇩2› ‹p⇩5 = add a p⇩1 p⇩3›
have "add a p⇩1 p⇩2 = add a p⇩1 (opp p⇩2)" by simp
show ?case
proof (cases "p⇩1 = opp p⇩1")
case True
with ‹p⇩1 ≠ opp p⇩2› ‹p⇩1 ≠ opp p⇩3›
have "p⇩1 ≠ p⇩2" "p⇩1 ≠ p⇩3" by auto
with ‹l' = l› ‹x⇩1 = x⇩2 ∧ _∨ _› ‹x⇩1' = x⇩3 ∧ _ ∨ _›
‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩1 = Point x⇩1' y⇩1'›
‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩3 = Point x⇩3 y⇩3›
‹p⇩2 = opp p⇩3›
have eq: "(y⇩2 - y⇩1) / (x⇩2 - x⇩1) = (y⇩3 - y⇩1) / (x⇩2 - x⇩1)" and "x⇩1 ≠ x⇩2"
from eq have "y⇩2 = y⇩3"
apply (field (prems))
apply (simp_all add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
with ‹p⇩2 = opp p⇩3› ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩3 = Point x⇩3 y⇩3›
show ?thesis by (simp add: opp_Point)
next
case False
with ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›
have "p⇩2 = opp p⇩2" by (rule compat_add_opp)
with ‹opp p⇩2 = p⇩3› show ?thesis by simp
qed
qed
next
assume "x⇩4 = x⇩1"
with ‹p⇩4 = Point x⇩4 y⇩4› [simplified ‹p⇩4 = add a p⇩1 p⇩2›]
‹p⇩1 = Point x⇩1 y⇩1›
add_closed [OF ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›]
‹on_curve a b p⇩1›
have "add a p⇩1 p⇩2 = p⇩1 ∨ add a p⇩1 p⇩2 = opp p⇩1" by (rule curve_elt_opp)
then show ?case
proof
assume "add a p⇩1 p⇩2 = p⇩1"
with ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›
with ab ‹on_curve a b p⇩2› ‹on_curve a b p⇩1›
have "p⇩2 = Infinity" by (rule uniq_zero)
moreover from ‹add a p⇩1 p⇩2 = p⇩1›
‹p⇩4 = p⇩5› ‹p⇩4 = add a p⇩1 p⇩2› ‹p⇩5 = add a p⇩1 p⇩3›
‹on_curve a b p⇩1› ‹on_curve a b p⇩3›
with ab ‹on_curve a b p⇩3› ‹on_curve a b p⇩1›
have "p⇩3 = Infinity" by (rule uniq_zero)
ultimately show ?case by simp
next
assume "add a p⇩1 p⇩2 = opp p⇩1"
with ab ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›
have "p⇩2 = add a (opp p⇩1) (opp p⇩1)" by (rule add_opp_double_opp)
moreover from ‹add a p⇩1 p⇩2 = opp p⇩1›
‹p⇩4 = p⇩5› ‹p⇩4 = add a p⇩1 p⇩2› ‹p⇩5 = add a p⇩1 p⇩3›
have "add a p⇩1 p⇩3 = opp p⇩1" by simp
with ab ‹on_curve a b p⇩1› ‹on_curve a b p⇩3›
have "p⇩3 = add a (opp p⇩1) (opp p⇩1)" by (rule add_opp_double_opp)
ultimately show ?case by simp
qed
qed
qed
qed

assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
proof (cases "add a p⇩1 p⇩2 = opp p⇩2")
case True
then have "add a (add a p⇩1 p⇩2) (opp p⇩2) = add a (opp p⇩2) (opp p⇩2)"
by simp
also from p⇩1 p⇩2 True have "add a p⇩2 p⇩1 = opp p⇩2"
with ab p⇩2 p⇩1 have "add a (opp p⇩2) (opp p⇩2) = p⇩1"
finally show ?thesis .
next
case False
from p⇩1 p⇩2 p⇩1 p⇩2 False show ?thesis
case InfL
next
case InfR
next
case Opp
next
case (Tan p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
note ab ‹on_curve a b p⇩1›
moreover from ‹y⇩1 ≠ 0› ‹p⇩1 = Point x⇩1 y⇩1›
have "p⇩1 ≠ opp p⇩1" by (simp add: opp_Point)
moreover from ‹p⇩2 = add a p⇩1 p⇩1› ‹p⇩2 ≠ opp p⇩1›
have "add a p⇩1 p⇩1 ≠ opp p⇩1" by simp
ultimately have "add a (add a p⇩1 p⇩1) (opp p⇩1) = p⇩1"
with ‹p⇩2 = add a p⇩1 p⇩1› show ?case by simp
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
from ‹p⇩3 = add a p⇩1 p⇩2› ‹on_curve a b p⇩2›
have "p⇩3 = add a p⇩1 (opp (opp p⇩2))" by (simp add: opp_opp)
with
add_closed [OF ‹on_curve a b p⇩1› ‹on_curve a b p⇩2›,
folded ‹p⇩3 = add a p⇩1 p⇩2›]
opp_closed [OF ‹on_curve a b p⇩2›]
opp_closed [OF ‹on_curve a b p⇩2›]
opp_opp [of p⇩2]
Gen
show ?case
case InfL
then show ?case by simp
next
case InfR
next
case (Opp p)
from ‹p = add a p⇩1 (opp (opp p))›
with ab ‹on_curve a b p⇩1› ‹on_curve a b p›
show ?case by (rule uniq_zero [symmetric])
next
case Tan
then show ?case by simp
next
case (Gen p⇩4 x⇩4 y⇩4 p⇩5 x⇩5 y⇩5 p⇩6 x⇩6 y⇩6 l')
from ‹on_curve a b p⇩5› ‹opp p⇩5 = p⇩2›
‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩5 = Point x⇩5 y⇩5›
have "y⇩5 = - y⇩2" "x⇩5 = x⇩2"
by (auto simp add: opp_Point on_curve_def)
from ‹p⇩4 = Point x⇩3 y⇩3› ‹p⇩4 = Point x⇩4 y⇩4›
have "x⇩4 = x⇩3" "y⇩4 = y⇩3" by simp_all
from ‹x⇩4 ≠ x⇩5› show ?case
‹y⇩5 = - y⇩2› ‹x⇩5 = x⇩2›
‹x⇩4 = x⇩3› ‹y⇩4 = y⇩3›
‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩1 = Point x⇩1 y⇩1›
‹x⇩6 = l' ^ 2 - x⇩4 - x⇩5› ‹y⇩6 = - y⇩4 - l' * (x⇩6 - x⇩4)›
‹l' = (y⇩5 - y⇩4) / (x⇩5 - x⇩4)›
‹x⇩3 = l ^ 2 - x⇩1 - x⇩2› ‹y⇩3 = - y⇩1 - l * (x⇩3 - x⇩1)›
‹l = (y⇩2 - y⇩1) / (x⇩2 - x⇩1)›)
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: ‹x⇩1 ≠ x⇩2› [symmetric])
apply field
apply (rule conjI)
apply (rule notI)
apply (erule notE)
apply (ring (prems))
apply (rule sym)
apply field
apply (simp_all add: ‹x⇩1 ≠ x⇩2› [symmetric])
done
qed
qed
qed

assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and eq: "add a p⇩1 p⇩2 = p⇩3"
shows "p⇩1 = add a p⇩3 (opp p⇩2)"
proof -
note eq
also from add_minus_id [OF ab p⇩3 opp_closed [OF p⇩2]] p⇩2
using p⇩1 p⇩2 p⇩3
with ab p⇩2 p⇩1 add_closed [OF p⇩3 opp_closed [OF p⇩2]]
show ?thesis by (rule cancel)
qed

lemma degen_assoc:
assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and H:
"(p⇩1 = Infinity ∨ p⇩2 = Infinity ∨ p⇩3 = Infinity) ∨
(p⇩1 = opp p⇩2 ∨ p⇩2 = opp p⇩3) ∨
(opp p⇩1 = add a p⇩2 p⇩3 ∨ opp p⇩3 = add a p⇩1 p⇩2)"
using H
proof (elim disjE)
assume "p⇩1 = Infinity"
next
assume "p⇩2 = Infinity"
next
assume "p⇩3 = Infinity"
next
assume "p⇩1 = opp p⇩2"
from p⇩2 p⇩3
also from ab p⇩3 p⇩2 have "… = p⇩3" by (rule add_minus_id)
also from p⇩2 have "… = add a (add a p⇩2 (opp p⇩2)) p⇩3"
also from p⇩2 have "… = add a (add a (opp p⇩2) p⇩2) p⇩3"
finally show ?thesis using ‹p⇩1 = opp p⇩2› by simp
next
assume "p⇩2 = opp p⇩3"
from p⇩3
also from ab p⇩1 p⇩3
have "… = add a (add a p⇩1 (opp p⇩3)) (opp (opp p⇩3))"
finally show ?thesis using p⇩3 ‹p⇩2 = opp p⇩3›
next
assume eq: "opp p⇩1 = add a p⇩2 p⇩3"
from eq [symmetric] p⇩1
also from p⇩3 have "… = add a (opp p⇩3) p⇩3"
also from ab p⇩2 p⇩3
have "… = add a (add a (add a (opp p⇩3) (opp p⇩2)) (opp (opp p⇩2))) p⇩3"
also from p⇩2 p⇩3
finally show ?thesis
using opp_add [OF p⇩2 p⇩3] eq [symmetric] p⇩1
next
assume eq: "opp p⇩3 = add a p⇩1 p⇩2"
from opp_add [OF p⇩1 p⇩2] eq [symmetric] p⇩3
also from p⇩1 p⇩2
have "… = add a p⇩1 (add a (add a (opp p⇩1) (opp p⇩2)) (opp (opp p⇩2)))"
also from ab p⇩1 p⇩2 have "… = Infinity"
also from p⇩3 have "… = add a (opp p⇩3) p⇩3"
finally show ?thesis using eq [symmetric] by simp
qed

lemma spec4_assoc:
assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
proof (cases "p⇩1 = Infinity")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩2 = Infinity")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩2 = opp p⇩2")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True [symmetric])
next
case False
show ?thesis
proof (cases "p⇩1 = opp p⇩2")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "opp p⇩1 = add a p⇩2 p⇩2")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "opp p⇩2 = add a p⇩1 p⇩2")
case True
from ab p⇩1 p⇩2 p⇩2
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩1 = add a p⇩2 p⇩2")
case True
from p⇩1 p⇩2 ‹p⇩1 ≠ opp p⇩2› ‹p⇩2 ≠ opp p⇩2›
‹opp p⇩1 ≠ add a p⇩2 p⇩2› ‹opp p⇩2 ≠ add a p⇩1 p⇩2›
‹p⇩1 ≠ Infinity› ‹p⇩2 ≠ Infinity›
show ?thesis
apply (rule spec3_assoc)
apply (rule notI)
apply (drule uniq_zero [OF ab p⇩2 p⇩2])
apply simp
apply (intro conjI notI)
apply (erule notE)
apply (rule uniq_opp [of a])
apply (erule notE)
apply (drule uniq_zero [OF ab add_closed [OF p⇩2 p⇩2] p⇩2])
apply simp
done
next
case False
show ?thesis
proof (cases "p⇩2 = add a p⇩1 p⇩2")
case True
from ab p⇩1 p⇩2 True [symmetric]
have "p⇩1 = Infinity" by (rule uniq_zero)
next
case False
show ?thesis
proof (cases "p⇩1 = p⇩2")
case True
with p⇩2 show ?thesis
next
case False
with p⇩1 p⇩2 ‹p⇩1 ≠ Infinity› ‹p⇩2 ≠ Infinity›
‹p⇩1 ≠ opp p⇩2› ‹p⇩2 ≠ opp p⇩2›
‹p⇩1 ≠ add a p⇩2 p⇩2› ‹p⇩2 ≠ add a p⇩1 p⇩2› ‹opp p⇩2 ≠ add a p⇩1 p⇩2›
show ?thesis
apply (rule_tac spec2_assoc)
apply (rule notI)
apply (erule notE [of "p⇩1 = opp p⇩2"])
apply (rule uniq_opp [of a])
apply (intro conjI notI)
apply (erule notE [of "p⇩2 = opp p⇩2"])
apply (rule uniq_opp)
apply assumption+
apply (rule notE [OF ‹opp p⇩1 ≠ add a p⇩2 p⇩2›])
done
qed
qed
qed
qed
qed
qed
qed
qed
qed

assumes ab: "nonsingular a b"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
proof (cases "p⇩1 = Infinity")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩2 = Infinity")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩3 = Infinity")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩1 = p⇩2")
case True
from p⇩2 p⇩3
also from ab p⇩3 p⇩2 have "… = add a p⇩3 (add a p⇩2 p⇩2)"
also from p⇩2 p⇩3
finally show ?thesis using True by simp
next
case False
show ?thesis
proof (cases "p⇩1 = opp p⇩2")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩2 = p⇩3")
case True
with ab p⇩1 p⇩3 show ?thesis
next
case False
show ?thesis
proof (cases "p⇩2 = opp p⇩3")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "opp p⇩1 = add a p⇩2 p⇩3")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "opp p⇩3 = add a p⇩1 p⇩2")
case True
from ab p⇩1 p⇩2 p⇩3
show ?thesis by (rule degen_assoc) (simp add: True)
next
case False
show ?thesis
proof (cases "p⇩1 = add a p⇩2 p⇩3")
case True
with ab p⇩2 p⇩3 show ?thesis
apply simp
apply (rule cancel [OF ab opp_closed [OF p⇩3]])
done
next
case False
show ?thesis
proof (cases "p⇩3 = add a p⇩1 p⇩2")
case True
with ab p⇩1 p⇩2 show ?thesis
apply simp
apply (rule cancel [OF ab opp_closed [OF p⇩1]])
done
next
case False
with p⇩1 p⇩2 p⇩3
‹p⇩1 ≠ Infinity› ‹p⇩2 ≠ Infinity› ‹p⇩3 ≠ Infinity›
‹p⇩1 ≠ p⇩2› ‹p⇩1 ≠ opp p⇩2› ‹p⇩2 ≠ p⇩3› ‹p⇩2 ≠ opp p⇩3›
‹opp p⇩3 ≠ add a p⇩1 p⇩2› ‹p⇩1 ≠ add a p⇩2 p⇩3›
show ?thesis
apply (rule_tac spec1_assoc [of a b])
apply (rule notI)
apply (erule notE [of "p⇩1 = opp p⇩2"])
apply (rule uniq_opp [of a])
apply (intro conjI notI)
apply (erule notE [of "p⇩2 = opp p⇩3"])
apply (rule uniq_opp [of a])
apply (rule notE [OF ‹opp p⇩1 ≠ add a p⇩2 p⇩3›])
done
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed

"nonsingular a b ⟹
on_curve a b p⇩1 ⟹ on_curve a b p⇩2 ⟹ on_curve a b p⇩3 ⟹

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

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

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

lemma point_mult2_eq_double:
"point_mult a 2 p = add a p p"

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
(let
(x⇩1, y⇩1, z⇩1) = p⇩1;
(x⇩2, y⇩2, z⇩2) = p⇩2
in
if z⇩1 = 0 then p⇩2
else if z⇩2 = 0 then p⇩1
else
let
d⇩1 = x⇩2 * z⇩1;
d⇩2 = x⇩1 * z⇩2;
l = d⇩1 - d⇩2;
m = y⇩2 * z⇩1 - y⇩1 * z⇩2
in
if l = 0 then
if m = 0 then pdouble a p⇩1
else (0, 0, 0)
else
let h = m ^ 2 * z⇩1 * z⇩2 - (d⇩1 + d⇩2) * l ^ 2
in
(l * h,
(d⇩2 * l ^ 2 - h) * m - l ^ 3 * y⇩1 * z⇩2,
l ^ 3 * z⇩1 * z⇩2))"

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

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

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"
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 (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
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
done
qed
qed
qed

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

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 field
apply simp
apply field
apply simp
done
qed

assumes p⇩1: "on_curvep a b p⇩1" and p⇩2: "on_curvep a b p⇩2"
shows "make_affine (padd a p⇩1 p⇩2) = add a (make_affine p⇩1) (make_affine p⇩2)"
using p⇩1
proof (induct p⇩1 rule: prod_induct3)
case (fields x⇩1 y⇩1 z⇩1)
note p⇩1' = fields
from p⇩2 show ?case
proof (induct p⇩2 rule: prod_induct3)
case (fields x⇩2 y⇩2 z⇩2)
then have
yz⇩2: "z⇩2 ≠ 0 ⟹ y⇩2 ^ 2 * z⇩2 * z⇩1 ^ 3 =
(x⇩2 ^ 3 + a * x⇩2 * z⇩2 ^ 2 + b * z⇩2 ^ 3) * z⇩1 ^ 3"
from p⇩1' have
yz⇩1: "z⇩1 ≠ 0 ⟹ y⇩1 ^ 2 * z⇩1 * z⇩2 ^ 3 =
(x⇩1 ^ 3 + a * x⇩1 * z⇩1 ^ 2 + b * z⇩1 ^ 3) * z⇩2 ^ 3"
show ?case
proof (cases "z⇩1 = 0")
case True
then show ?thesis
next
case False
show ?thesis
proof (cases "z⇩2 = 0")
case True
then show ?thesis
next
case False
show ?thesis
proof (cases "x⇩2 * z⇩1 - x⇩1 * z⇩2 = 0")
case True
note x = this
then have x': "x⇩2 * z⇩1 = x⇩1 * z⇩2" by simp
show ?thesis
proof (cases "y⇩2 * z⇩1 - y⇩1 * z⇩2 = 0")
case True
then have y: "y⇩2 * z⇩1 = y⇩1 * z⇩2" by simp
from ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0› x
have "make_affine (x⇩2, y⇩2, z⇩2) = make_affine (x⇩1, y⇩1, z⇩1)"
apply (rule conjI)
apply (field x')
apply simp
apply (field y)
apply simp
done
with True x ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0› p⇩1' fields show ?thesis
next
case False
have "y⇩2 ^ 2 * z⇩1 ^ 3 * z⇩2 = y⇩1 ^ 2 * z⇩1 * z⇩2 ^ 3"
by (ring yz⇩1 [OF ‹z⇩1 ≠ 0›] yz⇩2 [OF ‹z⇩2 ≠ 0›] x')
then have "y⇩2 ^ 2 * z⇩1 ^ 3 * z⇩2 / z⇩1 / z⇩2 =
y⇩1 ^ 2 * z⇩1 * z⇩2 ^ 3 / z⇩1 / z⇩2"
by simp
then have "(y⇩2 * z⇩1) * (y⇩2 * z⇩1) = (y⇩1 * z⇩2) * (y⇩1 * z⇩2)"
apply (field (prems))
apply (field)
apply (rule TrueI)
apply (simp add: ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0›)
done
with False
have y⇩2z⇩1: "y⇩2 * z⇩1 = - (y⇩1 * z⇩2)"
from x False ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0› show ?thesis
apply (rule conjI)
apply (rule impI)
apply (field x')
apply simp
apply (field y⇩2z⇩1)
apply simp
done
qed
next
case False
then have "x⇩1 / z⇩1 ≠ x⇩2 / z⇩2"
apply (rule_tac notI)
apply (erule notE)
apply (drule sym)
apply (field (prems))
apply ring
apply (simp add: ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0›)
done
with False ‹z⇩1 ≠ 0› ‹z⇩2 ≠ 0›
show ?thesis
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)"

"on_curvep a b p⇩1 ⟹ on_curvep a b p⇩2 ⟹ on_curvep a b (padd a p⇩1 p⇩2)"

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

lemma ppoint_mult_correct: "on_curvep a b p ⟹
make_affine (ppoint_mult a n p) = point_mult a n (make_affine p)"

context ell_field begin

definition proj_eq :: "'a ppoint ⇒ 'a ppoint ⇒ bool" where
"proj_eq = (λ(x⇩1, y⇩1, z⇩1) (x⇩2, y⇩2, z⇩2).
(z⇩1 = 0) = (z⇩2 = 0) ∧ x⇩1 * z⇩2 = x⇩2 * z⇩1 ∧ y⇩1 * z⇩2 = y⇩2 * z⇩1)"

end

lemma proj_eq_refl: "proj_eq p p"

lemma proj_eq_sym: "proj_eq p p' ⟹ proj_eq p' p"

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'"
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
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"
then show "make_affine (x, y, z) = make_affine (x', y', z')"
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')"

"on_curvep a b p⇩1 ⟹ on_curvep a b p⇩1' ⟹ on_curvep a b p⇩2 ⟹ on_curvep a b p⇩2' ⟹
proj_eq p⇩1 p⇩1' ⟹ proj_eq p⇩2 p⇩2' ⟹ proj_eq (padd a p⇩1 p⇩2) (padd a p⇩1' p⇩2')"

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

lemma neg_equal_zero:
assumes x: "x ∈ carrier R"
shows "(⊖ x = x) = (x = 𝟬)"
proof
assume "⊖ x = x"
with x have "«2» ⊗ x = x ⊕ ⊖ x"
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 p⇩1 p⇩2 = (case p⇩1 of
Infinity ⇒ p⇩2
| Point x⇩1 y⇩1 ⇒ (case p⇩2 of
Infinity ⇒ p⇩1
| Point x⇩2 y⇩2 ⇒
if x⇩1 = x⇩2 then
if y⇩1 = ⊖ y⇩2 then Infinity
else
let
l = («3» ⊗ x⇩1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ y⇩1);
x⇩3 = l [^] (2::nat) ⊖ «2» ⊗ x⇩1
in
Point x⇩3 (⊖ y⇩1 ⊖ l ⊗ (x⇩3 ⊖ x⇩1))
else
let
l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1);
x⇩3 = l [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2
in
Point x⇩3 (⊖ y⇩1 ⊖ l ⊗ (x⇩3 ⊖ x⇩1))))"

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"

lemma opp_Infinity [simp]: "opp Infinity = Infinity"

lemma opp_Point: "opp (Point x y) = Point x (⊖ y)"

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 "p⇩1 = Point x⇩1 y⇩1"
and "p⇩2 = Point x⇩2 y⇩2"
and "on_curve a b p⇩1"
and "on_curve a b p⇩2"
and "x⇩1 = x⇩2"
shows "p⇩1 = p⇩2 ∨ p⇩1 = opp p⇩2"
proof -
from ‹p⇩1 = Point x⇩1 y⇩1› ‹on_curve a b p⇩1›
have "y⇩1 ∈ carrier R" "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b"
moreover from ‹p⇩2 = Point x⇩2 y⇩2› ‹on_curve a b p⇩2› ‹x⇩1 = x⇩2›
have "y⇩2 ∈ carrier R" "x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b = y⇩2 [^] (2::nat)"
ultimately have "y⇩1 = y⇩2 ∨ y⇩1 = ⊖ y⇩2"
with ‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹x⇩1 = x⇩2› show ?thesis
qed

assumes "a ∈ carrier R" and "b ∈ carrier R"
and "on_curve a b p⇩1" and "on_curve a b p⇩2"
shows "on_curve a b (add a p⇩1 p⇩2)"
proof (cases p⇩1)
case (Point x⇩1 y⇩1)
note Point' = this
show ?thesis
proof (cases p⇩2)
case (Point x⇩2 y⇩2)
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
note True' = this
show ?thesis
proof (cases "y⇩1 = ⊖ y⇩2")
case True
with True' Point Point'
show ?thesis
next
case False
from ‹on_curve a b p⇩1› Point' True'
have "x⇩2 ∈ carrier R" "y⇩1 ∈ carrier R" and
on_curve1: "y⇩1 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
from False True' Point Point' assms
have "y⇩1 ≠ 𝟬"
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 (field on_curve1)
done
qed
next
case False
from ‹on_curve a b p⇩1› Point'
have  "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R"
and on_curve1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b"
from ‹on_curve a b p⇩2› Point
have "x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R"
and on_curve2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
from assms not_sym [OF False] show ?thesis
apply (field on_curve1 on_curve2)
done
qed
next
case Infinity
with Point ‹on_curve a b p⇩1› show ?thesis
qed
next
case Infinity
with ‹on_curve a b p⇩2› show ?thesis
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: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹
p⇩2 = add a p⇩1 p⇩1 ⟹ y⇩1 ≠ 𝟬 ⟹
l = («3» ⊗ x⇩1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ y⇩1) ⟹
x⇩2 = l [^] (2::nat) ⊖ «2» ⊗ x⇩1 ⟹
y⇩2 = ⊖ y⇩1 ⊖ l ⊗ (x⇩2 ⊖ x⇩1) ⟹
P p⇩1 p⇩1 p⇩2"
and R5: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹ p⇩3 = Point x⇩3 y⇩3 ⟹
p⇩3 = add a p⇩1 p⇩2 ⟹ x⇩1 ≠ x⇩2 ⟹
l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1) ⟹
x⇩3 = l [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2 ⟹
y⇩3 = ⊖ y⇩1 ⊖ l ⊗ (x⇩3 ⊖ x⇩1) ⟹
P p⇩1 p⇩2 p⇩3"
shows "P p q (add a p q)"
proof (cases p)
case Infinity
then show ?thesis
next
case (Point x⇩1 y⇩1)
note Point' = this
with p have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R"
and p': "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b"
show ?thesis
proof (cases q)
case Infinity
with Point show ?thesis
next
case (Point x⇩2 y⇩2)
with q have "x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R"
and q': "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
note True' = this
show ?thesis
proof (cases "y⇩1 = ⊖ y⇩2")
case True
with p Point Point' True' R3 [of p] ‹y⇩2 ∈ carrier R› show ?thesis
next
case False
have "(y⇩1 ⊖ y⇩2) ⊗ (y⇩1 ⊕ y⇩2) = 𝟬"
by (ring True' p' q')
with False ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R› have "y⇩1 = y⇩2"
with False True' Point Point' show ?thesis
apply simp
apply (rule R4)
done
qed
next
case False
with Point Point' show ?thesis
apply -
apply (rule R5)
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: "⋀p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l.
p⇩1 = Point x⇩1 y⇩1 ⟹ p⇩2 = Point x⇩2 y⇩2 ⟹ p⇩3 = Point x⇩3 y⇩3 ⟹
p⇩3 = add a p⇩1 p⇩2 ⟹ p⇩1 ≠ opp p⇩2 ⟹
x⇩1 = x⇩2 ∧ y⇩1 = y⇩2 ∧ l = («3» ⊗ x⇩1 [^] (2::nat) ⊕ a) ⊘ («2» ⊗ y⇩1) ∨
x⇩1 ≠ x⇩2 ∧ l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1) ⟹
x⇩3 = l [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2 ⟹
y⇩3 = ⊖ y⇩1 ⊖ l ⊗ (x⇩3 ⊖ x⇩1) ⟹
P p⇩1 p⇩2 p⇩3"
shows "P p q (add a p q)"
using a b p q p q
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
then show ?case
apply (rule_tac R4)
apply assumption+
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 p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_generic p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_generic p⇩1 (add a p⇩2 p⇩3)"
using a b p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with a b ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩3 x⇩3 y⇩3 p⇩5 x⇩5 y⇩5 l⇩1)
from a b ‹on_curve a b p⇩2› ‹on_curve a b p⇩3› ‹p⇩5 = add a p⇩2 p⇩3›
with a b ‹on_curve a b p⇩1› show ?case using Gen [simplified ‹p⇩2 = Point x⇩2' y⇩2'›]
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 p⇩1 x⇩1' y⇩1' p⇩5' x⇩5' y⇩5' p⇩6 x⇩6 y⇩6 l⇩2)
from a b ‹on_curve a b p⇩1› ‹on_curve a b (Point x⇩2' y⇩2')›
‹p⇩4 = add a p⇩1 (Point x⇩2' y⇩2')›
with a b show ?case using ‹on_curve a b p⇩3› Gen
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 p⇩4' x⇩4' y⇩4' p⇩3' x⇩3' y⇩3' p⇩7 x⇩7 y⇩7 l⇩3)
from ‹p⇩4' = Point x⇩4' y⇩4'› ‹p⇩4' = Point x⇩4 y⇩4›
have p⇩4: "x⇩4' = x⇩4" "y⇩4' = y⇩4" by simp_all
from ‹p⇩3' = Point x⇩3' y⇩3'› ‹p⇩3' = Point x⇩3 y⇩3›
have p⇩3: "x⇩3' = x⇩3" "y⇩3' = y⇩3" by simp_all
from ‹p⇩1 = Point x⇩1' y⇩1'› ‹p⇩1 = Point x⇩1 y⇩1›
have p⇩1: "x⇩1' = x⇩1" "y⇩1' = y⇩1" by simp_all
from ‹p⇩5' = Point x⇩5' y⇩5'› ‹p⇩5' = Point x⇩5 y⇩5›
have p⇩5: "x⇩5' = x⇩5" "y⇩5' = y⇩5" by simp_all
from ‹Point x⇩2' y⇩2' = Point x⇩2 y⇩2›
have p⇩2: "x⇩2' = x⇩2" "y⇩2' = y⇩2" by simp_all
note ps = p⇩1 p⇩2 p⇩3 p⇩4 p⇩5
from
‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
‹on_curve a b p⇩3› ‹p⇩3 = Point x⇩3 y⇩3›
have
"x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" and y1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b" and
"x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R" and y2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b" and
"x⇩3 ∈ carrier R" "y⇩3 ∈ carrier R" and y3: "y⇩3 [^] (2::nat) = x⇩3 [^] (3::nat) ⊕ a ⊗ x⇩3 ⊕ b"
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps
‹x⇩6 = l⇩2 [^] 2 ⊖ x⇩1' ⊖ x⇩5'› ‹x⇩7 = l⇩3 [^] 2 ⊖ x⇩4' ⊖ x⇩3'›
‹y⇩6 = ⊖ y⇩1' ⊖ l⇩2 ⊗ (x⇩6 ⊖ x⇩1')› ‹y⇩7 = ⊖ y⇩4' ⊖ l⇩3 ⊗ (x⇩7 ⊖ x⇩4')›
‹l⇩2 = (y⇩5' ⊖ y⇩1') ⊘ (x⇩5' ⊖ x⇩1')› ‹l⇩3 = (y⇩3' ⊖ y⇩4') ⊘ (x⇩3' ⊖ x⇩4')›
‹l⇩1 = (y⇩3 ⊖ y⇩2') ⊘ (x⇩3 ⊖ x⇩2')› ‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›
‹x⇩5 = l⇩1 [^] 2 ⊖ x⇩2' ⊖ x⇩3› ‹y⇩5 = ⊖ y⇩2' ⊖ l⇩1 ⊗ (x⇩5 ⊖ x⇩2')›
‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2› ‹y⇩4 = ⊖ y⇩1 ⊖ l ⊗ (x⇩4 ⊖ x⇩1)›)
apply (rule conjI)
apply (field y1 y2 y3)
apply (rule conjI)
apply (simp add: eq_diff0 ‹x⇩3 ∈ carrier R› ‹x⇩2 ∈ carrier R›
not_sym [OF ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›]])
apply (rule conjI)
apply (rule notI)
apply (ring (prems) y1 y2)
apply (cut_tac ‹x⇩1' ≠ x⇩5'› [simplified ‹x⇩5' = x⇩5› ‹x⇩1' = x⇩1› ‹x⇩5 = l⇩1 [^] 2 ⊖ x⇩2' ⊖ x⇩3›
‹l⇩1 = (y⇩3 ⊖ y⇩2') ⊘ (x⇩3 ⊖ x⇩2')› ‹y⇩2' = y⇩2› ‹x⇩2' = x⇩2›])
apply (erule notE)
apply (rule sym)
apply (field y1 y2)
apply (simp add: eq_diff0 ‹x⇩3 ∈ carrier R› ‹x⇩2 ∈ carrier R›
not_sym [OF ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›]])
apply (rule conjI)
apply (simp add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (cut_tac ‹x⇩4' ≠ x⇩3'› [simplified ‹x⇩4' = x⇩4› ‹x⇩3' = x⇩3› ‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›])
apply (erule notE)
apply (rule sym)
apply (field y1 y2)
apply (simp add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
apply (field y1 y2 y3)
apply (rule conjI)
apply (rule notI)
apply (ring (prems) y1 y2)
apply (cut_tac ‹x⇩1' ≠ x⇩5'› [simplified ‹x⇩5' = x⇩5› ‹x⇩1' = x⇩1› ‹x⇩5 = l⇩1 [^] 2 ⊖ x⇩2' ⊖ x⇩3›
‹l⇩1 = (y⇩3 ⊖ y⇩2') ⊘ (x⇩3 ⊖ x⇩2')› ‹y⇩2' = y⇩2› ‹x⇩2' = x⇩2›])
apply (erule notE)
apply (rule sym)
apply (field y1 y2)
apply (simp add: eq_diff0 ‹x⇩3 ∈ carrier R› ‹x⇩2 ∈ carrier R›
not_sym [OF ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›]])
apply (rule conjI)
apply (simp add: eq_diff0 ‹x⇩3 ∈ carrier R› ‹x⇩2 ∈ carrier R›
not_sym [OF ‹x⇩2' ≠ x⇩3› [simplified ‹x⇩2' = x⇩2›]])
apply (rule conjI)
apply (rule notI)
apply (ring (prems) y1 y2)
apply (cut_tac ‹x⇩4' ≠ x⇩3'› [simplified ‹x⇩4' = x⇩4› ‹x⇩3' = x⇩3› ‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›])
apply (erule notE)
apply (rule sym)
apply (field y1 y2)
apply (simp_all add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
done
qed
qed
qed
qed

lemma spec2_assoc:
assumes a: "a ∈ carrier R"
and b: "b ∈ carrier R"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_tangent p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_generic p⇩1 (add a p⇩2 p⇩3)"
using a b p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with a b ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩5 x⇩5 y⇩5 l⇩1)
from a b ‹on_curve a b p⇩2› ‹p⇩5 = add a p⇩2 p⇩2›
with a b ‹on_curve a b p⇩1› show ?case using Tan
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 p⇩1 x⇩1' y⇩1' p⇩5' x⇩5' y⇩5' p⇩6 x⇩6 y⇩6 l⇩2)
from a b ‹on_curve a b p⇩1› ‹on_curve a b p⇩2› ‹p⇩4 = add a p⇩1 p⇩2›
with a b show ?case using ‹on_curve a b p⇩2› Gen
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 p⇩4' x⇩4' y⇩4' p⇩3' x⇩3' y⇩3' p⇩7 x⇩7 y⇩7 l⇩3)
from
‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
have
"x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" and y1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b" and
"x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R" and y2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
from
‹p⇩5' = Point x⇩5' y⇩5'›
‹p⇩5' = Point x⇩5 y⇩5›
‹p⇩4' = Point x⇩4' y⇩4'›
‹p⇩4' = Point x⇩4 y⇩4›
‹p⇩3' = Point x⇩2' y⇩2'›
‹p⇩3' = Point x⇩2 y⇩2›
‹p⇩3' = Point x⇩3' y⇩3'›
‹p⇩1 = Point x⇩1' y⇩1'›
‹p⇩1 = Point x⇩1 y⇩1›
have ps:
"x⇩5' = x⇩5" "y⇩5' = y⇩5"
"x⇩4' = x⇩4" "y⇩4' = y⇩4" "x⇩3' = x⇩2" "y⇩3' = y⇩2" "x⇩2' = x⇩2" "y⇩2' = y⇩2"
"x⇩1' = x⇩1" "y⇩1' = y⇩1"
by simp_all
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps
‹x⇩7 = l⇩3 [^] 2 ⊖ x⇩4' ⊖ x⇩3'›
‹y⇩7 = ⊖ y⇩4' ⊖ l⇩3 ⊗ (x⇩7 ⊖ x⇩4')›
‹l⇩3 = (y⇩3' ⊖ y⇩4') ⊘ (x⇩3' ⊖ x⇩4')›
‹x⇩6 = l⇩2 [^] 2 ⊖ x⇩1' ⊖ x⇩5'›
‹y⇩6 = ⊖ y⇩1' ⊖ l⇩2 ⊗ (x⇩6 ⊖ x⇩1')›
‹l⇩2 = (y⇩5' ⊖ y⇩1') ⊘ (x⇩5' ⊖ x⇩1')›
‹x⇩5 = l⇩1 [^] 2 ⊖ «2» ⊗ x⇩2'›
‹y⇩5 = ⊖ y⇩2' ⊖ l⇩1 ⊗ (x⇩5 ⊖ x⇩2')›
‹l⇩1 = («3» ⊗ x⇩2' [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩2')›
‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹y⇩4 = ⊖ y⇩1 ⊖ l ⊗ (x⇩4 ⊖ x⇩1)›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›)
apply (rule conjI)
apply (field y1 y2)
apply (intro conjI)
apply (simp add: integral_iff [OF _ ‹y⇩2 ∈ carrier R›] ‹y⇩2' ≠ 𝟬› [simplified ‹y⇩2' = y⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩1' ≠ x⇩5'› [simplified
‹x⇩5 = l⇩1 [^] 2 ⊖ «2» ⊗ x⇩2'›
‹l⇩1 = («3» ⊗ x⇩2' [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩2')›
‹x⇩1' = x⇩1› ‹x⇩2' = x⇩2› ‹y⇩2' = y⇩2› ‹x⇩5' = x⇩5›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: integral_iff [OF _ ‹y⇩2 ∈ carrier R›] ‹y⇩2' ≠ 𝟬› [simplified ‹y⇩2' = y⇩2›])
apply (simp add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩4' ≠ x⇩3'› [simplified
‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›
‹x⇩4' = x⇩4› ‹x⇩3' = x⇩2›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
apply (field y1 y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩1' ≠ x⇩5'› [simplified
‹x⇩5 = l⇩1 [^] 2 ⊖ «2» ⊗ x⇩2'›
‹l⇩1 = («3» ⊗ x⇩2' [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩2')›
‹x⇩1' = x⇩1› ‹x⇩2' = x⇩2› ‹y⇩2' = y⇩2› ‹x⇩5' = x⇩5›]])
apply (rule sym)
apply (field y1 y2)
apply (simp add: integral_iff [OF _ ‹y⇩2 ∈ carrier R›] ‹y⇩2' ≠ 𝟬› [simplified ‹y⇩2' = y⇩2›])
apply (simp add: integral_iff [OF _ ‹y⇩2 ∈ carrier R›] ‹y⇩2' ≠ 𝟬› [simplified ‹y⇩2' = y⇩2›])
apply (rule notI)
apply (ring (prems) y1 y2)
apply (rule notE [OF ‹x⇩4' ≠ x⇩3'› [simplified
‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›
‹x⇩4' = x⇩4› ‹x⇩3' = x⇩2›]])
apply (rule sym)
apply (field y1 y2)
apply (simp_all add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
done
qed
qed
next
case (Gen p⇩3 x⇩3 y⇩3 p⇩5 x⇩5 y⇩5 p⇩6 x⇩6 y⇩6 l⇩1)
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 p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and p⇩3: "on_curve a b p⇩3"
and "is_generic p⇩1 p⇩2"
and "is_tangent p⇩2 p⇩3"
and "is_generic (add a p⇩1 p⇩2) p⇩3"
and "is_tangent p⇩1 (add a p⇩2 p⇩3)"
using a b p⇩1 p⇩2 assms
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩4 x⇩4 y⇩4 l)
with a b ‹on_curve a b p⇩2› ‹on_curve a b p⇩3›
show ?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 p⇩2 x⇩2' y⇩2' p⇩5 x⇩5 y⇩5 l⇩1)
from a b ‹on_curve a b p⇩2› ‹p⇩5 = add a p⇩2 p⇩2›
with a b ‹on_curve a b p⇩1› show ?case using Tan
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 p⇩1 x⇩1' y⇩1' p⇩6 x⇩6 y⇩6 l⇩2)
from a b ‹on_curve a b p⇩1› ‹on_curve a b p⇩2› ‹p⇩4 = add a p⇩1 p⇩2›
with a b show ?case using ‹on_curve a b p⇩2› Tan
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 p⇩4' x⇩4' y⇩4' p⇩2' x⇩2'' y⇩2'' p⇩7 x⇩7 y⇩7 l⇩3)
from
‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
‹on_curve a b p⇩2› ‹p⇩2 = Point x⇩2 y⇩2›
have
"x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" and y1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b" and
"x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R" and y2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
from
‹p⇩4' = Point x⇩4' y⇩4'›
‹p⇩4' = Point x⇩4 y⇩4›
‹p⇩2' = Point x⇩2' y⇩2'›
‹p⇩2' = Point x⇩2 y⇩2›
‹p⇩2' = Point x⇩2'' y⇩2''›
‹p⇩1 = Point x⇩1' y⇩1'›
‹p⇩1 = Point x⇩1 y⇩1›
‹p⇩1 = Point x⇩5 y⇩5›
have ps:
"x⇩4' = x⇩4" "y⇩4' = y⇩4" "x⇩2' = x⇩2" "y⇩2' = y⇩2" "x⇩2'' = x⇩2" "y⇩2'' = y⇩2"
"x⇩1' = x⇩5" "y⇩1' = y⇩5" "x⇩1 = x⇩5" "y⇩1 = y⇩5"
by simp_all
note qs =
‹x⇩7 = l⇩3 [^] 2 ⊖ x⇩4' ⊖ x⇩2''›
‹y⇩7 = ⊖ y⇩4' ⊖ l⇩3 ⊗ (x⇩7 ⊖ x⇩4')›
‹l⇩3 = (y⇩2'' ⊖ y⇩4') ⊘ (x⇩2'' ⊖ x⇩4')›
‹x⇩6 = l⇩2 [^] 2 ⊖ «2» ⊗ x⇩1'›
‹y⇩6 = ⊖ y⇩1' ⊖ l⇩2 ⊗ (x⇩6 ⊖ x⇩1')›
‹x⇩5 = l⇩1 [^] 2 ⊖ «2» ⊗ x⇩2'›
‹y⇩5 = ⊖ y⇩2' ⊖ l⇩1 ⊗ (x⇩5 ⊖ x⇩2')›
‹l⇩1 = («3» ⊗ x⇩2' [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩2')›
‹l⇩2 = («3» ⊗ x⇩1' [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩1')›
‹x⇩4 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2›
‹y⇩4 = ⊖ y⇩1 ⊖ l ⊗ (x⇩4 ⊖ x⇩1)›
‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›
from ‹y⇩2 ∈ carrier R› ‹y⇩2' ≠ 𝟬› ‹y⇩2' = y⇩2›
have "«2» ⊗ y⇩2 ≠ 𝟬" by (simp add: integral_iff)
show ?case
apply (simp add: ‹p⇩6 = Point x⇩6 y⇩6› ‹p⇩7 = Point x⇩7 y⇩7›)
apply (simp only: ps qs)
apply (rule conjI)
apply (field y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹y⇩1' ≠ 𝟬›])
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩4' ≠ x⇩2''›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (intro conjI)
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (erule thin_rl)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (field y2)
apply (intro conjI)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹y⇩1' ≠ 𝟬›])
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩4' ≠ x⇩2''›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (erule thin_rl)
apply (rule conjI)
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
apply (rule notI)
apply (ring (prems))
apply (rule notE [OF ‹x⇩1 ≠ x⇩2›])
apply (rule sym)
apply (simp only: ps qs)
apply field
apply (rule ‹«2» ⊗ y⇩2 ≠ 𝟬›)
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_opp: "on_curve a b p ⟹ add a p (opp p) = Infinity"

assumes "a ∈ carrier R" "b ∈ carrier R" "on_curve a b p⇩1" "on_curve a b p⇩2"
proof (cases p⇩1)
case Infinity
next
case (Point x⇩1 y⇩1)
note Point' = this
with ‹on_curve a b p⇩1›
have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R"
and y1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b"
show ?thesis
proof (cases p⇩2)
case Infinity
next
case (Point x⇩2 y⇩2)
with ‹on_curve a b p⇩2› have "x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R"
and y2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
show ?thesis
proof (cases "x⇩1 = x⇩2")
case True
show ?thesis
proof (cases "y⇩1 = ⊖ y⇩2")
case True
with Point Point' ‹x⇩1 = x⇩2› ‹y⇩2 ∈ carrier R› show ?thesis
next
case False
with y1 y2 [symmetric] ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R› ‹x⇩1 = x⇩2› Point Point'
show ?thesis
qed
next
case False
with Point Point' show ?thesis
apply (rule conjI)
apply field
apply (cut_tac ‹x⇩1 ∈ carrier R› ‹x⇩2 ∈ carrier R›)
apply field
apply (cut_tac ‹x⇩1 ∈ carrier R› ‹x⇩2 ∈ carrier R›)
done
qed
qed
qed

lemma uniq_opp:
assumes "on_curve a b p⇩2"
and "add a p⇩1 p⇩2 = Infinity"
shows "p⇩2 = opp p⇩1"
using assms
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 p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
shows "p⇩1 = Infinity"
using a b p⇩1 p⇩2 assms
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
from ‹on_curve a b p⇩1› ‹p⇩1 = Point x⇩1 y⇩1›
have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" by (simp_all add: on_curve_def)
with a ‹l = («3» ⊗ x⇩1 [^] 2 ⊕ a) ⊘ («2» ⊗ y⇩1)› ‹y⇩1 ≠ 𝟬›
have "l ∈ carrier R" by (simp add: integral_iff)
from ‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩2 = p⇩1›
have "x⇩2 = x⇩1" "y⇩2 = y⇩1" by simp_all
with ‹x⇩1 ∈ carrier R› ‹y⇩1 ∈ carrier R› ‹l ∈ carrier R› ‹y⇩2 = ⊖ y⇩1 ⊖ l ⊗ (x⇩2 ⊖ x⇩1)› ‹y⇩1 ≠ 𝟬›
have "⊖ y⇩1 = y⇩1" by (simp add: r_neg minus_eq)
with ‹y⇩1 ∈ carrier R› ‹y⇩1 ≠ 𝟬›
show ?case by (simp add: neg_equal_zero)
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
then have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" "x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R"
and y1: "y⇩1 [^] (2::nat) = x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b"
and y2: "y⇩2 [^] (2::nat) = x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b"
with ‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)› ‹x⇩1 ≠ x⇩2›
have "l ∈ carrier R" by (simp add: eq_diff0)
from ‹p⇩3 = p⇩2› ‹p⇩2 = Point x⇩2 y⇩2› ‹p⇩3 = Point x⇩3 y⇩3›
have ps: "x⇩3 = x⇩2" "y⇩3 = y⇩2" by simp_all
with ‹y⇩3 = ⊖ y⇩1 ⊖ l ⊗ (x⇩3 ⊖ x⇩1)›
have "y⇩2 = ⊖ y⇩1 ⊖ l ⊗ (x⇩2 ⊖ x⇩1)" by simp
also from ‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)› ‹x⇩1 ≠ x⇩2›
‹x⇩1 ∈ carrier R› ‹x⇩2 ∈ carrier R› ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R›
have "l ⊗ (x⇩2 ⊖ x⇩1) = y⇩2 ⊖ y⇩1"
by (simp add: m_div_def m_assoc eq_diff0)
also from ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R›
have "⊖ y⇩1 ⊖ (y⇩2 ⊖ y⇩1) = (⊖ y⇩1 ⊕ y⇩1) ⊕ ⊖ y⇩2"
finally have "y⇩2 = 𝟬" using ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R›
with ‹p⇩2 = Point x⇩2 y⇩2› ‹on_curve a b p⇩2›
‹a ∈ carrier R› ‹b ∈ carrier R› ‹x⇩2 ∈ carrier R›
have x2: "x⇩2 [^] (3::nat) = ⊖ (a ⊗ x⇩2 ⊕ b)"
from ‹x⇩3 = l [^] 2 ⊖ x⇩1 ⊖ x⇩2› ‹x⇩3 = x⇩2›
have "l [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2 ⊖ x⇩2 = x⇩2 ⊖ x⇩2" by simp
with ‹x⇩1 ∈ carrier R› ‹x⇩2 ∈ carrier R› ‹l ∈ carrier R›
have "l [^] (2::nat) ⊖ x⇩1 ⊖ «2» ⊗ x⇩2 = 𝟬"
then have "x⇩2 ⊗ (l [^] (2::nat) ⊖ x⇩1 ⊖ «2» ⊗ x⇩2) = x⇩2 ⊗ 𝟬" by simp
then have "(x⇩2 ⊖ x⇩1) ⊗ («2» ⊗ a ⊗ x⇩2 ⊕ «3» ⊗ b) = 𝟬"
apply (simp add: ‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)› ‹y⇩2 = 𝟬›)
apply (field (prems) y1 x2)
apply (ring y1 x2)
apply (simp add: eq_diff0 ‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› not_sym [OF ‹x⇩1 ≠ x⇩2›])
done
with not_sym [OF ‹x⇩1 ≠ x⇩2›]
‹x⇩2 ∈ carrier R› ‹x⇩1 ∈ carrier R› ‹a ∈ carrier R› ‹b ∈ carrier R›
have "«2» ⊗ a ⊗ x⇩2 ⊕ «3» ⊗ b = 𝟬"
with ‹a ∈ carrier R› ‹b ∈ carrier R› ‹x⇩2 ∈ carrier R›
have "«2» ⊗ a ⊗ x⇩2 = ⊖ («3» ⊗ b)"
from y2 [symmetric] ‹y⇩2 = 𝟬› ‹a ∈ carrier R›
have "⊖ («2» ⊗ a) [^] (3::nat) ⊗ (x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b) = 𝟬"
then have "b ⊗ («4» ⊗ a [^] (3::nat) ⊕ «27» ⊗ b [^] (2::nat)) = 𝟬"
apply (ring (prems) ‹«2» ⊗ a ⊗ x⇩2 = ⊖ («3» ⊗ b)›)
apply (ring ‹«2» ⊗ a ⊗ x⇩2 = ⊖ («3» ⊗ b)›)
done
with ab a b have "b = 𝟬" by (simp add: nonsingular_def integral_iff)
with ‹«2» ⊗ a ⊗ x⇩2 ⊕ «3» ⊗ b = 𝟬› ab a b ‹x⇩2 ∈ carrier R›
have "x⇩2 = 𝟬" by (simp add: nonsingular_def nat_pow_zero integral_iff)
from ‹l [^] (2::nat) ⊖ x⇩1 ⊖ «2» ⊗ x⇩2 = 𝟬›
show ?case
apply (simp add: ‹x⇩2 = 𝟬› ‹y⇩2 = 𝟬› ‹l = (y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)›)
apply (field (prems) y1 ‹b = 𝟬›)
apply (insert a b ab ‹x⇩1 ∈ carrier R› ‹b = 𝟬› ‹x⇩1 ≠ x⇩2› ‹x⇩2 = 𝟬›)
apply (simp add: nonsingular_def nat_pow_zero integral_iff)
done
qed

assumes a: "a ∈ carrier R"
and b: "b ∈ carrier R"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
shows "opp (add a p⇩1 p⇩2) = add a (opp p⇩1) (opp p⇩2)"
proof (cases p⇩1)
case Infinity
next
case (Point x⇩1 y⇩1)
show ?thesis
proof (cases p⇩2)
case Infinity
with ‹p⇩1 = Point x⇩1 y⇩1› show ?thesis
next
case (Point x⇩2 y⇩2)
with ‹p⇩1 = Point x⇩1 y⇩1› p⇩1 p⇩2
have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" "x⇩1 [^] (3::nat) ⊕ a ⊗ x⇩1 ⊕ b = y⇩1 [^] (2::nat)"
"x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R" "x⇩2 [^] (3::nat) ⊕ a ⊗ x⇩2 ⊕ b = y⇩2 [^] (2::nat)"
with Point ‹p⇩1 = Point x⇩1 y⇩1› show ?thesis
apply (cases "x⇩1 = x⇩2")
apply (cases "y⇩1 = ⊖ y⇩2")
apply (rule conjI)
apply field
apply (auto simp add: integral_iff nat_pow_zero
apply field
apply (auto simp add: integral_iff nat_pow_zero
apply (rule conjI)
apply field
apply field
done
qed
qed

assumes a: "a ∈ carrier R"
and b: "b ∈ carrier R"
and p⇩1: "on_curve a b p⇩1"
and p⇩2: "on_curve a b p⇩2"
and "p⇩1 ≠ opp p⇩1"
shows "p⇩2 = opp p⇩2"
using a b p⇩1 p⇩2 assms
case InfL
next
case InfR
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 p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 l)
then have "add a p⇩1 p⇩1 = Infinity"
with ‹on_curve a b p⇩1› have "p⇩1 = opp p⇩1" by (rule uniq_opp)
with ‹p⇩1 ≠ opp p⇩1› show ?case ..
next
case (Gen p⇩1 x⇩1 y⇩1 p⇩2 x⇩2 y⇩2 p⇩3 x⇩3 y⇩3 l)
then have "x⇩1 ∈ carrier R" "y⇩1 ∈ carrier R" "x⇩2 ∈ carrier R" "y⇩2 ∈ carrier R"
have "«2» ⊗ «2» ≠ 𝟬"
then have "«4» ≠ 𝟬" by (simp add: of_int_mult [symmetric])
from Gen have "((⊖ y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)) [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2 =
((y⇩2 ⊖ y⇩1) ⊘ (x⇩2 ⊖ x⇩1)) [^] (2::nat) ⊖ x⇩1 ⊖ x⇩2"
then show ?case
apply (field (prems))
apply (insert ‹y⇩1 ∈ carrier R› ‹y⇩2 ∈ carrier R› ‹p⇩1 ≠ opp p⇩1›
‹p⇩1 = Point x⇩1 y⇩1› ‹p⇩2 = Point x⇩2 y⇩2› ‹«4» ≠ 𝟬›)[1]
apply (insert ‹x⇩1 ∈ carrier R› ‹x⇩2 ∈ carrier R› ‹x⇩1 ≠ x⇩2›)
done
qed

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"
using a b add_closed [OF a b p p] opp_closed [OF p] assms
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›