I'm trying to represent projective elliptic curve addition in Isabelle:
function proj_add :: "(real × real) × bit ⇒ (real × real) × bit ⇒ (real × real) × bit" where
"proj_add ((x1,y1),l) ((x2,y2),j) = ((add (x1,y1) (x2,y2)), l+j)"
if "delta x1 y1 x2 y2 ≠ 0"
| "proj_add ((x1,y1),l) ((x2,y2),j) = ((ext_add (x1,y1) (x2,y2)), l+j)"
if "delta' x1 y1 x2 y2 ≠ 0"
so far, I was taught how to do conditional definition and suggested to use the bit type for values in {0,1}. Here is a third representation problem. Assume the following definitions:
definition "e_aff = {(x,y). e' x y = 0}"
definition "e_circ = {(x,y). x ≠ 0 ∧ y ≠ 0 ∧ (x,y) ∈ e_aff}"
A projective elliptic curve is defined by (see pages 12, 13 here for the original):
taking two copies of e_aff glued along e_circ with isomorphism τ. We write (P,i) ∈ E with i ∈ {0,1} for the image of P ∈ e_aff in E using th ith copy of e_aff. The gluing condition gives for P ∈ e_circ, (P,i) = (τ P,i+1)
How should I represent this set in Isabelle? My idea is that this should be a quotient set with equivalence classes made of one or two elements. But then how do i restrict the above function to work on these equivalence classes?
Edit
The equivalence relation is obtained by composing this relation with an or condition making it reflexive.
Here is a sketch of the approach I followed:
definition "proj_add_class c1 c2 =
(((case_prod (λ x y. the (proj_add x y))) `
(Map.dom (case_prod proj_add) ∩ (c1 × c2)))
// gluing)"
definition "proj_addition c1 c2 = the_elem(proj_add_class c1 c2)"
where I follow the answer to Gather all non-undefined values after addition.