Re: [isabelle] Case distinction on sets



Hi Cornelius,

You can simplify your definitions if you split the filtering from the section of the elements. It looks as if you are trying to lift the operation "pick the unique element in a set" into the option monad. So just lift this operaton:

definition the_elem_option :: "'a set => 'a option"
where "the_elem_option A = (if EX1 x. x : A then Some (the_elem A) else None)"

Note that this specification is tighter than yours as the result is None if there are several elements in the set. If you wanted the function to be undefined in a mathematical sense, then this approach is likely to make your life hard anyway, because working with underspecified functions usually causes quite some pain.

Moreover, I've replaces EX x. A = {x} with EX1 x. x : A, because the latter involves more primitive operations on sets than the former. Intuitively, I'd expect better automation for the latter, but I have not tested it.

In general, I recommend that you work only at the level of abstraction that fits your needs. If you want sets (without order on the elements), then stick to the type set (or fset, if you need finiteness) and never talk about lists. If you need the order of the elements in the list, then work with lists and convert them to sets when needed, but do not try to lift the operations from lists to sets when they rely on the order---this normally directly leads to ugly, messy, tedious proofs.

Picking an element from a set is hard for the automated tools, because it involves a tricky mix of rewriting and resolution. Blast can only deal with resolution, but not rewriting, so blast usually does not work well for proofs involving equality. Conversely, the simplifier cannot deal well with underspecified functions (like the_elem).

Hope this helps,
Andreas

On 06/07/15 11:39, C. Diekmann wrote:
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.