Сократить предложение с аббревиатурами в Изабель

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). Предложение defines наиболее полезно, когда вы хотите контролировать в доказательстве, когда средства проверки Изабель просто видят p и когда они видят развернутую правую часть.