*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Unnecessary Transitivity Assumption in Multiset Extension*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 18 Mar 2016 12:53:34 +0100*In-reply-to*: <87vb4lmezs.fsf@jnx230.uibk.ac.at>*References*: <87vb4lmezs.fsf@jnx230.uibk.ac.at>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.7.0

I have removed the superfluous assumption, thanks.

Tobias On 17/03/2016 14:05, Julian Nagele wrote:

Dear all, recently, when using the multiset extension "mult" from "~~/src/HOL/Library/Multiset", I noticed the following oddity: The lemma lemma one_step_implies_mult: "trans r â J â {#} â âk â set_mset K. âj â set_mset J. (k, j) â r â (I + K, I + J) â mult r" requires transitivity of the underlying order, which I think is not needed here. And indeed the proof of one_step_implies_mult is using one_step_implies_mult_aux by blast and one_step_implies_mult_aux, basically a object-level version of one_step_implies_mult, reads lemma one_step_implies_mult_aux: "âI J K. size J = n â J â {#} â (âk â set_mset K. âj â set_mset J. (k, j) â r) â (I + K, I + J) â mult r" Is this intended? Best, Julian

**Attachment:
smime.p7s**

**References**:**[isabelle] Unnecessary Transitivity Assumption in Multiset Extension***From:*Julian Nagele

- Previous by Date: Re: [isabelle] successful attempt vs failed to apply initial proof method
- Next by Date: [isabelle] PhD and Post-Doc positions at Chalmers
- Previous by Thread: [isabelle] Unnecessary Transitivity Assumption in Multiset Extension
- Next by Thread: [isabelle] Completion for long names inserts quotes
- Cl-isabelle-users March 2016 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