Re: [isabelle] Unnecessary Transitivity Assumption in Multiset Extension

I have removed the superfluous assumption, thanks.

The AFP entry Decreasing-Diagrams also contains superfluous "trans r" assumptions because it uses one_step_implies_mult. The proofs still work, but the authors may want to update their theories anyway.


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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.