0

inductive内に実行可能ファイルを作成したいlocale。localeすべてが正常に動作しなければ:

definition "P a b = True"

inductive test :: "'a ⇒ 'a ⇒ bool" where
  "test a a" |
  "test a b ⟹ P b c ⟹ test a c" 

code_pred test .

ただし、 alocaleで同じことを試しても機能しません。

locale localTest
begin
definition "P' a b = True"

inductive test' :: "'a ⇒ 'a ⇒ bool" where
  "test' a a" |
  "test' a b ⟹ P' b c ⟹ test' a c" 

code_pred test' 
end

code_predロケールの行は次のエラーを返します。

Not a constant: test'
4

3 に答える 3

2

別の導入ルールを指定して (isabelle doc codegenセクション 4.2: 別の導入ルールを参照)、解釈を回避できます。これは、パラメーターを持つロケールでも機能します (帰納的に定義されていない定数の場合でも)。パラメータを持つ例の変形：

locale l =
  fixes A :: "'a set"
begin
definition "P a b = True"

inductive test :: "'a ⇒ 'a ⇒ bool" where
  "a ∈ A ⟹ test a a" |
  "test a b ⟹ P b c ⟹ test a c" 
end

新しい定数を導入します

definition "foo A = l.test A"

そして、その導入規則を証明してください (したがって、新しい定数は古い定数に対して健全です)。

lemma [code_pred_intro]:
  "a ∈ A ⟹ foo A a a"
  "foo A a b ⟹ l.P b c ⟹ foo A a c"
  unfolding foo_def by (fact l.test.intros)+

最後に、新しい定数も古い定数に対して完全であることを示す必要があります。

code_pred foo by (unfold foo_def) (metis l.test.simps)
于 2013-03-11T05:23:32.107 に答える
2

ずさんに表現すると、ロケールは、仮想プロパティを満たすいくつかの仮想定数に関連する新しい定数を導入できるようにする抽象化メカニズムですが、コード生成はより具体的です (関数の抽象的な仕様だけでなく、関数を実装するために必要なすべての情報が必要です)。

そのため、コードを生成する前に、まずロケールを解釈する必要があります。もちろん、あなたの例には仮説上の定数とプロパティがないため、解釈は簡単です

interpretation test: localTest .

その後、使用できます

code_pred test.test' .
于 2013-03-10T03:52:39.163 に答える
0

ここでは完全な推測ですが、名前testをtest'に変更したことで混乱が生じたのではないかと思います。code_pred test'( に変更することを検討してくださいcode_pred "test'"。)

于 2013-03-09T22:11:17.987 に答える