如何刪除某個屬性列表中的所有元素？

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。