Рассмотрим следующие определения в Изабель:
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]))
В нотации указано, как один элемент группы действует напредставитель класса.
Как я могу формализовать это в Изабель?
Вот связанный вопрос: Уточнение определения в Изабель
Издесь полный код: https://github.com/rjraya/Isabelle/blob/master/curves/Hales.thy
Первый вопрос: как трактовать симметрии как тип, поскольку они зависят от фиксированной переменной d.