Search code examples
listsumisabelle

Do I need to save Isabelle files to import them?

I want to import the ListSum theory which, in turn, depends on the ListAux, EfficientNat, and Main theory files.

However, I was unable to import these so I tried copying and saving ListSum but it depends on ListAux and that seems to use an outdated style/syntax (at least the version I found on google).

In the end, I just want to do something like

n = \sum_{i =1..m} (List!i)*i

First, what files do I actually need to sum over a list and do I need to save them locally? I successfully imported the HOL.Groups_List and HOL.Factorial (theories?) without needing to download these locally... why? But when I try to add ListSum to the "imports" line it throws an error.

Secondly, how do I write the above summation in Isabelle?

Solution

  • The ListSum theory is part of the entry Flyspeck I: Tame Graphs in the Isabelle AFP (see isa-afp.org/entries/Flyspeck-Tame.html) and seems to be an internal theory which basically contains the special construct ∑⇘x ∈ xs⇙ f for summation over lists plus associated properties.

    Regarding the second part of your question: In Isabelle, your summation is written as ∑i ∈ {1..m}. List ! i * i. You don't need to import anything special for this.