1

私の地元の人々の何人かは、かなりの数の仮定を持っており、データ型に対する帰納法に非常に似ています (それが仮定の由来です)。このようなロケールを解釈する場合、ケースに名前を付けると非常に便利です。次のように動作するようにするにはどうすればよいですか?

locale Foo = 
  fixes P
  assumes 0: "P 0"
  assumes Suc: "P n ⟹ P (Suc n)"

interpretation Foo "λ _ . True"
proof(default)
  case 0 show ?case..
next
  case (Suc n) show ?case ..
qed
4

2 に答える 2

2

メソッドは、メソッド、および をdefault内部的に呼び出します。これらのサポート名はありません ( については、これは2008 年の Isabelle メーリング リストで既に議論されています)。したがって、システムを で動作させる方法はありません。そのスレッドでは、次の 2 つの重要な点について言及しています。ruleunfold_localesintro_classescaseunfold_localescase_namedefault

  1. ロケール階層がフラットである場合、基本的にはロケールの名前であるルールunfold_localesを適用するだけです。ロケールの複雑な階層がある場合、どの解釈が既に利用可能かをチェックし、それに応じてルールを組み合わせます。Foo.introFoo.intro

  2. casesケース名を取得する正規の方法です。

したがって、case_name属性を使用してケース名を手動で取得できます。

interpretation Foo "λ _ . True"
proof(cases rule: Foo.intro[case_names 0 Suc])

もちろん、複数回必要な場合は、定理にケース名をタグ付けすることもできます。

lemmas Foo_intro[case_names 0 Suc] = Foo.intro

でのケース名のサポートの問題unfold_localesは、どのサブゴールがどのロケール継承に由来するかを実装が追跡しないことです。時間があれば、ケース名のサポートを自由に実装してください。

于 2014-10-16T11:57:34.363 に答える