如何删除某个属性列表中的所有元素？

Question

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

完成此类任务的最佳方式是什么？我如何才能了解可能对我有帮助的现有功能？

Answer 1

短篇小说：使用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" 

它从主返回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 

Answer 2

一个办法，找出你所期望存在的功能是从伊莎贝尔文档文件What's in Main。它简要概述了Isabelle/HOL的理论Main提供的主要类型，功能和语法。

如果您查看该文档中的列表部分，您会发现功能似乎具有正确类型的功能filter。