isabelle - 如何删除具有特定属性的列表中的所有元素？

Question

我想匹配并删除与l :: 'a list谓词匹配的那些元素P :: ('a => bool)

完成此类任务的最佳方法是什么？如何找到可能对我有帮助的现有功能？

Answer 1

查找您期望存在的函数的一种方法是 Isabelle 文档中的文档What's in Main。它简要概述了MainIsabelle/HOL 理论提供的主要类型、功能和语法。

如果您查看文档中的 List 部分，您会发现该函数filter似乎具有正确的类型。

Answer 2

短篇小说：使用find_consts

很长的故事：

这是克服此类问题的方法。

中Main，有List.dropWhile

List.dropWhile :: "('a => bool) => 'a list => 'a list"

但是，它只会从一开始就删除。这可能不是预期的功能。

value "List.dropWhile (λ x. x = ''c'') [''c'', ''c'', ''d'']"
"[''d'']"

value "List.dropWhile (λ x. x = ''c'') [''d'', ''c'', ''c'']"
"[''d'', ''c'', ''c'']"

手动方法

我们可以自己编写一个函数来删除所有出现的事件

fun dropAll :: "('a => bool) => 'a list => 'a list" where
    "dropAll P [] = []"
  | "dropAll P (x # xs) = (if P x then dropAll P xs else x # (dropAll P xs))"

搜索图书馆

但是，此功能相当于过滤¬ P

我们怎样才能找到这样的库函数？

如果我们知道我们想要做什么的签名，我们可以使用find_consts

find_consts "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"

它从 Main 返回 3 个具有该签名的函数：List.dropWhile, List.filter,List.takeWhile

现在，让我们证明我们不需要dropAll但可以对filter.

lemma "dropAll P l = filter (λ x. ¬ P x) l"
  apply(induction l)
  by simp_all

建议不要实现像dropAll你自己这样的东西，而是使用过滤器。因此，所有被证明的引理filter都是可用的。

提示

提示：我们可以使用方便的列表理解语法来编写过滤器表达式

lemma "filter (λ x. ¬ P x) l = [x ← l. ¬ P x]" by simp