Isabelle中的集合推导式与命题逻辑

Isabelle中的集合推导式与命题逻辑

在Isabelle/HOL中，集合推导式（set comprehension）是定义集合的一种强大方式。它们允许我们基于某个条件来构建集合。但是在使用时，有一些细微的区别需要注意，特别是在涉及到多变量的条件时。本文将通过两个示例来探讨这些区别。

示例1：简单集合交集

首先，我们看一个简单的例子：

lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}" by auto

在这个例子中，左边的集合包含所有满足P x的x，而右边的集合包含所有存在某个y使得Q x y成立的x。它们的交集就是所有同时满足P x和Q x y的x。这个命题通过auto自动证明工具可以很容易地被验证。

解释

• 左边：{x | x. P x}表示所有满足条件P x的x构成的集合。
• 右边：{x | x y. (Q x y)}