code_pred in locales

Question

我想在locale內創建一個可執行文件inductive。如果沒有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 . 

然而，當我嘗試同樣的locale，這是行不通的：

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' 

Answer 1

你可以給替代引進規則（見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" 

並證明其引入規則（因此新的常量是健全w.r.t.舊）。

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)+ 

最後，我們必須證明新常數也是完整的w.r.t.舊的：

code_pred foo by (unfold foo_def) (metis l.test.simps) 

Answer 2

完整的猜測在這裏，但我想知道如果重命名test到test'弄糟了你的東西。 （考慮更改code_pred test'到code_pred "test'"。）

Answer 3

草率表達，語言環境是一種抽象機制，允許引入相對於滿足假設性的一些假設的常量新常量，而代碼生成更具體的（你需要所有需要的信息實現一個函數，而不僅僅是它的抽象規範）。

因此，您首先需要解釋一個語言環境，然後才能生成代碼。當然，在你的榜樣，沒有假設常數和特性，從而解釋是微不足道

interpretation test: localTest . 

之後，您可以使用

code_pred test.test' .