問題タブ [isabelle]

Isabelleファイルからisabelle build -D xxxLaTeX ファイルを生成するために使用したいと考えています。しかし、Isabelle はすべての理論の依存関係をチェックし、すべての関連ファイルが含まれている必要があります。.tex.thy.thy

.thy構文エラーのあるファイルを何気なく使用してファイルを生成することは.texできますか? 実際、論文を書くにはその一部しか必要ありません。

私はこのCコードを持っています:

リストがどんなに長くても、このループが終わったら にp->next等しくNULL、EIP はこのループの次の命令を参照することを証明したいのです。

しかし、私はできません。Isabelle/HOLでループを証明する方法を知っている人はいますか?

私は図書館で働いていますHOL/Library/Polynomial.thy。

単純なプロパティが機能しませんでした。たとえば、次数は-2x *2の次数に等しい2x

レンマを証明するにはどうすればよいですか (つまり、「申し訳ありません」を削除します):

.

マヌエルの答えから、私が探していた解決策:

私はすでに楽しみbubble_mainが注文されていることを証明しようとしましたが、どのアプローチも機能していないようです. ここで誰かが補題を証明するのを手伝ってくれませんかis_ordered (bubble_main L)。

イザベルが証明を見つけるのに役立つものはないように見えるので、以前の補題をすべて削除しました。ここに私のコード/理論があります:

Cartesian_Euclidean_Space(ディレクトリ HOL/Multivariate_Analysis内) に行列乗算の定義があります。

これで、二乗行列は になりA ** A、A^3 は になりますA ** A ** A。

定義する累乗関数が見つかりませんでしたA^n (つまり、A ** A ** ... ** An 回)。

ライブラリに累乗関数はありますか? 手動定義は必要ですか?

Metisは私に警告を出します：

この警告はどういう意味ですか? これは、メティスプルーフが警告なしよりも「音が少ない」ことを示していますか?

証明することに困惑している

イザベルで。明らかにあなたができる

しかし、ルールを使用してこれをどのように証明できますか?

または、使用されているルールをダンプする方法はありsimpますか? ありがとう。