定义等价函数类 Isabelle

Question

考虑 Isabelle 中的以下定义：

definition "e_aff = {(x, y). e' x y = 0}"
definition "e_circ = {(x,y). x ≠ 0 ∧ y ≠ 0 ∧ (x,y) ∈ e_aff}"
definition gluing :: "(((real × real) × bit) × ((real × real) × bit)) set" where
  "gluing = {(((x0,y0),l),((x1,y1),j)). 
               ((x0,y0) ∈ e_aff ∧ (x1,y1) ∈ e_aff) ∧
               (((x0,y0) ∈ e_circ ∧ (x1,y1) = τ (x0,y0) ∧ j = l+1) ∨
                ((x0,y0) ∈ e_aff ∧ x0 = x1 ∧ y0 = y1 ∧ l = j))}"
definition "Bits = range Bit"
definition e_aff_bit :: "((real × real) × bit) set" where
 "e_aff_bit = e_aff × Bits"
definition e_proj where "e_proj = e_aff_bit // gluing"

fun ρ :: "real × real ⇒ real × real" where 
  "ρ (x,y) = (-y,x)"
fun τ :: "real × real ⇒ real × real" where 
  "τ (x,y) = (1/(t*x),1/(t*y))"
definition symmetries where 
  "symmetries = {τ,τ ∘ ρ,τ ∘ ρ ∘ ρ,τ ∘ ρ ∘ ρ ∘ ρ}"

我想定义对称群对基础椭圆曲线投影点的作用。动作指定如下：

τ [P,i] = [P,i+1]
ρ [P,i] = [ρ (P),i]

其余对称性的作用可以从规则推导出来：

s1 ∘ s2 [P,i] = s2 (s1 [P,i]))

该符号指定群中的一个元素如何作用于 class 的代表。

如何在 Isabelle 中将其正式化？

这是一个相关问题：

这里是完整代码：https://github.com/rjraya/Isabelle/blob/master/curves/Hales.thy

第一个问题是如何将对称性视为一种类型，因为它们依赖于固定变量 d。

Answer 1

解决方案的一个合理选择可能是使用归纳谓词。下面的定义只是一个template/idea：我还没有验证它确实是你试图获得的定义。

inductive φ where
    "φ τ s (the_elem ({(P, i + 1) | P i. (P, i) ∈ s } // gluing))"
    if "s ∈ E" 
  | "φ ρ s (the_elem ({(ρ P, i) | P i. (P, i) ∈ s } // gluing))"
    if "s ∈ E" 
  | "φ (g1 ∘ g2) s s''" 
    if "g1 ∈ G" and "g2 ∈ G" and "s ∈ E" and "φ g1 s s'" and "φ g2 s' s''"

definition Φ where 
  "Φ g s = (if g ∈ G ∧ s ∈ E then (THE s'. φ g s s') else {})"

附带说明一下，也可以使用 function 基础结构而不是归纳谓词。

定义等价函数类 Isabelle

Defining function over equivalence classes Isabelle

isabelle

定义等价函数 类 Isabelle

Defining function over equivalence classes Isabelle

isabelle

定义等价函数类 Isabelle