リストを数量化するための関数：構文と型のエラー（Isabelle）

Question

現在、「Quantifying Lists」エクササイズをhttp://isabelle.in.tum.de/exercises/から行っています。それは、「原始的な再帰を使用してリストに普遍的および実在的な量子を定義するように求めます。式{{term xs} ... '{term xs} ...のすべての要素{term "P x"}が{@ "term"}の要素に当てはまる場合、Expression @ {term "alls P xs"}は真でなければなりません。私には信じられる：

primrec alls :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where 
"alls P x # [] = (if P x then True else False)" 
| "alls P x # xs = (if P x then alls P xs else False)" 

私はのように私は数学的表記で表現だろうか書き込みしようとしています：

オールズ（P、[X]）= {Pxが、その後真の場合はそうでない場合はfalse

および

alls（P、[x、...]）= {Pxの場合はalls（P、[...]）そうでない場合はfalse。

しかし、Isabelleは、「統一にタイプエラーがあります」と示し、xがタイプ'a listであると仮定していることを示しています。私は文法を正しく表現していないと感じますが、どのように変えるべきかはわかりません。

Answer 1

x # fooを単一オペランドとして扱うには、かっこで囲む必要があります。(x # foo)。

これはストーリーの終わりではありません。上記の修正を適用すると、エラーが発生しますNonprimitive pattern in left-hand side at "alls P [x]" ...違反パターンは単一要素リストに一致するx # []です。

リストは2つのコンストラクタNilとConsを使用して定義されているとprimrecは（Cons x Nilのように見える）単一要素のリストを含む非プリミティブコンストラクタ、することができません。このエラーを回避するには、primrecをfunに置き換えることができますが、空のリストも処理するためには、関数全体を定義したい場合は問題が深刻です。関数はプリミティブコンストラクタNilとConsの両方のパターンを持っている必要があり、これを解決するには

：あなたが適切な値でそれを埋めることができるように

primrec alls :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where 
    "alls P [] = ..." 
| "alls P (x # xs) = (if P x then alls P xs else False)" 

一部...が意図的に不足しています。