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

但它在定理陈述中不起作用。想法？

标签： isabelle

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）的定义方程。defines当您想控制 Isabelle 的证明工具何时看到p以及何时看到扩展的右侧时，该子句最有用。