覚え書き: 集合内での EX (存在限量)

限量子の使いようが、いまひとつ理解しきれていない。 Isabelle の集合の条件部に EX を書くと、 EX の条件を満たすものが列挙される。

lemma "{0, 1, 2, 3, 4} = {u::nat. EX j k. j <= k & k < 3 & u = j + k}"
apply auto
apply (rule_tac x=0 in exI)
apply (rule_tac x=1 in exI)
apply simp
apply (rule_tac x=1 in exI)
apply (rule_tac x=1 in exI)
apply simp
apply (rule_tac x=1 in exI)
apply (rule_tac x=2 in exI)
apply simp
apply (rule_tac x=2 in exI)
apply (rule_tac x=2 in exI)
by simp