合計内の if ステートメントに問題があります。

isabelle の if ステートメントに関する別の質問で解決策を確認しました が、役に立ちませんでした。

次に例を示します。

「申し訳ありません」がどこにある補題をどのように証明できますか?

*行列の場合と**A * 1 andA ** mat 1`の違いは何ですか?

例：

simpメソッドがタプルをコンポーネントに分割しないようにするにはどうすればよいですか?

例。私が書くなら

証明状態は良好です∃z. foo z。私がそれから書くなら

証明状態になり∃a aa ab ac b. blah (a, aa, ab, ac, b)ます。simpに展開fooされているのが好きですがblah、変数zをそのままにしておきたいと思います。

ここで、Isabelle メタ論理論理積消去規則の証明を求めます。

以下のソースには、私がやっていることを少し説明する私のコメントが含まれています。理論的には、メタ偽定義と接続詞消去規則のペアが 2 つあります。2 つのペアは次のとおりです。

• falseH、andH_E1、および
• falseM、andM_E1。

私のandM接続詞の形は(P ==> Q ==> falseM) ==> falseM)で、簡単に証明できないのはこの形です。

将来的には、上記と同様のメタ論理演算子を使用して、HOL.thy 自然演繹規則を複製する予定andMです。その一環として、オペレーター==>はプリミティブ オペレーターとして扱われます。Pure 演算子!!も と同じ意味でプリミティブであるため、以下で使用するように==>、メタ偽の定義 に役立つルールを開発できない可能性があると推測して!!P. PROP Pいます。でも、私は間違っているかもしれません。

HOL と組み合わせて既に機能している魔法を助長するfalseMため、以下で使用しようとしている必要があるわけではありません。しゃれは意図されていません。なくてもいいけど、あったらいいな。falseHsimp

更新 (131211)

私はこれを 3 つのことで更新します。そのうちの 2 つは、除外された中間の公理が必要であるという Andreas の回答に関連しています。以下で私が言うことは、実際には何に対する答えでもありません。単純なことで間違っている可能性があるため、より多くのコメントを受け付けています.

ここに長いコメントを入れて、私の質問の中心的なアイデアに関連するいくつかのアイデアを統合します。これは、メタロジック false を使用してメタロジック演算子を定義する方法です。

1. ロケールで除外された中間のメタロジック公理をどのように追加すると思うかを示します。
2. 排除中間の公理のどのような形式が必要かを理解するに至った理由を示します。ほとんどすべての文献は、除外されたミドルは であると言っていますがP or not P、これは欺瞞的です。
3. "(P &&& Q) ==> Pは で証明さconjunctionD1れconjunction.ML、展開されたバージョンは で証明されることに注意してくださいmeta_allE。なぜandMは!!外側ではなく内側にあるのに、証明できるように操作できないのだろうか。

メタロジック除外ミドルをロケールに配置する

Adreas は、Isabelle/Pure には除外されたミドルがなく、私にはそれが必要であることを指摘することで、何ヶ月、おそらく少なくとも 1 年、おそらく何年にもわたる無益な策略から私を救ってくれました。これは、私が持っていた関連する質問への回答に役立ち、Isabelle/Pure とは何かをより理解するのに役立ちました。

HOL 除外の中間を使用することが強制されている場合はFalse、 の代わりに , を使用し(!!P. P::bool)ます。

メタ偽が必要な場合は、次のようなロケールでメタロジック除外ミドルを追加すると思います。

私が言ったように、私はそれを解決しなければならないので、これは答えではありません.

Andreas が提供した証拠から、classicalHOL からのものがあります。

このような HOL 定理の証明手順は、メタロジック バージョンに必要なものを教えてくれます。locale axiom を提供することで簡単な部分を行いましたt_or_f。残りは単純な作業です。

Isabelle/Pure 除外されたミドルを持たない

ここでは、話すためだけに話すのではなく==、除外された中間の一部として必要であることを確認するために、私が取り組んだことを入れました。私はこれらすべてをもう一度見る必要があるかもしれないので、私に不利にならないかもしれません.

最初に、HOL レンマについて次に述べることに先んじて、ある人、特に私は、この公理、171 行 excluded_middle目についても考えたいと思うでしょう 。HOL.thy

Andreas は、排除された中間の法則が必要であり、Pure はそれを提供していないと指摘しています。これは、HOL.thyという名前の定理 excluded_middle、行 604 です。

同様に、これを を使用したメタ論理定理として述べますfalseM。ここで、メタオアは(P ==> falseM) ==> Qであり、メタノットは ですP ==> falseM。

メタオア表記が実際の内容を曖昧にするように定義されている場合、論理的な初心者 (もちろん私ではありません) は、これを、「P が false でない場合に必要なもの」ではなく、「P が false の場合、P は false である」と認識しない可能性があります。 、それなら真実に違いない」.

更新 (131213): これを入れたのは、自分が何かをした理由を忘れてしまう可能性があるためです。その後、ロジックを元に戻そうとすると、そうしなかったときに、かなりの時間を台無しにしてしまったと思います。完了しました。

のメタロジック バージョンを実際に実装したので~P | Pはなく、P | ~P. おそらくそれが明らかでない場合、私は真理値表に基づく含意の定義を DeMorgan の法則と共に使用し、論理の基本的な定理を使用しています。

しかし、私は現在、除外された中間の公理に関して後知恵で取り組んでいます。これにより、私が使用したという事実がP | ~Pあまり受け入れられなくなり"((P ==> falseM) ==> falseM) ==> P"ます. 今まで、私は自分の人生で排除された中間に関心を持つ必要があったことは一度もありませんでした. それは構成主義者が考えることになっているはずです。

=inの重要性を理解するきっかけになったので、切り替えを行ったのは実際には偶然ですTrue_or_False。

意味のある定理は、「not (P and not P)」です (またはそうなりますか?)。だから私はメタアンド式で 代用(P ==> falseM)します。Q(P ==> Q ==> falseM) ==> falseM

falseM 展開する必要がなかったため、これは完全な論理的愚か者の赤い警告になりました。ここで、同じ定理 を述べま​​すが、bool変数や を使用せずに、またはfalseMとは関係がないことを明確にします。falseMbool

最初に飛びついたことに戻りますが、主な違いは、 で演算子=が使用されていることTrue_or_Falseです。

True_or_Falseここで、演算子 を使用するメタ論理形式を==、 meta-or を として(P ==> falseM) ==> Q、真の部分を として(P == (falseM ==> falseM))、偽の部分をとして述べます(P == falseM)。

falseMこれにより、最終的に、拡張する必要がある除外された中間の意味のあるメタロジックステートメントが得られました。私はこれを証明することはできませんが、それ自体は何の意味もありません。

これは、私の最終目標が伝統的にこの種の知識を必要としない高レベルの数学であるのに、定理アシスタントを使用するために多くの低レベルのロジックを勉強しなければならない理由を示しています。

除外された中間がないことの重要性をよく理解していないと、とりわけ、私を殺してしまいました.

なぜ"(P &&& Q) ==> P"上で証明できるのですか？

上記の方法で(P &&& Q) ==> P証明できる重要性はまだあります。これは次のとおりです。linarithpresburger&&&pure_thy.ML

私の meta-and, usingfalseMは、実際には展開され!!た後、外側から内側への使用を移動するだけfalseMです。

ここでは、メタと消去の拡張項を証明し、拡張されていないバージョンを を使用して証明しPure.conjunctiond1ます。

ルールconjunctionD1は にあり、が と同じことをしていると思われる operator を処理してconjunction.MLいるように見えます。forall_elim_vars!!meta_allE

標準の Meta-And を使用できますが、Meta-And は目的ではありません

結合消去規則の 2 つの拡張バージョンを比較します。最初の項は standard&&&を使用し、2 番目の項は my を使用しますandM。

を使用すると、上に示したよう&&&に で簡単に第 1 項を証明できmeta_allEます。

私には、第 2 項を第 1 項の形に操作できるはずですが、わかりません。それが本当なら、この定理に排除中間の公理を追加する必要はありません。必要に応じて、自然演繹法をたくさん勉強すればわかります。

私の目標が単なるメタ論理演算子である場合、私は を使用します&&&が、それは私の目標ではありません。私の目標は、メタ論理演算子を省略するために使用するメタ偽を定義することです。HOL のすべてを複製するのではなく、Isabelle/Pure の自然な推論フレームワークを少し拡張しようとしています。

この質問から得た主な価値は、除外中間の公理の必要性に注意する必要があることを知っていることです。メタ偽が必要な場合は、除外された中間の公理が必要になるようです。

ここで私は出発します。助けてくれてありがとう、そして長い追加を許してください。

Isabelle の証明には 2 つのスタイルがあります。

ステートメント、および新しい「構造化された」Isar スタイル。私自身、どちらも役に立つと思います。「apply」スタイルはより簡潔なので、興味のない技術的な補題には便利ですが、「構造化」スタイルは主要な定理に便利です。

あるスタイルから別のスタイルに切り替えるのが好きな場合もあります。「適用」スタイルから「構造化」スタイルへの切り替えは簡単です。

私の適用チェーンで。私の質問は、「構造化」スタイルから「適用」スタイルに戻すにはどうすればよいですか?

より具体的な例を挙げると、5 つのサブゴールがあるとします。最初の 2 つのサブゴールをディスパッチするために、いくつかの「適用」命令を発行します。次に、構造化された証明を開始して、3 番目の証明を省きます。サブゴールが 2 つ残っています。これらのスタイルを「適用」するにはどうすればよいですか?

単純な帰納的に定義された集合について補題があるとしましょう:

(「⋀x y」ビットが残ることは私にとって重要です。補題は、長い適用チェーンの途中で私の証明の状態を実際に述べているからです。)

この補題の証明を開始するのに問題があります。ルール誘導で進めたいと思います。

最初の試み

書いてみた

しかし、それはうまくいきません:inductメソッドは失敗します。x次のように、y明示的に修正してからメソッドを呼び出すことで、これを回避できることがわかりましinductた。

ただし、実際には適用チェーンの途中なので、構造化された証明ブロックには入りたくありません。

2 回目の試行

代わりにメソッドを使用してみましinduct_tacたが、残念ながら、ルールを希望どおりにinduct_tac適用できません。foo.induct入力すると

最初のサブゴールは

qux x []これは私が望むものではありません:の代わりに欲しかったのですqux x y。このinduct方法はこれを正しく行いましたが、上記で説明した他の問題がありました。

私が理解しているように、イザベルの行列は本質的に関数であり、任意の次元です。この設定では、平方行列 ( n x n行列) を定義するのは簡単ではありません。また、紙の校正では、二乗の次元 "n" を校正に使用できます。しかし、イザベルでそれを行うにはどうすればよいですか?

ライプニッツ式:

紙の上の私の証拠：

これは、私の Isabelle 証明の関連する抜粋です。

この状況で何ができますか？

---

アップデート：

('a ^ 'n ^ 'n) の制限されたバージョンである C の型は、 > Polynomial.thy をインポートした後でも使用しようとするとエラーが発生するため、> あなたのカスタム型のようです。しかし、他のHOL理論で定義されている可能性があります。

残念ながら、私のコード例にはインクルードを書きませんでした。更新された例を参照してください。ただし、これはカスタム タイプではないため、"Polynomial.thy" と "Determinants" をインポートするだけで十分です。(Isabelle バージョン 2013-1 と 2013-2 をテストしました。)

マトリックスのカスタム定義を使用している場合、ほとんどの場合、自分で作成する可能性が高くなります。

マトリックスのカスタム定義を使用しているとは思いません。ライブラリDeterminants(~~/src/HOL/Multivariate_Analysis/Determinants) には、次の行列式の定義があります:
definition det:: "'a::comm_ring_1^'n^'n ⇒ 'a" where .... そのため、ライブラリは行列の概念をベクトルのベクトルとして使用します。私のリングが多項式を超えていても、私の目には違いはありません。

とにかく、('a ^ 'n ^ 'n) のような型の場合、行列のサイズの値を返す関数を記述できるはずです。したがって、(p ^ n ^ n) が行列で、n がセットの場合、n のカーディナリティは、質問で必要な n である可能性があります。

これは私を正しい道に導きました。私の現在の推測では、次の定義が役に立ちます。

cardで定義されていFinite_Setます。

Isabelle で次のデータ型を定義しました

次の基本補題を証明する方法がわかりません

仮定B≠Cの下で、証明は次のようになります。

BとCが異なるという明示的な仮定なしに補題を証明する方法はありますか?

更新:[simp] Manuel Eberl が回答へのコメントで示唆したように、単純化プロセスをループさせ、自動生成された単純化ルールを無視する誤った単純化規則 (属性を持つレンマ、ここでは省略) がB≠C問題の原因でしたC≠B(bs_t.simpsクリスが答えで指摘したように）。gc44 による回答のようsimpに、通常の状況で補題を証明するのに十分です。