Isabelle列表求和：依赖文件导入疑问与求和语法咨询

• 实现列表求和无需额外本地保存非标准文件，Isabelle的HOL标准库已提供完备工具。你能直接导入HOL.Groups_List和HOL.Factorial是因为它们属于Isabelle自带的标准库理论，默认处于Isabelle的搜索路径中，无需手动下载或本地存放。
• 导入ListSum报错的原因是：该理论并非Isabelle标准库的一部分，属于第三方或旧版本非官方理论，要么不在Isabelle默认搜索路径内，要么其依赖的ListAux使用的语法已被标准库淘汰，因此无法直接导入使用。

你需要的$\boldsymbol{n = \sum_{i=1..m} (List!i)*i}$操作，是对列表前m个1-based索引的元素，按“元素×索引”的规则累加求和，可通过Isabelle标准库的sum函数结合列表操作实现：

1. 先导入必要的标准库理论：

theory Weighted_Sum_Example
imports HOL.List HOL.Num
begin

2. 定义加权求和函数：
   由于Isabelle列表默认是0-based索引，要对应数学中的1-based索引，需将索引i转换为i-1来访问列表元素。通过sum函数遍历{1..m}的整数集合，计算每个项的累加：

definition list_weighted_sum :: "nat list ⇒ nat ⇒ nat" where
  "list_weighted_sum xs m = sum (λi. (xs ! (i - 1)) * i) {1..m}"

3. 逻辑验证：例如对列表[a, b, c]，调用list_weighted_sum [a,b,c] 3会得到1*a + 2*b + 3*c，完全匹配你的需求。

内容的提问来源于stack exchange，提问作者Squirtle