問題タブ [isabelle]

n各単項式の指数が より小さいか等しい場合、単項式の和の次数は常に より小さいか等しいことを示す補題に取り組んでいnます。

これまでのところ、次のことを行う必要があります (Isabelle の初心者であることに注意してください)。

ここに問題があります。次の補題が証明を完了するのに十分でない理由がわかりません。特に、最後の部分 (申し訳ありませんが) は、大槌が証明を見つけるのに十分なほど単純であると思います。

.
Brian Huffman の優れた回答からの解決策:
.

有限集合から 1 つの要素を選択する関数について推論したいと思います。

特定の関数がそのような「選択」関数であるかどうかを示す述語を定義しようとしました。

実際には、要素を選択したい有限集合は具象型ですが、'aの代わりに具象型を配置すると、同じ問題が発生します。

も省略しようとしましfinite Aたが、扱っている集合は有限であり、ここでは選択公理について考えたくありません。

現在、この定義は矛盾しているようです。

どうすればchooser合理的な方法で定義できますか? 次のように使用したいと思います。

ほとんどの場合、どのように選択するかではなく、セットのメンバーを選択することが重要です。

背景: オークションのタイブレーカーを形式化したいと考えています (このペーパーのセクション 4 )。オークションにかけられているアイテムに 2 つの最高入札額があると仮定すると、オークションに勝つべき 1 人の入札者を任意に選択する必要があります。

これは、ところで、本当に最小限の例です（これは少し理解しにくいです）：

Isabelle を使ったプロジェクトに取り組んでいます。

何らかの理由で、次のようにビット/バイト システムをシミュレートする必要があります。

(BTTTTTTTT) を使用して (11111111) を表し、(BFFFFFFFF) を使用して (00000000) を表します。

しかし、そのような明白な補題を証明することはできません: b != b + 1

私は本当に助けが必要です。

以下が機能するのはなぜですか：

しかし、これは失敗します

と

同様に、以下は成功します。

しかし、これは失敗します

と

と呼ばれる関数がありword_rsplitます~~/src/HOL/Word/Word.thy。

32 wordaを fourに分割したいのですが8 word、この機能は完璧のようです。

そしてレンマword_rcat (word_rsplit w) = wは私にとっても役に立ちます。

なので、 の使い方、 = 32 と= 8のword_rsplit指定方法を知る必要があります。'a'b

私はvimのファンですが、この Isabelle/HOL 環境を備えているのはemacsだけです。jEditは素晴らしいですが、私は使用できません

emacsのように。

jEditで「トレース」を有効にする方法は?

私はFOL.thyquantifierを増補しようとしMOSTています。これは、単純多数派として定義するつもりです。つまり、

ファイルの変更方法がわかりませんFOL.thy。の下axiomatizationに、次を追加することを考えました:

そして、where句の下に：

ここで、「...」は、上で概説した制約を表現する適切な方法P(x)です~P(x)。（繰り返しますが、ここで良い名前がわかりませんでした。提案は大歓迎です。）

「シンボル」セクションにエントリを追加することを考えましたが、より良いアイデアがないため、デルタを使用することにしました。

notationセクションでも同様です。

1)カーディナリティ制約を適切に表現するにはどうすればよいですか?

2) 他に何を変更する必要がありますか?

後者の質問に対しては、最終的には、「Most」と「All」を使用した定量化された主張を含む前提を前提として、多くの異なる結論が必要か、可能か、不可能かを評価したいということを指摘しておくと役立つかもしれません (接続詞、選言など）。