修复 Isabelle 中特征不同于 2 的字段

Question

我为椭圆曲线做了一个 proof，以实数为基场。

现在我想通过一个具有不同于 2 的特性的任意场来改变实数，以便从等式 2x = 0 可以推导出 x = 0。

像 Isabelle 这样的校对助手怎么说这个？

Answer 1

本质上，你可以使用

class ell_field = field +
  assumes zero_ne_two: "2 ≠ 0"

例如，参见 The Group Law for Elliptic Curves by Stefan Berghofer。

我假设您希望使用对象逻辑 HOL 主库中的 class field。不幸的是，我不知道上述库中对环特征的一般处理（希望，如果确实存在，有人会为我们指出）。因此，我设计了自己的定义框架来为这个答案提供一个上下文：

context semiring_1
begin

definition characteristic :: "'a itself ⇒ nat" where
  "characteristic a = 
    (if (∃n. n ≥ 1 ∧ of_nat n = 0) 
    then (LEAST n. n ≥ 1 ∧ of_nat n = 0) 
    else 0)"

end

class ell_field = field +
  assumes zero_ne_two: "2 ≠ 0"
begin

lemma x2: "2 * x = 0 ⟹ x = 0"
  by (simp add: zero_ne_two)

lemma "characteristic TYPE('a) ≠ 2"
proof(rule ccontr, simp)
  assume c2: "characteristic TYPE('a) = 2"
  define P where "P = (λn. (n ≥ 1 ∧ of_nat n = 0))" 
  from c2 have ex: "∃n. P n" 
    unfolding P_def characteristic_def by presburger
  with c2 have least_2: "(LEAST n. P n) = 2"
    unfolding characteristic_def P_def by auto
  from LeastI2_ex[OF ex, of P] have "P (LEAST n. P n)" by simp
  then have "2 = 0" unfolding least_2 unfolding P_def by simp
  with zero_ne_two show False by simp
qed

end

修复 Isabelle 中特征不同于 2 的字段

Fix a field with characteristic different from 2 in Isabelle

isabelle