특정 속성이있는 목록의 모든 요소를 ​​제거하려면 어떻게해야합니까?

Question

내가 일치 l :: 'a list에 이러한 요소를 제거 할

는 그 술어 P :: ('a => bool)

이러한 작업을 수행하는 가장 좋은 방법은 무엇입니까 일치? 나에게 도움이 될 수있는 기존 기능에 대해 어떻게 알 수 있습니까?

Answer 1

짧은 이야기 : 사용 find_consts

긴 이야기 :

이것은 어떻게에 이러한 문제를 정복.

는 Main에서, 그것은 단지 처음부터 제거, 그러나 List.dropWhile

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

있다. 의도 한 기능이 아닐 수도 있습니다. 우리는

그러나 라이브러리를 검색 모든 항목

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))" 

을 제거하는 함수 자신을 작성할 수 있습니다

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

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

수동 접근 방식은,이 기능과 필터링에 해당 ¬ 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

예상되는 기능을 찾는 한 가지 방법은 Isabelle 설명서의 What's in Main 문서입니다. Isabelle/HOL의 Main 이론에 의해 제공되는 주요 유형, 기능 및 구문에 대한 간략한 개요를 제공합니다.

ths 문서의 목록 섹션을 보면 올바른 유형 인 것으로 보이는 filter 함수를 찾을 수 있습니다.