在 Isabelle 中用缩写缩短命题

Question

想象以下定理：

 assumes d: "distinct (map fst zs_ws)"
 assumes e: "(p :: complex poly) = lagrange_interpolation_poly zs_ws"
 shows "degree p ≤ (length zs_ws)-1 ∧
         (∀ x y. (x,y) ∈ set zs_ws ⟶ poly p x = y)"

我想消除第二个假设，而不必在每次出现时都替换 p 的值。我用 let 命令在校样中做了这个：

let ?p = lagrange_interpolation_poly zs_ws

但是在定理语句中不起作用。想法？

Answer 1

你可以像这样在引理语句中进行局部定义：

lemma l:
  fixes zs_ws
  defines "p == lagrange_interpolation_poly zs_ws"
  assumes d: "distinct (map fst zs_ws)"
  shows "degree p ≤ (length zs_ws)-1 ∧ (∀(x,y) ∈ set zs_ws. poly p x = y)"

证明完成后展开定义。因此，当您稍后查看 thm l 时，所有出现的 p 都已被右侧替换。在证明中，p_def 指的是 p 的定义方程（你称之为 e）。当 Isabelle 的证明工具只看到 p 并且他们看到扩展的右侧时，当您想要控制证明时，defines 子句最有用。

在 Isabelle 中用缩写缩短命题

Shorten proposition with abbreviations in Isabelle

isabelle