*To*: "C. Diekmann" <diekmann at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Case distinction on sets*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 6 Jul 2015 12:02:46 +0200*In-reply-to*: <CAGbqCMw3Do1fA9sGOTBCz2-SyB_ozO_=w5t6G1zq04=xosnbKQ@mail.gmail.com>*References*: <CAGbqCMw3Do1fA9sGOTBCz2-SyB_ozO_=w5t6G1zq04=xosnbKQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Hi Cornelius,

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)"

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

**References**:**[isabelle] Case distinction on sets***From:*C. Diekmann

- Previous by Date: [isabelle] Case distinction on sets
- Next by Date: [isabelle] PhD Students in Concurrency Theory at Uppsala University
- Previous by Thread: [isabelle] Case distinction on sets
- Next by Thread: [isabelle] PhD Students in Concurrency Theory at Uppsala University
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list