背景
对形式化所依据的文章有了一定程度的理解后,我决定更新答案。原始答案可以通过修订历史记录获得:我相信原始答案中陈述的所有内容都是合理的,但从阐述风格的角度来看,可能不如修订后的答案最佳。
介绍
我根据自己对与 4033cbf288 相关的形式化草案的一部分的修订,使用了稍微更新的符号。引进了以下理论:Complex_Main
"HOL-Algebra.Group"
"HOL-Algebra.Bij"
and "HOL-Library.Bit"
定义一
首先,我重申一些相关定义,以确保答案是独立的:
locale curve_addition =
fixes c d :: real
begin
definition e :: "real ⇒ real ⇒ real"
where "e x y = x⇧2 + c*y⇧2 - 1 - d*x⇧2*y⇧2"
fun add :: "real × real ⇒ real × real ⇒ real × real" (infix ‹⊕⇩E› 65)
where
"(x1, y1) ⊕⇩E (x2, y2) =
(
(x1*x2 - c*y1*y2) div (1 - d*x1*y1*x2*y2),
(x1*y2 + y1*x2) div (1 + d*x1*y1*x2*y2)
)"
definition delta_plus :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩y›)
where "δ⇩y x1 y1 x2 y2 = 1 + d*x1*y1*x2*y2"
definition delta_minus :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩x›)
where "δ⇩x x1 y1 x2 y2 = 1 - d*x1*y1*x2*y2"
definition delta :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩E›)
where "δ⇩E x1 y1 x2 y2 = (δ⇩x x1 y1 x2 y2) * (δ⇩y x1 y1 x2 y2)"
end
locale ext_curve_addition = curve_addition +
fixes c' d' t
assumes c'_eq_1[simp]: "c' = 1"
assumes d'_neq_0[simp]: "d' ≠ 0"
assumes c_def: "c = c'⇧2"
assumes d_def: "d = d'⇧2"
assumes t_sq_def: "t⇧2 = d/c"
assumes t_sq_n1: "t⇧2 ≠ 1"
begin
fun add0 :: "real × real ⇒ real × real ⇒ real × real" (infix ‹⊕⇩0› 65)
where "(x1, y1) ⊕⇩0 (x2, y2) = (x1, y1/sqrt(c)) ⊕⇩E (x2, y2/sqrt(c))"
definition delta_plus_0 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩0⇩y›)
where "δ⇩0⇩y x1 y1 x2 y2 = δ⇩y x1 (y1/sqrt(c)) x2 (y2/sqrt(c))"
definition delta_minus_0 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩0⇩x›)
where "δ⇩0⇩x x1 y1 x2 y2 = δ⇩x x1 (y1/sqrt(c)) x2 (y2/sqrt(c))"
definition delta_0 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩0›)
where "δ⇩0 x1 y1 x2 y2 = (δ⇩0⇩x x1 y1 x2 y2) * (δ⇩0⇩y x1 y1 x2 y2)"
definition delta_plus_1 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩1⇩y›)
where "δ⇩1⇩y x1 y1 x2 y2 = x1*x2 + y1*y2"
definition delta_minus_1 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩1⇩x›)
where "δ⇩1⇩x x1 y1 x2 y2 = x2*y1 - x1*y2"
definition delta_1 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" (‹δ⇩1›)
where "δ⇩1 x1 y1 x2 y2 = (δ⇩1⇩x x1 y1 x2 y2) * (δ⇩1⇩y x1 y1 x2 y2)"
fun ρ :: "real × real ⇒ real × real"
where "ρ (x, y) = (-y, x)"
fun τ :: "real × real ⇒ real × real"
where "τ (x, y) = (1/(t*x), 1/(t*y))"
fun add1 :: "real × real ⇒ real × real ⇒ real × real" (infix ‹⊕⇩1› 65)
where
"(x1, y1) ⊕⇩1 (x2, y2) =
(
(x1*y1 - x2*y2) div (x2*y1 - x1*y2),
(x1*y1 + x2*y2) div (x1*x2 + y1*y2)
)"
definition e' :: "real ⇒ real ⇒ real"
where "e' x y = x⇧2 + y⇧2 - 1 - t⇧2*x⇧2*y⇧2"
end
locale projective_curve = ext_curve_addition
begin
definition "E⇩a⇩f⇩f = {(x, y). e' x y = 0}"
definition "E⇩O = {(x, y). x ≠ 0 ∧ y ≠ 0 ∧ (x, y) ∈ E⇩a⇩f⇩f}"
definition G where
"G ≡ {id, ρ, ρ ∘ ρ, ρ ∘ ρ ∘ ρ, τ, τ ∘ ρ, τ ∘ ρ ∘ ρ, τ ∘ ρ ∘ ρ ∘ ρ}"
definition symmetries where
"symmetries = {τ, τ ∘ ρ, τ ∘ ρ ∘ ρ, τ ∘ ρ ∘ ρ ∘ ρ}"
definition rotations where
"rotations = {id, ρ, ρ ∘ ρ, ρ ∘ ρ ∘ ρ}"
definition E⇩a⇩f⇩f⇩0 where
"E⇩a⇩f⇩f⇩0 =
{
((x1, y1), (x2, y2)).
(x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f ∧ δ⇩0 x1 y1 x2 y2 ≠ 0
}"
definition E⇩a⇩f⇩f⇩1 where
"E⇩a⇩f⇩f⇩1 =
{
((x1, y1), (x2, y2)).
(x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f ∧ δ⇩1 x1 y1 x2 y2 ≠ 0
}"
end
定义二
I use coherence
没有证明,但在将定理的陈述复制到这个答案之前,我已将存储库中的证明移植到我的符号中,即证明确实存在,但它不是答案的一部分。
context projective_curve
begin
type_synonym repEPCT = ‹((real × real) × bit)›
type_synonym EPCT = ‹repEPCT set›
definition gluing :: "(repEPCT × repEPCT) set"
where
"gluing =
{
(((x0, y0), l), ((x1, y1), j)).
((x0, y0) ∈ E⇩a⇩f⇩f ∧ (x1, y1) ∈ E⇩a⇩f⇩f) ∧
(
((x0, y0) ∈ E⇩O ∧ (x1, y1) = τ (x0, y0) ∧ j = l + 1) ∨
(x0 = x1 ∧ y0 = y1 ∧ l = j)
)
}"
definition E where "E = (E⇩a⇩f⇩f × UNIV) // gluing"
lemma coherence:
assumes "δ⇩0 x1 y1 x2 y2 ≠ 0" "δ⇩1 x1 y1 x2 y2 ≠ 0"
assumes "e' x1 y1 = 0" "e' x2 y2 = 0"
shows "(x1, y1) ⊕⇩1 (x2, y2) = (x1, y1) ⊕⇩0 (x2, y2)"
sorry
end
proj_add
的定义proj_add
除了添加的选项之外,与原始问题中的几乎相同domintros
(如果没有域定理,几乎不可能陈述任何有意义的内容)。我还表明它相当于当前使用的简单定义。
context projective_curve
begin
function (domintros) proj_add :: "repEPCT ⇒ repEPCT ⇒ repEPCT"
(infix ‹⊙› 65)
where
"((x1, y1), i) ⊙ ((x2, y2), j) = ((x1, y1) ⊕⇩0 (x2, y2), i + j)"
if "(x1, y1) ∈ E⇩a⇩f⇩f" and "(x2, y2) ∈ E⇩a⇩f⇩f" and "δ⇩0 x1 y1 x2 y2 ≠ 0"
| "((x1, y1), i) ⊙ ((x2, y2), j) = ((x1, y1) ⊕⇩1 (x2, y2), i + j)"
if "(x1, y1) ∈ E⇩a⇩f⇩f" and "(x2, y2) ∈ E⇩a⇩f⇩f" and "δ⇩1 x1 y1 x2 y2 ≠ 0"
| "((x1, y1), i) ⊙ ((x2, y2), j) = undefined"
if "(x1, y1) ∉ E⇩a⇩f⇩f ∨ (x2, y2) ∉ E⇩a⇩f⇩f ∨
(δ⇩0 x1 y1 x2 y2 = 0 ∧ δ⇩1 x1 y1 x2 y2 = 0)"
subgoal by (metis τ.cases surj_pair)
subgoal by auto
subgoal unfolding E⇩a⇩f⇩f_def using coherence by auto
by auto
termination proj_add using "termination" by blast
lemma proj_add_pred_undefined:
assumes "¬ ((x1, y1), (x2, y2)) ∈ E⇩a⇩f⇩f⇩0 ∪ E⇩a⇩f⇩f⇩1"
shows "((x1, y1), l) ⊙ ((x2, y2), j) = undefined"
using assms unfolding E⇩a⇩f⇩f⇩0_def E⇩a⇩f⇩f⇩1_def
by (auto simp: proj_add.domintros(3) proj_add.psimps(3))
lemma proj_add_def:
"(proj_add ((x1, y1), i) ((x2, y2), j)) =
(
if ((x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f ∧ δ⇩0 x1 y1 x2 y2 ≠ 0)
then ((x1, y1) ⊕⇩0 (x2, y2), i + j)
else
(
if ((x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f ∧ δ⇩1 x1 y1 x2 y2 ≠ 0)
then ((x1, y1) ⊕⇩1 (x2, y2), i + j)
else undefined
)
)"
(is "?lhs = ?rhs")
proof(cases ‹δ⇩0 x1 y1 x2 y2 ≠ 0 ∧ (x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f›)
case True
then have True_exp: "(x1, y1) ∈ E⇩a⇩f⇩f" "(x2, y2) ∈ E⇩a⇩f⇩f" "δ⇩0 x1 y1 x2 y2 ≠ 0"
by auto
then have rhs: "?rhs = ((x1, y1) ⊕⇩0 (x2, y2), i + j)" by simp
show ?thesis unfolding proj_add.simps(1)[OF True_exp, of i j] rhs ..
next
case n0: False show ?thesis
proof(cases ‹δ⇩1 x1 y1 x2 y2 ≠ 0 ∧ (x1, y1) ∈ E⇩a⇩f⇩f ∧ (x2, y2) ∈ E⇩a⇩f⇩f›)
case True show ?thesis
proof-
from True n0 have False_exp:
"(x1, y1) ∈ E⇩a⇩f⇩f" "(x2, y2) ∈ E⇩a⇩f⇩f" "δ⇩1 x1 y1 x2 y2 ≠ 0"
by auto
with n0 have rhs: "?rhs = ((x1, y1) ⊕⇩1 (x2, y2), i + j)" by auto
show ?thesis unfolding proj_add.simps(2)[OF False_exp, of i j] rhs ..
qed
next
case False then show ?thesis using n0 proj_add.simps(3) by auto
qed
qed
end
项目添加类
我还提供了我认为是自然的解决方案(再次,使用function
基础设施)的声明proj_add_class
并表明它与目前在感兴趣的领域使用的定义一致。
context projective_curve
begin
function (domintros) proj_add_class :: "EPCT ⇒ EPCT ⇒ EPCT" (infix ‹⨀› 65)
where
"A ⨀ B =
the_elem
(
{
((x1, y1), i) ⊙ ((x2, y2), j) | x1 y1 i x2 y2 j.
((x1, y1), i) ∈ A ∧ ((x2, y2), j) ∈ B ∧
((x1, y1), (x2, y2)) ∈ E⇩a⇩f⇩f⇩0 ∪ E⇩a⇩f⇩f⇩1
} // gluing
)"
if "A ∈ E" and "B ∈ E"
| "A ⨀ B = undefined" if "A ∉ E ∨ B ∉ E"
by (meson surj_pair) auto
termination proj_add_class using "termination" by auto
definition proj_add_class' (infix ‹⨀''› 65) where
"proj_add_class' c1 c2 =
the_elem
(
(case_prod (⊙) `
({(x, y). x ∈ c1 ∧ y ∈ c2 ∧ (fst x, fst y) ∈ E⇩a⇩f⇩f⇩0 ∪ E⇩a⇩f⇩f⇩1})) // gluing
)"
lemma proj_add_class_eq:
assumes "A ∈ E" and "B ∈ E"
shows "A ⨀' B = A ⨀ B"
proof-
have
"(λ(x, y). x ⊙ y) `
{(x, y). x ∈ A ∧ y ∈ B ∧ (fst x, fst y) ∈ E⇩a⇩f⇩f⇩0 ∪ E⇩a⇩f⇩f⇩1} =
{
((x1, y1), i) ⊙ ((x2, y2), j) | x1 y1 i x2 y2 j.
((x1, y1), i) ∈ A ∧ ((x2, y2), j) ∈ B ∧ ((x1, y1), x2, y2) ∈ E⇩a⇩f⇩f⇩0 ∪ E⇩a⇩f⇩f⇩1
}"
apply (standard; standard)
subgoal unfolding image_def by clarsimp blast
subgoal unfolding image_def by clarsimp blast
done
then show ?thesis
unfolding proj_add_class'_def proj_add_class.simps(1)[OF assms]
by auto
qed
end
结论
定义的适当选择是一个主观问题。因此,我只能表达我个人认为最合适的选择。