覚え書き: 集合内での 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