表示具有粘合条件的集合

Question

我正在尝试在 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"

到目前为止，我被教导如何进行条件定义，并建议对{0,1}中的值使用位类型。这是第三个表示问题。假定以下定义：

 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）：

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)

我应该如何在 Isabelle 中表示这个集合？我的想法是，这应该是一个由一个或两个元素组成的等价类的商集。但是，我如何限制上述功能以处理这些等价物类?

编辑

这个等价关系是用一个or条件组合起来的，使其自反。

Answer 1

这是我所采用的方法的草图：

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

我按照 .

的答案

表示具有粘合条件的集合

Representing a set with gluing conditions

isabelle