用胶合条件表示集合

我试图用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"

 definition "e_aff = {(x,y). e' x y = 0}" 
 definition "e_circ = {(x,y). x ≠ 0 ∧ y ≠ 0 ∧ (x,y) ∈ e_aff}"

投影椭圆曲线由(见第12、13页)定义 here 对于原件):

=(P,i+1)

我该如何在伊莎贝尔身上表现这一套?我的想法是,这应该是一个商集,等价类由一个或两个元素组成。但是如何限制上面的函数在这些等价类上工作呢?