CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2600

Shorten proposition with abbreviations in Isabelle

Imagine the following theorem:

 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)"

I would like to eliminate the second assumption, without having to substitute the value of p on each occurrence. I did this in proofs with the let command:

let ?p = lagrange_interpolation_poly zs_ws

But it doesn't work in the theorem statement. Ideas?

Upvotes: 1

Views: 207

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

You can make a local definition in the lemma statement like this:

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)"

The definition gets unfolded when the proof is finished. So when you look at thm l later, all occurrences of p have been substituted by the right-hand side. Inside the proof, p_def refers to the definining equation for p (what you call e). The defines clause is most useful when you want to control in the proof when Isabelle's proof tools just see p and when they see the expanded right-hand side.

Upvotes: 2

Related Questions