代码之家 › 专栏 › 技术社区 › user1868607

如何将标准应用于Isabelle中的所有子目标?

isabelle

0

user1868607 · 技术社区 · 5 年前

我怎么能在伊莎贝尔做到这一点?

0 回复 | 直到 5 年前

1

user9716869 - supports Ukraine 5 年前

我决定加上 peq 对我的回答的评论

如果你导入 HOL-Eisbach.Eisbach 你可以用 apply(allâ¹standardâº)

;

lemma "(A::'a set) = B â§ (C::'a set) = D"
  apply (intro conjI; standard; standard)
  oops

作为附言,我不相信重复使用 standard 被认为是一种很好的风格。例如,对于您的用例,通常我使用

lemma "(A::'a set) = B"
  apply(intro subset_antisym subsetI)
  oops

希望能够很容易地看到如何同时将此方法应用于多个子目标。

伊莎贝尔版本:伊莎贝尔2020