isabelle

2熱

1答えて

私は含んでゴールにSIMP法を適用AN場合、表現、整理が自動的に大文字小文字の区別を導入した場合： lemma "undefined (if x then True else False)" apply simp この目標を与える： (x ⟶ undefined True) ∧ (¬ x ⟶ undefined False) 私の質問はどのようになっていますか？私は単純化ルールを

1熱

1答えて

イザベルのMLプログラミング：組み込みの関数と戦術の一部を見つけることができませんでした

私はIsabelleにMLコードを書くために "Isabelle Cookbook"を研究しています。残念ながら、組み込み関数が見つかりませんでした（名前が変更され、パスのstructure.fctを指定する必要があります）ので、多くの例は機能しません。たとえば、etac,rtacおよびatacを使用する例は、もはや動作しません。新しい名前は何ですか？私は自分でそれらを見つける方法を教えてくだ

0熱

2答えて

Isabelle/jEditで集合理論の記号を入力するにはどうすればよいですか？

Isabelle/jEditに∈、⊆、∪、∩などの記号を入力するにはどうすればよいですか？ Isabelle/HOLチュートリアルでは、「：」、「< =」、「Un」、「Int」と入力する必要があります。ただし、 "< ="は≤を返し、他はシンボルにまったく変換されません。これまでのところ、\ <に>という文字を入力するか、その接頭辞を付けてマウスで目的のシンボルを選択しています。しかし、私はキー

1熱

2答えて

AFPの `find_theorems`

find_theoremsメカニズムを使用して、正式証明書（AFP）のアーカイブ全体を検索するにはどうすればよいですか？アーカイブを自分のマシンにダウンロードしました。そこから理論をインポートできます。たとえば、私がimports Kleene_Algebra.Kleene_Algebra_Modelsと書くと、その理論の定理はすべて私に利用可能になります。しかし、find_theorems <

0熱

1答えて

Isabelleでルール誘導と変数一般化を組み合わせるにはどうすればよいですか？

イザベルでは、arbitraryキーワードを使用して、誘導プルーフの変数を一般化できます。これは間違いなく普通の誘導のために働きます。apply (induction n arbitrary: m)のように。私はapply (induction rule: R.induct)のようにルールの誘導をすることもできます。しかし、ルール誘導を使用するときに、どのように変数を一般化できますか？私の特定の

0熱

1答えて

Isabelle/Isarに複数の変数を使って存在命題を効率的に証明するにはどうすればよいですか？

Isabelle/Isarに補題∃ n m k . [n, m, k] = [2, 3, 5]を証明したいとします。 45ページのイザベル/ HOLチュートリアルで提案されているように、私は先に行く場合は、次のように、私の証明はなりますもちろん lemma "∃ n m k . [n, m, k] = [2, 3, 5]" proof show "∃ m k . [2, m, k] =

0熱

1答えて

"4.6 Isabelle/HOLのプログラミングと証明"のエクササイズ4.6で補題を証明するにはどうしたらいいですか？

私は "プログラミングとIsabelle/HOLの検証"でエクササイズ4.6を解決しようとしています。リストを集合に変換する関数elems :: "'a list ⇒ 'a set"を定義し、補助詞"x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"を証明するよう求めます。これまでのところ、私は遠くに来ました： fun elems :

0熱

1答えて

Isabelleタイプのエラー

私はIsabelleを初めて勉強して、Exercise for Universityをやっています。私はイザベルで逆関数を証明する必要があります。 Haskellでは関数は次のようになります。私は今、イザベルでこの機能「REV」を定義するためにしようと試み rev [] = [] rev (x:xs) = rev xs ++ [x] 。タイプリストと機能「アプリ」（追加）エラーイザベルは私

0熱

1答えて

Isabelleで任意の記号の否定版を使用できますか？

Isabelleでは、他のシンボルのバージョンを無効にしたシンボルを使用することができます。例は≠と∉です。 LaTeXの\notマクロのような、任意のシンボルのネガティブバージョンを取得するメカニズムはありますか？

1熱

2答えて

イザベルで誘導的に定義された関係の非再帰性をどのように証明できますか？

はイザベルの例として、自然数の不平等の次の定義を考えてみましょう： inductive unequal :: "nat ⇒ nat ⇒ bool" where zero_suc: "unequal 0 (Suc _)" | suc_zero: "unequal (Suc _) 0" | suc_suc: "unequal n m ⟹ unequal (Suc n) (