[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.