私はIsar証明で規則linordered_field_class.frac_leを使用しようとしています。ここでコードスニペットがあります（これは証拠の前の部分に依存するかもしれませんが、それはそうではありません）。 nはnat型です。 ...
then have 4:"2 ≤ (2^(n+1)::real)" by simp
have 1:"(0::real)≤(1::re
イザベルのチュートリアルで演習を行っているうちに、私は混乱するような状況に遭遇しました。リストの前に付ける次の補助定理がとても簡単に証明されるのはなぜですか： lemma ‹count_list xs x = n ⟹ count_list (x # xs) x = Suc n›
by simp
これは追加を伴うものですか？ lemma ‹count_list xs x = n ⟹ c
私は"\<forall>x. \<exists>y.\<forall>(z::real). P x y z"のような目標を持っています。すぐに私が"\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"と結論づけることができるルールはありますか？もしそうでなければ、私はこのタイプの目標をどのように証明するかについての一般的な助言に感謝します。
私はちょうどIsabelleとの最初のステップを開始していますが、定理証明者と証明補助人には新しく、少し失われています。私は主に機能解析や代数への応用に興味があります。ドキュメンテーションを見ましたが、ロケールを使って独自の例を得ようとしていますが、いくつかの非常に基本的な問題に遭遇しました。私のコードは theory MyTheory
imports Main
begin
locale
私はイザベルのチュートリアルに従っています。 25ページでは、素数の定義を参照しています。私はそれを書いた： definition prime :: "nat ⇒ bool" where "prime p ≡ 1 < p ∧ (∀m. m dvd p ⟶ m = 1 ∨ m = p)"
これはイサベルによって受け入れられています。私は value "prime (Suc 0)"
をしようと