3

Isabelle では、中間タイプの項が証明の正確性にとって重要である証明の目標を達成できることがよくあります。たとえば、nat42 を に変換して'a wordから元に戻す次の補題を考えてみましょう。

theory Test
imports "~~/src/HOL/Word/Word"
begin

lemma "unat (of_nat 42) = 42"
  ...

ここで、このステートメントの真偽は のタイプに依存します。 でof_nat 42ある場合32 word、ステートメントは真であり、 である場合2 word、ステートメントは偽です。

残念ながら、Isabelle にこの中間タイプを表示してもらうことはできないようです。

私は次のことを試しました：

  • declare [[show_types]]
  • declare [[show_sorts]]
  • local_setup {* Config.put show_all_types true *}

すべてが表示されます:

unat (of_nat (42::nat)) = (42::nat)

ピンチでは、次のことができます。

apply (tactic {* (fn t => (tracing (PolyML.makestring (prems_of t)); all_tac t))  *})

の生のダンプを取得しますtermが、もっと良い方法があることを望んでいました。

証明の目標で中間項の型を表示する良い方法はありますか?

4

3 に答える 3

4

Isabelle / jEditでは、追加情報を取得するために、いつでも一定の位置に「コントロールホバー」（つまり、コントロールボタンを押したままマウスをホバーする）できます。のためof_natに

lemma "unat (of_nat 42) = 42"

これにより、

constant "Nat.semiring_1_class.of_nat"
:: nat => 'a word

今、あなたは再帰的に同じことをすることが'aでき'a word、

:: len
free type variable

これは、それ'aが一種であることを示していますlen（controlキーを押しながらクリックするlenと、この型クラスの定義に直接ジャンプできます。これも非常に便利です）。

したがって、あなたの質問に対する答えは次のとおりです。はい、Isabelle/jEditでcontrolキーを押します。

于 2013-03-19T02:28:58.120 に答える
4

この例で Isabelle に unat の型を表示させるには、次のように宣言します。

  declare [[show_types]]
  declare [[show_sorts]]
  declare [[show_consts]]

最後の行は、出力ウィンドウのゴールで使用される各定数の型を出力します。これは、jEdit と ProofGeneral の両方で機能します。

このソリューションには問題があります。 unat が異なるタイプで複数回発生した場合、これらのインスタンスはすべて出力されますが、どのタイプのインスタンスがどのオカレンスであるかはわかりません。ただし、jEdit ホバーを除けば、その解決策はわかりません。

于 2013-03-19T08:56:00.527 に答える
2

コマンドの実行:

setup {* Config.put_global show_all_types true *}

トリックを行うようです。

目標unat (of_nat 3) = 3は恐ろしいものになります（しかし完全です）：

goal (1 subgoal):
 1. (Trueprop::bool => prop)
     ((op =::nat => nat => bool)
       ((unat::'a word => nat)
         ((of_nat::nat => 'a word)
           ((numeral::num => nat)
             ((num.Bit1::num => num) (num.One::num)))))
       ((numeral::num => nat)
         ((num.Bit1::num => num) (num.One::num))))

望んだ通りに。

declare [[show_all_types]]aが機能しないのは興味深いことです。ソースはそうあるべきように見えます。おそらく Isabelle2013 のバグでしょうか?

于 2013-03-19T11:32:27.580 に答える