# [isabelle] Case distinction on sets

Hi everyone,
with lists, I can do case distinctions, which I cannot do with sets.
Is there any good advice to express case distinctions on sets?
Here is my example. With lists, I can write the following:
case [xâxs. P x] of [] => None
| [y] => Some y
| _ => undefined
I would like to write this down for xs being a set. To prove
equivalence, I will use "set xs". Unfortunately, I cannot use "case"
with a set. The best I could come up with is the following:
let matching_entries = {x â set xs. P x} in
if matching_entries = {} then None else
if ây. matching_entries = {y} then Some (the_elem matching_entries) else
undefined
Is there a nicer and better way to express this?
If xs is distinct, both versions are equivalent (though the proof was
horrible). For the proof I needed some helper lemmas, for example the
following:
lemma "distinct xs â {x. x â set xs â P x} = {x} â
[xâxs . P x] = [x]"
apply(induction xs)
apply(simp)
apply(simp)
apply(case_tac "x=a")
apply simp_all
apply (smt DiffD2 Diff_insert_absorb filter_False insert_compr mem_Collect_eq)
by (smt Collect_cong ball_empty insert_iff mem_Collect_eq)
The lemma seems pretty obvious to me so I didn't want to invest much
time into it. This was the best proof I could come up with. Why can't
the built-in tools such as blast solve this lemma instantly? I could
not replace those two smt calls with other one-line methods. What is
it that makes this lemma so hard for Isabelle?
Thanks for your advice,
Cornelius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*