*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] primrec of datatype containing fset*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sun, 9 Jul 2017 13:15:48 +0100*In-reply-to*: <C44A23AF-2B04-43F4-B3D9-C5ACE05699E3@indiana.edu>*References*: <D782803A-301C-473B-BB84-4660FA6D7D7D@indiana.edu> <c16902b46998fc43cef14f8f4d119c06@hupel.info> <405B7CB8-1B4F-4453-A238-51F61ECA0B4A@indiana.edu> <9202b002fd78ec6100e0d7d7312d69d4@hupel.info> <AM4PR0101MB213253F6578699A926A025DDB7A80@AM4PR0101MB2132.eurprd01.prod.exchangelabs.com> <C44A23AF-2B04-43F4-B3D9-C5ACE05699E3@indiana.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Personally, I would suggest something like this: lemma single_le_sumI: assumes "âbâA. a â (f b :: nat)" "finite A" shows "a â (âbâA. f b)" proof - from assms obtain b where "b â A" "a â f b" by blast note this(2) also from âb â Aâ and âfinite Aâ have "f b â (âbâA. f b)" by (intro member_le_sum) auto finally show ?thesis . qed function count :: "val â nat" where "count (VNat n) = 1" | "count (VRel A) = (â(x,y)âfset A. count x + count y)" by pat_completeness auto termination by (relation "measure size") (force simp: less_Suc_eq_le intro: single_le_sumI)+ This reuses the summation function for sets, and I think that will be much nicer to work with than a fold. The termination proof is still a bit messy, unfortunately, and I don't know what can be done about it in general, but at least similar cases should also work with this "one-liner". Manuel On 2017-07-09 12:56, Siek, Jeremy wrote: > Hi Andrei, > > Good catch! > > But now Iâm a bit unsatisfiedâ the function version of count required a fair bit of work and > looks like itâs rather specific, so I may have to repeat this amount of work for every > other recursive function on datatype val. > > I wonder if the termination argument involving fsum could be adapted to ffold? > > Cheers, > Jeremy > > On Jul 9, 2017, at 7:19 AM, Andrei Popescu <A.Popescu at mdx.ac.uk<mailto:A.Popescu at mdx.ac.uk>> wrote: > > > Hi Jeremy and Lars, > > > Special care is needed when recursing through permutative structures like sets and multisets. For example, the primrec version discussed here is _not_ equal to the 'fun' version of 'count', since it recursively collapses the numbers coming from subtrees that happen to have the same count. The 'fun' version is the correct one. > > > All the best, > > > Andrei > > > ________________________________ > From: cl-isabelle-users-bounces at lists.cam.ac.uk<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk> <cl-isabelle-users-bounces at lists.cam.ac.uk<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk>> on behalf of Lars Hupel <hupel at in.tum.de<mailto:hupel at in.tum.de>> > Sent: 09 July 2017 11:28 > To: Siek, Jeremy > Cc: cl-isabelle-users at lists.cam.ac.uk<mailto:cl-isabelle-users at lists.cam.ac.uk> > Subject: Re: [isabelle] primrec of datatype containing fset > >> Thank you for your very thorough answer! It looks like option 1 will > suite >> my needs. > On second thought, I realised that your use of "ffold" is merely to > compute the sum of some things in a set. Luckily, we can make "function" > cope with that. See attachment for a possible solution (also a version with > "primrec" that doesn't use "ffold"). > > Cheers > Lars > > __________________________________________ > Jeremy G. Siek <jsiek at indiana.edu<mailto:jsiek at indiana.edu>> > Associate Professor > School of Informatics and Computing > Indiana University Bloomington > http://homes.soic.indiana.edu/jsiek/ > > >

**References**:**[isabelle] primrec of datatype containing fset***From:*Siek, Jeremy

**Re: [isabelle] primrec of datatype containing fset***From:*Lars Hupel

**Re: [isabelle] primrec of datatype containing fset***From:*Siek, Jeremy

**Re: [isabelle] primrec of datatype containing fset***From:*Lars Hupel

**Re: [isabelle] primrec of datatype containing fset***From:*Andrei Popescu

**Re: [isabelle] primrec of datatype containing fset***From:*Siek, Jeremy

- Previous by Date: Re: [isabelle] primrec of datatype containing fset
- Next by Date: Re: [isabelle] primrec of datatype containing fset
- Previous by Thread: Re: [isabelle] primrec of datatype containing fset
- Next by Thread: Re: [isabelle] primrec of datatype containing fset
- Cl-isabelle-users July 2017 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