1

l :: 'a list述語に一致する要素を一致させて削除したいP :: ('a => bool)

そのようなタスクを達成するための最良の方法は何ですか?役立つ可能性のある既存の機能をどのように見つけることができますか?

4

2 に答える 2

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"

Mainから3つの関数を返し、そのシグネチャは次のとおりです。List.dropWhile、、List.filterList.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 
于 2013-03-08T11:40:39.990 に答える
1

存在すると予想される関数を見つける1つの方法は、Isabelleドキュメントの「What'sinMain」ドキュメントですMainIsabelle / HOLの理論によって提供される主なタイプ、関数、および構文の概要を簡単に説明します。

このドキュメントのリストセクションを見るとfilter、正しいタイプのように見える関数が見つかります。

于 2013-03-08T12:22:51.157 に答える