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调用方法rule和。这些都不支持名称（因为，这已经在 2008 年的 Isabelle 邮件列表中讨论过）。所以没有办法让系统工作。该线程提到了两个重要点：unfold_localesintro_classescaseunfold_localescase_namedefault

  1. 如果您的语言环境层次结构是扁平的，则unfold_locales基本上只是应用语言环境名称Foo.intro所在的规则Foo。如果您有复杂的语言环境层次结构，它会检查哪些解释已经可用并.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 回答
1

据我所知方法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-16T11:37:29.533 回答