l :: 'a list
述語に一致する要素を一致させて削除したいP :: ('a => bool)
そのようなタスクを達成するための最良の方法は何ですか?役立つ可能性のある既存の機能をどのように見つけることができますか?
l :: 'a list
述語に一致する要素を一致させて削除したいP :: ('a => bool)
そのようなタスクを達成するための最良の方法は何ですか?役立つ可能性のある既存の機能をどのように見つけることができますか?
短編小説:使用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
存在すると予想される関数を見つける1つの方法は、Isabelleドキュメントの「What'sinMain」ドキュメントです。Main
Isabelle / HOLの理論によって提供される主なタイプ、関数、および構文の概要を簡単に説明します。
このドキュメントのリストセクションを見るとfilter
、正しいタイプのように見える関数が見つかります。