區域設置解釋的案例名稱

我的一些本地人有很多假設，非常類似於數據類型的導入（這是假設的來源）。在解釋這樣的語言環境時，命名個案會非常方便。我如何實現以下功能？區域設置解釋的案例名稱

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

來源

2014-10-16 Joachim Breitner

方法default內部調用方法rule,unfold_locales和intro_classes。這些都不支持case名稱（對於unfold_locales，這已在Isabelle mailing list in 2008上討論過）。因此沒有辦法讓case_name系統與default一起使用。該線程提到了很重要的兩點：

如果您的語言環境的層次結構是扁平的，unfold_locales本質上只是將規則應用於Foo.intro其中Foo是語言環境的名稱。如果您有複雜的區域設置層次結構，它會檢查哪些解釋已經可用，並相應地組合.intro規則。
cases是獲取案例名稱的規範方法。
：
```
interpretation Foo "λ _ . True" 
proof(cases rule: Foo.intro[case_names 0 Suc]) 
```
當然，你也可以，如果你需要它多次標記與本案名稱的定理：

因此，您可以用case_name屬性手動獲取區分名

lemmas Foo_intro[case_names 0 Suc] = Foo.intro

unfold_locales中的案例名稱支持問題是，實現不記錄哪個子目標來自哪個區域繼承。如果您有空閒時間，請隨時實施對案例名稱的支持。

來源

2014-10-16 11:57:34

謝謝，特別是指出'Foo.intro'。我有這樣的感覺，但沒有找到它，因爲當我發出'find_theorems Foo'時，這個定理不會出現。 – 2014-10-16 13:53:06

我有同樣的麻煩，因此在下面的答案中使用了尷尬的輔助引理。 – chris 2014-10-16 19:33:35

據我所知方法induct和case負責設置一個名爲案件。因此，我不認爲default會按照你的要求去做。

你可以引入新的規則像

lemma foo_rule [case_names 0 Suc]: 
    assumes "P 0" 
    and "⋀n. P n ⟹ P (Suc n)" 
    shows "foo P" 
    using assms by (simp add: foo_def)

或可替代像

lemmas foo_rule [case_names 0 Suc] = 
    conjI [THEN foo_def [THEN meta_eq_to_obj_eq, THEN iffD2], rule_format]

如果你正是如此傾斜的。然後用

interpretation foo "λ_. True" 
proof (induct rule: foo_rule)

無意中，我發現，宣佈foo_rule [case_names 0 Suc, induct type]讓你忽略規則的名稱，即

interpretation foo "λ_. True" 
proof (induct)

但我能想象，這將打破現有的默認吸納規則。

來源

2014-10-16 11:37:29 chris

區域設置解釋的案例名稱

回答

相關問題