isabelle - 伊莎贝尔：与“intro impI”相反

Question

如果我的目标状态是foo ==> bar --> qux，我知道我可以使用该语句

apply (intro impI)

让出目标状态foo ==> bar ==> qux。另一个方向呢？哪个命令会让我回到目标状态foo ==> bar --> qux？

---

到目前为止我想出的最好的是

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar")

但这很笨拙，我想知道是否有更好的方法。

Answer 1

代替

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar")

你可以写

apply (erule_tac P="bar" in rev_mp)

whereerule_tac为您消除了匹配的假设，因此您不再需要thin_tac了。

Answer 2

我假设你想留在apply-style。那么这只是一个可能有许多可能解决方案的难题。这是一个：

apply (unfold atomize_imp, rule)

或者更明确一点

apply (unfold atomize_imp, rule impI)

其中unfold atomize_imp替换所有出现的==>by -->。然后，一般来说，您可以指定-->应该用==>（从左边开始）替换的数字，用相应的数字rule（或rule impI）替换。

无论如何，如果您使用Isar 风格，那么您只需明确说明您想要拥有的内容，几乎任何自动工具都可以填写其余部分。