添加后收集所有非未定义的值

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 ∧ (x1,y1) ∈ e_aff ∧ (x2,y2) ∈ e_aff"
| "proj_add ((x1,y1),l) ((x2,y2),j) = ((ext_add (x1,y1) (x2,y2)), l+j)" 
    if "delta' x1 y1 x2 y2 ≠ 0 ∧ (x1,y1) ∈ e_aff ∧ (x2,y2) ∈ e_aff"
| "proj_add ((x1,y1),l) ((x2,y2),j) = undefined"
    if "delta x1 y1 x2 y2 = 0 ∧ delta' x1 y1 x2 y2 = 0 ∨ (x1,y1) ∉ e_aff ∨ (x2,y2) ∉ e_aff"
  apply(fast,fastforce)
  using coherence e_aff_def by auto

现在，我想提取所有定义的值来模拟类上的加法，而不是特定值：

function proj_add_class :: "((real × real) × bit) set ⇒ ((real × real) × bit) set ⇒ ((real × real) × bit) set"  where
"proj_add_class c1 c2 = 
  (⋃ cr ∈ c1 × c2.  proj_add cr.fst cr.snd)"

以上只是一个模板。显然，我无法从 cr 中获取第一个元素，因此出现错误。另一方面，如何删除未定义的值？

有关完整理论，请参阅 here。

Answer 1

背景

在对形式化所依据的文章有了一定程度的了解后，我决定更新答案。原始答案可通过修订历史获得：我相信原始答案中陈述的所有内容都是明智的，但从阐述风格的角度来看，可能不如修订后的答案最佳。

简介

我根据自己对与 4033cbf288 相关的形式化草案的一部分所做的修改，使用了稍微更新的符号。已导入以下理论：Complex_Main "HOL-Algebra.Group" "HOL-Algebra.Bij" 和 "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

定义二

我在没有证明的情况下使用 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

proj_add_class

我还为 proj_add_class 的陈述提供了我认为是自然的解决方案（同样，使用 function 基础设施），并表明它与 at 中使用的定义一致感兴趣领域的时刻。

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

结论

选择合适的定义是一个主观问题。因此，我只能表达我个人的看法，认为什么是最合适的选择。

添加后收集所有非未定义的值

Gather all non-undefined values after addition

isabelle